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

Use reflection for all applicable assertions in add, sub, mul

parent f2575d8b
...@@ -1256,7 +1256,7 @@ let madd (a b:t) ...@@ -1256,7 +1256,7 @@ let madd (a b:t)
= qinterp q1 *. p +. qinterp q2 *. p = qinterp q1 *. p +. qinterp q2 *. p
= minterp a y +. minterp b y }; = minterp a y +. minterp b y };
(q,e1) end (q,e1) end
else raise Unknown else (print a; print b; raise Unknown)
end end
let mmul (a b:t) let mmul (a b:t)
...@@ -1486,6 +1486,7 @@ let mp_decision (l: context') (g: equality') : bool ...@@ -1486,6 +1486,7 @@ let mp_decision (l: context') (g: equality') : bool
R.decision (m_ctx l) (m_eq g) R.decision (m_ctx l) (m_eq g)
end end
module TestMP module TestMP
use import LinearDecisionIntMP use import LinearDecisionIntMP
...@@ -1531,8 +1532,6 @@ end ...@@ -1531,8 +1532,6 @@ end
module Fmla module Fmla
use import map.Map use import map.Map
use import int.Int use import int.Int
......
...@@ -150,10 +150,10 @@ ...@@ -150,10 +150,10 @@
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal> </goal>
<goal name="VC sprod.2" expl="exceptional postcondition" proved="true"> <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>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true"> <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> </goal>
</transf> </transf>
</goal> </goal>
...@@ -1132,7 +1132,7 @@ ...@@ -1132,7 +1132,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof> <proof prover="2"><result status="valid" time="0.07"/></proof>
</goal> </goal>
<goal name="VC linear_decision.10" expl="precondition" proved="true"> <goal name="VC linear_decision.10" 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> <proof prover="2"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC linear_decision.11" expl="precondition" proved="true"> <goal name="VC linear_decision.11" expl="precondition" proved="true">
...@@ -1142,24 +1142,24 @@ ...@@ -1142,24 +1142,24 @@
<proof prover="2"><result status="valid" time="0.06"/></proof> <proof prover="2"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="VC linear_decision.13" expl="precondition" proved="true"> <goal name="VC linear_decision.13" 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> <proof prover="2"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC linear_decision.14" expl="precondition" proved="true"> <goal name="VC linear_decision.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal> </goal>
<goal name="VC linear_decision.15" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.19" expl="assertion" proved="true"> <goal name="VC linear_decision.19" expl="assertion" proved="true">
...@@ -1190,10 +1190,10 @@ ...@@ -1190,10 +1190,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal> </goal>
<goal name="VC linear_decision.28" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.29" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.30" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.30" expl="exceptional postcondition" proved="true">
...@@ -1230,10 +1230,10 @@ ...@@ -1230,10 +1230,10 @@
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.41" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.41" 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>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.42" 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>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof> <proof prover="2"><result status="valid" time="0.00"/></proof>
...@@ -1316,19 +1316,19 @@ ...@@ -1316,19 +1316,19 @@
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.68" 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>
<goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.69" 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>
<goal name="VC linear_decision.70" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.71" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.71" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.72" expl="exceptional postcondition" proved="true"> <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> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</transf> </transf>
......
...@@ -100,7 +100,7 @@ module N ...@@ -100,7 +100,7 @@ module N
function l2i (x:limb) : int = Limb.to_int x function l2i (x:limb) : int = Limb.to_int x
function p2i (i:int32) : int = Int32.to_int i function p2i (i:int32) : int = int32'int i
exception Break exception Break
exception Return32 int32 exception Return32 int32
...@@ -656,8 +656,6 @@ module N ...@@ -656,8 +656,6 @@ module N
assert { !c = 0 by !i < sx }; assert { !c = 0 by !i < sx };
lx := get_ofs x !i; lx := get_ofs x !i;
set_ofs r !i !lx; set_ofs r !i !lx;
(*assert { value r !i + (power radix !i) * !c =
value x !i + value y sy };*) (* false without this, cannotreduce with this *)
value_tail r !i; value_tail r !i;
value_tail x !i; value_tail x !i;
assert { value r !i = value x !i + value y sy }; (* true with this, should not be needed *) assert { value r !i = value x !i + value y sy }; (* true with this, should not be needed *)
...@@ -911,14 +909,12 @@ module N ...@@ -911,14 +909,12 @@ module N
assert { value r !i - (power radix !i) * !b = assert { value r !i - (power radix !i) * !b =
value x !i - value y !i }; value x !i - value y !i };
b := borrow; b := borrow;
let ghost k = p2i !i in value_tail r !i;
i := Int32.(+) !i (Int32.of_int 1); value_tail x !i;
value_sub_tail (pelts r) r.offset (r.offset + k); value_tail y !i;
value_sub_tail (pelts x) x.offset (x.offset + k); assert { value r (!i+1) - (power radix (!i+1)) * !b
value_sub_tail (pelts y) y.offset (y.offset + k); = value x (!i+1) - value y (!i+1)
assert { value r !i - (power radix !i) * !b (*by
= value x !i - value y !i
by
value r !i - power radix !i * !b value r !i - power radix !i * !b
= value r k + power radix k * res = value r k + power radix k * res
- power radix !i * !b - power radix !i * !b
...@@ -938,8 +934,9 @@ module N ...@@ -938,8 +934,9 @@ module N
- (value y k + power radix k * !ly) - (value y k + power radix k * !ly)
= value x !i = value x !i
- (value y k + power radix k * !ly) - (value y k + power radix k * !ly)
= value x !i - value y !i = value x !i - value y !i*)
}; };
i := Int32.(+) !i (Int32.of_int 1);
done; done;
!b !b
...@@ -976,14 +973,12 @@ module N ...@@ -976,14 +973,12 @@ module N
assert { value r !i - power radix !i * !b = assert { value r !i - power radix !i * !b =
value x !i - value y !i }; value x !i - value y !i };
b := borrow; b := borrow;
let ghost k = p2i !i in value_tail r !i;
i := Int32.(+) !i one; value_tail x !i;
value_sub_tail (pelts r) r.offset (r.offset + k); value_tail y !i;
value_sub_tail (pelts x) x.offset (x.offset + k); assert { value r (!i+1) - power radix (!i+1) * !b =
value_sub_tail (pelts y) y.offset (y.offset + k); value x (!i+1) - value y (!i+1)
assert { value r !i - power radix !i * !b = (*by
value x !i - value y !i
by
value r !i - power radix !i * !b value r !i - power radix !i * !b
= value r k + power radix k * res = value r k + power radix k * res
- power radix !i * !b - power radix !i * !b
...@@ -1001,7 +996,8 @@ module N ...@@ -1001,7 +996,8 @@ module N
- value y k - power radix k * !ly - value y k - power radix k * !ly
= value x !i = value x !i
- (value y k + power radix k * !ly) - (value y k + power radix k * !ly)
= value x !i - value y !i }; = value x !i - value y !i*) };
i := Int32.(+) !i one;
done; done;
try try
begin while Int32.(<) !i sx do begin while Int32.(<) !i sx do
...@@ -1018,13 +1014,11 @@ module N ...@@ -1018,13 +1014,11 @@ module N
assert { value r !i - power radix !i * !b = assert { value r !i - power radix !i * !b =
value x !i - value y sy }; value x !i - value y sy };
b := borrow; b := borrow;
let ghost k = p2i !i in value_tail r !i;
i := Int32.(+) !i one; value_tail x !i;
value_sub_tail (pelts r) r.offset (r.offset + k); assert { value r (!i+1) - power radix (!i+1) * !b =
value_sub_tail (pelts x) x.offset (x.offset + k); value x (!i+1) - value y sy
assert { value r !i - power radix !i * !b = (*by
value x !i - value y sy
by
value r !i - power radix !i * !b value r !i - power radix !i * !b
= value r k + power radix k * res = value r k + power radix k * res
- (power radix !i) * !b - (power radix !i) * !b
...@@ -1038,7 +1032,8 @@ module N ...@@ -1038,7 +1032,8 @@ module N
= value x k - value y sy = value x k - value y sy
+ (power radix k) * !lx + (power radix k) * !lx
= value x !i = value x !i
- value y sy } - value y sy*) };
i := Int32.(+) !i one;
done; done;
assert { !i = sx } assert { !i = sx }
end end
...@@ -1053,13 +1048,12 @@ module N ...@@ -1053,13 +1048,12 @@ module N
assert { !b = 0 by !i < sx }; assert { !b = 0 by !i < sx };
lx := get_ofs x !i; lx := get_ofs x !i;
set_ofs r !i !lx; set_ofs r !i !lx;
let ghost k = p2i !i in value_tail r !i;
i := Int32.(+) !i (Int32.of_int 1); value_tail x !i;
value_sub_tail (pelts r) r.offset (r.offset + k); assert { value r !i = value x !i - value y sy };
value_sub_tail (pelts x) x.offset (x.offset + k); assert { value r (!i+1) - power radix (!i+1) * !b
assert { value r !i - power radix !i * !b = value x (!i+1) - value y sy
= value x !i - value y sy (*by
by
value r !i + power radix !i * !b value r !i + power radix !i * !b
= value r !i = value r !i
= value r k + power radix k * !lx = value r k + power radix k * !lx
...@@ -1067,8 +1061,9 @@ module N ...@@ -1067,8 +1061,9 @@ module N
= value x k + power radix k * !lx = value x k + power radix k * !lx
so value r k so value r k
= value r k + power radix k * !b = value r k + power radix k * !b
= value x k - value y sy = value x k - value y sy*)
} };
i := Int32.(+) !i (Int32.of_int 1);
done; done;
!b !b
...@@ -1102,7 +1097,7 @@ module N ...@@ -1102,7 +1097,7 @@ module N
(pelts x)[j] = (pelts (old x))[j] } (pelts x)[j] = (pelts (old x))[j] }
label StartLoop in label StartLoop in
lx := get_ofs x !i; lx := get_ofs x !i;
assert { !lx = (pelts ox)[x.offset + !i] }; assert { !lx = (pelts ox)[ox.offset + !i] };
ly := get_ofs y !i; ly := get_ofs y !i;
let res, borrow = sub_with_borrow !lx !ly !b in let res, borrow = sub_with_borrow !lx !ly !b in
set_ofs x !i res; set_ofs x !i res;
...@@ -1114,14 +1109,12 @@ module N ...@@ -1114,14 +1109,12 @@ module N
= (pelts ox)[x.offset + j]}; = (pelts ox)[x.offset + j]};
assert { value x !i - power radix !i * !b = value ox !i - value y !i }; assert { value x !i - power radix !i * !b = value ox !i - value y !i };
b := borrow; b := borrow;
let ghost k = p2i !i in value_tail ox !i;
i := Int32.(+) !i one; value_tail x !i;
value_sub_tail (pelts ox) x.offset (x.offset + k); value_tail y !i;
value_sub_tail (pelts x) x.offset (x.offset + k); assert { value x (!i+1) - power radix (!i+1) * !b =
value_sub_tail (pelts y) y.offset (y.offset + k); value ox (!i+1) - value y (!i+1)
assert { value x !i - power radix !i * !b = (*by value x !i - power radix !i * !b
value ox !i - value y !i
by value x !i - power radix !i * !b
= value x k + power radix k * res = value x k + power radix k * res
- power radix !i * !b - power radix !i * !b
= value x k + power radix k * res = value x k + power radix k * res
...@@ -1138,7 +1131,8 @@ module N ...@@ -1138,7 +1131,8 @@ module N
- value y k - power radix k * !ly - value y k - power radix k * !ly
= value ox !i = value ox !i
- (value y k + power radix k * !ly) - (value y k + power radix k * !ly)
= value ox !i - value y !i }; = value ox !i - value y !i*) };
i := Int32.(+) !i one;
done; done;
try try
begin while Int32.(<) !i sx do begin while Int32.(<) !i sx do
...@@ -1154,7 +1148,7 @@ module N ...@@ -1154,7 +1148,7 @@ module N
(if (Limb.(=) !b limb_zero) then raise ReturnLimb limb_zero); (if (Limb.(=) !b limb_zero) then raise ReturnLimb limb_zero);
label StartLoop2 in label StartLoop2 in
lx := get_ofs x !i; lx := get_ofs x !i;
assert { !lx = (pelts ox)[x.offset + !i] }; assert { !lx = (pelts ox)[ox.offset + !i] };
let res, borrow = sub_with_borrow !lx limb_zero !b in let res, borrow = sub_with_borrow !lx limb_zero !b in
value_sub_update_no_change (pelts x) (x.offset + p2i !i) value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1) (x.offset + p2i !i + 1)
...@@ -1162,15 +1156,13 @@ module N ...@@ -1162,15 +1156,13 @@ module N
set_ofs x !i res; set_ofs x !i res;
assert { value x !i - power radix !i * !b = value ox !i - value y sy }; assert { value x !i - power radix !i * !b = value ox !i - value y sy };
b := borrow; b := borrow;
let ghost k = p2i !i in assert { forall j. !i < j < sx ->
i := Int32.(+) !i one;
assert { forall j. !i <= j < sx ->
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] }; (pelts x)[x.offset + j] = (pelts ox) [x.offset + j] };
value_sub_tail (pelts ox) x.offset (x.offset + k); value_tail ox !i;
value_sub_tail (pelts x) x.offset (x.offset + k); value_tail x !i;
assert { value x !i - power radix !i * !b = assert { value x (!i+1) - power radix (!i+1) * !b =
value ox !i - value y sy value ox (!i+1) - value y sy
by (*by
value x !i - power radix !i * !b value x !i - power radix !i * !b
= value x k + power radix k * res = value x k + power radix k * res
- (power radix !i) * !b - (power radix !i) * !b
...@@ -1184,7 +1176,8 @@ module N ...@@ -1184,7 +1176,8 @@ module N
= value ox k - value y sy = value ox k - value y sy
+ (power radix k) * !lx + (power radix k) * !lx
= value ox !i = value ox !i
- value y sy } - value y sy*) };
i := Int32.(+) !i one;
done; done;
assert { !i = sx }; assert { !i = sx };
!b !b
...@@ -1199,17 +1192,7 @@ module N ...@@ -1199,17 +1192,7 @@ module N
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sx); value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sx);
value_sub_concat (pelts x) x.offset (x.offset + p2i !i) (x.offset + p2i sx); value_sub_concat (pelts x) x.offset (x.offset + p2i !i) (x.offset + p2i sx);
value_sub_concat (pelts ox) x.offset (x.offset + p2i !i) (x.offset + p2i sx); value_sub_concat (pelts ox) x.offset (x.offset + p2i !i) (x.offset + p2i sx);
assert { value x sx = value (old x) sx - value y sy assert { value x sx = value (old x) sx - value y sy };
by value x sx
= value x !i
+ (power radix !i)
* value_sub (pelts ox) (x.offset + !i) (x.offset + sx)
= value ox !i
+ (power radix !i)
* value_sub (pelts ox) (x.offset + !i) (x.offset + sx)
- value y sy
= value_sub (pelts ox) x.offset (x.offset + sx) - value y sy
= value ox sx - value y sy };
n n
end end
end end
...@@ -1463,7 +1446,8 @@ module N ...@@ -1463,7 +1446,8 @@ module N
value_sub_update_no_change (pelts r) ((!rp).offset + p2i sz) 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; set_ofs !rp sz res;
assert { (pelts !rp)[offset !rp + sz] = res = (pelts r)[offset r + (!i + sz)] }; assert { (pelts !rp)[offset !rp + sz] = res
= (pelts r)[offset r + (!i + sz)] };
c:= carry; c:= carry;
assert { value r !i = value (r at BeforeCarry) !i assert { value r !i = value (r at BeforeCarry) !i
= value (r at StartLoop) !i}; = value (r at StartLoop) !i};
...@@ -1598,13 +1582,6 @@ module N ...@@ -1598,13 +1582,6 @@ module N
let lr = ref limb_zero in let lr = ref limb_zero in
let c = ref limb_zero in let c = ref limb_zero in
let i = ref (Int32.of_int 0) in let i = ref (Int32.of_int 0) in
let rec lemma old_tail_shift (i:int)
requires { i >= 0 }
variant { i }
ensures { value (old r) (i+1) = value (old r) i
+ power radix i * (pelts (old r))[r.offset+i] }
=
if i > 0 then old_tail_shift (i-1) else assert {1+2=3} in
while Int32.(<) !i sz do while Int32.(<) !i sz do
invariant { 0 <= !i <= sz } invariant { 0 <= !i <= sz }
invariant { value r (!i + sz) invariant { value r (!i + sz)
...@@ -1615,21 +1592,16 @@ module N ...@@ -1615,21 +1592,16 @@ module N
invariant { r.data = (!rp).data } invariant { r.data = (!rp).data }
invariant { 0 <= !c <= 1 } invariant { 0 <= !c <= 1 }
invariant { forall j. (!rp).offset + sz <= j -> invariant { forall j. (!rp).offset + sz <= j ->
(pelts (old r)) [j] = (pelts r)[j] } (pelts (old r)) [j] = (pelts r)[j] }
variant { sz - !i } variant { sz - !i }
label StartLoop in label StartLoop in
let ghost k = p2i !i in value_concat r !i (!i+sz);
value_sub_concat (pelts r) r.offset (r.offset + k) assert { value !rp sz
(r.offset + k + p2i sz); = value_sub (pelts r) (r.offset + !i) (r.offset + (!i + sz)) };
assert { value r k
+ (power radix k) * value_sub (pelts r) (r.offset + k)
(r.offset + k + sz)
= value r (k + sz) };
ly := get_ofs y !i; ly := get_ofs y !i;
let c' = addmul_limb !rp x !ly sz in let c' = addmul_limb !rp x !ly sz in
assert { value !rp sz + power radix sz * c' assert { value !rp sz + power radix sz * c'
= value (!rp at StartLoop) sz = value (!rp at StartLoop) sz + value x sz * !ly };
+ value x sz * !ly };
assert { MapEq.map_eq_sub (pelts r) (pelts r at StartLoop) assert { MapEq.map_eq_sub (pelts r) (pelts r at StartLoop)
r.offset (!rp).offset r.offset (!rp).offset
by (!rp).offset = r.offset + !i by (!rp).offset = r.offset + !i
...@@ -1639,7 +1611,7 @@ module N ...@@ -1639,7 +1611,7 @@ module N
so (pelts !rp)[j] = (pelts !rp at StartLoop)[j] so (pelts !rp)[j] = (pelts !rp at StartLoop)[j]
= (pelts r at StartLoop)[j]) }; = (pelts r at StartLoop)[j]) };
lr := get_ofs !rp sz; lr := get_ofs !rp sz;
assert { !lr = (pelts (old r))[r.offset+ !i + sz] }; assert { !lr = (pelts (old r))[(old r).offset + (!i + sz)] };
let (res, carry) = add_with_carry c' !lr !c in let (res, carry) = add_with_carry c' !lr !c in
label BeforeCarry in label BeforeCarry in
value_sub_update_no_change (pelts r) ((!rp).offset + p2i sz) value_sub_update_no_change (pelts r) ((!rp).offset + p2i sz)
...@@ -1647,21 +1619,25 @@ module N ...@@ -1647,21 +1619,25 @@ module N
set_ofs !rp sz res; set_ofs !rp sz res;
assert { value !rp sz = value (!rp at BeforeCarry) sz }; assert { value !rp sz = value (!rp at BeforeCarry) sz };
c:= carry; c:= carry;
i := Int32.(+) !i one; assert { value r !i = value (r at BeforeCarry) !i
assert { value r k = value (r at BeforeCarry) k = value (r at StartLoop) !i};
= value (r at StartLoop) k}; value_tail r (!i+sz);
value_sub_tail (pelts r) r.offset (r.offset + p2i sz + k); value_tail y !i;
value_sub_tail (pelts y) y.offset (y.offset + k); assert { value (old r) ((!i+sz)+1)
old_tail_shift (k+p2i sz); = value (old r) (!i+sz) + power radix (!i+sz) * !lr };
value_sub_concat (pelts r) r.offset (r.offset + k) (r.offset + k + p2i sz); assert { (pelts r)[r.offset + (!i + sz)] = res };
assert { value_sub (pelts r) (r.offset+k) (r.offset+k+sz) value_concat r !i (!i+sz);
assert { value_sub (pelts r) (r.offset + !i) (r.offset+(!i+sz))
= value !rp sz }; = value !rp sz };
assert { value r (!i + sz) assert { value x sz * value y (!i+1)
+ (power radix (!i + sz)) * !c = value x sz * value y !i + power radix !i * (value x sz * !ly) };
= value (old r) (!i + sz) (* nonlinear *)
assert { value r (!i + sz + 1)
+ (power radix (!i + sz + 1)) * !c
= value (old r) (!i + sz + 1)
+ value x sz + value x sz
* value y !i * value y (!i + 1)