checked the result with alt-ergo 0.99.1, removing reliance on buggy 1.01-1.30 range,

to validate that the result of the original paper is still solid

README.md

@@ -18,7 +18,7 @@ https://gitlab.science.ru.nl/sovereign/why3-avr/tree/master
 
 The proofs were developed using Why3 0.87.3; as well as the following theorem provers:
 
-* Alt-Ergo 1.01
+* Alt-Ergo 0.99.1
 * CVC3 2.4.1
 * CVC4 1.4 
 * Eprover 1.8

avr_code3/why3session.xml

@@ -2,12 +2,12 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="13" steplimit="1" memlimit="1000"/>
 <prover id="1" name="CVC3" version="2.4.1" timelimit="13" steplimit="1" memlimit="1000"/>
-<prover id="3" name="Alt-Ergo" version="1.01" timelimit="13" steplimit="1" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
 <prover id="6" name="Eprover" version="1.8-001" timelimit="30" steplimit="1" memlimit="1000"/>
 <prover id="7" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
-<file name="../avr_code3.mlw">
+<file name="../avr_code3.mlw" expanded="true">
 <theory name="BV_asr_Lemmas" sum="2e06fe444b9c75ba2a223e558b72c17b">
  <goal name="asr_0">
  <proof prover="1"><result status="valid" time="0.28"/></proof>
@@ -99,10 +99,10 @@
 </theory>
 <theory name="AvrModelLemmas" sum="d5df575e801e47c8904feabb80c0c51c">
  <goal name="register_file_invariant_strengthen">
- <proof prover="3"><result status="valid" time="0.02" steps="68"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="69"/></proof>
  </goal>
  <goal name="pow_split">
- <proof prover="3"><result status="valid" time="0.02" steps="67"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="67"/></proof>
  </goal>
 </theory>
 <theory name="KaratAvr" sum="a98b83e98134aa08abcf8148ed2ae510">

avr_code4/why3session.xml

@@ -3,17 +3,17 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="CVC3" version="2.4.1" timelimit="13" steplimit="1" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="30" steplimit="1" memlimit="1000"/>
 <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"/>
-<prover id="6" name="Alt-Ergo" version="1.01" timelimit="30" steplimit="1" memlimit="1000"/>
-<file name="../avr_code4.mlw" expanded="true">
+<file name="../avr_code4.mlw">
 <theory name="BV_asr_Lemmas" sum="2e06fe444b9c75ba2a223e558b72c17b">
  <goal name="asr_0">
  <proof prover="4" steplimit="-1"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="asr_1">
- <proof prover="0" steplimit="-1"><result status="valid" time="2.17"/></proof>
+ <proof prover="0" steplimit="-1"><result status="valid" time="2.95"/></proof>
  </goal>
  <goal name="asr_f">
  <proof prover="4" steplimit="-1"><result status="valid" time="0.04"/></proof>
@@ -37,40 +37,40 @@
  <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.32"/></proof>
  </goal>
  <goal name="pow2_96">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.35"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.75"/></proof>
  </goal>
  <goal name="pow2_104">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.40"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.69"/></proof>
  </goal>
  <goal name="pow2_112">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.42"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.87"/></proof>
  </goal>
  <goal name="pow2_120">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.58"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.77"/></proof>
  </goal>
  <goal name="pow2_128">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.59"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.05"/></proof>
  </goal>
  <goal name="pow2_136">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.65"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.22"/></proof>
  </goal>
  <goal name="pow2_144">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.71"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.92"/></proof>
  </goal>
  <goal name="pow2_152">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.74"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.22"/></proof>
  </goal>
  <goal name="pow2_160">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.80"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.20"/></proof>
  </goal>
  <goal name="pow2_168">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.88"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.67"/></proof>
  </goal>
  <goal name="pow2_176">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="0.97"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.19"/></proof>
  </goal>
  <goal name="pow2_184">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.05"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.54"/></proof>
  </goal>
  <goal name="pow2_192">
  <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.14"/></proof>
@@ -79,33 +79,33 @@
  <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.18"/></proof>
  </goal>
  <goal name="pow2_208">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.27"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.74"/></proof>
  </goal>
  <goal name="pow2_216">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.45"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.91"/></proof>
  </goal>
  <goal name="pow2_224">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.44"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.86"/></proof>
  </goal>
  <goal name="pow2_232">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.44"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="2.23"/></proof>
  </goal>
  <goal name="pow2_240">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.56"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="2.07"/></proof>
  </goal>
  <goal name="pow2_248">
- <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="1.68"/></proof>
+ <proof prover="0" timelimit="30" steplimit="-1"><result status="valid" time="2.09"/></proof>
  </goal>
 </theory>
 <theory name="AvrModelLemmas" sum="f2b30af10f3e78ab15070cab44dacb50">
  <goal name="register_file_invariant_strengthen">
- <proof prover="6"><result status="valid" time="0.01" steps="68"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="69"/></proof>
  </goal>
  <goal name="pow_split">
- <proof prover="6"><result status="valid" time="0.02" steps="67"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="67"/></proof>
  </goal>
 </theory>
-<theory name="KaratAvr" sum="832c9e7058e400833dcad4f3b837de87" expanded="true">
+<theory name="KaratAvr" sum="832c9e7058e400833dcad4f3b837de87">
  <goal name="WP_parameter mul16" expl="VC for mul16">
  <transf name="compute_in_goal">
   <goal name="WP_parameter mul16.1" expl="1. VC for mul16">
@@ -116,8 +116,8 @@
  <goal name="mul_bound_preserve">
  <proof prover="5"><result status="valid" time="0.15"/></proof>
  </goal>
- <goal name="WP_parameter karatsuba96_marked" expl="VC for karatsuba96_marked" expanded="true">
- <transf name="split_goal_wp" expanded="true">
+ <goal name="WP_parameter karatsuba96_marked" expl="VC for karatsuba96_marked">
+ <transf name="split_goal_wp">
   <goal name="WP_parameter karatsuba96_marked.1" expl="1. precondition">
   <transf name="compute_in_goal">
    <goal name="WP_parameter karatsuba96_marked.1.1" expl="1. precondition">

avrmodel.mlw

@@ -1428,6 +1428,8 @@ let mul (dst src: register): unit
   ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
 = let prod = BV8.to_uint (M.get reg.data dst)*BV8.to_uint (M.get reg.data src) in
   reg.data <- M.set (M.set reg.data 0 (BV8.of_int (mod prod 256))) 1 (BV8.of_int (div prod 256));
+  assert { prod < 0x10000 };
+  assert { div prod (pow2 15) = 0 \/ div prod (pow2 15) = 1 };
   cf.value <- (div prod (pow2 15) <> 0);
   ()