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

brought karatsuba branch in line with curve25519 changes

parent 164fbe01
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(*
general TODO:
- memory stack invariance
labels to investigate
'AD
'Q1
*)
module BV_asr_Lemmas
use import bv.BV8
......@@ -17,9 +9,6 @@ lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones
lemma lsr_0: eq (lsr zeros 1) zeros
lemma lsr_1: eq (lsr (of_int 1) 1) zeros
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
......@@ -544,7 +533,6 @@ 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) };
......@@ -694,7 +682,6 @@ end;
ldd r24 rY 14;
ldd r25 rY 15;
(* 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) };
......@@ -1109,8 +1096,6 @@ assert {
end; (* BLOCK2 *)
'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) };
......@@ -1685,7 +1670,7 @@ check { reg[0] = 0xFF -> uint 4 reg 4 + pow2 32*uint 8 reg 10 + pow2 96*uint 2 r
add r28 r28; (* sets carry flag if r28 = 0xff *)
(*
check { ?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)
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();
......@@ -1850,11 +1835,11 @@ check { let x0 = at(uint 8 mem (uint 2 reg rZ))'AD in
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
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
};
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;
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 };
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment