val lemma_loc_mutable_buffers (l: list buffer_info)
    : Lemma
    (ensures
      (let s = list_to_seq l in
        forall (i: nat). {:pattern Seq.index s i}
          i < Seq.length s ==>
          (let bi = Seq.index s i in
            bi.bi_mutable == Mutable ==>
            loc_includes (loc_mutable_buffers l) (loc_buffer bi.bi_buffer))))
let lemma_loc_mutable_buffers (l:list buffer_info) : Lemma
  (ensures (
    let s = list_to_seq l in
    forall (i:nat).{:pattern Seq.index s i} i < Seq.length s ==> (
      let bi = Seq.index s i in
      bi.bi_mutable == Mutable ==> loc_includes (loc_mutable_buffers l) (loc_buffer bi.bi_buffer))
  ))
  =
  lemma_list_to_seq l;
  lemma_loc_mutable_buffers_rec l (list_to_seq l) 0
val lemma_loc_mutable_buffers (l: list buffer_info)
    : Lemma
    (ensures
      (let s = list_to_seq l in
        forall (i: nat). {:pattern Seq.index s i}
          i < Seq.length s ==>
          (let bi = Seq.index s i in
            bi.bi_mutable == Mutable ==>
            loc_includes (loc_mutable_buffers l) (loc_buffer bi.bi_buffer))))
let lemma_loc_mutable_buffers (l: list buffer_info)
    : Lemma
    (ensures
      (let s = list_to_seq l in
        forall (i: nat). {:pattern Seq.index s i}
          i < Seq.length s ==>
          (let bi = Seq.index s i in
            bi.bi_mutable == Mutable ==>
            loc_includes (loc_mutable_buffers l) (loc_buffer bi.bi_buffer)))) =
lemma_list_to_seq l;
lemma_loc_mutable_buffers_rec l (list_to_seq l) 0
Vale.PPC64LE.Memory_Sems.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.BufferViewStore.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Heap_s.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.MachineHeap.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Memory_Sems.fst
Prims.list Vale.Arch.HeapImpl.buffer_info Vale.PPC64LE.Memory_Sems.lemma_loc_mutable_buffers_rec Vale.Lib.Seqs.list_to_seq Prims.unit Vale.Lib.Seqs.lemma_list_to_seq Prims.l_True Prims.squash Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.eq2 Vale.Arch.HeapImpl.mutability Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_mutable Vale.Arch.HeapImpl.Mutable Vale.PPC64LE.Memory.loc_includes Vale.PPC64LE.Memory.loc_mutable_buffers Vale.PPC64LE.Memory.loc_buffer Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_typ Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_buffer FStar.Seq.Base.index FStar.Seq.Base.seq Prims.Nil FStar.Pervasives.pattern
module Vale.PPC64LE.Memory_Sems

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.Def.Words_s
module I = Vale.Interop
module S = Vale.PPC64LE.Semantics_s
module MB = LowStar.Monotonic.Buffer
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
open Vale.Arch.HeapImpl
open Vale.Arch.Heap

friend Vale.PPC64LE.Memory
module IB = Vale.Interop.Base

let same_domain h m = Set.equal (IB.addrs_set (_ih h)) (Map.domain m)

let lemma_same_domains h m1 m2 = ()

let get_heap h = I.down_mem (_ih h)

let upd_heap h m = mi_heap_upd h m

//let lemma_upd_get_heap h = I.down_up_identity (_ih h)

let lemma_get_upd_heap h m = I.up_down_identity (_ih h) m

let lemma_heap_impl = ()

let lemma_heap_get_heap h = ()

let lemma_heap_taint h = ()

//let lemma_heap_upd_heap h mh mt = ()

[@"opaque_to_smt"]
let rec set_of_range (a:int) (n:nat) : Pure (Set.set int)
  (requires True)
  (ensures fun s -> (forall (i:int).{:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n))
  =
  if n = 0 then Set.empty else Set.union (set_of_range a (n - 1)) (Set.singleton (a + n - 1))

let buffer_info_has_addr (bi:buffer_info) (a:int) =
  let b = bi.bi_buffer in
  let addr = Vale.Interop.Heap_s.global_addrs_map b in
  let len = DV.length (get_downview b.bsrc) in
  addr <= a /\ a < addr + len

let buffer_info_has_addr_opt (bi:option buffer_info) (a:int) =
  match bi with
  | None -> False
  | Some bi -> buffer_info_has_addr bi a

#set-options "--z3rlimit 100"
let rec make_owns_rec (h:vale_heap) (bs:Seq.seq buffer_info) (n:nat{n <= Seq.length bs}) :
  GTot ((int -> option (n:nat{n < Seq.length bs})) & (heaplet_id -> Set.set int))
  =
  if n = 0 then ((fun _ -> None), (fun _ -> Set.empty)) else
  let (m0, s0) = make_owns_rec h bs (n - 1) in
  let bi = Seq.index bs (n - 1) in
  let b = bi.bi_buffer in
  let hi = bi.bi_heaplet in
  let addr = Vale.Interop.Heap_s.global_addrs_map b in
  let len = DV.length (get_downview b.bsrc) in
  let s_b = set_of_range addr len in
  let s i = if i = hi then Set.union (s0 i) s_b else s0 i in
  let m a = if addr <= a && a < addr + len then Some (n - 1) else m0 a in
  (m, s)

[@"opaque_to_smt"]
let make_owns (h:vale_heap) (bs:Seq.seq buffer_info) (n:nat{n <= Seq.length bs}) :
  GTot ((int -> option (n:nat{n < Seq.length bs})) & (heaplet_id -> Set.set int))
  =
  make_owns_rec h bs n

let rec lemma_make_owns (h:vale_heap) (bs:Seq.seq buffer_info) (n:nat) : Lemma
  (requires
    n <= Seq.length bs /\
    (forall (i:nat).{:pattern Seq.index bs i} i < Seq.length bs ==> buffer_readable h (Seq.index bs i).bi_buffer) /\
    (forall (i1 i2:nat).{:pattern (Seq.index bs i1); (Seq.index bs i2)}
      i1 < Seq.length bs /\ i2 < Seq.length bs ==> buffer_info_disjoint (Seq.index bs i1) (Seq.index bs i2))
  )
  (ensures (
    let (m, s) = make_owns h bs n in
    (forall (i:heaplet_id) (a:int).{:pattern Set.mem a (s i)}
      (Set.mem a (s i) <==> Option.mapTot (fun n -> (Seq.index bs n).bi_heaplet) (m a) == Some i) /\
      (Set.mem a (s i) ==> buffer_info_has_addr_opt (Option.mapTot (fun n -> Seq.index bs n) (m a)) a) /\
      (Set.mem a (s i) ==> Set.mem a (Map.domain h.mh))
    ) /\
    (forall (k:nat) (a:int).{:pattern Set.mem a (s (Seq.index bs k).bi_heaplet)}
      k < n /\ buffer_info_has_addr (Seq.index bs k) a ==> Set.mem a (s (Seq.index bs k).bi_heaplet))
  ))
  =
  reveal_opaque (`%make_owns) make_owns;
  if n = 0 then () else
  let _ = make_owns h bs (n - 1) in
  let (m, s) = make_owns h bs n in
  lemma_make_owns h bs (n - 1);
  let bi = Seq.index bs (n - 1) in
  let b = bi.bi_buffer in
  let hi = bi.bi_heaplet in
  let addr = Vale.Interop.Heap_s.global_addrs_map b in
  let len = DV.length (get_downview b.bsrc) in
  let s_b = set_of_range addr len in
  let lem1 (a:int) : Lemma
    (requires Set.mem a s_b)
    (ensures Set.mem a (Map.domain h.mh))
    [SMTPat (Set.mem a (Map.domain h.mh))]
    =
    I.addrs_set_mem h.ih b a
    in
  let lem2 (i:heaplet_id) (a:int) : Lemma
    (requires i =!= hi /\ Set.mem a (Set.intersect s_b (s i)))
    (ensures False)
    [SMTPat (Set.mem a (s i))]
    =
    reveal_opaque (`%addr_map_pred) addr_map_pred
    in
  ()

#push-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 2 --max_ifuel 2"
let rec lemma_loc_mutable_buffers_rec (l:list buffer_info) (s:Seq.seq buffer_info) (n:nat) : Lemma
  (requires
    n + List.length l == Seq.length s /\
    list_to_seq_post l s n
  )
  (ensures (
    let modloc = loc_mutable_buffers l in
    forall (i:nat).{:pattern Seq.index s i} n <= i /\ i < Seq.length s ==> (
      let bi = Seq.index s i in
      bi.bi_mutable == Mutable ==> loc_includes modloc (loc_buffer bi.bi_buffer))
  ))
  (decreases l)
  =
  match l with
  | [] -> ()
  | h::t -> lemma_loc_mutable_buffers_rec t s (n + 1)
#pop-options

let lemma_loc_mutable_buffers (l:list buffer_info) : Lemma
  (ensures (
    let s = list_to_seq l in
    forall (i:nat).{:pattern Seq.index s i} i < Seq.length s ==> (
      let bi = Seq.index s i in
      bi.bi_mutable == Mutable ==> loc_includes (loc_mutable_buffers l) (loc_buffer bi.bi_buffer))
  ))
val lemma_loc_mutable_buffers (l: list buffer_info)
    : Lemma
    (ensures
      (let s = list_to_seq l in
        forall (i: nat). {:pattern Seq.index s i}
          i < Seq.length s ==>
          (let bi = Seq.index s i in
            bi.bi_mutable == Mutable ==>
            loc_includes (loc_mutable_buffers l) (loc_buffer bi.bi_buffer))))
l: Prims.list Vale.Arch.HeapImpl.buffer_info
  -> FStar.Pervasives.Lemma
    (ensures
      (let s = Vale.Lib.Seqs.list_to_seq l in
        forall (i: Prims.nat). {:pattern FStar.Seq.Base.index s i}
          i < FStar.Seq.Base.length s ==>
          (let bi = FStar.Seq.Base.index s i in
            Mkbuffer_info?.bi_mutable bi == Vale.Arch.HeapImpl.Mutable ==>
            Vale.PPC64LE.Memory.loc_includes (Vale.PPC64LE.Memory.loc_mutable_buffers l)
              (Vale.PPC64LE.Memory.loc_buffer (Mkbuffer_info?.bi_buffer bi)))))