val reveal_machine_eval_code_ins (i: S.ins) (s: S.machine_state)
    : Lemma (requires True)
      (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
      [SMTPat (S.machine_eval_code_ins i s)]
let reveal_machine_eval_code_ins (i:S.ins) (s:S.machine_state) : Lemma
  (requires True)
  (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
  [SMTPat (S.machine_eval_code_ins i s)]
  =
  reveal_opaque (`%S.machine_eval_code_ins) S.machine_eval_code_ins
val reveal_machine_eval_code_ins (i: S.ins) (s: S.machine_state)
    : Lemma (requires True)
      (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
      [SMTPat (S.machine_eval_code_ins i s)]
let reveal_machine_eval_code_ins (i: S.ins) (s: S.machine_state)
    : Lemma (requires True)
      (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
      [SMTPat (S.machine_eval_code_ins i s)] =
reveal_opaque (`%S.machine_eval_code_ins) S.machine_eval_code_ins
Vale.X64.Leakage_Ins.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Leakage_s.fst.checked Vale.X64.Leakage_Helpers.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Lib.Set.fsti.checked Vale.Lib.MapTree.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Leakage_Ins.fst
Vale.X64.Machine_Semantics_s.ins Vale.X64.Machine_Semantics_s.machine_state FStar.Pervasives.reveal_opaque FStar.Pervasives.Native.option Vale.X64.Machine_Semantics_s.machine_eval_code_ins Prims.unit Prims.l_True Prims.squash Prims.eq2 Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module Vale.X64.Leakage_Ins
open FStar.Mul
open Vale.Arch.MachineHeap_s
open Vale.Arch.Heap
open Vale.X64.Machine_s
open Vale.X64.Instruction_s
module BC = Vale.X64.Bytes_Code_s
module S = Vale.X64.Machine_Semantics_s
open Vale.X64.Leakage_s
open Vale.X64.Leakage_Helpers

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

unfold let obs_args = S.obs_args
unfold let obs_inouts = S.obs_inouts
unfold let machine_eval_code = S.machine_eval_code

let reveal_machine_eval_code_ins (i:S.ins) (s:S.machine_state) : Lemma
  (requires True)
  (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
  [SMTPat (S.machine_eval_code_ins i s)]
val reveal_machine_eval_code_ins (i: S.ins) (s: S.machine_state)
    : Lemma (requires True)
      (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
      [SMTPat (S.machine_eval_code_ins i s)]
i: Vale.X64.Machine_Semantics_s.ins -> s: Vale.X64.Machine_Semantics_s.machine_state
  -> FStar.Pervasives.Lemma
      (ensures
        Vale.X64.Machine_Semantics_s.machine_eval_code_ins i s ==
        Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def i s)
      [SMTPat (Vale.X64.Machine_Semantics_s.machine_eval_code_ins i s)]