val state_of_S (s: machine_state) : GTot vale_state
let state_of_S (s:machine_state) : GTot vale_state =
  let open Ms in
  {
    vs_ok = s.ms_ok;
    vs_regs = Regs.of_fun s.ms_regs;
    vs_flags = Flags.of_fun s.ms_flags;
    vs_heap = coerce s.ms_heap;
    vs_stack = VSS.stack_from_s s.ms_stack;
    vs_stackTaint = s.ms_stackTaint;
  }
val state_of_S (s: machine_state) : GTot vale_state
let state_of_S (s: machine_state) : GTot vale_state =
let open Ms in
{
  vs_ok = s.ms_ok;
  vs_regs = Regs.of_fun s.ms_regs;
  vs_flags = Flags.of_fun s.ms_flags;
  vs_heap = coerce s.ms_heap;
  vs_stack = VSS.stack_from_s s.ms_stack;
  vs_stackTaint = s.ms_stackTaint
}
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 Vale.X64.State.Mkvale_state Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.X64.Regs.of_fun Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs Vale.X64.Flags.of_fun Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Vale.X64.StateLemmas.coerce Vale.X64.Memory.vale_full_heap Vale.Arch.Heap.heap_impl Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.Stack_Sems.stack_from_s Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Vale.X64.State.vale_state
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

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

val use_machine_state_equal (_:unit) : Lemma
  (requires True)
  (ensures forall (s1 s2:machine_state).{:pattern machine_state_eq s1 s2}
    machine_state_equal s1 s2 ==> machine_state_eq s1 s2)

let state_to_S (s:vale_state) : GTot machine_state =
  let open Ms in
  {
    ms_ok = s.vs_ok;
    ms_regs = Regs.to_fun s.vs_regs;
    ms_flags = Flags.to_fun s.vs_flags;
    ms_heap = coerce s.vs_heap;
    ms_stack = VSS.stack_to_s s.vs_stack;
    ms_stackTaint = s.vs_stackTaint;
    ms_trace = [];
  }
val state_of_S (s: machine_state) : GTot vale_state
s: Vale.X64.StateLemmas.machine_state -> Prims.GTot Vale.X64.State.vale_state