module BV_asr_Lemmas

use bv.BV8
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 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 pow2_72: pow2 72 = 0x1000000000000000000
lemma pow2_80: pow2 80 = 0x100000000000000000000
lemma pow2_88: pow2 88 = 0x10000000000000000000000
lemma pow2_96: pow2 96 = 0x1000000000000000000000000

end

module AvrModelLemmas

use int.Int
use map.Map
use int.EuclideanDivision
use bv.Pow2int

lemma register_file_invariant_strengthen:
  forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)

lemma pow_split: forall k. k >= 0 -> pow2 (2*k) = pow2 k*pow2 k

end

module KaratAvr

use int.Int
use int.EuclideanDivision
use bv.Pow2int
use avrmodelunbounded.AVRint
use AvrModelLemmas
use BV_asr_Lemmas

(*
axiom addr_contains_bytes: forall reg:address_space. forall i. 0 <= reg[i] < 256
*)
(*
Having these predicates is useful, but having it in the proof context messes with the provers
predicate regs_positive (reg: int -> int) = reg[0] >= 0 /\ reg[1] >= 0 /\ reg[2] >= 0 /\ reg[3] >= 0/\ reg[4] >= 0/\ reg[5] >= 0/\ reg[6] >= 0/\ reg[7] >= 0/\ reg[8] >= 0/\ reg[9] >= 0 /\ reg[10] >= 0 /\ reg[11] >= 0 /\ reg[12] >= 0 /\ reg[13] >= 0 /\ reg[14] >= 0 /\ reg[15] >= 0 /\ reg[16] >= 0 /\ reg[17] >= 0 /\ reg[18] >= 0 /\ reg[19] >= 0 /\ reg[20] >= 0 /\ reg[21] >= 0 /\ reg[22] >= 0 /\ reg[23] >= 0 /\ reg[24] >= 0/\ reg[25] >= 0/\ reg[26] >= 0/\ reg[27] >= 0/\ reg[28] >= 0/\ reg[29] >= 0/\ reg[30] >= 0/\ reg[31] >= 0
predicate regs_below_256 (reg: int -> int) = reg[0] < 256 /\ reg[1] < 256 /\ reg[2] < 256 /\ reg[3] < 256/\ reg[4] < 256/\ reg[5] < 256/\ reg[6] < 256/\ reg[7] < 256/\ reg[8] < 256/\ reg[9] < 256 /\ reg[10] < 256 /\ reg[11] < 256 /\ reg[12] < 256 /\ reg[13] < 256 /\ reg[14] < 256 /\ reg[15] < 256 /\ reg[16] < 256 /\ reg[17] < 256 /\ reg[18] < 256 /\ reg[19] < 256 /\ reg[20] < 256 /\ reg[21] < 256 /\ reg[22] < 256 /\ reg[23] < 256 /\ reg[24] < 256/\ reg[25] < 256/\ reg[26] < 256/\ reg[27] < 256/\ reg[28] < 256/\ reg[29] < 256/\ reg[30] < 256/\ reg[31] < 256
*)
let mul8 (): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 2 reg 12 = old(uint 1 reg 3 * uint 1 reg 8) }
= mul r3 r8;
  movw r12 r0

let mul16 (): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  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;
  ()

(* NOTE: by changing (some of) the checks into asserts, we can test the impact on performance
   of having vs. not having an explicit mention of the 8bit-ness of the AVR architecture in the proof context.
   in the polished version, these checks should probably take place elsewhere (e.g. in avrmodel.mlw) *)
let mul24_flat (): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
=
	clr r23;
	mul r2 r9;
	movw r14  r0;

	mul r2 r7;
	movw r12  r0;

	mul r2 r8;
	add r13 r0;
	adc r14 r1;
	adc r15 r23;

	clr r16;
	mul r3 r9;
	movw r24 r0;

	mul r3 r7;
	add r13 r0;
	adc r14 r1;
	adc r15 r24;
	adc r25 r23;

	mul r3 r8;
	add r14 r0;
	adc r15 r1;
	adc r16 r25;

	clr r17;
	mul r4 r9;
	movw r24 r0;

	mul r4 r7;
	add r14 r0;
	adc r15 r1;
	adc r16 r24;
	adc r25 r23;

	mul r4 r8;
	add r15 r0;
	adc r16 r1;
	adc r17 r25

let mul32_flat(): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) }
=
	clr r23;
	mul r2 r9;
	movw r14 r0;
	mul r2 r7;
	movw r12 r0;
	mul r2 r8;
	add r13 r0;
	adc r14 r1;
	adc r15 r23;

	mul r3 r10;
	movw r16 r0;
	clr r18;
	mul r2 r10;
	movw r24 r0;
	mul r3 r7;
	add r13 r0;
	adc r14 r1;
	adc r15 r24;
	adc r25 r23;
	mul r3 r8;
	add r14 r0;
	adc r15 r1;
	adc r25 r23;
	mul r4 r10;
	add r16 r25;
	adc r17 r0;
	adc r18 r1;

  clr r19;
	mul r4 r9;
	movw r24 r0;
	mul r4 r7;
	add r14 r0;
	adc r15 r1;
	adc r16 r24;
	adc r25 r23;
	mul r3 r9;
	add r15 r0;
	adc r16 r1;
	adc r25 r23;
	mul r5 r10;
	add r17 r25;
	adc r18 r0;
	adc r19 r1;
	mul r5 r8;
	movw r24 r0;
	mul r4 r8;
	add r15 r0;
	adc r24 r1;
	adc r25 r23;
	mul r5 r7;
	add r15 r0;
	adc r24 r1;
	adc r25 r23;
	mul r5 r9;
	add r16 r24;
	adc r0 r25;
	adc r1 r23;
	add r17 r0;
	adc r18 r1;
	adc r19 r23

let mul40(): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) }
= label S in
begin
ensures { uint 10 reg 12 = old(uint 3 reg 2*uint 5 reg 7) }
ensures { eq 5 reg (reg at S) 2 }
ensures { eq 5 reg (reg at S) 7 }
ensures { reg[20] = 0 /\ reg[21] = 0 }
ensures { valid_addr_space reg by reg[0] >= 0 /\ reg[1] >= 0 /\ reg[2] >= 0 /\ reg[3] >= 0/\ reg[4] >= 0/\ reg[5] >= 0/\ reg[6] >= 0/\ reg[7] >= 0/\ reg[8] >= 0/\ reg[9] >= 0 /\ reg[10] >= 0 /\ reg[11] >= 0 /\ reg[12] >= 0 /\ reg[13] >= 0 /\ reg[14] >= 0 /\ reg[15] >= 0 /\ reg[16] >= 0 /\ reg[17] >= 0 /\ reg[18] >= 0 /\ reg[19] >= 0 /\ reg[20] >= 0 /\ reg[21] >= 0 /\ reg[22] >= 0 /\ reg[23] >= 0 /\ reg[24] >= 0/\ reg[25] >= 0/\ reg[26] >= 0/\ reg[27] >= 0/\ reg[28] >= 0/\ reg[29] >= 0/\ reg[30] >= 0/\ reg[31] >= 0 /\ reg[0] < 256 /\ reg[1] < 256 /\ reg[2] < 256 /\ reg[3] < 256/\ reg[4] < 256/\ reg[5] < 256/\ reg[6] < 256/\ reg[7] < 256/\ reg[8] < 256/\ reg[9] < 256 /\ reg[10] < 256 /\ reg[11] < 256 /\ reg[12] < 256 /\ reg[13] < 256 /\ reg[14] < 256 /\ reg[15] < 256 /\ reg[16] < 256 /\ reg[17] < 256 /\ reg[18] < 256 /\ reg[19] < 256 /\ reg[20] < 256 /\ reg[21] < 256 /\ reg[22] < 256 /\ reg[23] < 256 /\ reg[24] < 256/\ reg[25] < 256/\ reg[26] < 256/\ reg[27] < 256/\ reg[28] < 256/\ reg[29] < 256/\ reg[30] < 256/\ reg[31] < 256 }
	clr r18;
	clr r19;
	movw r20 r18;
	mul r2 r9;
	movw r14 r0;
	mul r2 r7;
	movw r12 r0;
	mul r2 r8;
	add r13 r0;
	adc r14 r1;
	adc r15 r21;
	mul r2 r11;
	movw r16 r0;
	mul r2 r10;
	add r15 r0;
	adc r16 r1;
	adc r17 r21;
	mul r3 r9;
	movw r24 r0;
	mul r3 r7;
	add r13 r0;
	adc r14 r1;
	adc r15 r24;
	adc r25 r21;
	mul r3 r8;
	add r14 r0;
	adc r15 r1;
	adc r25 r21;
	mul r3 r11;
	add r16 r25;
	adc r17 r0;
	adc r18 r1;
	mul r3 r10;
	add r16 r0;
	adc r17 r1;
	adc r18 r21;
	mul r4 r9;
	movw r24 r0;
	mul r4 r7;
	add r14 r0;
	adc r15 r1;
	adc r16 r24;
	adc r25 r21;
	mul r4 r8;
	add r15 r0;
	adc r16 r1;
	adc r25 r21;
	mul r4 r11;
	add r17 r25;
	adc r18 r0;
	adc r19 r1;
	mul r4 r10;
	add r17 r0;
	adc r18 r1;
	adc r19 r21;
