Integer-like casts and integer numeric intrinsics from the pinned rustc_const_eval::interpret::{cast,intrinsics} sources. The caller supplies the compiler-resolved layouts. This module does not represent floating point, raw/function pointers, or pointer provenance, so those casts cannot be routed through these operations.

inductive Miri.Interpreter.IntegerCastSource : Type

• integer (type : IntegerType) : IntegerCastSource
• boolean : IntegerCastSource
• character : IntegerCastSource

def Miri.Interpreter.instDecidableEqIntegerCastSource.decEq (x✝ x✝¹ : IntegerCastSource) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntegerCastSource.decEq (Miri.Interpreter.IntegerCastSource.integer type) Miri.Interpreter.IntegerCastSource.boolean = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastSource.decEq (Miri.Interpreter.IntegerCastSource.integer type) Miri.Interpreter.IntegerCastSource.character = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastSource.decEq Miri.Interpreter.IntegerCastSource.boolean (Miri.Interpreter.IntegerCastSource.integer type) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastSource.decEq Miri.Interpreter.IntegerCastSource.boolean Miri.Interpreter.IntegerCastSource.boolean = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntegerCastSource.decEq Miri.Interpreter.IntegerCastSource.character (Miri.Interpreter.IntegerCastSource.integer type) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastSource.decEq Miri.Interpreter.IntegerCastSource.character Miri.Interpreter.IntegerCastSource.character = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerCastSource : DecidableEq IntegerCastSource

Equations

• Miri.Interpreter.instDecidableEqIntegerCastSource = Miri.Interpreter.instDecidableEqIntegerCastSource.decEq

def Miri.Interpreter.instReprIntegerCastSource.repr : IntegerCastSource → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerCastSource : Repr IntegerCastSource

Equations

• Miri.Interpreter.instReprIntegerCastSource = { reprPrec := Miri.Interpreter.instReprIntegerCastSource.repr }

inductive Miri.Interpreter.IntegerCastTarget : Type

• integer (type : IntegerType) : IntegerCastTarget
• character : IntegerCastTarget

def Miri.Interpreter.instDecidableEqIntegerCastTarget.decEq (x✝ x✝¹ : IntegerCastTarget) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntegerCastTarget.decEq (Miri.Interpreter.IntegerCastTarget.integer type) Miri.Interpreter.IntegerCastTarget.character = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastTarget.decEq Miri.Interpreter.IntegerCastTarget.character (Miri.Interpreter.IntegerCastTarget.integer type) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastTarget.decEq Miri.Interpreter.IntegerCastTarget.character Miri.Interpreter.IntegerCastTarget.character = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerCastTarget : DecidableEq IntegerCastTarget

Equations

• Miri.Interpreter.instDecidableEqIntegerCastTarget = Miri.Interpreter.instDecidableEqIntegerCastTarget.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerCastTarget : Repr IntegerCastTarget

Equations

• Miri.Interpreter.instReprIntegerCastTarget = { reprPrec := Miri.Interpreter.instReprIntegerCastTarget.repr }

def Miri.Interpreter.instReprIntegerCastTarget.repr : IntegerCastTarget → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.IntegerCastError : Type

• scalar (reason : Memory.ScalarIntError) : IntegerCastError
• integerToCharTryFromPanicked (value : Nat) : IntegerCastError

def Miri.Interpreter.instDecidableEqIntegerCastError.decEq (x✝ x✝¹ : IntegerCastError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntegerCastError.decEq (Miri.Interpreter.IntegerCastError.scalar a) (Miri.Interpreter.IntegerCastError.scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastError.decEq (Miri.Interpreter.IntegerCastError.scalar reason) (Miri.Interpreter.IntegerCastError.integerToCharTryFromPanicked value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerCastError.decEq (Miri.Interpreter.IntegerCastError.integerToCharTryFromPanicked value) (Miri.Interpreter.IntegerCastError.scalar reason) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerCastError : DecidableEq IntegerCastError

Equations

• Miri.Interpreter.instDecidableEqIntegerCastError = Miri.Interpreter.instDecidableEqIntegerCastError.decEq

def Miri.Interpreter.instReprIntegerCastError.repr : IntegerCastError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerCastError : Repr IntegerCastError

Equations

• Miri.Interpreter.instReprIntegerCastError = { reprPrec := Miri.Interpreter.instReprIntegerCastError.repr }

def Miri.Interpreter.IntegerCast.cast (source : IntegerCastSource) (value : Memory.ScalarInt) (target : IntegerCastTarget) : Except IntegerCastError Memory.ScalarInt

Pinned cast_from_int_like behavior for integer, bool, and char inputs. Signed integer sources are sign-extended to the source's u128 intermediate before destination truncation. The char target follows u8::try_from(v).unwrap() and records that unwrap's panic when conversion fails.

Equations

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

inductive Miri.Interpreter.IntegerIntrinsic : Type

• ctpop : IntegerIntrinsic
• cttz : IntegerIntrinsic
• cttzNonzero : IntegerIntrinsic
• ctlz : IntegerIntrinsic
• ctlzNonzero : IntegerIntrinsic
• bswap : IntegerIntrinsic
• bitreverse : IntegerIntrinsic

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerIntrinsic : DecidableEq IntegerIntrinsic

Equations

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

def Miri.Interpreter.instReprIntegerIntrinsic.repr : IntegerIntrinsic → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerIntrinsic : Repr IntegerIntrinsic

Equations

• Miri.Interpreter.instReprIntegerIntrinsic = { reprPrec := Miri.Interpreter.instReprIntegerIntrinsic.repr }

inductive Miri.Interpreter.IntegerIntrinsicError : Type

• scalar (reason : Memory.ScalarIntError) : IntegerIntrinsicError
• undefinedBehaviorOnZero (intrinsic : IntegerIntrinsic) : IntegerIntrinsicError
• layoutMismatch (input output : IntegerType) : IntegerIntrinsicError

def Miri.Interpreter.instDecidableEqIntegerIntrinsicError.decEq (x✝ x✝¹ : IntegerIntrinsicError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerIntrinsicError : DecidableEq IntegerIntrinsicError

Equations

• Miri.Interpreter.instDecidableEqIntegerIntrinsicError = Miri.Interpreter.instDecidableEqIntegerIntrinsicError.decEq

def Miri.Interpreter.instReprIntegerIntrinsicError.repr : IntegerIntrinsicError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerIntrinsicError : Repr IntegerIntrinsicError

Equations

• Miri.Interpreter.instReprIntegerIntrinsicError = { reprPrec := Miri.Interpreter.instReprIntegerIntrinsicError.repr }

def Miri.Interpreter.IntegerIntrinsic.run (intrinsic : IntegerIntrinsic) (value : Memory.ScalarInt) (inputType outputType : IntegerType) : Except IntegerIntrinsicError Memory.ScalarInt

The pinned numeric_intrinsic branches. Counting ignores signedness and uses the input width; byte swap and bit reversal require matching layouts.

Equations

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

inductive Miri.Interpreter.IntegerArithmeticIntrinsicError : Type

• integerOperation (reason : IntegerOpError) : IntegerArithmeticIntrinsicError
• scalar (reason : Memory.ScalarIntError) : IntegerArithmeticIntrinsicError
• exactDivisionHasRemainder (remainder : Memory.ScalarInt) : IntegerArithmeticIntrinsicError
• unexpectedOverflowResult (result : IntegerResult) : IntegerArithmeticIntrinsicError
• unexpectedDivisionResult (result : IntegerResult) : IntegerArithmeticIntrinsicError

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerArithmeticIntrinsicError : DecidableEq IntegerArithmeticIntrinsicError

Equations

• Miri.Interpreter.instDecidableEqIntegerArithmeticIntrinsicError = Miri.Interpreter.instDecidableEqIntegerArithmeticIntrinsicError.decEq

def Miri.Interpreter.instDecidableEqIntegerArithmeticIntrinsicError.decEq (x✝ x✝¹ : IntegerArithmeticIntrinsicError) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Interpreter.instReprIntegerArithmeticIntrinsicError.repr : IntegerArithmeticIntrinsicError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerArithmeticIntrinsicError : Repr IntegerArithmeticIntrinsicError

Equations

• Miri.Interpreter.instReprIntegerArithmeticIntrinsicError = { reprPrec := Miri.Interpreter.instReprIntegerArithmeticIntrinsicError.repr }

inductive Miri.Interpreter.IntegerSaturatingOp : Type

• add : IntegerSaturatingOp
• sub : IntegerSaturatingOp

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerSaturatingOp : DecidableEq IntegerSaturatingOp

Equations

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

def Miri.Interpreter.instReprIntegerSaturatingOp.repr : IntegerSaturatingOp → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerSaturatingOp : Repr IntegerSaturatingOp

Equations

• Miri.Interpreter.instReprIntegerSaturatingOp = { reprPrec := Miri.Interpreter.instReprIntegerSaturatingOp.repr }

def Miri.Interpreter.IntegerArithmeticIntrinsic.saturatingArith (op : IntegerSaturatingOp) (left right : IntegerValue) : Except IntegerArithmeticIntrinsicError Memory.ScalarInt

Pinned saturating_arith: use the source overflowing operation, then select the signed bound using the first operand's sign or the unsigned bound from the operation direction.

Equations

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

def Miri.Interpreter.IntegerArithmeticIntrinsic.exactDiv (left right : IntegerValue) : Except IntegerArithmeticIntrinsicError Memory.ScalarInt

Pinned exact_div: the ordinary remainder operation supplies division by zero and signed MIN / -1 UB checks; a nonzero remainder is the intrinsic's own UB branch; only then is ordinary division evaluated.

Equations

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