subp initial version

avrmodel.mlw

@@ -73,6 +73,12 @@ let mov (dst src: register): unit
   ensures { reg = old reg[dst<-reg[src]] }
 = reg.data <- Map.set reg.data dst (Map.get reg.data src)
 
+let ldi (dst: register) (imm: int): unit
+  writes { reg }
+  requires { 0 <= imm < 256 }
+  ensures { reg = old reg[dst<-imm] }
+= reg.data <- Map.set reg.data dst imm
+
 let mul (dst src: register): unit
   writes { cf }
   writes { reg }
@@ -216,6 +222,21 @@ let ldd (dst src ofs: register): unit
 = let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
   reg.data <- Map.set reg.data dst (Map.get mem.data (cur+ofs))
 
+let st_inc (dst src: register): unit
+  writes { reg }
+  writes { mem }
+  requires { 32 <= uint 2 reg src < pow2 16-1 }
+  ensures { let cur = uint 2 (old reg) src in
+            let inc = cur+1 in
+            reg = (old reg)[src <- mod inc 256][src+1 <- div inc 256] }
+  ensures { let cur = uint 2 (old reg) src in
+            mem = (old mem)[cur <- reg[src]] }
+  ensures { uint 2 reg src = old(uint 2 reg src)+1 }
+= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
+  let nxt = mod (cur+1) (pow2 16) in
+  reg.data <- Map.set (Map.set reg.data src (mod nxt 256)) (src+1) (div nxt 256);
+  mem.data <- Map.set mem.data cur (Map.get reg.data src)
+
 let std (dst ofs src: register): unit
   writes { mem }
   reads { reg }

avrmodel/why3session.xml

@@ -7,14 +7,17 @@
 <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="29d453cb11304d4b5824732def8ab77b">
+<file name="../avrmodel.mlw" expanded="true">
+<theory name="AVRint" sum="52dc8b8980ef39ce241a0a771d91e2d3" expanded="true">
  <goal name="WP_parameter prefix ?" expl="VC for prefix ?">
  <proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
  </goal>
  <goal name="WP_parameter mov" expl="VC for mov">
  <proof prover="4"><result status="valid" time="0.07" steps="83"/></proof>
  </goal>
+ <goal name="WP_parameter ldi" expl="VC for ldi">
+ <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.06" steps="79"/></proof>
+ </goal>
  <goal name="WP_parameter mul" expl="VC for mul">
  <proof prover="4"><result status="valid" time="1.34" steps="255"/></proof>
  </goal>
@@ -61,6 +64,25 @@
  <goal name="WP_parameter ldd" expl="VC for ldd">
  <proof prover="4"><result status="valid" time="0.28" steps="173"/></proof>
  </goal>
+ <goal name="WP_parameter st_inc" expl="VC for st_inc" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="WP_parameter st_inc.1" expl="type invariant">
+  <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.18" steps="130"/></proof>
+  </goal>
+  <goal name="WP_parameter st_inc.2" expl="type invariant">
+  <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.10" steps="109"/></proof>
+  </goal>
+  <goal name="WP_parameter st_inc.3" expl="postcondition">
+  <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.37" steps="135"/></proof>
+  </goal>
+  <goal name="WP_parameter st_inc.4" expl="postcondition" expanded="true">
+  <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.45" steps="130"/></proof>
+  </goal>
+  <goal name="WP_parameter st_inc.5" expl="postcondition" expanded="true">
+  <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="1.60" steps="211"/></proof>
+  </goal>
+ </transf>
+ </goal>
  <goal name="WP_parameter std" expl="VC for std">
  <proof prover="4"><result status="valid" time="0.30" steps="176"/></proof>
  </goal>
@@ -293,7 +315,6 @@
   <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.06" steps="72"/></proof>
   </goal>
   <goal name="WP_parameter rol.2" expl="postcondition">
-  <proof prover="2" steplimit="0" obsolete="true"><result status="valid" time="0.29"/></proof>
   <proof prover="4" steplimit="0" memlimit="2000"><result status="valid" time="0.06" steps="72"/></proof>
   </goal>
  </transf>

bigint_subp.mlw

+(*
+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 rX < pow2 15 }
+  requires { 32 <= uint 2 reg rZ < pow2 15 }
+  ensures { uint 32 mem (uint 2 reg rZ) = pow2 256*reg[24] + old (uint 32 mem (uint 2 reg rX)) - p25519 }
+=
+  movw r26 r22; (* load operand address a to x *)
+  movw r30 r24; (* load address of result to z *)
+
+  ldi r21 0xed;
+  ld_inc r20 rX;
+  sub r20 r21;
+  st_inc rZ  r20;
+
+  ldi r21 0xff;
+
+  (* perhaps unrolling saves on asserts? *)
+  for rept = 1 to 30 do
+    invariant { 32 <= uint 2 reg rX < pow2 15 + 32 }
+    invariant { 32 <= uint 2 reg rZ < pow2 15 + 32 }
+    
+    ld_inc r20 rX;
+    sbc r20 r21;
+    st_inc rZ  r20;
+  done;
+
+  ldi r21 0x7f;
+  ld_inc r20 rX;
+  sbc r20 r21;
+  st_inc rZ  r20;
+
+  clr r24;
+  adc r24 r24;
+
+end