end;
begin
ensures { uint 7 reg 15 = old(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7) }
(*ensures { uint 10 reg 12 = old(uint 10 reg 12 + pow2 24*uint 2 reg 5*uint 5 reg 7) }*)
ensures { eq 3 reg (old reg) 12 }
ensures { eq 5 reg (reg at S) 2 }
ensures { eq 5 reg (reg at S) 7 }
ensures { valid_addr_space reg by reg[0] >= 0 /\ reg[1] >= 0 /\ reg[2] >= 0 /\ reg[3] >= 0/\ reg[4] >= 0/\ reg[5] >= 0/\ reg[6] >= 0/\ reg[7] >= 0/\ reg[8] >= 0/\ reg[9] >= 0 /\ reg[10] >= 0 /\ reg[11] >= 0 /\ reg[12] >= 0 /\ reg[13] >= 0 /\ reg[14] >= 0 /\ reg[15] >= 0 /\ reg[16] >= 0 /\ reg[17] >= 0 /\ reg[18] >= 0 /\ reg[19] >= 0 /\ reg[20] >= 0 /\ reg[21] >= 0 /\ reg[22] >= 0 /\ reg[23] >= 0 /\ reg[24] >= 0/\ reg[25] >= 0/\ reg[26] >= 0/\ reg[27] >= 0/\ reg[28] >= 0/\ reg[29] >= 0/\ reg[30] >= 0/\ reg[31] >= 0 /\ reg[0] < 256 /\ reg[1] < 256 /\ reg[2] < 256 /\ reg[3] < 256/\ reg[4] < 256/\ reg[5] < 256/\ reg[6] < 256/\ reg[7] < 256/\ reg[8] < 256/\ reg[9] < 256 /\ reg[10] < 256 /\ reg[11] < 256 /\ reg[12] < 256 /\ reg[13] < 256 /\ reg[14] < 256 /\ reg[15] < 256 /\ reg[16] < 256 /\ reg[17] < 256 /\ reg[18] < 256 /\ reg[19] < 256 /\ reg[20] < 256 /\ reg[21] < 256 /\ reg[22] < 256 /\ reg[23] < 256 /\ reg[24] < 256/\ reg[25] < 256/\ reg[26] < 256/\ reg[27] < 256/\ reg[28] < 256/\ reg[29] < 256/\ reg[30] < 256/\ reg[31] < 256 }
label B in
(* ?  check { uint 10 reg 12 < pow2 64 -> uint 7 reg 15 < pow2 40 }; *)
	mul r5 r9;
	movw r24 r0;
	mul r5 r7;
	add r15 r0;
	adc r16 r1;
	adc r17 r24;
	adc r25 r21;
	mul r5 r8;
	add r16 r0;
	adc r17 r1;
	adc r25 r21;
	mul r5 r11;
	add r18 r25;
	adc r19 r0;
	adc r20 r1;
	mul r5 r10;
	add r18 r0;
	adc r19 r1;
	adc r20 r21;
	mul r6 r9;
	movw r24 r0;
	mul r6 r7;
	add r16 r0;
	adc r17 r1;
	adc r18 r24;
	adc r25 r21;
	mul r6 r8;
	add r17 r0;
	adc r18 r1;
	adc r25 r21;
	mul r6 r10;
	add r19 r0;
	adc r20 r1;
	adc r21 r21;
	mul r6 r11;
	add r19 r25;
	adc r20 r0;
	adc r21 r1;
