val written_buffer_down64
      (b: buffer64{buffer_writeable b})
      (i: nat{i < buffer_length b})
      (v: nat64)
      (h: vale_heap)
    : Lemma (requires List.memP b (IB.ptrs_of_mem (_ih h)))
      (ensures
        (let mem1 = I.down_mem (_ih h) in
          let h1 = buffer_write b i v h in
          let mem2 = I.down_mem (_ih h1) in
          let base = buffer_addr b h in
          let n = buffer_length b in
          forall j. {:pattern (mem1.[ j ])\/(mem2.[ j ])}
            (base <= j /\ j < base + scale8 i) \/
            (base + scale8 (i + 1) <= j /\ j < base + scale8 n) ==>
            mem1.[ j ] == mem2.[ j ]))
let written_buffer_down64 (b:buffer64{buffer_writeable b}) (i:nat{i < buffer_length b}) (v:nat64) (h:vale_heap)
  : Lemma
      (requires List.memP b (IB.ptrs_of_mem (_ih h)))
      (ensures (
          let mem1 = I.down_mem (_ih h) in
          let h1 = buffer_write b i v h in
          let mem2 = I.down_mem (_ih h1) in
          let base = buffer_addr b h in
          let n = buffer_length b in
          forall j. {:pattern (mem1.[j]) \/ (mem2.[j])}
               (base <= j /\ j < base + scale8 i) \/
               (base + scale8 (i+1) <= j /\ j < base + scale8 n) ==>
               mem1.[j] == mem2.[j]))
  = let mem1 = I.down_mem (_ih h) in
    let h1 = buffer_write b i v h in
    let mem2 = I.down_mem (_ih h1) in
    let base = buffer_addr b h in
    let n = buffer_length b in
    written_buffer_down64_aux1 b i v h base 0 h1 mem1 mem2;
    written_buffer_down64_aux2 b i v h base n (i+1) h1 mem1 mem2
val written_buffer_down64
      (b: buffer64{buffer_writeable b})
      (i: nat{i < buffer_length b})
      (v: nat64)
      (h: vale_heap)
    : Lemma (requires List.memP b (IB.ptrs_of_mem (_ih h)))
      (ensures
        (let mem1 = I.down_mem (_ih h) in
          let h1 = buffer_write b i v h in
          let mem2 = I.down_mem (_ih h1) in
          let base = buffer_addr b h in
          let n = buffer_length b in
          forall j. {:pattern (mem1.[ j ])\/(mem2.[ j ])}
            (base <= j /\ j < base + scale8 i) \/
            (base + scale8 (i + 1) <= j /\ j < base + scale8 n) ==>
            mem1.[ j ] == mem2.[ j ]))
let written_buffer_down64
      (b: buffer64{buffer_writeable b})
      (i: nat{i < buffer_length b})
      (v: nat64)
      (h: vale_heap)
    : Lemma (requires List.memP b (IB.ptrs_of_mem (_ih h)))
      (ensures
        (let mem1 = I.down_mem (_ih h) in
          let h1 = buffer_write b i v h in
          let mem2 = I.down_mem (_ih h1) in
          let base = buffer_addr b h in
          let n = buffer_length b in
          forall j. {:pattern (mem1.[ j ])\/(mem2.[ j ])}
            (base <= j /\ j < base + scale8 i) \/
            (base + scale8 (i + 1) <= j /\ j < base + scale8 n) ==>
            mem1.[ j ] == mem2.[ j ])) =
let mem1 = I.down_mem (_ih h) in
let h1 = buffer_write b i v h in
let mem2 = I.down_mem (_ih h1) in
let base = buffer_addr b h in
let n = buffer_length b in
written_buffer_down64_aux1 b i v h base 0 h1 mem1 mem2;
written_buffer_down64_aux2 b i v h base n (i + 1) h1 mem1 mem2
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.PPC64LE.Memory.buffer64 Vale.PPC64LE.Memory.buffer_writeable Vale.PPC64LE.Memory.vuint64 Prims.nat Prims.b2t Prims.op_LessThan Vale.PPC64LE.Memory.buffer_length Vale.Def.Words_s.nat64 Vale.Arch.HeapImpl.vale_heap Vale.PPC64LE.Memory_Sems.written_buffer_down64_aux2 Prims.op_Addition Prims.unit Vale.PPC64LE.Memory_Sems.written_buffer_down64_aux1 Prims.int Vale.PPC64LE.Memory.buffer_addr Vale.Arch.MachineHeap_s.machine_heap Vale.Interop.Heap_s.correct_down Vale.Arch.HeapImpl._ih Vale.Interop.down_mem Vale.PPC64LE.Memory.buffer_write FStar.List.Tot.Base.memP Vale.Interop.Types.b8 Vale.Interop.Heap_s.ptrs_of_mem Prims.squash Prims.l_Forall Prims.l_imp Prims.l_or Prims.l_and Prims.op_LessThanOrEqual Vale.PPC64LE.Memory.scale8 Prims.eq2 Vale.Def.Types_s.nat8 Vale.PPC64LE.Memory.op_String_Access 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))
  ))
  =
  lemma_list_to_seq l;
  lemma_loc_mutable_buffers_rec l (list_to_seq l) 0

let create_heaplets buffers h1 =
  let bs = list_to_seq buffers in
  let modloc = loc_mutable_buffers buffers in
  let layout1 = h1.vf_layout in
  let layin1 = layout1.vl_inner in
  let (hmap, hsets) = make_owns h1.vf_heap bs (Seq.length bs) in
  let hmap a = Option.mapTot (fun n -> (Seq.index bs n).bi_heaplet) (hmap a) in
  let l = {
    vl_heaplets_initialized = true;
    vl_heaplet_map = hmap;
    vl_heaplet_sets = hsets;
    vl_old_heap = h1.vf_heap;
    vl_buffers = bs;
    vl_mod_loc = modloc;
  } in
  let layout2 = {layout1 with vl_inner = l} in
  let h2 = {
    vf_layout = layout2;
    vf_heap = h1.vf_heap;
    vf_heaplets = h1.vf_heaplets;
  } in
  h2

let lemma_create_heaplets buffers h1 =
  let bs = list_to_seq buffers in
  let h2 = create_heaplets buffers h1 in
  assert (h2.vf_layout.vl_inner.vl_buffers == bs); // REVIEW: why is this necessary, even with extra ifuel?
  lemma_make_owns h1.vf_heap bs (Seq.length bs);
  lemma_loc_mutable_buffers buffers;
  reveal_opaque (`%valid_layout_buffer_id) valid_layout_buffer_id;
  ()

let destroy_heaplets h1 =
  h1

let lemma_destroy_heaplets h1 =
  ()

val heap_shift (m1 m2:S.machine_heap) (base:int) (n:nat) : Lemma
  (requires (forall i. 0 <= i /\ i < n ==> m1.[base + i] == m2.[base + i]))
  (ensures (forall i. {:pattern (m1.[i])} base <= i /\ i < base + n ==> m1.[i] == m2.[i]))

#push-options "--smtencoding.l_arith_repr boxwrap"
let heap_shift m1 m2 base n =
  assert (forall i. base <= i /\ i < base + n ==>
    m1.[base + (i - base)] == m2.[base + (i - base)])
#pop-options

val same_mem_eq_slices64 (b:buffer64{buffer_writeable b})
                       (i:nat{i < buffer_length b})
                       (v:nat64)
                       (k:nat{k < buffer_length b})
                       (h1:vale_heap{List.memP b (IB.ptrs_of_mem (_ih h1))})
                       (h2:vale_heap{h2 == buffer_write b i v h1})
                       (mem1:S.machine_heap{IB.correct_down_p (_ih h1) mem1 b})
                       (mem2:S.machine_heap{IB.correct_down_p (_ih h2) mem2 b}) : Lemma
  (requires (Seq.index (buffer_as_seq h1 b) k == Seq.index (buffer_as_seq h2 b) k))
  (ensures (
    k * 8 + 8 <= DV.length (get_downview b.bsrc) /\
    Seq.slice (DV.as_seq (IB.hs_of_mem (_ih h1)) (get_downview b.bsrc)) (k * 8) (k * 8 + 8) ==
    Seq.slice (DV.as_seq (IB.hs_of_mem (_ih h2)) (get_downview b.bsrc)) (k * 8) (k * 8 + 8)))

let same_mem_eq_slices64 b i v k h1 h2 mem1 mem2 =
    let t = TUInt64 in
    let db = get_downview b.bsrc in
    let ub = UV.mk_buffer db (uint_view t) in
    UV.as_seq_sel (IB.hs_of_mem (_ih h1)) ub k;
    UV.as_seq_sel (IB.hs_of_mem (_ih h2)) ub k;
    UV.put_sel (IB.hs_of_mem (_ih h1)) ub k;
    UV.put_sel (IB.hs_of_mem (_ih h2)) ub k;
    UV.length_eq ub

let length_up64 (b:buffer64) (h:vale_heap) (k:nat{k < buffer_length b}) (i:nat{i < 8}) : Lemma
  (scale8 k + i <= DV.length (get_downview b.bsrc)) =
  let vb = UV.mk_buffer (get_downview b.bsrc) uint64_view in
  UV.length_eq vb

val same_mem_get_heap_val64 (b:buffer64{buffer_writeable b})
                          (i:nat{i < buffer_length b})
                          (v:nat64)
                          (k:nat{k < buffer_length b})
                          (h1:vale_heap{List.memP b (IB.ptrs_of_mem (_ih h1))})
                          (h2:vale_heap{h2 == buffer_write b i v h1})
                          (mem1:S.machine_heap{IB.correct_down_p (_ih h1) mem1 b})
                          (mem2:S.machine_heap{IB.correct_down_p (_ih h2) mem2 b}) : Lemma
  (requires (Seq.index (buffer_as_seq h1 b) k == Seq.index (buffer_as_seq h2 b) k))
  (ensures (let ptr = buffer_addr b h1 + scale8 k in
    forall (x:int).{:pattern (mem1.[x])} ptr <= x /\ x < ptr + 8 ==> mem1.[x] == mem2.[x]))

let same_mem_get_heap_val64 b j v k h1 h2 mem1 mem2 =
  let ptr = buffer_addr b h1 + scale8 k in
  let addr = buffer_addr b h1 in
  let aux (x:int{ptr <= x /\ x < ptr + 8}) : Lemma (mem1.[x] == mem2.[x]) =
    let i = x - ptr in
    let db = get_downview b.bsrc in
    let ub = UV.mk_buffer db uint64_view in
    UV.as_seq_sel (IB.hs_of_mem (_ih h1)) ub k;
    UV.as_seq_sel (IB.hs_of_mem (_ih h2)) ub k;
    same_mem_eq_slices64 b j v k h1 h2 mem1 mem2;
    let s1 = (Seq.slice (DV.as_seq (IB.hs_of_mem (_ih h1)) db) (k * 8) (k * 8 + 8)) in
    let s2 = (Seq.slice (DV.as_seq (IB.hs_of_mem (_ih h2)) db) (k * 8) (k * 8 + 8)) in
    assert (Seq.index s1 i == Seq.index (DV.as_seq (IB.hs_of_mem (_ih h1)) db) (k * 8 + i));
    length_up64 b h1 k i;
    assert (mem1.[addr+(scale8 k + i)] == UInt8.v (Seq.index (DV.as_seq (IB.hs_of_mem (_ih h1)) db) (k * 8 + i)));
    assert (Seq.index s2 i == Seq.index (DV.as_seq (IB.hs_of_mem (_ih h2)) db) (k * 8 + i));
    length_up64 b h2 k i;
    assert (mem2.[addr+(scale8 k + i)] == UInt8.v (Seq.index (DV.as_seq (IB.hs_of_mem (_ih h2)) db) (k * 8 + i)))
  in
  Classical.forall_intro aux;
  assert (forall i. addr + (scale8 k + i) == ptr + i)

let rec written_buffer_down64_aux1
  (b:buffer64{buffer_writeable b})
  (i:nat{i < buffer_length b})
  (v:nat64)
  (h:vale_heap{List.memP b (IB.ptrs_of_mem (_ih h))})
  (base:nat{base == buffer_addr b h})
  (k:nat) (h1:vale_heap{h1 == buffer_write b i v h})
  (mem1:S.machine_heap{IB.correct_down (_ih h) mem1})
  (mem2:S.machine_heap{IB.correct_down (_ih h1) mem2 /\
               (forall j.{:pattern (mem1.[j]) \/ (mem2.[j])}
                 base <= j /\ j < base + k * 8 ==>
                 mem1.[j] == mem2.[j])})
  : Lemma
      (ensures (forall j. {:pattern (mem1.[j]) \/ (mem1.[j])}
                  j >= base /\ j < base + scale8 i ==>
                  mem1.[j] == mem2.[j]))
      (decreases %[i-k]) =
    if k >= i then ()
    else begin
      let ptr = base + scale8 k in
      same_mem_get_heap_val64 b i v k h h1 mem1 mem2;
      heap_shift mem1 mem2 ptr 8;
      written_buffer_down64_aux1 b i v h base (k+1) h1 mem1 mem2
    end

let rec written_buffer_down64_aux2
  (b:buffer64{buffer_writeable b})
  (i:nat{i < buffer_length b})
  (v:nat64)
  (h:vale_heap{List.memP b (IB.ptrs_of_mem (_ih h))})
  (base:nat{base == buffer_addr b h})
  (n:nat{n == buffer_length b})
  (k:nat{k > i}) (h1:vale_heap{h1 == buffer_write b i v h})
  (mem1:S.machine_heap{IB.correct_down (_ih h) mem1})
  (mem2:S.machine_heap{IB.correct_down (_ih h1) mem2 /\
               (forall j. {:pattern (mem1.[j]) \/ (mem2.[j])}
                 base + scale8 (i+1) <= j /\ j < base + k * 8 ==>
                 mem1.[j] == mem2.[j])})
  : Lemma
      (ensures (forall j. {:pattern (mem1.[j]) \/ (mem2.[j])}
                     j >= base + scale8 (i+1) /\ j < base + scale8 n ==>
                     mem1.[j] == mem2.[j]))
      (decreases %[n-k]) =
    if k >= n then ()
    else begin
      let ptr = base + scale8 k in
      same_mem_get_heap_val64 b i v k h h1 mem1 mem2;
      heap_shift mem1 mem2 ptr 8;
      written_buffer_down64_aux2 b i v h base n (k+1) h1 mem1 mem2
    end

let written_buffer_down64 (b:buffer64{buffer_writeable b}) (i:nat{i < buffer_length b}) (v:nat64) (h:vale_heap)
  : Lemma
      (requires List.memP b (IB.ptrs_of_mem (_ih h)))
      (ensures (
          let mem1 = I.down_mem (_ih h) in
          let h1 = buffer_write b i v h in
          let mem2 = I.down_mem (_ih h1) in
          let base = buffer_addr b h in
          let n = buffer_length b in
          forall j. {:pattern (mem1.[j]) \/ (mem2.[j])}
               (base <= j /\ j < base + scale8 i) \/
               (base + scale8 (i+1) <= j /\ j < base + scale8 n) ==>
val written_buffer_down64
      (b: buffer64{buffer_writeable b})
      (i: nat{i < buffer_length b})
      (v: nat64)
      (h: vale_heap)
    : Lemma (requires List.memP b (IB.ptrs_of_mem (_ih h)))
      (ensures
        (let mem1 = I.down_mem (_ih h) in
          let h1 = buffer_write b i v h in
          let mem2 = I.down_mem (_ih h1) in
          let base = buffer_addr b h in
          let n = buffer_length b in
          forall j. {:pattern (mem1.[ j ])\/(mem2.[ j ])}
            (base <= j /\ j < base + scale8 i) \/
            (base + scale8 (i + 1) <= j /\ j < base + scale8 n) ==>
            mem1.[ j ] == mem2.[ j ]))

    b: Vale.PPC64LE.Memory.buffer64{Vale.PPC64LE.Memory.buffer_writeable b} ->
    i: Prims.nat{i < Vale.PPC64LE.Memory.buffer_length b} ->
    v: Vale.Def.Words_s.nat64 ->
    h: Vale.Arch.HeapImpl.vale_heap
  -> FStar.Pervasives.Lemma
      (requires
        FStar.List.Tot.Base.memP b (Vale.Interop.Heap_s.ptrs_of_mem (Vale.Arch.HeapImpl._ih h)))
      (ensures
        (let mem1 = Vale.Interop.down_mem (Vale.Arch.HeapImpl._ih h) in
          let h1 = Vale.PPC64LE.Memory.buffer_write b i v h in
          let mem2 = Vale.Interop.down_mem (Vale.Arch.HeapImpl._ih h1) in
          let base = Vale.PPC64LE.Memory.buffer_addr b h in
          let n = Vale.PPC64LE.Memory.buffer_length b in
          forall (j: Prims.int). {:pattern mem1.[ j ]\/mem2.[ j ]}
            base <= j /\ j < base + Vale.PPC64LE.Memory.scale8 i \/
            base + Vale.PPC64LE.Memory.scale8 (i + 1) <= j /\
            j < base + Vale.PPC64LE.Memory.scale8 n ==>
            mem1.[ j ] == mem2.[ j ]))