val coerce (#b #a: Type) (x: a{a == b}) : b
let coerce (#b #a:Type) (x:a{a == b}) : b = x
val coerce (#b #a: Type) (x: a{a == b}) : b
let coerce (#b #a: Type) (x: a{a == b}) : b =
x
Vale.X64.MemoryAdapters.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Lib.Map16.fsti.checked Vale.Interop.Base.fst.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked LowStar.BufferView.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.fst.checked
Vale.X64.MemoryAdapters.fsti
Prims.eq2
module Vale.X64.MemoryAdapters

open FStar.Mul
open Vale.Interop.Base
open Vale.Arch.HeapTypes_s
open Vale.Arch.HeapImpl
open Vale.Arch.Heap
open Vale.Arch.MachineHeap_s
module BS = Vale.X64.Machine_Semantics_s
module BV = LowStar.BufferView
module HS = FStar.HyperStack
module ME = Vale.X64.Memory
module SI = Vale.X64.Stack_i
module IB = Vale.Interop.Base
module VS = Vale.X64.State
module V = Vale.X64.Decls
module Map16 = Vale.Lib.Map16
val as_vale_buffer (#src #t:base_typ) (i:IB.buf_t src t) : GTot (ME.buffer t)
val as_vale_immbuffer (#src #t:base_typ) (i:IB.ibuf_t src t) : GTot (ME.buffer t)

val stack_eq : squash (BS.machine_stack == SI.vale_stack)

val as_mem (h:ME.vale_heap) : GTot IB.interop_heap
val coerce (#b #a: Type) (x: a{a == b}) : b
x: a{a == b} -> b