let vale_save_reg (r:MS.reg_64) (s0 s1:V.va_state) =
  VS.eval_reg_64 r s0 == VS.eval_reg_64 r s1
let vale_save_reg (r: MS.reg_64) (s0 s1: V.va_state) =
VS.eval_reg_64 r s0 == VS.eval_reg_64 r s1
Vale.AsLowStar.ValeSig.fst.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Lib.Map16.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked LowStar.BufferView.fsti.checked LowStar.Buffer.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.fst.checked FStar.BigOps.fsti.checked
Vale.AsLowStar.ValeSig.fst
Vale.X64.Machine_s.reg_64 Vale.X64.Decls.va_state Prims.eq2 Vale.X64.Memory.nat64 Vale.X64.State.eval_reg_64 Prims.logical
module Vale.AsLowStar.ValeSig
open FStar.Mul
open Vale.Arch.HeapImpl
open Vale.Interop.Base
module B = LowStar.Buffer
module BS = Vale.X64.Machine_Semantics_s
module BV = LowStar.BufferView
module HS = FStar.HyperStack
module ME = Vale.X64.Memory
module MS = Vale.X64.Machine_s
module IA = Vale.Interop.Assumptions
module V = Vale.X64.Decls
module VS = Vale.X64.State
module IX64 = Vale.Interop.X64
module List = FStar.List.Tot
module Map16 = Vale.Lib.Map16
open Vale.X64.MemoryAdapters

[@__reduce__]
let vale_pre_tl (dom:list td) =
    n_arrow dom (V.va_state -> prop)

[@__reduce__]
let vale_pre (dom:list td) =
    code:V.va_code ->
    vale_pre_tl dom

[@__reduce__]
let vale_post_tl (dom:list td) =
    n_arrow dom
            (s0:V.va_state -> s1:V.va_state -> f:V.va_fuel -> prop)

[@__reduce__]
let vale_post (dom:list td) =
    code:V.va_code ->
    vale_post_tl dom
val vale_save_reg : r: Vale.X64.Machine_s.reg_64 -> s0: Vale.X64.Decls.va_state -> s1: Vale.X64.Decls.va_state
  -> Prims.logical
r: Vale.X64.Machine_s.reg_64 -> s0: Vale.X64.Decls.va_state -> s1: Vale.X64.Decls.va_state
  -> Prims.logical