val wrap_variadic (c:BS.code) : as_lowstar_sig c
let wrap_variadic c n arg_reg regs_modified xmms_modified args #pre_rel #post_rel predict =
  let h0 = ST.get () in
  assert (mem_roots_p h0 args);
  let rax, fuel, final_mem =
    IA.st_put
      #(UInt64.t & nat & interop_heap)
      (fun h0' -> h0' == h0)
      (fun h0' ->
        let va_s0, mem_s0 =
          create_initial_trusted_state n arg_reg args h0' in
        let (rax, fuel, final_mem) = predict h0 va_s0 in
        let Some va_s1 = BS.machine_eval_code c fuel va_s0 in
        let final_hs = hs_of_mem final_mem in
        (rax, fuel, final_mem), hs_of_mem final_mem
      ) in
  assert (ST.equal_domains h0 (hs_of_mem final_mem));
  rax, Ghost.hide (As_lowstar_sig_ret n args fuel final_mem)
val wrap_variadic (c:BS.code) : as_lowstar_sig c
let wrap_variadic c n arg_reg regs_modified xmms_modified args #pre_rel #post_rel predict =
let h0 = ST.get () in
assert (mem_roots_p h0 args);
let rax, fuel, final_mem =
  IA.st_put #(UInt64.t & nat & interop_heap)
    (fun h0' -> h0' == h0)
    (fun h0' ->
        let va_s0, mem_s0 = create_initial_trusted_state n arg_reg args h0' in
        let rax, fuel, final_mem = predict h0 va_s0 in
        let Some va_s1 = BS.machine_eval_code c fuel va_s0 in
        let final_hs = hs_of_mem final_mem in
        (rax, fuel, final_mem), hs_of_mem final_mem)
in
assert (ST.equal_domains h0 (hs_of_mem final_mem));
rax, Ghost.hide (As_lowstar_sig_ret n args fuel final_mem)
Vale.Interop.X64.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Vale.Interop.X64.fst
Vale.X64.Machine_Semantics_s.code Prims.nat Vale.Interop.X64.arg_reg_relation Vale.X64.Machine_s.reg_64 Prims.bool Vale.X64.Machine_s.reg_xmm Vale.Interop.X64.arg_list Vale.Interop.X64.prediction_pre_rel_t Vale.Interop.X64.prediction_post_rel_t Vale.Interop.X64.prediction FStar.UInt64.t Vale.Interop.Heap_s.interop_heap FStar.Pervasives.Native.Mktuple2 FStar.Ghost.erased Vale.Interop.X64.as_lowstar_sig_ret FStar.Ghost.hide Vale.Interop.X64.As_lowstar_sig_ret Prims.unit Prims._assert FStar.HyperStack.ST.equal_domains Vale.Interop.Heap_s.hs_of_mem Vale.Interop.X64.als_ret FStar.Pervasives.Native.tuple3 Vale.Interop.Assumptions.st_put FStar.Monotonic.HyperStack.mem Prims.eq2 Vale.X64.Machine_Semantics_s.machine_state FStar.Pervasives.Native.Mktuple3 FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.snd FStar.Pervasives.Native.option Vale.X64.Machine_Semantics_s.machine_eval_code Vale.Interop.X64.create_initial_trusted_state Vale.Interop.Base.mem_roots_p FStar.HyperStack.ST.get
module Vale.Interop.X64

open FStar.Mul
open Vale.Interop.Base
module B = LowStar.Buffer
module BS = Vale.X64.Machine_Semantics_s
module HS = FStar.HyperStack
module IA = Vale.Interop.Assumptions
module ST = FStar.HyperStack.ST
val wrap_variadic (c:BS.code) : as_lowstar_sig c
c: Vale.X64.Machine_Semantics_s.code -> Vale.Interop.X64.as_lowstar_sig c