val has_taint128 (o: operand128) (t: taint) : bool
let has_taint128 (o:operand128) (t:taint) : bool =
  match o with
  | OMem (_, t') | OStack (_, t') -> t = t'
  | _ -> true
val has_taint128 (o: operand128) (t: taint) : bool
let has_taint128 (o: operand128) (t: taint) : bool =
match o with
| OMem (_, t') | OStack (_, t') -> t = t'
| _ -> true
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
Vale.X64.Machine_s.operand128 Vale.Arch.HeapTypes_s.taint Vale.X64.Machine_s.maddr Prims.op_Equality Vale.X64.Machine_s.operand Vale.X64.Machine_s.quad32 Vale.X64.Machine_s.reg_xmm Prims.bool
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
val has_taint128 (o: operand128) (t: taint) : bool
o: Vale.X64.Machine_s.operand128 -> t: Vale.Arch.HeapTypes_s.taint -> Prims.bool