The power-of-two alignment primitives from rustc_abi::Align.

Alignments created from target data or byte counts are restricted to the upstream maximum exponent 29. maxAlignedFactor 0 deliberately preserves the upstream exponent 64 sentinel; asking for its byte count is represented as an explicit shift error, while restrictForOffset safely reduces it first.

inductive Miri.ABI.AlignError : Type

• notPowerOfTwo (bytes : UInt64) : AlignError
• tooLarge (bytes : UInt64) : AlignError
• shiftOverflow (pow2 : Nat) : AlignError
• sizeOverflow (size : Size) (mask : UInt64) : AlignError

def Miri.ABI.instReprAlignError.repr : AlignError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprAlignError : Repr AlignError

Equations

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

def Miri.ABI.instDecidableEqAlignError.decEq (x✝ x✝¹ : AlignError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.notPowerOfTwo a) (Miri.ABI.AlignError.notPowerOfTwo b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.notPowerOfTwo bytes) (Miri.ABI.AlignError.tooLarge bytes_1) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.notPowerOfTwo bytes) (Miri.ABI.AlignError.shiftOverflow pow2) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.notPowerOfTwo bytes) (Miri.ABI.AlignError.sizeOverflow size mask) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.tooLarge bytes) (Miri.ABI.AlignError.notPowerOfTwo bytes_1) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.tooLarge a) (Miri.ABI.AlignError.tooLarge b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.tooLarge bytes) (Miri.ABI.AlignError.shiftOverflow pow2) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.tooLarge bytes) (Miri.ABI.AlignError.sizeOverflow size mask) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.shiftOverflow pow2) (Miri.ABI.AlignError.notPowerOfTwo bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.shiftOverflow pow2) (Miri.ABI.AlignError.tooLarge bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.shiftOverflow a) (Miri.ABI.AlignError.shiftOverflow b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.shiftOverflow pow2) (Miri.ABI.AlignError.sizeOverflow size mask) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.sizeOverflow size mask) (Miri.ABI.AlignError.notPowerOfTwo bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.sizeOverflow size mask) (Miri.ABI.AlignError.tooLarge bytes) = isFalse ⋯
• Miri.ABI.instDecidableEqAlignError.decEq (Miri.ABI.AlignError.sizeOverflow size mask) (Miri.ABI.AlignError.shiftOverflow pow2) = isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqAlignError : DecidableEq AlignError

Equations

• Miri.ABI.instDecidableEqAlignError = Miri.ABI.instDecidableEqAlignError.decEq

@[instance_reducible]

instance Miri.ABI.instToStringAlignError : ToString AlignError

Equations

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

structure Miri.ABI.Align : Type

• pow2 : Nat

def Miri.ABI.instDecidableEqAlign.decEq (x✝ x✝¹ : Align) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqAlign : DecidableEq Align

Equations

• Miri.ABI.instDecidableEqAlign = Miri.ABI.instDecidableEqAlign.decEq

def Miri.ABI.instReprAlign.repr : Align → Nat → Std.Format

Equations

• Miri.ABI.instReprAlign.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "pow2" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.pow2)).group) " }"

@[instance_reducible]

instance Miri.ABI.instReprAlign : Repr Align

Equations

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

def Miri.ABI.Align.ONE : Align

Equations

• Miri.ABI.Align.ONE = { pow2 := 0 }

def Miri.ABI.Align.EIGHT : Align

Equations

• Miri.ABI.Align.EIGHT = { pow2 := 3 }

def Miri.ABI.Align.MAX : Align

Equations

• Miri.ABI.Align.MAX = { pow2 := 29 }

@[inline]

def Miri.ABI.Align.fromBytes (bytes : UInt64) : Except AlignError Align

Equations

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

@[inline]

def Miri.ABI.Align.fromBits (bits : UInt64) : Except AlignError Align

Equations

• Miri.ABI.Align.fromBits bits = Miri.ABI.Align.fromBytes (Miri.ABI.Size.fromBits bits).bytes

@[inline]

def Miri.ABI.Align.bytes (align : Align) : Except AlignError UInt64

Equations

• align.bytes = if align.pow2 ≥ 64 then Except.error (Miri.ABI.AlignError.shiftOverflow align.pow2) else Except.ok (UInt64.shiftLeft 1 (UInt64.ofNat align.pow2))

@[inline]

def Miri.ABI.Align.bits (align : Align) : Except AlignError UInt64

Equations

• align.bits = do let __do_lift ← align.bytes pure (__do_lift * 8)

@[inline]

def Miri.ABI.Align.bytesNat (align : Align) : Except AlignError Nat

Equations

• align.bytesNat = do let __do_lift ← align.bytes pure __do_lift.toNat

@[inline]

def Miri.ABI.Align.bitsNat (align : Align) : Except AlignError Nat

Equations

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

@[inline]

def Miri.ABI.Align.maxForTarget (layout : TargetDataLayout) : Align

Equations

• Miri.ABI.Align.maxForTarget layout = { pow2 := min (layout.pointerWidth.bits.toNat - 1) Miri.ABI.Align.MAX.pow2 }

@[inline]

def Miri.ABI.Align.maxAlignedFactor (size : Size) : Align

Equations

• Miri.ABI.Align.maxAlignedFactor size = { pow2 := Miri.ABI.Align.countTrailingZeros✝ size.bytes }

@[inline]

def Miri.ABI.Align.restrictForOffset (align : Align) (size : Size) : Align

Equations

• align.restrictForOffset size = { pow2 := min align.pow2 (Miri.ABI.Align.maxAlignedFactor size).pow2 }

@[inline]

def Miri.ABI.Align.min (left right : Align) : Align

Equations

• left.min right = { pow2 := left.pow2.min right.pow2 }

@[inline]

def Miri.ABI.Align.max (left right : Align) : Align

Equations

• left.max right = { pow2 := left.pow2.max right.pow2 }

ABI-mandated alignment wrapper used by target layout.

structure Miri.ABI.AbiAlign : Type

• abi : Align

@[instance_reducible]

instance Miri.ABI.instDecidableEqAbiAlign : DecidableEq AbiAlign

Equations

• Miri.ABI.instDecidableEqAbiAlign = Miri.ABI.instDecidableEqAbiAlign.decEq

def Miri.ABI.instDecidableEqAbiAlign.decEq (x✝ x✝¹ : AbiAlign) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.ABI.instReprAbiAlign.repr : AbiAlign → Nat → Std.Format

Equations

• Miri.ABI.instReprAbiAlign.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "abi" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.abi)).group) " }"

@[instance_reducible]

instance Miri.ABI.instReprAbiAlign : Repr AbiAlign

Equations

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

@[inline]

def Miri.ABI.AbiAlign.new (align : Align) : AbiAlign

Equations

• Miri.ABI.AbiAlign.new align = { abi := align }

@[inline]

def Miri.ABI.AbiAlign.min (left right : AbiAlign) : AbiAlign

Equations

• left.min right = { abi := left.abi.min right.abi }

@[inline]

def Miri.ABI.AbiAlign.max (left right : AbiAlign) : AbiAlign

Equations

• left.max right = { abi := left.abi.max right.abi }

@[inline]

def Miri.ABI.Size.alignTo (size : Size) (align : Align) : Except AlignError Size

Equations

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

@[inline]

def Miri.ABI.Size.isAligned (size : Size) (align : Align) : Except AlignError Bool

Equations

• size.isAligned align = do let alignmentBytes ← align.bytes have mask : UInt64 := alignmentBytes - 1 pure (size.bytes.land mask == 0)