Commit 1bcdae7f authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

updated README; removed vestigial dependency on Z3

parent db0572e2
......@@ -2,13 +2,17 @@
## Files
1. avrmodel.mlw - WhyML model for the AVR instruction set architecture
1. avrmodel.mlw - WhyML model for the AVR instruction set architecture
2. avrmodel/ - Why3 session files
2. avrmodel/ - Why3 session files
3. avr_code.mlw - AVR assembly translated to WhyML
3. schoolbook.mlw - AVR assembly of schoolbook multiplications translated to WhyML
4. avr_code/ - Why3 session files
4. schoolbook/ - Why3 session files
5. karatsubaXX.mlw - AVR assembly of XX-bit Karatsuba implementation translated to WhyML
6. karatsubaXX/ - Why3 session files
These can be viewed at:
......@@ -16,12 +20,11 @@ https://gitlab.science.ru.nl/sovereign/why3-avr/tree/master
## Checking the proofs
The proofs were developed using Why3 0.87.3; as well as the following theorem provers:
The proofs can be checked using Why3 0.88.3; as well as the following theorem provers:
* Alt-Ergo 1.01
* Alt-Ergo 2.0.0
* CVC3 2.4.1
* CVC4 1.4
* Eprover 1.8
* Z3 4.5.0
Then, simply running `why3 replay -L . avr_code` should work.
......@@ -549,6 +549,8 @@ let rec ghost uint_bound (reg: address_space) (lo w: int): unit
uint_recursion reg lo w;
assert { B.sum (reg,lo) 0 w = reg[lo] + 256*B.sum (reg,lo+1) 0 (w-1) };
uint_bound reg (lo+1) (w-1);
(* otherwise Z3 is needed *)
assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
end
end
......
......@@ -3,13 +3,12 @@
"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="Z3" version="4.5.0" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="1" memlimit="1000"/>
<file name="../avrmodel.mlw">
<theory name="AVRint" sum="c3e8923ffb42634aba535e05a1593bcf">
<theory name="AVRint" sum="83836e1ba6b23d458a4d1413c05eef71">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
......@@ -327,10 +326,13 @@
<goal name="WP_parameter uint_bound.4" expl="precondition">
<proof prover="4" steplimit="-1"><result status="valid" time="0.08" steps="75"/></proof>
</goal>
<goal name="WP_parameter uint_bound.5" expl="postcondition">
<proof prover="1"><result status="valid" time="4.13"/></proof>
<goal name="WP_parameter uint_bound.5" expl="assertion">
<proof prover="4" steplimit="0"><result status="valid" time="0.08" steps="82"/></proof>
</goal>
<goal name="WP_parameter uint_bound.6" expl="postcondition">
<proof prover="5" steplimit="0"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter uint_bound.7" expl="postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="0.21"/></proof>
</goal>
</transf>
......
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