val make_instr_t_args (args: list instr_operand) : Type0
let rec make_instr_t_args (args:list instr_operand) : Type0 =
  match normal args with
  | [] -> S.ins
  | (IOpEx i)::args -> arrow (instr_operand_t i) (make_instr_t_args args)
  | (IOpIm _)::args -> make_instr_t_args args
val make_instr_t_args (args: list instr_operand) : Type0
let rec make_instr_t_args (args: list instr_operand) : Type0 =
match normal args with
| [] -> S.ins
| IOpEx i :: args -> arrow (instr_operand_t i) (make_instr_t_args args)
| IOpIm _ :: args -> make_instr_t_args args
Vale.X64.InsLemmas.fsti.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.InsLemmas.fsti
Prims.list Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.normal Vale.X64.Machine_Semantics_s.ins Vale.X64.Instruction_s.instr_operand_explicit Vale.X64.Instruction_s.arrow Vale.X64.Instruction_s.instr_operand_t Vale.X64.InsLemmas.make_instr_t_args Vale.X64.Instruction_s.instr_operand_implicit
module Vale.X64.InsLemmas

open FStar.Mul
open Vale.Arch.HeapImpl
open Vale.X64.Machine_s
open Vale.X64.Instruction_s
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.Decls
open Vale.X64.Memory
module BC = Vale.X64.Bytes_Code_s
module S = Vale.X64.Machine_Semantics_s
let has_taint128 (o:operand128) (t:taint) : bool =
  match o with
  | OMem (_, t') | OStack (_, t') -> t = t'
  | _ -> true

val lemma_valid_src_operand64_and_taint (o:operand64) (s:vale_state) : Lemma
  (requires valid_operand o s)
  (ensures S.valid_src_operand64_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand64_and_taint o (state_to_S s))]

val lemma_valid_src_operand128_and_taint (o:operand128) (s:vale_state) : Lemma
  (requires valid_operand128 o s)
  (ensures S.valid_src_operand128_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand128_and_taint o (state_to_S s))]

[@instr_attr]
val make_instr_t_args (args: list instr_operand) : Type0
args: Prims.list Vale.X64.Instruction_s.instr_operand -> Type0