val 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
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)
val 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
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) -> let open LSig in to_low_pre #max_arity #arg_reg pre args h0
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.Interop.X64.arg_reg_relation Vale.AsLowStar.ValeSig.vale_pre_tl Prims.Nil Vale.Interop.Base.td Vale.X64.Decls.va_code Vale.Interop.X64.arg_list Vale.Interop.Base.mem_roots Vale.AsLowStar.LowStarSig.to_low_pre Prims.prop Vale.Interop.X64.prediction_pre_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
val 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

    pre: Vale.AsLowStar.ValeSig.vale_pre_tl [] ->
    code: Vale.X64.Decls.va_code ->
    args: Vale.Interop.X64.arg_list
  -> Vale.Interop.X64.prediction_pre_rel_t code args