Commit 0ffc2ae5 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

cleanup proof; moved two instructions back to original position

parent 70d2f1bd
......@@ -283,21 +283,15 @@ ensures { uint 6 reg 14 = old (uint 3 reg 2*uint 3 reg 5) }
S.modify_r24(); S.modify_r25();
end;
(* TODO optimize/analyse me? *)
(* S.init(); *)
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 48 = old (uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 3 reg 11 + pow2 24*uint 3 reg 20) }
(*
ensures { old(uint 3 reg 8) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 72 = (pow2 24+1)*(at(uint 3 reg 2*uint 3 reg 5)'L00 + at(pow2 24*uint 3 reg 14*uint 3 reg 17)'L11) }
*)
(* TODO *)
ensures { reg[26] = if old(reg[26] = reg[27]) then 0xFF else 0x00 }
'Pre:
(* ;--- process sign bit --- *)
(* original location
eor r26 r27;
com r26;
*)
(* ;--- add l3+h0 to l0 and h3 --- *)
add r8 r11;
adc r9 r12;
......@@ -305,27 +299,20 @@ ensures { old(uint 3 reg 8) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf
adc r11 r20;
adc r12 r21;
adc r13 r22;
S.modify_r26();
S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13();
end;
(* S.init(); *)
abstract
ensures { S.synchronized S.shadow reg }
(*
ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) + (if old (reg[26] = 0x00 <-> reg[27] = 0x00) then -1 else 1)*old(uint 6 reg 14) }
*)
ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) + (if old (reg[26] = reg[27]) then -1 else 1)*old(uint 6 reg 14) }
ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) + (if old (reg[26] = 0xFF) then -1 else 1)*old(uint 6 reg 14) }
ensures { let cor = reg[23] + (pow2 8+pow2 16)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 24 + old ?cf - ?cf }
(* ; merge carry and borrow *)
'B:
eor r26 r27; (* moved here *)
com r26;
assert { reg[26] = if at(reg[26] = reg[27])'B then 0xFF else 0x00 };
adc r23 r26;
mov r0 r23;
asr r0;
'B:
(* ; invert all bits or do nothing *)
eor r14 r26;
eor r15 r26;
......@@ -357,25 +344,31 @@ S.modify_r11(); S.modify_r12(); S.modify_r13();
S.modify_r20(); S.modify_r21(); S.modify_r22();
end;
(* the following 3 asserts establish a bounds result about multiplying uint's -- can't this be put in a lemma? *)
assert { 0 <= at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 < pow2 96 };
(* the following asserts establish a bounds result about multiplying uint's -- can't this be put in a lemma? *)
assert { 0 <= at((uint 3 reg 2 + pow2 24*uint 3 reg 14))'L11 <= pow2 48-1 };
assert { 0 <= at((uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 <= pow2 48-1 };
assert { 0 <= at((uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 <= (pow2 48-1)*(pow2 48-1) };
assert { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
assert { 0 <= at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 < pow2 96 };
(* these checks can be useful in debugging when porting to a new version, but are not needed at the moment if we
add the above assert, which is much simpler to comprehend *)
(*
check { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 \/
at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 + pow2 96
};
assert { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20
check { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11
};
assert { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
check { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 + ?cf*pow2 96
};
*)
std rZ 3 r8;
std rZ 4 r9;
......
......@@ -71,7 +71,7 @@
</transf>
</goal>
</theory>
<theory name="KaratAvr" sum="142f7cc56838b108a6cf52e682fe22a4">
<theory name="KaratAvr" sum="94222744ffad59123652bc6ced119489">
<goal name="mul_bound_preserve" expl="">
<proof prover="5"><result status="valid" time="0.13"/></proof>
</goal>
......@@ -80,28 +80,28 @@
<goal name="WP_parameter karatsuba48_marked.1" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.1.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.46"/></proof>
<proof prover="6"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.2" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.2.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.41"/></proof>
<proof prover="6"><result status="valid" time="0.19"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.3" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.3.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.55"/></proof>
<proof prover="6"><result status="valid" time="0.25"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.4" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.4.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.53"/></proof>
<proof prover="6"><result status="valid" time="0.32"/></proof>
</goal>
</transf>
</goal>
......@@ -115,28 +115,28 @@
<goal name="WP_parameter karatsuba48_marked.6" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.6.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.45"/></proof>
<proof prover="6"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.7" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.7.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="2.08"/></proof>
<proof prover="6"><result status="valid" time="1.54"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.8" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.8.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="3.00"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="1.90"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.9" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.9.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.50"/></proof>
<proof prover="6"><result status="valid" time="0.31"/></proof>
</goal>
</transf>
</goal>
......@@ -192,21 +192,21 @@
<goal name="WP_parameter karatsuba48_marked.17" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.17.1" expl="precondition">
<proof prover="6"><result status="valid" time="0.70"/></proof>
<proof prover="6"><result status="valid" time="0.46"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.18" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.18.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="1.41"/></proof>
<proof prover="6"><result status="valid" time="1.14"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.19" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.19.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="3.69"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="3.22"/></proof>
</goal>
</transf>
</goal>
......@@ -220,7 +220,7 @@
<goal name="WP_parameter karatsuba48_marked.21" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.21.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="2.04"/></proof>
<proof prover="6"><result status="valid" time="1.45"/></proof>
</goal>
</transf>
</goal>
......@@ -241,14 +241,14 @@
<goal name="WP_parameter karatsuba48_marked.24" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.24.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="3.59"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="2.97"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.25" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.25.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="2.22"/></proof>
<proof prover="6"><result status="valid" time="1.66"/></proof>
</goal>
</transf>
</goal>
......@@ -262,14 +262,14 @@
<goal name="WP_parameter karatsuba48_marked.27" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.27.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="3.29"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="2.82"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.28" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.28.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="0.91"/></proof>
<proof prover="6"><result status="valid" time="0.73"/></proof>
</goal>
</transf>
</goal>
......@@ -280,17 +280,17 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.30" expl="assertion">
<goal name="WP_parameter karatsuba48_marked.30" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.30.1" expl="assertion">
<proof prover="2" steplimit="-1"><result status="valid" time="3.20"/></proof>
<goal name="WP_parameter karatsuba48_marked.30.1" expl="VC for karatsuba48_marked">
<proof prover="2" steplimit="-1"><result status="valid" time="2.49"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.31" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.31.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="0.99"/></proof>
<proof prover="6"><result status="valid" time="0.74"/></proof>
</goal>
</transf>
</goal>
......@@ -299,7 +299,7 @@
<goal name="WP_parameter karatsuba48_marked.32.1" expl="VC for karatsuba48_marked">
<transf name="eliminate_if_term">
<goal name="WP_parameter karatsuba48_marked.32.1.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="4.92"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="3.76"/></proof>
</goal>
</transf>
</goal>
......@@ -308,143 +308,133 @@
<goal name="WP_parameter karatsuba48_marked.33" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.33.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="3.10"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="2.51"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.34" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.34.1" expl="VC for karatsuba48_marked">
<proof prover="6"><result status="valid" time="1.00"/></proof>
<proof prover="6"><result status="valid" time="0.97"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.35" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.35.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13"><result status="valid" time="2.38"/></proof>
<proof prover="6" timelimit="13"><result status="valid" time="1.96"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.36" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter karatsuba48_marked.36.1" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.36.1" expl="assertion">
<proof prover="6" timelimit="13"><result status="valid" time="4.32"/></proof>
<goal name="WP_parameter karatsuba48_marked.36.1.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13" steplimit="0"><result status="valid" time="2.35"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.36.2" expl="VC for karatsuba48_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.36.2.1" expl="VC for karatsuba48_marked">
<proof prover="6" timelimit="13" steplimit="0"><result status="valid" time="2.23"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.37" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.37.1" expl="assertion">
<proof prover="6" timelimit="13"><result status="valid" time="3.48"/></proof>
<proof prover="6" timelimit="13" steplimit="0"><result status="valid" time="3.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.38" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.38.1" expl="assertion">
<proof prover="6" timelimit="13"><result status="valid" time="3.22"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter karatsuba48_marked.38.1" expl="VC for karatsuba48_marked">
<proof prover="0" steplimit="0"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="WP_parameter karatsuba48_marked.38.2" expl="VC for karatsuba48_marked">
<proof prover="5" steplimit="0"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.39" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter karatsuba48_marked.39.1" expl="VC for karatsuba48_marked">
<proof prover="0" steplimit="-1"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="WP_parameter karatsuba48_marked.39.2" expl="VC for karatsuba48_marked">
<proof prover="5" steplimit="-1"><result status="valid" time="0.28"/></proof>
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.39.1" expl="assertion">
<proof prover="6" timelimit="13"><result status="valid" time="4.32"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.40" expl="assertion">
<goal name="WP_parameter karatsuba48_marked.40" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.40.1" expl="assertion">
<proof prover="0" steplimit="0"><result status="valid" time="2.82"/></proof>
<goal name="WP_parameter karatsuba48_marked.40.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.29"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.41" expl="assertion">
<goal name="WP_parameter karatsuba48_marked.41" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.41.1" expl="assertion">
<proof prover="6"><result status="valid" time="1.54"/></proof>
<goal name="WP_parameter karatsuba48_marked.41.1" expl="precondition">
<proof prover="0" timelimit="1" steplimit="-1"><result status="valid" time="0.69"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.42" expl="assertion">
<goal name="WP_parameter karatsuba48_marked.42" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.42.1" expl="assertion">
<proof prover="0" steplimit="-1"><result status="valid" time="0.85"/></proof>
<goal name="WP_parameter karatsuba48_marked.42.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.20"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.43" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.43.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.40"/></proof>
<proof prover="6"><result status="valid" time="1.17"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.44" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.44.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.66"/></proof>
<proof prover="6"><result status="valid" time="1.28"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.45" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.45.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.58"/></proof>
<proof prover="6"><result status="valid" time="1.32"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.46" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.46.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.69"/></proof>
<proof prover="6"><result status="valid" time="1.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.47" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.47.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.44"/></proof>
<proof prover="6"><result status="valid" time="1.30"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.48" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.48.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.98"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.49" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.49.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.86"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.50" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.50.1" expl="precondition">
<proof prover="0" timelimit="1" steplimit="-1"><result status="valid" time="0.90"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.51" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.51.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.83"/></proof>
<proof prover="6"><result status="valid" time="1.40"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba48_marked.52" expl="postcondition">
<goal name="WP_parameter karatsuba48_marked.49" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba48_marked.52.1" expl="postcondition">
<proof prover="0" timelimit="1" steplimit="-1"><result status="valid" time="0.91"/></proof>
<goal name="WP_parameter karatsuba48_marked.49.1" expl="postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="7.31"/></proof>
</goal>
</transf>
</goal>
......
No preview for this file type
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment