Commit c66c91e5 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Automate most post-decision transformations, finish proofs of mp reflection examples

parent 939eb5a4
......@@ -150,10 +150,10 @@
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sprod.2" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......@@ -359,13 +359,6 @@
<goal name="VC opp_expr.5.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC opp_expr.5.2">
<transf name="compute_in_goal" >
<goal name="VC opp_expr.5.2.0">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC opp_expr.6" expl="postcondition" proved="true">
......@@ -411,12 +404,6 @@
<goal name="VC norm_eq_aux.10" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC norm_eq_aux.5">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC norm_eq_aux.6">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC norm_eq" expl="VC for norm_eq" proved="true">
......@@ -540,12 +527,6 @@
<goal name="VC mul_expr.13" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mul_expr.6">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="VC mul_expr.5">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_expr" expl="VC for add_expr" proved="true">
......@@ -678,66 +659,6 @@
<goal name="VC add_expr.37" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.24">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_expr.28">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_expr.25">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_expr.29">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.17">
<proof prover="0"><result status="valid" time="0.17" steps="99"/></proof>
</goal>
<goal name="VC add_expr.3">
<proof prover="0"><result status="valid" time="0.14" steps="98"/></proof>
</goal>
<goal name="VC add_expr.20">
<proof prover="0"><result status="valid" time="0.04" steps="72"/></proof>
</goal>
<goal name="VC add_expr.5">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC add_expr.19">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC add_expr.23">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC add_expr.22">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC add_expr.27">
<proof prover="0"><result status="valid" time="0.30" steps="269"/></proof>
</goal>
<goal name="VC add_expr.31">
<proof prover="0"><result status="valid" time="0.49" steps="510"/></proof>
</goal>
<goal name="VC add_expr.4">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.18">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.21">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.33">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.32">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_expr.30">
<proof prover="0"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="VC add_expr.26">
<proof prover="0"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_eq" expl="VC for mul_eq" proved="true">
......@@ -784,9 +705,6 @@
<goal name="VC zero_expr.2.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
<goal name="VC zero_expr.2.2">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="VC zero_expr.3" expl="postcondition" proved="true">
......@@ -1165,12 +1083,9 @@
</goal>
<goal name="VC linear_decision.6" expl="index in matrix bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC linear_decision.7" expl="index in matrix bounds" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC linear_decision.8" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -1179,7 +1094,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC linear_decision.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.11" expl="precondition" proved="true">
......@@ -1189,24 +1104,24 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="VC linear_decision.15" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.19" expl="assertion" proved="true">
......@@ -1237,10 +1152,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="VC linear_decision.28" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.29" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.30" expl="exceptional postcondition" proved="true">
......@@ -1277,10 +1192,10 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.41" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
......@@ -1291,11 +1206,9 @@
</goal>
<goal name="VC linear_decision.45" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC linear_decision.46" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC linear_decision.47" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -1365,43 +1278,21 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.70" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.71" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.72" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.10">
<proof prover="0"><result status="valid" time="0.02" steps="79"/></proof>
<proof prover="2"><undone/></proof>
</goal>
<goal name="VC linear_decision.9">
<proof prover="0"><result status="valid" time="0.02" steps="79"/></proof>
<proof prover="2"><undone/></proof>
</goal>
<goal name="VC linear_decision.52">
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
<proof prover="2"><undone/></proof>
</goal>
<goal name="VC linear_decision.51">
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
<proof prover="2"><undone/></proof>
</goal>
<goal name="VC linear_decision.11">
<proof prover="2"><undone/></proof>
</goal>
<goal name="VC linear_decision.53">
<proof prover="2"><undone/></proof>
</goal>
</transf>
</goal>
<goal name="VC valid_expr&#39;" expl="VC for valid_expr'" proved="true">
......@@ -2005,27 +1896,7 @@
<goal name="g.0" proved="true">
<transf name="reflection_f" proved="true" arg1="decision">
<goal name="g.0.0" expl="reification check" proved="true">
<transf name="revert" proved="true" arg1="HR">
<goal name="g.0.0.0" expl="reification check" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g.0.0.0.0" expl="reification check" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="g.0.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.0.2" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.0.3" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
......@@ -2036,27 +1907,7 @@
<goal name="g" proved="true">
<transf name="reflection_f" proved="true" arg1="int_decision">
<goal name="g.0" expl="reification check" proved="true">
<transf name="revert" proved="true" arg1="HR">
<goal name="g.0.0" expl="reification check" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g.0.0.0" expl="reification check" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="g.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.2" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.3" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
......@@ -2632,41 +2483,13 @@
<goal name="g" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="g.0" expl="reification check" proved="true">
<transf name="revert" proved="true" arg1="HR">
<goal name="g.0.0" expl="reification check" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g.0.0.0" expl="reification check" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
</transf>
</goal>
</transf>
<proof prover="0"><result status="valid" time="0.04" steps="23"/></proof>
</goal>
<goal name="g.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="g.2" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.3" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g.3.0" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
</transf>
</goal>
<goal name="g.4" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g.4.0" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
</transf>
</goal>
<goal name="g.5" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
......@@ -2675,30 +2498,13 @@
<goal name="g&#39;.0" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="g&#39;.0.0" expl="reification check" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="23"/></proof>
</goal>
<goal name="g&#39;.0.1" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="g&#39;.0.2" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="g&#39;.0.3" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g&#39;.0.3.0" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
</goal>
<goal name="g&#39;.0.4" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g&#39;.0.4.0" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="g&#39;.0.5" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
......@@ -2711,40 +2517,13 @@
<goal name="g&#39;&#39;.0.0" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="g&#39;&#39;.0.0.0" expl="reification check" proved="true">
<transf name="revert" proved="true" arg1="HR">
<goal name="g&#39;&#39;.0.0.0.0" expl="reification check" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g&#39;&#39;.0.0.0.0.0" expl="reification check" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="29"/></proof>
</goal>
</transf>
</goal>
</transf>
<proof prover="0"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="g&#39;&#39;.0.0.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="g&#39;&#39;.0.0.2" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g&#39;&#39;.0.0.3" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g&#39;&#39;.0.0.3.0" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="g&#39;&#39;.0.0.4" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g&#39;&#39;.0.0.4.0" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="g&#39;&#39;.0.0.5" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
......
......@@ -255,6 +255,16 @@ module N
meta remove_prop axiom value_tail
let lemma value_concat (x:t) (n m:int32)
requires { 0 <= n <= m }
ensures { value x m
= value x n + power radix n
* value_sub (pelts x) (x.offset + n) (x.offset + m) }
= value_sub_concat (pelts x) x.offset (x.offset + p2i n) (x.offset + p2i m)
meta remove_prop axiom value_concat
function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1
......@@ -1409,7 +1419,7 @@ module N
requires { sz > 0 }
requires { valid x sz }
requires { valid y sz }
requires { valid r (sz + sz) }
requires { valid r (sz + sz) }
writes { r.data.elts }
ensures { value r (sz + sz)
= value x sz * value y sz }
......@@ -1433,18 +1443,11 @@ module N
invariant { 0 <= !c <= 1 }
variant { sz - !i }
label StartLoop in
let ghost k = p2i !i in
value_sub_concat (pelts r) r.offset (r.offset + k)
(r.offset + k + p2i sz);
assert { value r k
+ (power radix k) * value_sub (pelts r) (r.offset + k)
(r.offset + k + sz)
= value r (k + sz) };
value_concat r !i (!i + sz);
ly := get_ofs y !i;
let c' = addmul_limb !rp x !ly sz in
assert { value !rp sz + power radix sz * c'
= value (!rp at StartLoop) sz
+ value x sz * !ly };
= value (!rp at StartLoop) sz + value x sz * !ly };
assert { MapEq.map_eq_sub (pelts r) (pelts r at StartLoop)
r.offset (!rp).offset
by (!rp).offset = r.offset + !i
......@@ -1456,30 +1459,33 @@ module N
let (res, carry) = add_with_carry c' limb_zero !c in
label BeforeCarry in
value_sub_update_no_change (pelts r) ((!rp).offset + p2i sz)
r.offset (r.offset + p2i !i) res;
r.offset (r.offset + p2i !i) res;
set_ofs !rp sz res;
assert { (pelts !rp)[offset !rp + sz] = res = (pelts r)[offset r + (!i + sz)] };
c:= carry;
i := Int32.(+) !i one;
assert { value r k = value (r at BeforeCarry) k
= value (r at StartLoop) k};
value_sub_tail (pelts r) r.offset (r.offset + p2i sz + k);
value_sub_tail (pelts y) y.offset (y.offset + k);
value_sub_concat (pelts r) r.offset (r.offset + k) (r.offset + k + p2i sz);
assert { value_sub (pelts r) (r.offset+k) (r.offset+k+sz)
assert { value r !i = value (r at BeforeCarry) !i
= value (r at StartLoop) !i};
value_tail r (!i + sz);
assert { value r (!i + sz + 1) = value r (!i + sz)
+ power radix (!i + sz) * (pelts r)[offset r + (!i + sz)] };
value_tail y !i;
value_concat r !i (!i + sz);
assert { value_sub (pelts r) (r.offset + !i) (r.offset + (!i + sz))
= value !rp sz };
assert { value r (!i + sz)
+ (power radix (!i + sz)) * !c
= value x sz
* value y !i
by (value !rp sz + power radix sz * c'
= value (!rp at StartLoop) sz + value x sz * !ly
by value !rp sz = value (!rp at BeforeCarry) sz)
so power radix (k + sz) = power radix k * power radix sz
so
value (r at StartLoop) k
+ (power radix k) * value_sub (pelts r at StartLoop)
(r.offset + k) (r.offset + k + sz)
= value (r at StartLoop) (k + sz)
assert { value !rp sz = value (!rp at BeforeCarry) sz };
assert { value !rp sz + power radix sz * c'
= value (!rp at StartLoop) sz + value x sz * !ly };
assert { value (r at StartLoop) !i
+ (power radix !i) * value_sub (pelts r at StartLoop)
(r.offset + !i) (r.offset + (!i + sz))
= value (r at StartLoop) (!i + sz) };
assert { value x sz * value y (!i + 1)
= value x sz * value y !i + (power radix !i) * (value x sz * !ly) };
(* nonlinear *)
assert { value r (!i + sz + 1)
+ (power radix (!i + sz + 1)) * !c
= value x sz * value y (!i+1)
(*by power radix (k + sz) = power radix k * power radix sz
so
value r (!i + sz)
+ (power radix (!i + sz)) * !c
......@@ -1543,8 +1549,9 @@ module N
+ power radix k * value x sz * !ly
= value x sz *
(value y k + power radix k * !ly)
= value x sz * value y !i
= value x sz * value y !i *)
};
i := Int32.(+) !i one;
rp.contents <- C.incr !rp one;
done;
value_sub_lower_bound (pelts r) r.offset (r.offset + p2i sz + p2i sz);
......@@ -1893,11 +1900,10 @@ module N
let lsld_ext (x cnt:limb) : (limb,limb)
requires { 0 <= cnt < Limb.length }
returns { (r,d) -> l2i r + radix * l2i d =
(power 2 (cnt)) * x }
returns { (r,_d) -> mod (l2i r) (power 2 (cnt)) = 0 }
returns { (r,_d) -> l2i r <= radix - (power 2 (cnt)) }
returns { (_r,d) -> l2i d < power 2 (cnt) }
returns { (r,d) -> uint64'int r + radix * uint64'int d = (power 2 cnt) * x }
returns { (r,_d) -> mod (l2i r) (power 2 cnt) = 0 }
returns { (r,_d) -> l2i r <= radix - (power 2 cnt) }
returns { (_r,d) -> l2i d < power 2 cnt }
=
let uzero = Limb.of_int 0 in
if (Limb.(=) cnt uzero) then (x, uzero)
......@@ -2148,7 +2154,6 @@ module N
invariant { pelts !xp = pelts x }
invariant { !low < power 2 (tnc) }
label StartLoop in
let ghost k = p2i !i in
xp.contents <- C.incr !xp one;
high := C.get !xp;
let l,h = lsld_ext !high tnc in
......@@ -2156,15 +2161,17 @@ module N
let ghost v = Limb.(+) !low l in
value_sub_shift_no_change (pelts r) r.offset (p2i !i) (p2i !i) v;
C.set !rp (Limb.(+) !low l);
assert { value r k = value (r at StartLoop) k };
rp.contents <- C.incr !rp one;
assert { value r !i = value (r at StartLoop) !i };
value_tail r !i;
value_tail x (!i+1);
assert { (pelts r)[r.offset + !i] = !low + l };
low := h;
let ghost k = p2i !i in
i := Int32.(+) !i one;
value_sub_tail (pelts r) r.offset (r.offset + k);
value_sub_tail (pelts x) x.offset (x.offset + p2i !i);
(*todo let c = power 2 tnc in... replace occurences by c and try reflection*)
assert { retval + radix * (value r !i