Commit dcadaed8 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Update karatsuba files

parent 7193c010
module BV_asr_Lemmas
use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision
use bv.BV8
use int.Int
use bv.Pow2int
use int.EuclideanDivision
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 asr_0: (asr zeros 1) = zeros
lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: (asr ones 1) = ones
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
......@@ -21,10 +21,10 @@ end
module AvrModelLemmas
use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int
use int.Int
use map.Map
use int.EuclideanDivision
use bv.Pow2int
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
......@@ -35,15 +35,15 @@ end
module KaratAvr
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use int.Int
use int.EuclideanDivision
use bv.Pow2int
use bv.BV8
use avrmodel.AVRint
use AvrModelLemmas
use BV_asr_Lemmas
use import int.Abs
use int.Abs
use avrmodel.Shadow as S
......@@ -66,7 +66,7 @@ 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)) }
=
'S:
label S in
(* ; init zero registers *)
clr r22;
clr r23;
......@@ -80,9 +80,9 @@ let karatsuba48_marked(): unit
ldd r5 rY 0;
ldd r6 rY 1;
ldd r7 rY 2;
'L00:
label L00 in
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 8 = old(uint 3 reg 2 * uint 3 reg 5) }
mul r2 r7;
......@@ -136,10 +136,10 @@ end;
std rZ 0 r8;
std rZ 1 r9;
std rZ 2 r10;
'L11:
label L11 in
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
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)) }
......@@ -186,7 +186,7 @@ end;
(* ;--- Compute H + (l3l4l5) --- *)
(* S.init(); *)
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 3 reg 11 + pow2 24*uint 3 reg 20 = old (uint 3 reg 11 + uint 3 reg 14*uint 3 reg 17) }
ensures { reg[18] = 0 /\ reg[19] = 0 }
......@@ -235,7 +235,7 @@ end;
(* ;--- Compute M --- *)
(* S.init(); *)
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 14 = old (uint 3 reg 2*uint 3 reg 5) }
......@@ -278,11 +278,11 @@ ensures { uint 6 reg 14 = old (uint 3 reg 2*uint 3 reg 5) }
end;
(* S.init(); *)
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 48 = old (uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 3 reg 11 + pow2 24*uint 3 reg 20) }
ensures { reg[26] = if old(reg[26] = reg[27]) then 0xFF else 0x00 }
'Pre:
label Pre in
(* ;--- process sign bit --- *)
eor r26 r27;
com r26;
......@@ -298,7 +298,7 @@ ensures { reg[26] = if old(reg[26] = reg[27]) then 0xFF else 0x00 }
end;
(* S.init(); *)
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 14 = ?cf*(pow2 48 - 1) + (if old (reg[26] = 0xFF) then -1 else 1)*old(uint 6 reg 14) }
ensures { let cor = reg[23] + (pow2 8+pow2 16)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 24 + old ?cf - ?cf }
......@@ -321,7 +321,7 @@ ensures { let cor = reg[23] + (pow2 8+pow2 16)*reg[0] in cor = old ?cf - ?cf \/
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19();
end;
(* ; add in M *)
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 72 = old(?cf + uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 6 reg 14 + pow2 48*(reg[23] + (pow2 8+pow2 16)*reg[0])) }
adc r8 r14;
adc r9 r15;
......@@ -339,28 +339,28 @@ S.modify_r20(); S.modify_r21(); S.modify_r22();
end;
(* the following asserts establish a bounds result about multiplying uint's -- can't this be put in a lemma? *)
assert { 0 <= at((uint 3 reg 2 + pow2 24*uint 3 reg 14))'L11 <= pow2 48-1 };
assert { 0 <= at((uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 <= pow2 48-1 };
assert { 0 <= at((uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 <= (pow2 48-1)*(pow2 48-1) };
assert { 0 <= ((uint 3 reg 2 + pow2 24*uint 3 reg 14) at L11) <= pow2 48-1 };
assert { 0 <= ((uint 3 reg 5 + pow2 24*uint 3 reg 17) at L11) <= pow2 48-1 };
assert { 0 <= ((uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) at L11) <= (pow2 48-1)*(pow2 48-1) };
assert { 0 <= at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 < pow2 96 };
assert { 0 <= ((uint 3 reg 8) at L11) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 < pow2 96 };
(* these checks can be useful in debugging when porting to a new version, but are not needed at the moment if we
add the above assert, which is much simpler to comprehend *)
(*
check { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 \/
at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 + pow2 96
check { ((uint 3 reg 8) at L11) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= ((( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )) at L11) \/
((uint 3 reg 8) at L11) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= ((( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )) at L11) + pow2 96
};
check { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11
check { ((uint 3 reg 8) at L11) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20
= ((( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )) at L11)
};
check { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= at( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )'L11 + ?cf*pow2 96
check { ((uint 3 reg 8) at L11) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 96
= ((( (uint 3 reg 2 + pow2 24*uint 3 reg 14)*(uint 3 reg 5 + pow2 24*uint 3 reg 17) )) at L11) + ?cf*pow2 96
};
*)
......
module BV_asr_Lemmas
use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision
use bv.BV8
use int.Int
use bv.Pow2int
use int.EuclideanDivision
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 asr_0: (asr zeros 1) = zeros
lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: (asr ones 1) = ones
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
......@@ -27,10 +27,10 @@ end
module AvrModelLemmas
use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int
use int.Int
use map.Map
use int.EuclideanDivision
use bv.Pow2int
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
......@@ -41,15 +41,16 @@ end
module KaratAvr
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use int.Int
use int.EuclideanDivision
use bv.Pow2int
use bv.BV8
use avrmodel.AVRint
use AvrModelLemmas
use BV_asr_Lemmas
use int.Abs
use import int.Abs
use avrmodel.Shadow as S
lemma mul_bound_preserve:
......@@ -61,7 +62,7 @@ let karatsuba64_marked()
requires { 32 <= uint 2 reg rZ < pow2 15 }
ensures { uint 16 mem (old (uint 2 reg rZ)) = old (uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY)) }
=
'S:
label S in
(* init rZero registers *)
clr r20;
clr r21;
......@@ -77,9 +78,9 @@ let karatsuba64_marked()
ldd r8 rY 2;
ldd r9 rY 3;
'L00:
label L00 in
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 = old(uint 4 reg 2 * uint 4 reg 6) }
mul r2 r8; (* a0*b2 *)
movw r12 r0;
......@@ -172,14 +173,14 @@ end;
std rZ 2 r12;
std rZ 3 r13;
'L11:
label L11 in
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 2 = old (abs (uint 4 reg 2 - uint 4 reg 18)) }
ensures { uint 4 reg 6 = old (abs (uint 4 reg 6 - uint 4 reg 22)) }
ensures { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22)) }
'B:
label B in
(* subtract a0 a4 *)
sub r2 r18;
sbc r3 r19;
......@@ -223,8 +224,8 @@ ensures { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uin
end;
S.init();
'Tmp:
abstract ensures { S.synchronized S.shadow reg }
label Tmp in
begin ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18 = old (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) }
(* compute h (l4 l5 l6 l7) *)
mul r18 r22;
......@@ -307,7 +308,7 @@ ensures { uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18 = old (u
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = old (uint 4 reg 2*uint 4 reg 6) }
(* compute m *)
mul r2 r6;
......@@ -385,11 +386,11 @@ ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = old (uint 4 reg 2*uint 4 reg 6)
end;
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + ?cf*pow2 64 = old(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18) }
(* add l4 h0 to l0 and h4 *)
'B:
label B in
add r10 r14;
adc r11 r15;
adc r12 r16;
......@@ -403,13 +404,13 @@ ensures { uint 8 reg 10 + ?cf*pow2 64 = old(uint 8 reg 10 + uint 4 reg 14 + pow2
end;
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
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 *)
'B:
label B in
bld r27 0;
dec 27;
assert { reg[27] = 0xFF*(1 - ?tf) };
......@@ -419,7 +420,7 @@ assert { reg[27] = 0xFF*(1 - ?tf) };
mov r0 r26;
asr r0;
'B:
label B in
(* invert all bits or do nothing *)
eor r20 r27;
eor r21 r27;
......@@ -429,7 +430,7 @@ assert { reg[27] = 0xFF*(1 - ?tf) };
eor r25 r27;
eor r2 r27;
eor r3 r27;
'B:
label B in
add r27 r27; (* sets carry flag if r27 = 0xff *)
S.modify_r0(); S.modify_r26(); S.modify_r27();
S.modify_r2(); S.modify_r3();
......@@ -437,7 +438,7 @@ assert { reg[27] = 0xFF*(1 - ?tf) };
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf = old(?cf + uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(uint 1 reg 26 + (pow2 8+pow2 16+pow2 24)*reg[0])) }
(* add in m *)
adc r10 r20;
......@@ -461,26 +462,26 @@ end;
(* the checks will speed things up, but are not necessary *)
(*
check { 0 <= at(uint 4 reg 10)'L11 /\ 0 <= uint 8 reg 10 /\ 0 <= uint 2 reg 28 /\ 0 <= pow2 16*uint 2 reg 18 };
check { 0 <= ((uint 4 reg 10) at L11) /\ 0 <= uint 8 reg 10 /\ 0 <= uint 2 reg 28 /\ 0 <= pow2 16*uint 2 reg 18 };
*)
assert { 0 <= at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
assert { 0 <= ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
assert { 0 <= at((uint 4 reg 2 + pow2 32*uint 4 reg 18))'L11 <= pow2 64-1 };
assert { 0 <= at((uint 4 reg 6 + pow2 32*uint 4 reg 22))'L11 <= pow2 64-1 };
assert { 0 <= at((uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22))'L11 <= (pow2 64-1)*(pow2 64-1) };
assert { 0 <= ((uint 4 reg 2 + pow2 32*uint 4 reg 18) at L11) <= pow2 64-1 };
assert { 0 <= ((uint 4 reg 6 + pow2 32*uint 4 reg 22) at L11) <= pow2 64-1 };
assert { 0 <= ((((uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22))) at L11) <= (pow2 64-1)*(pow2 64-1) };
(*
check {
at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
((( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )) at L11)
\/
at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
((( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )) at L11)
+ pow2 128
};
check { at(uint 4 reg 10)'L11 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
= at( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L11
check { ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
= ((( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )) at L11)
};
*)
......
module BV_asr_Lemmas
use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision
use bv.BV8
use int.Int
use bv.Pow2int
use int.EuclideanDivision
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 asr_0: (asr zeros 1) = zeros
lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: (asr ones 1) = ones
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
......@@ -42,10 +42,10 @@ end
module AvrModelLemmas
use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int
use int.Int
use map.Map
use int.EuclideanDivision
use bv.Pow2int
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
......@@ -56,15 +56,15 @@ end
module KaratAvr
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use int.Int
use int.EuclideanDivision
use bv.Pow2int
use bv.BV8
use avrmodel.AVRint
use AvrModelLemmas
use BV_asr_Lemmas
use import int.Abs
use int.Abs
use avrmodel.Shadow as S
......@@ -79,7 +79,7 @@ let karatsuba80_marked()
requires { uint 2 reg rZ <= uint 2 reg rY \/ uint 2 reg rZ >= uint 2 reg rY+10 }
ensures { uint 20 mem (old (uint 2 reg rZ)) = old (uint 10 mem (uint 2 reg rX) * uint 10 mem (uint 2 reg rY)) }
=
'S:
label S in
(* init rZero registers *)
clr r18;
clr r19;
......@@ -97,11 +97,11 @@ let karatsuba80_marked()
ldd r10 rY 3;
ldd r11 rY 4;
'L00:
label L00 in
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 10 reg 12 = old(uint 5 reg 2 * uint 5 reg 7) }
'B:
label B in
mul r2 r9;
movw r14 r0;
mul r2 r7;
......@@ -201,7 +201,7 @@ S.modify_r0(); S.modify_r1();
S.modify_r24(); S.modify_r25();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21();
end;
'L00':
label L00' in
std rZ 0 r12;
std rZ 1 r13;
std rZ 2 r14;
......@@ -219,10 +219,10 @@ end;
ldd r25 rY 7;
ldd r26 rY 8;
ldd r27 rY 9;
'L11:
label L11 in
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 2 = old (abs (uint 5 reg 2 - uint 5 reg 12)) }
ensures { uint 5 reg 7 = old (abs (uint 5 reg 7 - uint 5 reg 23)) }
ensures { ?tf = 0 <-> old((uint 5 reg 2 < uint 5 reg 12) <-> (uint 5 reg 7 < uint 5 reg 23)) }
......@@ -277,7 +277,7 @@ ensures { reg[22] = 0 } (* strange location! *)
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 10 reg 17 = old (uint 5 reg 17 + uint 5 reg 12*uint 5 reg 23) }
(* compute h (l5 l6 l7 l8 l9) *)
mul r23 r14;
......@@ -389,7 +389,7 @@ ensures { uint 10 reg 17 = old (uint 5 reg 17 + uint 5 reg 12*uint 5 reg 23) }
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = old (uint 5 reg 2*uint 5 reg 7) }
(* compute m *)
clr r27;
......@@ -507,10 +507,10 @@ end;
ldd r11 rZ 4 ;
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 7 + pow2 40*uint 5 reg 17 + ?cf*pow2 80 = old (uint 5 reg 7 + pow2 40*uint 5 reg 17 + uint 10 reg 17) }
'B:
label B in
add r7 r17;
adc r8 r18;
adc r9 r19;
......@@ -527,11 +527,11 @@ ensures { uint 5 reg 7 + pow2 40*uint 5 reg 17 + ?cf*pow2 80 = old (uint 5 reg 7
end;
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ?cf*(pow2 80 - 1) + (if ?tf = 0 then -1 else 1)*old (uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2) }
ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 40 + old ?cf - ?cf }
'B:
label B in
(* process sign bit *)
clr r28;
clr r29;
......@@ -556,8 +556,8 @@ ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = o
eor r4 r29;
eor r5 r29;
(*
check { reg[29] = 0x00 -> 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 { 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 };
check { reg[29] = 0x00 -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = ((uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2) at B) };
check { reg[29] = 0xFF -> uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 = pow2 80 - 1 - ((uint 5 reg 12 + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2) at B) };
*)
add r29 r29; (* sets carry flag if r29 = 0xff *)
(*
......@@ -572,7 +572,7 @@ ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = o
end;
S.init();
abstract
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 7 + pow2 40*uint 10 reg 17 + ?cf*pow2 120 = old(uint 5 reg 7 + pow2 40*uint 10 reg 17 + uint 5 reg 12 + ?cf + pow2 40*uint 1 reg 27 + pow2 48*uint 4 reg 2 + pow2 80*reg[28] + (pow2 88 + pow2 96 + pow2 104 + pow2 112)*reg[0] ) }
(* add in m *)
......@@ -598,24 +598,24 @@ 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 * 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 { 0 <= ((uint 5 reg 2 + pow2 40*uint 5 reg 12) at L11) * ((uint 5 reg 7 + pow2 40*uint 5 reg 23) at L11) <= (pow2 80-1)*(pow2 80-1)
by 0 <= ((uint 5 reg 2 + pow2 40*uint 5 reg 12) at L11) <= pow2 80-1
/\ 0 <= ((uint 5 reg 7 + pow2 40*uint 5 reg 23) at L11) <= pow2 80-1
};
assert { "expl:obvious" 0 <= uint 10 reg 17 };
assert { 0 <= at (uint 5 reg 12)'L00' + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 < pow2 160 };
assert { 0 <= uint 10 reg 17 }; (* expl:obvious *)
assert { 0 <= (( (uint 5 reg 12)) at L00') + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 < 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
(( (uint 5 reg 12)) at L00') + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 160
= (pow2 40+1)*(((uint 5 reg 2*uint 5 reg 7 + pow2 40*uint 5 reg 12*uint 5 reg 23) at L11))
- pow2 40 * ((((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23)) ) at 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
((uint 5 reg 2*uint 5 reg 7) at L00) = ((uint 5 reg 2*uint 5 reg 7) at L11)
/\
at(uint 5 reg 7)'L00 + pow2 40*at(uint 5 reg 23)'L11 = at(uint 10 mem (uint 2 reg rY))'S
((uint 5 reg 7) (( L00) + pow2 40*((uint 5 reg 23) at L11) = at(uint 10 mem (uint 2 reg rY))) at S)
};
*)
......
module BV_asr_Lemmas
use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision
use bv.BV8
use int.Int
use bv.Pow2int
use int.EuclideanDivision
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 asr_0: (asr zeros 1) = zeros
lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: (asr ones 1) = ones
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
......@@ -42,10 +42,10 @@ end
module AvrModelLemmas
use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int
use int.Int
use map.Map
use int.EuclideanDivision
use bv.Pow2int
lemma register_file_invariant_strengthen:
forall m m': map int int. (forall i. 0 <= m[i] < 256) -> (forall i. 0 <= m'[i] < 256) -> (forall i j. 0 <= m[i]*m'[j] <= 255*255)
......@@ -60,15 +60,15 @@ end
module KaratAvr
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use int.Int
use int.EuclideanDivision
use bv.Pow2int
use bv.BV8
use avrmodel.AVRint
use AvrModelLemmas
use BV_asr_Lemmas
use import int.Abs
use int.Abs
use avrmodel.Shadow as S
......@@ -84,7 +84,7 @@ let karatsuba96_marked()
requires { uint 2 reg rZ+6 <= uint 2 reg rY \/ uint 2 reg rZ >= uint 2 reg rY+12 }
ensures { uint 24 mem (old (uint 2 reg rZ)) = old (uint 12 mem (uint 2 reg rX) * uint 12 mem (uint 2 reg rY)) }
=
'S:
label S in
(* init rZero registers *)
clr r20;
clr r21;
......@@ -92,7 +92,7 @@ let karatsuba96_marked()
movw r24 r20;
S.init();
abstract ensures { S.synchronized S.shadow reg }
begin ensures { S.synchronized S.shadow reg }
ensures { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 = old(uint 6 mem (uint 2 reg rX) * uint 6 mem (uint 2 reg rY)) }
ensures { uint 2 reg rX = old(uint 2 reg rX+6) }
ensures { forall i. not (uint 2 reg rZ <= i < uint 2 reg rZ+6) -> mem[i] = (old mem)[i] }
......@@ -105,7 +105,7 @@ ensures { forall i. not (uint 2 reg rZ <= i < uint 2 reg rZ+6) -> mem[i] = (old
ldd r12 rY 4;
ldd r13 rY 5;
'B:
label B in
mul r2 r10; (* a0 * b2 *)
movw r16 r0;
mul r2 r8; (* a0 * b0 *)
......@@ -124,10 +124,10 @@ ensures { forall i. not (uint 2 reg rZ <= i < uint 2 reg rZ+6) -> mem[i] = (old
add r19 r0;
adc r20 r1;
assert { uint 7 reg 14 = at(uint 1 reg 2 * uint 6 reg 8)'B };
assert { uint 7 reg 14 = ((uint 1 reg 2 * uint 6 reg 8) at B) };
ld_inc r3 rX;