Commit 98a67a51 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

incorporated changes to the interface for the mul256 operation

parent 2dfe64a8
......@@ -85,22 +85,24 @@ lemma bit_blit: forall b. BV8.t'int (bitset (BV8.of_int 0) 0 b) = (if b then 1 e
function as_bool (x: int): int = if x = 0 then 0 else 1
let mul128()
requires { 32 <= uint 2 reg rX < pow2 15 }
(* NOTE: the first four bytes are preloaded in r2..r5 (for X, with increment) and r6..r9 (for Y) *)
let mul128 ()
requires { uint 4 reg 2 = uint 4 mem (uint 2 reg rX-4) /\ uint 4 reg 6 = uint 4 mem (uint 2 reg rY) }
requires { 32 <= uint 2 reg rX-4 < pow2 15 }
requires { 32 <= uint 2 reg rY < pow2 15 }
requires { 32 <= uint 2 reg rZ < pow2 15 }
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 rX-4 \/ uint 2 reg rZ >= uint 2 reg rX-4+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)) }
ensures { uint 32 mem (old (uint 2 reg rZ)) = old (uint 16 mem (uint 2 reg rX-4) * uint 16 mem (uint 2 reg rY)) }
=
'S:
S.init();
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 }
= at( uint 8 mem (uint 2 reg rX-4) * 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 }
ensures { uint 2 reg rX = old(uint 2 reg rX)-4+8 }
ensures { uint 2 reg rY = old(uint 2 reg rY) }
ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
......@@ -112,6 +114,7 @@ ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
movw r16 r20;
(* level 2: compute l *)
(*NOTE: standalone Karatsuba128 would load rX and rY here
ld_inc r2 rX;
ld_inc r3 rX;
ld_inc r4 rX;
......@@ -120,6 +123,7 @@ ensures { uint 2 reg rZ = old(uint 2 reg rZ) }
ldd r7 rY 1;
ldd r8 rY 2;
ldd r9 rY 3;
*)
'L00:
S.init();
......@@ -538,7 +542,7 @@ 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 rX-4+8)'S) };
assert { "expl:memory" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) };
abstract (* BLOCK2: karatsuba64 on upper half + add to lower half in prep for (w+1)(Xl*Yl + w*Xh*Yh) *)
......@@ -548,7 +552,7 @@ 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 }
+ at( uint 8 mem (uint 2 reg rX-4+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 *)
......@@ -687,7 +691,7 @@ end;
ldd r24 rY 14;
ldd r25 rY 15;
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 rX-4+8)'S) };
assert { "expl:memory" eq 8 mem (at mem 'S) (at (uint 2 reg rY+8)'S) };
'L01:
......@@ -1008,7 +1012,7 @@ end;
(* this assert helps verification time later on *)
assert { "expl:speedbooster"
let x = at (uint 2 reg rX)'S in
let x = at (uint 2 reg rX-4)'S in
let y = at (uint 2 reg rY)'S in
let z = at (uint 2 reg rZ)'S in
uint 4 reg 22 + pow2 32*uint 1 reg 18 + pow2 40*uint 3 reg 2 =
......@@ -1049,10 +1053,10 @@ end;
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 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 { 0 <= at(uint 8 mem (uint 2 reg rX))'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-4+8)*uint 8 mem (uint 2 reg rY+8))'S < pow2 128 }
assert { 0 <= at(uint 8 mem (uint 2 reg rX-4))'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 { 0 <= at(uint 8 mem (uint 2 reg rX-4)*uint 8 mem (uint 2 reg rY))'S <= (pow2 64-1)*(pow2 64-1) };
(*
check { 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 <= (pow2 64-1)*(pow2 64-1) };
......@@ -1062,15 +1066,15 @@ end;
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
};
*)
assert { 0 <= at(uint 8 mem (uint 2 reg rX+8))'S <= (pow2 64-1) };
assert { 0 <= at(uint 8 mem (uint 2 reg rX-4+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) };
assert { 0 <= at(uint 8 mem (uint 2 reg rX-4+8)*uint 8 mem (uint 2 reg rY+8))'S <= (pow2 64-1)*(pow2 64-1) };
end;
(* this assert appears to be necessary for provers to see that the carry flag can be ignored *)
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)
= 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-4+8) * uint 8 mem (uint 2 reg rY+8) ) 'S + (if at ?cf 'QQ > at (reg[21] + ?cf)'Q then pow2 128 else 0)
};
(*
......@@ -1103,16 +1107,16 @@ assert {
end; (* BLOCK2 *)
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 rX-4)'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 2 + pow2 32*uint 4 reg 18 = at(abs(uint 8 mem (uint 2 reg rX-4) - uint 8 mem (uint 2 reg rX-4+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)) <->
<-> at((uint 8 mem (uint 2 reg rX-4) < uint 8 mem (uint 2 reg rX-4+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] = 0x01 }
......@@ -1121,8 +1125,8 @@ 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 }
ensures { uint 4 reg 2 + pow2 32*uint 4 reg 18 = at(uint 8 mem (uint 2 reg rX-4))'S }
ensures { uint 8 reg 10 = at(uint 8 mem (uint 2 reg rX-4+8))'S }
sbiw r26 16;
ld_inc r2 rX;
ld_inc r3 rX;
......@@ -1140,6 +1144,12 @@ ensures { uint 8 reg 10 = at(uint 8 mem (uint 2 reg rX+8))'S }
ld_inc r15 rX;
ld_inc r16 rX;
ld_inc r17 rX;
(*TODO: enable
push r26;
push r27;
push r28;
push r29;
*)
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();
......@@ -1818,6 +1828,12 @@ 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;
(* TODO: enable
pop r29;
pop r28;
pop r27;
pop r26;
*)
(*
(* this is a corollary of the last block *)
......@@ -1845,17 +1861,17 @@ check { let x0 = at(uint 8 mem (uint 2 reg rZ))'AD in
*)
(* the final stepping stone; only one of these is actually the case, of course, but provers cannot decide that yet *)
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
assert { uint 32 mem (at (uint 2 reg rZ)'S) = at (uint 16 mem (uint 2 reg rX-4) * 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-4) * 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-4) * 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-4) * uint 16 mem (uint 2 reg rY))'S
};
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 };
abstract ensures { 0 <= at (uint 16 mem (uint 2 reg rX-4) * uint 16 mem (uint 2 reg rY))'S <= (pow2 128-1)*(pow2 128-1) }
assert { 0 <= at (uint 16 mem (uint 2 reg rX-4))'S <= pow2 128-1 };
assert { 0 <= at (uint 16 mem (uint 2 reg rY))'S <= pow2 128-1 };
()
end
......
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment