val correct_down_p_frame (mem: interop_heap) (heap: machine_heap) (p: b8)
    : Lemma
    (forall p'.
        disjoint p p' /\ correct_down_p mem heap p' ==>
        (let b = get_downview p.bsrc in
          let length = DV.length b in
          let contents = DV.as_seq (hs_of_mem mem) b in
          let addr = addrs_of_mem mem p in
          let new_heap = write_vale_mem contents length addr 0 heap in
          correct_down_p mem new_heap p'))
let correct_down_p_frame (mem:interop_heap) (heap:machine_heap) (p:b8) : Lemma
  (forall p'. disjoint p p' /\ correct_down_p mem heap p' ==>
      (let b = get_downview p.bsrc in
      let length = DV.length b in
      let contents = DV.as_seq (hs_of_mem mem) b in
      let addr = addrs_of_mem mem p in
      let new_heap = write_vale_mem contents length addr 0 heap in
      correct_down_p mem new_heap p')) =
  let rec aux (p':b8) : Lemma
    (disjoint p p' /\ correct_down_p mem heap p' ==> (
      let b = get_downview p.bsrc in
      let length = DV.length b in
      let contents = DV.as_seq (hs_of_mem mem) b in
      let addr = addrs_of_mem mem p in
      let new_heap = write_vale_mem contents length addr 0 heap in
      correct_down_p mem new_heap p')) =
    let b = get_downview p.bsrc in
    let length = DV.length b in
    let contents = DV.as_seq (hs_of_mem mem) b in
    let addr = addrs_of_mem mem p in
    let new_heap = write_vale_mem contents length addr 0 heap in
    reveal_opaque (`%addr_map_pred) addr_map_pred;
    Classical.forall_intro (Classical.move_requires (frame_write_vale_mem contents length addr 0 heap))
  in
  Classical.forall_intro aux
val correct_down_p_frame (mem: interop_heap) (heap: machine_heap) (p: b8)
    : Lemma
    (forall p'.
        disjoint p p' /\ correct_down_p mem heap p' ==>
        (let b = get_downview p.bsrc in
          let length = DV.length b in
          let contents = DV.as_seq (hs_of_mem mem) b in
          let addr = addrs_of_mem mem p in
          let new_heap = write_vale_mem contents length addr 0 heap in
          correct_down_p mem new_heap p'))
let correct_down_p_frame (mem: interop_heap) (heap: machine_heap) (p: b8)
    : Lemma
    (forall p'.
        disjoint p p' /\ correct_down_p mem heap p' ==>
        (let b = get_downview p.bsrc in
          let length = DV.length b in
          let contents = DV.as_seq (hs_of_mem mem) b in
          let addr = addrs_of_mem mem p in
          let new_heap = write_vale_mem contents length addr 0 heap in
          correct_down_p mem new_heap p')) =
let rec aux (p': b8)
    : Lemma
    (disjoint p p' /\ correct_down_p mem heap p' ==>
      (let b = get_downview p.bsrc in
        let length = DV.length b in
        let contents = DV.as_seq (hs_of_mem mem) b in
        let addr = addrs_of_mem mem p in
        let new_heap = write_vale_mem contents length addr 0 heap in
        correct_down_p mem new_heap p')) =
  let b = get_downview p.bsrc in
  let length = DV.length b in
  let contents = DV.as_seq (hs_of_mem mem) b in
  let addr = addrs_of_mem mem p in
  let new_heap = write_vale_mem contents length addr 0 heap in
  reveal_opaque (`%addr_map_pred) addr_map_pred;
  Classical.forall_intro (Classical.move_requires (frame_write_vale_mem contents length addr 0 heap)
    )
in
Classical.forall_intro aux
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
Vale.Interop.Heap_s.interop_heap Vale.Arch.MachineHeap_s.machine_heap Vale.Interop.Types.b8 FStar.Classical.forall_intro Prims.l_imp Prims.l_and Vale.Interop.disjoint Vale.Interop.Heap_s.correct_down_p Vale.Interop.write_vale_mem LowStar.BufferView.Down.as_seq FStar.UInt8.t Vale.Interop.Heap_s.hs_of_mem 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 LowStar.BufferView.Down.length Vale.Interop.Heap_s.addrs_of_mem Prims.unit Prims.l_True Prims.squash Vale.Def.Words_s.nat64 FStar.Seq.Properties.lseq Prims.nat LowStar.BufferView.Down.buffer Prims.Nil FStar.Pervasives.pattern Prims.int Prims.l_or Prims.b2t Prims.op_LessThan Prims.op_GreaterThanOrEqual Prims.op_Addition Prims.eq2 Vale.Def.Types_s.nat8 Vale.Interop.op_String_Access FStar.Classical.move_requires Vale.Interop.frame_write_vale_mem FStar.Pervasives.reveal_opaque Prims.logical Vale.Interop.Types.addr_map_pred Prims.l_Forall
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))
  =
  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

let rec domain_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. Set.mem j (Map.domain new_heap) /\ not (Set.mem j (Map.domain curr_heap)) ==>
        addr <= j /\ j < addr + length))
      (decreases (length - i))=
   if i >= length then ()
   else begin
     let heap = curr_heap.[addr + i] <- UInt8.v (FStar.Seq.index contents i) in
     domain_write_vale_mem contents length addr (i+1) heap
    end

let rec domain2_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 forall j. addr <= j /\ j < addr + i ==> Set.mem j (Map.domain curr_heap))
      (ensures (let new_heap = write_vale_mem contents length addr i curr_heap in
        forall j. addr <= j /\ j < addr + length ==> Set.mem j (Map.domain new_heap)))
      (decreases (length - i))=
   if i >= length then ()
   else begin
     let heap = curr_heap.[addr + i] <- UInt8.v (FStar.Seq.index contents i) in
     domain2_write_vale_mem contents length addr (i+1) heap
    end

let rec monotone_domain_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. Set.mem j (Map.domain curr_heap) ==> Set.mem j (Map.domain new_heap)))
      (decreases (length - i))=
   if i >= length then ()
   else begin
     let heap = curr_heap.[addr + i] <- UInt8.v (FStar.Seq.index contents i) in
     monotone_domain_write_vale_mem contents length addr (i+1) heap
    end

