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

ported the proofs to why3 version 0.88.3;

removed any dependency on alt-ergo < 2.0.0
parent 02ec34b5
......@@ -9,8 +9,8 @@ lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma xor_0: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 - w
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
lemma pow2_72: pow2 72 = 0x1000000000000000000
lemma pow2_80: pow2 80 = 0x100000000000000000000
......
This diff is collapsed.
No preview for this file type
......@@ -9,8 +9,8 @@ lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma xor_0: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 - w
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
......
This diff is collapsed.
No preview for this file type
......@@ -9,8 +9,8 @@ lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma xor_0: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 - w
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
......@@ -240,10 +240,6 @@ end;
ldd r26 rY 8;
ldd r27 rY 9;
'L11:
(*TODO *)
assert { at(uint 5 reg 7)'L00 + pow2 40*at(uint 5 reg 23)'L11 = at(uint 10 mem (uint 2 reg rY))'S };
assert { at(uint 5 reg 2*uint 5 reg 7)'L00 = at(uint 5 reg 2*uint 5 reg 7)'L11 };
assert { at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 = at(uint 10 mem (uint 2 reg rX))'S };
S.init();
abstract ensures { S.synchronized S.shadow reg }
......@@ -626,15 +622,23 @@ ensures { uint 5 reg 7 + pow2 40*uint 10 reg 17 + ?cf*pow2 120 = old(uint 5 reg
S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25(); S.modify_r26();
end;
assert { 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 <= pow2 80-1 };
assert { 0 <= at(uint 5 reg 7 + pow2 40*uint 5 reg 23)'L11 <= pow2 80-1 };
assert { 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 * at(uint 5 reg 7 + pow2 40*uint 5 reg 23)'L11 <= (pow2 80-1)*(pow2 80-1) };
assert { "expl:hack" 0 <= uint 10 reg 17 by 0 <= uint 5 reg 17 /\ 0 <= uint 5 reg 22 };
assert { at(uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 160
= at( (uint 5 reg 2 + pow2 40*uint 5 reg 12)*(uint 5 reg 7 + pow2 40*uint 5 reg 23) )'L11 + ?cf*pow2 160
};
assert { 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 * at(uint 5 reg 7 + pow2 40*uint 5 reg 23)'L11 <= (pow2 80-1)*(pow2 80-1)
by 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 <= pow2 80-1
/\ 0 <= at(uint 5 reg 7 + pow2 40*uint 5 reg 23)'L11 <= pow2 80-1
};
assert { "expl:obvious" 0 <= uint 10 reg 17 };
assert {
at (uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 160
= (pow2 40+1)*(at(uint 5 reg 2*uint 5 reg 7 + pow2 40*uint 5 reg 12*uint 5 reg 23)'L11)
- pow2 40 * at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23)) 'L11
+ ?cf*pow2 160
by
at(uint 5 reg 2*uint 5 reg 7)'L00 = at(uint 5 reg 2*uint 5 reg 7)'L11
/\
at(uint 5 reg 7)'L00 + pow2 40*at(uint 5 reg 23)'L11 = at(uint 10 mem (uint 2 reg rY))'S
};
std rZ 5 r7;
std rZ 6 r8;
......
This diff is collapsed.
No preview for this file type
......@@ -9,8 +9,8 @@ lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma xor_0: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 - w
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
......@@ -828,6 +828,7 @@ end;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
(* this next one fails *)
ensures { uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = ?cf*(pow2 96 - 1) - (at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) }
ensures { let cor = reg[31] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40)*reg[30] in cor = old ?cf - ?cf \/ cor = pow2 48 + old ?cf - ?cf }
'B:
......@@ -869,6 +870,7 @@ assert { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFE + ?tf };
assert { at reg[30] 'QQ = 0x00 -> reg[30] = ?tf };
asr r30;
assume { ?cf = 1 - at ?tf 'B };
S.modify_r6(); S.modify_r7();
S.modify_r26(); S.modify_r27(); S.modify_r28(); S.modify_r29();
S.modify_r12(); S.modify_r13();
......@@ -906,7 +908,7 @@ assert { 0 <= at( (at(uint 6 mem (uint 2 reg rY))'S + pow2 48*uint 6 reg 8) )'L1
assert { 0 <= at( (at(uint 6 mem (uint 2 reg rX))'S + pow2 48*uint 6 reg 14) )'L11 <= (pow2 96-1) };
assert { 0 <= at( (at(uint 6 mem (uint 2 reg rX))'S + pow2 48*uint 6 reg 14)*(at(uint 6 mem (uint 2 reg rY))'S + pow2 48*uint 6 reg 8) )'L11 <= (pow2 96-1)*(pow2 96-1) };
assert { "expl:hack" 0 <= uint 12 reg 14 by 0 <= uint 6 reg 14 /\ 0 <= uint 6 reg 20 };
assert { "expl:obvious" 0 <= uint 12 reg 14 by 0 <= uint 6 reg 14 /\ 0 <= uint 6 reg 20 };
assert { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6 reg 0 + ?cf*pow2 192
= at( (at(uint 6 mem (uint 2 reg rX))'S + pow2 48*uint 6 reg 14)*(at(uint 6 mem (uint 2 reg rY))'S + pow2 48*uint 6 reg 8) )'L11 + ?cf*pow2 192
......
This diff is collapsed.
No preview for this file type
......@@ -314,7 +314,7 @@ let add_ (dst src: register): unit
= 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');
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
......@@ -322,7 +322,7 @@ let inc_ (dst: register): unit
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.to_uint rd')
reg.data <- Map.set reg.data dst (BV8.t'int rd')
let dec_ (dst: register): unit
writes { reg }
......@@ -332,8 +332,8 @@ let dec_ (dst: register): unit
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
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
......@@ -343,16 +343,16 @@ let clr (dst: register): unit
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
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.to_uint (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { reg = old reg[dst<- BV8.t'int (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))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
(* t flag operations *)
val tf: cpu_flag
......@@ -385,38 +385,38 @@ function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
let bld (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.to_uint (bitset (BV8.of_int (old reg)[dst]) bit tf.value)] }
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.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
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.to_uint (bitset' (BV8.of_int (old reg)[dst]) bit tf.value)] }
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
assert { forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v) };
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
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.to_uint (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
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
assert { BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b };
assert { forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v) };
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
(*
let bld_incorrect (dst: register) (bit: int): unit
......@@ -424,10 +424,10 @@ let bld_incorrect (dst: register) (bit: int): unit
requires { 0 <= bit < 8 }
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
reg = (old reg)[dst <- BV8.to_uint (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask)] }
reg = (old reg)[dst <- BV8.t'int (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask)] }
= let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (Map.get reg.data dst) in
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask))
let bld_xor_incorrect (dst: register) (bit: int): unit
writes { reg }
......@@ -435,13 +435,13 @@ let bld_xor_incorrect (dst: register) (bit: int): unit
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
let upd = if BV8.nth prev bit = tf.value then prev else BV8.bw_xor prev mask in
reg = (old reg)[dst <- BV8.to_uint upd] }
reg = (old reg)[dst <- BV8.t'int upd] }
= 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.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
*)
end
......@@ -806,6 +806,7 @@ let ghost uint_shift (reg reg': address_space) (lo lo' w w' arg: int): unit
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 { forall b. b >= 0 -> pow2 8 * pow2 b = pow2 (8+b) };
assert { pow2 8*pow2 (8*n) = pow2 (8*(n+1)) }
done
......@@ -833,7 +834,7 @@ let add_ (dst src: register): unit
= 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');
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 add__ (dst src: register): unit
......@@ -843,7 +844,7 @@ let add__ (dst src: register): unit
= 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');
reg.data <- set reg.data dst (BV8.t'int 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
......@@ -852,8 +853,8 @@ let add__ (dst src: register): unit
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
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
......@@ -863,16 +864,16 @@ let clr (dst: register): unit
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
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.to_uint (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { reg = old reg[dst<- BV8.t'int (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))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
end
......@@ -1213,6 +1214,7 @@ let ghost uint_shift (reg reg': address_space) (lo lo' w w' arg: int): unit
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 { forall b. b >= 0 -> pow2 8 * pow2 b = pow2 (8+b) };
assert { pow2 8*pow2 (8*n) = pow2 (8*(n+1)) }
done
......@@ -1240,7 +1242,7 @@ let add_ (dst src: register): unit
= 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');
reg.data <- Map.set reg.data dst (BV8.t'int 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 <- 1
......@@ -1249,8 +1251,8 @@ let add_ (dst src: register): unit
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
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
......@@ -1260,16 +1262,16 @@ let clr (dst: register): unit
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
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.to_uint (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { reg = old reg[dst<- BV8.t'int (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = mod (old reg[dst]) 2 }
= cf.value <- if BV8.nth (BV8.of_int (Map.get reg.data dst)) 0 then 1 else 0;
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
end
......@@ -1327,7 +1329,7 @@ val cf: int_flag
type address_space = { mutable data: map int BV8.t }
function ([]) (r: address_space) (i: register): int = BV8.to_uint (M.get r.data i)
function ([]) (r: address_space) (i: register): int = BV8.t'int (M.get r.data i)
function ([<-]) (r: address_space) (i: register) (v: int): address_space
= { data = M.set r.data i (BV8.of_int v) }
......@@ -1426,7 +1428,7 @@ let mul (dst src: register): unit
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) }
= let prod = BV8.to_uint (M.get reg.data dst)*BV8.to_uint (M.get reg.data src) in
= let prod = BV8.t'int (M.get reg.data dst)*BV8.t'int (M.get reg.data src) in
reg.data <- M.set (M.set reg.data 0 (BV8.of_int (mod prod 256))) 1 (BV8.of_int (div prod 256));
cf.value <- (div prod (pow2 15) <> 0);
()
......@@ -1436,7 +1438,7 @@ let add (dst src: register): unit
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 = BV8.to_uint (M.get reg.data src) + BV8.to_uint (M.get reg.data dst) in
= let sum = BV8.t'int (M.get reg.data src) + BV8.t'int (M.get reg.data dst) in
reg.data <- M.set reg.data dst (BV8.of_int (mod sum 256));
cf.value <- (div sum 256 <> 0);
()
......@@ -1447,7 +1449,7 @@ let adc (dst src: register): unit
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 = BV8.to_uint (M.get reg.data src) + BV8.to_uint (M.get reg.data dst) + if cf.value then 1 else 0 in
= let sum = BV8.t'int (M.get reg.data src) + BV8.t'int (M.get reg.data dst) + if cf.value then 1 else 0 in
reg.data <- M.set reg.data dst (BV8.of_int ((mod sum 256)));
cf.value <- (div sum 256 <> 0);
()
......@@ -1457,7 +1459,7 @@ let sub (dst src: register): unit
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 = BV8.to_uint (M.get reg.data dst) - BV8.to_uint (M.get reg.data src) in
= let sum = BV8.t'int (M.get reg.data dst) - BV8.t'int (M.get reg.data src) in
reg.data <- M.set reg.data dst (BV8.of_int ((mod sum 256)));
assert { -255 <= sum <= 255 };
cf.value <- (-div sum 256 <> 0);
......@@ -1469,7 +1471,7 @@ let sbc (dst src: register): unit
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 = BV8.to_uint (M.get reg.data dst) - BV8.to_uint (M.get reg.data src) - if cf.value then 1 else 0 in
= let sum = BV8.t'int (M.get reg.data dst) - BV8.t'int (M.get reg.data src) - if cf.value then 1 else 0 in
reg.data <- M.set reg.data dst (BV8.of_int ((mod sum 256)));
cf.value <- (-div sum 256 <> 0);
()
......@@ -1490,7 +1492,7 @@ let ld_inc (dst src: register): unit
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 = BV8.to_uint (M.get reg.data src) + 256*BV8.to_uint (M.get reg.data (src+1)) in
= let cur = BV8.t'int (M.get reg.data src) + 256*BV8.t'int (M.get reg.data (src+1)) in
let nxt = mod (cur+1) (pow2 16) in
reg.data <- M.set (M.set (M.set reg.data dst (M.get mem.data cur)) src (BV8.of_int (mod nxt 256))) (src+1) (BV8.of_int (div nxt 256))
......@@ -1500,7 +1502,7 @@ let ldd (dst src ofs: register): unit
requires { 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 = BV8.to_uint (M.get reg.data src) + 256*BV8.to_uint (M.get reg.data (src+1)) in
= let cur = BV8.t'int (M.get reg.data src) + 256*BV8.t'int (M.get reg.data (src+1)) in
reg.data <- M.set reg.data dst (M.get mem.data (cur+ofs))
let std (dst ofs src: register): unit
......@@ -1509,7 +1511,7 @@ let std (dst ofs src: register): unit
requires { 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 = BV8.to_uint (M.get reg.data dst) + 256*BV8.to_uint (M.get reg.data (dst+1)) in
= let cur = BV8.t'int (M.get reg.data dst) + 256*BV8.t'int (M.get reg.data (dst+1)) in
mem.data <- M.set mem.data (cur+ofs) (M.get reg.data src)
let nop (): unit
......@@ -1522,14 +1524,14 @@ let sbci (dst: register) (k: int): unit
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 = BV8.to_uint (M.get reg.data dst) - k - if cf.value then 1 else 0 in
= let sum = BV8.t'int (M.get reg.data dst) - k - if cf.value then 1 else 0 in
reg.data <- M.set reg.data dst (BV8.of_int ((mod sum 256)));
cf.value <- (-div sum 256 <> 0);
()
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])) ] }
ensures { reg = old reg[dst <- BV8.t'int (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
= let tmp = BV8.bw_xor (M.get reg.data dst) (M.get reg.data src) in
reg.data <- M.set reg.data dst tmp
......@@ -1540,13 +1542,13 @@ let clr (dst: register): unit
let com (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<- BV8.to_uint (BV8.bw_not (BV8.of_int reg[dst]))] }
ensures { reg = old reg[dst<- BV8.t'int (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = BV8.bw_not (M.get reg.data dst) in
reg.data <- M.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 { reg = old reg[dst<- BV8.t'int (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = mod (old reg[dst]) 2 }
= cf.value <- BV8.nth (M.get reg.data dst) 0;
reg.data <- M.set reg.data dst (BV8.asr (M.get reg.data dst) 1)
......@@ -1865,7 +1867,7 @@ use bv.BV8
val eor (dst: register) (src: int): unit
writes { dst }
ensures { !dst = BV8.to_uint (BV8.bw_xor (BV8.of_int (old !dst)) (BV8.of_int src)) }
ensures { !dst = BV8.t'int (BV8.bw_xor (BV8.of_int (old !dst)) (BV8.of_int src)) }
let clr (dst: register): unit
writes { dst }
......
This diff is collapsed.
No preview for this file type
......@@ -418,7 +418,7 @@ let add_ (dst src: register): unit
= 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');
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
......@@ -426,7 +426,7 @@ let inc_ (dst: register): unit
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.to_uint rd')
reg.data <- Map.set reg.data dst (BV8.t'int rd')
let dec_ (dst: register): unit
writes { reg }
......@@ -436,8 +436,8 @@ let dec_ (dst: register): unit
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
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
......@@ -447,19 +447,19 @@ let clr (dst: register): unit
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
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.to_uint (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { reg = old reg[dst<- BV8.t'int (BV8.asr (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.to_uint (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
(* t flag operations *)
val tf: cpu_flag
......@@ -509,36 +509,36 @@ goal bitsetx_equiv_def:
let bld (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.to_uint (bitset (BV8.of_int (old reg)[dst]) bit tf.value)] }
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.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
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.to_uint (bitset' (BV8.of_int (old reg)[dst]) bit tf.value)] }
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.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
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.to_uint (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
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.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
*)
(*
......@@ -547,10 +547,10 @@ let bld_incorrect (dst: register) (bit: int): unit
requires { 0 <= bit < 8 }
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
reg = (old reg)[dst <- BV8.to_uint (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask)] }
reg = (old reg)[dst <- BV8.t'int (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask)] }
= let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (Map.get reg.data dst) in
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask))
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask))
let bld_xor_incorrect (dst: register) (bit: int): unit
writes { reg }
......@@ -558,13 +558,13 @@ let bld_xor_incorrect (dst: register) (bit: int): unit
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
let upd = if BV8.nth prev bit = tf.value then prev else BV8.bw_xor prev mask in
reg = (old reg)[dst <- BV8.to_uint upd] }
reg = (old reg)[dst <- BV8.t'int upd] }
= 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.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
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.to_uint (BV8.bw_or rd mask))
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
......
This diff is collapsed.
No preview for this file type
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