Commit 37735ce6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move predicate 'writable' to the type of 'ptr'.

parent aa97f302
......@@ -15,13 +15,12 @@ module Add
(** `wmpn_add_n 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`. *)
let wmpn_add_n (r x y:ptr limb) (sz:int32) : limb
let wmpn_add_n (r:t) (x:s 'wx) (y:s 'wy) (sz:int32) : limb
requires { 0 <= sz }
requires { valid r sz /\ valid x sz /\ valid y sz }
requires { offset r = offset x \/ offset r + sz <= offset x }
requires { offset r = offset y \/ offset r + sz <= offset y }
requires { r.data = x.data = y.data }
requires { writable r }
alias { r.data with x.data }
alias { r.data with y.data }
alias { x.data with y.data }
......@@ -82,13 +81,12 @@ module Add
(** `wmpn_add r x sx y sy` adds `(x, sx)` to `(y, sy)` and writes the
result in `(r, sx)`. `sx` must be greater than or equal to
`sy`. Returns carry, either 0 or 1. Corresponds to `mpn_add`. *)
let wmpn_add (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
let wmpn_add (r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { offset r = offset x \/ offset r + sx <= offset x }
requires { offset r = offset y \/ offset r + sx <= offset y }
requires { r.data = x.data = y.data }
requires { writable r }
alias { r.data with x.data }
alias { r.data with y.data }
alias { x.data with y.data }
......@@ -188,10 +186,9 @@ module Add
done;
c
let add_n [@extraction:inline] (r x y:ptr limb) (sz:int32) : limb
let add_n [@extraction:inline] (r:t) (x:s 'wx) (y:s 'wy) (sz:int32) : limb
requires { 0 <= sz }
requires { valid r sz /\ valid x sz /\ valid y sz }
requires { writable r }
ensures { value r sz + power radix sz * result
= old (value x sz + value y sz) }
ensures { 0 <= result <= 1 }
......@@ -230,10 +227,9 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_n_rx [@extraction:inline] (x y:ptr limb) (sz:int32) : limb
let add_n_rx [@extraction:inline] (x:t) (y:s 'w) (sz:int32) : limb
requires { 0 <= sz }
requires { valid x sz /\ valid y sz }
requires { writable x }
ensures { value x sz + power radix sz * result
= old (value x sz + value y sz) }
ensures { 0 <= result <= 1 }
......@@ -259,11 +255,9 @@ module Add
= (pelts oy)[offset y + j] };
res
let add [@extraction:inline] (r x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let add [@extraction:inline] (r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { writable r }
ensures { value r sx + power radix sx * result
= old (value x sx + value y sy) }
ensures { 0 <= result <= 1 }
......@@ -302,11 +296,9 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_rx [@extraction:inline] (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let add_rx [@extraction:inline] (x:t) (sx:int32) (y:s 'w) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sy }
requires { writable x }
ensures { value x sx + power radix sx * result
= old (value x sx + value y sy) }
ensures { 0 <= result <= 1 }
......@@ -333,11 +325,9 @@ module Add
= (pelts oy)[offset y + j] };
res
let add_ry [@extraction:inline] (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
let add_ry [@extraction:inline] (x:s 'w) (sx:int32) (y:t) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sx }
requires { writable y }
ensures { value y sx + power radix sx * result
= old (value x sx + value y sy) }
ensures { 0 <= result <= 1 }
......@@ -364,9 +354,8 @@ module Add
= (pelts ox)[offset x + j] };
res
let add_n_rxy [@extraction:inline] (x:ptr limb) (sx:int32) : limb
let add_n_rxy [@extraction:inline] (x:t) (sx:int32) : limb
requires { 0 <= sx }
requires { writable x }
requires { valid x sx }
ensures { value x sx + power radix sx * result
= old (value x sx + value x sx) }
......@@ -400,11 +389,10 @@ module AddOld
use ptralias.Alias
use ref.Ref
let wmpn_add_n (r x y:t) (sz:int32) : limb
let wmpn_add_n (r:t) (x:s 'wx) (y:s 'wy) (sz:int32) : limb
requires { valid x sz }
requires { valid y sz }
requires { valid r sz }
requires { writable r }
ensures { 0 <= result <= 1 }
ensures { value r sz + (power radix sz) * result =
value x sz + value y sz }
......@@ -445,12 +433,11 @@ module AddOld
(** `wmpn_add r x sx y sy` adds `(x, sx)` to `(y, sy)` and writes the
result in `(r, sx)`. `sx` must be greater than or equal to
`sy`. Returns carry, either 0 or 1. Corresponds to `mpn_add`. *)
let wmpn_add (r x:t) (sx:int32) (y:t) (sy:int32) : limb
let wmpn_add (r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
requires { valid r sx }
requires { writable r }
ensures { value r sx + (power radix sx) * result =
value x sx + value y sy }
ensures { forall j. (j < offset r \/ offset r + sx <= j)
......@@ -514,10 +501,9 @@ module AddOld
done;
c
let wmpn_add_n_in_place (x y:t) (sz:int32) : limb
let wmpn_add_n_in_place (x:t) (y:s 'w) (sz:int32) : limb
requires { valid x sz }
requires { valid y sz }
requires { writable x }
ensures { 0 <= result <= 1 }
ensures { value x sz + (power radix sz) * result
= value (old x) sz + value y sz }
......@@ -563,11 +549,10 @@ module AddOld
done;
c
let wmpn_add_in_place (x:t) (sx:int32) (y:t) (sy:int32) : limb
let wmpn_add_in_place (x:t) (sx:int32) (y:s 'w) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
requires { writable x }
ensures { value x sx + (power radix sx) * result
= value (old x) sx + value y sy }
ensures { 0 <= result <= 1 }
......
......@@ -16,11 +16,10 @@ module Add_1
writes the result in `r` and returns the carry. `r` and `x`
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 *)
let wmpn_add_1 (r x:t) (sz:int32) (y:limb) : limb
let wmpn_add_1 (r:t) (x:s 'w) (sz:int32) (y:limb) : limb
requires { valid x sz }
requires { valid r sz }
requires { sz > 0 } (* ? GMP does the same for 0 and 1*)
requires { writable r }
ensures { value r sz + (power radix sz) * result =
value x sz + y }
ensures { 0 <= result <= 1 }
......@@ -92,7 +91,6 @@ module Add_1
requires { valid x sz }
requires { sz > 0 }
requires { value x sz + y < power radix sz }
requires { writable x }
ensures { value x sz = value (old x) sz + y }
ensures { forall j. j < x.offset \/ x.offset + sz <= j ->
(pelts x)[j] = (pelts (old x))[j] }
......@@ -117,7 +115,6 @@ module Add_1
invariant { min xp = min x /\ max xp = max x }
invariant { i = sz -> c = 0 }
invariant { 0 <= c <= 1 }
invariant { writable xp }
invariant { value x i + (power radix i) * c
= value ox i + y }
invariant { forall j. i <= j < sz ->
......@@ -176,7 +173,6 @@ module Add_1
requires { valid x sz }
requires { sz > 0 }
requires { value x sz + 1 < power radix sz }
requires { writable x }
ensures { value x sz = value (old x) sz + 1 }
ensures { forall j. j < x.offset \/ x.offset + sz <= j ->
(pelts x)[j] = (pelts (old x))[j] }
......@@ -197,7 +193,6 @@ module Add_1
invariant { min xp = min x /\ max xp = max x }
invariant { r <> 0 <-> c = 0 }
invariant { 0 <= c <= 1 }
invariant { writable xp }
invariant { value x i + (power radix i) * c
= value ox i + 1 }
invariant { forall j. i <= j < sz ->
......@@ -243,7 +238,6 @@ module Add_1
let wmpn_add_1_in_place (x:t) (sz:int32) (y:limb) : limb
requires { valid x sz }
requires { sz > 0 }
requires { writable x }
ensures { value x sz + (power radix sz) * result = value (old x) sz + y }
ensures { 0 <= result <= 1 }
ensures { forall j. (j < offset x \/ offset x + sz <= j)
......
......@@ -15,7 +15,7 @@ module Compare
(** `wmpn_cmp` compares `x[0..sz-1]` and `y[0..sz-1]` as unsigned integers.
It corresponds to `GMPN_CMP`. *)
let wmpn_cmp (x y:t) (sz:int32) : int32
let wmpn_cmp (x:s 'wx) (y:s 'wy) (sz:int32) : int32
requires { valid x sz }
requires { valid y sz }
ensures { result = compare_int (value x sz) (value y sz) }
......
......@@ -318,12 +318,11 @@ module Div
(** `wmpn_divrem_1 q x sz y` divides `(x, sz)` by `y`, writes the quotient
in `(q, sz)` and returns the remainder. Corresponds to
`mpn_wmpn_divrem_1`. *)
`mpn_divrem_1`. *)
(* TODO develop further decimal points (qxn) *)
let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
let wmpn_divrem_1 (q:t) (x:s 'w) (sz:int32) (y:limb) : limb
requires { valid x sz }
requires { valid q sz }
requires { writable q }
requires { 0 < sz }
requires { 0 < y }
ensures { value x sz
......@@ -1187,10 +1186,9 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
least significant limbs from `(r, sz)` and writes the result in `(r, sz)`.
Returns the most significant limb of the product plus the borrow
of the subtraction. Corresponds to `mpn_submul_1`.*)
let wmpn_submul_1 (r x:t) (sz:int32) (y:limb):limb
let wmpn_submul_1 (r:t) (x:s 'w) (sz:int32) (y:limb):limb
requires { valid x sz }
requires { valid r sz }
requires { writable r }
ensures { value r sz - (power radix sz) * result
= value (old r) sz
- value x sz * y }
......@@ -1307,17 +1305,15 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
!b
(* `(x, sz)` is normalized if its most significant bit is set. *)
predicate normalized (x:t) (sz:int32) =
predicate normalized (x:s 'w) (sz:int32) =
valid x sz
/\ (pelts x)[x.offset + sz - 1] >= div radix 2
let div_sb_qr (q x:t) (sx:int32) (y:t) (sy:int32) : limb
let div_sb_qr (q x:t) (sx:int32) (y:s 'w) (sy:int32) : limb
requires { 3 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
requires { valid q (sx - sy) }
requires { writable q }
requires { writable x }
requires { normalized y sy }
ensures { value (old x) sx =
(value q (sx - sy)
......@@ -1552,7 +1548,6 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
invariant { !xp.max = x.max }
invariant { pelts !qp = pelts q }
invariant { pelts !xp = pelts x }
invariant { writable !qp /\ writable !xp }
invariant { value (old x) sx =
(value !qp (sx - sy - !i)
+ qh * power radix (sx - sy - !i))
......@@ -3109,13 +3104,12 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
+ value x sy };
qh
let wmpn_divrem_2 (q x y:t) (sx:int32) : limb
let wmpn_divrem_2 (q x:t) (y:s 'w) (sx:int32) : limb
requires { 2 <= sx }
requires { valid x sx }
requires { valid y 2 }
requires { valid q (sx - 2) }
requires { (pelts y)[y.offset + 1] >= div radix 2 }
requires { writable q /\ writable x }
ensures { value (old x) sx =
(value q (sx - 2)
+ power radix (sx - 2) * result)
......@@ -3202,7 +3196,6 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
invariant { !xp.min = x.min }
invariant { !xp.max = x.max }
invariant { pelts !xp = pelts x }
invariant { writable !xp }
invariant { value x sx
= (value_sub (pelts q) (q.offset + !i) (q.offset + sx - 2)
+ !qh * power radix (sx - 2 - !i))
......@@ -3349,7 +3342,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
(** `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
`mpn_tdiv_qr`. *)
let div_qr (q r x y nx ny:t) (sx sy:int32) : unit
let div_qr (q r:t) (x:s 'wx) (y:s 'wy) (nx ny:t) (sx sy:int32) : unit
requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) }
requires { valid x sx }
requires { valid y sy }
......@@ -3357,9 +3350,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
requires { valid r sy }
requires { valid nx (sx + 1) }
requires { valid ny sy }
requires { writable nx /\ writable ny }
requires { (pelts y)[y.offset + sy - 1] > 0 }
requires { writable q /\ writable r }
ensures { value x sx
= value q (sx - sy + 1) * value y sy
+ value r sy }
......@@ -3978,13 +3969,12 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
end
end
let wmpn_tdiv_qr (q r x:t) (sx:int32) (y:t) (sy:int32) : unit
let wmpn_tdiv_qr (q r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32) : unit
requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) }
requires { valid x sx }
requires { valid y sy }
requires { valid q (sx - sy + 1) }
requires { valid r sy }
requires { writable q /\ writable r }
requires { (pelts y)[y.offset + sy - 1] > 0 }
ensures { value x sx
= value q (sx - sy + 1) * value y sy
......@@ -3999,15 +3989,13 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
free nx;
free ny
let div_qr_in_place (q x y nx ny:t) (sx sy:int32) : unit
let div_qr_in_place (q x:t) (y:s 'w) (nx ny:t) (sx sy:int32) : unit
requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) }
requires { valid x sx }
requires { valid y sy }
requires { valid q (sx - sy + 1) }
requires { valid nx (sx + 1) }
requires { valid ny sy }
requires { writable q /\ writable x }
requires { writable nx /\ writable ny }
requires { (pelts y)[y.offset + sy - 1] > 0 }
ensures { value (old x) sx
= value q (sx - sy + 1) * value y sy
......@@ -4628,12 +4616,11 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
end
end
let wmpn_tdiv_qr_in_place (q x:t) (sx:int32) (y:t) (sy:int32) : unit
let wmpn_tdiv_qr_in_place (q x:t) (sx:int32) (y:s 'w) (sy:int32) : unit
requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) }
requires { valid x sx }
requires { valid y sy }
requires { valid q (sx - sy + 1) }
requires { writable x /\ writable q }
requires { (pelts y)[y.offset + sy - 1] > 0 }
ensures { value (old x) sx
= value q (sx - sy + 1) * value y sy
......
......@@ -211,17 +211,17 @@ module Lemmas
ensures { value_sub x x1 x2 < power radix (x2-x1-1) * (l2i (Map.get x (x2-1)) + 1) }
= value_sub_upper_bound x x1 (x2-1)
function value (x:t) (sz:int) : int =
function value (x:s 'w) (sz:int) : int =
value_sub (pelts x) x.offset (x.offset + sz)
let lemma value_tail (x:t) (sz:int32)
let lemma value_tail (x:s 'w) (sz:int32)
requires { 0 <= sz }
ensures { value x (sz+1) = value x sz + (pelts x)[x.offset + sz] * power radix sz }
= value_sub_tail (pelts x) x.offset (x.offset + p2i sz)
meta remove_prop axiom value_tail
let lemma value_concat (x:t) (n m:int32)
let lemma value_concat (x:s 'w) (n m:int32)
requires { 0 <= n <= m }
ensures { value x m
= value x n + power radix n
......
......@@ -28,7 +28,8 @@ module Logical
ensures { mod (x * y + z) x = mod z x }
=
()
let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
requires { 0 <= cnt < Limb.length }
ensures { result = mod (x * power 2 cnt) radix }
ensures { result <= radix - power 2 cnt }
......@@ -145,11 +146,10 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
writes the result in `(r, sz)`. Returns the `cnt` most significant
bits of `(x, sz)`. Corresponds to `mpn_wmpn_lshift`. *)
(*TODO overlapping allowed if r >= x*)
let wmpn_lshift (r x:t) (sz:int32) (cnt:limb) : limb
let wmpn_lshift (r:t) (x:s 'w) (sz:int32) (cnt:limb) : limb
requires { 0 < cnt < Limb.length }
requires { valid r sz }
requires { valid x sz }
requires { writable r }
requires { 0 < sz }
ensures { value r sz + (power radix sz) * result =
value x sz * (power 2 (cnt)) }
......@@ -173,7 +173,6 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
invariant { plength !rp = plength r }
invariant { !rp.min = r.min }
invariant { !rp.max = r.max }
invariant { writable !rp }
invariant { pelts !rp = pelts r }
invariant { plength !xp = plength x }
invariant { !xp.min = x.min }
......@@ -282,12 +281,11 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
writes the result in `(r, sz)`. Returns the `cnt` least significant
bits of `(x, sz)`. Corresponds to `mpn_wmpn_rshift`. *)
(*TODO overlapping allowed if r <= x*)
let wmpn_rshift (r x:t) (sz:int32) (cnt:limb) : limb
let wmpn_rshift (r:t) (x:s 'w) (sz:int32) (cnt:limb) : limb
requires { valid x sz }
requires { valid r sz }
requires { 0 < cnt < Limb.length }
requires { 0 < sz }
requires { writable r }
ensures { result + radix * value r sz
= value x sz * (power 2 (Limb.length - cnt)) }
=
......@@ -312,7 +310,6 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
invariant { plength !rp = plength r }
invariant { !rp.min = r.min }
invariant { !rp.max = r.max }
invariant { writable !rp }
invariant { plength !xp = plength x }
invariant { !xp.min = x.min }
invariant { !xp.max = x.max }
......@@ -371,7 +368,6 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
let wmpn_lshift_in_place (x:t) (sz:int32) (cnt:limb) : limb
requires { 0 < cnt < Limb.length }
requires { valid x sz }
requires { writable x }
requires { 0 < sz }
ensures { value x sz + (power radix sz) * result =
value (old x) sz * power 2 cnt }
......@@ -402,7 +398,6 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
invariant { plength !xp = plength x }
invariant { !xp.min = x.min }
invariant { !xp.max = x.max }
invariant { writable !xp }
invariant { pelts !xp = pelts x }
invariant { !high <= radix - c }
invariant { forall j. 0 <= j <= !i ->
......@@ -475,7 +470,6 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
let wmpn_rshift_in_place (x:t) (sz:int32) (cnt:limb) : limb
requires { valid x sz }
requires { writable x }
requires { 0 < cnt < Limb.length }
requires { 0 < sz }
ensures { result + radix * value x sz
......@@ -505,7 +499,6 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
invariant { plength !xp = plength x }
invariant { !xp.min = x.min }
invariant { !xp.max = x.max }
invariant { writable !xp }
invariant { pelts !xp = pelts x }
invariant { !low < c }
invariant { forall j. !i <= j < sz ->
......
......@@ -17,10 +17,9 @@ module Mul
(** `wmpn_mul_1 r x sz y` multiplies `x[0..sz-1]` by the limb `y` and
writes the n least significant limbs in `r`, and returns the most
significant limb. It corresponds to `mpn_mul_1`. *)
let wmpn_mul_1 (r x:t) (sz:int32) (y:limb) : limb
let wmpn_mul_1 (r:t) (x:s 'w) (sz:int32) (y:limb) : limb
requires { valid x sz }
requires { valid r sz }
requires { writable r }
ensures { value r sz + (power radix sz) * result
= value x sz * y }
ensures { forall j. (j < offset r \/ offset r + sz <= j)
......@@ -42,7 +41,6 @@ module Mul
invariant { plength rp = plength r }
invariant { rp.min = r.min }
invariant { rp.max = r.max }
invariant { writable rp }
invariant { pelts rp = pelts r }
invariant { up.offset = x.offset + i }
invariant { plength up = plength x }
......@@ -84,10 +82,9 @@ module Mul
least significant limbs to `(r, sz)` and writes the result in `(r, sz)`.
Returns the most significant limb of the product plus the carry
of the addition. Corresponds to `mpn_addmul_1`.*)
let wmpn_addmul_1 (r x:t) (sz: int32) (y:limb) : limb
let wmpn_addmul_1 (r:t) (x:s 'w) (sz: int32) (y:limb) : limb
requires { valid x sz }
requires { valid r sz }
requires { writable r }
ensures { value r sz + (power radix sz) * result
= value (old r) sz
+ value x sz * y }
......@@ -111,7 +108,6 @@ module Mul
invariant { (rp).offset = r.offset + i }
invariant { rp.min = r.min }
invariant { rp.max = r.max }
invariant { writable rp }
invariant { pelts rp = pelts r }
invariant { up.offset = x.offset + i }
invariant { plength up = plength x }
......@@ -164,12 +160,11 @@ module Mul
done;
cl
let wmpn_addmul_n (r x y:t) (sz:int32) : limb
let wmpn_addmul_n (r:t) (x:s 'wx) (y:s 'wy) (sz:int32) : limb
requires { sz > 0 }
requires { valid x sz }
requires { valid y sz }
requires { valid r (sz + sz) }
requires { writable r }
writes { r.data.elts }
ensures { value r (sz + sz)
+ power radix (sz + sz) * result
......@@ -192,7 +187,6 @@ module Mul
invariant { rp.offset = r.offset + i }
invariant { rp.min = r.min }
invariant { rp.max = r.max }
invariant { writable rp }
invariant { pelts rp = pelts r }
invariant { plength rp = plength r }
invariant { vp.offset = y.offset + i }
......@@ -267,12 +261,11 @@ module Mul
(** `wmpn_mul_basecase r x sx y sy` multiplies `(x, sx)` and `(y,sy)` and writes
the result in `(r, sx+sy)`. `sx` must be greater than or equal to
`sy`. Corresponds to `mpn_mul`. *)
let wmpn_mul_basecase (r x:t) (sx:int32) (y:t) (sy:int32) : unit
let wmpn_mul_basecase (r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32) : unit
requires { 0 < sy <= sx }
requires { valid x sx }
requires { valid y sy }
requires { valid r (sy + sx) }
requires { writable r }
writes { r.data.elts }
ensures { value r (sy + sx) = value x sx * value y sy }
ensures { forall j. (j < offset r \/ offset r + (sy + sx) <= j)
......@@ -300,7 +293,6 @@ module Mul
invariant { rp.min = r.min }
invariant { rp.max = r.max }
invariant { pelts rp = pelts r }
invariant { writable rp }
invariant { vp.offset = y.offset + i }
invariant { plength vp = plength y }
invariant { vp.min = y.min }
......
......@@ -133,13 +133,11 @@ module Powm
meta remove_prop axiom unredc_inv
meta remove_prop axiom unredc
let wmpn_redc_1 (rp up mp : t) (n: int32) (invm : limb)
let wmpn_redc_1 (rp up: t) (mp: s 'w) (n: int32) (invm: limb)
requires { n > 0 }
requires { valid mp n /\ valid up (2 * n) /\ valid rp n }
requires { odd (value mp n) }
requires { mod ((value mp n) * invm) radix = radix - 1 }
requires { writable up }
requires { writable rp }
ensures { redc (value (old up) (2*n)) (value rp n) n (value mp n) }
ensures { forall j. j < offset rp \/ j >= offset rp + n
-> (pelts rp)[j] = (pelts (old rp))[j] }
......@@ -164,7 +162,6 @@ module Powm
invariant { u.min = up.min }
invariant { u.max = up.max }
invariant { plength u = plength up }
invariant { writable u }
(*invariant { mod (value u n + value up j) (power radix j) = 0 }*)
invariant { power radix j * value u (n+n-j) + power radix n * value up j
= value (old up) (n+n) + vm * added }
......@@ -478,12 +475,11 @@ module Powm
else 10
let redcify [@extraction:c_static_inline]
(rp up: t) (un: int32) (mp: t) (n: int32)
(rp: t) (up: s 'wu) (un: int32) (mp: s 'wm) (n: int32)
requires { valid rp n /\ valid up un /\ valid mp n }
requires { 1 <= n /\ 1 <= un }
requires { un + n < max_int32 }
requires { (pelts mp)[offset mp + n - 1] > 0 }
requires { writable rp }
ensures { value rp n = mod (power radix n * value up un) (value mp n) }
ensures { redc (value rp n) (value up un) n (value mp n) }
=
......@@ -505,21 +501,21 @@ module Powm
assert { 0 <= value rp n < value mp n };
assert { mod (value rp n) (value mp n) = value rp n };
function valueb (p:t) (nbits:int) : int
function valueb (p:s 'w) (nbits:int) : int
=
if nbits < 0 then 0 else
let i = div nbits 64 in
value p i
+ power radix i * mod ((pelts p)[offset p + i]) (power 2 (nbits - 64*i))
let lemma valueb_lower_bound (p:t) (nbits:int)
let lemma valueb_lower_bound (p:s 'w) (nbits:int)
ensures { 0 <= valueb p nbits }
= if nbits < 0 then ()
else
let i = div nbits 64 in
value_sub_lower_bound (pelts p) (offset p) (offset p + i)
let lemma valueb_upper_bound (p:t) (nbits:int)
let lemma valueb_upper_bound (p:s 'w) (nbits:int)
requires { 0 <= nbits }
ensures { valueb p nbits < power 2 nbits }
= if nbits < 0 then ()
......@@ -540,7 +536,7 @@ module Powm
= power 2 (64 * i + (nbits - 64 * i))
= power 2 nbits }
let getbit [@extraction:c_static_inline] (p:t) (ghost pn:int32) (bi:int32) : limb
let getbit [@extraction:c_static_inline] (p:s 'w) (ghost pn:int32) (bi:int32) : limb
requires { valid p pn }
requires { 1 <= bi }
requires { pn >= (div (bi + 63) 64) }
......@@ -649,7 +645,7 @@ module Powm
= mod (2 * d + res) 2 = mod res 2 = res };
lps % 2
let getbits [@extraction:c_static_inline] (p: t) (ghost pn: int32) (bi:int32)
let getbits [@extraction:c_static_inline] (p: s 'w) (ghost pn: int32) (bi:int32)
(nbits:int32) : limb
requires { 1 <= nbits < 64 }
requires { 0 <= bi }
......@@ -969,7 +965,7 @@ module Powm
end;
r % (lsl 1 (Limb.of_int32 nbits))
let lemma valueb_mod (p:t) (nbits:int) (n:int32)
let lemma valueb_mod (p:s 'w) (nbits:int) (n:int32)
requires { nbits >= 0 }
requires { 64 * n >= nbits }
ensures { valueb p nbits = mod (value p n) (power 2 nbits) }
......@@ -1033,7 +1029,7 @@ module Powm
= mod (value p (i+1)) (power 2 nbits)
= valueb p nbits }
let lemma valueb_mon (p:t) (pn:int32) (bi1 bi2:int32)
let lemma valueb_mon (p:s 'w) (pn:int32) (bi1 bi2:int32)
requires { 0 <= bi1 <= bi2 }
requires { valid p pn }
requires { pn >= div (bi2 + 63) 64 }
......@@ -1088,11 +1084,10 @@ module Powm
= mod (power radix n * (power radix n * a * b)) m };
unredc c (p * q) (power radix n * (a * b)) n m
let wmpn_powm (rp bp : t) (bn : int32) (ep : t) (en : int32) (mp : t)
let wmpn_powm (rp: t) (bp: s 'wb) (bn: int32) (ep: s 'we) (en: int32) (mp: s 'wm)
(n : int32) (tp : t) : unit
requires { valid rp n /\ valid bp bn /\ valid ep en /\ valid mp n }
requires { valid tp (2*n) }
requires { writable tp /\ writable rp }
requires { odd (value mp n) }
requires { value ep en > 1 }
requires { en >= 1 }
......@@ -1226,7 +1221,6 @@ module Powm
invariant { min this_pp = min pp }
invariant { max this_pp = max pp }
invariant { plength this_pp = plength pp }
invariant { writable this_pp }
invariant { plength tp = plength (tp at Window) }
invariant { min tp = min (tp at Window) }
invariant { max tp = max (tp at Window) }
......
......@@ -14,17 +14,15 @@ module Alias
lr: int32; lx: int32; ly: int32;
mutable ok: bool }
predicate identical (p1 p2:ptr limb) =
predicate identical (p1: s 'w1) (p2: s 'w2) =
data p1 = data p2 /\ offset p1 = offset p2
/\ min p1 = min p2 /\ max p1 = max p2 /\ zone p1 = zone p2
val open_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
val open_sep (r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32) :
(nr:t, nx:s readonly, ny:s readonly, ghost m:mem)
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { writable r }
requires { 0 <= sy <= sx }
ensures { writable nr }
ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
ensures { valid nr sx /\ valid nx sx /\ valid ny sy }
ensures { 0 <= offset nr /\ offset nr + sx <= offset nx
......@@ -47,8 +45,8 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
val close_sep (r:t) (x:s 'wx) (sx:int32) (y:s 'wy) (sy:int32)
(nr:t) (nx ny:s readonly) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
......@@ -58,7 +56,6 @@ module Alias
requires { m.lr = sx /\ m.lx = sx /\ m.ly = sy }
requires { 0 <= offset nr /\ offset nr + sx <= offset nx
/\ offset nx + sx <= offset ny }
requires { writable r /\ writable nr }
ensures { r.max = m.mr /\ x.max = m.mx /\ y.max = m.my }
ensures { map_eq_sub_shift (old pelts nr) (pelts r)
(offset nr) (offset r) sx }
......@@ -78,12 +75,10 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
r.data, r.max, x.data, x.max, y.data, y.max, m.ok }
val open_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
val open_rx (x:t) (sx:int32) (y:s 'w) (sy:int32) :
(nr:t, nx:s readonly, ny:s readonly, ghost m:mem)
requires { valid x sx /\ valid y sy }
requires { 0 <= sy <= sx }
requires { writable x }
ensures { writable nr }
ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
ensures { valid nx sx /\ valid ny sy }
ensures { identical nr nx }
......@@ -103,12 +98,10 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val open_ry (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
val open_ry (x:s 'w) (sx:int32) (y:t) (sy:int32) :
(nr:t, nx:s readonly, ny:s readonly, ghost m:mem)
requires { valid x sx /\ valid y sx }
requires { 0 <= sy <= sx }
requires { writable y }
ensures { writable nr }
ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
ensures { valid nx sx /\ valid ny sx }
ensures { identical nr ny }
......@@ -128,12 +121,10 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val open_rxy (x:ptr limb) (sx:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
val open_rxy (x:t) (sx:int32) :
(nr:t, nx:s readonly, ny:s readonly, ghost m:mem)
requires { valid x sx }
requires { 0 <= sx }
requires { writable x }
ensures { writable nr }
ensures { value nx sx = old value x sx }
ensures { valid nx sx }
ensures { identical nr nx }
......@@ -152,12 +143,11 @@ module Alias
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
val close_rx (x:t) (sx:int32) (y:s 'w) (sy:int32)
(nr:t) (nx ny:s readonly) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
requires { writable x /\ writable nr }
requires { m.ok }
requires { 0 <= sy <= sx }
requires { identical nr nx }
......@@ -178,12 +168,11 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
x.data, x.max, y.data, y.max, m.ok }
val close_ry (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
(nr nx ny:ptr limb) (ghost m:mem) : unit
val close_ry (x:s 'w) (sx:int32) (y:t) (sy:int32)
(nr:t) (nx ny:s readonly) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
requires { writable y /\ writable nr }
requires { m.ok }
requires { 0 <= sy <= sx }
requires { identical nr ny }
......@@ -204,7 +193,7 @@ module Alias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
x.data, x.max, y.data, y.max, m.ok }
val close_rxy (x:ptr limb) (sx:int32) (nr nx ny:ptr limb) (ghost m:mem) : unit
val close_rxy (x:t) (sx:int32) (nr:t) (nx ny:s readonly) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
......@@ -214,7 +203,6 @@ module Alias
requires { identical nr nx }
requires { 0 <= offset nr }
requires { m.zx = x.zone /\ m.lx = sx }
requires { writable x /\ writable nr }
ensures { x.max = m.mx }
ensures { map_eq_sub_shift (old pelts nx) (pelts x)
(offset nx) (offset x) sx }
......
......@@ -41,10 +41,9 @@ val rsa_estimate (a: fxp): fxp
ensures { let rsa = 1. /. sqrt a in
let e0 = (result -. rsa) /. rsa in -0.00281 <=. e0 <=. 0.002655 }
let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
let sqrt1 (rp: ptr uint64 writable) (a0: uint64): uint64