#set-options "--z3rlimit 40"

let correct_down_p_cancel (mem:interop_heap) heap (p:b8) : Lemma
  (forall p'. p == p' ==>
      (let b = get_downview p.bsrc in
      let length = DV.length b in
      let contents = DV.as_seq (hs_of_mem mem) b in
      let addr = addrs_of_mem mem p in
      let new_heap = write_vale_mem contents length addr 0 heap in
      correct_down_p mem new_heap p')) =
  let rec aux (p':b8) : Lemma
    (p == p'  ==> (
      let b = get_downview p.bsrc in
      let length = DV.length b in
      let contents = DV.as_seq (hs_of_mem mem) b in
      let addr = addrs_of_mem mem p in
      let new_heap = write_vale_mem contents length addr 0 heap in
      correct_down_p mem new_heap p')) =
    let b = get_downview p.bsrc in
    let length = DV.length b in
    let contents = DV.as_seq (hs_of_mem mem) b in
    let addr = addrs_of_mem mem p in
    let new_heap = write_vale_mem contents length addr 0 heap in
    load_store_write_vale_mem contents length addr 0 heap
  in
  Classical.forall_intro aux

let correct_down_p_frame (mem:interop_heap) (heap:machine_heap) (p:b8) : Lemma
  (forall p'. disjoint p p' /\ correct_down_p mem heap p' ==>
      (let b = get_downview p.bsrc in
      let length = DV.length b in
      let contents = DV.as_seq (hs_of_mem mem) b in
      let addr = addrs_of_mem mem p in
val correct_down_p_frame (mem: interop_heap) (heap: machine_heap) (p: b8)
    : Lemma
    (forall p'.
        disjoint p p' /\ correct_down_p mem heap p' ==>
        (let b = get_downview p.bsrc in
          let length = DV.length b in
          let contents = DV.as_seq (hs_of_mem mem) b in
          let addr = addrs_of_mem mem p in
          let new_heap = write_vale_mem contents length addr 0 heap in
          correct_down_p mem new_heap p'))

    mem: Vale.Interop.Heap_s.interop_heap ->
    heap: Vale.Arch.MachineHeap_s.machine_heap ->
    p: Vale.Interop.Types.b8
  -> FStar.Pervasives.Lemma
    (ensures
      forall (p': Vale.Interop.Types.b8).
        Vale.Interop.disjoint p p' /\ Vale.Interop.Heap_s.correct_down_p mem heap p' ==>
        (let b = Vale.Interop.Types.get_downview (Buffer?.bsrc p) in
          let length = LowStar.BufferView.Down.length b in
          let contents = LowStar.BufferView.Down.as_seq (Vale.Interop.Heap_s.hs_of_mem mem) b in
          let addr = Vale.Interop.Heap_s.addrs_of_mem mem p in
          let new_heap = Vale.Interop.write_vale_mem contents length addr 0 heap in
          Vale.Interop.Heap_s.correct_down_p mem new_heap p'))