val prediction_post_rel
      (#max_arity: nat)
      (post: VSig.vale_post_tl [])
      (code: V.va_code)
      (args: IX64.arg_list)
    : IX64.prediction_post_rel_t code args
let prediction_post_rel
    (#max_arity:nat)
    (post:VSig.vale_post_tl [])
    (code:V.va_code)
    (args:IX64.arg_list)
  : IX64.prediction_post_rel_t code args
  =
  fun
    (h0:mem_roots args)
    (_s0:BS.machine_state)
    (rax_fuel_mem:(UInt64.t & nat & interop_heap))
    (s1:BS.machine_state) ->
  let rax, fuel, mem = rax_fuel_mem in
  exists h1.
    h1 == hs_of_mem mem /\
    mem_roots_p h1 args /\
    LSig.(to_low_post post args h0 rax h1)
val prediction_post_rel
      (#max_arity: nat)
      (post: VSig.vale_post_tl [])
      (code: V.va_code)
      (args: IX64.arg_list)
    : IX64.prediction_post_rel_t code args
let prediction_post_rel
      (#max_arity: nat)
      (post: VSig.vale_post_tl [])
      (code: V.va_code)
      (args: IX64.arg_list)
    : IX64.prediction_post_rel_t code args =
fun
  (h0: mem_roots args)
  (_s0: BS.machine_state)
  (rax_fuel_mem: (UInt64.t & nat & interop_heap))
  (s1: BS.machine_state)
  ->
  let rax, fuel, mem = rax_fuel_mem in
  exists h1. h1 == hs_of_mem mem /\ mem_roots_p h1 args /\ LSig.(to_low_post post args h0 rax h1)
Vale.AsLowStar.Wrapper.fsti.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Stack_i.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.Lemmas.fsti.checked Vale.X64.Decls.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Interop.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Calc.fsti.checked
Vale.AsLowStar.Wrapper.fsti
Prims.nat Vale.AsLowStar.ValeSig.vale_post_tl Prims.Nil Vale.Interop.Base.td Vale.X64.Decls.va_code Vale.Interop.X64.arg_list Vale.Interop.Base.mem_roots Vale.X64.Machine_Semantics_s.machine_state FStar.Pervasives.Native.tuple3 FStar.UInt64.t Vale.Interop.Heap_s.interop_heap Prims.l_Exists FStar.Monotonic.HyperStack.mem Vale.Interop.Base.mem_roots_p Prims.l_and Prims.eq2 Vale.Interop.Heap_s.hs_of_mem Vale.AsLowStar.LowStarSig.to_low_post Prims.prop Vale.Interop.X64.prediction_post_rel_t
module Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters
open Vale.Interop.Base
module B = LowStar.Buffer
module BS = Vale.X64.Machine_Semantics_s
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
module HS = FStar.HyperStack
module ME = Vale.X64.Memory
module SI = Vale.X64.Stack_i
module MS = Vale.X64.Machine_s
module IA = Vale.Interop.Assumptions
module I = Vale.Interop
module V = Vale.X64.Decls
module VS = Vale.X64.State
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module SL = Vale.X64.StateLemmas
module VL = Vale.X64.Lemmas
module ST = FStar.HyperStack.ST
open FStar.Mul
open FStar.Calc

[@__reduce__]
let prediction_pre_rel
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (pre:VSig.vale_pre_tl [])
    (code:V.va_code)
    (args:IX64.arg_list)
  : IX64.prediction_pre_rel_t code args
  =
  fun (h0:mem_roots args) ->
    LSig.(to_low_pre #max_arity #arg_reg pre args h0)

[@__reduce__]
let prediction_post_rel
    (#max_arity:nat)
    (post:VSig.vale_post_tl [])
    (code:V.va_code)
    (args:IX64.arg_list)
  : IX64.prediction_post_rel_t code args
val prediction_post_rel
      (#max_arity: nat)
      (post: VSig.vale_post_tl [])
      (code: V.va_code)
      (args: IX64.arg_list)
    : IX64.prediction_post_rel_t code args

    post: Vale.AsLowStar.ValeSig.vale_post_tl [] ->
    code: Vale.X64.Decls.va_code ->
    args: Vale.Interop.X64.arg_list
  -> Vale.Interop.X64.prediction_post_rel_t code args