inductive Miri.Interpreter.IntrinsicX86.Shift : Type

• left : Shift
• logicalRight : Shift
• arithmeticRight : Shift

@[instance_reducible]

instance Miri.Interpreter.IntrinsicX86.instDecidableEqShift : DecidableEq Shift

Equations

• Miri.Interpreter.IntrinsicX86.instDecidableEqShift x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.IntrinsicX86.shiftScalar {P S : Type} [Memory.PointerProvenance P] (value : Memory.Scalar P) (size : ABI.Size) (amount : Nat) (which : Shift) : M S (Memory.Scalar P)

Equations

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

def Miri.Interpreter.IntrinsicX86.extractFirstU64 {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (source : OpTy P) : M S UInt64

Equations

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

def Miri.Interpreter.IntrinsicX86.shiftVector {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left right : OpTy P) (dest : V) (which : Shift) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.shiftByScalar {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left right : OpTy P) (dest : V) (which : Shift) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.wideBinary {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (average : Bool) (left right : OpTy P) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.multiplyAdd {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (bytes : Bool) (left right : OpTy P) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.multiplyRound {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left right : OpTy P) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.signVector {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left right : OpTy P) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.shuffleBytes {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left right : OpTy P) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.permute {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left indices : OpTy P) (right : Option (OpTy P)) (dest : V) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.testBits {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (source mask : OpTy P) (high : Bool) : M S (Bool × Bool)

Equations

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