val update_state_mod (m: mod_t) (sM sK: vale_state) : vale_state
let update_state_mod (m:mod_t) (sM sK:vale_state) : vale_state =
  match m with
  | Mod_None -> sK
  | Mod_ok -> va_update_ok sM sK
  | Mod_reg r -> update_register r sM sK
  | Mod_flags -> va_update_flags sM sK
  | Mod_mem -> va_update_mem sM sK
  | Mod_mem_layout -> va_update_mem_layout sM sK
  | Mod_mem_heaplet n -> va_update_mem_heaplet n sM sK
  | Mod_stack -> va_update_stack sM sK
  | Mod_stackTaint -> va_update_stackTaint sM sK
val update_state_mod (m: mod_t) (sM sK: vale_state) : vale_state
let update_state_mod (m: mod_t) (sM sK: vale_state) : vale_state =
match m with
| Mod_None -> sK
| Mod_ok -> va_update_ok sM sK
| Mod_reg r -> update_register r sM sK
| Mod_flags -> va_update_flags sM sK
| Mod_mem -> va_update_mem sM sK
| Mod_mem_layout -> va_update_mem_layout sM sK
| Mod_mem_heaplet n -> va_update_mem_heaplet n sM sK
| Mod_stack -> va_update_stack sM sK
| Mod_stackTaint -> va_update_stackTaint sM sK
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_t Vale.X64.State.vale_state Vale.X64.Decls.va_update_ok Vale.X64.Machine_s.reg Vale.X64.Decls.update_register Vale.X64.Decls.va_update_flags Vale.X64.Decls.va_update_mem Vale.X64.Decls.va_update_mem_layout Vale.X64.Decls.heaplet_id Vale.X64.Decls.va_update_mem_heaplet Vale.X64.Decls.va_update_stack Vale.X64.Decls.va_update_stackTaint
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

[@va_qattr] unfold let va_Mod_None = Mod_None
[@va_qattr] unfold let va_Mod_ok = Mod_ok
[@va_qattr] unfold let va_Mod_reg64 (r:reg_64) = Mod_reg (Reg 0 r)
[@va_qattr] unfold let va_Mod_xmm (r:reg_xmm) = Mod_reg (Reg 1 r)
[@va_qattr] unfold let va_Mod_flags = Mod_flags
[@va_qattr] unfold let va_Mod_mem = Mod_mem
[@va_qattr] unfold let va_Mod_mem_layout = Mod_mem_layout
[@va_qattr] unfold let va_Mod_mem_heaplet (n:heaplet_id) = Mod_mem_heaplet n
[@va_qattr] unfold let va_Mod_stack = Mod_stack
[@va_qattr] unfold let va_Mod_stackTaint = Mod_stackTaint

[@va_qattr "opaque_to_smt"]
let mod_eq (x y:mod_t) : Pure bool (requires True) (ensures fun b -> b == (x = y)) =
  match x with
  | Mod_None -> (match y with Mod_None -> true | _ -> false)
  | Mod_ok -> (match y with Mod_ok -> true | _ -> false)
  | Mod_reg rx -> (match y with Mod_reg ry -> rx = ry | _ -> false)
  | Mod_flags -> (match y with Mod_flags -> true | _ -> false)
  | Mod_mem -> (match y with Mod_mem -> true | _ -> false)
  | Mod_mem_layout -> (match y with Mod_mem_layout -> true | _ -> false)
  | Mod_mem_heaplet nx -> (match y with Mod_mem_heaplet ny -> nx = ny | _ -> false)
  | Mod_stack -> (match y with Mod_stack -> true | _ -> false)
  | Mod_stackTaint -> (match y with Mod_stackTaint -> true | _ -> false)

[@va_qattr]
val update_state_mod (m: mod_t) (sM sK: vale_state) : vale_state
m: Vale.X64.QuickCode.mod_t -> sM: Vale.X64.State.vale_state -> sK: Vale.X64.State.vale_state
  -> Vale.X64.State.vale_state