val modified_arg_mloc (x: arg) : GTot ME.loc
let modified_arg_mloc (x:arg) : GTot ME.loc =
    match x with
    | (|TD_Buffer src t {modified=true}, x|) -> ME.loc_buffer (as_vale_buffer #src #t x)
    | _ -> ME.loc_none
val modified_arg_mloc (x: arg) : GTot ME.loc
let modified_arg_mloc (x: arg) : GTot ME.loc =
match x with
| (| TD_Buffer src t { modified = true } , x |) -> ME.loc_buffer (as_vale_buffer #src #t x)
| _ -> ME.loc_none
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.Interop.Base.arg Vale.Arch.HeapTypes_s.base_typ Vale.Arch.HeapTypes_s.taint Prims.bool Vale.Interop.Base.td_as_type Vale.Interop.Base.TD_Buffer Vale.Interop.Base.Mkbuffer_qualifiers Vale.X64.Memory.loc_buffer Vale.X64.MemoryAdapters.as_vale_buffer Prims.dtuple2 Vale.Interop.Base.td Vale.X64.Memory.loc_none Vale.X64.Memory.loc
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

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_xmm (r:MS.reg_xmm) (s0 s1:V.va_state) =
  VS.eval_reg_xmm r s0 == VS.eval_reg_xmm r s1

let vale_calling_conventions
  (s0 s1:V.va_state)
  (regs_modified:MS.reg_64 -> bool)
  (xmms_modified:MS.reg_xmm -> bool) =
  let open MS in
  s1.VS.vs_ok /\
  vale_save_reg MS.rRsp s0 s1 /\
  (forall (r:MS.reg_64).
    not (regs_modified r) ==> vale_save_reg r s0 s1) /\
  (forall (x:MS.reg_xmm).
    not (xmms_modified x) ==> vale_save_xmm x s0 s1)

[@__reduce__]
val modified_arg_mloc (x: arg) : GTot ME.loc
x: Vale.Interop.Base.arg -> Prims.GTot Vale.X64.Memory.loc