Commit 9c944eea authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

friday afternoon commit: second block of outer level karatsuba proven

parent 7d81c154
......@@ -79,7 +79,7 @@ lemma mul_bound_preserve:
function as_bool (x: int): int = if x = 0 then 0 else 1
let karatsuba128_marked()
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 }
......@@ -478,7 +478,7 @@ end;
S.init();
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 =
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*(reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0])) }
(* add in m *)
adc r6 r22;
......@@ -536,13 +536,13 @@ 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) }
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 }
'B:
(* level 2: compute l *)
ld_inc r2 rX;
......@@ -670,7 +670,7 @@ assert { at(uint 4 reg 10)'B2 + pow2 32*uint 4 reg 14 = at(uint 4 reg 2*uint 4 r
S.modify_r20(); S.modify_r21();
end;
assert { "expl:tussenstand"
check { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : {Z+20}[2] : 12[6]
: 14[4] : {!pop!} = X0*Y0 + ww(w+1)(X1l*Y1l)
......@@ -680,14 +680,16 @@ assert { "expl:tussenstand"
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 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*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 *)
......@@ -700,6 +702,7 @@ by
ldd r23 rY 13;
ldd r24 rY 14;
ldd r25 rY 15;
(* TODO: optimize this *)
(*
abstract
......@@ -709,6 +712,8 @@ 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;
*)
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) };
'L01:
S.init();
......@@ -844,24 +849,32 @@ 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!}
{Z}[8] : {Z+16}[4] : {Z+20}[2] : 12[2] : 14[4] : 10[2] : 19[2]
: 14[4] : 10[2] : 19[2] = X0*Y0 + ww(w+1)(X1l*Y1l) + www(w+1)*X1h*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)
uint 8 mem z + pow2 64*uint 6 mem (z+16) + pow2 112*uint 2 reg 12 + pow2 96*(pow2 32+1)*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19)
+ pow2 128*as_bool stack[!stack_pointer+1]
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (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
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) &&
uint 2 reg 12 = at(uint 2 reg 12)'L01
*)
(*
uint 8 mem z + pow2 64*uint 6 mem (z+16) + pow2 112*uint 2 reg 12 = uint 8 mem z + pow2 64*uint 6 mem (z+16) + at(pow2 112*uint 2 reg 12)'L01 /\
uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 10 = at(uint 4 reg 14)'L01 + uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)
*)
};
S.init();
......@@ -950,6 +963,26 @@ end;
ldd r6 rZ 20;
ldd r7 rZ 21;
check { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : 6[2] : 12[2] : 14[4] : 10[2] : 19[2]
: 14[4] : 10[2] : 19[2] = X0*Y0 + ww(w+1)(X1l*Y1l) + www*X1h*Y1h + wwww*X1h*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 4 mem (z+16) + pow2 96*uint 2 reg 6 + pow2 112*uint 2 reg 12 + pow2 96*(pow2 32+1)*(uint 4 reg 14 + pow2 32*uint 2 reg 10 + pow2 48*uint 2 reg 19)
+ pow2 128*as_bool stack[!stack_pointer+1]
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12))
};
S.init();
abstract
ensures { S.synchronized S.shadow reg }
......@@ -969,6 +1002,27 @@ ensures { uint 2 reg 6 + pow2 16*uint 6 reg 12 + ?cf*pow2 64 = old(uint 2 reg 6
S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
check { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : 6[2] : 12[2] : 14[4] : ?cf
: 10[2] : 19[2] = X0*Y0 + ww(w+1)(X1l*Y1l) + www*X1h*Y1h + wwww*X1h*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 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 160*(?cf)
+ pow2 128*as_bool stack[!stack_pointer+1]
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12))
};
abstract
ensures { S.synchronized S.shadow reg }
ensures { reg[21] = old ?cf }
......@@ -998,25 +1052,36 @@ assert { reg[0] = as_bool stack[!stack_pointer] };
S.modify_r14(); S.modify_r15(); S.modify_r16(); S.modify_r17();
end;
check { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : 6[2] : 12[2] : 14[4] : 21 + ?cf = X0*Y0 + ww(w+1)(X1l*Y1l) + wwwX1h*Y1h
{Z}[8] : {Z+16}[4] : 6[2] : 12[2] : 14[4] : 21 + ?cf = X0*Y0 + ww(w+1)(X1l*Y1l) + www*X1h*Y1h + wwww*X1h*Y1h
: 10[2] : 19[2]
*)
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
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 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 160*(?cf + reg[21])
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12))
};
(* store carrrY in r21 *)
'Q:
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) + (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 }
*)
ensures { let cor = reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old reg[21] + old ?cf - ?cf + (if ?cf > old (reg[21] + ?cf) then pow2 32 else 0) }
(* process sign bit *)
clr r8;
......@@ -1047,12 +1112,59 @@ 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;
'QQ:
assert { "expl:tussenstand-aux"
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
at(uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2)'QQ =
at (?cf*(pow2 64 - 1))'QQ - (uint 4 (at mem 'S) (x+8) - uint 4 (at mem 'S) (x+12))*(uint 4 (at mem 'S) (y+8) - uint 4 (at mem 'S) (y+12))
};
check { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : 6[2] : 12[2] : 14[4] : cor + ?cf = X0*Y0 + ww(w+1)(X1l*Y1l) + www*X1h*Y1h + wwww*X1h*Y1h
: 10[2] : 19[2] : -???
*)
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
let cor = reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0] in
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 160*(cor + ?cf)
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) + (if ?cf > at (reg[21] + ?cf)'Q then pow2 192 else 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 160*(cor + ?cf)
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12))
\/
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 160*(cor + ?cf)
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) + pow2 192
*)
};
S.init();
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
+ 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;
......@@ -1075,34 +1187,173 @@ S.modify_r12(); S.modify_r13(); S.modify_r14(); S.modify_r15(); S.modify_r16();
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 }
()
check { "expl:preherhaling"
at(
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
let cor = reg[21] + (pow2 8+pow2 16+pow2 24)*reg[0] in
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 160*(cor + ?cf)
)'QQ
=
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 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) + (if at ?cf 'QQ > at (reg[21] + ?cf)'Q then pow2 192 else 0)
};
check { "expl:herhaling"
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 4 mem (z+16) + at(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 160*(uint 1 reg 21 + (pow2 8+pow2 16+pow2 24)*reg[0] + ?cf))'QQ
=
uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) + (if at ?cf 'QQ > at (reg[21] + ?cf)'Q then pow2 192 else 0)
};
abstract abstract ensures { "expl:eindstand"
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 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
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(uint 8 (at mem 'S) (x+8)*uint 8 (at mem 'S) (y+8))
}
assert { "expl:tussenstand"
(*
{Z}[8] : {Z+16}[4] : 6[2] : 12[6] : 10[2] : 19[2] : new ?cf
= X0*Y0 + ww(w+1)(X1l*Y1l) + www*X1h*Y1h + wwww*X1h*Y1h - www*(X1l-X1h)*(Y1l-Y1h) + wwwwww ?cf
*)
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 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*(?cf)
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) -
pow2 96*(uint 4 (at mem 'S) (x+8) - uint 4 (at mem 'S) (x+12))*(uint 4 (at mem 'S) (y+8) - uint 4 (at mem 'S) (y+12))
\/
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*(?cf)
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(pow2 32+1)*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 96*(pow2 32+1)*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) +
pow2 96*(uint 4 (at mem 'S) (x+8) - uint 4 (at mem 'S) (x+12))*(uint 4 (at mem 'S) (y+8) - uint 4 (at mem 'S) (y+12))
+ pow2 192
*)
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*(?cf)
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(uint 4 (at mem 'S) (x+8) * uint 4 (at mem 'S) (y+8)) +
pow2 128*(uint 4 (at mem 'S) (x+12) * uint 4 (at mem 'S) (y+12)) + (if at ?cf 'QQ > at (reg[21] + ?cf)'Q then pow2 192 else 0)
+ pow2 96*(uint 4 (at mem 'S) (x+8)*uint 4 (at mem 'S) (y+12))
+ pow2 96*(uint 4 (at mem 'S) (x+12)*uint 4 (at mem 'S) (y+8))
= uint 8 (at mem 'S) x * uint 8 (at mem 'S) y +
pow2 64*(uint 8 (at mem 'S) (x+8)*uint 8 (at mem 'S) (y+8))
+ (if at ?cf 'QQ > at (reg[21] + ?cf)'Q then pow2 192 else 0)
};
assert {
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 {
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 (at mem 'S) x * uint 8 (at mem 'S) y + pow2 64*(uint 8 (at mem 'S) (x+8)*uint 8 (at mem 'S) (y+8)) < pow2 192
};
end end;
(* TODO find optimal proofs *)
(* to prevent why3 from splitting this too much, this is formulated using abstract instead of 'by' *)
abstract ensures { 0 <= uint 4 mem (uint 2 reg rZ+16) + pow2 32*(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19) < pow2 128 }
assert {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) };
abstract ensures { 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 }
check { "expl:doesthishelp" (pow2 64-1)*(pow2 64-1) < (pow2 64-1)*pow2 64 };
assert { 0 <= at(uint 8 mem (uint 2 reg rX))'S <= (pow2 64-1) };
assert { 0 <= at(uint 8 mem (uint 2 reg rY))'S <= (pow2 64-1) };
assert { 0 <= at(uint 8 mem (uint 2 reg rX)*uint 8 mem (uint 2 reg rY))'S <= (pow2 64-1)*(pow2 64-1) };
assert { "expl:temp" 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 };
assert { "expl:temp" 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) };
assert { 0 <= at(uint 8 mem (uint 2 reg rZ))'B <= (pow2 64-1) };
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
*)
check { "expl:doesthishelp" (pow2 64-1)*(pow2 64-1) + pow2 64-1 < pow2 128 };
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) };
assert { 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) };
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 };
assert {
uint 4 mem (uint 2 reg rZ+16) + pow2 32*(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19) + ?cf*pow2 128
= 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 + (if at ?cf 'QQ > at (reg[21] + ?cf)'Q then pow2 128 else 0)
};
assert {
uint 4 mem (uint 2 reg rZ+16) + pow2 32*(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19)
= 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
};
(*
assert {
uint 4 mem (uint 2 reg rZ+16) + pow2 32*(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19) + ?cf*pow2 128
= 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
\/
uint 4 mem (uint 2 reg rZ+16) + pow2 32*(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19) + ?cf*pow2 128
= 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
};
assert {
uint 4 mem (uint 2 reg rZ+16) + pow2 32*(uint 2 reg 6 + pow2 16*uint 6 reg 12 + pow2 64*uint 2 reg 10 + pow2 80*uint 2 reg 19)
= 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
};
*)
std rZ 20 r6;
std rZ 21 r7;
......@@ -1119,6 +1370,8 @@ end;
end; (* BLOCK2 *)
abstract
ensures { reg[26] = reg[27] = 0 }
(* level 1: subtract a0 a7 *)
sbiw r26 16;
ld_inc r2 rX;
......@@ -1216,10 +1469,15 @@ end; (* BLOCK2 *)
clr r27;
eor r0 r1;
push r0;
end;
(* level 1: compute m *)
movw r16 r26;
S.init();
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 = old(uint 4 reg 2 * uint 4 reg 6) }
mul r2 r8; (* a0*b2 *)
movw r12 r0;
mul r2 r6; (* a0*b0 *)
......@@ -1280,7 +1538,15 @@ end; (* BLOCK2 *)
add r15 r0;
adc r16 r1;
adc r17 r26;
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();
S.modify_r28(); S.modify_r29();
end;
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)) }
ensures { ?tf = 0 <-> old((uint 4 reg 2 < uint 4 reg 18) <-> (uint 4 reg 6 < uint 4 reg 22)) }
(* subtract a0 a4 *)
sub r2 r18;
sbc r3 r19;
......@@ -1316,8 +1582,13 @@ end; (* BLOCK2 *)
sbc r9 r1 ;
eor r0 r1;
bst r0 0 ;
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();
end;
(* level 2: compute h (l3 l4 l5) *)
(* level 2: compute h (l3 l4 l5) *)
mul r18 r24; (* a0*b2 *)
movw r28 r0;
mul r18 r22; (* a0*b0 *)
......@@ -1389,6 +1660,9 @@ end; (* BLOCK2 *)
adc r18 r1;
adc r25 r19;
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) }
(* level 2: compute m *)
mul r2 r8; (* a0*b2 *)
movw r22 r0;
......@@ -1455,6 +1729,7 @@ end; (* BLOCK2 *)
add r2 r0;
adc r19 r1;
adc r9 r3;
end;
(* add l4 h0 to l0 and h4 *)
movw r4 r10;
......@@ -1469,10 +1744,16 @@ end; (* BLOCK2 *)
adc r17 r25;
(* store carrrY in r3 *)
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) }
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;
dec r0;
assert { reg[0] = 0xFF*(1 - ?tf) };
(* merge carry and borrow *)
adc r3 r0;
......@@ -1489,7 +1770,18 @@ end; (* BLOCK2 *)
eor r19 r0;
eor r9 r0;
add r0 r0; (* sets carry flag if r0 = 0xff *)
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();
S.modify_r9();
end;
abstract ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + pow2 64*uint 2 reg 26 + pow2 80*uint 2 reg 18 + ?cf*pow2 96
= old(uint 8 reg 10 + pow2 64*uint 2 reg 26 + pow2 80*uint 1 reg 18 + pow2 88*uint 1 reg 25
+ ?cf
+ uint 5 reg 20 + pow2 40*uint 1 reg 2 + pow2 48*uint 1 reg 19 + pow2 56*uint 1 reg 9
+ pow2 64*(uint 1 reg 3 + (pow2 8+pow2 16+pow2 24)*reg[1])) }
(* add in m *)
adc r10 r20;
adc r11 r21;
......@@ -1505,8 +1797,10 @@ end; (* BLOCK2 *)
adc r27 r1;
adc r18 r1;
adc r25 r1;
mov r19 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();
S.modify_r26(); S.modify_r27(); S.modify_r18(); S.modify_r25(); S.modify_r19();
end;
(* level 1: combine l h and m *)
ldd r20 rZ 0;
......
......@@ -2,19 +2,19 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"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="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="3" name="Eprover" version="1.8-001" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="60" steplimit="0" 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="60" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="2.0" timelimit="13" steplimit="0" memlimit="1000"/>
<file name="../karatsuba128.mlw" expanded="true">
<theory name="BV_asr_Lemmas" sum="e307a42e87b86733d48290e3efbe337c">
<goal name="asr_0" expl="">
<proof prover="5"><result status="valid" time="0.06" steps="110"/></proof>
</goal>
<goal name="asr_1" expl="">
<proof prover="0"><result status="valid" time="7.19"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="7.19"/></proof>
</goal>
<goal name="asr_f" expl="">
<proof prover="5"><result status="valid" time="0.08" steps="165"/></proof>
......@@ -29,76 +29,76 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="pow2_72" expl="">
<proof prover="0"><result status="valid" time="0.66"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="pow2_80" expl="">
<proof prover="0"><result status="valid" time="0.59"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="0.59"/></proof>
</goal>
<goal name="pow2_88" expl="">
<proof prover="0"><result status="valid" time="0.50"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="pow2_96" expl="">
<proof prover="0"><result status="valid" time="0.52"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="pow2_104" expl="">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="pow2_112" expl="">
<proof prover="0"><result status="valid" time="1.10"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="1.10"/></proof>
</goal>
<goal name="pow2_120" expl="">
<proof prover="0"><result status="valid" time="0.96"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="0.96"/></proof>
</goal>
<goal name="pow2_128" expl="">
<proof prover="0"><result status="valid" time="1.16"/></proof>
<proof prover="0" steplimit="1"><result status="valid" time="1.16"<