The machine-width size primitives from rustc_abi::Size.

The upstream source stores byte counts in u64, and stores integer values in u128. Lean 4 has no UInt128, so U128 is represented by BitVec 128; this preserves the source machine width and wrapping behavior. Operations that panic in upstream return an explicit Except error here.

A structural equality decider for the standard Except result type.

@[instance_reducible]

instance Miri.ABI.instDecidableEqExcept_miri {ε : Type u_1} {α : Type u_2} [DecidableEq ε] [DecidableEq α] : DecidableEq (Except ε α)

Equations

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

@[reducible, inline]

abbrev Miri.ABI.U128 : Type

Equations

• Miri.ABI.U128 = BitVec 128

inductive Miri.ABI.Endian : Type

• little : Endian
• big : Endian

@[instance_reducible]

instance Miri.ABI.instDecidableEqEndian : DecidableEq Endian

Equations

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

def Miri.ABI.instReprEndian.repr : Endian → Nat → Std.Format

Equations

• Miri.ABI.instReprEndian.repr Miri.ABI.Endian.little prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Endian.little")).group prec✝
• Miri.ABI.instReprEndian.repr Miri.ABI.Endian.big prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Endian.big")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprEndian : Repr Endian

Equations

• Miri.ABI.instReprEndian = { reprPrec := Miri.ABI.instReprEndian.repr }

def Miri.ABI.Endian.asString : Endian → String

Equations

• Miri.ABI.Endian.little.asString = "little"
• Miri.ABI.Endian.big.asString = "big"

def Miri.ABI.Endian.parse (value : String) : Except String Endian

Equations

• Miri.ABI.Endian.parse "little" = Except.ok Miri.ABI.Endian.little
• Miri.ABI.Endian.parse "big" = Except.ok Miri.ABI.Endian.big
• Miri.ABI.Endian.parse value = Except.error (toString "unknown endian: \"" ++ toString value ++ toString "\"")

inductive Miri.ABI.PointerWidth : Type

• w16 : PointerWidth
• w32 : PointerWidth
• w64 : PointerWidth

@[instance_reducible]

instance Miri.ABI.instDecidableEqPointerWidth : DecidableEq PointerWidth

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprPointerWidth : Repr PointerWidth

Equations

• Miri.ABI.instReprPointerWidth = { reprPrec := Miri.ABI.instReprPointerWidth.repr }

def Miri.ABI.instReprPointerWidth.repr : PointerWidth → Nat → Std.Format

Equations

• Miri.ABI.instReprPointerWidth.repr Miri.ABI.PointerWidth.w16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.PointerWidth.w16")).group prec✝
• Miri.ABI.instReprPointerWidth.repr Miri.ABI.PointerWidth.w32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.PointerWidth.w32")).group prec✝
• Miri.ABI.instReprPointerWidth.repr Miri.ABI.PointerWidth.w64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.PointerWidth.w64")).group prec✝

def Miri.ABI.PointerWidth.bits : PointerWidth → UInt64

Equations

• Miri.ABI.PointerWidth.w16.bits = 16
• Miri.ABI.PointerWidth.w32.bits = 32
• Miri.ABI.PointerWidth.w64.bits = 64

def Miri.ABI.PointerWidth.objSizeBound : PointerWidth → UInt64

Equations

• Miri.ABI.PointerWidth.w16.objSizeBound = 32768
• Miri.ABI.PointerWidth.w32.objSizeBound = 2147483648
• Miri.ABI.PointerWidth.w64.objSizeBound = 2305843009213693952

The relevant projection of rustc_abi's target-dependent data layout.

structure Miri.ABI.TargetDataLayout : Type

• endian : Endian
• pointerWidth : PointerWidth

def Miri.ABI.instDecidableEqTargetDataLayout.decEq (x✝ x✝¹ : TargetDataLayout) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqTargetDataLayout : DecidableEq TargetDataLayout

Equations

• Miri.ABI.instDecidableEqTargetDataLayout = Miri.ABI.instDecidableEqTargetDataLayout.decEq

@[instance_reducible]

instance Miri.ABI.instReprTargetDataLayout : Repr TargetDataLayout

Equations

• Miri.ABI.instReprTargetDataLayout = { reprPrec := Miri.ABI.instReprTargetDataLayout.repr }

def Miri.ABI.instReprTargetDataLayout.repr : TargetDataLayout → Nat → Std.Format

Equations

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

def Miri.ABI.TargetDataLayout.objSizeBound (layout : TargetDataLayout) : UInt64

Equations

• layout.objSizeBound = layout.pointerWidth.objSizeBound

