Commit b7d720e3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Convert some more examples.

parent 1b197bd7
...@@ -79,8 +79,8 @@ end ...@@ -79,8 +79,8 @@ end
(** Mergesort. (** Mergesort.
This implementation splits the input list in two according to even- and This implementation splits the input list in two according to even- and
odd-order elements (see function [split] below). Thus it is not stable. odd-order elements (see function `split` below). Thus it is not stable.
For a stable implementation, see below module [OCamlMergesort]. *) For a stable implementation, see below module `OCamlMergesort`. *)
module Mergesort module Mergesort
...@@ -124,8 +124,8 @@ end ...@@ -124,8 +124,8 @@ end
- all functions are tail recursive. To avoid the extra cost of - all functions are tail recursive. To avoid the extra cost of
List.rev, sort is duplicated in two versions that respectively List.rev, sort is duplicated in two versions that respectively
sort in order and in reverse order ([sort] and [sort_rev]) and sort in order and in reverse order (`sort` and `sort_rev`) and
merge is duplicated as well ([rev_merge] and [rev_merge_rev]). merge is duplicated as well (`rev_merge` and `rev_merge_rev`).
Note: this is a stable sort, but stability is not proved here. Note: this is a stable sort, but stability is not proved here.
*) *)
...@@ -214,8 +214,8 @@ module OCamlMergesort ...@@ -214,8 +214,8 @@ module OCamlMergesort
| Nil -> absurd | Nil -> absurd
end end
(** [sort n l] sorts [prefix n l] (** `sort n l` sorts `prefix n l`
and [rev_sort n l] sorts [prefix n l] in reverse order. *) and `rev_sort n l` sorts `prefix n l` in reverse order. *)
use import mach.int.Int use import mach.int.Int
......
...@@ -11,9 +11,9 @@ module Add ...@@ -11,9 +11,9 @@ module Add
use import types.Types use import types.Types
use import lemmas.Lemmas use import lemmas.Lemmas
(** [add_limb r x y sz] adds to [x] the value of the limb [y], (** `add_limb r x y sz` adds to `x` the value of the limb `y`,
writes the result in [r] and returns the carry. [r] and [x] writes the result in `r` and returns the carry. `r` and `x`
have size [sz]. This corresponds to the function [mpn_add_1] *) have size `sz`. This corresponds to the function `mpn_add_1` *)
(* r and x must be separated. This is enforced by Why3 regions in typing *) (* r and x must be separated. This is enforced by Why3 regions in typing *)
let add_limb (r x:t) (y:limb) (sz:int32) : limb let add_limb (r x:t) (y:limb) (sz:int32) : limb
requires { valid x sz } requires { valid x sz }
...@@ -87,8 +87,8 @@ module Add ...@@ -87,8 +87,8 @@ module Add
end end
(** [add_limbs r x y sz] adds [x[0..sz-1]] and [y[0..sz-1]] and writes the result in [r]. (** `add_limbs r x y sz` adds `x[0..sz-1]` and `y[0..sz-1]` and writes the result in `r`.
Returns the carry, either [0] or [1]. Corresponds to the function [mpn_add_n]. *) Returns the carry, either `0` or `1`. Corresponds to the function `mpn_add_n`. *)
let add_limbs (r x y:t) (sz:int32) : limb let add_limbs (r x y:t) (sz:int32) : limb
requires { valid x sz } requires { valid x sz }
...@@ -152,9 +152,9 @@ module Add ...@@ -152,9 +152,9 @@ module Add
done; done;
!c !c
(** [add r x y sx sy] adds [(x, sx)] to [(y,sy)] and writes the (** `add r x y sx sy` adds `(x, sx)` to `(y, sy)` and writes the
result in [(r, sx)]. [sx] must be greater than or equal to result in `(r, sx)`. `sx` must be greater than or equal to
[sy]. Returns carry, either 0 or 1. Corresponds to [mpn_add]. *) `sy`. Returns carry, either 0 or 1. Corresponds to `mpn_add`. *)
let add (r x y:t) (sx sy:int32) : limb let add (r x y:t) (sx sy:int32) : limb
requires { 0 <= sy <= sx } requires { 0 <= sy <= sx }
requires { valid x sx } requires { valid x sx }
...@@ -422,9 +422,9 @@ module Add ...@@ -422,9 +422,9 @@ module Add
use import int.EuclideanDivision use import int.EuclideanDivision
(** [incr x y sz] adds to [x] the value of the limb [y] in place. (** `incr x y sz` adds to `x` the value of the limb `y` in place.
[x] has size [sz]. The addition must not overflow. This corresponds `x` has size `sz`. The addition must not overflow. This corresponds
to [mpn_incr] *) to `mpn_incr` *)
let incr (x:t) (y:limb) (ghost sz:int32) : unit let incr (x:t) (y:limb) (ghost sz:int32) : unit
requires { valid x sz } requires { valid x sz }
requires { sz > 0 } requires { sz > 0 }
...@@ -482,9 +482,9 @@ module Add ...@@ -482,9 +482,9 @@ module Add
so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]}; so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz) value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz)
(** [incr_1 x sz] adds 1 to [x] in place. (** `incr_1 x sz` adds 1 to `x` in place.
[x] has size [sz]. The addition must not overflow. `x` has size `sz`. The addition must not overflow.
This corresponds to [mpn_incr] *) This corresponds to `mpn_incr` *)
let incr_1 (x:t) (ghost sz:int32) : unit let incr_1 (x:t) (ghost sz:int32) : unit
requires { valid x sz } requires { valid x sz }
requires { sz > 0 } requires { sz > 0 }
......
...@@ -13,7 +13,8 @@ module Compare ...@@ -13,7 +13,8 @@ module Compare
function compare_int (x y:int) : int = function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1 if x < y then -1 else if x=y then 0 else 1
(** [compare_same_size] compares [x[0..sz-1]] and [y[0..sz-1]] as unsigned integers. It corresponds to [GMPN_CMP]. *) (** `compare_same_size` compares `x[0..sz-1]` and `y[0..sz-1]` as unsigned integers.
It corresponds to `GMPN_CMP`. *)
let compare_same_size (x y:t) (sz:int32) : int32 let compare_same_size (x y:t) (sz:int32) : int32
requires { valid x sz } requires { valid x sz }
requires { valid y sz } requires { valid y sz }
......
...@@ -318,9 +318,9 @@ module Div ...@@ -318,9 +318,9 @@ module Div
assert { !qh * d + !r = ul + radix * uh }; assert { !qh * d + !r = ul + radix * uh };
(!qh,!r) (!qh,!r)
(** [divmod_1 q x y sz] divides [(x,sz)] by [y], writes the quotient (** `divmod_1 q x y sz` divides `(x, sz)` by `y`, writes the quotient
in [(q, sz)] and returns the remainder. Corresponds to in `(q, sz)` and returns the remainder. Corresponds to
[mpn_divmod_1]. *) `mpn_divmod_1`. *)
(* TODO develop further decimal points (qxn) *) (* TODO develop further decimal points (qxn) *)
let divmod_1 (q x:t) (y:limb) (sz:int32) : limb let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
requires { valid x sz } requires { valid x sz }
...@@ -1241,10 +1241,10 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -1241,10 +1241,10 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let u2, b2 = sub_with_borrow u1 z limb_zero in let u2, b2 = sub_with_borrow u1 z limb_zero in
(u2, (Limb.(+) b1 b2)) (u2, (Limb.(+) b1 b2))
(** [submul_limb r x y sz] multiplies [(x, sz)] by [y], substracts the [sz] (** `submul_limb r x y sz` multiplies `(x, sz)` by `y`, subtracts the `sz`
least significant limbs from [(r, sz)] and writes the result in [(r,sz)]. least significant limbs from `(r, sz)` and writes the result in `(r, sz)`.
Returns the most significant limb of the product plus the borrow Returns the most significant limb of the product plus the borrow
of the substraction. Corresponds to [mpn_submul_1].*) of the subtraction. Corresponds to `mpn_submul_1`.*)
let submul_limb (r x:t) (y:limb) (sz:int32):limb let submul_limb (r x:t) (y:limb) (sz:int32):limb
requires { valid x sz } requires { valid x sz }
requires { valid r sz } requires { valid r sz }
...@@ -1363,7 +1363,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -1363,7 +1363,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
done; done;
!b !b
(* [(x,sz)] is normalized if its most significant bit is set. *) (* `(x, sz)` is normalized if its most significant bit is set. *)
predicate normalized (x:t) (sz:int32) = predicate normalized (x:t) (sz:int32) =
valid x sz valid x sz
/\ (pelts x)[x.offset + sz - 1] >= div radix 2 /\ (pelts x)[x.offset + sz - 1] >= div radix 2
...@@ -3722,9 +3722,9 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ...@@ -3722,9 +3722,9 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
(* val sub_limb_in_place (x:t) (y:limb) (sz:int32) : limb*) (* val sub_limb_in_place (x:t) (y:limb) (sz:int32) : limb*)
(** [div_qr q r x y sx sy] divides [(x,sx)] by [(y,sy)], writes the quotient (** `div_qr q r x y sx sy` divides `(x, sx)` by `(y, sy)`, writes the quotient
in [(q, (sx-sy))] and the remainder in [(r, sy)]. Corresponds to in `(q, (sx-sy))` and the remainder in `(r, sy)`. Corresponds to
[mpn_tdiv_qr]. *) `mpn_tdiv_qr`. *)
let div_qr (q r x y nx ny:t) (sx sy:int32) : unit let div_qr (q r x y nx ny:t) (sx sy:int32) : unit
requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) } requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) }
requires { valid x sx } requires { valid x sx }
......
...@@ -6,7 +6,7 @@ module Lemmas ...@@ -6,7 +6,7 @@ module Lemmas
use map.Const use map.Const
use import int.Int use import int.Int
(** {3 complements to map standard library} *) (** {3 Complements to map standard library} *)
predicate map_eq_sub_shift (x y:map int 'a) (xi yi sz:int) = predicate map_eq_sub_shift (x y:map int 'a) (xi yi sz:int) =
forall i. 0 <= i < sz -> x[xi+i] = y[yi+i] forall i. 0 <= i < sz -> x[xi+i] = y[yi+i]
...@@ -63,8 +63,8 @@ module Lemmas ...@@ -63,8 +63,8 @@ module Lemmas
(** {3 Integer value of a natural number} *) (** {3 Integer value of a natural number} *)
(** [value_sub x n m] denotes the integer represented by (** `value_sub x n m` denotes the integer represented by
the digits x[n..m-1] with lsb at index n *) the digits `x[n..m-1]` with lsb at index n *)
let rec ghost function value_sub (x:map int limb) (n:int) (m:int) : int let rec ghost function value_sub (x:map int limb) (n:int) (m:int) : int
variant {m - n} variant {m - n}
= =
......
...@@ -113,9 +113,9 @@ module Logical ...@@ -113,9 +113,9 @@ module Logical
}; };
r r
(** [lshift r x sz cnt] shifts [(x,sz)] [cnt] bits to the left and (** `lshift r x sz cnt` shifts `(x, sz)` `cnt` bits to the left and
writes the result in [(r, sz)]. Returns the [cnt] most significant writes the result in `(r, sz)`. Returns the `cnt` most significant
bits of [(x, sz)]. Corresponds to [mpn_lshift]. *) bits of `(x, sz)`. Corresponds to `mpn_lshift`. *)
(*TODO overlapping allowed if r >= x*) (*TODO overlapping allowed if r >= x*)
let lshift (r x:t) (sz:int32) (cnt:limb) : limb let lshift (r x:t) (sz:int32) (cnt:limb) : limb
requires { 0 < cnt < Limb.length } requires { 0 < cnt < Limb.length }
...@@ -252,9 +252,9 @@ module Logical ...@@ -252,9 +252,9 @@ module Logical
value_sub_head (pelts r) r.offset (r.offset + p2i sz); value_sub_head (pelts r) r.offset (r.offset + p2i sz);
retval retval
(** [rshift r x sz cnt] shifts [(x,sz)] [cnt] bits to the right and (** `rshift r x sz cnt` shifts `(x, sz)` `cnt` bits to the right and
writes the result in [(r, sz)]. Returns the [cnt] least significant writes the result in `(r, sz)`. Returns the `cnt` least significant
bits of [(x, sz)]. Corresponds to [mpn_rshift]. *) bits of `(x, sz)`. Corresponds to `mpn_rshift`. *)
(*TODO overlapping allowed if r <= x*) (*TODO overlapping allowed if r <= x*)
let rshift (r x:t) (sz:int32) (cnt:limb) : limb let rshift (r x:t) (sz:int32) (cnt:limb) : limb
requires { valid x sz } requires { valid x sz }
......
...@@ -14,9 +14,9 @@ module Mul ...@@ -14,9 +14,9 @@ module Mul
use import add.Add use import add.Add
(** [mul_limb r x y sz] multiplies [x[0..sz-1]] by the limb [y] and (** `mul_limb r x y sz` multiplies `x[0..sz-1]` by the limb `y` and
writes the n least significant limbs in [r], and returns the most writes the n least significant limbs in `r`, and returns the most
significant limb. It corresponds to [mpn_mul_1]. *) significant limb. It corresponds to `mpn_mul_1`. *)
let mul_limb (r x:t) (y:limb) (sz:int32) : limb let mul_limb (r x:t) (y:limb) (sz:int32) : limb
requires { valid x sz } requires { valid x sz }
requires { valid r sz } requires { valid r sz }
...@@ -91,10 +91,10 @@ module Mul ...@@ -91,10 +91,10 @@ module Mul
done; done;
!c !c
(** [addmul_limb r x y sz] multiplies [(x, sz)] by [y], adds the [sz] (** `addmul_limb r x y sz` multiplies `(x, sz)` by `y`, adds the `sz`
least significant limbs to [(r, sz)] and writes the result in [(r,sz)]. least significant limbs to `(r, sz)` and writes the result in `(r, sz)`.
Returns the most significant limb of the product plus the carry Returns the most significant limb of the product plus the carry
of the addition. Corresponds to [mpn_addmul_1].*) of the addition. Corresponds to `mpn_addmul_1`.*)
let addmul_limb (r x:t) (y:limb) (sz:int32):limb let addmul_limb (r x:t) (y:limb) (sz:int32):limb
requires { valid x sz } requires { valid x sz }
requires { valid r sz } requires { valid r sz }
...@@ -214,9 +214,9 @@ module Mul ...@@ -214,9 +214,9 @@ module Mul
done; done;
!c !c
(** [mul_limbs r x y sz] multiplies [(x, sz)] and [(y, sz)] and (** `mul_limbs r x y sz` multiplies `(x, sz)` and `(y, sz)` and
writes the result to [(r, 2*sz)]. [r] must not overlap with either writes the result to `(r, 2*sz)`. `r` must not overlap with either
[x] or [y]. Corresponds to [mpn_mul_n]. *) `x` or `y`. Corresponds to `mpn_mul_n`. *)
let mul_limbs (r x y:t) (sz:int32) : unit let mul_limbs (r x y:t) (sz:int32) : unit
requires { sz > 0 } requires { sz > 0 }
requires { valid x sz } requires { valid x sz }
...@@ -479,9 +479,9 @@ module Mul ...@@ -479,9 +479,9 @@ module Mul
done; done;
!c !c
(** [mul r x y sx sy] multiplies [(x, sx)] and [(y,sy)] and writes (** `mul r x y sx sy` multiplies `(x, sx)` and `(y,sy)` and writes
the result in [(r, sx+sy)]. [sx] must be greater than or equal to the result in `(r, sx+sy)`. `sx` must be greater than or equal to
[sy]. Corresponds to [mpn_mul]. *) `sy`. Corresponds to `mpn_mul`. *)
let mul (r x y:t) (sx sy:int32) : unit let mul (r x y:t) (sx sy:int32) : unit
requires { 0 < sy <= sx } requires { 0 < sy <= sx }
requires { valid x sx } requires { valid x sx }
......
...@@ -12,9 +12,9 @@ module Sub ...@@ -12,9 +12,9 @@ module Sub
use import lemmas.Lemmas use import lemmas.Lemmas
(** [sub_limb r x y sz] substracts [y] from [(x, sz)] and writes (** `sub_limb r x y sz` subtracts `y` from `(x, sz)` and writes
the result to [(r, sz)]. Returns borrow, either 0 or the result to `(r, sz)`. Returns borrow, either 0 or
1. Corresponds to [mpn_sub_1]. *) 1. Corresponds to `mpn_sub_1`. *)
let sub_limb (r x:t) (y:limb) (sz:int32) : limb let sub_limb (r x:t) (y:limb) (sz:int32) : limb
requires { valid x sz } requires { valid x sz }
requires { valid r sz } requires { valid r sz }
...@@ -87,9 +87,9 @@ module Sub ...@@ -87,9 +87,9 @@ module Sub
!b !b
end end
(** [sub_limbs r x y sz] substracts [(y, sz)] from [(x, sz)] and (** `sub_limbs r x y sz` subtracts `(y, sz)` from `(x, sz)` and
writes the result to [(r, sz)]. Returns borrow, either 0 or writes the result to `(r, sz)`. Returns borrow, either 0 or
1. Corresponds to [mpn_sub_n]. *) 1. Corresponds to `mpn_sub_n`. *)
let sub_limbs (r x y:t) (sz:int32) : limb let sub_limbs (r x y:t) (sz:int32) : limb
requires { valid x sz } requires { valid x sz }
requires { valid y sz } requires { valid y sz }
...@@ -153,9 +153,9 @@ module Sub ...@@ -153,9 +153,9 @@ module Sub
done; done;
!b !b
(** [sub r x y sx sy] substracts [(y,sy)] from [(x, sx)] and writes the (** `sub r x y sx sy` subtracts `(y,sy)` from `(x, sx)` and writes the
result in [(r, sx)]. [sx] must be greater than or equal to result in `(r, sx)`. `sx` must be greater than or equal to
[sy]. Returns borrow, either 0 or 1. Corresponds to [mpn_sub]. *) `sy`. Returns borrow, either 0 or 1. Corresponds to `mpn_sub`. *)
let sub (r x y:t) (sx sy:int32) : limb let sub (r x y:t) (sx sy:int32) : limb
requires { 0 <= sy <= sx } requires { 0 <= sy <= sx }
requires { valid x sx } requires { valid x sx }
...@@ -418,9 +418,9 @@ module Sub ...@@ -418,9 +418,9 @@ module Sub
end end
end end
(** [decr x y sz] subtracts from [x] the value of the limb [y] in place. (** `decr x y sz` subtracts from `x` the value of the limb `y` in place.
[x] has size [sz]. The subtraction must not overflow. This corresponds `x` has size `sz`. The subtraction must not overflow. This corresponds
to [mpn_decr] *) to `mpn_decr` *)
let decr (x:t) (y:limb) (ghost sz:int32) : unit let decr (x:t) (y:limb) (ghost sz:int32) : unit
requires { valid x sz } requires { valid x sz }
requires { sz > 0 } requires { sz > 0 }
...@@ -480,9 +480,9 @@ module Sub ...@@ -480,9 +480,9 @@ module Sub
so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]}; so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz) value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz)
(** [incr_1 x sz] subtracts 1 from [x] in place. (** `incr_1 x sz` subtracts 1 from `x` in place.
[x] has size [sz]. The subtraction must not overflow. `x` has size `sz`. The subtraction must not overflow.
This corresponds to [mpn_decr] *) This corresponds to `mpn_decr` *)
let decr_1 (x:t) (ghost sz:int32) : unit let decr_1 (x:t) (ghost sz:int32) : unit
requires { valid x sz } requires { valid x sz }
requires { sz > 0 } requires { sz > 0 }
......
...@@ -42,7 +42,7 @@ module Util ...@@ -42,7 +42,7 @@ module Util
i := Int32.(+) !i one; i := Int32.(+) !i one;
done done
(* [is_zero] checks if [x[0..sz-1]] is zero. It corresponds to [mpn_zero_p]. *) (* `is_zero` checks if `x[0..sz-1]` is zero. It corresponds to `mpn_zero_p`. *)
let is_zero (x:t) (sz:int32) : int32 let is_zero (x:t) (sz:int32) : int32
requires { valid x sz } requires { valid x sz }
ensures { 0 <= Int32.to_int result <= 1 } ensures { 0 <= Int32.to_int result <= 1 }
...@@ -75,7 +75,7 @@ module Util ...@@ -75,7 +75,7 @@ module Util
with Return32 r -> r with Return32 r -> r
end end
(** [zero r sz] sets [(r,sz)] to zero. Corresponds to [mpn_zero]. *) (** `zero r sz` sets `(r,sz)` to zero. Corresponds to `mpn_zero`. *)
let zero (r:t) (sz:int32) : unit let zero (r:t) (sz:int32) : unit
requires { valid r sz } requires { valid r sz }
ensures { value r sz = 0 } ensures { value r sz = 0 }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment