Integer branches of pinned rustc_const_eval interpret/operator.rs. Layout acquisition and scalar extraction are separate interpreter operations. These entry points take their checked scalar payload and integer layout; they do not assert that an arbitrary MIR operand has either property.

structure Miri.Interpreter.IntegerType : Type

• size : ABI.Size
• kind : MIR.IntegerKind

def Miri.Interpreter.instDecidableEqIntegerType.decEq (x✝ x✝¹ : IntegerType) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqIntegerType.decEq { size := a, kind := a_1 } { size := b, kind := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerType : DecidableEq IntegerType

Equations

• Miri.Interpreter.instDecidableEqIntegerType = Miri.Interpreter.instDecidableEqIntegerType.decEq

def Miri.Interpreter.instReprIntegerType.repr : IntegerType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerType : Repr IntegerType

Equations

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

def Miri.Interpreter.IntegerType.signed (type : IntegerType) : Bool

Equations

• type.signed = type.kind.signed

structure Miri.Interpreter.IntegerValue : Type

• scalar : Memory.ScalarInt
• type : IntegerType

def Miri.Interpreter.instDecidableEqIntegerValue.decEq (x✝ x✝¹ : IntegerValue) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqIntegerValue.decEq { scalar := a, type := a_1 } { scalar := b, type := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerValue : DecidableEq IntegerValue

Equations

• Miri.Interpreter.instDecidableEqIntegerValue = Miri.Interpreter.instDecidableEqIntegerValue.decEq

def Miri.Interpreter.instReprIntegerValue.repr : IntegerValue → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerValue : Repr IntegerValue

Equations

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

inductive Miri.Interpreter.IntegerUB : Type

• divisionByZero : IntegerUB
• remainderByZero : IntegerUB
• divisionOverflow : IntegerUB
• remainderOverflow : IntegerUB
• arithmeticOverflow (op : MIR.BinOp) : IntegerUB
• shiftOverflow (op : MIR.BinOp) (amount : Int) (signed : Bool) : IntegerUB

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerUB : DecidableEq IntegerUB

Equations

• Miri.Interpreter.instDecidableEqIntegerUB = Miri.Interpreter.instDecidableEqIntegerUB.decEq

def Miri.Interpreter.instDecidableEqIntegerUB.decEq (x✝ x✝¹ : IntegerUB) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.divisionByZero Miri.Interpreter.IntegerUB.divisionByZero = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.divisionByZero (Miri.Interpreter.IntegerUB.arithmeticOverflow op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.divisionByZero (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.remainderByZero Miri.Interpreter.IntegerUB.remainderByZero = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.remainderByZero (Miri.Interpreter.IntegerUB.arithmeticOverflow op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.remainderByZero (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.divisionOverflow Miri.Interpreter.IntegerUB.divisionOverflow = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.divisionOverflow (Miri.Interpreter.IntegerUB.arithmeticOverflow op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.divisionOverflow (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.remainderOverflow Miri.Interpreter.IntegerUB.remainderOverflow = isTrue ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.remainderOverflow (Miri.Interpreter.IntegerUB.arithmeticOverflow op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq Miri.Interpreter.IntegerUB.remainderOverflow (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.arithmeticOverflow op) Miri.Interpreter.IntegerUB.divisionByZero = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.arithmeticOverflow op) Miri.Interpreter.IntegerUB.remainderByZero = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.arithmeticOverflow op) Miri.Interpreter.IntegerUB.divisionOverflow = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.arithmeticOverflow op) Miri.Interpreter.IntegerUB.remainderOverflow = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.arithmeticOverflow op) (Miri.Interpreter.IntegerUB.shiftOverflow op_1 amount signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) Miri.Interpreter.IntegerUB.divisionByZero = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) Miri.Interpreter.IntegerUB.remainderByZero = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) Miri.Interpreter.IntegerUB.divisionOverflow = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) Miri.Interpreter.IntegerUB.remainderOverflow = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerUB.decEq (Miri.Interpreter.IntegerUB.shiftOverflow op amount signed) (Miri.Interpreter.IntegerUB.arithmeticOverflow op_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerUB : Repr IntegerUB

Equations

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

def Miri.Interpreter.instReprIntegerUB.repr : IntegerUB → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.IntegerOpError : Type

• scalar (reason : Memory.ScalarIntError) : IntegerOpError
• undefinedBehavior (reason : IntegerUB) : IntegerOpError
• asymmetricTypes (left right : IntegerType) : IntegerOpError
• invalidBinaryOperator (op : MIR.BinOp) : IntegerOpError
• invalidUnaryOperator (op : MIR.UnOp) (signed : Bool) : IntegerOpError

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerOpError : DecidableEq IntegerOpError

Equations

• Miri.Interpreter.instDecidableEqIntegerOpError = Miri.Interpreter.instDecidableEqIntegerOpError.decEq

def Miri.Interpreter.instDecidableEqIntegerOpError.decEq (x✝ x✝¹ : IntegerOpError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.scalar a) (Miri.Interpreter.IntegerOpError.scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.scalar reason) (Miri.Interpreter.IntegerOpError.undefinedBehavior reason_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.scalar reason) (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.scalar reason) (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.scalar reason) (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) (Miri.Interpreter.IntegerOpError.scalar reason_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) (Miri.Interpreter.IntegerOpError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) (Miri.Interpreter.IntegerOpError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op) (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op_1 signed) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) (Miri.Interpreter.IntegerOpError.scalar reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) (Miri.Interpreter.IntegerOpError.undefinedBehavior reason) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) (Miri.Interpreter.IntegerOpError.asymmetricTypes left right) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerOpError.decEq (Miri.Interpreter.IntegerOpError.invalidUnaryOperator op signed) (Miri.Interpreter.IntegerOpError.invalidBinaryOperator op_1) = isFalse ⋯

def Miri.Interpreter.instReprIntegerOpError.repr : IntegerOpError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerOpError : Repr IntegerOpError

Equations

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

inductive Miri.Interpreter.IntegerResult : Type

• scalar (value : Memory.ScalarInt) : IntegerResult
• withOverflow (value : Memory.ScalarInt) (overflow : Bool) : IntegerResult
• boolean (value : Bool) : IntegerResult
• ordering (value : Ordering) : IntegerResult

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqIntegerResult : DecidableEq IntegerResult

Equations

• Miri.Interpreter.instDecidableEqIntegerResult = Miri.Interpreter.instDecidableEqIntegerResult.decEq

def Miri.Interpreter.instDecidableEqIntegerResult.decEq (x✝ x✝¹ : IntegerResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.scalar a) (Miri.Interpreter.IntegerResult.scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.scalar value) (Miri.Interpreter.IntegerResult.withOverflow value_1 overflow) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.scalar value) (Miri.Interpreter.IntegerResult.boolean value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.scalar value) (Miri.Interpreter.IntegerResult.ordering value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.withOverflow value overflow) (Miri.Interpreter.IntegerResult.scalar value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.withOverflow value overflow) (Miri.Interpreter.IntegerResult.boolean value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.withOverflow value overflow) (Miri.Interpreter.IntegerResult.ordering value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.boolean value) (Miri.Interpreter.IntegerResult.scalar value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.boolean value) (Miri.Interpreter.IntegerResult.withOverflow value_1 overflow) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.boolean a) (Miri.Interpreter.IntegerResult.boolean b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.boolean value) (Miri.Interpreter.IntegerResult.ordering value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.ordering value) (Miri.Interpreter.IntegerResult.scalar value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.ordering value) (Miri.Interpreter.IntegerResult.withOverflow value_1 overflow) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.ordering value) (Miri.Interpreter.IntegerResult.boolean value_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqIntegerResult.decEq (Miri.Interpreter.IntegerResult.ordering a) (Miri.Interpreter.IntegerResult.ordering b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprIntegerResult : Repr IntegerResult

Equations

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

def Miri.Interpreter.instReprIntegerResult.repr : IntegerResult → Nat → Std.Format

Equations

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

def Miri.Interpreter.IntegerOps.binaryBool (op : MIR.BinOp) (l r : Bool) : Except IntegerOpError IntegerResult

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.Eq l r = do let result ← pure (l == r) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.Ne l r = do let result ← pure (l != r) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.Lt l r = do let result ← pure (decide (l < r)) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.Le l r = do let result ← pure (decide (l ≤ r)) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.Gt l r = do let result ← pure (decide (l > r)) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.Ge l r = do let result ← pure (decide (l ≥ r)) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.BitAnd l r = do let result ← pure (l && r) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.BitOr l r = do let result ← pure (l || r) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result
• Miri.Interpreter.IntegerOps.binaryBool Miri.MIR.BinOp.BitXor l r = do let result ← pure (l ^^ r) (fun (result : Bool) => pure (Miri.Interpreter.IntegerResult.boolean result)) result

def Miri.Interpreter.IntegerOps.binaryChar (op : MIR.BinOp) (l r : Char) : Except IntegerOpError IntegerResult

Equations

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

def Miri.Interpreter.IntegerOps.decode (value : IntegerValue) : Except IntegerOpError Int

Size-checked extraction using the source layout's signedness.

Equations

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

def Miri.Interpreter.IntegerOps.binary (op : MIR.BinOp) (left right : IntegerValue) : Except IntegerOpError IntegerResult

Equations

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

def Miri.Interpreter.IntegerOps.unary (op : MIR.UnOp) (value : IntegerValue) : Except IntegerOpError Memory.ScalarInt

Equations

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

def Miri.Interpreter.IntegerOps.computeSizeInBytes (elementSize : ABI.Size) (count : UInt64) (maxSizeOfVal : ABI.Size) : Option ABI.Size

Source compute_size_in_bytes checks u64 multiplication and an inclusive max_size_of_val, which differs from Size.checkedMul's object-size bound.

Equations

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

theorem Miri.Interpreter.IntegerOps.binary_division_by_zero (left right : IntegerValue) (l : Int) (hl : decode left = Except.ok l) (hr : decode right = Except.ok 0) (ht : left.type = right.type) : binary MIR.BinOp.Div left right = Except.error (IntegerOpError.undefinedBehavior IntegerUB.divisionByZero)

Once operand extraction and type agreement have succeeded, division by zero is always UB; wrapping arithmetic never turns it into a successful result.

theorem Miri.Interpreter.IntegerOps.binary_remainder_by_zero (left right : IntegerValue) (l : Int) (hl : decode left = Except.ok l) (hr : decode right = Except.ok 0) (ht : left.type = right.type) : binary MIR.BinOp.Rem left right = Except.error (IntegerOpError.undefinedBehavior IntegerUB.remainderByZero)

theorem Miri.Interpreter.IntegerOps.division_success_nonzero (left right : IntegerValue) (l r : Int) (hl : decode left = Except.ok l) (hr : decode right = Except.ok r) (ht : left.type = right.type) (value : IntegerResult) (success : binary MIR.BinOp.Div left right = Except.ok value) : r ≠ 0