(*assert { uint 7 reg 15 = at(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7)'B };*)
end

let mul40_flat(): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) }
= label S in
	clr r18;
	clr r19;
	movw r20 r18;
	mul r2 r9;
	movw r14 r0;
	mul r2 r7;
	movw r12 r0;
	mul r2 r8;
	add r13 r0;
	adc r14 r1;
	adc r15 r21;
	mul r2 r11;
	movw r16 r0;
	mul r2 r10;
	add r15 r0;
	adc r16 r1;
	adc r17 r21;
	mul r3 r9;
	movw r24 r0;
	mul r3 r7;
	add r13 r0;
	adc r14 r1;
	adc r15 r24;
	adc r25 r21;
	mul r3 r8;
	add r14 r0;
	adc r15 r1;
	adc r25 r21;
	mul r3 r11;
	add r16 r25;
	adc r17 r0;
	adc r18 r1;
	mul r3 r10;
	add r16 r0;
	adc r17 r1;
	adc r18 r21;
	mul r4 r9;
	movw r24 r0;
	mul r4 r7;
	add r14 r0;
	adc r15 r1;
	adc r16 r24;
	adc r25 r21;
	mul r4 r8;
	add r15 r0;
	adc r16 r1;
	adc r25 r21;
	mul r4 r11;
	add r17 r25;
	adc r18 r0;
	adc r19 r1;
	mul r4 r10;
	add r17 r0;
	adc r18 r1;
	adc r19 r21;
	mul r5 r9;
	movw r24 r0;
	mul r5 r7;
	add r15 r0;
	adc r16 r1;
	adc r17 r24;
	adc r25 r21;
	mul r5 r8;
	add r16 r0;
	adc r17 r1;
	adc r25 r21;
	mul r5 r11;
	add r18 r25;
	adc r19 r0;
	adc r20 r1;
	mul r5 r10;
	add r18 r0;
	adc r19 r1;
	adc r20 r21;
	mul r6 r9;
	movw r24 r0;
	mul r6 r7;
	add r16 r0;
	adc r17 r1;
	adc r18 r24;
	adc r25 r21;
	mul r6 r8;
	add r17 r0;
	adc r18 r1;
	adc r25 r21;
	mul r6 r10;
	add r19 r0;
	adc r20 r1;
	adc r21 r21;
	mul r6 r11;
	add r19 r25;
	adc r20 r0;
	adc r21 r1

let mul48 (): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= label S in
begin
ensures { uint 12 reg 14 = (uint 3 reg 2*uint 6 reg 8) at S }
ensures { eq 6 reg (reg at S) 2 }
ensures { eq 6 reg (reg at S) 8 }
ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 }
ensures { valid_addr_space reg }
	clr r20;
	clr r21;
	movw r22  r20;
	movw r24  r20;
	mul r2 r10;
	movw r16  r0;
	mul r2 r8;
	movw r14  r0;
	mul r2 r9;
	add r15 r0;
	adc r16 r1;
	adc r17 r25;
	mul r2 r12;
	movw r18 r0;
	mul r2 r11;
	add r17 r0;
	adc r18 r1;
	adc r19 r25;
	mul r2 r13;
	add r19  r0;
	adc r20  r1;
	mul r3 r10;
	movw r26  r0;
	mul r3 r8;
	add r15 r0;
	adc r16 r1;
	adc r17 r26;
	adc r27 r25;
	mul r3 r9;
	add r16 r0;
	adc r17 r1;
	adc r27 r25;
	mul r3 r12;
	add r18 r27;
	adc r19 r0;
	adc r20 r1;
	adc r21 r25;
	mul r3 r11;
	movw r26 r0;
	mul r3 r13;
	add r18 r26;
	adc r19 r27;
	adc r20 r0;
	adc r21 r1;
	mul r4 r10;
	movw r26  r0;
	mul r4 r8;
	add r16 r0;
	adc r17 r1;
	adc r18 r26;
	adc r27 r25;
	mul r4 r9;
	add r17 r0;
	adc r18 r1;
	adc r27 r25;
	mul r4 r12;
	add r19 r27;
	adc r20 r0;
	adc r21 r1;
	adc r22 r25;
	mul r4 r11;
	movw r26 r0;
	mul r4 r13;
	add r19 r26;
	adc r20 r27;
	adc r21 r0;
	adc r22 r1;
