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

rough formalized version of karatsuba128 (with intermediate checks)

parent 9c944eea
......@@ -459,9 +459,7 @@ let asr (dst: register): unit
let lsr (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsr (BV8.of_int reg[dst]) 1)] }
(*
ensures { ?cf = mod (old reg[dst]) 2 }
*)
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.lsr (BV8.of_int (Map.get reg.data dst)) 1))
......
(* TODO checks and tussenstand: remove *)
module BV_asr_Lemmas
use import bv.BV8
......@@ -41,6 +42,16 @@ lemma pow2_256: pow2 256 = 0x100000000000000000000000000000000000000000000000000
end
module BV_lsr_Lemmas
use import bv.BV8
use import int.Int
lemma lsr_0: eq (lsr zeros 1) zeros
lemma lsr_1: eq (lsr (of_int 1) 1) zeros
end
module AvrModelLemmas
use import int.Int
......@@ -77,25 +88,28 @@ use avrmodel3.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
(* TODO: see if this helps the 'assert 0xFF' *)
lemma bit_blit: forall b. BV8.t'int (bitset (BV8.of_int 0) 0 b) = (if b then 1 else 0)
function as_bool (x: int): int = if x = 0 then 0 else 1
let karatsuba128_marked()
requires { 32 <= uint 2 reg rX < pow2 15 }
requires { 32 <= uint 2 reg rY < pow2 15 }
requires { 32 <= uint 2 reg rZ < pow2 15 }
(* can we tighten this? *)
requires { uint 2 reg rZ+32 <= uint 2 reg rX \/ uint 2 reg rZ >= uint 2 reg rX+16 }
requires { uint 2 reg rZ+32 <= uint 2 reg rY \/ uint 2 reg rZ >= uint 2 reg rY+16 }
ensures { uint 32 mem (old (uint 2 reg rZ)) = old (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY)) }
=
'S:
S.init();
abstract (* BLOCK1: karatsuba64 *)
abstract (* BLOCK1: karatsuba64 on lower half *)
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 }
ensures { forall i. mem[i] <> (old mem)[i] -> uint 2 reg rZ+0 <= i < uint 2 reg rZ+8 }
ensures { uint 2 reg rX = old(uint 2 reg rX)+8 }
(* TODO remove this? *)
ensures { uint 2 reg rY = old(uint 2 reg rY) }
ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
......@@ -531,12 +545,15 @@ end; (* BLOCK1 *)
movw r14 r12;
movw r16 r12;
(*TODO: is this necessary ? *)
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 *)
'PreBlock2:
abstract (* BLOCK2: karatsuba64 on upper half + add to lower half in prep for (w+1)(Xl*Yl + w*Xh*Yh) *)
ensures { S.synchronized S.shadow reg }
ensures { uint 2 reg rX = old(uint 2 reg rX)+8 }
(* TODO: remove this? *)
ensures { uint 2 reg rY = old(uint 2 reg rY) }
ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
ensures { uint 16 mem (at (uint 2 reg rZ)'S+16)
......@@ -1077,6 +1094,7 @@ check { "expl:tussenstand"
S.init();
abstract
ensures { S.synchronized S.shadow reg }
(* TODO: which one is best? *)
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 }
......@@ -1273,15 +1291,13 @@ assert { "expl:tussenstand"
};
assert {
assume {
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
0 <= uint 8 mem z + pow2 64*uint 4 mem (z+16) + pow2 96*uint 2 reg 6 + pow2 112*uint 2 reg 12 + pow2 128*uint 4 reg 14 + pow2 160*uint 2 reg 10 + pow2 176*uint 2 reg 19 < pow2 192
by
(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)
};
assert {
assume {
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
......@@ -1370,9 +1386,28 @@ assert {
end; (* BLOCK2 *)
abstract
'AD:
assert { "expl:memory" eq 16 mem (at mem 'S) (at (uint 2 reg rX)'S) };
assert { "expl:memory" eq 16 mem (at mem 'S) (at (uint 2 reg rY)'S) };
abstract (* BLOCK3.1: compute absolute values *)
ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 2 + pow2 32*uint 4 reg 18 = at(abs(uint 8 mem (uint 2 reg rX) - uint 8 mem (uint 2 reg rX+8)))'S }
ensures { uint 4 reg 6 + pow2 32*uint 4 reg 22 = at(abs(uint 8 mem (uint 2 reg rY) - uint 8 mem (uint 2 reg rY+8)))'S }
ensures { stack[old !stack_pointer] = 0
<-> at((uint 8 mem (uint 2 reg rX) < uint 8 mem (uint 2 reg rX+8)) <->
(uint 8 mem (uint 2 reg rY) < uint 8 mem (uint 2 reg rY+8)))'S }
ensures { !stack_pointer = old !stack_pointer-1 }
ensures { stack[old !stack_pointer] = 0x00 \/ stack[old !stack_pointer] = 0xFF }
ensures { reg[26] = reg[27] = 0 }
(* level 1: subtract a0 a7 *)
ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 2 + pow2 32*uint 4 reg 18 = at(uint 8 mem (uint 2 reg rX))'S }
ensures { uint 8 reg 10 = at(uint 8 mem (uint 2 reg rX+8))'S }
sbiw r26 16;
ld_inc r2 rX;
ld_inc r3 rX;
......@@ -1389,21 +1424,38 @@ ensures { reg[26] = reg[27] = 0 }
ld_inc r14 rX;
ld_inc r15 rX;
ld_inc r16 rX;
ld_inc r17 rX;
(* TODO original
ld r17 rX ;
*)
ld_inc r17 rX;
S.modify_r2(); S.modify_r3(); S.modify_r4(); S.modify_r5();
S.modify_r18(); S.modify_r19(); S.modify_r20(); S.modify_r21();
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
S.modify_r26(); S.modify_r27();
end;
'Q:
sub r2 r10;
check { uint 1 reg 2 = ?cf*pow2 8 + at(uint 1 reg 2 - uint 1 reg 10)'Q };
sbc r3 r11;
check { uint 2 reg 2 = ?cf*pow2 16 + at(uint 2 reg 2 - uint 2 reg 10)'Q };
sbc r4 r12;
sbc r5 r13;
check { uint 4 reg 2 = ?cf*pow2 32 + at(uint 4 reg 2 - uint 4 reg 10)'Q };
sbc r18 r14;
sbc r19 r15;
sbc r20 r16;
sbc r21 r17;
(* 0xff if carry and 0x00 if no carry *)
check { uint 4 reg 2 + pow2 32*uint 4 reg 18 = ?cf*pow2 64 + at(uint 4 reg 2 + pow2 32*uint 4 reg 18 - uint 8 reg 10)'Q };
sbc r0 r0;
check { uint 4 reg 2 + pow2 32*uint 4 reg 18 = ?cf*pow2 64 + at(uint 8 mem (uint 2 reg rX) - uint 8 mem (uint 2 reg rX+8))'S };
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 6 + pow2 32*uint 4 reg 22 = at(uint 8 mem (uint 2 reg rY))'S }
ensures { uint 8 reg 10 = at(uint 8 mem (uint 2 reg rY+8))'S }
(* level 1: subtract b0 b7 *)
ldd r6 rY 0;
ldd r7 rY 1;
......@@ -1421,6 +1473,11 @@ ensures { reg[26] = reg[27] = 0 }
ldd r15 rY 13;
ldd r16 rY 14;
ldd r17 rY 15;
S.modify_r6(); S.modify_r7(); S.modify_r8(); S.modify_r9();
S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25();
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
sub r6 r10;
sbc r7 r11;
sbc r8 r12;
......@@ -1431,6 +1488,7 @@ ensures { reg[26] = reg[27] = 0 }
sbc r25 r17;
(* 0xff if carry and 0x00 if no carry *)
sbc r1 r1;
check { uint 4 reg 6 + pow2 32*uint 4 reg 22 = ?cf*pow2 64 + at(uint 8 mem (uint 2 reg rY))'S - at(uint 8 mem (uint 2 reg rY+8))'S };
(* level 1: absolute values *)
eor r2 r0;
......@@ -1469,15 +1527,26 @@ ensures { reg[26] = reg[27] = 0 }
clr r27;
eor r0 r1;
push r0;
end;
(* this block touches almost all values *)
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_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(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25(); S.modify_r26(); S.modify_r27();
end; (* BLOCK3.1: compute absolute values *)
(* level 1: compute m *)
movw r16 r26;
abstract (* BLOCK 3.2: karatsuba64: compute product of absolute values *)
ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18 =
old((uint 4 reg 2 + pow2 32*uint 4 reg 18) * (uint 4 reg 6 + pow2 32*uint 4 reg 22)) }
ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
'S:
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 = old(uint 4 reg 2 * uint 4 reg 6) }
movw r16 r26;
mul r2 r8; (* a0*b2 *)
movw r12 r0;
mul r2 r6; (* a0*b0 *)
......@@ -1543,6 +1612,7 @@ S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14();
S.modify_r28(); S.modify_r29();
end;
S.init();
abstract 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)) }
......@@ -1587,6 +1657,9 @@ ensures { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uin
S.modify_r6(); S.modify_r7(); S.modify_r8(); S.modify_r9();
end;
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 1 reg 18 + pow2 56*uint 1 reg 25 = old (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) }
ensures { reg[19] = 0 }
(* level 2: compute h (l3 l4 l5) *)
mul r18 r24; (* a0*b2 *)
......@@ -1659,10 +1732,16 @@ end;
add r27 r0;
adc r18 r1;
adc r25 r19;
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_r25(); S.modify_r26(); S.modify_r27(); S.modify_r28(); S.modify_r29();
end;
S.init();
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9
= old (uint 4 reg 2*uint 4 reg 6) }
ensures { reg[3] = 0 }
(* level 2: compute m *)
mul r2 r8; (* a0*b2 *)
movw r22 r0;
......@@ -1729,8 +1808,14 @@ ensures { uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56
add r2 r0;
adc r19 r1;
adc r9 r3;
S.modify_r0(); S.modify_r1(); S.modify_r2(); S.modify_r3();
S.modify_r9(); S.modify_r28(); S.modify_r29();
S.modify_r19(); S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24();
end;
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 2 reg 4 + pow2 16*uint 2 reg 6 + pow2 32*uint 8 reg 10 + ?cf*pow2 96 = old(uint 4 reg 10) + pow2 32*old(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 1 reg 18 + pow2 56*uint 1 reg 25) }
(* add l4 h0 to l0 and h4 *)
movw r4 r10;
movw r6 r12;
......@@ -1743,15 +1828,25 @@ end;
adc r16 r18;
adc r17 r25;
(* store carrrY in r3 *)
S.modify_r4(); S.modify_r5(); S.modify_r6(); S.modify_r7();
S.modify_r10(); S.modify_r11(); 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 { uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9) }
(* TODO: which one is best *)
(*
ensures { let cor = reg[3] + (pow2 8+pow2 16+pow2 24)*reg[1] in cor = old ?cf - ?cf + (if ?cf > old ?cf then pow2 32 else 0) }
*)
ensures { let cor = reg[3] + (pow2 8+pow2 16+pow2 24)*reg[1] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
(* process sign bit *)
'B:
clr r0;
bld r0 0;
(* TODO optimize me *)
assert { reg[0] = ?tf };
dec r0;
assert { reg[0] = 0xFF*(1 - ?tf) };
......@@ -1769,7 +1864,10 @@ assert { reg[0] = 0xFF*(1 - ?tf) };
eor r2 r0;
eor r19 r0;
eor r9 r0;
assert { reg[0] = 0x00 -> uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9 = at(uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9)'B };
assert { reg[0] = 0xFF -> uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9 = pow2 64 - 1 - at(uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9)'B };
add r0 r0; (* sets carry flag if r0 = 0xff *)
assert { ?cf = 1 - ?tf };
S.modify_r0(); S.modify_r1();
S.modify_r2(); S.modify_r3();
S.modify_r19(); S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24();
......@@ -1802,6 +1900,22 @@ S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14();
S.modify_r26(); S.modify_r27(); S.modify_r18(); S.modify_r25(); S.modify_r19();
end;
(* this is now necessary, probably due to the context overload;
just hang in there, smt solvers! the proof is almost done. you can do this! *)
assert { uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + 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))'S \/
uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + 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))'S + pow2 128 };
assert { 0 <= uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18 < pow2 128 };
abstract ensures { 0 <= at(uint 4 reg 2 + pow2 32*uint 4 reg 18)'S * at(uint 4 reg 6 + pow2 32*uint 4 reg 22)'S <= (pow2 64-1)*(pow2 64-1) }
assert{ 0 <= at(uint 4 reg 2 + pow2 32*uint 4 reg 18)'S <= pow2 64-1 };
assert{ 0 <= at(uint 4 reg 6 + pow2 32*uint 4 reg 22)'S <= pow2 64-1 };
end;
end; (* BLOCK3.2 *)
(* level 1: combine l h and m *)
ldd r20 rZ 0;
ldd r21 rZ 1;
......@@ -1812,12 +1926,28 @@ end;
ldd r8 rZ 6 ;
ldd r9 rZ 7;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18 = ?cf*(pow2 128 - 1) + (if stack[!stack_pointer] = 0 then -1 else 1)*old(uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18) }
ensures { reg[1] = reg[0] = ?cf*0xFF }
ensures { !stack_pointer = old !stack_pointer + 1 }
(* TODO optimise *)
'B:
(* process sign bit *)
pop r0 ;
com r0;
assert { reg[0] = if stack[!stack_pointer] = 0 then 0xFF else 0x00 };
(* TODO OPT: i don't think this is necessary *)
'Q:
mov r1 r0;
'Q1:
asr r1;
assert { at reg[1] 'Q1 = 0x00 -> reg[1] = 0x00 };
assert { at reg[1] 'Q1 = 0xFF -> reg[1] = 0xFF };
assert { at reg[0] 'Q = 0x00 -> reg[1] = 0x00 };
assert { at reg[0] 'Q = 0xFF -> reg[1] = 0xFF };
(* invert all bits or do nothing *)
eor r4 r0;
......@@ -1836,8 +1966,35 @@ end;
eor r27 r0;
eor r18 r0;
eor r19 r0;
assert { reg[0] = 0x00 -> uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18 = at(uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'B };
assert { reg[0] = 0xFF -> uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18 = pow2 128 - 1 - at(uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'B };
(* TODO OPT: replace with asr *)
mov r28 r0;
add r28 r28; (* sets carry flag if r28 = 0xff *)
assert { ?cf = 1-as_bool stack[!stack_pointer] };
check { "expl:possible endcondition" let cor = reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] in cor = ?cf*(pow2 64-1)
by reg[1] = reg[0] = ?cf*0xFF };
S.modify_r0(); S.modify_r1();
S.modify_r4(); S.modify_r5(); S.modify_r6(); S.modify_r7();
S.modify_r10(); S.modify_r11(); 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_r26(); S.modify_r27(); S.modify_r28(); S.modify_r29();
end;
'AD:
(* TODO: do we need this abstract block? *)
abstract
ensures { S.synchronized S.shadow reg }
ensures { let dst = uint 24 mem (old (uint 2 reg rZ+8)) in
let x1y = old(uint 16 mem (uint 2 reg rZ+16)) in
let x0 = old(uint 6 reg 20 + pow2 48*uint 2 reg 8) in
let m = old(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18) in
let cor = old(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1]) in
let res = (1+pow2 64)*x1y + x0 + m + pow2 128*cor in
dst = res \/ dst + pow2 192 = res \/ dst + 2*pow2 192 = res }
ensures { forall i. mem[i] <> (old mem)[i] -> uint 2 reg rZ+8 <= i < uint 2 reg rZ+32 }
'E:
(* add in m *)
adc r20 r4;
adc r21 r5;
......@@ -1847,7 +2004,9 @@ end;
adc r25 r11;
adc r8 r12;
adc r9 r13;
check { ?cf*pow2 64 + uint 6 reg 20 + pow2 48*uint 2 reg 8 = at(?cf + uint 6 reg 20 + pow2 48*uint 2 reg 8+ uint 4 reg 4 + pow2 32*uint 4 reg 10)'E };
(* store carrrY in r28 *)
'A:
clr r28;
adc r28 r28;
......@@ -1879,11 +2038,21 @@ end;
std rZ 14 r8;
std rZ 15 r9;
movw r8 r2;
check { (?cf+reg[28])*pow2 64 + uint 8 mem (uint 2 reg rZ+8) = at(uint 8 mem (uint 2 reg rZ+16) + ?cf + uint 6 reg 20 + pow2 48*uint 2 reg 8+ uint 4 reg 4 + pow2 32*uint 4 reg 10)'E };
(* store carrrY in r2 *)
'B:
clr r2;
adc r2 r2;
(* TODO enable the theory in the next big re-load *)
assume { "expl:removeme" BV8.eq (BV8.lsr BV8.zeros 1) BV8.zeros };
assume { "expl:removeme" BV8.eq (BV8.lsr (BV8.of_int 1) 1) BV8.zeros };
check { reg[28] = 0 \/ reg[28] = 1 };
'Q:
lsr r28;
check { ?cf = 0 <-> at reg[28] 'Q = 0 };
check { reg[28] = 0 }; (* TODO OPT i don't get this *)
adc r20 r14;
adc r21 r15;
adc r22 r16;
......@@ -1892,9 +2061,13 @@ end;
adc r25 r27;
adc r8 r18;
adc r9 r19;
check { ?cf*pow2 64 + uint 6 reg 20 + pow2 48*uint 2 reg 8 = at ?cf 'A + at(uint 8 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18)'E };
'QQ:
(* store carrrY in r1:r0 *)
adc r0 r28;
adc r1 r28;
'QP:
check { reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] + ?cf*pow2 64 = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ };
ldd r4 rZ 24;
ldd r5 rZ 25;
......@@ -1904,8 +2077,12 @@ end;
ldd r11 rZ 29;
ldd r12 rZ 30;
ldd r13 rZ 31;
check { uint 4 reg 4 + pow2 32*uint 4 reg 10 = at(uint 8 mem (uint 2 reg rZ+24))'E };
check { reg[2] = 0 \/ reg[2] = 1 };
'Q:
lsr r2;
check { ?cf = 0 <-> at reg[2] 'Q = 0 };
adc r20 r4;
adc r21 r5;
adc r22 r6;
......@@ -1914,9 +2091,16 @@ end;
adc r25 r11;
adc r8 r12;
adc r9 r13;
check { ?cf*pow2 64 + uint 6 reg 20 + pow2 48*uint 2 reg 8 = - at ?cf 'QQ * pow2 64 + at ?cf 'B + at ?cf 'A + at(uint 8 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E };
(* store carrrY in r1:r0 *)
'QQ2:
check { reg[2] = 0 };
check { reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] + (at ?cf 'QP)*pow2 64 = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ };
adc r0 r2;
adc r1 r2;
'QP2:
check { reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] + ?cf*pow2 64 = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'QQ2 + at ?cf 'QQ2 };
check { reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] + (at ?cf 'QP)*pow2 64 + ?cf*pow2 64 = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2};
std rZ 16 r20;
std rZ 17 r21;
......@@ -1926,6 +2110,21 @@ end;
std rZ 21 r25;
std rZ 22 r8;
std rZ 23 r9;
check { at ?cf 'QQ2*pow2 64 + uint 8 mem (uint 2 reg rZ+16) = - at ?cf 'QQ * pow2 64 + at ?cf 'B + at ?cf 'A + at(uint 8 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E };
check { at ?cf 'QQ2*pow2 64 + uint 16 mem (uint 2 reg rZ+16) = - at ?cf 'QQ * pow2 64 + at ?cf 'B + at ?cf 'A + at(uint 16 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E };
check { pow2 64*at(?cf+reg[28]) 'B + at ?cf 'QQ2*pow2 128 + uint 24 mem (uint 2 reg rZ+8) = - at ?cf 'QQ * pow2 128 + pow2 64*(at ?cf 'B + at ?cf 'A) + pow2 64*at(uint 16 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E + at(uint 8 mem (uint 2 reg rZ+16) + ?cf + uint 6 reg 20 + pow2 48*uint 2 reg 8+ uint 4 reg 4 + pow2 32*uint 4 reg 10)'E};
check { (at ?cf 'QQ+at ?cf 'QQ2)*pow2 128 + uint 24 mem (uint 2 reg rZ+8) = pow2 64*at(uint 16 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E + at(uint 8 mem (uint 2 reg rZ+16) + ?cf + uint 6 reg 20 + pow2 48*uint 2 reg 8+ uint 4 reg 4 + pow2 32*uint 4 reg 10)'E};
check { reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2 \/
reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] + pow2 64 = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2};
check { reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2 \/
reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1] + pow2 64 = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2 };
'PP:
(* propagate carry to end *)
add r4 r0;
......@@ -1945,6 +2144,102 @@ end;
std rZ 29 r11;
std rZ 30 r12;
std rZ 31 r13;
check { ?cf*pow2 64 + uint 8 mem (uint 2 reg rZ+24) = at (uint 8 mem (uint 2 reg rZ+24))'E + at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'PP};
check { ?cf*pow2 64 + uint 8 mem (uint 2 reg rZ+24) = at (uint 8 mem (uint 2 reg rZ+24))'E + at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2 - (at ?cf 'QP + at ?cf 'QP2)*pow2 64 };
check { ?cf*pow2 64 + uint 8 mem (uint 2 reg rZ+24) = at (uint 8 mem (uint 2 reg rZ+24))'E + at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E + at ?cf 'QQ + at ?cf 'QQ2 - (at ?cf 'QP + at ?cf 'QP2)*pow2 64 };
check {
?cf*pow2 192 + uint 24 mem (uint 2 reg rZ+8) =
pow2 64*at(uint 16 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E + at(uint 8 mem (uint 2 reg rZ+16) + ?cf + uint 6 reg 20 + pow2 48*uint 2 reg 8+ uint 4 reg 4 + pow2 32*uint 4 reg 10)'E + pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E
\/
?cf*pow2 192 + uint 24 mem (uint 2 reg rZ+8) =
pow2 64*at(uint 16 mem (uint 2 reg rZ+16) + uint 4 reg 14 + pow2 32*uint 2 reg 26 + pow2 48*uint 2 reg 18 + uint 8 mem (uint 2 reg rZ+24))'E + at(uint 8 mem (uint 2 reg rZ+16) + ?cf + uint 6 reg 20 + pow2 48*uint 2 reg 8+ uint 4 reg 4 + pow2 32*uint 4 reg 10)'E + pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E - pow2 192
};
check {
?cf*pow2 192 + uint 24 mem (uint 2 reg rZ+8)
= (1+pow2 64)*at(uint 16 mem (uint 2 reg rZ+16))'E
+ at(uint 6 reg 20 + pow2 48*uint 2 reg 8)'E
+ at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'E
+ pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E
\/
?cf*pow2 192 + uint 24 mem (uint 2 reg rZ+8)
= (1+pow2 64)*at(uint 16 mem (uint 2 reg rZ+16))'E
+ at(uint 6 reg 20 + pow2 48*uint 2 reg 8)'E
+ at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'E
+ pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E
-pow2 192
};
check {
uint 24 mem (uint 2 reg rZ+8)
= (1+pow2 64)*at(uint 16 mem (uint 2 reg rZ+16))'E
+ at(uint 6 reg 20 + pow2 48*uint 2 reg 8)'E
+ at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'E
+ pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E
\/
pow2 192 + uint 24 mem (uint 2 reg rZ+8)
= (1+pow2 64)*at(uint 16 mem (uint 2 reg rZ+16))'E
+ at(uint 6 reg 20 + pow2 48*uint 2 reg 8)'E
+ at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'E
+ pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E
\/
2*pow2 192 + uint 24 mem (uint 2 reg rZ+8)
= (1+pow2 64)*at(uint 16 mem (uint 2 reg rZ+16))'E
+ at(uint 6 reg 20 + pow2 48*uint 2 reg 8)'E
+ at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'E
+ pow2 128*at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'E
};
S.modify_r0(); S.modify_r1();
S.modify_r2(); S.modify_r3(); S.modify_r28();
S.modify_r4(); S.modify_r5(); S.modify_r6(); S.modify_r7();
S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13();
S.modify_r20(); S.modify_r21(); S.modify_r22(); S.modify_r23(); S.modify_r24(); S.modify_r25(); S.modify_r8(); S.modify_r9();
end;
assert { let dst = uint 32 mem (at (uint 2 reg rZ)'AD) in
let x0 = at(uint 8 mem (uint 2 reg rZ))'AD in
let x1y = at(uint 16 mem (uint 2 reg rZ+16))'AD in
(* let x0 = at(uint 6 reg 20 + pow2 48*uint 2 reg 8)'AD in *)
let m = at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'AD in
let cor = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'AD in
let res = (pow2 64+1)*x0 + pow2 64*((pow2 64+1)*x1y + m) + pow2 192*cor in
dst = res \/ dst + pow2 256 = res \/ dst + 2*pow2 256 = res };
assert { let m = at(?cf + uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 26 + pow2 112*uint 2 reg 18)'AD in
let cor = at(reg[0] + (pow2 8+pow2 16+pow2 24+pow2 32+pow2 40+pow2 48+pow2 56)*reg[1])'AD in
m + pow2 128*cor = - at(((uint 8 mem (uint 2 reg rX)-uint 8 mem (uint 2 reg rX+8)))*(uint 8 mem (uint 2 reg rY)-uint 8 mem (uint 2 reg rY+8)))'S \/
m + pow2 128*cor = pow2 192 - at(((uint 8 mem (uint 2 reg rX)-uint 8 mem (uint 2 reg rX+8)))*(uint 8 mem (uint 2 reg rY)-uint 8 mem (uint 2 reg rY+8)))'S
};
assert { let x0 = at(uint 8 mem (uint 2 reg rZ))'AD in
let x1y = at(uint 16 mem (uint 2 reg rZ+16))'AD in
x0 + pow2 64*x1y = at (uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY)
+pow2 64 * uint 8 mem (uint 2 reg rX+8) * uint 8 mem (uint 2 reg rY+8))'S
};
assert { uint 32 mem (at (uint 2 reg rZ)'AD) = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S \/
uint 32 mem (at (uint 2 reg rZ)'AD) - pow2 256 = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S \/
uint 32 mem (at (uint 2 reg rZ)'AD) + pow2 256 = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S \/
uint 32 mem (at (uint 2 reg rZ)'AD) + 2*pow2 256 = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S };
assert { uint 32 mem (at (uint 2 reg rZ)'S) = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S \/
uint 32 mem (at (uint 2 reg rZ)'S) - pow2 256 = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S \/
uint 32 mem (at (uint 2 reg rZ)'S) + pow2 256 = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S \/
uint 32 mem (at (uint 2 reg rZ)'S) + 2*pow2 256 = at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S
by at (uint 2 reg rZ)'S = at(uint 2 reg rZ)'AD
};
abstract ensures { 0 <= uint 32 mem (at (uint 2 reg rZ)'S) < pow2 256 }
uint_bound mem (!(S.shadow.S.r30) + !(S.shadow.S.r31)*pow2 8) 32;
end;
abstract ensures { 0 <= at (uint 16 mem (uint 2 reg rX) * uint 16 mem (uint 2 reg rY))'S <= (pow2 128-1)*(pow2 128-1) }
assert { 0 <= at (uint 16 mem (uint 2 reg rX))'S <= pow2 128-1 };
assert { 0 <= at (uint 16 mem (uint 2 reg rY))'S <= pow2 128-1 };
()
end
end
......@@ -3,12 +3,12 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="130" steplimit="0" 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="130" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="6" name="Eprover" version="2.0" timelimit="13" steplimit="0" memlimit="1000"/>
<file name="../karatsuba128.mlw" expanded="true">
<file name="../karatsuba128.mlw">
<theory name="BV_asr_Lemmas" sum="e307a42e87b86733d48290e3efbe337c">
<goal name="asr_0" expl="">
<proof prover="5"><result status="valid" time="0.06" steps="110"/></proof>
......@@ -20,13 +20,13 @@
<proof prover="5"><result status="valid" time="0.08" steps="165"/></proof>
</goal>
<goal name="xor_0" expl="">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="1" timelimit="13" steplimit="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="xor_1" expl="">
<proof prover="1"><result status="valid" time="0.15"/></proof>
<proof prover="1" timelimit="13" steplimit="1"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="or_0" expl="">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="13" steplimit="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="pow2_72" expl="">
<proof prover="0" steplimit="1"><result status="valid" time="0.66"/></proof>
......@@ -101,6 +101,14 @@
<proof prover="0"><result status="valid" time="3.36"/></proof>
</goal>
</theory>
<theory name="BV_lsr_Lemmas" sum="af454ff5a915f88995d04e41f1fcc86c">
<goal name="lsr_0" expl="">
<proof prover="5" steplimit="0"><result status="valid" time="0.10" steps="110"/></proof>
</goal>
<goal name="lsr_1" expl="">
<proof prover="0"><result status="valid" time="0.44"/></proof>
</goal>
</theory>
<theory name="AvrModelLemmas" sum="84c2740c682dbec30eb04b8ce55086ee">
<goal name="register_file_invariant_strengthen" expl="">
<proof prover="5"><result status="valid" time="0.04" steps="70"/></proof>
......@@ -109,29 +117,81 @@
<proof prover="5"><result status="valid" time="0.01" steps="68"/></proof>
</goal>
</theory>
<theory name="KaratAvr" sum="54655722877aba4ce2f42ed07971f1da" expanded="true">
<theory name="KaratAvr" sum="b3afa891be0a7075af19bee8f53526c2">
<goal name="mul_bound_preserve" expl="">
<proof prover="3" obsolete="true"><result status="valid" time="0.26"/></proof>
<proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter peel_apart" expl="VC for peel_apart" expanded="true">
<goal name="bit_blit" expl="">
<transf name="eliminate_if">
<goal name="bit_blit.1" expl="">
<transf name="split_goal_wp">
<goal name="bit_blit.1.1" expl="">
<proof prover="4" timelimit="13"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="bit_blit.1.2" expl="">
<proof prover="1" timelimit="13"><result status="valid" time="0.33"/></proof>
</goal>
</transf>