val 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: nat) (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))))
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
  ()
val 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: nat) (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))))
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: nat) (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
  ()
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.op_Equality Prims.int Prims.bool FStar.Pervasives.Native.option Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Vale.Arch.HeapImpl.heaplet_id FStar.Set.set Prims.unit Prims.l_and Prims.l_not Prims.eq2 FStar.Set.mem FStar.Set.intersect Prims.squash Prims.l_False Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil FStar.Pervasives.reveal_opaque Vale.Interop.Types.b8 Vale.Def.Words_s.nat64 Prims.logical Vale.Interop.Types.addr_map_pred FStar.Map.domain Vale.Def.Words_s.nat8 Vale.Arch.HeapImpl.__proj__ValeHeap__item__mh Vale.Interop.addrs_set_mem FStar.Ghost.reveal Vale.Interop.Heap_s.interop_heap Vale.Arch.HeapImpl.__proj__ValeHeap__item__ih Vale.Def.Types_s.nat8 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.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 Prims.op_Subtraction Vale.PPC64LE.Memory_Sems.lemma_make_owns FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Memory_Sems.make_owns Prims.op_LessThanOrEqual Prims.l_Forall Prims.l_imp Vale.PPC64LE.Memory.buffer_readable Vale.PPC64LE.Memory.buffer_info_disjoint Prims.l_iff FStar.Option.mapTot FStar.Pervasives.Native.Some Vale.PPC64LE.Memory_Sems.buffer_info_has_addr_opt Vale.PPC64LE.Memory_Sems.buffer_info_has_addr
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))
  ))
val 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: nat) (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))))

    h: Vale.Arch.HeapImpl.vale_heap ->
    bs: FStar.Seq.Base.seq Vale.Arch.HeapImpl.buffer_info ->
    n: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        n <= FStar.Seq.Base.length bs /\
        (forall (i: Prims.nat). {:pattern FStar.Seq.Base.index bs i}
            i < FStar.Seq.Base.length bs ==>
            Vale.PPC64LE.Memory.buffer_readable h
              (Mkbuffer_info?.bi_buffer (FStar.Seq.Base.index bs i))) /\
        (forall (i1: Prims.nat) (i2: Prims.nat).
            {:pattern FStar.Seq.Base.index bs i1; FStar.Seq.Base.index bs i2}
            i1 < FStar.Seq.Base.length bs /\ i2 < FStar.Seq.Base.length bs ==>
            Vale.PPC64LE.Memory.buffer_info_disjoint (FStar.Seq.Base.index bs i1)
              (FStar.Seq.Base.index bs i2)))
      (ensures
        (let _ = Vale.PPC64LE.Memory_Sems.make_owns h bs n in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ m s = _ in
            (forall (i: Vale.Arch.HeapImpl.heaplet_id) (a: Prims.int).
                {:pattern FStar.Set.mem a (s i)}
                (FStar.Set.mem a (s i) <==>
                  FStar.Option.mapTot (fun n ->
                        Mkbuffer_info?.bi_heaplet (FStar.Seq.Base.index bs n))
                    (m a) ==
                  FStar.Pervasives.Native.Some i) /\
                (FStar.Set.mem a (s i) ==>
                  Vale.PPC64LE.Memory_Sems.buffer_info_has_addr_opt (FStar.Option.mapTot (fun n ->
                            FStar.Seq.Base.index bs n)
                        (m a))
                    a) /\
                (FStar.Set.mem a (s i) ==> FStar.Set.mem a (FStar.Map.domain (ValeHeap?.mh h)))) /\
            (forall (k: Prims.nat) (a: Prims.int).
                {:pattern
                FStar.Set.mem a (s (Mkbuffer_info?.bi_heaplet (FStar.Seq.Base.index bs k)))}
                k < n /\ Vale.PPC64LE.Memory_Sems.buffer_info_has_addr (FStar.Seq.Base.index bs k) a ==>
                FStar.Set.mem a (s (Mkbuffer_info?.bi_heaplet (FStar.Seq.Base.index bs k)))))
          <:
          Type0))