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

added shadow-registers to remove several assertions and improve verification times

parent a8bc648b
......@@ -981,4 +981,585 @@ 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
let karatsuba48_flat(): unit
(*
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)) }
=
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 *)
clr r22;
clr r23;
movw r12 r22;
movw r20 r22;
(* ;--- Compute L --- *)
ld_inc r2 rX;
ld_inc r3 rX;
ld_inc r4 rX;
ldd r5 rY 0;
ldd r6 rY 1;
ldd r7 rY 2;
'L00:
mul r2 r7;
movw r10 r0;
mul r2 r5;
movw r8 r0;
mul r2 r6;
add r9 r0;
adc r10 r1;
adc r11 r23;
mul r3 r7;
movw r14 r0;
mul r3 r5;
add r9 r0;
adc r10 r1;
adc r11 r14;
adc r15 r23;
mul r3 r6;
add r10 r0;
adc r11 r1;
adc r12 r15;
mul r4 r7;
movw r14 r0;
mul r4 r5;
add r10 r0;
adc r11 r1;
adc r12 r14;
adc r15 r23;
mul r4 r6;
add r11 r0;
adc r12 r1;
adc r13 r15;
(* original position
std rZ 0 r8;
std rZ 1 r9;
std rZ 2 r10;
*)
(* ;--- load a3..a5 and b3..b5 --- *)
ld_inc r14 rX;
ld_inc r15 rX;
ld_inc r16 rX;
ldd r17 rY 3;
ldd r18 rY 4;
ldd r19 rY 5;
std rZ 0 r8;
std rZ 1 r9;
std rZ 2 r10;
'L11:
(* ;--- subtract a0-a3 --- *)
sub r2 r14;
sbc r3 r15;
sbc r4 r16;
(* ; 0xff if carry and 0x00 if no carry *)
sbc r26 r26;
(* ;--- subtract b0-b3 --- *)
sub r5 r17;
sbc r6 r18;
sbc r7 r19;
(* ; 0xff if carry and 0x00 if no carry *)
sbc r27 r27;
(* ;--- absolute values --- *)
eor r2 r26;
eor r3 r26;
eor r4 r26;
eor r5 r27;
eor r6 r27;
eor r7 r27;
sub r2 r26;
sbc r3 r26;
sbc r4 r26;
sub r5 r27;
sbc r6 r27;
sbc r7 r27;
'Tmp:
(* ;--- Compute H + (l3l4l5) --- *)
mul r14 r19;
movw r24 r0;
mul r14 r17;
add r11 r0;
adc r12 r1;
adc r13 r24;
adc r25 r23;
mul r14 r18;
add r12 r0;
adc r13 r1;
adc r20 r25;
mul r15 r19;
movw r24 r0;
mul r15 r17;
add r12 r0;
adc r13 r1;
adc r20 r24;
adc r25 r23;
mul r15 r18;
add r13 r0;
adc r20 r1;
adc r21 r25;
mul r16 r19;
movw r24 r0;
mul r16 r17;
add r13 r0;
adc r20 r1;
adc r21 r24;
adc r25 r23;
mul r16 r18;
movw r18 r22;
add r20 r0;
adc r21 r1;
adc r22 r25;
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 };
(* ;--- Compute M --- *)
mul r2 r7;
movw r16 r0;
mul r2 r5;
movw r14 r0;
mul r2 r6;
add r15 r0;
adc r16 r1;
adc r17 r23;
mul r3 r7;
movw r24 r0;
mul r3 r5;
add r15 r0;
adc r16 r1;
adc r17 r24;
adc r25 r23;
mul r3 r6;
add r16 r0;
adc r17 r1;
adc r18 r25;
mul r4 r7;
movw r24 r0;
mul r4 r5;
add r16 r0;
adc r17 r1;
adc r18 r24;
adc r25 r23;
mul r4 r6;
add r17 r0;
adc r18 r1;
adc r19 r25;
'Pre:
(* ;--- process sign bit --- *)
eor r26 r27;
com r26;
assert { reg[26] = 0xFF <-> at((uint 3 reg 2 < uint 3 reg 14) <-> (uint 3 reg 5 < uint 3 reg 17))'L11 };
(* ;--- add l3+h0 to l0 and h3 --- *)
add r8 r11;
adc r9 r12;
adc r10 r13;
adc r11 r20;
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 };
(* ; merge carry and borrow *)
adc r23 r26;
mov r0 r23;
asr r0;
(* ; invert all bits or do nothing *)
eor r14 r26;
eor r15 r26;
eor r16 r26;
eor r17 r26;
eor r18 r26;
eor r19 r26;
add r26 r26; (* ; sets carry if R26 = 0xff *)
(* ; add in M *)
adc r8 r14;
adc r9 r15;
adc r10 r16;
adc r11 r17;
adc r12 r18;
adc r13 r19;
(* ; propagate carry/borrow *)
adc r20 r23;
adc r21 r0;
adc r22 r0;
(* the following 5 asserts re-state some trivial facts *)
assert { at(uint 3 reg 2)'L00 = at(uint 3 reg 2)'L11 };
assert { at(uint 3 reg 5)'L00 = at(uint 3 reg 5)'L11 };
assert { at(uint 3 reg 2*uint 3 reg 5)'L00 = at(uint 3 reg 2*uint 3 reg 5)'L11 };
assert { at((uint 3 reg 2 + pow2 24*uint 3 reg 14))'L11 = at(uint 6 mem (uint 2 reg rX))'S };
assert { at((uint 3 reg 5 + pow2 24*uint 3 reg 17))'L11 = at(uint 6 mem (uint 2 reg rY))'S };
(* the following 3 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 { 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
};
std rZ 3 r8;
std rZ 4 r9;
std rZ 5 r10;
std rZ 6 r11;
std rZ 7 r12;
std rZ 8 r13;
std rZ 9 r20;
std rZ 10 r21;
std rZ 11 r22
use avrmodel.Shadow as S
let karatsuba48_marked(): unit
(*
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)) }
=
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;
ld_inc r4 rX;
ldd r5 rY 0;
ldd r6 rY 1;
ldd r7 rY 2;
'L00:
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 8 = old(uint 3 reg 2 * uint 3 reg 5) }
mul r2 r7;
movw r10 r0;
mul r2 r5;
movw r8 r0;
mul r2 r6;
add r9 r0;
adc r10 r1;
adc r11 r23;
mul r3 r7;
movw r14 r0;
mul r3 r5;
add r9 r0;
adc r10 r1;
adc r11 r14;
adc r15 r23;
mul r3 r6;
add r10 r0;
adc r11 r1;
adc r12 r15;
mul r4 r7;
movw r14 r0;
mul r4 r5;
add r10 r0;
adc r11 r1;
adc r12 r14;
adc r15 r23;
mul r4 r6;
add r11 r0;
adc r12 r1;
adc r13 r15;
S.modify_r0(); S.modify_r1(); S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15();
end;
(* original position
std rZ 0 r8;
std rZ 1 r9;
std rZ 2 r10;
*)
(* ;--- load a3..a5 and b3..b5 --- *)
ld_inc r14 rX;
ld_inc r15 rX;
ld_inc r16 rX;
ldd r17 rY 3;
ldd r18 rY 4;
ldd r19 rY 5;
std rZ 0 r8;
std rZ 1 r9;
std rZ 2 r10;
'L11:
assert { at(uint 3 reg 2*uint 3 reg 5)'L00 = at(uint 3 reg 2*uint 3 reg 5)'L11 };
assert { at(uint 3 reg 2 + pow2 24*uint 3 reg 14)'L11 = at(uint 6 mem (uint 2 reg rX))'S };
abstract ensures { S.synchronized S.shadow reg }
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19();
S.modify_r26(); S.modify_r27();
end;
(*
S.init();
*)
abstract
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)) }
ensures { reg[26] = if old (uint 3 reg 2 < uint 3 reg 14) then 0xFF else 0x00 }
ensures { reg[27] = if old (uint 3 reg 5 < uint 3 reg 17) then 0xFF else 0x00 }
(* ;--- subtract a0-a3 --- *)
sub r2 r14;
sbc r3 r15;
sbc r4 r16;
(* ; 0xff if carry and 0x00 if no carry *)
sbc r26 r26;
(* ;--- subtract b0-b3 --- *)
sub r5 r17;
sbc r6 r18;
sbc r7 r19;
(* ; 0xff if carry and 0x00 if no carry *)
sbc r27 r27;
(* ;--- absolute values --- *)
eor r2 r26;
eor r3 r26;
eor r4 r26;
eor r5 r27;
eor r6 r27;
eor r7 r27;
sub r2 r26;
sbc r3 r26;
sbc r4 r26;
sub r5 r27;
sbc r6 r27;
sbc r7 r27;
S.modify_r2();
S.modify_r3();
S.modify_r4();
S.modify_r5();
S.modify_r6();
S.modify_r7();
S.modify_r26();
S.modify_r27();
end;
'Tmp:
(* ;--- Compute H + (l3l4l5) --- *)
(*
S.init();
*)
abstract
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 }
mul r14 r19;
movw r24 r0;
mul r14 r17;
add r11 r0;
adc r12 r1;
adc r13 r24;
adc r25 r23;
mul r14 r18;
add r12 r0;
adc r13 r1;
adc r20 r25;
mul r15 r19;
movw r24 r0;
mul r15 r17;
add r12 r0;
adc r13 r1;
adc r20 r24;
adc r25 r23;
mul r15 r18;
add r13 r0;
adc r20 r1;
adc r21 r25;
mul r16 r19;
movw r24 r0;
mul r16 r17;
add r13 r0;
adc r20 r1;
adc r21 r24;
adc r25 r23;
mul r16 r18;
movw r18 r22;
add r20 r0;
adc r21 r1;
adc r22 r25;
S.modify_r0(); S.modify_r1();
S.modify_r11(); S.modify_r12(); S.modify_r13();
S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21(); S.modify_r22();
S.modify_r24(); S.modify_r25();
end;
(* ;--- Compute M --- *)
(*
S.init();
*)
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 14 = old (uint 3 reg 2*uint 3 reg 5) }
mul r2 r7;
movw r16 r0;
mul r2 r5;
movw r14 r0;
mul r2 r6;
add r15 r0;
adc r16 r1;
adc r17 r23;
mul r3 r7;
movw r24 r0;
mul r3 r5;
add r15 r0;
adc r16 r1;
adc r17 r24;
adc r25 r23;
mul r3 r6;
add r16 r0;
adc r17 r1;
adc r18 r25;
mul r4 r7;
movw r24 r0;
mul r4 r5;
add r16 r0;
adc r17 r1;
adc r18 r24;
adc r25 r23;
mul r4 r6;
add r17 r0;
adc r18 r1;
adc r19 r25;
S.modify_r0(); S.modify_r1();
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19();
S.modify_r24(); S.modify_r25();
end;
(*
S.init();
*)
abstract
ensures { S.synchronized S.shadow reg }
ensures { old(uint 3 reg 8) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf*pow2 72 = (pow2 24+1)*(at(uint 3 reg 2*uint 3 reg 5)'L00 + at(pow2 24*uint 3 reg 14*uint 3 reg 17)'L11) }
ensures { reg[26] = 0xFF -> uint 6 reg 14 = at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
ensures { reg[26] = 0x00 -> uint 6 reg 14 = -at((uint 3 reg 2 - uint 3 reg 14)*(uint 3 reg 5 - uint 3 reg 17))'L11 }
ensures { reg[26] = 0x00 \/ reg[26] = 0xFF }
'Pre:
(* ;--- process sign bit --- *)
eor r26 r27;
com r26;
assert { reg[26] = 0xFF <-> at((uint 3 reg 2 < uint 3 reg 14) <-> (uint 3 reg 5 < uint 3 reg 17))'L11 };
(* ;--- add l3+h0 to l0 and h3 --- *)
add r8 r11;
adc r9 r12;
adc r10 r13;
adc r11 r20;
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;
(*
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 { 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;
mov r0 r23;
asr r0;
(* ; invert all bits or do nothing *)
eor r14 r26;
eor r15 r26;
eor r16 r26;
eor r17 r26;
eor r18 r26;
eor r19 r26;
add r26 r26; (* ; sets carry if R26 = 0xff *)
S.modify_r23(); S.modify_r26();
S.modify_r0();
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19();
end;
(* ; add in M *)
adc r8 r14;
adc r9 r15;
adc r10 r16;
adc r11 r17;
adc r12 r18;
adc r13 r19;
(* ; propagate carry/borrow *)
adc r20 r23;
adc r21 r0;
adc r22 r0;
(* the following 3 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 { 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
};
std rZ 3 r8;
std rZ 4 r9;
std rZ 5 r10;
std rZ 6 r11;
std rZ 7 r12;
std rZ 8 r13;
std rZ 9 r20;
std rZ 10 r21;
std rZ 11 r22
end
......@@ -1718,3 +1718,366 @@ let clr (dst: register): unit
= eor dst dst.data
end
module Shadow
use import int.Int
use import ref.Ref
use import AVRint as AVR
use map.Map
type shadow_registers = {
ghost r0: ref int;
ghost r1: ref int;
ghost r2: ref int;
ghost r3: ref int;
ghost r4: ref int;
ghost r5: ref int;
ghost r6: ref int;
ghost r7: ref int;
ghost r8: ref int;
ghost r9: ref int;
ghost r10: ref int;
ghost r11: ref int;
ghost r12: ref int;
ghost r13: ref int;
ghost r14: ref int;
ghost r15: ref int;
ghost r16: ref int;
ghost r17: ref int;
ghost r18: ref int;
ghost r19: ref int;
ghost r20: ref int;
ghost r21: ref int;
ghost r22: ref int;
ghost r23: ref int;
ghost r24: ref int;
ghost r25: ref int;
ghost r26: ref int;
ghost r27: ref int;
ghost r28: ref int;
ghost r29: ref int;
ghost r30: ref int;
ghost r31: ref int
}
predicate synchronized (self: shadow_registers) (avr: address_space) =
avr[0] = !(self.r0) /\
avr[1] = !(self.r1) /\
avr[2] = !(self.r2) /\
avr[3] = !(self.r3) /\
avr[4] = !(self.r4) /\
avr[5] = !(self.r5) /\
avr[6] = !(self.r6) /\
avr[7] = !(self.r7) /\
avr[8] = !(self.r8) /\
avr[9] = !(self.r9) /\
avr[10] = !(self.r10) /\
avr[11] = !(self.r11) /\
avr[12] = !(self.r12) /\
avr[13] = !(self.r13) /\
avr[14] = !(self.r14) /\
avr[15] = !(self.r15) /\
avr[16] = !(self.r16) /\
avr[17] = !(self.r17) /\
avr[18] = !(self.r18) /\
avr[19] = !(self.r19) /\
avr[20] = !(self.r20) /\
avr[21] = !(self.r21) /\
avr[22] = !(self.r22) /\
avr[23] = !(self.r23) /\
avr[24] = !(self.r24) /\
avr[25] = !(self.r25) /\
avr[26] = !(self.r26) /\
avr[27] = !(self.r27) /\
avr[28] = !(self.r28) /\
avr[29] = !(self.r29) /\
avr[30] = !(self.r30) /\
avr[31] = !(self.r31)