Commit f05fa190 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

partial proof of karatsuba64

parent 272de8d1
......@@ -5,9 +5,9 @@ use int.Int
use bv.Pow2int
use int.EuclideanDivision
lemma asr_0: (asr zeros 1) = zeros
lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: (asr ones 1) = ones
lemma asr_0: (asr zeros 1) == zeros
lemma asr_1: (asr (of_int 1) 1) == zeros
lemma asr_f: (asr ones 1) == ones
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
......@@ -48,6 +48,7 @@ use bv.BV8
use avrmodel.AVRint
use AvrModelLemmas
use BV_asr_Lemmas
use ref.Ref
use int.Abs
......@@ -56,10 +57,18 @@ use avrmodel.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
meta rewrite_def function (!)
let karatsuba64_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 }
requires { valid_addr_space reg }
requires { valid_addr_space mem }
requires { valid_addr_space stack }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
ensures { uint 16 mem (old (uint 2 reg rZ)) = old (uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY)) }
=
label S in
......@@ -82,6 +91,9 @@ label L00 in
S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 = old(uint 4 reg 2 * uint 4 reg 6) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
mul r2 r8; (* a0*b2 *)
movw r12 r0;
mul r2 r6; (* a0*b0 *)
......@@ -179,6 +191,9 @@ begin 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)) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
label B in
(* subtract a0 a4 *)
......@@ -227,6 +242,10 @@ S.init();
label Tmp in
begin ensures { S.synchronized S.shadow reg }
ensures { uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18 = old (uint 4 reg 14 + uint 4 reg 18*uint 4 reg 22) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* compute h (l4 l5 l6 l7) *)
mul r18 r22;
add r14 r0;
......@@ -310,6 +329,10 @@ end;
S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = old (uint 4 reg 2*uint 4 reg 6) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* compute m *)
mul r2 r6;
movw r20 r0;
......@@ -389,6 +412,9 @@ S.init();
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + ?cf*pow2 64 = old(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* add l4 h0 to l0 and h4 *)
label B in
add r10 r14;
......@@ -408,6 +434,9 @@ begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* process sign bit *)
label B in
......@@ -440,6 +469,10 @@ end;
S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf = old(?cf + uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(uint 1 reg 26 + (pow2 8+pow2 16+pow2 24)*reg[0])) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* add in m *)
adc r10 r20;
adc r11 r21;
......
This diff is collapsed.
This diff is collapsed.
No preview for this file type
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