let obs_inouts = S.obs_inouts
let obs_inouts =
S.obs_inouts
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.obs_inouts
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
val obs_inouts : inouts: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    oprs: Vale.X64.Instruction_s.instr_operands_t inouts args ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.list Vale.X64.Machine_s.observation

    inouts: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    oprs: Vale.X64.Instruction_s.instr_operands_t inouts args ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.list Vale.X64.Machine_s.observation