Skip to content
GitLab
Commit d94b7b24 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

cleaned up files

parent 16b1f0f4
Expand all Hide whitespace changes
Inline Side-by-side
prodscan.mlw → avr_code.mlw
View file @ d94b7b24
......@@ -460,7 +460,6 @@ ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 }
end;
abstract
ensures { uint 9 reg 17 = old(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8) }
(* ensures { uint 12 reg 14 = old(uint 12 reg 14 + pow2 24*uint 3 reg 5*uint 6 reg 8) } *)
ensures { eq 3 reg (old reg) 14 }
ensures { eq 6 reg (at reg 'S) 2 }
ensures { eq 6 reg (at reg 'S) 8 }
......@@ -488,7 +487,6 @@ ensures { eq 6 reg (at reg 'S) 8 }
adc r21 r27;
adc r22 r0;
adc r23 r1;
(* check { uint 9 reg 17 = at(uint 9 reg 17 + uint 1 reg 5*uint 6 reg 8)'B }; *)
mul r6 r10;
movw r26 r0;
mul r6 r8;
......@@ -512,7 +510,6 @@ ensures { eq 6 reg (at reg 'S) 8 }
adc r22 r27;
adc r23 r0;
adc r24 r1;
(* check { uint 9 reg 17 = at(uint 9 reg 17 + uint 2 reg 5*uint 6 reg 8)'B }; *)
mul r7 r10;
movw r26 r0;
mul r7 r8;
......@@ -536,7 +533,6 @@ ensures { eq 6 reg (at reg 'S) 8 }
adc r23 r27;
adc r24 r0;
adc r25 r1;
(* assert { uint 9 reg 17 = at(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8)'B }; *)
end
let mul48_flat (): unit
......
avr_code/why3session.xml 0 → 100644
View file @ d94b7b24
This diff is collapsed.
avrmodel.mlw
View file @ d94b7b24
......@@ -53,9 +53,6 @@ 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
......@@ -150,8 +147,6 @@ constant rZ: register = 30
val mem: address_space
(* TODO mem and reg overlap *)
(* TODO memory wrap around *)
let ld_inc (dst src: register): unit
writes { reg }
reads { mem }
......@@ -236,35 +231,6 @@ lemma 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]
(*
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
......@@ -279,79 +245,6 @@ 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
......@@ -370,21 +263,6 @@ let add_ (dst src: register): unit
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])) ] }
......
avrmodel/why3session.xml 0 → 100644
View file @ d94b7b24
This diff is collapsed.
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