Skip to content
GitLab
Commit 887f74f0 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

cleanup of karatsuba64

parent 6f42fc27
Hide whitespace changes
Inline Side-by-side
karatsuba64.mlw
View file @ 887f74f0
......@@ -384,7 +384,6 @@ ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = old (uint 4 reg 2*uint 4 reg 6)
S.modify_r20(); S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
end;
(* TODO analyse me *)
S.init();
abstract
ensures { S.synchronized S.shadow reg }
......@@ -402,17 +401,11 @@ ensures { uint 8 reg 10 + ?cf*pow2 64 = old(uint 8 reg 10 + uint 4 reg 14 + pow2
(* store carrrY in r26 *)
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
'CC:
(* TODO optimise me *)
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
(*
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11 }
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = ?cf*(1-old ?cf)*pow2 32 + old ?cf - ?cf }
*)
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
(* process sign bit *)
......@@ -442,11 +435,6 @@ assert { reg[27] = 0xFF*(1 - ?tf) };
S.modify_r2(); S.modify_r3();
S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
end;
(*
'DD:
check { "expl:temp"
at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + at ?cf 'CC *pow2 96 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) };
*)
S.init();
abstract ensures { S.synchronized S.shadow reg }
......@@ -469,27 +457,20 @@ ensures { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 9
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
S.modify_r28(); S.modify_r29(); S.modify_r18(); S.modify_r19();
end;
(* the checks will speed things up, but are not necessary *)
(*
assert { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf = at(?cf + uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(uint 1 reg 26 + (pow2 8+pow2 16+pow2 24)*reg[0]))'DD };
check {
at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
= (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) - pow2 32*at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11
};
check {
at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) - pow2 32*at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11
\/
at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*uint 4 reg 18*uint 4 reg 22)'L11) - pow2 32*at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11
+ pow2 128
};
check { 0 <= at(uint 4 reg 10)'L11 /\ 0 <= uint 8 reg 10 /\ 0 <= uint 2 reg 28 /\ 0 <= pow2 16*uint 2 reg 18 };
*)
assert { 0 <= at(uint 4 reg 10)'L11 /\ 0 <= uint 8 reg 10 /\ 0 <= uint 2 reg 28 /\ 0 <= pow2 16*uint 2 reg 18 };
assert { 0 <= at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
assert { 0 <= at((uint 4 reg 2 + pow2 32*uint 4 reg 18))'L11 <= pow2 64-1 };
assert { 0 <= at((uint 4 reg 6 + pow2 32*uint 4 reg 22))'L11 <= pow2 64-1 };
assert { 0 <= at((uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22))'L11 <= (pow2 64-1)*(pow2 64-1) };
assert {
(*
check {
at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
\/
......@@ -498,9 +479,10 @@ assert {
+ pow2 128
};
assert { at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
check { at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
= at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
};
*)
std rZ 4 r10;
std rZ 5 r11;
......
karatsuba64/why3session.xml
View file @ 887f74f0
......@@ -71,7 +71,7 @@
</transf>
</goal>
</theory>
<theory name="KaratAvr" sum="d01ad02a790d1d658e33f5849fdc9857">
<theory name="KaratAvr" sum="b3edb4560a891fcf74aa0ca40192c3e2">
<goal name="mul_bound_preserve" expl="">
<proof prover="5"><result status="valid" time="0.13"/></proof>
</goal>
......@@ -369,139 +369,129 @@
<goal name="WP_parameter karatsuba64_marked.41" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.41.1" expl="assertion">
<proof prover="6"><result status="valid" time="2.97"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter karatsuba64_marked.41.1.1" expl="VC for karatsuba64_marked">
<proof prover="6" steplimit="0"><result status="valid" time="9.69"/></proof>
</goal>
<goal name="WP_parameter karatsuba64_marked.41.1.2" expl="VC for karatsuba64_marked">
<proof prover="6" steplimit="0"><result status="valid" time="2.92"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.42" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.42.1" expl="assertion">
<proof prover="6"><result status="valid" time="2.73"/></proof>
<proof prover="6"><result status="valid" time="4.06"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.43" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.43.1" expl="assertion">
<proof prover="6"><result status="valid" time="3.17"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.44" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.44.1" expl="assertion">
<proof prover="6"><result status="valid" time="3.23"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.45" expl="assertion">
<goal name="WP_parameter karatsuba64_marked.44" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter karatsuba64_marked.45.1" expl="VC for karatsuba64_marked">
<goal name="WP_parameter karatsuba64_marked.44.1" expl="VC for karatsuba64_marked">
<proof prover="0"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter karatsuba64_marked.45.2" expl="VC for karatsuba64_marked">
<proof prover="5"><result status="valid" time="0.80"/></proof>
<goal name="WP_parameter karatsuba64_marked.44.2" expl="VC for karatsuba64_marked">
<proof prover="5"><result status="valid" time="1.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.46" expl="assertion">
<goal name="WP_parameter karatsuba64_marked.45" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.46.1" expl="assertion">
<proof prover="0"><result status="valid" time="3.93"/></proof>
<goal name="WP_parameter karatsuba64_marked.45.1" expl="precondition">
<proof prover="6" steplimit="0"><result status="valid" time="1.52"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.47" expl="assertion">
<proof prover="0"><result status="valid" time="0.41"/></proof>
<goal name="WP_parameter karatsuba64_marked.46" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.46.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.96"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.47" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.47.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.05"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.48" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.48.1" expl="precondition">
<proof prover="6"><result status="valid" time="1.90"/></proof>
<proof prover="0"><result status="valid" time="1.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.49" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.49.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.04"/></proof>
<proof prover="6"><result status="valid" time="2.37"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.50" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.50.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.05"/></proof>
<proof prover="0"><result status="valid" time="1.33"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.51" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.51.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.57"/></proof>
<proof prover="0"><result status="valid" time="1.38"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.52" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.52.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.25"/></proof>
<proof prover="0"><result status="valid" time="1.24"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.53" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.53.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.87"/></proof>
<proof prover="0"><result status="valid" time="1.42"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.54" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.54.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.87"/></proof>
<proof prover="0"><result status="valid" time="1.74"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.55" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.55.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.87"/></proof>
<proof prover="0"><result status="valid" time="1.37"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.56" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.56.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.94"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.57" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.57.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.58" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.58.1" expl="precondition">
<proof prover="0"><result status="valid" time="1.11"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.59" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.59.1" expl="precondition">
<proof prover="0"><result status="valid" time="0.84"/></proof>
<proof prover="0"><result status="valid" time="1.44"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba64_marked.60" expl="postcondition">
<goal name="WP_parameter karatsuba64_marked.57" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba64_marked.60.1" expl="postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="1.61"/></proof>
<goal name="WP_parameter karatsuba64_marked.57.1" expl="postcondition">
<proof prover="0" timelimit="60" steplimit="-1"><result status="valid" time="11.14"/></proof>
</goal>
</transf>
</goal>
......
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