Commit 9d308b2c authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

optimised (removed checks)

parent 3ab5cbd5
......@@ -14,6 +14,8 @@ lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 -
lemma pow2_72: pow2 72 = 0x1000000000000000000
lemma pow2_80: pow2 80 = 0x100000000000000000000
lemma pow2_88: pow2 88 = 0x10000000000000000000000
lemma pow2_96: pow2 96 = 0x1000000000000000000000000
end
......@@ -33,7 +35,7 @@ end
module KaratAvr
use import avrmodel.AVRint
use import avrmodel2.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
......@@ -538,8 +540,6 @@ end
let mul48_flat (): unit
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= 'S:
assert { pow2 88 = 0x10000000000000000000000 };
assert { pow2 96 = 0x1000000000000000000000000 };
clr r20;
clr r21;
movw r22 r20;
......@@ -997,8 +997,6 @@ let karatsuba48_flat(): unit
*)
ensures { uint 12 mem (old (uint 2 reg rZ)) = old (uint 6 mem (uint 2 reg rX) * uint 6 mem (uint 2 reg rY)) }
=
assert { pow2 88 = 0x10000000000000000000000 };
assert { pow2 96 = 0x1000000000000000000000000 };
assert { forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l };
'S:
(* ; init zero registers *)
......@@ -1236,7 +1234,10 @@ assert { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 +
std rZ 10 r21;
std rZ 11 r22
use avrmodel.Shadow as S
use avrmodel2.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
let karatsuba48_marked(): unit
(*
......@@ -1254,7 +1255,6 @@ let karatsuba48_marked(): unit
*)
ensures { uint 12 mem (old (uint 2 reg rZ)) = old (uint 6 mem (uint 2 reg rX) * uint 6 mem (uint 2 reg rY)) }
=
assert { forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l };
'S:
(* ; init zero registers *)
clr r22;
......@@ -1381,7 +1381,6 @@ ensures { reg[27] = if old (uint 3 reg 5 < uint 3 reg 17) then 0xFF else 0x00 }
S.modify_r27();
end;
'Tmp:
(* ;--- Compute H + (l3l4l5) --- *)
(*
S.init();
......@@ -1501,7 +1500,6 @@ assert { reg[26] = 0xFF <-> at((uint 3 reg 2 < uint 3 reg 14) <-> (uint 3 reg 5
adc r12 r21;
adc r13 r22;
assert { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 48 = at (uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 3 reg 11 + pow2 24*uint 3 reg 20)'Pre };
assert { at(uint 6 reg 8)'Tmp = at(uint 3 reg 2*uint 3 reg 5)'L00 };
S.modify_r26();
S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13();
end;
......@@ -1511,7 +1509,7 @@ S.init();
*)
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 14 + ?cf = ?cf*pow2 48 - at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) - at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
ensures { let cor = reg[23] + (pow2 8+pow2 16)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 24 + old ?cf - ?cf }
(* ; merge carry and borrow *)
adc r23 r26;
......
This diff is collapsed.
No preview for this file type
......@@ -41,7 +41,7 @@ end
module KaratAvr
use import avrmodel.AVRint
use import avrmodel2.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
......@@ -49,9 +49,6 @@ use import AvrModelLemmas
use BV_asr_Lemmas
use bv.BV8
function (+:) (x y: int): int = x + pow2 8*y
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) }
=
......@@ -71,7 +68,7 @@ let mul16 (): unit
use import int.Abs
use avrmodel.Shadow as S
use avrmodel2.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
......@@ -562,11 +559,8 @@ ensures { ?tf = 0 <-> at((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint
sbc r8 r1;
sbc r9 r1;
(* check { reg[0] = if at (uint 4 reg 2 < uint 4 reg 18)'B then 0xFF else 0x00 }; *)
(* check { reg[1] = if at (uint 4 reg 6 < uint 4 reg 22)'B then 0xFF else 0x00 }; *)
eor r0 r1;
bst r0 0 ;
(* check { reg[0] = if at (uint 4 reg 2 < uint 4 reg 18 <-> uint 4 reg 6 < uint 4 reg 22)'B then 0x00 else 0xFF }; *)
S.modify_r0(); S.modify_r1();
S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5();
S.modify_r6(); S.modify_r7(); S.modify_r8(); S.modify_r9();
......@@ -751,17 +745,6 @@ ensures { old(uint 4 reg 10) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + p
adc r17 r19;
assert { uint 8 reg 10 + ?cf*pow2 64
= at(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18) 'B };
check { uint 8 reg 10 + ?cf*pow2 64
= at(uint 8 reg 10)'B + at (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22)'L11 };
check { at(uint 4 reg 10)'B + pow2 32*uint 8 reg 10 + ?cf*pow2 96
= pow2 32*at(uint 8 reg 10)'B + at (uint 8 reg 10 + pow2 32*uint 4 reg 18*uint 4 reg 22)'L11 };
check { at(uint 4 reg 10)'B + pow2 32*uint 8 reg 10 + ?cf*pow2 96
= pow2 32*at(uint 8 reg 10)'B + at (uint 4 reg 2*uint 4 reg 6 + pow2 32*uint 4 reg 18*uint 4 reg 22)'L11 };
check { at(uint 4 reg 10)'B + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + pow2 32*uint 8 reg 10 + ?cf*pow2 96
= pow2 32*at(uint 4 reg 10)'B + pow2 64*at(uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22)'L11 + at (uint 4 reg 2*uint 4 reg 6 + pow2 32*uint 4 reg 18*uint 4 reg 22)'L11 };
check { at(uint 4 reg 10)'B + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + pow2 32*uint 8 reg 10 + ?cf*pow2 96
= pow2 32*at(uint 4 reg 2*uint 4 reg 6 + pow2 32*uint 4 reg 18*uint 4 reg 22)'L11 + at (uint 4 reg 2*uint 4 reg 6 + pow2 32*uint 4 reg 18*uint 4 reg 22)'L11 };
(* store carrrY in r26 *)
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
......@@ -773,22 +756,16 @@ ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11 }
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
(* process sign bit *)
check { reg[27] = 0 };
'B:
bld r27 0;
dec 27;
assert { reg[27] = 0xFF*(1 - ?tf) };
check { reg[27] = 0xFF <-> at((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22))'L11 };
check { reg[27] = 0xFF \/ reg[27] = 0x00 };
check { reg[26] = 0 };
(* merge carry and borrow *)
adc r26 r27;
mov r0 r26;
asr r0;
check { uint 6 reg 20 + pow2 48*uint 2 reg 2 = at (uint 4 reg 2*uint 4 reg 6)'Tmp };
check { uint 6 reg 20 + pow2 48*uint 2 reg 2 = at (abs (uint 4 reg 2 - uint 4 reg 18)*abs (uint 4 reg 6 - uint 4 reg 22))'L11 };
'B:
(* invert all bits or do nothing *)
eor r20 r27;
......@@ -805,10 +782,6 @@ check { uint 6 reg 20 + pow2 48*uint 2 reg 2 = at (abs (uint 4 reg 2 - uint 4 re
'B:
add r27 r27; (* sets carry flag if r27 = 0xff *)
assert { ?cf = 1 - ?tf };
check { at reg[27] 'B = ?cf*0xFF };
check { at reg[27] 'B = 0x00 -> uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11 };
check { at reg[27] 'B = 0xFF -> uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11 };
check { "expl:alternative ensures" uint 6 reg 20 + pow2 48*uint 2 reg 2 = (1 - ?tf)*(pow2 64 - 1) - at((uint 4 reg 2 - uint 4 reg 18)*(uint 4 reg 6 - uint 4 reg 22))'L11 };
S.modify_r0(); S.modify_r26(); S.modify_r27();
S.modify_r2(); S.modify_r3();
S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
......
This diff is collapsed.
No preview for this file type
......@@ -589,19 +589,8 @@ ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = i
assert { reg[29] = 0xFF -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
add r29 r29; (* sets carry flag if r29 = 0xff *)
assert { ?cf = 1 - ?tf };
check { ?cf = 1 <-> at((uint 5 reg 2 < uint 5 reg 12) <-> (uint 5 reg 7 < uint 5 reg 23))'L11 };
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2)'B };
(*
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(uint 5 reg 2*uint 5 reg 7)'Tmp };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(uint 5 reg 2*uint 5 reg 7)'Tmp };
*)
assert { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = at(abs (uint 5 reg 2 - uint 5 reg 12)*abs(uint 5 reg 7 - uint 5 reg 23))'L11 };
assert { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at(abs (uint 5 reg 2 - uint 5 reg 12)*abs(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 0 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ?cf*(pow2 80 - 1) - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
check { ?cf = 1 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ?cf*(pow2 80 - 1) - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 };
S.modify_r0();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16();
......@@ -637,65 +626,12 @@ 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;
(*
check { 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
\/
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 + pow2 160
};
*)
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 };
(*
check { 0 <= at (uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 < pow2 160 };
check { 0 <= (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) < pow2 160 };
check {
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
};
check { forall x y. x < pow2 160 -> 0 <= y -> x = y + pow2 160 -> x = y };
check { forall x y. 0 <= x -> y < pow2 160 -> x + pow2 160 = y -> x = y };
check { forall x y. x + pow2 160 = y + pow2 160 -> x = y };
check { ?cf = 0 ->
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
};
check { forall x y.
0 <= y ->
y + pow2 160 = x
-> x >= pow2 160
};
check { forall b. 0 <= uint 10 reg b };
check {
at(uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + pow2 160
= at( (uint 5 reg 2 + pow2 40*uint 5 reg 12)*(uint 5 reg 7 + pow2 40*uint 5 reg 23) )'L11
->at( (uint 5 reg 2 + pow2 40*uint 5 reg 12)*(uint 5 reg 7 + pow2 40*uint 5 reg 23) )'L11 >= pow2 160
};
check { ?cf = 1 ->
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 + pow2 160
};
check { 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 { 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
};
......
This diff is collapsed.
No preview for this file type
......@@ -145,7 +145,6 @@ ensures { forall i. not (uint 2 reg rZ <= i < uint 2 reg rZ+6) -> mem[i] = (old
adc r20 r1;
assert { uint 7 reg 14 = at(uint 1 reg 2 * uint 6 reg 8)'B };
check { uint 7 reg 14 = at(uint 1 mem (uint 2 reg rX))'S * at(uint 6 reg 8)'B };
ld_inc r3 rX;
'Q:
......@@ -174,7 +173,6 @@ check { uint 7 reg 14 = at(uint 1 mem (uint 2 reg rX))'S * at(uint 6 reg 8)'B }
adc r21 r1;
assert { uint 8 reg 14 = at(uint 7 reg 14)'Q + at(pow2 8*uint 1 reg 3)'Q * at(uint 6 reg 8)'B };
check { uint 8 reg 14 = at(uint 2 mem (uint 2 reg rX))'S * at(uint 6 reg 8)'B };
ld_inc r4 rX;
'Q:
......@@ -202,7 +200,6 @@ check { uint 8 reg 14 = at(uint 2 mem (uint 2 reg rX))'S * at(uint 6 reg 8)'B }
adc r21 r0;
adc r22 r1;
assert { uint 9 reg 14 = at(uint 8 reg 14)'Q + at(pow2 16*uint 1 reg 4)'Q * at(uint 6 reg 8)'B };
check { uint 9 reg 14 = at(uint 3 mem (uint 2 reg rX))'S * at(uint 6 reg 8)'B };
std rZ 0 r14;
std rZ 1 r15;
std rZ 2 r16;
......@@ -303,8 +300,8 @@ end;
(* TODO which one is better; also try 'uint 6' *)
assert { eq 12 mem (at mem 'S) (at (uint 2 reg rX) 'S) };
assert { eq 12 mem (at mem 'S) (at (uint 2 reg rY) 'S) };
check { uint 12 mem (at (uint 2 reg rX) 'S) = at (uint 12 mem (uint 2 reg rX))'S };
check { uint 12 mem (at (uint 2 reg rY) 'S) = at (uint 12 mem (uint 2 reg rY))'S };
(* check { uint 12 mem (at (uint 2 reg rX) 'S) = at (uint 12 mem (uint 2 reg rX))'S };
check { uint 12 mem (at (uint 2 reg rY) 'S) = at (uint 12 mem (uint 2 reg rY))'S }; *)
(* load a6..a11 and b6..b11 *)
ld_inc r14 rX;
......@@ -514,28 +511,25 @@ ensures { uint 6 reg 8 = old (abs (uint 6 reg 8 - at(uint 6 mem (uint 2 reg rY))
ensures { ?tf = 0 <-> old(uint 6 reg 14) < at(uint 6 mem (uint 2 reg rX))'S <-> old(uint 6 reg 8) < at(uint 6 mem (uint 2 reg rY))'S }
(* subtract a0 a5 *)
sbiw r26 12;
check { uint 2 reg rX = at(uint 2 reg rX)'S };
check { eq 6 mem (at mem 'S) (uint 2 reg rX) };
check { eq 6 mem (at mem 'S) (uint 2 reg rY) };
'B:
(* if you transform these checks into asserts, verification will speed up because cvc4 can then discharge the two assertions *)
ld_inc r0 rX;
check { reg[0] = at(mem[uint 2 reg rX])'S };
(* check { reg[0] = at(mem[uint 2 reg rX])'S }; *)
sub r14 r0;
ld_inc r0 rX;
check { reg[0] = at(mem[uint 2 reg rX+1])'S };
(* check { reg[0] = at(mem[uint 2 reg rX+1])'S }; *)
sbc r15 r0;
ld_inc r0 rX;
check { reg[0] = at(mem[uint 2 reg rX+2])'S };
(* check { reg[0] = at(mem[uint 2 reg rX+2])'S }; *)
sbc r16 r0;
ld_inc r0 rX;
check { reg[0] = at(mem[uint 2 reg rX+3])'S };
(* check { reg[0] = at(mem[uint 2 reg rX+3])'S }; *)
sbc r17 r0;
ld_inc r0 rX;
check { reg[0] = at(mem[uint 2 reg rX+4])'S };
(* check { reg[0] = at(mem[uint 2 reg rX+4])'S }; *)
sbc r18 r0;
ld_inc r0 rX;
check { reg[0] = at(mem[uint 2 reg rX+5])'S };
(* check { reg[0] = at(mem[uint 2 reg rX+5])'S }; *)
sbc r19 r0;
(* 0xff if carry and 0x00 if no carry *)
sbc r0 r0;
......@@ -544,22 +538,22 @@ assert { uint 6 reg 14 = ?cf*pow2 48 + at(uint 6 reg 14)'B - at(uint 6 mem (uint
(* subtract b0 b5 *)
ldd r1 rY 0;
check { reg[1] = at(mem[uint 2 reg rY])'S };
(* check { reg[1] = at(mem[uint 2 reg rY])'S }; *)
sub r8 r1;
ldd r1 rY 1;
check { reg[1] = at(mem[uint 2 reg rY+1])'S };
(* check { reg[1] = at(mem[uint 2 reg rY+1])'S }; *)
sbc r9 r1;
ldd r1 rY 2;
check { reg[1] = at(mem[uint 2 reg rY+2])'S };
(* check { reg[1] = at(mem[uint 2 reg rY+2])'S }; *)
sbc r10 r1;
ldd r1 rY 3;
check { reg[1] = at(mem[uint 2 reg rY+3])'S };
(* check { reg[1] = at(mem[uint 2 reg rY+3])'S }; *)
sbc r11 r1;
ldd r1 rY 4;
check { reg[1] = at(mem[uint 2 reg rY+4])'S };
(* check { reg[1] = at(mem[uint 2 reg rY+4])'S }; *)
sbc r12 r1;
ldd r1 rY 5;
check { reg[1] = at(mem[uint 2 reg rY+5])'S };
(* check { reg[1] = at(mem[uint 2 reg rY+5])'S }; *)
sbc r13 r1;
(* 0xff if carry and 0x00 if no carry *)
sbc r1 r1;
......@@ -779,11 +773,6 @@ end;
pop r1;
pop r31;
pop r30;
check { uint 6 reg 20 + pow2 48*uint 6 reg 0 = at (uint 6 reg 20 + uint 6 reg 14*uint 6 reg 8)'L11 };
check { at(uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20)'L11 = at(uint 6 mem (uint 2 reg rX) * uint 6 mem (uint 2 reg rY))'S };
check { pow2 48*uint 6 reg 20 + pow2 96*uint 6 reg 0 = pow2 48*at (uint 6 reg 20 + uint 6 reg 14*uint 6 reg 8)'L11 };
check { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 + pow2 96*uint 6 reg 0 = at (uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 + pow2 48*uint 6 reg 14*uint 6 reg 8)'L11 };
check { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 + pow2 96*uint 6 reg 0 = at (uint 6 mem (uint 2 reg rX)*uint 6 mem (uint 2 reg rY))'S + at(pow2 48*uint 6 reg 14*uint 6 reg 8)'L11 };
assert { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 + pow2 96*uint 6 reg 0 = at (uint 6 mem (uint 2 reg rX)*uint 6 mem (uint 2 reg rY))'S + at(pow2 48*uint 6 reg 14*uint 6 reg 8)'L11 };
S.init();
......@@ -870,7 +859,6 @@ assert { reg[30] = 0xFF -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2
(* i do not understand this sequence TODO; also optimise *)
bst r30 0 ;
check { ?tf = 1 - at ?tf 'B };
mov r30 r31;
asr r30;
......@@ -880,26 +868,15 @@ assert { forall t. BV8.eq BV8.zeros (BV8.asr (bitset BV8.zeros 0 t) 1) };
assert { forall t. BV8.eq BV8.ones (BV8.asr (bitset BV8.ones 0 t) 1) };
'QQ:
bld r30 0;
check { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFF \/ reg[30] = 0xFE };
assert { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFE + ?tf };
assert { at reg[30] 'QQ = 0x00 -> reg[30] = ?tf };
check { at reg[30] 'QQ = 0x00 -> reg[30] = 0x00 \/ reg[30] = 0x01 };
check { BV8.nth (BV8.of_int reg[30]) 0 <-> tf.value };
'QQQ:
asr r30;
check { at reg[30] 'QQQ = 0xFE -> reg[30] = 0xFF };
check { at reg[30] 'QQQ = 0x01 -> reg[30] = 0x00 };
check { at reg[30] 'QQQ = 0xFF -> reg[30] = 0xFF };
check { at reg[30] 'QQQ = 0x00 -> reg[30] = 0x00 };
check { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFF };
check { at reg[30] 'QQ = 0x00 -> reg[30] = 0x00 };
check { cf.value <-> tf.value };
assert { reg[30] = if reg[31] = 0xFF then 0xFF else 0 };
assert { ?cf = 1 - at ?tf 'B };
assert { ?cf = 0 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = abs(at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*abs(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) };
assert { ?cf = 1 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = (pow2 96 - 1) - abs(at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*abs(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) };
check { ?cf = 0 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = abs(at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*abs(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) };
check { ?cf = 1 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = (pow2 96 - 1) - abs(at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*abs(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) };
S.modify_r6(); S.modify_r7();
S.modify_r26(); S.modify_r27(); S.modify_r28(); S.modify_r29();
S.modify_r12(); S.modify_r13();
......
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