(*
general TODO:
- memory stack invariance

labels to investigate
'AD
'Q1
*)
module BV_asr_Lemmas

use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision

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

lemma or_0: forall w. bw_or zeros w = 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
lemma pow2_104: pow2 104 = 0x100000000000000000000000000
lemma pow2_112: pow2 112 = 0x10000000000000000000000000000
lemma pow2_120: pow2 120 = 0x1000000000000000000000000000000
lemma pow2_128: pow2 128 = 0x100000000000000000000000000000000
lemma pow2_136: pow2 136 = 0x10000000000000000000000000000000000
lemma pow2_144: pow2 144 = 0x1000000000000000000000000000000000000
lemma pow2_152: pow2 152 = 0x100000000000000000000000000000000000000
lemma pow2_160: pow2 160 = 0x10000000000000000000000000000000000000000
lemma pow2_168: pow2 168 = 0x1000000000000000000000000000000000000000000
lemma pow2_176: pow2 176 = 0x100000000000000000000000000000000000000000000
lemma pow2_184: pow2 184 = 0x10000000000000000000000000000000000000000000000
lemma pow2_192: pow2 192 = 0x1000000000000000000000000000000000000000000000000
lemma pow2_200: pow2 200 = 0x100000000000000000000000000000000000000000000000000
lemma pow2_208: pow2 208 = 0x10000000000000000000000000000000000000000000000000000
lemma pow2_216: pow2 216 = 0x1000000000000000000000000000000000000000000000000000000
lemma pow2_224: pow2 224 = 0x100000000000000000000000000000000000000000000000000000000
lemma pow2_232: pow2 232 = 0x10000000000000000000000000000000000000000000000000000000000
lemma pow2_240: pow2 240 = 0x1000000000000000000000000000000000000000000000000000000000000
lemma pow2_248: pow2 248 = 0x100000000000000000000000000000000000000000000000000000000000000
lemma pow2_256: pow2 256 = 0x10000000000000000000000000000000000000000000000000000000000000000

end

module AvrModelLemmas

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

lemma register_file_invariant_strengthen:
  forall m m': map int int. (forall i. 0 <= m[i] < 256) -> (forall i. 0 <= m'[i] < 256) -> (forall i j. 0 <= m[i]*m'[j] <= 255*255)
(*
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 AVRcode

use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use bv.BV8
use import ref.Ref

use import int.Abs

use avrmodel.Shadow as S

lemma mul_bound_preserve:
  forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l

constant p25519: int = 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffed

let bigint_subp ()
  requires { 32 <= uint 2 reg 22 < pow2 15 }
  requires { 32 <= uint 2 reg 24 < pow2 15 }
  requires { uint 2 reg 24 <= uint 2 reg 22 \/ uint 2 reg 24 >= uint 2 reg 22 + 32 }
  ensures { uint 32 mem (old (uint 2 reg 24)) - pow2 256*reg[24] = old (uint 32 mem (uint 2 reg 22)) - p25519 }
=
  movw r26 r22; (* load operand address a to x *)
  movw r30 r24; (* load address of result to z *)
'S:

  ldi r21 0xed;
  ld_inc r20 rX;
  sub r20 r21;
  st_inc rZ  r20;

  ldi r21 0xff;

  S.init();
  for i = 1 to 30 do
    invariant { S.synchronized S.shadow reg }
    invariant { forall i. 0 <= reg[i] < 256 }
    invariant { forall i. 0 <= mem[i] < 256 }
    invariant { uint 2 reg rX = at(uint 2 reg rX+i)'S }
    invariant { uint 2 reg rZ = at(uint 2 reg rZ+i)'S }
    invariant { forall j. mem[j] <> (at mem 'S)[j] -> at(uint 2 reg rZ)'S <= j < at(uint 2 reg rZ)'S+i }
    invariant { uint i mem (at (uint 2 reg rZ)'S) = ?cf*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) }
    (* this is an on-the-fly proof by induction *)
    invariant { forall mem mem', o. eq i mem mem' o -> uint i mem o = uint i mem' o }
    let ghost i = i in
    
'B:
    assert { pow2 8*pow2 (8*i) = pow2 (8*i+8) };
    assert { mem[uint 2 reg rX] = (at mem 'S)[uint 2 reg rX] };
    ld_inc r20 rX;
    sbc r20 r21;
    st_inc rZ  r20;
(*
    check { eq i mem (at mem 'B) (at(uint 2 reg rZ)'S) };
*)
    (* apply the inductive proof *)
    assert { uint i mem (at (uint 2 reg rZ)'S) = uint i (at mem 'B) (at(uint 2 reg rZ)'S) };
    assert { mem[at(uint 2 reg rZ)'B] = ?cf*pow2 8 + at(mem[uint 2 reg rX])'B - 0xff - at (?cf) 'B };
    assert { forall o, mem. uint (i+1) mem o = uint i mem o + pow2 (8*i)*mem[o+i] };
(*
  check { uint (i+1) mem (at (uint 2 reg rZ)'S) 
         = uint i mem (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'S+i]
         = uint i mem (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
         = uint i (at mem 'B) (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
         = at(?cf)'B*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) 
           + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
         = at(?cf)'B*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) 
           + pow2 (8*i)*at(mem[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i) - pow2 (8*i)*at(?cf)'B
         = at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at(mem[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
         = at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at((at mem 'S)[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
         = at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at(mem[uint 2 reg rX+i])'S + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
         = at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i) 
         = ?cf*pow2 (8*i)*pow2 8 + at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 8*pow2 (8*i)-19)
         = ?cf*pow2 (8*(i+1)) + at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 (8*(i+1))-19) };
*)
    S.modify_r20();
    S.modify_r26(); S.modify_r27();
    S.modify_r30(); S.modify_r31();
      assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem o = uint i mem' o /\ mem[o+i] = mem'[o+i] };
(*
      assert { forall mem mem', o. eq (i+1) mem mem' o -> eq i mem mem' o };
      assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem' o = uint i mem o };
      assert { forall mem mem', o. eq (i+1) mem mem' o -> mem[o+i] = mem'[o+i] };
      assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem o + pow2 (8*i)*mem[o+i] = uint i mem' o + pow2 (8*i)*mem'[o+i] };
*)
  done;

  ldi r21 0x7f;
  ld_inc r20 rX;
  sbc r20 r21;
  st_inc rZ  r20;
(*
  check { uint 32 mem (at (uint 2 reg rZ)'S) = ?cf*pow2 256 + at(uint 32 mem (uint 2 reg rX))'S - p25519 };
*)

  clr r24;
  adc r24 r24;

end