let va_Mod_ok = Mod_ok
let va_Mod_ok =
Mod_ok
Vale.X64.QuickCode.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.QuickCode.fst
Vale.X64.QuickCode.Mod_ok
module Vale.X64.QuickCode
open FStar.Mul
open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.Arch.HeapImpl
open Vale.X64.State
open Vale.X64.Decls

irreducible let qmodattr = ()

type mod_t =
| Mod_None : mod_t
| Mod_ok: mod_t
| Mod_reg: reg -> mod_t
| Mod_flags: mod_t
| Mod_mem: mod_t
| Mod_mem_layout: mod_t
| Mod_mem_heaplet: heaplet_id -> mod_t
| Mod_stack: mod_t
| Mod_stackTaint: mod_t
unfold let mods_t = list mod_t
unfold let va_mods_t = mods_t
val va_Mod_ok : Vale.X64.QuickCode.mod_t
Vale.X64.QuickCode.mod_t