Commit 7d81c154 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

work

parent a476a7d9
......@@ -37,6 +37,7 @@ lemma pow2_224: pow2 224 = 0x100000000000000000000000000000000000000000000000000
lemma pow2_232: pow2 232 = 0x10000000000000000000000000000000000000000000000000000000000
lemma pow2_240: pow2 240 = 0x1000000000000000000000000000000000000000000000000000000000000
lemma pow2_248: pow2 248 = 0x100000000000000000000000000000000000000000000000000000000000000
lemma pow2_256: pow2 256 = 0x10000000000000000000000000000000000000000000000000000000000000000
end
......@@ -89,7 +90,7 @@ let karatsuba128_marked()
=
'S:
S.init();
abstract (* BLOCK1 *)
abstract (* BLOCK1: karatsuba64 *)
ensures { S.synchronized S.shadow reg }
ensures { uint 8 mem (at (uint 2 reg rZ)'S) + pow2 64*uint 4 reg 22 + pow2 96*uint 1 reg 18 + pow2 104*uint 1 reg 21 + pow2 112*uint 2 reg 19
= at( uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY) ) 'S }
......@@ -419,14 +420,10 @@ end;
ldd r6 rZ 0;
ldd r7 rZ 1;
(* TODO LOCALIZE *)
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 2 reg 6 + pow2 16*uint 6 reg 12 + ?cf*pow2 64 = old(uint 2 reg 6 + pow2 16*uint 6 reg 12 + uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) }
(*
ensures { old (uint 2 reg 6 + pow2 16*uint 2 reg 12) + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 96 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01) }
*)
'B:
(* add l4 h0 to l0 and h4 *)
add r6 r14;
......@@ -437,31 +434,15 @@ ensures { old (uint 2 reg 6 + pow2 16*uint 2 reg 12) + pow2 32*uint 2 reg 6 + po
adc r15 r11;
adc r16 r19;
adc r17 r20;
(*
check { "expl:template"
at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 96
= at(
(pow2 32+1)*(uint 2 reg 6 + pow2 16*uint 2 reg 12 + pow2 32*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19))
) 'B };
check { "expl:template"
at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 96
= (pow2 32+1)*(at(uint 2 reg 6)'B + pow2 16*at(uint 6 reg 12)'L01 + pow2 32*at((uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
};
*)
S.modify_r6(); S.modify_r7();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
(* store carrrY in r21 *)
(* TODO LOCALIZE *)
S.init();
abstract
ensures { S.synchronized S.shadow reg }
(*
ensures { uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01 }
*)
ensures { uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2) }
ensures { let cor = reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
(* process sign bit *)
......@@ -485,11 +466,9 @@ assert { reg[8] = 0xFF*(1 - ?tf) };
eor r2 r8;
eor r3 r8;
eor r4 r8;
check { reg[8] = 0x00 -> uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'B };
check { reg[8] = 0xFF -> uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = pow2 64 - 1 - at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'B };
add r8 r8; (* sets carry flag if r8 = 0xff *)
check { ?cf = 1 - ?tf };
S.modify_r0();
S.modify_r2(); S.modify_r3(); S.modify_r4();
S.modify_r8(); S.modify_r18();
......@@ -525,129 +504,15 @@ assert { 0 <= at((uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg r
assert { 0 <= at((uint 4 reg 6 + pow2 32*uint 4 reg 22))'L01 <= pow2 64-1 };
assert { 0 <= at((uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22))'L01 <= (pow2 64-1)*(pow2 64-1) };
(*
check { at(uint 4 mem (uint 2 reg rZ))'L01tmp + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 + ?cf*pow2 128
= at(uint 4 mem (uint 2 reg rZ))'L01tmp + pow2 32*at(?cf + uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19 +
uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 + pow2 64*(reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0]))'Barf
= at(uint 4 mem (uint 2 reg rZ))'L01tmp + pow2 32*at(?cf + uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19 +
?cf*(pow2 64 - 1) - at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01
+ pow2 64*(reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0]))'Barf
= at(uint 4 mem (uint 2 reg rZ))'L01tmp + pow2 32*at(?cf + uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19 +
?cf*(pow2 64 - 1) - at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01
+ pow2 64*((if at ?cf 'Burp < ?cf then pow2 32 else 0) + at ?cf 'Burp - ?cf))'Barf
= at(uint 4 mem (uint 2 reg rZ))'L01tmp +
pow2 32*at(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19)'Barf +
- pow2 32*at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01
+ pow2 96*at((if at ?cf 'Burp < ?cf then pow2 32 else 0) + at ?cf 'Burp)'Barf
= at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'Crap +
pow2 32*at(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19)'Barf +
- pow2 32*at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01
+ pow2 96*at((if at ?cf 'Burp < ?cf then pow2 32 else 0) + at ?cf 'Burp)'Barf
= (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
- pow2 32*at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01
+ at(if at ?cf 'Burp < ?cf then pow2 128 else 0)'Barf
= at (
(pow2 32+1)*(uint 4 reg 2*uint 4 reg 6 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)
- pow2 32*(uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22)
)'L01
+ at(if at ?cf 'Burp < ?cf then pow2 128 else 0)'Barf
= at (
let al = uint 4 reg 2 in
let bl = uint 4 reg 6 in
let ah = uint 3 reg 18+pow2 24*mem[uint 2 reg rX] in
let bh = uint 4 reg 22 in
(pow2 32+1)*(al*bl + pow2 32*ah*bh) - pow2 32*(al - ah)*(bl - bh)
)'L01
+ at(if at ?cf 'Burp < ?cf then pow2 128 else 0)'Barf
= at (
let al = uint 4 reg 2 in
let bl = uint 4 reg 6 in
let ah = uint 3 reg 18+pow2 24*mem[uint 2 reg rX] in
let bh = uint 4 reg 22 in
al*bl + pow2 64*ah*bh + pow2 32*ah*bl + pow2 32*al*bh
)'L01
+ at(if at ?cf 'Burp < ?cf then pow2 128 else 0)'Barf
= at (
let al = uint 4 reg 2 in
let bl = uint 4 reg 6 in
let ah = uint 3 reg 18+pow2 24*mem[uint 2 reg rX] in
let bh = uint 4 reg 22 in
(al+pow2 32*ah)*(bl+pow2 32*bh)
)'L01
+ at(if at ?cf 'Burp < ?cf then pow2 128 else 0)'Barf
};
check { uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 + ?cf*pow2 128
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
+ if at ?cf 'Burp < at ?cf 'Barf then pow2 128 else 0
};
*)
abstract ensures { 0 <= uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 < pow2 128 }
assert { 0 <= uint 4 mem (at (uint 2 reg rZ)'S) };
assert { 0 <= uint 6 reg 12 };
end;
assert { "expl:hack" 0 <= uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 < pow2 128
by 0 <= uint 4 mem (at (uint 2 reg rZ)'S)
(*
/\
0 <= pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
*)};
(* FNORD*)
check { uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 + ?cf*pow2 128
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
\/
uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 + ?cf*pow2 128
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + pow2 128
};
check { ?cf = 0 ->
uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
\/
uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + pow2 128
};
check { ?cf = 0 ->
uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + pow2 128
->
false
};
check { ?cf = 0 ->
uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + pow2 128
->
0 <= uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 < pow2 128
&&
pow2 128 <= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + pow2 128
&& false
};
check { ?cf = 1 -> uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 + pow2 128
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + pow2 128
};
check { uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19 + ?cf*pow2 128
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01 + ?cf*pow2 128
};
(* FNORD*)
check { uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 2 reg 6 + pow2 48*uint 6 reg 12 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
};
check { uint 2 reg rZ = at(uint 2 reg rZ)'S };
std rZ 4 r6;
std rZ 5 r7;
std rZ 6 r12;
std rZ 7 r13;
check { mem[uint 2 reg rZ+4] = reg[6] };
check { mem[uint 2 reg rZ+5] = reg[7] };
check { mem[uint 2 reg rZ+6] = reg[12] };
check { mem[uint 2 reg rZ+7] = reg[13] };
check { uint 4 mem (uint 2 reg rZ+4) = uint 2 reg 6 + pow2 16*uint 2 reg 12 };
check { uint 4 mem (at (uint 2 reg rZ)'S+4) = uint 2 reg 6 + pow2 16*uint 2 reg 12 };
check { uint 4 mem (at (uint 2 reg rZ)'S) + pow2 32*uint 4 mem (at (uint 2 reg rZ)'S+4) + pow2 64*uint 4 reg 14 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
};
check { uint 8 mem (at (uint 2 reg rZ)'S) + pow2 64*uint 4 reg 14 + pow2 96*uint 2 reg 10 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
};
movw r22 r14;
movw r24 r16;
......@@ -655,9 +520,6 @@ check { uint 8 mem (at (uint 2 reg rZ)'S) + pow2 64*uint 4 reg 14 + pow2 96*ui
mov r21 r11;
(* h8...h15 stored in 22 23 24 25 18 21 19 20 *)
check { uint 8 mem (at (uint 2 reg rZ)'S) + pow2 64*uint 4 reg 22 + pow2 96*uint 1 reg 18 + pow2 104*uint 1 reg 21 + pow2 112*uint 2 reg 19
= at( (uint 4 reg 2 + pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )'L01
};
S.modify_r18(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
end; (* BLOCK1 *)
......@@ -669,6 +531,19 @@ end; (* BLOCK1 *)
movw r14 r12;
movw r16 r12;
assert { "expl:memory" eq 8 mem (at mem 'S) (at (uint 2 reg rX+8)'S) };
assert { "expl:memory" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) };
abstract (* BLOCK2: karatsuba64 *)
ensures { S.synchronized S.shadow reg }
ensures { uint 16 mem (at (uint 2 reg rZ)'S+16)
= old(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)
+ at( uint 8 mem (uint 2 reg rX+8) * uint 8 mem (uint 2 reg rY+8) ) 'S }
ensures { forall i. mem[i] <> (old mem)[i] -> uint 2 reg rZ+16 <= i < uint 2 reg rZ+32 }
ensures { uint 2 reg rX = old(uint 2 reg rX)+8 }
ensures { uint 2 reg rY = old(uint 2 reg rY) }
ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
'B:
(* level 2: compute l *)
ld_inc r2 rX;
ld_inc r3 rX;
......@@ -678,8 +553,6 @@ end; (* BLOCK1 *)
ldd r7 rY 9;
ldd r8 rY 10;
ldd r9 rY 11;
assert { "expl:temp" eq 8 mem (at mem 'S) (at (uint 2 reg rX+8)'S) };
assert { "expl:temp" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) };
'L00:
S.init();
......@@ -691,6 +564,8 @@ ensures { reg[20] = 0 /\ reg[21] = 0 }
ensures { forall i. mem[i] <> (old mem)[i] -> uint 2 reg rZ+16 <= i < uint 2 reg rZ+22 }
ensures { !stack_pointer = old(!stack_pointer-1) }
ensures { stack[old !stack_pointer] = 0x00 \/ stack[old !stack_pointer] = 0xFF }
(* TODO: preservation of the stack *)
'B:
mul r2 r6;
......@@ -699,53 +574,44 @@ ensures { !stack_pointer = old(!stack_pointer-1) }
mul r2 r7;
add r11 r0;
adc r12 r1;
check { uint 3 reg 10 = at(uint 1 reg 2*uint 2 reg 6)'B };
mul r3 r6;
add r11 r0;
adc r12 r1;
adc r13 r17;
check { uint 4 reg 10 = at(uint 1 reg 2*uint 2 reg 6 + pow2 8*uint 1 reg 3*uint 1 reg 6)'B };
mul r2 r8;
add r12 r0;
adc r13 r1;
adc r14 r17;
check { uint 5 reg 10 = at(uint 1 reg 2*uint 3 reg 6 + pow2 8*uint 1 reg 3*uint 1 reg 6)'B };
mul r3 r7;
add r12 r0;
adc r13 r1;
adc r14 r17;
check { uint 5 reg 10 = at(uint 1 reg 2*uint 3 reg 6 + pow2 8*uint 1 reg 3*uint 2 reg 6)'B };
mul r4 r6;
add r12 r0;
adc r13 r1;
adc r14 r17;
check { uint 5 reg 10 = at(uint 1 reg 2*uint 3 reg 6 + pow2 8*uint 1 reg 3*uint 2 reg 6 + pow2 16*uint 1 reg 4*uint 1 reg 6)'B };
mul r2 r9;
add r13 r0;
adc r14 r1;
adc r15 r17;
check { uint 6 reg 10 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 2 reg 6 + pow2 16*uint 1 reg 4*uint 1 reg 6)'B };
mul r3 r8;
add r13 r0;
adc r14 r1;
adc r15 r17;
check { uint 6 reg 10 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 3 reg 6 + pow2 16*uint 1 reg 4*uint 1 reg 6)'B };
mul r4 r7;
add r13 r0;
adc r14 r1;
adc r15 r17;
check { uint 6 reg 10 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 3 reg 6 + pow2 16*uint 1 reg 4*uint 2 reg 6)'B };
mul r5 r6;
add r13 r0;
adc r14 r1;
adc r15 r17;
check { uint 6 reg 10 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 3 reg 6 + pow2 16*uint 1 reg 4*uint 2 reg 6 + pow2 24*uint 1 reg 5*uint 1 reg 6)'B };
'B2:
(* now add h0 l8 and h0 l12 *)
(* TODO: move stores away from here *)
(* COMMENT: these stores are annoying for the formal specification *)
add r22 r10;
std rZ 16 r22;
adc r23 r11;
......@@ -761,12 +627,9 @@ check { uint 6 reg 10 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint
adc r12 r19;
adc r13 r20;
check { uint 4 reg 22 + pow2 32*uint 4 reg 10 + ?cf*pow2 64 = at(uint 4 reg 22 + pow2 32*uint 4 reg 10 + uint 4 reg 10 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B2 };
(* store carrrY on stack *)
'B3:
sbc r0 r0;
check { reg[0] = 0x00 \/ reg[0] = 0xFF };
check { reg[0] = 0xFF * ?cf };
push r0;
clr r20;
clr r21;
......@@ -776,42 +639,30 @@ check { reg[0] = 0xFF * ?cf };
add r14 r0;
adc r15 r1;
adc r16 r21;
check { at(uint 4 reg 10)'B2 + pow2 32*uint 3 reg 14 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 4 reg 6 + pow2 16*uint 1 reg 4*uint 2 reg 6 + pow2 24*uint 1 reg 5*uint 1 reg 6)'B };
mul r4 r8;
add r14 r0;
adc r15 r1;
adc r16 r21;
check { at(uint 4 reg 10)'B2 + pow2 32*uint 3 reg 14 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 4 reg 6 + pow2 16*uint 1 reg 4*uint 3 reg 6 + pow2 24*uint 1 reg 5*uint 1 reg 6)'B };
mul r5 r7;
add r14 r0;
adc r15 r1;
adc r16 r21;
check { at(uint 4 reg 10)'B2 + pow2 32*uint 3 reg 14 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 4 reg 6 + pow2 16*uint 1 reg 4*uint 3 reg 6 + pow2 24*uint 1 reg 5*uint 2 reg 6)'B };
mul r4 r9;
add r15 r0;
adc r16 r1;
adc r17 r21;
check { at(uint 4 reg 10)'B2 + pow2 32*uint 4 reg 14 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 4 reg 6 + pow2 16*uint 1 reg 4*uint 4 reg 6 + pow2 24*uint 1 reg 5*uint 2 reg 6)'B };
mul r5 r8;
add r15 r0;
adc r16 r1;
adc r17 r21;
check { at(uint 4 reg 10)'B2 + pow2 32*uint 4 reg 14 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 4 reg 6 + pow2 16*uint 1 reg 4*uint 4 reg 6 + pow2 24*uint 1 reg 5*uint 3 reg 6)'B };
mul r5 r9;
add r16 r0;
adc r17 r1;
check { at(uint 4 reg 10)'B2 + pow2 32*uint 4 reg 14 = at(uint 1 reg 2*uint 4 reg 6 + pow2 8*uint 1 reg 3*uint 4 reg 6 + pow2 16*uint 1 reg 4*uint 4 reg 6 + pow2 24*uint 1 reg 5*uint 4 reg 6)'B };
assert { at(uint 4 reg 10)'B2 + pow2 32*uint 4 reg 14 = at(uint 4 reg 2*uint 4 reg 6)'B };
check { uint 4 reg 22 + pow2 32*uint 4 reg 10 + pow2 64*at ?cf 'B3 = at((pow2 32+1)*uint 4 reg 10)'B2 + at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B2 };
check { uint 4 reg 22 + pow2 32*uint 4 reg 10 + pow2 64*at ?cf 'B3 + (pow2 32+1)*pow2 32*uint 4 reg 14 = (pow2 32+1)*at(uint 4 reg 2*uint 4 reg 6)'B + at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B2 };
check { uint 4 reg 22 + pow2 32*uint 8 reg 10 + pow2 64*at ?cf 'B3 + pow2 32*uint 4 reg 14 = (pow2 32+1)*at(uint 4 reg 2*uint 4 reg 6)'B + at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B2 };
check { uint 6 mem (uint 2 reg rZ+16) + pow2 48*uint 6 reg 12 + pow2 64*at ?cf 'B3 + pow2 32*uint 4 reg 14 = (pow2 32+1)*at(uint 4 reg 2*uint 4 reg 6)'B + at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B2 };
check { uint 6 mem (uint 2 reg rZ+16) + pow2 48*uint 6 reg 12 + pow2 64*at ?cf 'B3 + pow2 32*uint 4 reg 14 = (pow2 32+1)*at(uint 4 reg 2*uint 4 reg 6)'B + at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B };
check { at ?cf 'B3 = as_bool stack[at (!stack_pointer) 'B] };
S.modify_r0(); S.modify_r1();
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13();
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
......@@ -819,7 +670,26 @@ check { at ?cf 'B3 = as_bool stack[at (!stack_pointer) 'B] };
S.modify_r20(); S.modify_r21();
end;
'Q:
assert { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : {Z+20}[2] : 12[6]
: 14[4] : {!pop!} = X0*Y0 + ww(w+1)(X1l*Y1l)
*)
let x = at (uint 2 reg rX)'S in
let y = at (uint 2 reg rY)'S in
let z = at (uint 2 reg rZ)'S in
uint 8 mem z + pow2 64*uint 6 mem (z+16) + pow2 112*uint 6 reg 12 + pow2 96*uint 4 reg 14 + pow2 128*as_bool stack[!stack_pointer+1]
= pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
uint 8 (at mem 'S) x * uint 8 (at mem 'S) y
by
pow2 64*uint 6 mem (z+16) + pow2 112*uint 6 reg 12 + pow2 96*uint 4 reg 14 + pow2 128*as_bool stack[!stack_pointer+1]
= (pow2 64)*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 64*at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'L00
};
(* load a4..a7 and b4..b7 *)
movw r10 r20;
ld_inc r18 rX;
......@@ -831,12 +701,14 @@ end;
ldd r24 rY 14;
ldd r25 rY 15;
(* TODO: optimize this *)
(*
abstract
ensures { uint 3 reg 18 + pow2 24*mem[uint 2 reg rX] = at (uint 4 mem (uint 2 reg rX+12))'S }
ensures { uint 4 reg 22 = at (uint 4 mem (uint 2 reg rY+12))'S }
assert { "expl:temp" eq 8 mem (at mem 'S) (at (uint 2 reg rX+8)'S) };
assert { "expl:temp" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) };
end;
*)
'L01:
S.init();
......@@ -962,12 +834,36 @@ ensures { uint 2 reg rX = old(uint 2 reg rX)+1 }
add r19 r0;
adc r20 r1;
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();
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20();
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();
S.modify_r10(); S.modify_r11();
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17(); S.modify_r18(); S.modify_r19(); S.modify_r20();
S.modify_r26(); S.modify_r27();
end;
check { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : {Z+20}[2] : 12[6]
: 14[4] : 10[2] : 19[2] = X0*Y0 + ww(w+1)(X1l*Y1l) + wwwX1h*Y1h
: {!pop!}
*)
let x = at (uint 2 reg rX)'S in
let y = at (uint 2 reg rY)'S in
let z = at (uint 2 reg rZ)'S in
uint 8 mem z + pow2 64*uint 6 mem (z+16) + pow2 112*uint 6 reg 12 + pow2 96*uint 4 reg 14 + pow2 128*as_bool stack[!stack_pointer+1]
+ pow2 128*uint 2 reg 10 + pow2 144*uint 2 reg 19
= pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 96*uint 8 (at mem 'S) (x+12)*uint 8 (at mem 'S) (y+12)
by
at(uint 3 reg 18+pow2 24*mem[uint 2 reg rX])'L01 = uint 4 (at mem 'S) (x+12) /\
at(uint 4 reg 22)'L01 = uint 4 (at mem 'S) (y+12)
by uint 2 reg rY = at (uint 2 reg rY)'S
};
S.init();
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = old (uint 4 reg 2*uint 4 reg 6) }
......@@ -1057,7 +953,7 @@ end;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { old (uint 2 reg 6 + pow2 16*uint 2 reg 12) + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 96 = (pow2 32+1)*(at(uint 4 reg 2*uint 4 reg 6)'L00 + at(pow2 32*(uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01) }
ensures { uint 2 reg 6 + pow2 16*uint 6 reg 12 + ?cf*pow2 64 = old(uint 2 reg 6 + pow2 16*uint 6 reg 12 + uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) }
'B:
(* add l4 h0 to l0 and h4 *)
add r6 r14;
......@@ -1068,47 +964,26 @@ ensures { old (uint 2 reg 6 + pow2 16*uint 2 reg 12) + pow2 32*uint 2 reg 6 + po
adc r15 r11;
adc r16 r19;
adc r17 r20;
assert { uint 2 reg 6 + pow2 16*uint 6 reg 12 + ?cf*pow2 64
= at(uint 2 reg 6 + pow2 16*uint 6 reg 12 + uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) 'B };
check { "expl:template"
at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 96
= at(
(pow2 32+1)*(uint 2 reg 6 + pow2 16*uint 2 reg 12 + pow2 32*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19))
) 'B };
check { "expl:template"
at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 96
= (pow2 32+1)*(at(uint 2 reg 6)'B + pow2 16*at(uint 6 reg 12)'L01 + pow2 32*at((uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
};
S.modify_r6(); S.modify_r7();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
abstract
ensures { S.synchronized S.shadow reg }
ensures { reg[21] = old ?cf }
ensures { uint 4 reg 14 + ?cf*pow2 32 = old (uint 4 reg 14) + as_bool stack[!stack_pointer] }
ensures { !stack_pointer = old (!stack_pointer)+1 }
ensures { reg[21] = 0 \/ ?cf = 0 }
(*
check { "expl:template"
pow2 32*at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 64*uint 2 reg 6 + pow2 80*uint 2 reg 12 + pow2 96*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 128
= (pow2 32+1)*(pow2 32*at(uint 2 reg 6)'B + pow2 48*at(uint 6 reg 12)'L01 + pow2 64*at((uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
};
check { "expl:template"
pow2 32*at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 64*uint 2 reg 6 + pow2 80*uint 2 reg 12 + pow2 96*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + ?cf*pow2 128
+ (pow2 32+1)*at(uint 4 reg 14)'L01
= (pow2 32+1)*(pow2 32*at(uint 2 reg 6)'B + pow2 48*at(uint 6 reg 12)'L01 + pow2 64*at((uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
};
ensures { uint 6 mem (uint 2 reg rZ+16) + pow2 48*uint 6 reg 12 + pow2 32*uint 4 reg 14 + pow2 64*as_bool stack[old !stack_pointer] = (pow2 32+1)*old(uint 4 reg 2*uint 4 reg 6) + old(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19) }
*)
(* store carrrY in r21 *)
'B:
adc r21 r21;
assert { "expl:template"
at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 32*uint 2 reg 6 + pow2 48*uint 2 reg 12 + pow2 64*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + reg[21]*pow2 96
= (pow2 32+1)*(at(uint 2 reg 6)'B + pow2 16*at(uint 6 reg 12)'L01 + pow2 32*at((uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
};
(* propagate carry *)
'XXX:
pop r0;
assert { reg[0] = (at stack 'XXX)[!stack_pointer] };
assert { reg[0] = 0x00 \/ reg[0] = 0xFF };
neg r0;
assert { reg[0] = as_bool stack[!stack_pointer] };
add r14 r0;
......@@ -1117,30 +992,31 @@ assert { reg[0] = as_bool stack[!stack_pointer] };
adc r16 r0;
adc r17 r0;
check { "expl:template"
pow2 32*at(uint 2 reg 6 + pow2 16*uint 2 reg 12)'B + pow2 64*uint 2 reg 6 + pow2 80*uint 2 reg 12 + pow2 96*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19) + reg[21]*pow2 128 + ?cf*pow2 128
+ (pow2 32+1)*at(uint 4 mem (uint 2 reg rZ+16) + pow2 32*uint 4 reg 14)'L01
= pow2 32*(pow2 32+1)*((pow2 32+1)*at(uint 4 reg 2*uint 4 reg 6)'L00 + at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'L00 +
pow2 32*at((uint 3 reg 18+pow2 24*mem[uint 2 reg rX])*uint 4 reg 22)'L01)
};
(*
ensures { uint 6 mem (uint 2 reg rZ+16) + pow2 48*uint 6 reg 12 + pow2 32*uint 4 reg 14 + pow2 64*as_bool stack[old !stack_pointer] = (pow2 32+1)*old(uint 4 reg 2*uint 4 reg 6) + old(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19) }
*)
S.modify_r6(); S.modify_r7();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
S.modify_r21();
S.modify_r0();
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
(*
{Z}[8] : {Z+16}[4] : 6[2] : 12[2] : 14[4] : 21 + ?cf = X0*Y0 + ww(w+1)(X1l*Y1l) + wwwX1h*Y1h
*)
check { uint 8 mem (at (uint 2 reg rZ)'S) + pow2 64*uint 4 mem (at (uint 2 reg rZ)'S)
+ pow2 96*uint 2 reg 6 + pow2 112*uint 2 reg 12 + pow2 128*uint 4 reg 14 + pow2 160*(reg[21] + ?cf)
=
at( uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY) +
pow2 64*(pow2 64+1)* uint 4 mem (uint 2 reg rX+8) * uint 4 mem (uint 2 reg rY+8) +
pow2 96*uint 4 mem (uint 2 reg rX+12)*uint 4 mem (uint 2 reg rX+12)
)'S
};
(* store carrrY in r21 *)
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = ?cf*(pow2 64 - 1) - at((uint 4 reg 2 - (uint 3 reg 18+pow2 24*mem[uint 2 reg rX]))*(uint 4 reg 6 - uint 4 reg 22))'L01 }
ensures { let cor = reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
ensures { uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2) }
ensures { let cor = reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old reg[21] + old ?cf - ?cf \/ cor = pow2 32 + old reg[21] + old ?cf - ?cf }
(* process sign bit *)
clr r8;
......@@ -1152,7 +1028,6 @@ assert { reg[8] = 0xFF*(1 - ?tf) };
adc r21 r8;
mov r0 r21;
asr r0;
'B:
(* invert all bits or do nothing *)
eor r22 r8;
......@@ -1163,16 +1038,22 @@ assert { reg[8] = 0xFF*(1 - ?tf) };
eor r2 r8;
eor r3 r8;
eor r4 r8;
assert { reg[8] = 0x00 -> uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'B };
assert { reg[8] = 0xFF -> uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = pow2 64 - 1 - at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'B };
check { reg[8] = 0x00 -> uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'B };
check { reg[8] = 0xFF -> uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 = pow2 64 - 1 - at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'B };
add r8 r8; (* sets carry flag if r8 = 0xff *)
assert { ?cf = 1 - ?tf };
check { ?cf = 1 - ?tf };
S.modify_r0();
S.modify_r2(); S.modify_r3(); S.modify_r4();
S.modify_r8(); S.modify_r18();
S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
end;
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19 + ?cf*pow2 96 =
old(?cf + uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19
+ uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2
+ pow2 64*(uint 1 reg 21 + (pow2 8+pow2 16+pow2 24)*reg[0])) }
(* add in m *)
adc r6 r22;
adc r7 r23;
......@@ -1189,6 +1070,40 @@ end;
adc r19 r0;
adc r20 r0;
S.modify_r6(); S.modify_r7();
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
S.modify_r10(); S.modify_r11(); S.modify_r19(); S.modify_r20();
end;
abstract ensures { 0 <= uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19 < pow2 96 }
()
end;
abstract ensures { 0 <= at(uint 8 mem (uint 2 reg rX+8)*uint 8 mem (uint 2 reg rY+8))'S <= (pow2 64-1)*(pow2 64-1) }
assert { 0 <= at(uint 8 mem (uint 2 reg rX+8))'S <= (pow2 64-1) };
assert { 0 <= at(uint 8 mem (uint 2 reg rY+8))'S <= (pow2 64-1) };
end;
(* TODO *)
assert { "expl:doesthishelp"
(pow2 64-1)*(pow2 64-1) < (pow2 64-1)*pow2 64
};
assert { "expl:doesthishelp"
0 <= at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B < pow2 64-1
by at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B <= pow2 64-2
by pow2 64*at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B <= (pow2 64-1)*(pow2 64-1) = pow2 128 - 2*pow2 64 + 1
by at(uint 8 mem (uint 2 reg rZ))'B + pow2 64*at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B <= (pow2 64-1)*(pow2 64-1)
/\ 0 <= at(uint 8 mem (uint 2 reg rZ))'B < pow2 64
by 0 <= at(uint 8 mem (uint 2 reg rX)*uint 8 mem (uint 2 reg rY))'S <= (pow2 64-1)*(pow2 64-1)
/\ at(uint 8 mem (uint 2 reg rZ))'B + pow2 64*at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B =
at(uint 8 mem (uint 2 reg rX)*uint 8 mem (uint 2 reg rY))'S
by 0 <= at(uint 8 mem (uint 2 reg rX))'S <= (pow2 64-1) /\
0 <= at(uint 8 mem (uint 2 reg rY))'S <= (pow2 64-1) /\
at (uint 2 reg rZ)'B = at(uint 2 reg rZ)'S
};
assert { "expl:doesthishelp" (pow2 64-1)*(pow2 64-1) + pow2 64-1 < pow2 128 };
assert { "expl:doesthishelp" 0 <= at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 1 reg 21 + pow2 48*uint 2 reg 19)'B + at(uint 8 mem (uint 2 reg rX+8)*uint 8 mem (uint 2 reg rY+8))'S < pow2 128 };
std rZ 20 r6;
std rZ 21 r7;
std rZ 22 r12;
......@@ -1202,6 +1117,8 @@ end;
std rZ 30 r19;
std rZ 31 r20;
end; (* BLOCK2 *)
(* level 1: subtract a0 a7 *)
sbiw r26 16;
ld_inc r2 rX;
......@@ -1219,7 +1136,7 @@ end;
ld_inc r14 rX;
ld_inc r15 rX;
ld_inc r16 rX;
(* original
(* TODO original
ld r17 rX ;
*)
ld_inc r17 rX;
......
......@@ -3,12 +3,13 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="30" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="1" memlimit="1000"/>
<file name="../avr_code5.mlw" expanded="true">
<theory name="BV_asr_Lemmas" sum="16edde4d72a282519bf221e18c8b7013">
<prover id="6" name="Eprover" version="2.0" timelimit="60" steplimit="0" memlimit="1000"/>
<file name="../karatsuba128.mlw" expanded="true">
<theory name="B