inductive Miri.Interpreter.IntrinsicX86.VectorInstruction : Type

• avg : VectorInstruction
• mulHigh : VectorInstruction
• madWord : VectorInstruction
• madByte : VectorInstruction
• mulRound : VectorInstruction
• sign : VectorInstruction
• shuffle : VectorInstruction
• sad : VectorInstruction
• pack (bits : Nat) (signed : Bool) : VectorInstruction
• permute : VectorInstruction
• permute2 : VectorInstruction
• shiftScalar (op : Shift) : VectorInstruction
• shiftVector (op : Shift) : VectorInstruction
• dot : VectorInstruction
• multipleSad : VectorInstruction
• dotBytes : VectorInstruction
• ternary : VectorInstruction
• permuteFloat (double : Bool) : VectorInstruction
• insert : VectorInstruction
• minPosition : VectorInstruction
• test (high : Bool) (kind : Nat) : VectorInstruction
• unaligned : VectorInstruction
• nop : VectorInstruction
• gather : VectorInstruction

def Miri.Interpreter.IntrinsicX86.vectorSpec : String → Option VectorInstruction

def Miri.Interpreter.IntrinsicX86.vectorArity : VectorInstruction → Nat

Equations

• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.gather = 5
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.ternary = 4
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.permute2 = 3
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.dot = 3
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.multipleSad = 3
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.dotBytes = 3
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.insert = 3
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.minPosition = 1
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.unaligned = 1
• Miri.Interpreter.IntrinsicX86.vectorArity Miri.Interpreter.IntrinsicX86.VectorInstruction.nop = 0
• Miri.Interpreter.IntrinsicX86.vectorArity x✝ = 2

def Miri.Interpreter.IntrinsicX86.vectorDispatch {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (full name : String) (args : Array (OpTy P)) (dest : V) : M S Bool

Equations

• One or more equations did not get rendered due to their size.