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

enhanced model with memory/register exclusion

parent 6e65fb15
......@@ -155,6 +155,423 @@ 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 { 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] }
= 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)
let nop (): unit
= ()
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);
()
(****** 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]
lemma uint_2:
forall reg, lo. B.sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
lemma uint_3:
forall reg, lo. B.sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
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]
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]
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]
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 32*pow2 16*reg[lo+6]
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]
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]
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]
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]
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]
(*
lemma uint_0:
forall reg, lo. uint 0 reg lo = 0
lemma uint_1:
forall reg, lo. uint 1 reg lo = reg[lo]
lemma uint_2:
forall reg, lo. uint 2 reg lo = reg[lo] + pow2 8*reg[lo+1]
lemma uint_3:
forall reg, lo. uint 3 reg lo = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
lemma uint_4:
forall reg, lo. uint 4 reg lo = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
lemma uint_5:
forall reg, lo. uint 5 reg lo = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4]
lemma uint_6:
forall reg, lo. uint 6 reg lo = 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]
lemma uint_7:
forall reg, lo. uint 7 reg lo = 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 32*pow2 16*reg[lo+6]
lemma uint_8:
forall reg, lo. uint 8 reg lo = 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]
lemma uint_9:
forall reg, lo. uint 9 reg lo = 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]
lemma uint_10:
forall reg, lo. uint 10 reg lo = 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]
lemma uint_11:
forall reg, lo. uint 11 reg lo = 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]
lemma uint_12:
forall reg, lo. uint 12 reg lo = 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_1
meta rewrite prop uint_2
meta rewrite prop uint_3
meta rewrite prop uint_4
meta rewrite prop uint_5
meta rewrite prop uint_6
meta rewrite prop uint_7
meta rewrite prop uint_8
meta rewrite prop uint_9
meta rewrite prop uint_10
meta rewrite prop uint_11
meta rewrite prop uint_12
meta compute_max_steps 0x1000000
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 <= uint w reg lo < pow2 (w*8) }
variant { w }
= if w > 0 then begin
uint_recursion reg lo w;
assert { 256*uint (w-1) reg (lo+1) + reg[lo] = uint w reg lo };
uint_bound reg (lo+1) (w-1);
end
let ghost eq_uint_rev (reg reg': address_space) (lo w: int): unit
requires { uint w reg lo = uint w reg' lo }
ensures { eq w reg reg' lo }
= for w' = 0 to w-1 do
invariant { uint w' reg lo = uint w' reg' lo -> eq w' reg reg' lo }
uint_bound reg lo w';
uint_bound reg' lo w';
assert { mod(uint w' reg lo + pow2 (8*w')*reg[lo+w']) (pow2 (8*w')) = uint w' reg lo };
assert { mod(uint w' reg' lo + pow2 (8*w')*reg'[lo+w']) (pow2 (8*w')) = uint w' reg' lo };
done
let rec ghost uint_extend (reg: address_space) (lo w w': int): unit
variant { w' }
requires { w >= 0 }
requires { w' >= 0 }
requires { forall i. lo+w <= i < lo+w+w' -> reg[i] = 0 }
ensures { uint w reg lo = uint (w+w') reg lo }
= if w' > 0 then begin
assert { reg[lo+(w+w'-1)] = 0 };
uint_extend reg lo w (w'-1);
end
let ghost uint_shift (reg reg': address_space) (lo lo' w w' arg: int): unit
requires { w >= 0 }
requires { w' >= 0 }
requires { forall i. 0 < i <= w' -> reg[lo-i] = reg'[lo'-i] }
requires { uint w reg lo = uint w reg' lo' + arg }
ensures { uint (w+w') reg (lo-w') = uint (w+w') reg' (lo'-w') + pow2 (8*w')*arg }
= for n = 0 to w'-1 do
invariant { uint (w+n) reg (lo-n) = uint (w+n) reg' (lo'-n) + pow2 (8*n)*arg }
assert { reg[lo-n-1] = reg'[lo'-n-1] };
uint_recursion reg (lo-(n+1)) (w+(n+1));
uint_recursion reg' (lo'-(n+1)) (w+(n+1));
assert { uint (w+(n+1)) reg (lo-(n+1)) =
reg[lo-n-1] + 256*uint (w+n) reg (lo-n) =
reg'[lo'-n-1] + 256*(uint (w+n) reg' (lo'-n) + pow2 (8*n)*arg) =
uint (w+n+1) reg' (lo'-n-1) + 256*pow2 (8*n)*arg
};
assert { pow2 8*pow2 (8*n) = pow2 (8*(n+1)) }
done
let ghost uint_combine (reg: address_space) (b w w': int)
requires { w >= 0 /\ w' >= 0 }
ensures { uint (w+w') reg b = uint w reg b + pow2 (8*w)*uint w' reg (b+w) }
= for n = 0 to w'-1 do
invariant { uint (w+n) reg b = uint w reg b + pow2 (8*w)*uint n reg (b+w) }
assert { pow2 (8*(w+n)) = pow2 (8*w)*pow2 (8*n) };
check { uint (w+n+1) reg b = uint (w+n) reg b + pow2 (8*(w+n))*reg[b+w+n]
= uint w reg b + pow2 (8*w)*uint n reg (b+w) + pow2 (8*(w+n))*reg[b+w+n]
= uint w reg b + pow2 (8*w)*uint n reg (b+w) + pow2 (8*w+8*n)*reg[b+w+n]
= uint w reg b + pow2 (8*w)*uint n reg (b+w) + pow2 (8*w)*pow2 (8*n)*reg[b+w+n]
= uint w reg b + pow2 (8*w)*(uint n reg (b+w) + pow2 (8*n)*reg[b+w+n]) = uint w reg b + pow2 (8*w)*uint (n+1) reg (b+w) }
done
(*************** 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.to_uint rd');
if 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
then
cf.value <- True
else
cf.value <- False
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 (get reg.data dst) in
let rr = BV8.of_int (get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- set reg.data dst (BV8.to_uint rd');
if 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
then
cf.value <- True
else
cf.value <- False
let eor (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- BV8.to_uint (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
= let tmp = BV8.to_uint (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.to_uint (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = BV8.to_uint (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.to_uint (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = mod (old reg[dst]) 2 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
end
module AVRint_limit
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 }
(*
invariant { (forall i. 0 <= self.data[i] < 256) && (forall i j. 0 <= self.data[i]*self.data[j] <= 255*255) }
*)
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 movw (dst src: register): unit
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 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);
()
constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30
val mem: address_space
constant ram_begin: int
constant ram_end: int
(* TODO mem and reg overlap *)
(* TODO memory wrap around *)
let ld_inc (dst src: register): unit
writes { reg }
reads { mem }
requires { ram_begin <= uint 2 reg src < ram_end-1 }
requires { uint 2 reg src < pow2 16-1 }
requires { dst <> src /\ dst <> src+1 }
ensures { let cur = uint 2 (old reg) src in
......@@ -167,7 +584,7 @@ let ld_inc (dst src: register): unit
let ldd (dst src ofs: register): unit
writes { reg }
reads { mem }
requires { uint 2 reg src + ofs < pow2 16 }
requires { ram_begin <= uint 2 reg src + ofs < ram_end }
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
......@@ -176,7 +593,7 @@ let ldd (dst src ofs: register): unit
let std (dst ofs src: register): unit
writes { mem }
reads { reg }
requires { uint 2 reg dst + ofs < pow2 16 }
requires { ram_begin <= uint 2 reg dst + ofs < ram_end }
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
......
......@@ -49,7 +49,7 @@ function (:+) (x y: int): int = pow2 8*x + y
let mul16 (): unit
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
=
=
clr r23;
mul r3 r8;
movw r14 r0;
......@@ -67,7 +67,7 @@ let mul16 (): unit
let mul24_flat (): unit
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
=
=
clr r23;
mul r2 r9;
movw r14 r0;
......@@ -175,7 +175,7 @@ ensures { eq 3 reg (at reg 'S) 7 }
add r15 r0;
adc r16 r1;
adc r17 r25;
assert { uint 4 reg 14 = at(uint 3 reg 14)'B + at(reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
assert { uint 4 reg 14 = at(uint 3 reg 14)'B + at(reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
= at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'S };
end;
()
......@@ -254,7 +254,7 @@ ensures { eq 3 reg (at reg 'S) 7 }
adc r17 r25;
assert { uint 4 reg 14 + ?cf*pow2 32 = at(uint 3 reg 14 + reg[4]*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B
<= at(uint 3 reg 14 + 255*(reg[7] + pow2 8*reg[8] + pow2 16*reg[9]))'B };
assert { uint 4 reg 14 = at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'B
assert { uint 4 reg 14 = at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'B
= at(uint 3 reg 14)'B + at(reg[4]*uint 3 reg 7)'S };
end;
......@@ -388,14 +388,14 @@ check { uint 7 reg 12 + pow2 32*reg[25] = at(uint 4 reg 12 + pow2 8*reg[3]*reg[7
add r14 r0;
adc r15 r1;
adc r25 r23;
check { uint 7 reg 12 + pow2 32*reg[25] + ?cf*pow2 40 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B
<= at(uint 4 reg 12 + pow2 24*255*reg[10] + 255*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B
= at(uint 4 reg 12 + 255*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 24*reg[10] + pow2 32*reg[10]))'B
= at(uint 4 reg 12 + 255*pow2 8*(reg[7] + pow2 8*reg[8] + pow2 16*reg[10] + pow2 24*reg[10]))'B
< at(uint 4 reg 12 + 255*pow2 40)'B
check { uint 7 reg 12 + pow2 32*reg[25] + ?cf*pow2 40 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B
<= at(uint 4 reg 12 + pow2 24*255*reg[10] + 255*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B
= at(uint 4 reg 12 + 255*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 24*reg[10] + pow2 32*reg[10]))'B
= at(uint 4 reg 12 + 255*pow2 8*(reg[7] + pow2 8*reg[8] + pow2 16*reg[10] + pow2 24*reg[10]))'B
< at(uint 4 reg 12 + 255*pow2 40)'B
};
check { uint 4 reg 12 + pow2 32*reg[25] + ?cf*pow2 40 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8]))'B
<= at(uint 4 reg 12 + pow2 24*255*reg[10] + 255*(pow2 8*reg[7] + pow2 16*reg[8]))'B
check { uint 4 reg 12 + pow2 32*reg[25] + ?cf*pow2 40 = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8]))'B
<= at(uint 4 reg 12 + pow2 24*255*reg[10] + 255*(pow2 8*reg[7] + pow2 16*reg[8]))'B
};
check { uint 7 reg 12 + pow2 32*reg[25] = at(uint 4 reg 12 + pow2 24*reg[2]*reg[10] + reg[3]*(pow2 8*reg[7] + pow2 16*reg[8] + pow2 32*reg[10]))'B };
mul r4 r10;
......@@ -429,7 +429,7 @@ check { uint 2 reg 14 + ?cf*pow2 16 = at(uint 2 reg 14 + reg[4]*reg[7])'B };
adc r16 r1;
adc r25 r23;
(* ! *)
check { uint 3 reg 14 + reg[25]*pow2 24 + ?cf*pow2 32 = at(uint 3 reg 14 + reg[4]*reg[7] + reg[4]*pow2 16*reg[9] + pow2 8*reg[3]*reg[9])'B
check { uint 3 reg 14 + reg[25]*pow2 24 + ?cf*pow2 32 = at(uint 3 reg 14 + reg[4]*reg[7] + reg[4]*pow2 16*reg[9] + pow2 8*reg[3]*reg[9])'B
<= at(uint 3 reg 14 + 255*255 + 255*pow2 16*255 + pow2 8*255*255)'B };
check { ?cf = 0 };
check { uint 3 reg 14 + reg[25]*pow2 24 = at(uint 3 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9])'B };
......@@ -457,7 +457,7 @@ check { reg[15] + pow2 8*uint 2 reg 24 + ?cf*pow2 24 = at(reg[15])'X + at(pow2 8
adc r25 r23;
check { uint 6 reg 14 + pow2 16*uint 2 reg 24 + ?cf*pow2 32 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B };
(* ! *)
check { reg[15] + pow2 8*uint 2 reg 24 + ?cf*pow2 24 = at(reg[15])'X + at(pow2 8*reg[5]*reg[8] + reg[4]*reg[8] + reg[5]*reg[7])'B
check { reg[15] + pow2 8*uint 2 reg 24 + ?cf*pow2 24 = at(reg[15])'X + at(pow2 8*reg[5]*reg[8] + reg[4]*reg[8] + reg[5]*reg[7])'B
<= 255 + pow2 8*255*255 + 255*255 + 255*255
};
check { uint 6 reg 14 + pow2 16*uint 2 reg 24 = at(uint 5 reg 14 + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B };
......@@ -472,7 +472,7 @@ check { ? cf = 0 };
adc r18 r1;
adc r19 r23;
(* check { uint 4 reg 16 + ?cf*pow2 32 = at(uint 4 reg 16)'Y + pow2 8*reg[5]*reg[9] + at(uint 2 reg 24)'Y }; *)
assert { uint 6 reg 14 + ?cf*pow2 48
assert { uint 6 reg 14 + ?cf*pow2 48
= at(uint 5 reg 14 + pow2 24*reg[5]*reg[9] + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 32*reg[5]*reg[10] + pow2 16*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B
(*= at(uint 5 reg 14 + pow2 8*pow2 16*reg[5]*reg[9] + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 24*pow2 8*reg[5]*reg[10] + pow2 8*pow2 8*reg[5]*reg[8] + pow2 8*reg[4]*reg[8] + pow2 8*reg[5]*reg[7])'B
= at(uint 5 reg 14 + pow2 8*reg[5]*(pow2 16*reg[9] + pow2 24*reg[10] + pow2 8*reg[8] + reg[7]) + reg[4]*reg[7] + pow2 8*reg[3]*reg[9] + pow2 16*reg[4]*reg[9] + pow2 8*reg[4]*reg[8])'B
......@@ -490,7 +490,7 @@ end;
let mul32_flat(): unit
ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) }
=
=
clr r23;
mul r2 r9;
movw r14 r0;
......@@ -765,7 +765,7 @@ let mul40_flat(): unit
adc r21 r1;
()
let mul48 (): unit
let mul48 (): unit
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= 'S:
abstract
......@@ -923,7 +923,7 @@ ensures { eq 6 reg (at reg 'S) 8 }
()
end
let mul48_flat (): unit
let mul48_flat (): unit
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= 'S:
assert { pow2 88 = 0x10000000000000000000000 };
......@@ -1068,21 +1068,30 @@ assert { pow2 96 = 0x1000000000000000000000000 };
use import int.Abs
lemma prod_limit:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
let karatsuba48(): unit
requires { uint 2 reg rX < pow2 15 }
requires { uint 2 reg rY < pow2 15 }
requires { uint 2 reg rZ < pow2 15 }
(*
requires { uint 2 reg rZ <= uint 2 reg rX \/ uint 2 reg rZ >= uint 2 reg rX+6 }
requires { uint 2 reg rZ <= uint 2 reg rY \/ uint 2 reg rZ >= uint 2 reg rY+6 }
*)
requires { 32 <= uint 2 reg rX < pow2 15 }
requires { 32 <= uint 2 reg rY < pow2 15 }
requires { 32 <= uint 2 reg rZ < pow2 15 }
(*
requires { 32 <= ram_begin < ram_end <= 0x10000 }
requires { ram_begin <= uint 2 reg rX <= ram_end-7 }
requires { ram_begin <= uint 2 reg rY <= ram_end-6 }
requires { ram_begin <= uint 2 reg rZ <= ram_end-12 }
*)
ensures { uint 12 mem (old (uint 2 reg rZ)) = old (uint 6 mem (uint 2 reg rX) * uint 6 mem (uint 2 reg rY)) }
= 'S:
=
assert { forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l };
'S:
(* ; init zero registers *)
clr r22;
clr r23;
movw r12 r22;
movw r20 r22;
(* ;--- Compute L --- *)
ld_inc r2 rX;
ld_inc r3 rX;
......@@ -1118,7 +1127,7 @@ ensures { reg[22] = 0 /\ reg[23] = 0 /\ reg[20] = 0 /\ reg[21] = 0 }
add r10 r0;
adc r11 r1;
adc r12 r15;
mul r4 r7;
movw r14 r0;
mul r4 r5;
......@@ -1148,7 +1157,7 @@ end;
std rZ 1 r9;
std rZ 2 r10;
'L11:
abstract
ensures { uint 3 reg 2 = old (abs (uint 3 reg 2 - uint 3 reg 14)) }
ensures { uint 3 reg 5 = old (abs (uint 3 reg 5 - uint 3 reg 17)) }
......@@ -1219,7 +1228,7 @@ ensures { uint 2 reg rZ = at (uint 2 reg rZ) 'S }
add r13 r0;
adc r20 r1;
adc r21 r25;
mul r16 r19;
movw r24 r0;
mul r16 r17;
......@@ -1233,7 +1242,7 @@ ensures { uint 2 reg rZ = at (uint 2 reg rZ) 'S }
adc r21 r1;
adc r22 r25;
end;
assert { uint 3 reg 2 = at (abs (uint 3 reg 2 - uint 3 reg 14))'L11 };
assert { uint 3 reg 5 = at (abs (uint 3 reg 5 - uint 3 reg 17))'L11 };
......@@ -1266,7 +1275,7 @@ ensures { uint 2 reg rZ = at (uint 2 reg rZ) 'S }
add r16 r0;
adc r17 r1;
adc r18 r25;
mul r4 r7;
movw r24 r0;
mul r4 r5;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment