val index128_get_heap_val128_aux (s: Seq.lseq UInt8.t 16) (ptr: int) (heap: S.machine_heap)
    : Lemma (requires (forall (j: nat). j < 16 ==> UInt8.v (Seq.index s j) == heap.[ ptr + j ]))
      (ensures
        Vale.Interop.Views.get128 s ==
        Mkfour (S.get_heap_val32 ptr heap)
          (S.get_heap_val32 (ptr + 4) heap)
          (S.get_heap_val32 (ptr + 8) heap)
          (S.get_heap_val32 (ptr + 12) heap))
let index128_get_heap_val128_aux (s:Seq.lseq UInt8.t 16) (ptr:int) (heap:S.machine_heap) : Lemma
  (requires (forall (j:nat) . j < 16 ==> UInt8.v (Seq.index s j) == heap.[ptr+j]))
  (ensures Vale.Interop.Views.get128 s == Mkfour
    (S.get_heap_val32 ptr heap)
    (S.get_heap_val32 (ptr+4) heap)
    (S.get_heap_val32 (ptr+8) heap)
    (S.get_heap_val32 (ptr+12) heap)) =
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  S.get_heap_val32_reveal ();
  Vale.Interop.Views.get128_reveal ();
  Vale.Def.Types_s.le_bytes_to_quad32_reveal ()
val index128_get_heap_val128_aux (s: Seq.lseq UInt8.t 16) (ptr: int) (heap: S.machine_heap)
    : Lemma (requires (forall (j: nat). j < 16 ==> UInt8.v (Seq.index s j) == heap.[ ptr + j ]))
      (ensures
        Vale.Interop.Views.get128 s ==
        Mkfour (S.get_heap_val32 ptr heap)
          (S.get_heap_val32 (ptr + 4) heap)
          (S.get_heap_val32 (ptr + 8) heap)
          (S.get_heap_val32 (ptr + 12) heap))
let index128_get_heap_val128_aux (s: Seq.lseq UInt8.t 16) (ptr: int) (heap: S.machine_heap)
    : Lemma (requires (forall (j: nat). j < 16 ==> UInt8.v (Seq.index s j) == heap.[ ptr + j ]))
      (ensures
        Vale.Interop.Views.get128 s ==
        Mkfour (S.get_heap_val32 ptr heap)
          (S.get_heap_val32 (ptr + 4) heap)
          (S.get_heap_val32 (ptr + 8) heap)
          (S.get_heap_val32 (ptr + 12) heap)) =
reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
S.get_heap_val32_reveal ();
Vale.Interop.Views.get128_reveal ();
Vale.Def.Types_s.le_bytes_to_quad32_reveal ()
Vale.PPC64LE.Memory.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Memory.fst
FStar.Seq.Properties.lseq FStar.UInt8.t Prims.int Vale.Arch.MachineHeap_s.machine_heap Vale.Def.Types_s.le_bytes_to_quad32_reveal Prims.unit Vale.Interop.Views.get128_reveal Vale.Arch.MachineHeap_s.get_heap_val32_reveal FStar.Pervasives.reveal_opaque FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.eq2 Prims.op_Modulus FStar.Seq.Base.length Vale.Def.Words_s.four Prims.op_Division Vale.Def.Words.Seq_s.seq_to_seq_four_LE Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Prims.l_or FStar.UInt.size FStar.UInt8.n Prims.l_and Prims.op_GreaterThanOrEqual Vale.Def.Words_s.pow2_8 FStar.UInt8.v FStar.Seq.Base.index Vale.PPC64LE.Memory.op_String_Access Prims.op_Addition Prims.squash Vale.Def.Types_s.nat32 Vale.Interop.Views.get128 Vale.Def.Words_s.Mkfour Vale.Arch.MachineHeap_s.get_heap_val32 Prims.Nil FStar.Pervasives.pattern
module Vale.PPC64LE.Memory
include Vale.Interop.Types
friend Vale.Arch.Heap
open Vale.Def.Opaque_s
open Vale.Arch.HeapImpl
open Vale.Arch.Heap
open Vale.Interop.Base
module IB = Vale.Interop.Base
module I = Vale.Interop
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module M = LowStar.Modifies
open LowStar.ModifiesPat
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
module H = FStar.Heap
module S = Vale.Arch.MachineHeap_s

