val loc : Type u#0
let loc = M.loc
val loc : Type u#0
let loc =
M.loc
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
LowStar.Monotonic.Buffer.loc
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
val loc : Type u#0
Type0