val bv_upd_update_heap64:
  (b:IB.b8{DV.length (IB.get_downview b.IB.bsrc) % 8 == 0}) ->
  (heap:machine_heap) ->
  (i:nat{i < DV.length (IB.get_downview b.IB.bsrc) / 8}) ->
  (v:nat64) ->
  (mem:IB.interop_heap{MB.live (IB.hs_of_mem mem) b.IB.bsrc}) ->
   Lemma
     (requires IB.correct_down_p mem heap b)
     (ensures
       (let dv = IB.get_downview b.IB.bsrc in
        let bv = UV.mk_buffer dv up_view64 in
        let addrs = IB.addrs_of_mem mem in
        let h = IB.hs_of_mem mem in
        UV.length_eq bv;
        let heap' = update_heap64 (addrs b + 8 * i) v heap in
        UV.upd h bv i (UInt64.uint_to_t v) == DV.upd_seq h dv (get_seq_heap heap' addrs b)))
let bv_upd_update_heap64 b heap i v mem =
  let dv = IB.get_downview b.IB.bsrc in
  DV.length_eq dv;
  let uv = UV.mk_buffer dv up_view64 in
  let addrs = IB.addrs_of_mem mem in
  let h = IB.hs_of_mem mem in
  UV.length_eq uv;
  let ptr = addrs b + 8 * i in
  let heap' = update_heap64 ptr v heap in
  let prefix, _, suffix = UV.split_at_i uv i h in
  let s_down = prefix `Seq.append` (put64 (UInt64.uint_to_t v) `Seq.append` suffix) in
  let s_f = get_seq_heap heap' addrs b in
  let h' = UV.upd h uv i (UInt64.uint_to_t v) in
  // This is by definition of UV.upd, fetched from the friended definition
  assert (h' == DV.upd_seq h dv s_down);
  DV.upd_seq_spec h dv s_down;
  // assert (DV.as_seq h' dv == s_down);

  // We know that all elements but UV.sel h' uv i will be the same, (using UV.sel_upd lemmas)
  // hence aux1 and aux3 can be proven with initial correct_down_p on h
  // and the Bytes_Semantics.frame lemma
  // For aux2, we know that get64 (Seq.slice s_down (i*8) (i*8+8)) = v (through UV.sel lemmas)
  // We also know that get_heap_val64 ptr = v, which with get64_aux and some index matching
  // should give us the property
  let aux1 (j:nat{j < i * 8}) : Lemma (Seq.index s_down j == Seq.index s_f j)
    = let base = j / 8 in
      let s_init = DV.as_seq h dv in

      calc (==) {
        Seq.index s_down j;
        ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
        Seq.index s_down (base * 8 + j%8);
        ( == ) {  assert (base * 8 + 8 <= Seq.length s_down);
                  Seq.lemma_index_slice s_down (base*8) (base*8 + 8) (j % 8)
                } // True by slice properties
        Seq.index (Seq.slice s_down (base*8) (base*8 + 8)) (j%8);
        ( == ) {
          UV.sel_upd uv i base (UInt64.uint_to_t v) h;
          // assert (UV.sel h uv base == UV.sel h' uv base);
          UV.get_sel h uv base;
          UV.get_sel h' uv base;
          // With the injectivity of get64, which we get from get64 and put64 being inverses,
          // we get the following
          assert (Seq.equal (Seq.slice s_init (base*8) (base*8+8)) (Seq.slice s_down (base*8) (base*8+8))) }
        Seq.index (Seq.slice s_init (base*8) (base*8 + 8)) (j%8);
        ( == ) { assert (base * 8 + 8 <= Seq.length s_init);
                  Seq.lemma_index_slice s_init (base*8) (base*8 + 8) (j % 8)
                } // True by slice properties
        Seq.index s_init (base * 8 + j%8);
        ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
        Seq.index s_init j;
        ( == ) { assert (Seq.index s_init j == UInt8.uint_to_t (heap.[addrs b + j])) }
        UInt8.uint_to_t (heap.[addrs b + j]); // True by correct_down_p
        ( == ) { Vale.Arch.MachineHeap.frame_update_heap64 ptr v heap } // True by frame_update
        UInt8.uint_to_t (heap'.[addrs b + j]);
        ( == ) { } // True by definition of get_seq_heap
        Seq.index s_f j;
      }
  in let aux2(j:nat{j >= i * 8 /\ j < i * 8 + 8}) : Lemma (Seq.index s_down j == Seq.index s_f j)
    = UV.sel_upd uv i i (UInt64.uint_to_t v) h;
      // assert (UV.sel h' uv i == UInt64.uint_to_t v);
      UV.get_sel h' uv i;
      // assert (Vale.Interop.Views.get64 (Seq.slice s_down (i*8) (i*8+8)) = UInt64.uint_to_t v);
      Vale.Arch.MachineHeap.correct_update_get64 ptr v heap;
      // assert (get_heap_val64 ptr heap' = v);
      let k = j - i * 8 in
      get64_aux ptr heap' v k;
      // assert (heap'.[ptr + k] = UInt8.v (Seq.index (put64 (UInt64.uint_to_t v)) k));
      map_aux (ptr + k) (addrs b + j) (UInt8.v (Seq.index s_down j))  heap'
      // assert (heap'.[ptr + k] = heap'.[addrs b + j])
  in let aux3 (j:nat{j >= i * 8 + 8 /\ j < Seq.length s_down}) : Lemma (Seq.index s_down j == Seq.index s_f j)
    = let base = j / 8 in
      let s_init = DV.as_seq h dv in

      calc (==) {
        Seq.index s_down j;
        ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
        Seq.index s_down (base * 8 + j%8);
        ( == ) {  assert (base * 8 + 8 <= Seq.length s_down);
                  Seq.lemma_index_slice s_down (base*8) (base*8 + 8) (j % 8)
                } // True by slice properties
        Seq.index (Seq.slice s_down (base*8) (base*8 + 8)) (j%8);
        ( == ) {
          UV.sel_upd uv i base (UInt64.uint_to_t v) h;
          // assert (UV.sel h uv base == UV.sel h' uv base);
          UV.get_sel h uv base;
          UV.get_sel h' uv base;
          // With the injectivity of get64, which we get from get64 and put64 being inverses,
          // we get the following
          assert (Seq.equal (Seq.slice s_init (base*8) (base*8+8)) (Seq.slice s_down (base*8) (base*8+8))) }
        Seq.index (Seq.slice s_init (base*8) (base*8 + 8)) (j%8);
        ( == ) { assert (base * 8 + 8 <= Seq.length s_init);
                  Seq.lemma_index_slice s_init (base*8) (base*8 + 8) (j % 8)
                } // True by slice properties
        Seq.index s_init (base * 8 + j%8);
        ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
        Seq.index s_init j;
        ( == ) { assert (Seq.index s_init j == UInt8.uint_to_t (heap.[addrs b + j])) }
        UInt8.uint_to_t (heap.[addrs b + j]); // True by correct_down_p
        ( == ) { Vale.Arch.MachineHeap.frame_update_heap64 ptr v heap } // True by frame_update
        UInt8.uint_to_t (heap'.[addrs b + j]);
        ( == ) { } // True by definition of get_seq_heap
        Seq.index s_f j;
      }
  in
  Classical.forall_intro aux1;
  Classical.forall_intro aux2;
  Classical.forall_intro aux3;
  assert (Seq.equal s_down s_f)
val bv_upd_update_heap64:
  (b:IB.b8{DV.length (IB.get_downview b.IB.bsrc) % 8 == 0}) ->
  (heap:machine_heap) ->
  (i:nat{i < DV.length (IB.get_downview b.IB.bsrc) / 8}) ->
  (v:nat64) ->
  (mem:IB.interop_heap{MB.live (IB.hs_of_mem mem) b.IB.bsrc}) ->
   Lemma
     (requires IB.correct_down_p mem heap b)
     (ensures
       (let dv = IB.get_downview b.IB.bsrc in
        let bv = UV.mk_buffer dv up_view64 in
        let addrs = IB.addrs_of_mem mem in
        let h = IB.hs_of_mem mem in
        UV.length_eq bv;
        let heap' = update_heap64 (addrs b + 8 * i) v heap in
        UV.upd h bv i (UInt64.uint_to_t v) == DV.upd_seq h dv (get_seq_heap heap' addrs b)))
let bv_upd_update_heap64 b heap i v mem =
let dv = IB.get_downview b.IB.bsrc in
DV.length_eq dv;
let uv = UV.mk_buffer dv up_view64 in
let addrs = IB.addrs_of_mem mem in
let h = IB.hs_of_mem mem in
UV.length_eq uv;
let ptr = addrs b + 8 * i in
let heap' = update_heap64 ptr v heap in
let prefix, _, suffix = UV.split_at_i uv i h in
let s_down = prefix `Seq.append` ((put64 (UInt64.uint_to_t v)) `Seq.append` suffix) in
let s_f = get_seq_heap heap' addrs b in
let h' = UV.upd h uv i (UInt64.uint_to_t v) in
assert (h' == DV.upd_seq h dv s_down);
DV.upd_seq_spec h dv s_down;
let aux1 (j: nat{j < i * 8}) : Lemma (Seq.index s_down j == Seq.index s_f j) =
  let base = j / 8 in
  let s_init = DV.as_seq h dv in
  calc ( == ) {
    Seq.index s_down j;
    ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
    Seq.index s_down (base * 8 + j % 8);
    ( == ) { (assert (base * 8 + 8 <= Seq.length s_down);
      Seq.lemma_index_slice s_down (base * 8) (base * 8 + 8) (j % 8)) }
    Seq.index (Seq.slice s_down (base * 8) (base * 8 + 8)) (j % 8);
    ( == ) { (UV.sel_upd uv i base (UInt64.uint_to_t v) h;
      UV.get_sel h uv base;
      UV.get_sel h' uv base;
      assert (Seq.equal (Seq.slice s_init (base * 8) (base * 8 + 8))
            (Seq.slice s_down (base * 8) (base * 8 + 8)))) }
    Seq.index (Seq.slice s_init (base * 8) (base * 8 + 8)) (j % 8);
    ( == ) { (assert (base * 8 + 8 <= Seq.length s_init);
      Seq.lemma_index_slice s_init (base * 8) (base * 8 + 8) (j % 8)) }
    Seq.index s_init (base * 8 + j % 8);
    ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
    Seq.index s_init j;
    ( == ) { assert (Seq.index s_init j == UInt8.uint_to_t (heap.[ addrs b + j ])) }
    UInt8.uint_to_t (heap.[ addrs b + j ]);
    ( == ) { Vale.Arch.MachineHeap.frame_update_heap64 ptr v heap }
    UInt8.uint_to_t (heap'.[ addrs b + j ]);
    ( == ) { () }
    Seq.index s_f j;
  }
in
let aux2 (j: nat{j >= i * 8 /\ j < i * 8 + 8}) : Lemma (Seq.index s_down j == Seq.index s_f j) =
  UV.sel_upd uv i i (UInt64.uint_to_t v) h;
  UV.get_sel h' uv i;
  Vale.Arch.MachineHeap.correct_update_get64 ptr v heap;
  let k = j - i * 8 in
  get64_aux ptr heap' v k;
  map_aux (ptr + k) (addrs b + j) (UInt8.v (Seq.index s_down j)) heap'
in
let aux3 (j: nat{j >= i * 8 + 8 /\ j < Seq.length s_down})
    : Lemma (Seq.index s_down j == Seq.index s_f j) =
  let base = j / 8 in
  let s_init = DV.as_seq h dv in
  calc ( == ) {
    Seq.index s_down j;
    ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
    Seq.index s_down (base * 8 + j % 8);
    ( == ) { (assert (base * 8 + 8 <= Seq.length s_down);
      Seq.lemma_index_slice s_down (base * 8) (base * 8 + 8) (j % 8)) }
    Seq.index (Seq.slice s_down (base * 8) (base * 8 + 8)) (j % 8);
    ( == ) { (UV.sel_upd uv i base (UInt64.uint_to_t v) h;
      UV.get_sel h uv base;
      UV.get_sel h' uv base;
      assert (Seq.equal (Seq.slice s_init (base * 8) (base * 8 + 8))
            (Seq.slice s_down (base * 8) (base * 8 + 8)))) }
    Seq.index (Seq.slice s_init (base * 8) (base * 8 + 8)) (j % 8);
    ( == ) { (assert (base * 8 + 8 <= Seq.length s_init);
      Seq.lemma_index_slice s_init (base * 8) (base * 8 + 8) (j % 8)) }
    Seq.index s_init (base * 8 + j % 8);
    ( == ) { FStar.Math.Lemmas.euclidean_division_definition j 8 }
    Seq.index s_init j;
    ( == ) { assert (Seq.index s_init j == UInt8.uint_to_t (heap.[ addrs b + j ])) }
    UInt8.uint_to_t (heap.[ addrs b + j ]);
    ( == ) { Vale.Arch.MachineHeap.frame_update_heap64 ptr v heap }
    UInt8.uint_to_t (heap'.[ addrs b + j ]);
    ( == ) { () }
    Seq.index s_f j;
  }
in
Classical.forall_intro aux1;
Classical.forall_intro aux2;
Classical.forall_intro aux3;
assert (Seq.equal s_down s_f)
Vale.X64.BufferViewStore.fst.checked
Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Two.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.MachineHeap.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferView.Up.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.X64.BufferViewStore.fst
Vale.Interop.Types.b8 Prims.eq2 Prims.int Prims.op_Modulus LowStar.BufferView.Down.length FStar.UInt8.t Vale.Interop.Types.get_downview Vale.Interop.Types.__proj__Buffer__item__src Vale.Interop.Types.b8_preorder Vale.Interop.Types.__proj__Buffer__item__writeable Vale.Interop.Types.base_typ_as_type Vale.Interop.Types.__proj__Buffer__item__bsrc Vale.Arch.MachineHeap_s.machine_heap Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Division Vale.Def.Words_s.nat64 Vale.Interop.Heap_s.interop_heap LowStar.Monotonic.Buffer.live Vale.Interop.Heap_s.hs_of_mem FStar.Seq.Base.seq LowStar.BufferView.Up.buffer_src FStar.UInt64.t FStar.Seq.Properties.lseq LowStar.BufferView.Up.__proj__View__item__n LowStar.BufferView.Up.get_view Prims._assert FStar.Seq.Base.equal Prims.unit FStar.Classical.forall_intro Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_Addition FStar.Mul.op_Star FStar.Seq.Base.length FStar.Seq.Base.index Prims.op_Multiply Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern FStar.Calc.calc_finish Prims.Cons FStar.Preorder.relation FStar.Calc.calc_step FStar.UInt8.uint_to_t Vale.Interop.op_String_Access Vale.Def.Types_s.nat8 FStar.Seq.Base.slice FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.euclidean_division_definition FStar.Seq.Base.lemma_index_slice Prims.op_LessThanOrEqual LowStar.BufferView.Up.get_sel LowStar.BufferView.Up.sel_upd FStar.UInt64.uint_to_t Vale.Arch.MachineHeap.frame_update_heap64 LowStar.BufferView.Down.as_seq Vale.X64.BufferViewStore.map_aux FStar.UInt8.v Vale.X64.BufferViewStore.get64_aux Prims.op_Subtraction Vale.Arch.MachineHeap.correct_update_get64 LowStar.BufferView.Down.upd_seq_spec FStar.Monotonic.HyperStack.mem LowStar.BufferView.Down.upd_seq LowStar.BufferView.Up.upd Vale.Interop.get_seq_heap FStar.Seq.Base.append Vale.Interop.Views.put64 FStar.Pervasives.Native.tuple3 LowStar.BufferView.Up.as_down_buffer LowStar.BufferView.Up.split_at_i Vale.Arch.MachineHeap_s.update_heap64 LowStar.BufferView.Up.length_eq Vale.Interop.Types.addr_map Vale.Interop.Heap_s.addrs_of_mem LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer Vale.Interop.Views.up_view64 LowStar.BufferView.Down.length_eq LowStar.BufferView.Down.buffer
module Vale.X64.BufferViewStore

open FStar.Mul
open Vale.Interop.Views
open Vale.Interop
module MB = LowStar.Monotonic.Buffer
module HS = FStar.HyperStack
open Vale.Lib.BufferViewHelpers
open Vale.Def.Types_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Two
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Seq
open Vale.Arch.Types

open FStar.Calc

friend LowStar.BufferView.Up

#reset-options "--z3rlimit 10 --max_fuel 0 --initial_fuel 0 --max_ifuel 1 --initial_ifuel 1"

let math_aux (a b c:int) : Lemma (a + b + (c - b) == a + c) = ()

let map_aux (ptr1 ptr2:int) (v:int) (m:machine_heap) : Lemma
  (requires ptr1 == ptr2 /\ m.[ptr1] == v)
  (ensures m.[ptr2] == v) = ()

let get64_aux (ptr:int) (heap:machine_heap) (v:nat64) (k:nat{k < 8}) : Lemma
  (requires get_heap_val64 ptr heap == v)
  (ensures heap.[ptr + k] == UInt8.v (Seq.index (put64 (UInt64.uint_to_t v)) k)) =
  get_heap_val64_reveal ();
  put64_reveal ();
  le_nat64_to_bytes_reveal ();
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  four_to_nat_8_injective ();
  two_to_nat_32_injective ()

let get128_aux (ptr:int) (heap:machine_heap) (v:quad32) (k:nat{k < 16}) : Lemma
  (requires get_heap_val128 ptr heap == v)
  (ensures heap.[ptr + k] == UInt8.v (Seq.index (put128 v) k)) =
  get_heap_val128_reveal ();
  get_heap_val32_reveal ();
  put128_reveal ();
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  reveal_opaque (`%le_quad32_to_bytes) le_quad32_to_bytes;
  four_to_nat_8_injective ()

#reset-options "--max_fuel 1 --initial_fuel 1 --z3rlimit 200"
val bv_upd_update_heap64:
  (b:IB.b8{DV.length (IB.get_downview b.IB.bsrc) % 8 == 0}) ->
  (heap:machine_heap) ->
  (i:nat{i < DV.length (IB.get_downview b.IB.bsrc) / 8}) ->
  (v:nat64) ->
  (mem:IB.interop_heap{MB.live (IB.hs_of_mem mem) b.IB.bsrc}) ->
   Lemma
     (requires IB.correct_down_p mem heap b)
     (ensures
       (let dv = IB.get_downview b.IB.bsrc in
        let bv = UV.mk_buffer dv up_view64 in
        let addrs = IB.addrs_of_mem mem in
        let h = IB.hs_of_mem mem in
        UV.length_eq bv;
        let heap' = update_heap64 (addrs b + 8 * i) v heap in
        UV.upd h bv i (UInt64.uint_to_t v) == DV.upd_seq h dv (get_seq_heap heap' addrs b)))

    b:
      Vale.Interop.Types.b8
        {LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview (Buffer?.bsrc b)) % 8 == 0} ->
    heap: Vale.Arch.MachineHeap_s.machine_heap ->
    i:
      Prims.nat
        {i < LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview (Buffer?.bsrc b)) / 8} ->
    v: Vale.Def.Words_s.nat64 ->
    mem:
      Vale.Interop.Heap_s.interop_heap
        {LowStar.Monotonic.Buffer.live (Vale.Interop.Heap_s.hs_of_mem mem) (Buffer?.bsrc b)}
  -> FStar.Pervasives.Lemma (requires Vale.Interop.Heap_s.correct_down_p mem heap b)
      (ensures
        (let dv = Vale.Interop.Types.get_downview (Buffer?.bsrc b) in
          let bv = LowStar.BufferView.Up.mk_buffer dv Vale.Interop.Views.up_view64 in
          let addrs = Vale.Interop.Heap_s.addrs_of_mem mem in
          let h = Vale.Interop.Heap_s.hs_of_mem mem in
          [@@ FStar.Pervasives.inline_let ]let _ = LowStar.BufferView.Up.length_eq bv in
          let heap' = Vale.Arch.MachineHeap_s.update_heap64 (addrs b + 8 * i) v heap in
          LowStar.BufferView.Up.upd h bv i (FStar.UInt64.uint_to_t v) ==
          LowStar.BufferView.Down.upd_seq h dv (Vale.Interop.get_seq_heap heap' addrs b)))