let machine_state_equal (s1 s2:machine_state) =
  let open Vale.X64.Machine_Semantics_s in
  s1.ms_ok == s2.ms_ok /\
  F.feq s1.ms_regs s2.ms_regs /\
  F.feq s1.ms_flags s2.ms_flags /\
  s1.ms_heap == s2.ms_heap /\
  s1.ms_stack == s2.ms_stack /\
  s1.ms_stackTaint == s2.ms_stackTaint /\
  s1.ms_trace == s2.ms_trace /\
  True
let machine_state_equal (s1 s2: machine_state) =
let open Vale.X64.Machine_Semantics_s in
s1.ms_ok == s2.ms_ok /\ F.feq s1.ms_regs s2.ms_regs /\ F.feq s1.ms_flags s2.ms_flags /\
s1.ms_heap == s2.ms_heap /\ s1.ms_stack == s2.ms_stack /\ s1.ms_stackTaint == s2.ms_stackTaint /\
s1.ms_trace == s2.ms_trace /\ True
Vale.X64.StateLemmas.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_Sems.fsti.checked Vale.X64.Regs.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Flags.fsti.checked Vale.Def.Prop_s.fst.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.FunctionalExtensionality.fsti.checked
Vale.X64.StateLemmas.fsti
Vale.X64.StateLemmas.machine_state Prims.l_and Prims.eq2 Prims.bool Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok FStar.FunctionalExtensionality.feq Vale.X64.Machine_s.reg Vale.X64.Machine_s.t_reg Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs Vale.X64.Machine_s.flag Vale.X64.Machine_Semantics_s.flag_val_t Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Vale.Arch.Heap.heap_impl Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.Machine_Semantics_s.machine_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack Vale.Arch.HeapTypes_s.memTaint_t Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Prims.list Vale.X64.Machine_s.observation Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace Prims.l_True Prims.logical
module Vale.X64.StateLemmas
open Vale.X64.Machine_s
open Vale.Arch.Heap
open Vale.X64.State
open FStar.FunctionalExtensionality
module Ms = Vale.X64.Machine_Semantics_s
//open Vale.X64.Machine_Semantics_s
//module ME = Vale.X64.Memory
open Vale.X64.Memory
open Vale.Arch.MachineHeap_s
//module MS = Vale.X64.Memory_Sems
module VSS = Vale.X64.Stack_Sems
module F = FStar.FunctionalExtensionality
open Vale.Def.Prop_s
open FStar.Mul

unfold let machine_state = Ms.machine_state
unfold let code = Ms.code
unfold let machine_eval_code = Ms.machine_eval_code
val same_heap_types : squash (vale_full_heap == heap_impl)
unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x

let machine_state_eq (s1 s2:machine_state) =
  s1 == s2
val machine_state_equal : s1: Vale.X64.StateLemmas.machine_state -> s2: Vale.X64.StateLemmas.machine_state -> Prims.logical
s1: Vale.X64.StateLemmas.machine_state -> s2: Vale.X64.StateLemmas.machine_state -> Prims.logical