Commit a476a7d9 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

import previous work

parent 274df245
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))
let adiw (dst: register) (k: int): unit
requires { 0 <= k < 64 }
(* TODO unnecessary
requires { dst = 24 \/ dst = 26 \/ dst = 28 \/ dst = 30 }
*)
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- mod (old (reg[dst] + k)) 256]
[dst+1 <- mod (old (reg[dst+1] + div (reg[dst] + k) 256)) 256] }
ensures { ?cf = div (old (uint 2 reg dst + k)) 65536 }
ensures { ?cf*pow2 16 + uint 2 reg dst = old (uint 2 reg dst + k) }
= let sum = Map.get reg.data dst + 256*Map.get reg.data (dst+1) +k in
reg.data <- Map.set reg.data dst (mod sum 256);
reg.data <- Map.set reg.data (dst+1) (mod (div sum 256) 256);
cf.value <- (sum > 65535)
let sbiw (dst: register) (k: int): unit
requires { 0 <= k < 64 }
(* TODO unnecessary
requires { dst = 24 \/ dst = 26 \/ dst = 28 \/ dst = 30 }
*)
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k)) 256]
[dst+1 <- mod (old (reg[dst+1] + div (reg[dst] - k) 256)) 256] }
ensures { ?cf = -div (old (uint 2 reg dst - k)) 65536 }
ensures { uint 2 reg dst = ?cf*pow2 16 + old (uint 2 reg dst - k) }
= subi dst k;
sbci (dst+1) 0
(*************** BITVECTOR IMPORTS ********************)
use bv.BV8
let add_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let rd = BV8.of_int (Map.get reg.data dst) in
let rr = BV8.of_int (Map.get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- Map.set reg.data dst (BV8.t'int rd');
cf.value <- (BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7)
let inc_ (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + 1)) 256] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let rd' = BV8.add rd (BV8.of_int 1) in
reg.data <- Map.set reg.data dst (BV8.t'int rd')
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)
let eor (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- BV8.t'int (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
= let tmp = BV8.t'int (BV8.bw_xor (BV8.of_int (Map.get reg.data dst)) (BV8.of_int (Map.get reg.data src))) in
reg.data <- Map.set reg.data dst tmp
let clr (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<-0] }
= eor dst dst
let com (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<- BV8.t'int (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = BV8.t'int (BV8.bw_not (BV8.of_int (Map.get reg.data dst))) in
reg.data <- Map.set reg.data dst tmp
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))
(* t flag operations *)
val tf: cpu_flag
let bst (dst: register) (bit: int): unit
writes { tf }
requires { 0 <= bit < 8 }
ensures { tf.value = BV8.nth (BV8.of_int reg[dst]) bit }
= tf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) bit
function bitset (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if v then
BV8.bw_or w mask
else
BV8.bw_and w (BV8.bw_not mask)
function bitset' (w: BV8.t) (b: int) (v: bool): BV8.t =
let v' = BV8.of_int (if v then 1 else 0) in
let one = BV8.of_int 1 in
BV8.bw_or (BV8.bw_and w (BV8.bw_not (BV8.lsl one b))) (BV8.lsl v' b)
function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if BV8.nth w b = v then
w
else
BV8.bw_xor w mask
lemma one_def:
BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b
goal bitset_correct1:
forall w, b, v. 0 <= b < 8 ->
BV8.nth (bitset w b v) b = v
goal bitset_correct2:
forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
BV8.nth (bitset w b v) i = BV8.nth w i
goal bitset_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v)
goal bitsetx_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v)
let bld (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.t'int (bitset (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
(*
let bld' (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.t'int (bitset' (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
let bld'' (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.t'int (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
*)
let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { B.sum (reg,lo) 1 w = 256*B.sum (reg,lo+1) 0 (w-1) }
variant { w }
= assert { forall k. 0 <= k < w-1 -> get_uint_term (reg,lo) (k+1) = 256*get_uint_term (reg,lo+1) k };
if w > 0 then begin
uint_recursion reg lo (w-1)
end
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { 0 <= B.sum (reg,lo) 0 w < pow2 (8*w) }
variant { w }
= if w > 0 then begin
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
module Shadow
use import int.Int
use import ref.Ref
use import AVRint as AVR
use map.Map
type shadow_registers = {
ghost r0: ref int;
ghost r1: ref int;
ghost r2: ref int;
ghost r3: ref int;
ghost r4: ref int;
ghost r5: ref int;
ghost r6: ref int;
ghost r7: ref int;
ghost r8: ref int;
ghost r9: ref int;
ghost r10: ref int;
ghost r11: ref int;
ghost r12: ref int;
ghost r13: ref int;
ghost r14: ref int;
ghost r15: ref int;
ghost r16: ref int;
ghost r17: ref int;
ghost r18: ref int;
ghost r19: ref int;
ghost r20: ref int;
ghost r21: ref int;
ghost r22: ref int;
ghost r23: ref int;
ghost r24: ref int;
ghost r25: ref int;
ghost r26: ref int;
ghost r27: ref int;
ghost r28: ref int;
ghost r29: ref int;
ghost r30: ref int;
ghost r31: ref int
}
predicate synchronized (self: shadow_registers) (avr: address_space) =
avr[0] = !(self.r0) /\
avr[1] = !(self.r1) /\
avr[2] = !(self.r2) /\
avr[3] = !(self.r3) /\
avr[4] = !(self.r4) /\
avr[5] = !(self.r5) /\
avr[6] = !(self.r6) /\
avr[7] = !(self.r7) /\
avr[8] = !(self.r8) /\
avr[9] = !(self.r9) /\
avr[10] = !(self.r10) /\
avr[11] = !(self.r11) /\
avr[12] = !(self.r12) /\
avr[13] = !(self.r13) /\
avr[14] = !(self.r14) /\
avr[15] = !(self.r15) /\
avr[16] = !(self.r16) /\
avr[17] = !(self.r17) /\
avr[18] = !(self.r18) /\
avr[19] = !(self.r19) /\
avr[20] = !(self.r20) /\
avr[21] = !(self.r21) /\
avr[22] = !(self.r22) /\
avr[23] = !(self.r23) /\
avr[24] = !(self.r24) /\
avr[25] = !(self.r25) /\
avr[26] = !(self.r26) /\
avr[27] = !(self.r27) /\
avr[28] = !(self.r28) /\
avr[29] = !(self.r29) /\
avr[30] = !(self.r30) /\
avr[31] = !(self.r31)
val shadow: shadow_registers
let ghost modify_r0 () ensures { !(shadow.r0) = reg[0] } = shadow.r0 := Map.get reg.data 0
let ghost modify_r1 () ensures { !(shadow.r1) = reg[1] } = shadow.r1 := Map.get reg.data 1; ()
let ghost modify_r2 () ensures { !(shadow.r2) = reg[2] } = shadow.r2 := Map.get reg.data 2
let ghost modify_r3 () ensures { !(shadow.r3) = reg[3] } = shadow.r3 := Map.get reg.data 3
let ghost modify_r4 () ensures { !(shadow.r4) = reg[4] } = shadow.r4 := Map.get reg.data 4
let ghost modify_r5 () ensures { !(shadow.r5) = reg[5] } = shadow.r5 := Map.get reg.data 5
let ghost modify_r6 () ensures { !(shadow.r6) = reg[6] } = shadow.r6 := Map.get reg.data 6
let ghost modify_r7 () ensures { !(shadow.r7) = reg[7] } = shadow.r7 := Map.get reg.data 7
let ghost modify_r8 () ensures { !(shadow.r8) = reg[8] } = shadow.r8 := Map.get reg.data 8
let ghost modify_r9 () ensures { !(shadow.r9) = reg[9] } = shadow.r9 := Map.get reg.data 9
let ghost modify_r10 () ensures { !(shadow.r10) = reg[10] } = shadow.r10 := Map.get reg.data 10
let ghost modify_r11 () ensures { !(shadow.r11) = reg[11] } = shadow.r11 := Map.get reg.data 11
let ghost modify_r12 () ensures { !(shadow.r12) = reg[12] } = shadow.r12 := Map.get reg.data 12