Commit 5279ed0a authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

typo: assume -> assert. luckily, it was easily proven.

parent 42741d7b
......@@ -850,7 +850,7 @@ assert { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFE + ?tf };
assert { at reg[30] 'QQ = 0x00 -> reg[30] = ?tf };
asr r30;
assume { ?cf = 1 - at ?tf 'B };
assert { ?cf = 1 - at ?tf 'B };
S.modify_r6(); S.modify_r7();
S.modify_r26(); S.modify_r27(); S.modify_r28(); S.modify_r29();
S.modify_r12(); S.modify_r13();
......
......@@ -7,7 +7,7 @@
<prover id="3" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="30" steplimit="1" memlimit="1000"/>
<file name="../karatsuba96.mlw" expanded="true">
<file name="../karatsuba96.mlw">
<theory name="BV_asr_Lemmas" sum="16edde4d72a282519bf221e18c8b7013">
<goal name="asr_0" expl="">
<proof prover="4" steplimit="-1"><result status="valid" time="0.05"/></proof>
......@@ -105,14 +105,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="68"/></proof>
</goal>
</theory>
<theory name="KaratAvr" sum="40e54402ac9db363c451a61a622e65b3" expanded="true">
<goal name="WP_parameter mul16" expl="VC for mul16">
<transf name="compute_in_goal">
<goal name="WP_parameter mul16.1" expl="VC for mul16">
<proof prover="4" obsolete="true"><result status="valid" time="0.39"/></proof>
</goal>
</transf>
</goal>
<theory name="KaratAvr" sum="151e7c12de0ac5b62c20abd89e35150a">
<goal name="mul_bound_preserve" expl="">
<proof prover="5"><result status="valid" time="0.15"/></proof>
</goal>
......@@ -734,194 +727,201 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.88" expl="VC for karatsuba96_marked">
<goal name="WP_parameter karatsuba96_marked.88" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.88.1" expl="VC for karatsuba96_marked">
<proof prover="0"><result status="valid" time="1.01"/></proof>
<goal name="WP_parameter karatsuba96_marked.88.1" expl="assertion">
<proof prover="4" timelimit="60" steplimit="0"><result status="valid" time="16.30"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.89" expl="VC for karatsuba96_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.89.1" expl="VC for karatsuba96_marked">
<proof prover="0"><result status="valid" time="2.34"/></proof>
<proof prover="0"><result status="valid" time="1.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.90" expl="VC for karatsuba96_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.90.1" expl="VC for karatsuba96_marked">
<proof prover="4"><result status="valid" time="18.27"/></proof>
<proof prover="0"><result status="valid" time="2.34"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.91" expl="assertion">
<goal name="WP_parameter karatsuba96_marked.91" expl="VC for karatsuba96_marked">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.91.1" expl="assertion">
<proof prover="4"><result status="valid" time="12.38"/></proof>
<goal name="WP_parameter karatsuba96_marked.91.1" expl="VC for karatsuba96_marked">
<proof prover="4"><result status="valid" time="18.27"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.92" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.92.1" expl="assertion">
<proof prover="4"><result status="valid" time="14.20"/></proof>
<proof prover="4"><result status="valid" time="12.38"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.93" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.93.1" expl="assertion">
<proof prover="4"><result status="valid" time="14.20"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.94" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter karatsuba96_marked.93.1" expl="VC for karatsuba96_marked">
<goal name="WP_parameter karatsuba96_marked.94.1" expl="VC for karatsuba96_marked">
<proof prover="0" timelimit="30"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="WP_parameter karatsuba96_marked.93.2" expl="VC for karatsuba96_marked">
<goal name="WP_parameter karatsuba96_marked.94.2" expl="VC for karatsuba96_marked">
<proof prover="5"><result status="valid" time="0.80"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.94" expl="obvious">
<goal name="WP_parameter karatsuba96_marked.95" expl="obvious">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.94.1" expl="obvious">
<goal name="WP_parameter karatsuba96_marked.95.1" expl="obvious">
<proof prover="4"><result status="valid" time="13.10"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.95" expl="assertion">
<goal name="WP_parameter karatsuba96_marked.96" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.95.1" expl="assertion">
<goal name="WP_parameter karatsuba96_marked.96.1" expl="assertion">
<proof prover="4"><result status="valid" time="20.24"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.96" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.96.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.97" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.97.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.08"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.98" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.98.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.38"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.08"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.99" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.99.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="2.73"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.38"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.100" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.100.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.49"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="2.73"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.101" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.101.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.14"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.49"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.102" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.102.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.18"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.14"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.103" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.103.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.24"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.18"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.104" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.104.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="2.99"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.24"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.105" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.105.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="2.90"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="2.99"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.106" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.106.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.12"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="2.90"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.107" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.107.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="2.87"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.12"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.108" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.108.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.02"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="2.87"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.109" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.109.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="2.88"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.110" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.110.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="2.97"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="2.88"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.111" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.111.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.50"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="2.97"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.112" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.112.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.28"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="3.50"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.113" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.113.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.28"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.114" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.114.1" expl="precondition">
<proof prover="0" timelimit="5"><result status="valid" time="3.82"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter karatsuba96_marked.114" expl="postcondition">
<goal name="WP_parameter karatsuba96_marked.115" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter karatsuba96_marked.114.1" expl="postcondition">
<goal name="WP_parameter karatsuba96_marked.115.1" expl="postcondition">
<proof prover="0" timelimit="30"><result status="valid" time="16.05"/></proof>
</goal>
</transf>
......
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