val pre_rel_generic
      (#max_arity: nat)
      (#arg_reg: IX64.arg_reg_relation max_arity)
      (code: V.va_code)
      (dom: list td)
      (args: list arg {List.length dom + List.length args <= 20})
      (pre: VSig.vale_pre_tl dom)
    : IX64.rel_gen_t code dom args (IX64.prediction_pre_rel_t (coerce code))
let rec pre_rel_generic
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (code:V.va_code)
    (dom:list td)
    (args:list arg{List.length dom + List.length args <= 20})
    (pre:VSig.vale_pre_tl dom)
  : IX64.rel_gen_t code dom args (IX64.prediction_pre_rel_t (coerce code))
  =
  match dom with
  | [] ->
    prediction_pre_rel #max_arity #arg_reg pre (coerce code) args
  | hd::tl ->
    fun (x:td_as_type hd) ->
    pre_rel_generic #max_arity #arg_reg code tl IX64.(x ++ args) (elim_1 pre x)
val pre_rel_generic
      (#max_arity: nat)
      (#arg_reg: IX64.arg_reg_relation max_arity)
      (code: V.va_code)
      (dom: list td)
      (args: list arg {List.length dom + List.length args <= 20})
      (pre: VSig.vale_pre_tl dom)
    : IX64.rel_gen_t code dom args (IX64.prediction_pre_rel_t (coerce code))
let rec pre_rel_generic
      (#max_arity: nat)
      (#arg_reg: IX64.arg_reg_relation max_arity)
      (code: V.va_code)
      (dom: list td)
      (args: list arg {List.length dom + List.length args <= 20})
      (pre: VSig.vale_pre_tl dom)
    : IX64.rel_gen_t code dom args (IX64.prediction_pre_rel_t (coerce code)) =
match dom with
| [] -> prediction_pre_rel #max_arity #arg_reg pre (coerce code) args
| hd :: tl ->
  fun (x: td_as_type hd) ->
    pre_rel_generic #max_arity #arg_reg code tl IX64.(x ++ args) (elim_1 pre x)
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.X64.Decls.va_code Prims.list Vale.Interop.Base.td Vale.Interop.Base.arg Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.List.Tot.Base.length Vale.AsLowStar.ValeSig.vale_pre_tl Vale.AsLowStar.Wrapper.prediction_pre_rel Vale.Interop.Base.coerce Vale.Interop.Base.td_as_type Vale.AsLowStar.Wrapper.pre_rel_generic Vale.Interop.X64.op_Plus_Plus Vale.Interop.Base.elim_1 Vale.X64.Decls.va_state Prims.prop Vale.Interop.X64.rel_gen_t Vale.Interop.X64.prediction_pre_rel_t Vale.X64.Machine_Semantics_s.code
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
  =
  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 vale_lemma_as_prediction
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (#regs_modified:MS.reg_64 -> bool)
    (#xmms_modified:MS.reg_xmm -> bool)
    (code:V.va_code)
    (args:IX64.arg_list)
    (pre:VSig.vale_pre_tl [])
    (post:VSig.vale_post_tl [])
    (v:VSig.vale_sig_tl regs_modified xmms_modified args (coerce code) pre post)
  : IX64.prediction
      max_arity
      arg_reg
      regs_modified
      xmms_modified
      (coerce code)
      args
      (prediction_pre_rel #max_arity #arg_reg pre (coerce code) args)
      (prediction_post_rel #max_arity post (coerce code) args)

// ////////////////////////////////////////////////////////////////////////////////
// //Wrap abstract
// ////////////////////////////////////////////////////////////////////////////////
[@__reduce__]
let rec pre_rel_generic
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (code:V.va_code)
    (dom:list td)
    (args:list arg{List.length dom + List.length args <= 20})
    (pre:VSig.vale_pre_tl dom)
  : IX64.rel_gen_t code dom args (IX64.prediction_pre_rel_t (coerce code))
val pre_rel_generic
      (#max_arity: nat)
      (#arg_reg: IX64.arg_reg_relation max_arity)
      (code: V.va_code)
      (dom: list td)
      (args: list arg {List.length dom + List.length args <= 20})
      (pre: VSig.vale_pre_tl dom)
    : IX64.rel_gen_t code dom args (IX64.prediction_pre_rel_t (coerce code))

    code: Vale.X64.Decls.va_code ->
    dom: Prims.list Vale.Interop.Base.td ->
    args:
      Prims.list Vale.Interop.Base.arg
        {FStar.List.Tot.Base.length dom + FStar.List.Tot.Base.length args <= 20} ->
    pre: Vale.AsLowStar.ValeSig.vale_pre_tl dom
  -> Vale.Interop.X64.rel_gen_t code
      dom
      args
      (Vale.Interop.X64.prediction_pre_rel_t (Vale.Interop.Base.coerce code))