#reset-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1"

let b8 = IB.b8

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

let get_heaplet_id h =
  h.heapletId

let tuint8 = UInt8.t
let tuint16 = UInt16.t
let tuint32 = UInt32.t
let tuint64 = UInt64.t

let v_of_typ (t:base_typ) (v:base_typ_as_vale_type t) : base_typ_as_type t =
  match t with
  | TUInt8 -> UInt8.uint_to_t v
  | TUInt16 -> UInt16.uint_to_t v
  | TUInt32 -> UInt32.uint_to_t v
  | TUInt64 -> UInt64.uint_to_t v
  | TUInt128 -> v

let v_to_typ (t:base_typ) (v:base_typ_as_type t) : base_typ_as_vale_type t =
  match t with
  | TUInt8 -> UInt8.v v
  | TUInt16 -> UInt16.v v
  | TUInt32 -> UInt32.v v
  | TUInt64 -> UInt64.v v
  | TUInt128 -> v

let lemma_v_to_of_typ (t:base_typ) (v:base_typ_as_vale_type t) : Lemma
  (ensures v_to_typ t (v_of_typ t v) == v)
  [SMTPat (v_to_typ t (v_of_typ t v))]
  =
  ()

let uint8_view = Vale.Interop.Views.up_view8
let uint16_view = Vale.Interop.Views.up_view16
let uint32_view = Vale.Interop.Views.up_view32
let uint64_view = Vale.Interop.Views.up_view64
let uint128_view = Vale.Interop.Views.up_view128

let uint_view (t:base_typ) : (v:UV.view UInt8.t (IB.base_typ_as_type t){UV.View?.n v == view_n t}) =
  match t with
  | TUInt8 -> uint8_view
  | TUInt16 -> uint16_view
  | TUInt32 -> uint32_view
  | TUInt64 -> uint64_view
  | TUInt128 -> uint128_view

let buffer_as_seq #t h b =
  let s = UV.as_seq (IB.hs_of_mem (_ih h)) (UV.mk_buffer (get_downview b.bsrc) (uint_view t)) in
  Vale.Lib.Seqs_s.seq_map (v_to_typ t) s

