Commit 044df936 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

merged avrmodel and avrmodel3

parent 9e2e0084
......@@ -135,6 +135,20 @@ let sbc (dst src: register): unit
cf.value <- (-div sum 256 <> 0);
()
let neg (dst: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (-reg[dst])) 256] }
(* TODO: which one is useful?
ensures { ?cf = if reg[dst] = 0 then 0 else 1 }
ensures { ?cf = -div (old (-reg[dst])) 256 }
*)
= let sum = - Map.get reg.data dst in
reg.data <- Map.set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
cf.value <- (-div sum 256 <> 0);
()
(* immediate versions *)
let subi (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
......@@ -445,13 +459,27 @@ let com (dst: register): unit
let asr (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.asr (BV8.of_int reg[dst]) 1)] }
(* TODO: is this useful?
ensures { ?cf = mod (old reg[dst]) 2 }
*)
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
let lsr (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsr (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = mod (old reg[dst]) 2 }
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.lsr (BV8.of_int (Map.get reg.data dst)) 1))
let lsl (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsl (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = 0 <-> old reg[dst] < 128 }
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 7 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 7;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.lsl (BV8.of_int (Map.get reg.data dst)) 1))
(* t flag operations *)
val tf: cpu_flag
......
......@@ -8,7 +8,7 @@
<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="83836e1ba6b23d458a4d1413c05eef71">
<theory name="AVRint" sum="b263d2793d6b4d719244c500d148f089">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
......@@ -16,20 +16,33 @@
<proof prover="4"><result status="valid" time="0.07" steps="83"/></proof>
</goal>
<goal name="WP_parameter mul" expl="VC for mul">
<proof prover="4"><result status="valid" time="1.66" steps="255"/></proof>
<proof prover="4"><result status="valid" time="1.34" steps="255"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="4"><result status="valid" time="1.76" steps="339"/></proof>
<proof prover="4"><result status="valid" time="1.36" steps="339"/></proof>
</goal>
<goal name="WP_parameter adc" expl="VC for adc">
<proof prover="4"><result status="valid" time="0.98" steps="167"/></proof>
<proof prover="4"><result status="valid" time="0.66" steps="167"/></proof>
</goal>
<goal name="WP_parameter sub" expl="VC for sub">
<proof prover="4"><result status="valid" time="0.85" steps="176"/></proof>
<proof prover="4"><result status="valid" time="0.59" steps="176"/></proof>
</goal>
<goal name="WP_parameter sbc" expl="VC for sbc">
<proof prover="4"><result status="valid" time="0.40" steps="158"/></proof>
</goal>
<goal name="WP_parameter neg" expl="VC for neg">
<transf name="split_goal_wp">
<goal name="WP_parameter neg.1" expl="assertion">
<proof prover="4" steplimit="0"><result status="valid" time="0.05" steps="74"/></proof>
</goal>
<goal name="WP_parameter neg.2" expl="type invariant">
<proof prover="4" steplimit="0"><result status="valid" time="0.09" steps="98"/></proof>
</goal>
<goal name="WP_parameter neg.3" expl="postcondition">
<proof prover="4" steplimit="0"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter subi" expl="VC for subi">
<proof prover="4" steplimit="-1"><result status="valid" time="0.59" steps="208"/></proof>
</goal>
......@@ -43,13 +56,13 @@
<proof prover="4"><result status="valid" time="0.12" steps="84"/></proof>
</goal>
<goal name="WP_parameter ld_inc" expl="VC for ld_inc">
<proof prover="0" steplimit="-1"><result status="valid" time="6.20"/></proof>
<proof prover="0" steplimit="-1"><result status="valid" time="5.46"/></proof>
</goal>
<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 std" expl="VC for std">
<proof prover="4"><result status="valid" time="0.46" steps="176"/></proof>
<proof prover="4"><result status="valid" time="0.30" steps="176"/></proof>
</goal>
<goal name="WP_parameter push" expl="VC for push">
<proof prover="4" steplimit="-1"><result status="valid" time="0.02" steps="89"/></proof>
......@@ -67,7 +80,7 @@
<proof prover="4"><result status="valid" time="0.04" steps="78"/></proof>
</goal>
<goal name="eq_uint" expl="">
<proof prover="0"><result status="valid" time="0.63"/></proof>
<proof prover="0"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="uint_0" expl="">
<proof prover="4"><result status="valid" time="0.04" steps="68"/></proof>
......@@ -100,7 +113,7 @@
<proof prover="4"><result status="valid" time="0.04" steps="88"/></proof>
</goal>
<goal name="uint_10" expl="">
<proof prover="4"><result status="valid" time="0.16" steps="92"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="92"/></proof>
</goal>
<goal name="uint_11" expl="">
<proof prover="4"><result status="valid" time="0.08" steps="96"/></proof>
......@@ -130,16 +143,16 @@
<proof prover="4"><result status="valid" time="0.29" steps="128"/></proof>
</goal>
<goal name="uint_20" expl="">
<proof prover="4"><result status="valid" time="0.55" steps="132"/></proof>
<proof prover="4"><result status="valid" time="0.38" steps="132"/></proof>
</goal>
<goal name="uint_21" expl="">
<proof prover="4"><result status="valid" time="0.55" steps="136"/></proof>
</goal>
<goal name="uint_22" expl="">
<proof prover="4"><result status="valid" time="0.80" steps="140"/></proof>
<proof prover="4"><result status="valid" time="0.39" steps="140"/></proof>
</goal>
<goal name="uint_23" expl="">
<proof prover="4"><result status="valid" time="0.68" steps="144"/></proof>
<proof prover="4"><result status="valid" time="0.47" steps="144"/></proof>
</goal>
<goal name="uint_24" expl="">
<proof prover="4"><result status="valid" time="0.49" steps="148"/></proof>
......@@ -154,19 +167,19 @@
<proof prover="4"><result status="valid" time="0.81" steps="160"/></proof>
</goal>
<goal name="uint_28" expl="">
<proof prover="4"><result status="valid" time="0.91" steps="164"/></proof>
<proof prover="4"><result status="valid" time="0.66" steps="164"/></proof>
</goal>
<goal name="uint_29" expl="">
<proof prover="4"><result status="valid" time="0.97" steps="168"/></proof>
<proof prover="4"><result status="valid" time="0.68" steps="168"/></proof>
</goal>
<goal name="uint_30" expl="">
<proof prover="4"><result status="valid" time="1.16" steps="172"/></proof>
</goal>
<goal name="uint_31" expl="">
<proof prover="4"><result status="valid" time="1.10" steps="176"/></proof>
<proof prover="4"><result status="valid" time="0.84" steps="176"/></proof>
</goal>
<goal name="uint_32" expl="">
<proof prover="4"><result status="valid" time="1.23" steps="180"/></proof>
<proof prover="4"><result status="valid" time="0.84" steps="180"/></proof>
</goal>
<goal name="WP_parameter movw" expl="VC for movw">
<proof prover="4"><result status="valid" time="0.13" steps="89"/></proof>
......@@ -231,8 +244,8 @@
<proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter add_.3" expl="postcondition">
<proof prover="2" timelimit="130"><result status="valid" time="41.35"/></proof>
<proof prover="3"><result status="valid" time="8.73"/></proof>
<proof prover="2" timelimit="130"><result status="valid" time="55.03"/></proof>
<proof prover="3"><result status="valid" time="7.47"/></proof>
</goal>
</transf>
</goal>
......@@ -251,7 +264,7 @@
</transf>
</goal>
<goal name="WP_parameter inc_" expl="VC for inc_">
<proof prover="2"><result status="valid" time="1.18"/></proof>
<proof prover="2"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="WP_parameter dec_" expl="VC for dec_">
<proof prover="4"><result status="valid" time="0.23" steps="124"/></proof>
......@@ -266,35 +279,41 @@
<proof prover="4"><result status="valid" time="0.09" steps="133"/></proof>
</goal>
<goal name="WP_parameter asr" expl="VC for asr">
<proof prover="2"><result status="valid" time="0.28"/></proof>
<proof prover="2"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="WP_parameter lsr" expl="VC for lsr">
<proof prover="2" steplimit="0"><result status="valid" time="1.57"/></proof>
</goal>
<goal name="WP_parameter lsl" expl="VC for lsl">
<proof prover="2" steplimit="0"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="WP_parameter bst" expl="VC for bst">
<proof prover="4"><result status="valid" time="0.08" steps="72"/></proof>
</goal>
<goal name="one_def" expl="">
<proof prover="2"><result status="valid" time="0.33"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="bitset_correct1" expl="">
<proof prover="0"><result status="valid" time="2.43"/></proof>
<proof prover="0"><result status="valid" time="1.56"/></proof>
</goal>
<goal name="bitset_correct2" expl="">
<proof prover="5"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="bitset_equiv_def" expl="">
<proof prover="0"><result status="valid" time="4.64"/></proof>
<proof prover="0"><result status="valid" time="1.42"/></proof>
</goal>
<goal name="bitsetx_equiv_def" expl="">
<proof prover="5"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter bld" expl="VC for bld">
<proof prover="4"><result status="valid" time="1.36" steps="786"/></proof>
<proof prover="4"><result status="valid" time="0.87" steps="786"/></proof>
</goal>
<goal name="WP_parameter uint_recursion" expl="VC for uint_recursion">
<transf name="split_goal_wp">
<goal name="WP_parameter uint_recursion.1" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter uint_recursion.1.1" expl="assertion">
<proof prover="0"><result status="valid" time="3.08"/></proof>
<proof prover="0"><result status="valid" time="1.76"/></proof>
</goal>
</transf>
</goal>
......@@ -305,10 +324,10 @@
<proof prover="4" steplimit="-1"><result status="valid" time="0.14" steps="73"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.4" expl="postcondition">
<proof prover="5"><result status="valid" time="3.55"/></proof>
<proof prover="5"><result status="valid" time="2.66"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.5" expl="postcondition">
<proof prover="0"><result status="valid" time="0.60"/></proof>
<proof prover="0"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
</goal>
......@@ -318,7 +337,7 @@
<proof prover="4" steplimit="-1"><result status="valid" time="0.10" steps="73"/></proof>
</goal>
<goal name="WP_parameter uint_bound.2" expl="assertion">
<proof prover="5"><result status="valid" time="3.11"/></proof>
<proof prover="5"><result status="valid" time="2.40"/></proof>
</goal>
<goal name="WP_parameter uint_bound.3" expl="variant decrease">
<proof prover="4" steplimit="-1"><result status="valid" time="0.06" steps="75"/></proof>
......
No preview for this file type
module AVRint
use import int.Int
use import int.EuclideanDivision
use import ref.Ref
use import map.Map
use import bv.Pow2int
(***** FORMAL MODEL OF AVR ******)
type register = int
constant r0: register = 0
constant r1: register = 1
constant r2: register = 2
constant r3: register = 3
constant r4: register = 4
constant r5: register = 5
constant r6: register = 6
constant r7: register = 7
constant r8: register = 8
constant r9: register = 9
constant r10: register = 10
constant r11: register = 11
constant r12: register = 12
constant r13: register = 13
constant r14: register = 14
constant r15: register = 15
constant r16: register = 16
constant r17: register = 17
constant r18: register = 18
constant r19: register = 19
constant r20: register = 20
constant r21: register = 21
constant r22: register = 22
constant r23: register = 23
constant r24: register = 24
constant r25: register = 25
constant r26: register = 26
constant r27: register = 27
constant r28: register = 28
constant r29: register = 29
constant r30: register = 30
constant r31: register = 31
type cpu_flag = { mutable value: bool }
function (?) (x: cpu_flag): int = if x.value then 1 else 0
let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0
val cf: cpu_flag
type address_space = { mutable data: map int int }
invariant { forall i. 0 <= self.data[i] < 256 }
function ([]) (r: address_space) (i: register): int = Map.get r.data i
function ([<-]) (r: address_space) (i: register) (v: int): address_space
= { data = Map.set r.data i v }
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]
clone sum.Sum as B with type container = (address_space, int), function f = get_uint_term
function uint (w: int) (reg: address_space) (lo: register): int
= B.sum (reg,lo) 0 w
val reg: address_space
let mov (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- Map.set reg.data dst (Map.get reg.data src)
let mul (dst src: register): unit
writes { cf }
writes { reg }
ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- mod p 256][1 <- div p 256] }
ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
(* ensures { reg[1] < 255 } *)
= let prod = Map.get reg.data dst*Map.get reg.data src in
reg.data <- Map.set (Map.set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf.value <- (div prod (pow2 15) <> 0);
()
let add (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst in
let r1 = (Map.get reg.data dst) in
let r2 = (Map.get reg.data src) in
reg.data <- Map.set reg.data dst (mod sum 256);
let res = (Map.get reg.data dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- True
else
cf.value <- False
let adc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src] + ?cf)) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src] + ?cf)) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst + ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (div sum 256 <> 0);
()
let sub (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src])) 256] }
ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let sum = Map.get reg.data dst - Map.get reg.data src in
reg.data <- Map.set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
cf.value <- (-div sum 256 <> 0);
()
let sbc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src] - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - reg[src] - ?cf)) 256 }
= let sum = Map.get reg.data dst - Map.get reg.data src - ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
let neg (dst: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (-reg[dst])) 256] }
(* TODO
ensures { ?cf = if reg[dst] = 0 then 0 else 1 }
ensures { ?cf = -div (old (-reg[dst])) 256 }
*)
= let sum = - Map.get reg.data dst in
reg.data <- Map.set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
cf.value <- (-div sum 256 <> 0);
()
(* immediate versions *)
let subi (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k)) 256] }
ensures { ?cf = -div (old (reg[dst] - k)) 256 }
= let sum = Map.get reg.data dst - k in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
let sbci (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = Map.get reg.data dst - k - ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
(* these instructions do not modify the carry flag *)
let inc (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + 1)) 256] }
= let sum = Map.get reg.data dst + 1 in
reg.data <- Map.set reg.data dst (mod sum 256)
let dec (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - 1)) 256] }
= let sum = Map.get reg.data dst - 1 in
reg.data <- Map.set reg.data dst (mod sum 256)
constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30
val mem: address_space
let ld_inc (dst src: register): unit
writes { reg }
reads { mem }
requires { 32 <= uint 2 reg src < pow2 16-1 }
(* TODO unnecessary
requires { dst <> src /\ dst <> src+1 }
*)
ensures { let cur = uint 2 (old reg) src in
let inc = cur+1 in
reg = (old reg)[dst <- mem[cur]][src <- mod inc 256][src+1 <- div inc 256] }
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 (Map.set reg.data dst (Map.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256)
let ldd (dst src ofs: register): unit
writes { reg }
reads { mem }
requires { 32 <= uint 2 reg src + ofs < pow2 16 }
ensures { let cur = uint 2 (old reg) src in
reg = (old reg)[dst <- mem[cur+ofs]] }
= 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 std (dst ofs src: register): unit
writes { mem }
reads { reg }
requires { 32 <= uint 2 reg dst + ofs < pow2 16 }
ensures { let cur = uint 2 (old reg) dst in
mem = (old mem)[cur+ofs <- reg[src]] }
= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
mem.data <- Map.set mem.data (cur+ofs) (Map.get reg.data src)
(* stack operations *)
constant stack_limit: int
val stack_pointer: ref int
val stack: address_space
let push (src: register): unit
writes { stack, stack_pointer }
reads { reg }
ensures { stack = old(stack[!stack_pointer <- reg[src]]) }
ensures { !stack_pointer = old !stack_pointer - 1 }
= stack.data <- Map.set stack.data (!stack_pointer) (Map.get reg.data src);
stack_pointer := !stack_pointer - 1
let pop (dst: register): unit
writes { reg, stack_pointer }
reads { stack }
ensures { reg = (old reg)[dst <- stack[!stack_pointer]] }
ensures { !stack_pointer = old !stack_pointer + 1 }
= stack_pointer := !stack_pointer + 1;
reg.data <- Map.set reg.data dst (Map.get stack.data !stack_pointer)
let nop (): unit
= ()
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': address_space) (lo: int)
= forall i. lo <= i < lo+w -> reg[i] = reg'[i]
goal eq_narrow:
forall reg reg', lo lo' w w'. lo <= lo' -> lo'+w' <= lo+w -> eq w reg reg' lo -> eq w' reg reg' lo'
goal eq_combine:
forall reg reg', lo lo' w w'. eq w reg reg' lo -> eq w' reg reg' lo' -> lo' = lo+w -> eq (w+w') reg reg' lo
goal eq_uint:
forall reg reg', lo w. eq w reg reg' lo -> uint w reg lo = uint w reg' lo
lemma uint_0:
forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
forall reg, lo. B.sum (reg,lo) 0 1 = reg[lo]
meta rewrite prop uint_1
lemma uint_2:
forall reg, lo. B.sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
meta rewrite prop uint_2
lemma uint_3:
forall reg, lo. B.sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
meta rewrite prop uint_3
lemma uint_4:
forall reg, lo. B.sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
meta rewrite prop uint_4
lemma uint_5:
forall reg, lo. B.sum (reg,lo) 0 5 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4]
meta rewrite prop uint_5
lemma uint_6:
forall reg, lo. B.sum (reg,lo) 0 6 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5]
meta rewrite prop uint_6
lemma uint_7:
forall reg, lo. B.sum (reg,lo) 0 7 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6]
meta rewrite prop uint_7
lemma uint_8:
forall reg, lo. B.sum (reg,lo) 0 8 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7]
meta rewrite prop uint_8
lemma uint_9:
forall reg, lo. B.sum (reg,lo) 0 9 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8]
meta rewrite prop uint_9
lemma uint_10:
forall reg, lo. B.sum (reg,lo) 0 10 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9]
meta rewrite prop uint_10
lemma uint_11:
forall reg, lo. B.sum (reg,lo) 0 11 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10]
meta rewrite prop uint_11
lemma uint_12:
forall reg, lo. B.sum (reg,lo) 0 12 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11]
meta rewrite prop uint_12
lemma uint_13:
forall reg, lo. B.sum (reg,lo) 0 13 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12]
meta rewrite prop uint_13
lemma uint_14:
forall reg, lo. B.sum (reg,lo) 0 14 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13]
meta rewrite prop uint_14
lemma uint_15:
forall reg, lo. B.sum (reg,lo) 0 15 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14]
meta rewrite prop uint_15
lemma uint_16:
forall reg, lo. B.sum (reg,lo) 0 16 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15]
meta rewrite prop uint_16
lemma uint_17:
forall reg, lo. B.sum (reg,lo) 0 17 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16]
meta rewrite prop uint_17
lemma uint_18:
forall reg, lo. B.sum (reg,lo) 0 18 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17]
meta rewrite prop uint_18
lemma uint_19:
forall reg, lo. B.sum (reg,lo) 0 19 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18]
meta rewrite prop uint_19
lemma uint_20:
forall reg, lo. B.sum (reg,lo) 0 20 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19]
meta rewrite prop uint_20
lemma uint_21:
forall reg, lo. B.sum (reg,lo) 0 21 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20]
meta rewrite prop uint_21
lemma uint_22:
forall reg, lo. B.sum (reg,lo) 0 22 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21]
meta rewrite prop uint_22
lemma uint_23:
forall reg, lo. B.sum (reg,lo) 0 23 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22]
meta rewrite prop uint_23
lemma uint_24:
forall reg, lo. B.sum (reg,lo) 0 24 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23]
meta rewrite prop uint_24
lemma uint_25:
forall reg, lo. B.sum (reg,lo) 0 25 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24]
meta rewrite prop uint_25
lemma uint_26:
forall reg, lo. B.sum (reg,lo) 0 26 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25]
meta rewrite prop uint_26
lemma uint_27:
forall reg, lo. B.sum (reg,lo) 0 27 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26]
meta rewrite prop uint_27
lemma uint_28:
forall reg, lo. B.sum (reg,lo) 0 28 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27]
meta rewrite prop uint_28
lemma uint_29:
forall reg, lo. B.sum (reg,lo) 0 29 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28]
meta rewrite prop uint_29
lemma uint_30:
forall reg, lo. B.sum (reg,lo) 0 30 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29]
meta rewrite prop uint_30
lemma uint_31:
forall reg, lo. B.sum (reg,lo) 0 31 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29] + pow2 240*reg[lo+30]
meta rewrite prop uint_31
lemma uint_32:
forall reg, lo. B.sum (reg,lo) 0 32 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29] + pow2 240*reg[lo+30] + pow2 248*reg[lo+31]
meta rewrite prop uint_32
meta compute_max_steps 0x1000000
(* word operations *)
let movw (dst src: register): unit
(* TODO unnecessary
requires { mod dst 2 = 0 /\ mod src 2 = 0 }
*)
writes { reg }
ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
= reg.data <- Map.set (Map.set reg.data dst (Map.get reg.data src)) (dst+1) (Map.get reg.data (src+1))