The bounded integer payload from rustc_middle::ty::consts::int::ScalarInt. The packed Rust layout is not semantically relevant here; construction keeps the payload truncated to its nonzero 1–16 byte width. Invalid sizes and source panics are returned explicitly.

inductive Miri.Memory.ScalarIntError : Type

• sizeError (reason : ABI.SizeError) : ScalarIntError
• zeroSize : ScalarIntError
• sizeTooLarge (size : ABI.Size) : ScalarIntError
• sizeMismatch (expected actual : ABI.Size) : ScalarIntError
• integerOutsideI128 (value : Int) : ScalarIntError
• integerConversionOverflow (value : Int) : ScalarIntError
• invalidBool (value : UInt8) : ScalarIntError
• invalidChar (value : UInt32) : ScalarIntError
• invalidAtomicOrdering (value : UInt32) : ScalarIntError
• invalidSimdAlignment (value : UInt32) : ScalarIntError

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarIntError : DecidableEq ScalarIntError

Equations

• Miri.Memory.instDecidableEqScalarIntError = Miri.Memory.instDecidableEqScalarIntError.decEq

def Miri.Memory.instDecidableEqScalarIntError.decEq (x✝ x✝¹ : ScalarIntError) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.instReprScalarIntError.repr : ScalarIntError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprScalarIntError : Repr ScalarIntError

Equations

• Miri.Memory.instReprScalarIntError = { reprPrec := Miri.Memory.instReprScalarIntError.repr }

@[instance_reducible]

instance Miri.Memory.instToStringScalarIntError : ToString ScalarIntError

Equations

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

inductive Miri.Memory.AtomicOrdering : Type

• relaxed : AtomicOrdering
• release : AtomicOrdering
• acquire : AtomicOrdering
• acqRel : AtomicOrdering
• seqCst : AtomicOrdering

@[instance_reducible]

instance Miri.Memory.instDecidableEqAtomicOrdering : DecidableEq AtomicOrdering

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprAtomicOrdering : Repr AtomicOrdering

Equations

• Miri.Memory.instReprAtomicOrdering = { reprPrec := Miri.Memory.instReprAtomicOrdering.repr }

def Miri.Memory.instReprAtomicOrdering.repr : AtomicOrdering → Nat → Std.Format

Equations

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

inductive Miri.Memory.SimdAlignment : Type

• unaligned : SimdAlignment
• element : SimdAlignment
• vector : SimdAlignment

@[instance_reducible]

instance Miri.Memory.instDecidableEqSimdAlignment : DecidableEq SimdAlignment

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprSimdAlignment : Repr SimdAlignment

Equations

• Miri.Memory.instReprSimdAlignment = { reprPrec := Miri.Memory.instReprSimdAlignment.repr }

def Miri.Memory.instReprSimdAlignment.repr : SimdAlignment → Nat → Std.Format

Equations

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

structure Miri.Memory.ScalarInt : Type

• rawData : Miri.ABI.U128
• byteSize : Miri.ABI.Size

def Miri.Memory.instDecidableEqScalarInt.decEq (x✝ x✝¹ : ScalarInt) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarInt : DecidableEq ScalarInt

Equations

• Miri.Memory.instDecidableEqScalarInt = Miri.Memory.instDecidableEqScalarInt.decEq

@[instance_reducible]

instance Miri.Memory.instReprScalarInt : Repr ScalarInt

Equations

• Miri.Memory.instReprScalarInt = { reprPrec := Miri.Memory.instReprScalarInt.repr }

def Miri.Memory.instReprScalarInt.repr : ScalarInt → Nat → Std.Format

Equations

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

def Miri.Memory.ScalarInt.size (self : ScalarInt) : ABI.Size

Equations

• self.size = Miri.Memory.ScalarInt.byteSize✝ self

def Miri.Memory.ScalarInt.data (self : ScalarInt) : ABI.U128

Equations

• self.data = Miri.Memory.ScalarInt.rawData✝ self

def Miri.Memory.ScalarInt.null (size : ABI.Size) : Except ScalarIntError ScalarInt

Equations

• Miri.Memory.ScalarInt.null size = do let _ ← Miri.Memory.ScalarInt.checkedWidth✝ size pure { rawData := 0, byteSize := size }

def Miri.Memory.ScalarInt.isNull (self : ScalarInt) : Bool

Equations

• self.isNull = (Miri.Memory.ScalarInt.rawData✝ self == 0)

def Miri.Memory.ScalarInt.trueValue : ScalarInt

Equations

• Miri.Memory.ScalarInt.trueValue = { rawData := 1, byteSize := Miri.ABI.Size.ofBytes 1 }

def Miri.Memory.ScalarInt.falseValue : ScalarInt

Equations

• Miri.Memory.ScalarInt.falseValue = { rawData := 0, byteSize := Miri.ABI.Size.ofBytes 1 }

def Miri.Memory.ScalarInt.truncateFromUInt (value : ABI.U128) (size : ABI.Size) : Except ScalarIntError (ScalarInt × Bool)

Return low bits plus the source truncation flag. size remains a checked source domain: zero and widths above 128 bits cannot become valid scalars.

Equations

• Miri.Memory.ScalarInt.truncateFromUInt value size = Miri.Memory.ScalarInt.truncated✝ value size

def Miri.Memory.ScalarInt.tryFromUInt (value : ABI.U128) (size : ABI.Size) : Except ScalarIntError (Option ScalarInt)

Equations

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

def Miri.Memory.ScalarInt.truncateFromInt (value : Int) (size : ABI.Size) : Except ScalarIntError (ScalarInt × Bool)

Signed input is an arbitrary Lean integer; first enforce Rust's i128 domain, then preserve its two's-complement bits before truncating.

Equations

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

def Miri.Memory.ScalarInt.tryFromInt (value : Int) (size : ABI.Size) : Except ScalarIntError (Option ScalarInt)

Equations

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

def Miri.Memory.ScalarInt.ofUInt8 (value : UInt8) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofUInt8 value = { rawData := BitVec.ofNat 128 value.toNat, byteSize := Miri.ABI.Size.ofBytes 1 }

def Miri.Memory.ScalarInt.ofUInt16 (value : UInt16) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofUInt16 value = { rawData := BitVec.ofNat 128 value.toNat, byteSize := Miri.ABI.Size.ofBytes 2 }

def Miri.Memory.ScalarInt.ofUInt32 (value : UInt32) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofUInt32 value = { rawData := BitVec.ofNat 128 value.toNat, byteSize := Miri.ABI.Size.ofBytes 4 }

def Miri.Memory.ScalarInt.ofUInt64 (value : UInt64) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofUInt64 value = { rawData := BitVec.ofNat 128 value.toNat, byteSize := Miri.ABI.Size.ofBytes 8 }

def Miri.Memory.ScalarInt.ofUInt128 (value : ABI.U128) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofUInt128 value = { rawData := value, byteSize := Miri.ABI.Size.ofBytes 16 }

def Miri.Memory.ScalarInt.ofInt8 (value : Int8) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofInt8 value = { rawData := BitVec.ofNat 128 value.toUInt8.toNat, byteSize := Miri.ABI.Size.ofBytes 1 }

def Miri.Memory.ScalarInt.ofInt16 (value : Int16) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofInt16 value = { rawData := BitVec.ofNat 128 value.toUInt16.toNat, byteSize := Miri.ABI.Size.ofBytes 2 }

def Miri.Memory.ScalarInt.ofInt32 (value : Int32) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofInt32 value = { rawData := BitVec.ofNat 128 value.toUInt32.toNat, byteSize := Miri.ABI.Size.ofBytes 4 }

def Miri.Memory.ScalarInt.ofInt64 (value : Int64) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofInt64 value = { rawData := BitVec.ofNat 128 value.toUInt64.toNat, byteSize := Miri.ABI.Size.ofBytes 8 }

def Miri.Memory.ScalarInt.ofInt128 (value : BitVec 128) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofInt128 value = { rawData := value, byteSize := Miri.ABI.Size.ofBytes 16 }

def Miri.Memory.ScalarInt.ofBool (value : Bool) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofBool value = if value = true then Miri.Memory.ScalarInt.trueValue else Miri.Memory.ScalarInt.falseValue

def Miri.Memory.ScalarInt.ofChar (value : Char) : ScalarInt

Equations

• Miri.Memory.ScalarInt.ofChar value = Miri.Memory.ScalarInt.ofUInt32 (UInt32.ofNat value.toNat)

def Miri.Memory.ScalarInt.toBits (self : ScalarInt) (expectedSize : ABI.Size) : Except ScalarIntError ABI.U128

The source's exact-size check is explicit instead of a Lean panic.

Equations

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

def Miri.Memory.ScalarInt.toBitsUnchecked (self : ScalarInt) : ABI.U128

Equations

• self.toBitsUnchecked = Miri.Memory.ScalarInt.rawData✝ self

def Miri.Memory.ScalarInt.toUInt (self : ScalarInt) (expectedSize : ABI.Size) : Except ScalarIntError ABI.U128

Equations

• self.toUInt expectedSize = self.toBits expectedSize

def Miri.Memory.ScalarInt.toInt (self : ScalarInt) (expectedSize : ABI.Size) : Except ScalarIntError Int

Equations

• self.toInt expectedSize = do let bits ← self.toBits expectedSize Except.mapError Miri.Memory.ScalarIntError.sizeError (expectedSize.signExtend bits)

def Miri.Memory.ScalarInt.toUInt8 (self : ScalarInt) : Except ScalarIntError UInt8

Equations

• self.toUInt8 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 1) pure (UInt8.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.ScalarInt.toUInt16 (self : ScalarInt) : Except ScalarIntError UInt16

Equations

• self.toUInt16 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 2) pure (UInt16.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.ScalarInt.toUInt32 (self : ScalarInt) : Except ScalarIntError UInt32

Equations

• self.toUInt32 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 4) pure (UInt32.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.ScalarInt.toUInt64 (self : ScalarInt) : Except ScalarIntError UInt64

Equations

• self.toUInt64 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 8) pure (UInt64.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.ScalarInt.toUInt128 (self : ScalarInt) : Except ScalarIntError ABI.U128

Equations

• self.toUInt128 = self.toUInt (Miri.ABI.Size.ofBytes 16)

def Miri.Memory.ScalarInt.toInt8 (self : ScalarInt) : Except ScalarIntError Int8

Equations

• self.toInt8 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 1) pure (Int8.ofInt __do_lift)

def Miri.Memory.ScalarInt.toInt16 (self : ScalarInt) : Except ScalarIntError Int16

Equations

• self.toInt16 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 2) pure (Int16.ofInt __do_lift)

def Miri.Memory.ScalarInt.toInt32 (self : ScalarInt) : Except ScalarIntError Int32

Equations

• self.toInt32 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 4) pure (Int32.ofInt __do_lift)

def Miri.Memory.ScalarInt.toInt64 (self : ScalarInt) : Except ScalarIntError Int64

Equations

• self.toInt64 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 8) pure (Int64.ofInt __do_lift)

def Miri.Memory.ScalarInt.toInt128 (self : ScalarInt) : Except ScalarIntError Int

Equations

• self.toInt128 = self.toInt (Miri.ABI.Size.ofBytes 16)

def Miri.Memory.ScalarInt.toTargetUsize (self : ScalarInt) (targetSize : ABI.Size) : Except ScalarIntError UInt64

Equations

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

def Miri.Memory.ScalarInt.toTargetIsize (self : ScalarInt) (targetSize : ABI.Size) : Except ScalarIntError Int64

Equations

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

def Miri.Memory.ScalarInt.tryToBool (self : ScalarInt) : Except ScalarIntError Bool

Equations

• self.tryToBool = do let value ← self.toUInt8 if (value == 0) = true then pure false else if (value == 1) = true then pure true else throw (Miri.Memory.ScalarIntError.invalidBool value)

def Miri.Memory.ScalarInt.toChar (self : ScalarInt) : Except ScalarIntError Char

Equations

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

def Miri.Memory.ScalarInt.toAtomicOrdering (self : ScalarInt) : Except ScalarIntError AtomicOrdering

Equations

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

def Miri.Memory.ScalarInt.toSimdAlignment (self : ScalarInt) : Except ScalarIntError SimdAlignment

Equations

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

theorem Miri.Memory.ScalarInt.trueValue_is_one : BitVec.toNat trueValue.data = 1

theorem Miri.Memory.ScalarInt.falseValue_is_zero : falseValue.data = 0