...
 
Commits (7)
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
......@@ -9,115 +9,115 @@
<file proved="true">
<path name=".."/><path name="compare.mlw"/>
<theory name="Compare" proved="true">
<goal name="VC wmpn_cmp" expl="VC for wmpn_cmp" proved="true">
<goal name="wmpn_cmp&#39;VC" expl="VC for wmpn_cmp" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_cmp.0" expl="loop invariant init" proved="true">
<goal name="wmpn_cmp&#39;VC.0" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="10"/></proof>
</goal>
<goal name="VC wmpn_cmp.1" expl="loop invariant init" proved="true">
<goal name="wmpn_cmp&#39;VC.1" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="2528"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
<goal name="VC wmpn_cmp.2" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="39"/></proof>
<goal name="wmpn_cmp&#39;VC.2" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="40"/></proof>
</goal>
<goal name="VC wmpn_cmp.3" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="46"/></proof>
<goal name="wmpn_cmp&#39;VC.3" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="47"/></proof>
</goal>
<goal name="VC wmpn_cmp.4" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
<goal name="wmpn_cmp&#39;VC.4" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="28"/></proof>
</goal>
<goal name="VC wmpn_cmp.5" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="15"/></proof>
<goal name="wmpn_cmp&#39;VC.5" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC wmpn_cmp.6" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="27"/></proof>
<goal name="wmpn_cmp&#39;VC.6" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
<goal name="VC wmpn_cmp.7" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="27"/></proof>
<goal name="wmpn_cmp&#39;VC.7" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="40"/></proof>
</goal>
<goal name="VC wmpn_cmp.8" expl="precondition" proved="true">
<goal name="wmpn_cmp&#39;VC.8" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="25754"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="19"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="25"/></proof>
</goal>
<goal name="VC wmpn_cmp.9" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="20"/></proof>
<goal name="wmpn_cmp&#39;VC.9" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="31"/></proof>
</goal>
<goal name="VC wmpn_cmp.10" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="50"/></proof>
<goal name="wmpn_cmp&#39;VC.10" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="64"/></proof>
</goal>
<goal name="VC wmpn_cmp.11" expl="precondition" proved="true">
<goal name="wmpn_cmp&#39;VC.11" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="26287"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="22"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="36"/></proof>
</goal>
<goal name="VC wmpn_cmp.12" expl="precondition" proved="true">
<goal name="wmpn_cmp&#39;VC.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="26553"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="23"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="40"/></proof>
</goal>
<goal name="VC wmpn_cmp.13" expl="precondition" proved="true">
<goal name="wmpn_cmp&#39;VC.13" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_cmp.14" expl="assertion" proved="true">
<goal name="wmpn_cmp&#39;VC.14" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.14.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="35"/></proof>
<goal name="wmpn_cmp&#39;VC.14.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="57"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_cmp.15" expl="assertion" proved="true">
<goal name="wmpn_cmp&#39;VC.15" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_cmp.15.0" expl="VC for wmpn_cmp" proved="true">
<goal name="wmpn_cmp&#39;VC.15.0" expl="VC for wmpn_cmp" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_cmp.15.1" expl="VC for wmpn_cmp" proved="true">
<goal name="wmpn_cmp&#39;VC.15.1" expl="VC for wmpn_cmp" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="35714"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_cmp.16" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="32862"/></proof>
<goal name="wmpn_cmp&#39;VC.16" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="32863"/></proof>
</goal>
<goal name="VC wmpn_cmp.17" expl="assertion" proved="true">
<goal name="wmpn_cmp&#39;VC.17" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="27093"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="25"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="45"/></proof>
</goal>
<goal name="VC wmpn_cmp.18" expl="precondition" proved="true">
<goal name="wmpn_cmp&#39;VC.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_cmp.19" expl="assertion" proved="true">
<goal name="wmpn_cmp&#39;VC.19" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.19.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
<goal name="wmpn_cmp&#39;VC.19.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="58"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_cmp.20" expl="assertion" proved="true">
<goal name="wmpn_cmp&#39;VC.20" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_cmp.20.0" expl="VC for wmpn_cmp" proved="true">
<goal name="wmpn_cmp&#39;VC.20.0" expl="VC for wmpn_cmp" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_cmp.20.1" expl="VC for wmpn_cmp" proved="true">
<goal name="wmpn_cmp&#39;VC.20.1" expl="VC for wmpn_cmp" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="35648"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_cmp.21" expl="postcondition" proved="true">
<goal name="wmpn_cmp&#39;VC.21" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="51439"/></proof>
</goal>
<goal name="VC wmpn_cmp.22" expl="loop variant decrease" proved="true">
<goal name="wmpn_cmp&#39;VC.22" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="27871"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="19"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="VC wmpn_cmp.23" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="19"/></proof>
<goal name="wmpn_cmp&#39;VC.23" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="VC wmpn_cmp.24" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
<goal name="wmpn_cmp&#39;VC.24" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="VC wmpn_cmp.25" expl="precondition" proved="true">
<goal name="wmpn_cmp&#39;VC.25" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="43"/></proof>
</goal>
<goal name="VC wmpn_cmp.26" expl="postcondition" proved="true">
<goal name="wmpn_cmp&#39;VC.26" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="28886"/></proof>
</goal>
</transf>
......
......@@ -323,6 +323,7 @@ module Div
let wmpn_divrem_1 (q x:t) (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
......@@ -1179,6 +1180,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
let wmpn_submul_1 (r x:t) (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 }
......@@ -1303,6 +1305,8 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
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)
......@@ -1352,7 +1356,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
if (not (qh = 0))
then begin
assert { qh = 1 };
let ghost b = wmpn_sub_in_place xd sy y sy in
let ghost b = wmpn_sub_n_in_place xd y sy in
begin
ensures { value (x at PreAdjust) sx =
(value !qp (sx - sy - !i)
......@@ -1537,6 +1541,7 @@ 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))
......@@ -2382,7 +2387,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
so 0 <= j < xc.Array.length
} ;
value_sub_frame (pelts x) xc.elts x.offset (x.offset + p2i !i);
let c = wmpn_add_in_place xd (sy - 1) y (sy - 1) in
let c = wmpn_add_n_in_place xd y (sy - 1) in
begin
ensures { value x !i
= value (x at Adjust) !i }
......@@ -3099,6 +3104,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
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)
......@@ -3185,6 +3191,7 @@ 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))
......@@ -3339,7 +3346,9 @@ 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 }
......@@ -3964,6 +3973,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
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
......@@ -3985,6 +3995,8 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
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
......@@ -4610,6 +4622,7 @@ let wmpn_divrem_1 (q x:t) (sz:int32) (y:limb) : limb
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
......
This diff is collapsed.
......@@ -149,6 +149,7 @@ let lsl_mod_ext [@extraction:inline] (x 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)) }
......@@ -172,6 +173,7 @@ 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 }
......@@ -285,6 +287,7 @@ let lsl_mod_ext [@extraction:inline] (x cnt: limb) : limb
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)) }
=
......@@ -308,6 +311,7 @@ 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 }
......@@ -366,6 +370,7 @@ 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 }
......@@ -396,6 +401,7 @@ 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 ->
......@@ -460,6 +466,7 @@ 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
......@@ -489,6 +496,7 @@ 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 ->
......
This diff is collapsed.
This diff is collapsed.
......@@ -20,6 +20,7 @@ module Mul
let wmpn_mul_1 (r x:t) (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)
......@@ -41,6 +42,7 @@ 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 }
......@@ -85,6 +87,7 @@ module Mul
let wmpn_addmul_1 (r x:t) (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 }
......@@ -108,6 +111,7 @@ 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 }
......@@ -165,6 +169,7 @@ module Mul
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
......@@ -187,6 +192,7 @@ 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 }
......@@ -266,6 +272,7 @@ module Mul
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)
......@@ -293,6 +300,7 @@ 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 }
......
This diff is collapsed.
......@@ -138,6 +138,8 @@ module Powm
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] }
......@@ -162,6 +164,7 @@ 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 }
......@@ -340,7 +343,7 @@ module Powm
if cy <> 0
then begin
assert { cy = 1 };
let ghost b = wmpn_sub_in_place rp n mp n in
let ghost b = wmpn_sub_n_in_place rp mp n in
assert { value rp n + power radix n * (cy - b)
= (value rp n at Sub + power radix n * cy) - vm };
assert { b = 1
......@@ -474,11 +477,13 @@ module Powm
else if eb <= 28161 then 9
else 10
let redcify [@extraction:c_static_inline] (rp up: t) (un: int32) (mp: t) (n: int32)
let redcify [@extraction:c_static_inline]
(rp up: t) (un: int32) (mp: t) (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) }
=
......@@ -1087,6 +1092,7 @@ module Powm
(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 }
......@@ -1220,6 +1226,7 @@ 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) }
......@@ -1540,7 +1547,7 @@ module Powm
if (wmpn_cmp rp mp n >= 0)
then begin
label Sub in
let ghost _b = wmpn_sub_in_place rp n mp n in
let ghost _b = wmpn_sub_n_in_place rp mp n in
assert { _b = 0
by value rp n - power radix n * _b
= value rp n at Sub - vm
......
......@@ -44,6 +44,7 @@ val rsa_estimate (a: fxp): fxp
let sqrt1 (rp: ptr uint64) (a0: uint64): uint64
requires { valid rp 1 }
requires { 0x4000000000000000 <= a0 }
requires { writable rp }
ensures { result * result <= a0 < (result + 1) * (result + 1) }
ensures { result * result + (pelts rp)[offset rp] = a0 }
ensures { (pelts rp)[offset rp] <= 2 * result }
......
# this is a prelude for Gappa
# this is a prelude for Gappa integer arithmetic
# this is a prelude for Gappa real arithmetic
{ @FIX(k,0) ->
@FIX(radix,0) ->
@FIX(max,0) ->
not x - (fixed<k,dn>(x) + pow10_2dt0_lpfrom_int10_k1rp) >= 0 }
......@@ -37,6 +37,7 @@ module Sqrt
requires { valid sp 1 }
requires { valid np 2 }
requires { (pelts np)[offset np + 1] >= power 2 (Limb.length - 2) }
requires { writable sp /\ writable rp }
ensures { value np 2
= (pelts sp)[offset sp] * (pelts sp)[offset sp]
+ result * radix + (pelts rp)[offset rp] }
......@@ -245,6 +246,7 @@ module Sqrt
requires { 1 <= n }
requires { valid scratch (1 + div n 2) }
requires { (pelts np)[offset np + n + n - 1] >= power 2 (Limb.length - 2) }
requires { writable sp /\ writable scratch /\ writable np }
requires { 4 * n < max_int32 }
(* writes { np, sp, scratch }*)
ensures { (value sp n) * (value sp n)
......@@ -333,7 +335,7 @@ module Sqrt
<= 2 * value spl h
so value np' h < power radix h
so value np' h + value np' h < 2 * value spl h };
let ghost b = wmpn_sub_in_place np' h spl h in
let ghost b = wmpn_sub_n_in_place np' spl h in
assert { b = 1 };
assert { value np' h = r' - value spl h
by value np' h - power radix h = value np' h at Sub - value spl h
......@@ -463,7 +465,7 @@ module Sqrt
assert { n1 + power radix l * r'
= 2 * value spl h * (value sp l + power radix l * q)
+ value spl h + value npl h };
let c' = wmpn_add_in_place npl h spl h in
let c' = wmpn_add_n_in_place npl spl h in
c <- to_int64 c';
end
end;
......@@ -524,7 +526,7 @@ module Sqrt
label Sub2 in
let ghost onp = pure { np } in
value_concat np ll n;
let bo = wmpn_sub_in_place np ll npn ll in
let bo = wmpn_sub_n_in_place np npn ll in
value_concat np ll n;
value_sub_frame (pelts np) (pelts onp) (offset np + int32'int ll)
(offset np + int32'int n);
......@@ -853,6 +855,7 @@ module Sqrt
requires { valid sp (ceilhalf n) }
requires { valid rp n }
requires { valid np n }
requires { writable sp /\ writable rp /\ writable np }
requires { 1 <= n }
requires { 4 * n < max_int32 }
requires { (pelts np)[offset np + n - 1] > 0 }
......
This diff is collapsed.
This diff is collapsed.
......@@ -46,6 +46,7 @@ let rec wmpn_toom22_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
requires { 0 < k <= 64 }
requires { sx <= toom22_threshold * power 2 k }
requires { valid scratch (2 * (sx + k)) } (*TODO faire en fonction de sy *)
requires { writable r /\ writable scratch }
requires { 8 * sx < max_int32 }
requires { 2 < sy <= sx < sy + sy - 1 }
requires { 4 * sx < 5 * sy }
......@@ -246,7 +247,7 @@ let rec wmpn_toom22_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
let ghost hvinf = value vinfn (int32'int s + int32'int t- int32'int n) in
assert { lv0 + m * hv0 = a0 * b0 };
assert { lvinf + m * hvinf = a1 * b1 };
let cy = ref (wmpn_add_in_place vinf n v0n n) in (*TODO wmpn_add_n_in_place*)
let cy = ref (wmpn_add_n_in_place vinf v0n n) in
assert { value vinf n = lvinf + hv0 - m * !cy };
let c = wmpn_add_n v0n vinf v0 n in
let cy2 = c + !cy in
......@@ -302,7 +303,7 @@ let rec wmpn_toom22_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
assert { power radix (n+n) = m * m };
if !vm1_neg
then
let c'' = wmpn_add_in_place v0n (n+n) scratch (n+n) in
let c'' = wmpn_add_n_in_place v0n scratch (n+n) in
assert { value v0n (n+n)
= value v0n (n+n) at AddSub + value scratch (n+n)
- power radix (n+n) * c'' };
......@@ -318,7 +319,7 @@ let rec wmpn_toom22_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
= a1 * b1 + a0 * b0 - (a0 - a1)*(b0 - b1)
+ hv0 + m * lvinf - m * cy2 - m * m * !cy }
else
let b = wmpn_sub_in_place v0n (n+n) scratch (n+n) in
let b = wmpn_sub_n_in_place v0n scratch (n+n) in
assert { value v0n (n+n)
= value v0n (n+n) at AddSub - value scratch (n+n)
+ power radix (n+n) * b };
......@@ -783,6 +784,7 @@ with wmpn_toom22_mul_rec (r x: ptr limb) (sx:int32) (y:ptr limb) (sy: int32)
requires { valid x sx }
requires { valid y sy }
requires { valid r (sx + sy) }
requires { writable r /\ writable scratch }
requires { 0 < sy <= sx <= sy + sy }
requires { 8 * sx < max_int32 }
requires { 0 <= k <= 64 }
......@@ -812,6 +814,7 @@ with wmpn_toom22_mul_n_rec (r x y scratch: ptr limb) (sz:int32) (ghost k: int) :
requires { valid x sz }
requires { valid y sz }
requires { valid r (sz + sz) }
requires { writable r /\ writable scratch }
requires { 0 < sz }
requires { 8 * sz < max_int32 }
requires { 0 <= k <= 64 }
......@@ -839,6 +842,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
requires { valid x sx }
requires { valid y sy }
requires { valid r (sx + sy) }
requires { writable r /\ writable scratch }
requires { toom22_threshold < sy }
requires { 0 < k <= 64 }
requires { sx <= toom22_threshold * power 2 k }
......@@ -930,7 +934,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
end;
label Addx1 in
assert { value xp1 n + m * !xp1_hi = a0 + a2 };
let c = wmpn_add_in_place xp1 n x1 n in
let c = wmpn_add_n_in_place xp1 x1 n in
xp1_hi := !xp1_hi + c;
assert { value xp1 n + m * !xp1_hi = a0 + a2 + a1
by value xp1 n + m * !xp1_hi
......@@ -1025,7 +1029,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
label Adjust1 in
value_concat scratch n (n+n);
assert { pelts scratch = pelts sn };
let c = wmpn_add_in_place sn n yp1 n in
let c = wmpn_add_n_in_place sn yp1 n in
assert { pelts scratch = pelts sn };
value_concat scratch n (n+n);
value_sub_frame_shift (pelts scratch) (pelts sa)
......@@ -1102,7 +1106,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
label Adjust3 in
value_concat scratch n (n+n);
assert { pelts scratch = pelts sn };
let c = wmpn_add_in_place sn n xp1 n in
let c = wmpn_add_n_in_place sn xp1 n in
value_concat scratch n (n+n);
assert { pelts scratch = pelts sn };
value_sub_frame_shift (pelts scratch) (pelts sa)
......@@ -1167,7 +1171,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
by value vm1n n = value_sub (pelts vm1 at HiSplit)
(offset vm1 + n) (offset vm1 + 2*n) };
label HiAdd in
let c = wmpn_add_in_place vm1n n ym1 n in
let c = wmpn_add_n_in_place vm1n ym1 n in
label HiJoin in
let vm1nj = { vm1n } in
join vm1 vm1n;
......@@ -1228,7 +1232,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
by am1_abs = a0 - a1 + a2 /\ bm1_abs = b1 - b0 };
assert { (a0 - a1 + a2) * (b1 - b0) = vx1 -vx0 + vx3 - vx2 };
label Sub in
let b = wmpn_sub_in_place scratch (2*n) vm1 (2*n) in
let b = wmpn_sub_n_in_place scratch vm1 (2*n) in
let r, ghost b' = sub_with_borrow !cy !hi b in
assert { (b' = 0 /\ value scratch (2*n) + m * m * r = 2 * (vx0 + vx2))
by r - radix * b' = !cy - !hi - b
......@@ -1274,7 +1278,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
by am1_abs = a0 - a1 + a2 /\ bm1_abs = b0 - b1 };
assert { (a0 - a1 + a2) * (b0 - b1) = vx0 - vx1 + vx2 - vx3 };
label Add in
let c = wmpn_add_in_place scratch (2*n) vm1 (2*n) in
let c = wmpn_add_n_in_place scratch vm1 (2*n) in
let r, ghost c' = add_with_carry !cy !hi c in
assert { (c' = 0 /\ value scratch (2*n) + (m*m) * r = 2 * (vx0 + vx2))
by r + radix * c' = !cy + !hi + c
......@@ -1390,9 +1394,9 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
then begin
assert { am1_abs*bm1_abs = (a0 - a1 + a2) * (b1 - b0)
= - (vx0 - vx1 + vx2 - vx3) };
let c1 = wmpn_add_in_place scratch n vm1 n in
let c1 = wmpn_add_n_in_place scratch vm1 n in
assert { value scratch n = value scratch n at Vm1 + value vm1 n - m * c1 };
let c2 = wmpn_add_in_place vy1 n vm1n n in
let c2 = wmpn_add_n_in_place vy1 vm1n n in
assert { value vy1 n = value vy1 n at Vm1 + value vm1n n - m * c2};
hi := !hi + c2;
let c3 = wmpn_add_1_in_place vy1 n c1 in
......@@ -1418,9 +1422,9 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
else begin
assert { am1_abs*bm1_abs = (a0 - a1 + a2) * (b0 - b1)
= vx0 - vx1 + vx2 - vx3 };
let b1 = wmpn_sub_in_place scratch n vm1 n in
let b1 = wmpn_sub_n_in_place scratch vm1 n in
assert { value scratch n = value scratch n at Vm1 - value vm1 n + m * b1 };
let b2 = wmpn_sub_in_place vy1 n vm1n n in
let b2 = wmpn_sub_n_in_place vy1 vm1n n in
assert { value vy1 n = value vy1 n at Vm1 - value vm1n n + m * b2 };
hi := !hi + b2;
let b3 = wmpn_sub_1_in_place vy1 n b1 in
......@@ -1511,7 +1515,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
= lvx0 + m * (vvy0 + hvx0 - lvx3) + m * m * (vvy1 - lvx0 - hvx3)
+ m * m * m * (vvy2 - (hvx0 - lvx3)) + m * m * m * m * hvx3 };
label R1 in
let bo1 = wmpn_sub_in_place r1n n r3n n in
let bo1 = wmpn_sub_n_in_place r1n r3n n in
let bo = ref bo1 in
assert { value r1n n - m * bo1 = hvx0 - lvx3 };
let ly2 = get_ofs vy2 n in
......@@ -1522,7 +1526,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
so (power radix n) * ly2 <= value vy2 (n+1) < (power radix n) * 6 };
let h = ref (Limb.to_int64 (ly2 + bo1)) in
label R2 in
let bo2 = wmpn_sub_in_place r2n n r n in
let bo2 = wmpn_sub_n_in_place r2n r n in
let bo2' = wmpn_sub_1_in_place r2n n !bo in
bo := bo2 + bo2';
assert { value r2n n - m * !bo = vvy1 - lvx0 - (!bo at R2) };
......@@ -1761,6 +1765,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
requires { valid x sx }
requires { valid y sy }
requires { valid r (sx + sy) }
requires { writable r }
requires { 0 < sy <= sx }
requires { 8 * sx < max_int32 }
requires { sx <= toom22_threshold * power 2 k }
......@@ -1812,6 +1817,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
invariant { plength !up = plength x }
invariant { min !rp = min r /\ max !rp = max r }
invariant { plength !rp = plength r }
invariant { writable !rp }
invariant { min ws = 0 /\ max ws = plength ws = 4 * sy }
invariant { min scratch = 0 /\ max scratch = plength scratch }
invariant { plength scratch = 5 * sy + 128 }
......@@ -1836,7 +1842,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
value_concat r !ou !or;
assert { value r !or = value r !ou + power radix !ou * value !rp sy };
wmpn_toom32_mul ws !up su y sy scratch k;
let cy = wmpn_add_in_place !rp sy ws sy in
let cy = wmpn_add_n_in_place !rp ws sy in
value_sub_frame (pelts r) (pelts o_r) (offset r) (offset r + p2i !ou);
assert { value r !ou = value o_r !ou };
assert { value !rp sy + (power radix sy) * cy
......@@ -1954,11 +1960,12 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
end
else wmpn_mul ws y sy !up !un (k-1)
end;
let cy = wmpn_add_in_place !rp sy ws sy in
let cy = wmpn_add_n_in_place !rp ws sy in
value_sub_frame (pelts r) (pelts o_r) (offset r) (offset r + p2i !ou);
assert { value r !ou = value o_r !ou };
assert { value !rp sy + (power radix sy) * cy
= value o_rp sy + value ws sy };
assert { valid !rp sy };
let rpn = C.incr !rp sy in
let wsy = C.incr ws sy in
let orp = { rpn } in
......@@ -2097,6 +2104,7 @@ with wmpn_toom32_mul (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
requires { valid x sz }
requires { valid y sz }
requires { valid r (sz + sz) }
requires { writable r }
requires { 8 * sz < max_int32 }
requires { sz <= toom22_threshold * power 2 k }
requires { 0 <= k <= 64 }
......
This diff is collapsed.
This diff is collapsed.