val load_store_write_vale_mem
      (contents: Seq.seq UInt8.t)
      (length: nat{length = FStar.Seq.Base.length contents})
      (addr: _)
      (i: nat{i <= length})
      (curr_heap:
          machine_heap
            { forall j. {:pattern (Seq.index contents j)}
                0 <= j /\ j < i ==> curr_heap.[ addr + j ] == UInt8.v (Seq.index contents j) })
    : Lemma (requires True)
      (ensures
        (let new_heap = write_vale_mem contents length addr i curr_heap in
          forall j. 0 <= j /\ j < length ==> UInt8.v (Seq.index contents j) == new_heap.[ addr + j ]
        ))
      (decreases (length - i))
let rec load_store_write_vale_mem
  (contents:Seq.seq UInt8.t)
  (length:nat{length = FStar.Seq.Base.length contents})
  addr
  (i:nat{i <= length})
  (curr_heap:machine_heap{forall j. {:pattern (Seq.index contents j)} 0 <= j /\ j < i ==>
    curr_heap.[addr + j] == UInt8.v (Seq.index contents j)})
  : Lemma
    (requires True)
    (ensures (let new_heap = write_vale_mem contents length addr i curr_heap in
    forall j. 0 <= j /\ j < length ==> UInt8.v (Seq.index contents j) == new_heap.[addr + j]))
    (decreases (length - i))
  =
  if i >= length then ()
  else begin
    let heap = curr_heap.[addr + i] <- UInt8.v (FStar.Seq.index contents i) in
    load_store_write_vale_mem contents length addr (i+1) heap
  end
val load_store_write_vale_mem
      (contents: Seq.seq UInt8.t)
      (length: nat{length = FStar.Seq.Base.length contents})
      (addr: _)
      (i: nat{i <= length})
      (curr_heap:
          machine_heap
            { forall j. {:pattern (Seq.index contents j)}
                0 <= j /\ j < i ==> curr_heap.[ addr + j ] == UInt8.v (Seq.index contents j) })
    : Lemma (requires True)
      (ensures
        (let new_heap = write_vale_mem contents length addr i curr_heap in
          forall j. 0 <= j /\ j < length ==> UInt8.v (Seq.index contents j) == new_heap.[ addr + j ]
        ))
      (decreases (length - i))
let rec load_store_write_vale_mem
      (contents: Seq.seq UInt8.t)
      (length: nat{length = FStar.Seq.Base.length contents})
      addr
      (i: nat{i <= length})
      (curr_heap:
          machine_heap
            { forall j. {:pattern (Seq.index contents j)}
                0 <= j /\ j < i ==> curr_heap.[ addr + j ] == UInt8.v (Seq.index contents j) })
    : Lemma (requires True)
      (ensures
        (let new_heap = write_vale_mem contents length addr i curr_heap in
          forall j. 0 <= j /\ j < length ==> UInt8.v (Seq.index contents j) == new_heap.[ addr + j ]
        ))
      (decreases (length - i)) =
if i >= length
then ()
else
  let heap = curr_heap.[ addr + i ] <- UInt8.v (FStar.Seq.index contents i) in
  load_store_write_vale_mem contents length addr (i + 1) heap
Vale.Interop.fst.checked
Vale.Lib.BufferViewHelpers.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Modifies.fst.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.Set.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.HyperStack.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.Base.fst.checked FStar.Classical.fsti.checked
Vale.Interop.fst
FStar.Seq.Base.seq FStar.UInt8.t Prims.nat Prims.b2t Prims.op_Equality FStar.Seq.Base.length Prims.int Prims.op_LessThanOrEqual Vale.Arch.MachineHeap_s.machine_heap Prims.l_Forall Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_LessThan Prims.l_imp Prims.eq2 Prims.l_or FStar.UInt.size FStar.UInt8.n Vale.Def.Words_s.pow2_8 Vale.Interop.op_String_Access Vale.Def.Types_s.nat8 Prims.op_Addition FStar.UInt8.v FStar.Seq.Base.index Prims.bool Vale.Interop.load_store_write_vale_mem FStar.Map.t Vale.Def.Words_s.nat8 Vale.Interop.op_String_Assignment Prims.unit Prims.l_True Prims.squash Vale.Interop.write_vale_mem Prims.Nil FStar.Pervasives.pattern
module Vale.Interop
open FStar.Mul

module List = FStar.List.Tot.Base
module HS = FStar.Monotonic.HyperStack
module HH = FStar.Monotonic.HyperHeap
module MB = LowStar.Monotonic.Buffer
module M = LowStar.Modifies
module DV = LowStar.BufferView.Down

open Vale.Def.Opaque_s
//open Vale.Interop.Base
open Vale.Lib.BufferViewHelpers

#reset-options "--max_fuel 2 --initial_fuel 2 --max_ifuel 1 --initial_ifuel 1"

(* Write a buffer in the vale memory *)

let rec write_vale_mem (contents:Seq.seq UInt8.t) (length:nat{length = FStar.Seq.Base.length contents}) addr (i:nat{i <= length})
      (curr_heap:machine_heap{forall j. {:pattern (Seq.index contents j)}
        0 <= j /\ j < i ==> curr_heap.[addr+j] == UInt8.v (Seq.index contents j)})
  : Tot machine_heap (decreases (length - i)) =
  if i >= length then curr_heap
  else (
    let heap = curr_heap.[addr + i] <- UInt8.v (FStar.Seq.index contents i) in
    write_vale_mem contents length addr (i+1) heap
  )

let rec frame_write_vale_mem
  (contents:Seq.seq UInt8.t)
  (length:nat{length = FStar.Seq.Base.length contents})
  addr
  (i:nat{i <= length})
  (curr_heap:machine_heap{forall j. {:pattern (Seq.index contents j)}
    0 <= j /\ j < i ==> curr_heap.[addr + j] == UInt8.v (Seq.index contents j)})
  (j:int) : Lemma
  (requires j < addr \/ j >= addr + length)
  (ensures (let new_heap = write_vale_mem contents length addr i curr_heap in
      curr_heap.[j] == new_heap.[j]))
  (decreases (length - i))=
    if i >= length then ()
    else (
      let heap = curr_heap.[addr + i] <- UInt8.v (FStar.Seq.index contents i) in
      frame_write_vale_mem contents length addr (i+1) heap j
    )

let rec load_store_write_vale_mem
  (contents:Seq.seq UInt8.t)
  (length:nat{length = FStar.Seq.Base.length contents})
  addr
  (i:nat{i <= length})
  (curr_heap:machine_heap{forall j. {:pattern (Seq.index contents j)} 0 <= j /\ j < i ==>
    curr_heap.[addr + j] == UInt8.v (Seq.index contents j)})
  : Lemma
    (requires True)
    (ensures (let new_heap = write_vale_mem contents length addr i curr_heap in
    forall j. 0 <= j /\ j < length ==> UInt8.v (Seq.index contents j) == new_heap.[addr + j]))
    (decreases (length - i))
val load_store_write_vale_mem
      (contents: Seq.seq UInt8.t)
      (length: nat{length = FStar.Seq.Base.length contents})
      (addr: _)
      (i: nat{i <= length})
      (curr_heap:
          machine_heap
            { forall j. {:pattern (Seq.index contents j)}
                0 <= j /\ j < i ==> curr_heap.[ addr + j ] == UInt8.v (Seq.index contents j) })
    : Lemma (requires True)
      (ensures
        (let new_heap = write_vale_mem contents length addr i curr_heap in
          forall j. 0 <= j /\ j < length ==> UInt8.v (Seq.index contents j) == new_heap.[ addr + j ]
        ))
      (decreases (length - i))

    contents: FStar.Seq.Base.seq FStar.UInt8.t ->
    length: Prims.nat{length = FStar.Seq.Base.length contents} ->
    addr: Prims.int ->
    i: Prims.nat{i <= length} ->
    curr_heap:
      Vale.Arch.MachineHeap_s.machine_heap
        { forall (j: i: Prims.int{i >= 0 /\ i < FStar.Seq.Base.length contents}).
            {:pattern FStar.Seq.Base.index contents j}
            0 <= j /\ j < i ==>
            curr_heap.[ addr + j ] == FStar.UInt8.v (FStar.Seq.Base.index contents j) }
  -> FStar.Pervasives.Lemma
      (ensures
        (let new_heap = Vale.Interop.write_vale_mem contents length addr i curr_heap in
          forall (j: i: Prims.int{i >= 0 /\ i < FStar.Seq.Base.length contents}).
            0 <= j /\ j < length ==>
            FStar.UInt8.v (FStar.Seq.Base.index contents j) == new_heap.[ addr + j ]))
      (decreases length - i)