let machine_eval_code = S.machine_eval_code
let machine_eval_code =
S.machine_eval_code
Vale.X64.Leakage.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Leakage_s.fst.checked Vale.X64.Leakage_Ins.fsti.checked Vale.X64.Leakage_Helpers.fst.checked Vale.Lib.MapTree.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Leakage.fst
Vale.X64.Machine_Semantics_s.machine_eval_code
module Vale.X64.Leakage
open FStar.Mul
open Vale.X64.Machine_s
module S = Vale.X64.Machine_Semantics_s
open Vale.X64.Leakage_s
open Vale.X64.Leakage_Helpers
open Vale.X64.Leakage_Ins
val machine_eval_code : c: Vale.X64.Machine_Semantics_s.code ->
    fuel: Prims.nat ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.Tot (FStar.Pervasives.Native.option Vale.X64.Machine_Semantics_s.machine_state)

    c: Vale.X64.Machine_Semantics_s.code ->
    fuel: Prims.nat ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.Tot (FStar.Pervasives.Native.option Vale.X64.Machine_Semantics_s.machine_state)