val 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))
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)
val 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))
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)
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
Vale.Arch.HeapImpl.vale_heap FStar.Seq.Base.seq Vale.Arch.HeapImpl.buffer_info Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.op_Equality Prims.int FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option Prims.op_LessThan Vale.Arch.HeapImpl.heaplet_id FStar.Set.set FStar.Pervasives.Native.None FStar.Set.empty Prims.bool Prims.op_AmpAmp Prims.op_Addition FStar.Pervasives.Native.Some Prims.op_Subtraction FStar.Set.union Vale.PPC64LE.Memory_Sems.set_of_range 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.Def.Words_s.nat64 Vale.Interop.Heap_s.global_addrs_map Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_heaplet Vale.Arch.HeapImpl.buffer Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_typ Vale.Arch.HeapImpl.__proj__Mkbuffer_info__item__bi_buffer FStar.Seq.Base.index FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Memory_Sems.make_owns_rec
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))
val 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))

    h: Vale.Arch.HeapImpl.vale_heap ->
    bs: FStar.Seq.Base.seq Vale.Arch.HeapImpl.buffer_info ->
    n: Prims.nat{n <= FStar.Seq.Base.length bs}
  -> Prims.GTot
    ((_: Prims.int -> FStar.Pervasives.Native.option (n: Prims.nat{n < FStar.Seq.Base.length bs})) *
      (_: Vale.Arch.HeapImpl.heaplet_id -> FStar.Set.set Prims.int))