let buffer_readable #t h b = List.memP b (IB.ptrs_of_mem (_ih h))
let buffer_writeable #t b = b.writeable
let buffer_length #t b = UV.length (UV.mk_buffer (get_downview b.bsrc) (uint_view t))
let loc = M.loc
let loc_none = M.loc_none
let loc_union = M.loc_union
let loc_buffer #t b = M.loc_buffer b.bsrc
let loc_disjoint = M.loc_disjoint
let loc_includes = M.loc_includes
let modifies s h h' =
  M.modifies s (_ih h).hs (_ih h').hs /\
  h.heapletId == h'.heapletId /\
  (_ih h).ptrs == (_ih h').ptrs /\
  (_ih h).addrs == (_ih h').addrs /\
  HST.equal_domains (_ih h).hs (_ih h').hs

let buffer_addr #t b h = IB.addrs_of_mem (_ih h) b

open FStar.Mul

#set-options "--z3rlimit 20"

let index64_heap_aux (s:Seq.lseq UInt8.t 8) (heap:S.machine_heap) (ptr:int) : Lemma
  (requires forall (j:nat{j < 8}). UInt8.v (Seq.index s j) == heap.[ptr+j])
  (ensures UInt64.v (Vale.Interop.Views.get64 s) == S.get_heap_val64 ptr heap) =
  let open Vale.Def.Words.Seq_s in
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  Vale.Interop.Views.get64_reveal ();
  S.get_heap_val64_reveal ();
  Vale.Def.Types_s.le_bytes_to_nat64_reveal ()

let index_helper (x y:int) (heap:S.machine_heap) : Lemma
  (requires x == y)
  (ensures heap.[x] == heap.[y])
  =
  ()

let index_mul_helper (addr i n j:int) : Lemma
  (addr + (i * n + j) == addr + n * i + j) =
 ()

#set-options "--max_fuel 0 --max_ifuel 0"

let index64_get_heap_val64
    (h:vale_heap)
    (b:buffer64{List.memP b (_ih h).ptrs})
    (heap:S.machine_heap{IB.correct_down (_ih h) heap})
    (i:nat{i < buffer_length b})
  : Lemma (Seq.index (buffer_as_seq h b) i == S.get_heap_val64 (buffer_addr b h + scale8 i) heap)
  =
  let db = get_downview b.bsrc in
  let ub = UV.mk_buffer db uint64_view in
  let ptr = buffer_addr b h + scale8 i in
  let s = DV.as_seq (_ih h).hs db in
  let t = TUInt64 in
  let addr = buffer_addr b h in
  UV.length_eq ub;
  UV.as_seq_sel (_ih h).hs ub i;
  UV.get_sel (_ih h).hs ub i;
  let s' = Seq.slice s (i*8) (i*8 + 8) in
  let aux (j:nat{j < 8}) : Lemma (UInt8.v (Seq.index s' j) == heap.[ptr+j]) =
    assert (UInt8.v (Seq.index s (i*8 + j)) == heap.[addr + (i*8+j)]);
    Seq.lemma_index_slice s (i*8) (i*8+8) j;
    assert (UInt8.v (Seq.index s' j) == heap.[addr+(i*8+j)]);
    index_mul_helper addr i 8 j;
    ()
  in Classical.forall_intro aux;
  index64_heap_aux s' heap ptr

#set-options "--z3rlimit 50"

open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Four_s
open Vale.Lib.Seqs_s

let index128_get_heap_val128_aux (s:Seq.lseq UInt8.t 16) (ptr:int) (heap:S.machine_heap) : Lemma
  (requires (forall (j:nat) . j < 16 ==> UInt8.v (Seq.index s j) == heap.[ptr+j]))
  (ensures Vale.Interop.Views.get128 s == Mkfour
    (S.get_heap_val32 ptr heap)
    (S.get_heap_val32 (ptr+4) heap)
    (S.get_heap_val32 (ptr+8) heap)
val index128_get_heap_val128_aux (s: Seq.lseq UInt8.t 16) (ptr: int) (heap: S.machine_heap)
    : Lemma (requires (forall (j: nat). j < 16 ==> UInt8.v (Seq.index s j) == heap.[ ptr + j ]))
      (ensures
        Vale.Interop.Views.get128 s ==
        Mkfour (S.get_heap_val32 ptr heap)
          (S.get_heap_val32 (ptr + 4) heap)
          (S.get_heap_val32 (ptr + 8) heap)
          (S.get_heap_val32 (ptr + 12) heap))

    s: FStar.Seq.Properties.lseq FStar.UInt8.t 16 ->
    ptr: Prims.int ->
    heap: Vale.Arch.MachineHeap_s.machine_heap
  -> FStar.Pervasives.Lemma
      (requires
        forall (j: Prims.nat).
          j < 16 ==> FStar.UInt8.v (FStar.Seq.Base.index s j) == heap.[ ptr + j ])
      (ensures
        Vale.Interop.Views.get128 s ==
        Vale.Def.Words_s.Mkfour (Vale.Arch.MachineHeap_s.get_heap_val32 ptr heap)
          (Vale.Arch.MachineHeap_s.get_heap_val32 (ptr + 4) heap)
          (Vale.Arch.MachineHeap_s.get_heap_val32 (ptr + 8) heap)
          (Vale.Arch.MachineHeap_s.get_heap_val32 (ptr + 12) heap))