Commit 70d2f1bd authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

ported to why3 0.88.3

parent c83341b2
......@@ -9,8 +9,8 @@ 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 xor_0: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> to_uint (bw_xor (of_int w) ones) = 255 - w
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
lemma or_0: forall w. bw_or zeros w = w
......@@ -41,7 +41,7 @@ end
module KaratAvr
use import avrmodel2.AVRint
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
......@@ -49,26 +49,9 @@ use import AvrModelLemmas
use BV_asr_Lemmas
use bv.BV8
let mul16 (): unit
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
=
clr r23;
mul r3 r8;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r23
use import int.Abs
use avrmodel2.Shadow as S
use avrmodel.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
......@@ -208,9 +191,7 @@ ensures { reg[27] = if old (uint 3 reg 5 < uint 3 reg 17) then 0xFF else 0x00 }
end;
(* ;--- Compute H + (l3l4l5) --- *)
(*
S.init();
*)
(* S.init(); *)
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 3 reg 11 + pow2 24*uint 3 reg 20 = old (uint 3 reg 11 + uint 3 reg 14*uint 3 reg 17) }
......@@ -259,9 +240,7 @@ ensures { reg[18] = 0 /\ reg[19] = 0 }
end;
(* ;--- Compute M --- *)
(*
S.init();
*)
(* S.init(); *)
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 14 = old (uint 3 reg 2*uint 3 reg 5) }
......@@ -305,9 +284,7 @@ ensures { uint 6 reg 14 = old (uint 3 reg 2*uint 3 reg 5) }
end;
(* TODO optimize/analyse me? *)
(*
S.init();
*)
(* S.init(); *)
abstract
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 8 + pow2 48*uint 3 reg 20 + ?cf*pow2 48 = old (uint 6 reg 8 + pow2 48*uint 3 reg 20 + uint 3 reg 11 + pow2 24*uint 3 reg 20) }
......@@ -331,9 +308,7 @@ ensures { old(uint 3 reg 8) + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 + ?cf
S.modify_r8(); S.modify_r9(); S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13();
end;
(*
S.init();
*)
(* S.init(); *)
abstract
ensures { S.synchronized S.shadow reg }
(*
......
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