let vale_full_heap = M.vale_full_heap
let vale_full_heap =
M.vale_full_heap
Vale.X64.Decls.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Flags.fsti.checked Vale.Lib.Map16.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.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.All.fst.checked
Vale.X64.Decls.fsti
Vale.X64.Memory.vale_full_heap
module Vale.X64.Decls
open FStar.Mul
open Vale.Arch.HeapTypes_s
open Vale.Arch.HeapImpl
module M = Vale.X64.Memory
module S = Vale.X64.Stack_i
module Map16 = Vale.Lib.Map16

// This interface should hide all of Machine_Semantics_s.
// (It should not refer to Machine_Semantics_s, directly or indirectly.)
// It should not refer to StateLemmas, Lemmas, or Print_s,
// because they refer to Machine_Semantics_s.
// Stack_i, Memory, Regs, Flags and State are ok, because they do not refer to Machine_Semantics_s.

open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.Def.Types_s
val vale_full_heap : Type
Type