val addrs_ptr_lemma
      (i: nat)
      (addrs: addr_map)
      (ptr: b8{i <= DV.length (get_downview ptr.bsrc)})
      (acc: Set.set int)
      (x: int)
    : Lemma (requires True)
      (ensures
        Set.mem x (addrs_ptr i addrs ptr acc) <==>
        ((addrs ptr + i <= x /\ x < addrs ptr + DV.length (get_downview ptr.bsrc)) \/ Set.mem x acc)
      )
      (decreases (DV.length (get_downview ptr.bsrc) - i))
let rec addrs_ptr_lemma
  (i:nat)
  (addrs:addr_map)
  (ptr:b8{i <= DV.length (get_downview ptr.bsrc)})
  (acc:Set.set int)
  (x:int) : Lemma
  (requires True)
  (ensures Set.mem x (addrs_ptr i addrs ptr acc) <==>
    ((addrs ptr + i <= x /\ x < addrs ptr + DV.length (get_downview ptr.bsrc)) \/ Set.mem x acc))
  (decreases (DV.length (get_downview ptr.bsrc) - i)) =
  if i = DV.length (get_downview ptr.bsrc) then ()
  else addrs_ptr_lemma (i+1) addrs ptr (Set.union (Set.singleton (addrs ptr + i)) acc) x
val addrs_ptr_lemma
      (i: nat)
      (addrs: addr_map)
      (ptr: b8{i <= DV.length (get_downview ptr.bsrc)})
      (acc: Set.set int)
      (x: int)
    : Lemma (requires True)
      (ensures
        Set.mem x (addrs_ptr i addrs ptr acc) <==>
        ((addrs ptr + i <= x /\ x < addrs ptr + DV.length (get_downview ptr.bsrc)) \/ Set.mem x acc)
      )
      (decreases (DV.length (get_downview ptr.bsrc) - i))
let rec addrs_ptr_lemma
      (i: nat)
      (addrs: addr_map)
      (ptr: b8{i <= DV.length (get_downview ptr.bsrc)})
      (acc: Set.set int)
      (x: int)
    : Lemma (requires True)
      (ensures
        Set.mem x (addrs_ptr i addrs ptr acc) <==>
        ((addrs ptr + i <= x /\ x < addrs ptr + DV.length (get_downview ptr.bsrc)) \/ Set.mem x acc)
      )
      (decreases (DV.length (get_downview ptr.bsrc) - i)) =
if i = DV.length (get_downview ptr.bsrc)
then ()
else addrs_ptr_lemma (i + 1) addrs ptr (Set.union (Set.singleton (addrs ptr + i)) acc) x
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
Prims.nat Vale.Interop.Types.addr_map Vale.Interop.Types.b8 Prims.b2t Prims.op_LessThanOrEqual 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 FStar.Set.set Prims.int Prims.op_Equality Prims.bool Vale.Interop.addrs_ptr_lemma Prims.op_Addition FStar.Set.union FStar.Set.singleton Prims.unit Prims.l_True Prims.squash Prims.l_iff FStar.Set.mem Vale.Interop.Heap_s.addrs_ptr Prims.l_or Prims.l_and Prims.op_LessThan 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))
  =
  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
      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

let rec addrs_ptr_lemma
  (i:nat)
  (addrs:addr_map)
  (ptr:b8{i <= DV.length (get_downview ptr.bsrc)})
  (acc:Set.set int)
  (x:int) : Lemma
  (requires True)
  (ensures Set.mem x (addrs_ptr i addrs ptr acc) <==>
    ((addrs ptr + i <= x /\ x < addrs ptr + DV.length (get_downview ptr.bsrc)) \/ Set.mem x acc))
val addrs_ptr_lemma
      (i: nat)
      (addrs: addr_map)
      (ptr: b8{i <= DV.length (get_downview ptr.bsrc)})
      (acc: Set.set int)
      (x: int)
    : Lemma (requires True)
      (ensures
        Set.mem x (addrs_ptr i addrs ptr acc) <==>
        ((addrs ptr + i <= x /\ x < addrs ptr + DV.length (get_downview ptr.bsrc)) \/ Set.mem x acc)
      )
      (decreases (DV.length (get_downview ptr.bsrc) - i))

    i: Prims.nat ->
    addrs: Vale.Interop.Types.addr_map ->
    ptr:
      Vale.Interop.Types.b8
        {i <= LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview (Buffer?.bsrc ptr))} ->
    acc: FStar.Set.set Prims.int ->
    x: Prims.int
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Set.mem x (Vale.Interop.Heap_s.addrs_ptr i addrs ptr acc) <==>
        addrs ptr + i <= x /\
        x <
        addrs ptr +
        LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview (Buffer?.bsrc ptr)) \/
        FStar.Set.mem x acc)
      (decreases
        LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview (Buffer?.bsrc ptr)) - i)