Commit 64685d99 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Add a model that does not use any byte invariants, schoolbook works

parent 16c1132c
module AVRint
use int.Int
use int.EuclideanDivision
use ref.Ref
use map.Map
use bv.Pow2int
use export map.Map
(***** FORMAL MODEL OF AVR ******)
type register = int
let constant r0: register = 0
let constant r1: register = 1
let constant r2: register = 2
let constant r3: register = 3
let constant r4: register = 4
let constant r5: register = 5
let constant r6: register = 6
let constant r7: register = 7
let constant r8: register = 8
let constant r9: register = 9
let constant r10: register = 10
let constant r11: register = 11
let constant r12: register = 12
let constant r13: register = 13
let constant r14: register = 14
let constant r15: register = 15
let constant r16: register = 16
let constant r17: register = 17
let constant r18: register = 18
let constant r19: register = 19
let constant r20: register = 20
let constant r21: register = 21
let constant r22: register = 22
let constant r23: register = 23
let constant r24: register = 24
let constant r25: register = 25
let constant r26: register = 26
let constant r27: register = 27
let constant r28: register = 28
let constant r29: register = 29
let constant r30: register = 30
let constant r31: register = 31
type cpu_flag = ref int
val cf: cpu_flag
type address_space = { mutable data: map int int }
predicate valid_addr_space (addr_space: address_space) = forall i. 0 <= (data addr_space)[i] < 256
(*
the provers (mainly cvc3) hate this predicate for some reason:
predicate valid_reg_space (addr_space: address_space) = forall i. 0 <= i < 32 -> 0 <= (data addr_space)[i] < 256
*)
meta coercion function data
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * (reg.data[lo+i])
let rec ghost function uint_sum (rlo: (address_space, int)) (i: int) (j: int) : int =
variant { j - i }
if i >= j then 0 else get_uint_term rlo i + uint_sum rlo (i+1) j
(* TODO: we probably don't need to clone this anymore; the above definition is more elegant *)
type container = (address_space, int)
clone sum.Sum as B with type container = container, function f = get_uint_term, function sum = uint_sum
function uint (w: int) (reg: address_space) (lo: register): int
= uint_sum (reg,lo) 0 w
(* WIP COMMENT: i'm not sure if this is beneficial for the proof context *)
let ghost function lo8 (x: int): int
ensures { result = mod x 256 }
= mod x 256
let ghost function hi8 (x: int): int
ensures { result = div x 256 }
= div x 256
meta rewrite_def function lo8
meta rewrite_def function hi8
val reg: address_space
(* WIP COMMENT: in why3 1.x, the "ghost" vs "non-ghost" distinction seems to be converging towards
the notion of "not computable" and "computable"; however, we can still use non-computable stuff
in non-ghost code by conjuring it into existence using the 'any' expression. in Why3 1.x, this is
safe (a witness must be provided), whereas in Why3 0.8x it would not be safe.
note: this may no longer work in future versions of Why3
this comment can be removed at any time.*)
let data_set (m: map int int) (i: register) (v: int): map int int
ensures { result = Map.set m i v }
= any map int int ensures { result = Map.set m i v }
let read (m: address_space) (i: int): int
= any int ensures { m[i] = result }
let mov (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- data_set reg.data dst (read reg src)
let mul (dst src: register): unit
writes { cf }
writes { reg }
ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- lo8 p][1 <- hi8 p] }
ensures { let p = old (reg[src]*reg[dst]) in !cf = div p (pow2 15) }
(* ensures { reg[1] < 255 } *)
= let prod = read reg dst*read reg src in
reg.data <- data_set (data_set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf := div prod 0x8000;
()
let add (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + reg[src]))] }
ensures { !cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = read reg src + read reg dst in
reg.data <- data_set reg.data dst (mod sum 256);
cf := div sum 256
let adc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + reg[src] + !cf))] }
ensures { !cf = div (old (reg[dst] + reg[src] + !cf)) 256 }
= let sum = read reg src + read reg dst + !cf in
reg.data <- data_set reg.data dst (mod sum 256);
cf := div sum 256;
()
let sub (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - reg[src]))] }
ensures { !cf = -div (old (reg[dst] - reg[src])) 256 }
= let sum = read reg dst - read reg src in
reg.data <- data_set reg.data dst (mod sum 256);
cf := -div sum 256;
()
let sbc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - reg[src] - !cf))] }
ensures { !cf = -div (old (reg[dst] - reg[src] - !cf)) 256 }
= let sum = read reg dst - read reg src - !cf in
reg.data <- data_set reg.data dst (mod sum 256);
cf := -div sum 256;
()
let neg (dst: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (-reg[dst]))] }
(* TODO: which one is useful?
ensures { ?cf = if reg[dst] = 0 then 0 else 1 }
ensures { ?cf = -div (old (-reg[dst])) 256 }
*)
= let sum = - read reg dst in
reg.data <- data_set reg.data dst (mod sum 256);
cf := -div sum 256;
()
(* immediate versions *)
let subi (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - k))] }
ensures { !cf = -div (old (reg[dst] - k)) 256 }
= let sum = read reg dst - k in
reg.data <- data_set reg.data dst (mod sum 256);
cf := -div sum 256;
()
let sbci (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - k - !cf))] }
ensures { !cf = -div (old (reg[dst] - k - !cf)) 256 }
= let sum = read reg dst - k - !cf in
reg.data <- data_set reg.data dst (mod sum 256);
cf := -div sum 256;
()
(* these instructions do not modify the carry flag *)
let inc (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + 1))] }
= let sum = read reg dst + 1 in
reg.data <- data_set reg.data dst (mod sum 256)
let dec (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - 1))] }
= let sum = read reg dst - 1 in
reg.data <- data_set reg.data dst (mod sum 256)
let constant rX: register = 26
let constant rY: register = 28
let 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 }
requires { valid_addr_space mem }
(* 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 <- lo8 inc][src+1 <- hi8 inc] }
ensures { uint 2 reg src = old(uint 2 reg src)+1 }
= let cur = read reg src + 256*read reg (src+1) in
let nxt = mod (cur+1) 0x10000 in
reg.data <- data_set (data_set (data_set reg.data dst (read mem cur)) src (mod nxt 256)) (src+1) (div nxt 256)
let ldd (dst src ofs: register): unit
writes { reg }
reads { mem }
requires { valid_addr_space 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 = read reg src + 256*read reg (src+1) in
reg.data <- data_set reg.data dst (read mem (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 = read reg dst + 256*read reg (dst+1) in
mem.data <- data_set mem.data (cur+ofs) (read reg 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 <- data_set stack.data (!stack_pointer) (read reg 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 <- data_set reg.data dst (read stack !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. uint_sum (reg,lo) 0 0 = 0
lemma uint_1:
forall reg, lo. uint_sum (reg,lo) 0 1 = reg[lo]
meta rewrite lemma uint_1
lemma uint_2:
forall reg, lo. uint_sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
meta rewrite lemma uint_2
lemma uint_3:
forall reg, lo. uint_sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
meta rewrite lemma uint_3
lemma uint_4:
forall reg, lo. uint_sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
meta rewrite lemma uint_4
lemma uint_5:
forall reg, lo. uint_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 lemma uint_5
lemma uint_6:
forall reg, lo. uint_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 lemma uint_6
lemma uint_7:
forall reg, lo. uint_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 lemma uint_7
lemma uint_8:
forall reg, lo. uint_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 lemma uint_8
lemma uint_9:
forall reg, lo. uint_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 lemma uint_9
lemma uint_10:
forall reg, lo. uint_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 lemma uint_10
lemma uint_11:
forall reg, lo. uint_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 lemma uint_11
lemma uint_12:
forall reg, lo. uint_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 lemma uint_12
lemma uint_13:
forall reg, lo. uint_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 lemma uint_13
lemma uint_14:
forall reg, lo. uint_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 lemma uint_14
lemma uint_15:
forall reg, lo. uint_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 lemma uint_15
lemma uint_16:
forall reg, lo. uint_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 lemma uint_16
lemma uint_17:
forall reg, lo. uint_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 lemma uint_17
lemma uint_18:
forall reg, lo. uint_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 lemma uint_18
lemma uint_19:
forall reg, lo. uint_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 lemma uint_19
lemma uint_20:
forall reg, lo. uint_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 lemma uint_20
lemma uint_21:
forall reg, lo. uint_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 lemma uint_21
lemma uint_22:
forall reg, lo. uint_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 lemma uint_22
lemma uint_23:
forall reg, lo. uint_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 lemma uint_23
lemma uint_24:
forall reg, lo. uint_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 lemma uint_24
lemma uint_25:
forall reg, lo. uint_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 lemma uint_25
lemma uint_26:
forall reg, lo. uint_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 lemma uint_26
lemma uint_27:
forall reg, lo. uint_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 lemma uint_27
lemma uint_28:
forall reg, lo. uint_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 lemma uint_28
lemma uint_29:
forall reg, lo. uint_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 lemma uint_29
lemma uint_30:
forall reg, lo. uint_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 lemma uint_30
lemma uint_31:
forall reg, lo. uint_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 lemma uint_31
lemma uint_32:
forall reg, lo. uint_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 lemma 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 <- data_set (data_set reg.data dst (read reg src)) (dst+1) (read reg (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 <- lo8 (old (reg[dst] + k))]
[dst+1 <- lo8 (old (reg[dst+1] + div (reg[dst] + k) 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 = read reg dst + 256*read reg (dst+1) +k in
reg.data <- data_set reg.data dst (mod sum 256);
assert { mod sum 256 = mod (old (reg[dst] + k)) 256 };
reg.data <- data_set reg.data (dst+1) (mod (div sum 256) 256);
cf := div sum 65536
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 <- lo8 (old (reg[dst] - k))]
[dst+1 <- lo8 (old (reg[dst+1] + div (reg[dst] - k) 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 ********************)
let lsl (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst <- lo8 (old (2*reg[dst]))] }
ensures { !cf = div (old (2*reg[dst])) 256 }
= add dst dst
use bv.BV8
let bv8_to_int (x: BV8.t): int
ensures { result = BV8.t'int x }
= any int ensures { result = BV8.t'int x }
(*
let add_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- lo8 (reg[dst] + reg[src])]) }
ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let rd = BV8.of_int (read reg dst) in
let rr = BV8.of_int (read reg src) in
let rd' = BV8.add rd rr in
reg.data <- data_set reg.data dst (bv8_to_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 sub_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - reg[src]))] }
ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let rd = BV8.of_int (read reg dst) in
let rr = BV8.of_int (read reg src) in
let rd' = BV8.sub rd rr in
reg.data <- data_set reg.data dst (bv8_to_int rd');
cf.value <- (not BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rr 7 && BV8.nth rd' 7 || BV8.nth rd' 7 && not BV8.nth rd 7)
*)
(*
let inc_ (dst: register): unit
writes { reg }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + 1))] }
= let rd = BV8.of_int (read reg dst) in
let rd' = BV8.add rd (BV8.of_int 1) in
reg.data <- data_set reg.data dst (bv8_to_int rd')
let dec_ (dst: register): unit
writes { reg }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - 1))] }
= let sum = read reg dst - 1 in
reg.data <- data_set reg.data dst (mod sum 256)
*)
let eor (dst src: register): unit
writes { reg }
requires { valid_addr_space reg }
ensures { valid_addr_space 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_to_int (BV8.bw_xor (BV8.of_int (read reg dst)) (BV8.of_int (read reg src))) in
reg.data <- data_set reg.data dst tmp
let clr (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- 0] }
= reg.data <- data_set reg.data dst 0
let com (dst: register): unit
writes { reg }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { reg = old reg[dst<- BV8.t'int (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = bv8_to_int (BV8.bw_not (BV8.of_int (read reg dst))) in
reg.data <- data_set reg.data dst tmp
let asr (dst: register): unit
writes { reg, cf }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { reg = old reg[dst<- BV8.t'int (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { !cf = mod (old reg[dst]) 2 }
= cf := mod (read reg dst) 2;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.asr (BV8.of_int (read reg dst)) 1));
assert { forall b. BV8.nth b 0 <-> mod (BV8.t'int b) 2 = 1 }
let lsr (dst: register): unit
writes { reg, cf }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsr (BV8.of_int reg[dst]) 1)] }
ensures { !cf = mod (old reg[dst]) 2 }
= cf := mod (read reg dst) 2;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (read reg dst)) 1));
assert { forall b. BV8.nth b 0 <-> mod (BV8.t'int b) 2 = 1 }
(*
let lsl (dst: register): unit
writes { reg, cf }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
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 = BV8.nth (BV8.of_int (old reg[dst])) 7 }
= cf := BV8.nth (BV8.of_int (read reg dst)) 7;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsl (BV8.of_int (read reg dst)) 1))
*)
(* t flag operations *)
val tf: cpu_flag
val pow2 (x: int): int
requires { 0 <= x}
ensures { result = pow2 x }
let bst (dst: register) (bit: int): unit
writes { tf }
requires { 0 <= bit < 8 }
ensures { !tf = mod (div reg[dst] (pow2 bit)) 2 }
= tf := mod (div (read reg dst) (pow2 bit)) 2
(* WIP note: we don't need multiple definitions of 'bitset'; the best one is probably this one *)
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
(* WIP TODO: this can be moved to the 'by' part of bitset_correct2, if it doesn't impact any other proofs *)
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
(* WIP: this goal can be removed if the alternative definitions are not needed *)
goal bitset_equiv_def:
forall w, b, v. 0 <= b < 8 -> bitset w b v = bitsetx w b v = bitset' w b v
let bld (dst: register) (bit: int): unit
writes { reg }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.t'int (bitset (BV8.of_int (old reg)[dst]) bit (!tf <> 0))] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if (!tf <> 0) then
reg.data <- data_set reg.data dst (bv8_to_int (BV8.bw_or rd mask))
else
reg.data <- data_set reg.data dst (bv8_to_int (BV8.bw_and rd (BV8.bw_not 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)] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- data_set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- data_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)] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- data_set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- data_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 { uint_sum (reg,lo) 1 w = 256*uint_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 { valid_addr_space reg }
requires { w >= 0 }
ensures { 0 <= uint_sum (reg,lo) 0 w < pow2 (8*w) }
variant { w }
= if w > 0 then begin
uint_recursion reg lo w;
assert { uint_sum (reg,lo) 0 w = reg[lo] + 256*uint_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 int.Int
use ref.Ref
use import AVRint as AVR
use map.Map
type shadow_registers = {
ghost r0: ref int;