end;
begin
ensures { uint 9 reg 17 = old(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8) }
ensures { eq 3 reg (old reg) 14 }
ensures { eq 6 reg (reg at S) 2 }
ensures { eq 6 reg (reg at S) 8 }
ensures { valid_addr_space reg }
label B in
	mul r5 r10;
	movw r26  r0;
	mul r5 r8;
	add r17 r0;
	adc r18 r1;
	adc r19 r26;
	adc r27 r25;
	mul r5 r9;
	add r18 r0;
	adc r19 r1;
	adc r27 r25;
	mul r5 r12;
	add r20 r27;
	adc r21 r0;
	adc r22 r1;
	adc r23 r25;
	mul r5 r11;
	movw r26 r0;
	mul r5 r13;
	add r20 r26;
	adc r21 r27;
	adc r22 r0;
	adc r23 r1;
	mul r6 r10;
	movw r26  r0;
	mul r6 r8;
	add r18 r0;
	adc r19 r1;
	adc r20 r26;
	adc r27 r25;
	mul r6 r9;
	add r19 r0;
	adc r20 r1;
	adc r27 r25;
	mul r6 r12;
	add r21 r27;
	adc r22 r0;
	adc r23 r1;
	adc r24 r25;
	mul r6 r11;
	movw r26 r0;
	mul r6 r13;
	add r21 r26;
	adc r22 r27;
	adc r23 r0;
	adc r24 r1;
	mul r7 r10;
	movw r26  r0;
	mul r7 r8;
	add r19 r0;
	adc r20 r1;
	adc r21 r26;
	adc r27 r25;
	mul r7 r9;
	add r20 r0;
	adc r21 r1;
	adc r27 r25;
	mul r7 r12;
	add r22 r27;
	adc r23 r0;
	adc r24 r1;
	adc r25 r25;
	mul r7 r11;
	movw r26 r0;
	mul r7 r13;
	add r22 r26;
	adc r23 r27;
	adc r24 r0;
	adc r25 r1;
end

let mul48_flat (): unit
  requires { valid_addr_space reg }
  ensures { valid_addr_space reg }
  ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= label S in
	clr r20;
	clr r21;
	movw r22  r20;
	movw r24  r20;
	mul r2 r10;
	movw r16  r0;
	mul r2 r8;
	movw r14  r0;
	mul r2 r9;
	add r15 r0;
	adc r16 r1;
	adc r17 r25;
	mul r2 r12;
	movw r18 r0;
	mul r2 r11;
	add r17 r0;
	adc r18 r1;
	adc r19 r25;
	mul r2 r13;
	add r19  r0;
	adc r20  r1;
	mul r3 r10;
	movw r26  r0;
	mul r3 r8;
	add r15 r0;
	adc r16 r1;
	adc r17 r26;
	adc r27 r25;
	mul r3 r9;
	add r16 r0;
	adc r17 r1;
	adc r27 r25;
	mul r3 r12;
	add r18 r27;
	adc r19 r0;
	adc r20 r1;
	adc r21 r25;
	mul r3 r11;
	movw r26 r0;
	mul r3 r13;
	add r18 r26;
	adc r19 r27;
	adc r20 r0;
	adc r21 r1;
	mul r4 r10;
	movw r26  r0;
	mul r4 r8;
	add r16 r0;
	adc r17 r1;
	adc r18 r26;
	adc r27 r25;
	mul r4 r9;
	add r17 r0;
	adc r18 r1;
	adc r27 r25;
	mul r4 r12;
	add r19 r27;
	adc r20 r0;
	adc r21 r1;
	adc r22 r25;
	mul r4 r11;
	movw r26 r0;
	mul r4 r13;
	add r19 r26;
	adc r20 r27;
	adc r21 r0;
	adc r22 r1;
	mul r5 r10;
	movw r26  r0;
	mul r5 r8;
	add r17 r0;
	adc r18 r1;
	adc r19 r26;
	adc r27 r25;
	mul r5 r9;
	add r18 r0;
	adc r19 r1;
	adc r27 r25;
	mul r5 r12;
	add r20 r27;
	adc r21 r0;
	adc r22 r1;
	adc r23 r25;
	mul r5 r11;
	movw r26 r0;
	mul r5 r13;
	add r20 r26;
	adc r21 r27;
	adc r22 r0;
	adc r23 r1;
	mul r6 r10;
	movw r26  r0;
	mul r6 r8;
	add r18 r0;
	adc r19 r1;
	adc r20 r26;
	adc r27 r25;
	mul r6 r9;
	add r19 r0;
	adc r20 r1;
	adc r27 r25;
	mul r6 r12;
	add r21 r27;
	adc r22 r0;
	adc r23 r1;
	adc r24 r25;
	mul r6 r11;
	movw r26 r0;
	mul r6 r13;
	add r21 r26;
	adc r22 r27;
	adc r23 r0;
	adc r24 r1;
	mul r7 r10;
	movw r26  r0;
	mul r7 r8;
	add r19 r0;
	adc r20 r1;
	adc r21 r26;
	adc r27 r25;
	mul r7 r9;
	add r20 r0;
	adc r21 r1;
	adc r27 r25;
	mul r7 r12;
	add r22 r27;
	adc r23 r0;
	adc r24 r1;
	adc r25 r25;
	mul r7 r11;
	movw r26 r0;
	mul r7 r13;
	add r22 r26;
	adc r23 r27;
	adc r24 r0;
	adc r25 r1

end