Skip to content

GitLab

Commit 99d5d173 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

test version (subp with loop is in 'bigint_subp_j.mlw')

parent 7ea1e096
Expand all Hide whitespace changes
Inline Side-by-side
bigint_subp.mlw
View file @ 99d5d173
This diff is collapsed.
bigint_subp/why3session.xml 0 → 100644
View file @ 99d5d173
This diff is collapsed.
bigint_subp_j.mlw 0 → 100644
View file @ 99d5d173
(*
general TODO:
- memory stack invariance
labels to investigate
'AD
'Q1
*)
module BV_asr_Lemmas
use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision
lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma lsr_0: eq (lsr zeros 1) zeros
lemma lsr_1: eq (lsr (of_int 1) 1) zeros
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
lemma pow2_72: pow2 72 = 0x1000000000000000000
lemma pow2_80: pow2 80 = 0x100000000000000000000
lemma pow2_88: pow2 88 = 0x10000000000000000000000
lemma pow2_96: pow2 96 = 0x1000000000000000000000000
lemma pow2_104: pow2 104 = 0x100000000000000000000000000
lemma pow2_112: pow2 112 = 0x10000000000000000000000000000
lemma pow2_120: pow2 120 = 0x1000000000000000000000000000000
lemma pow2_128: pow2 128 = 0x100000000000000000000000000000000
lemma pow2_136: pow2 136 = 0x10000000000000000000000000000000000
lemma pow2_144: pow2 144 = 0x1000000000000000000000000000000000000
lemma pow2_152: pow2 152 = 0x100000000000000000000000000000000000000
lemma pow2_160: pow2 160 = 0x10000000000000000000000000000000000000000
lemma pow2_168: pow2 168 = 0x1000000000000000000000000000000000000000000
lemma pow2_176: pow2 176 = 0x100000000000000000000000000000000000000000000
lemma pow2_184: pow2 184 = 0x10000000000000000000000000000000000000000000000
lemma pow2_192: pow2 192 = 0x1000000000000000000000000000000000000000000000000
lemma pow2_200: pow2 200 = 0x100000000000000000000000000000000000000000000000000
lemma pow2_208: pow2 208 = 0x10000000000000000000000000000000000000000000000000000
lemma pow2_216: pow2 216 = 0x1000000000000000000000000000000000000000000000000000000
lemma pow2_224: pow2 224 = 0x100000000000000000000000000000000000000000000000000000000
lemma pow2_232: pow2 232 = 0x10000000000000000000000000000000000000000000000000000000000
lemma pow2_240: pow2 240 = 0x1000000000000000000000000000000000000000000000000000000000000
lemma pow2_248: pow2 248 = 0x100000000000000000000000000000000000000000000000000000000000000
lemma pow2_256: pow2 256 = 0x10000000000000000000000000000000000000000000000000000000000000000
end
module AvrModelLemmas
use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int
lemma register_file_invariant_strengthen:
forall m m': map int int. (forall i. 0 <= m[i] < 256) -> (forall i. 0 <= m'[i] < 256) -> (forall i j. 0 <= m[i]*m'[j] <= 255*255)
(*
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
*)
lemma pow_split: forall k. k >= 0 -> pow2 (2*k) = pow2 k*pow2 k
end
module AVRcode
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use bv.BV8
use import ref.Ref
use import int.Abs
use avrmodel.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
constant p25519: int = 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffed
let bigint_subp ()
requires { 32 <= uint 2 reg 22 < pow2 15 }
requires { 32 <= uint 2 reg 24 < pow2 15 }
requires { uint 2 reg 24 <= uint 2 reg 22 \/ uint 2 reg 24 >= uint 2 reg 22 + 32 }
ensures { uint 32 mem (old (uint 2 reg 24)) - pow2 256*reg[24] = old (uint 32 mem (uint 2 reg 22)) - p25519 }
=
movw r26 r22; (* load operand address a to x *)
movw r30 r24; (* load address of result to z *)
'S:
ldi r21 0xed;
ld_inc r20 rX;
sub r20 r21;
st_inc rZ r20;
ldi r21 0xff;
S.init();
for i = 1 to 30 do
invariant { S.synchronized S.shadow reg }
invariant { forall i. 0 <= reg[i] < 256 }
invariant { forall i. 0 <= mem[i] < 256 }
invariant { uint 2 reg rX = at(uint 2 reg rX+i)'S }
invariant { uint 2 reg rZ = at(uint 2 reg rZ+i)'S }
invariant { forall j. mem[j] <> (at mem 'S)[j] -> at(uint 2 reg rZ)'S <= j < at(uint 2 reg rZ)'S+i }
invariant { uint i mem (at (uint 2 reg rZ)'S) = ?cf*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) }
(* this is an on-the-fly proof by induction *)
invariant { forall mem mem', o. eq i mem mem' o -> uint i mem o = uint i mem' o }
let ghost i = i in
'B:
assert { pow2 8*pow2 (8*i) = pow2 (8*i+8) };
assert { mem[uint 2 reg rX] = (at mem 'S)[uint 2 reg rX] };
ld_inc r20 rX;
sbc r20 r21;
st_inc rZ r20;
(*
check { eq i mem (at mem 'B) (at(uint 2 reg rZ)'S) };
*)
(* apply the inductive proof *)
assert { uint i mem (at (uint 2 reg rZ)'S) = uint i (at mem 'B) (at(uint 2 reg rZ)'S) };
assert { mem[at(uint 2 reg rZ)'B] = ?cf*pow2 8 + at(mem[uint 2 reg rX])'B - 0xff - at (?cf) 'B };
assert { forall o, mem. uint (i+1) mem o = uint i mem o + pow2 (8*i)*mem[o+i] };
(*
check { uint (i+1) mem (at (uint 2 reg rZ)'S)
= uint i mem (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'S+i]
= uint i mem (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
= uint i (at mem 'B) (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
= at(?cf)'B*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19)
+ pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
= at(?cf)'B*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19)
+ pow2 (8*i)*at(mem[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i) - pow2 (8*i)*at(?cf)'B
= at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at(mem[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
= at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at((at mem 'S)[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
= at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at(mem[uint 2 reg rX+i])'S + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
= at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
= ?cf*pow2 (8*i)*pow2 8 + at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 8*pow2 (8*i)-19)
= ?cf*pow2 (8*(i+1)) + at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 (8*(i+1))-19) };
*)
S.modify_r20();
S.modify_r26(); S.modify_r27();
S.modify_r30(); S.modify_r31();
assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem o = uint i mem' o /\ mem[o+i] = mem'[o+i] };
(*
assert { forall mem mem', o. eq (i+1) mem mem' o -> eq i mem mem' o };
assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem' o = uint i mem o };
assert { forall mem mem', o. eq (i+1) mem mem' o -> mem[o+i] = mem'[o+i] };
assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem o + pow2 (8*i)*mem[o+i] = uint i mem' o + pow2 (8*i)*mem'[o+i] };
*)
done;
ldi r21 0x7f;
ld_inc r20 rX;
sbc r20 r21;
st_inc rZ r20;
(*
check { uint 32 mem (at (uint 2 reg rZ)'S) = ?cf*pow2 256 + at(uint 32 mem (uint 2 reg rX))'S - p25519 };
*)
clr r24;
adc r24 r24;
end
bigint_subp_j/why3session.xml 0 → 100644
View file @ 99d5d173
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="1" steplimit="0" memlimit="2000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="2" name="CVC4" version="1.4" alternative="noBV" timelimit="1" steplimit="0" memlimit="2000"/>
<file name="../bigint_subp_j.mlw" expanded="true">
<theory name="BV_asr_Lemmas" sum="e8cfd36209084e7ef4bcdd056be94bf7" expanded="true">
<goal name="asr_0" expl="" expanded="true">
</goal>
<goal name="asr_1" expl="" expanded="true">
</goal>
<goal name="asr_f" expl="" expanded="true">
</goal>
<goal name="lsr_0" expl="" expanded="true">
</goal>
<goal name="lsr_1" expl="" expanded="true">
</goal>
<goal name="xor_0" expl="" expanded="true">
</goal>
<goal name="xor_1" expl="" expanded="true">
</goal>
<goal name="or_0" expl="" expanded="true">
</goal>
<goal name="pow2_72" expl="" expanded="true">
</goal>
<goal name="pow2_80" expl="" expanded="true">
</goal>
<goal name="pow2_88" expl="" expanded="true">
</goal>
<goal name="pow2_96" expl="" expanded="true">
</goal>
<goal name="pow2_104" expl="" expanded="true">
</goal>
<goal name="pow2_112" expl="" expanded="true">
</goal>
<goal name="pow2_120" expl="" expanded="true">
</goal>
<goal name="pow2_128" expl="" expanded="true">
</goal>
<goal name="pow2_136" expl="" expanded="true">
</goal>
<goal name="pow2_144" expl="" expanded="true">
</goal>
<goal name="pow2_152" expl="" expanded="true">
</goal>
<goal name="pow2_160" expl="" expanded="true">
</goal>
<goal name="pow2_168" expl="" expanded="true">
</goal>
<goal name="pow2_176" expl="" expanded="true">
</goal>
<goal name="pow2_184" expl="" expanded="true">
</goal>
<goal name="pow2_192" expl="" expanded="true">
</goal>
<goal name="pow2_200" expl="" expanded="true">
</goal>
<goal name="pow2_208" expl="" expanded="true">
</goal>
<goal name="pow2_216" expl="" expanded="true">
</goal>
<goal name="pow2_224" expl="" expanded="true">
</goal>
<goal name="pow2_232" expl="" expanded="true">
</goal>
<goal name="pow2_240" expl="" expanded="true">
</goal>
<goal name="pow2_248" expl="" expanded="true">
</goal>
<goal name="pow2_256" expl="" expanded="true">
</goal>
</theory>
<theory name="AvrModelLemmas" sum="84c2740c682dbec30eb04b8ce55086ee" expanded="true">
<goal name="register_file_invariant_strengthen" expl="" expanded="true">
</goal>
<goal name="pow_split" expl="" expanded="true">
</goal>
</theory>
<theory name="AVRcode" sum="fbfd135c62a09fa6675c1ac71f71492d" expanded="true">
<goal name="mul_bound_preserve" expl="" expanded="true">
</goal>
<goal name="WP_parameter bigint_subp" expl="VC for bigint_subp">
<transf name="split_goal_wp">
<goal name="WP_parameter bigint_subp.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.2" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.2.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.3" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.3.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.4" expl="precondition">
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.5" expl="precondition">
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.6" expl="precondition">
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.7" expl="precondition">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.8" expl="postcondition">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.9" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.10" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.11" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.63"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.12" expl="loop invariant init">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.12.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.13" expl="loop invariant init">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.13.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.14" expl="loop invariant init">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.14.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.35"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.15" expl="loop invariant init">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.15.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.16" expl="loop invariant init">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.16.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.32"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.17" expl="assertion">
<proof prover="1" timelimit="1"><result status="valid" time="0.38" steps="132"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.18" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.18.1" expl="assertion">
<proof prover="2"><result status="valid" time="1.11"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.19" expl="type invariant">
<proof prover="2"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.20" expl="type invariant">
<proof prover="2"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.21" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.21.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.22" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.22.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.23" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.23.1" expl="assertion">
<proof prover="1"><result status="valid" time="1.97" steps="287"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.24" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.24.1" expl="assertion">
<proof prover="2"><result status="valid" time="1.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.25" expl="assertion">
<proof prover="1"><result status="valid" time="1.40" steps="313"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.26" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.26.1" expl="assertion">
<proof prover="2" timelimit="15"><result status="valid" time="10.42"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.27" expl="loop invariant preservation">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.27.1" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.28" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.29" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.30" expl="loop invariant preservation">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.30.1" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.43"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.31" expl="loop invariant preservation">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.31.1" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="1.09"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.32" expl="loop invariant preservation">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.32.1" expl="loop invariant preservation">
<proof prover="2" timelimit="15"><result status="valid" time="1.09"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.33" expl="loop invariant preservation">
<proof prover="0" timelimit="15"><result status="valid" time="2.07"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.34" expl="loop invariant preservation">
<proof prover="0" timelimit="15"><result status="valid" time="2.02"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.35" expl="type invariant">
<proof prover="2"><result status="valid" time="0.61"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.36" expl="precondition">
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.37" expl="type invariant">
<proof prover="2"><result status="valid" time="0.77"/></proof>
</goal>
<goal name="WP_parameter bigint_subp.38" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.38.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.43"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.39" expl="precondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.39.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.40"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter bigint_subp.40" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter bigint_subp.40.1" expl="postcondition">
<proof prover="0" timelimit="5"><result status="valid" time="5.72"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
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