Commit 274df245 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

modified 96-bit karatsuba in similar sense

parent 5538acc9
...@@ -484,7 +484,8 @@ end; ...@@ -484,7 +484,8 @@ end;
push r7; push r7;
S.init(); S.init();
(* TODO optimise *) (* COMMENT: this block has not been localized, as in this case it complicates matters;
it is more natural to express this in the global parameters *)
abstract ensures { S.synchronized S.shadow reg } abstract ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 14 = old (abs (uint 6 reg 14 - at(uint 6 mem (uint 2 reg rX))'S)) } ensures { uint 6 reg 14 = old (abs (uint 6 reg 14 - at(uint 6 mem (uint 2 reg rX))'S)) }
ensures { uint 6 reg 8 = old (abs (uint 6 reg 8 - at(uint 6 mem (uint 2 reg rY))'S)) } ensures { uint 6 reg 8 = old (abs (uint 6 reg 8 - at(uint 6 mem (uint 2 reg rY))'S)) }
...@@ -492,6 +493,7 @@ ensures { ?tf = 0 <-> old(uint 6 reg 14) < at(uint 6 mem (uint 2 reg rX))'S <-> ...@@ -492,6 +493,7 @@ ensures { ?tf = 0 <-> old(uint 6 reg 14) < at(uint 6 mem (uint 2 reg rX))'S <->
(* subtract a0 a5 *) (* subtract a0 a5 *)
sbiw r26 12; sbiw r26 12;
'B: 'B:
(* if you transform these checks into asserts, verification will speed up because cvc4 can then discharge the two assertions *) (* if you transform these checks into asserts, verification will speed up because cvc4 can then discharge the two assertions *)
ld_inc r0 rX; ld_inc r0 rX;
(* check { reg[0] = at(mem[uint 2 reg rX])'S }; *) (* check { reg[0] = at(mem[uint 2 reg rX])'S }; *)
...@@ -753,11 +755,10 @@ end; ...@@ -753,11 +755,10 @@ end;
pop r1; pop r1;
pop r31; pop r31;
pop r30; pop r30;
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(); S.init();
abstract ensures { S.synchronized S.shadow reg } abstract ensures { S.synchronized S.shadow reg }
ensures { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6 reg 0 + ?cf*pow2 144 = (pow2 48+1)*(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) } ensures { uint 12 reg 14 + ?cf*pow2 96 = old(uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 + uint 6 reg 20 + pow2 48*uint 6 reg 0) }
(* add l5 h0 to l0 and h5 *) (* add l5 h0 to l0 and h5 *)
'B: 'B:
ldd r14 rZ 0; ldd r14 rZ 0;
...@@ -785,7 +786,6 @@ original location ...@@ -785,7 +786,6 @@ original location
adc r23 r3; adc r23 r3;
adc r24 r4; adc r24 r4;
adc r25 r5; adc r25 r5;
assert { uint 12 reg 14 + ?cf*pow2 96 = at(uint 6 mem (uint 2 reg rZ) + pow2 48*uint 6 reg 20 + uint 6 reg 20 + pow2 48*uint 6 reg 0)'B };
(* store carrrY in t register *) (* store carrrY in t register *)
S.modify_r14(); S.modify_r14();
S.modify_r15(); S.modify_r15();
...@@ -808,8 +808,7 @@ end; ...@@ -808,8 +808,7 @@ end;
S.init(); S.init();
abstract abstract
ensures { S.synchronized S.shadow reg } 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) + (if old ?tf = 0 then -1 else 1)*old (uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8) }
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 } 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: 'B:
clr r30; clr r30;
...@@ -819,7 +818,9 @@ ensures { let cor = reg[31] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40)*reg[30] i ...@@ -819,7 +818,9 @@ ensures { let cor = reg[31] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40)*reg[30] i
assert { reg[30] = 0xFF*(1 - ?tf) }; assert { reg[30] = 0xFF*(1 - ?tf) };
adc r31 r30; adc r31 r30;
assert { reg[31] = 0 \/ reg[31] = 1 \/ reg[31] = 0xFF }; (*
check { reg[31] = 0 \/ reg[31] = 1 \/ reg[31] = 0xFF };
*)
'Q: 'Q:
(* invert all bits or do nothing *) (* invert all bits or do nothing *)
...@@ -838,17 +839,18 @@ assert { reg[31] = 0 \/ reg[31] = 1 \/ reg[31] = 0xFF }; ...@@ -838,17 +839,18 @@ assert { reg[31] = 0 \/ reg[31] = 1 \/ reg[31] = 0xFF };
assert { reg[30] = 0x00 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = at(uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8)'B }; assert { reg[30] = 0x00 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = at(uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8)'B };
assert { reg[30] = 0xFF -> 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 - at(uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8)'B }; assert { reg[30] = 0xFF -> 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 - at(uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8)'B };
(* i do not understand this sequence TODO; also optimise *) (* this sequence is tricky; commented out assertions are left in to see in detail what happens *)
bst r30 0 ; bst r30 0 ;
mov r30 r31; mov r30 r31; (* assert { reg[30] = if at(?cf = ?tf)'B then (if at(?cf = 0)'B then 0xFF else 0x01) else 0x00 }; *)
asr r30; asr r30; (* assert { reg[30] = if at(?cf = ?tf = 0)'B then 0xFF else 0x00 }; *)
'QQ: 'QQ:
bld r30 0; bld r30 0;
assert { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFE + ?tf }; assert { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFE + ?tf };
assert { at reg[30] 'QQ = 0x00 -> reg[30] = ?tf }; assert { at reg[30] 'QQ = 0x00 -> reg[30] = ?tf };
asr r30; (* assert { reg[30] = if at(?cf = ?tf = 0)'B then 0xFF else ?tf }; *)
asr r30; (* assert { reg[30] = if at(?cf = ?tf = 0)'B then 0xFF else 0x00 }; *)
assert { ?cf = 1 - at ?tf 'B }; assert { ?cf = 1 - at ?tf 'B };
S.modify_r6(); S.modify_r7(); S.modify_r6(); S.modify_r7();
...@@ -858,6 +860,10 @@ assert { ?cf = 1 - at ?tf 'B }; ...@@ -858,6 +860,10 @@ assert { ?cf = 1 - at ?tf 'B };
S.modify_r30(); S.modify_r31(); S.modify_r30(); S.modify_r31();
end; end;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 12 reg 14 + pow2 96*uint 6 reg 0 + ?cf*pow2 144 = old (uint 12 reg 14 + pow2 96*uint 6 reg 0 + ?cf + uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 + pow2 96*reg[31] + (pow2 104 + pow2 112 + pow2 120 + pow2 128 + pow2 136)*reg[30]) }
(* add in m *) (* add in m *)
adc r14 r6; adc r14 r6;
adc r15 r7; adc r15 r7;
...@@ -879,6 +885,11 @@ end; ...@@ -879,6 +885,11 @@ end;
adc r3 r30; adc r3 r30;
adc r4 r30; adc r4 r30;
adc r5 r30; adc r5 r30;
S.modify_r14(); 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_r23(); S.modify_r24(); S.modify_r25();
S.modify_r0(); S.modify_r1(); S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5()
end;
(* restore rZ register *) (* restore rZ register *)
pop r31; pop r31;
...@@ -888,11 +899,25 @@ assert { 0 <= at( (at(uint 6 mem (uint 2 reg rY))'S + pow2 48*uint 6 reg 8) )'L1 ...@@ -888,11 +899,25 @@ 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) )'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 { 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:obvious" 0 <= uint 12 reg 14 by 0 <= uint 6 reg 14 /\ 0 <= uint 6 reg 20 }; assert { 0 <= uint 12 reg 14
by 0 <= uint 6 reg 14 /\ 0 <= uint 6 reg 20 by (0 <= uint 3 reg 20 /\ 0 <= uint 3 reg 23) };
assert { 0 <= uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6 reg 0 < pow2 192 };
assert { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6 reg 0 + ?cf*pow2 192 assert { at( (at(uint 6 mem (uint 2 reg rX))'S + pow2 48*uint 6 reg 14) )'L11 =
at( uint 12 mem (uint 2 reg rX) )'S
};
assert { at( (at(uint 6 mem (uint 2 reg rY))'S + pow2 48*uint 6 reg 8) )'L11 =
at( uint 12 mem (uint 2 reg rY))'S
};
(*
check { 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 = 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
}; };
check { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6 reg 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
};
*)
std rZ 6 r14; std rZ 6 r14;
std rZ 7 r15; std rZ 7 r15;
...@@ -912,6 +937,7 @@ assert { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6 ...@@ -912,6 +937,7 @@ assert { uint 6 mem (uint 2 reg rZ) + pow2 48*uint 12 reg 14 + pow2 144*uint 6
std rZ 21 r3; std rZ 21 r3;
std rZ 22 r4; std rZ 22 r4;
std rZ 23 r5; std rZ 23 r5;
() ()
end end
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