The actual caller interface used by rustc_abi Size::checked_add/mul: the caller supplies a data-layout value, from which the object-size bound is read.

class Miri.ABI.HasDataLayout (α : Type) : Type

• dataLayout : α → TargetDataLayout

@[instance_reducible]

instance Miri.ABI.instHasDataLayoutTargetDataLayout : HasDataLayout TargetDataLayout

Equations

• Miri.ABI.instHasDataLayoutTargetDataLayout = { dataLayout := id }

inductive Miri.ABI.SizeError : Type

• u64Overflow (operation : String) (left right : UInt64) : SizeError
• negativeSubtraction (left right : UInt64) : SizeError
• bitCountOverflow (bytes : UInt64) : SizeError
• integerWidthTooLarge (bits : UInt64) : SizeError
• zeroWidthUnsignedBound : SizeError
• zeroWidthSignedBound : SizeError

@[instance_reducible]

instance Miri.ABI.instReprSizeError : Repr SizeError

Equations

• Miri.ABI.instReprSizeError = { reprPrec := Miri.ABI.instReprSizeError.repr }

def Miri.ABI.instReprSizeError.repr : SizeError → Nat → Std.Format

Equations

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

def Miri.ABI.instDecidableEqSizeError.decEq (x✝ x✝¹ : SizeError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.u64Overflow operation left right) (Miri.ABI.SizeError.negativeSubtraction left_1 right_1) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.u64Overflow operation left right) (Miri.ABI.SizeError.bitCountOverflow bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.u64Overflow operation left right) (Miri.ABI.SizeError.integerWidthTooLarge bits) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.u64Overflow operation left right) Miri.ABI.SizeError.zeroWidthUnsignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.u64Overflow operation left right) Miri.ABI.SizeError.zeroWidthSignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.negativeSubtraction left right) (Miri.ABI.SizeError.u64Overflow operation left_1 right_1) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.negativeSubtraction left right) (Miri.ABI.SizeError.bitCountOverflow bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.negativeSubtraction left right) (Miri.ABI.SizeError.integerWidthTooLarge bits) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.negativeSubtraction left right) Miri.ABI.SizeError.zeroWidthUnsignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.negativeSubtraction left right) Miri.ABI.SizeError.zeroWidthSignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.bitCountOverflow bytes) (Miri.ABI.SizeError.u64Overflow operation left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.bitCountOverflow bytes) (Miri.ABI.SizeError.negativeSubtraction left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.bitCountOverflow a) (Miri.ABI.SizeError.bitCountOverflow b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.bitCountOverflow bytes) (Miri.ABI.SizeError.integerWidthTooLarge bits) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.bitCountOverflow bytes) Miri.ABI.SizeError.zeroWidthUnsignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.bitCountOverflow bytes) Miri.ABI.SizeError.zeroWidthSignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.integerWidthTooLarge bits) (Miri.ABI.SizeError.u64Overflow operation left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.integerWidthTooLarge bits) (Miri.ABI.SizeError.negativeSubtraction left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.integerWidthTooLarge bits) (Miri.ABI.SizeError.bitCountOverflow bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.integerWidthTooLarge a) (Miri.ABI.SizeError.integerWidthTooLarge b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.integerWidthTooLarge bits) Miri.ABI.SizeError.zeroWidthUnsignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq (Miri.ABI.SizeError.integerWidthTooLarge bits) Miri.ABI.SizeError.zeroWidthSignedBound = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthUnsignedBound (Miri.ABI.SizeError.u64Overflow operation left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthUnsignedBound (Miri.ABI.SizeError.negativeSubtraction left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthUnsignedBound (Miri.ABI.SizeError.bitCountOverflow bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthUnsignedBound (Miri.ABI.SizeError.integerWidthTooLarge bits) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthUnsignedBound Miri.ABI.SizeError.zeroWidthUnsignedBound = isTrue ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthUnsignedBound Miri.ABI.SizeError.zeroWidthSignedBound = isFalse Miri.ABI.instDecidableEqSizeError.decEq._proof_36
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthSignedBound (Miri.ABI.SizeError.u64Overflow operation left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthSignedBound (Miri.ABI.SizeError.negativeSubtraction left right) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthSignedBound (Miri.ABI.SizeError.bitCountOverflow bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthSignedBound (Miri.ABI.SizeError.integerWidthTooLarge bits) = isFalse ⋯
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthSignedBound Miri.ABI.SizeError.zeroWidthUnsignedBound = isFalse Miri.ABI.instDecidableEqSizeError.decEq._proof_41
• Miri.ABI.instDecidableEqSizeError.decEq Miri.ABI.SizeError.zeroWidthSignedBound Miri.ABI.SizeError.zeroWidthSignedBound = isTrue ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqSizeError : DecidableEq SizeError

Equations

• Miri.ABI.instDecidableEqSizeError = Miri.ABI.instDecidableEqSizeError.decEq

@[instance_reducible]

instance Miri.ABI.instToStringSizeError : ToString SizeError

Equations

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

structure Miri.ABI.Size : Type

• bytes : UInt64

def Miri.ABI.instDecidableEqSize.decEq (x✝ x✝¹ : Size) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqSize.decEq { bytes := a } { bytes := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqSize : DecidableEq Size

Equations

• Miri.ABI.instDecidableEqSize = Miri.ABI.instDecidableEqSize.decEq

@[instance_reducible]

instance Miri.ABI.instReprSize : Repr Size

Equations

• Miri.ABI.instReprSize = { reprPrec := Miri.ABI.instReprSize.repr }

def Miri.ABI.instReprSize.repr : Size → Nat → Std.Format

Equations

• Miri.ABI.instReprSize.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "bytes" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.bytes)).group) " }"

@[instance_reducible]

instance Miri.ABI.instInhabitedSize : Inhabited Size

Equations

• Miri.ABI.instInhabitedSize = { default := Miri.ABI.instInhabitedSize.default }

def Miri.ABI.Size.ZERO : Size

Equations

• Miri.ABI.Size.ZERO = { bytes := 0 }

@[inline]

def Miri.ABI.Size.ofBytes (bytes : UInt64) : Size

Equations

• Miri.ABI.Size.ofBytes bytes = { bytes := bytes }

@[inline]

def Miri.ABI.Size.fromBytes (bytes : UInt64) : Size

Equations

• Miri.ABI.Size.fromBytes bytes = Miri.ABI.Size.ofBytes bytes

div_ceil(8) written without the overflowing bits + 7 formulation.

@[inline]

def Miri.ABI.Size.fromBits (bits : UInt64) : Size

Equations

• Miri.ABI.Size.fromBits bits = Miri.ABI.Size.ofBytes (bits / 8 + if (bits % 8 == 0) = true then 0 else 1)

@[inline]

def Miri.ABI.Size.bits (size : Size) : Except SizeError UInt64

Equations

• size.bits = if size.bytes > UInt64.ofNat (18446744073709551615 / 8) then Except.error (Miri.ABI.SizeError.bitCountOverflow size.bytes) else Except.ok (size.bytes * 8)

@[inline]

def Miri.ABI.Size.bitsNat (size : Size) : Except SizeError Nat

Equations

• size.bitsNat = do let __do_lift ← size.bits pure __do_lift.toNat

@[inline]

def Miri.ABI.Size.bytesNat (size : Size) : Nat

Equations

• size.bytesNat = size.bytes.toNat

@[inline]

def Miri.ABI.Size.add (left right : Size) : Except SizeError Size

Equations

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

@[inline]

def Miri.ABI.Size.sub (left right : Size) : Except SizeError Size

Equations

• left.sub right = if left.bytes < right.bytes then Except.error (Miri.ABI.SizeError.negativeSubtraction left.bytes right.bytes) else Except.ok (Miri.ABI.Size.ofBytes (left.bytes - right.bytes))

@[inline]

def Miri.ABI.Size.mul (size : Size) (count : UInt64) : Except SizeError Size

Equations

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

Checked target-layout addition. This mirrors the upstream exclusive bound: the resulting byte count must be strictly less than obj_size_bound().

@[inline]

def Miri.ABI.Size.checkedAdd {α : Type} [HasDataLayout α] (size offset : Size) (cx : α) : Option Size

Equations

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

@[inline]

def Miri.ABI.Size.checkedMul {α : Type} [HasDataLayout α] (size : Size) (count : UInt64) (cx : α) : Option Size

Equations

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

Truncate a u128 value to the low Size.bits bits. The error case corresponds to the upstream primitive's overflowing bits() or shift.

@[inline]

def Miri.ABI.Size.truncate (size : Size) (value : U128) : Except SizeError U128

Equations

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

Truncate to Size.bits and interpret the resulting bits as a signed two's-complement i128.

@[inline]

def Miri.ABI.Size.signExtend (size : Size) (value : U128) : Except SizeError Int

Equations

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

@[inline]

def Miri.ABI.Size.unsignedIntMax (size : Size) : Except SizeError U128

Equations

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

@[inline]

def Miri.ABI.Size.signedIntMin (size : Size) : Except SizeError Int

Equations

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

@[inline]

def Miri.ABI.Size.signedIntMax (size : Size) : Except SizeError Int

Equations

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