Commit 5538acc9 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

convert karatsuba80 into a 'localized' version

parent 887f74f0
......@@ -225,7 +225,7 @@ S.init();
abstract 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 <-> at((uint 5 reg 2 < uint 5 reg 12) <-> (uint 5 reg 7 < uint 5 reg 23))'L11 }
ensures { ?tf = 0 <-> old((uint 5 reg 2 < uint 5 reg 12) <-> (uint 5 reg 7 < uint 5 reg 23)) }
ensures { reg[22] = 0 } (* strange location! *)
(* subtract a0 a5 *)
sub r2 r12;
......@@ -505,12 +505,11 @@ end;
ldd r9 rZ 2;
ldd r10 rZ 3;
ldd r11 rZ 4 ;
assert { uint 5 reg 7 = at (uint 5 reg 12)'L00' };
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { old(uint 5 reg 7) + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?cf*pow2 120 = (pow2 40+1)*(at(uint 5 reg 2*uint 5 reg 7)'L00 + at(pow2 40*uint 5 reg 12*uint 5 reg 23)'L11) }
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:
add r7 r17;
adc r8 r18;
......@@ -522,8 +521,6 @@ ensures { old(uint 5 reg 7) + pow2 40*uint 5 reg 7 + pow2 80*uint 10 reg 17 + ?c
adc r19 r24;
adc r20 r25;
adc r21 r26;
assert { uint 5 reg 7 + pow2 40*uint 5 reg 17 + ?cf*pow2 80
= at(uint 5 reg 7 + pow2 40*uint 5 reg 17 + uint 10 reg 17) 'B };
(* store carrrY later in r0 *)
S.modify_r7(); S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11();
S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21();
......@@ -532,11 +529,8 @@ end;
S.init();
abstract
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) - at((uint 5 reg 2 - uint 5 reg 12)*(uint 5 reg 7 - uint 5 reg 23))'L11 }
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 }
(*
ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = if ?cf <= old ?cf then old ?cf - ?cf else pow2 40 + old ?cf - ?cf }
*)
'B:
(* process sign bit *)
clr r28;
......@@ -561,12 +555,14 @@ ensures { let cor = reg[28] + (pow2 8+pow2 16+pow2 24+pow2 32)*reg[0] in cor = i
eor r3 r29;
eor r4 r29;
eor r5 r29;
assert { 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 };
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 };
(*
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 };
*)
add r29 r29; (* sets carry flag if r29 = 0xff *)
assert { ?cf = 1 - ?tf };
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 = 1 - ?tf };
*)
S.modify_r0();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16();
......@@ -608,8 +604,10 @@ assert { 0 <= at(uint 5 reg 2 + pow2 40*uint 5 reg 12)'L11 * at(uint 5 reg 7 + p
};
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 {
(*
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
......@@ -619,6 +617,7 @@ assert {
/\
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.
Markdown is supported
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