let vuint8 = TUInt8
let vuint8 =
TUInt8
Vale.X64.Memory.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.BigOps.fsti.checked
Vale.X64.Memory.fsti
Vale.Arch.HeapTypes_s.TUInt8
module Vale.X64.Memory
include Vale.Arch.HeapTypes_s
open FStar.Mul
open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16

unfold let vale_heap = vale_heap
unfold let vale_full_heap = vale_full_heap
unfold let heaplet_id = heaplet_id

[@va_qattr]
let get_vale_heap (vhi:vale_full_heap) : vale_heap = vhi.vf_heap

[@va_qattr]
let set_vale_heap (vfh:vale_full_heap) (vh:vale_heap) : vale_full_heap =
  {vfh with vf_heap = vh}

let vale_full_heap_equal (h1 h2:vale_full_heap) =
  h1.vf_layout == h2.vf_layout /\
  h1.vf_heap == h2.vf_heap /\
  Map16.equal h1.vf_heaplets h2.vf_heaplets

val get_heaplet_id (h:vale_heap) : option heaplet_id

unfold let nat8 = Vale.Def.Words_s.nat8
unfold let nat16 = Vale.Def.Words_s.nat16
unfold let nat32 = Vale.Def.Words_s.nat32
unfold let nat64 = Vale.Def.Words_s.nat64
unfold let quad32 = Vale.Def.Types_s.quad32

let base_typ_as_vale_type (t:base_typ) : Tot eqtype =
  match t with
  | TUInt8 -> nat8
  | TUInt16 -> nat16
  | TUInt32 -> nat32
  | TUInt64 -> nat64
  | TUInt128 -> quad32

let scale_by (scale index:int) : int = scale * index
unfold let scale2 (index:int) : int = scale_by 2 index
unfold let scale4 (index:int) : int = scale_by 4 index
unfold let scale8 (index:int) : int = scale_by 8 index
unfold let scale16 (index:int) : int = scale_by 16 index

unfold let buffer (t:base_typ) : Type0 = Vale.Arch.HeapImpl.buffer t
val buffer_as_seq (#t:base_typ) (h:vale_heap) (b:buffer t) : GTot (Seq.seq (base_typ_as_vale_type t))
val buffer_readable (#t:base_typ) (h:vale_heap) (b:buffer t) : GTot prop0
val buffer_writeable (#t:base_typ) (b:buffer t) : GTot prop0
val buffer_length (#t:base_typ) (b:buffer t) : GTot nat
val loc : Type u#0
val loc_none : loc
val loc_union (s1 s2:loc) : GTot loc
val loc_buffer (#t:base_typ) (b:buffer t) : GTot loc
val loc_disjoint (s1 s2:loc) : GTot prop0
val loc_includes (s1 s2:loc) : GTot prop0
val modifies (s:loc) (h1 h2:vale_heap) : GTot prop0

let valid_buffer_read (#t:base_typ) (h:vale_heap) (b:buffer t) (i:int) : prop0 =
  0 <= i /\ i < buffer_length b /\ buffer_readable h b

let valid_buffer_write (#t:base_typ) (h:vale_heap) (b:buffer t) (i:int) : prop0 =
  valid_buffer_read h b i /\ buffer_writeable b
val vuint8 : Vale.Arch.HeapTypes_s.base_typ
Vale.Arch.HeapTypes_s.base_typ