Source-shaped scalar and backend runtime-layout representations from pinned rustc_abi. RuntimeTargetDataLayout is a complete extension of the existing arithmetic TargetDataLayout: it stores that view once and requires the source alignment and pointer-space details used by these APIs. Unknown address spaces and malformed Lean alignments are explicit errors.

structure Miri.ABI.AddressSpace : Type

• value : UInt32

def Miri.ABI.instDecidableEqAddressSpace.decEq (x✝ x✝¹ : AddressSpace) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqAddressSpace : DecidableEq AddressSpace

Equations

• Miri.ABI.instDecidableEqAddressSpace = Miri.ABI.instDecidableEqAddressSpace.decEq

def Miri.ABI.instReprAddressSpace.repr : AddressSpace → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprAddressSpace : Repr AddressSpace

Equations

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

@[instance_reducible]

instance Miri.ABI.instInhabitedAddressSpace : Inhabited AddressSpace

Equations

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

def Miri.ABI.AddressSpace.ZERO : AddressSpace

Equations

• Miri.ABI.AddressSpace.ZERO = { value := 0 }

def Miri.ABI.AddressSpace.GPU_CONSTANT : AddressSpace

Equations

• Miri.ABI.AddressSpace.GPU_CONSTANT = { value := 4 }

def Miri.ABI.AddressSpace.GPU_WORKGROUP : AddressSpace

Equations

• Miri.ABI.AddressSpace.GPU_WORKGROUP = { value := 3 }

inductive Miri.ABI.Integer : Type

• I8 : Integer
• I16 : Integer
• I32 : Integer
• I64 : Integer
• I128 : Integer

@[instance_reducible]

instance Miri.ABI.instDecidableEqInteger : DecidableEq Integer

Equations

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

def Miri.ABI.instReprInteger.repr : Integer → Nat → Std.Format

Equations

• Miri.ABI.instReprInteger.repr Miri.ABI.Integer.I8 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Integer.I8")).group prec✝
• Miri.ABI.instReprInteger.repr Miri.ABI.Integer.I16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Integer.I16")).group prec✝
• Miri.ABI.instReprInteger.repr Miri.ABI.Integer.I32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Integer.I32")).group prec✝
• Miri.ABI.instReprInteger.repr Miri.ABI.Integer.I64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Integer.I64")).group prec✝
• Miri.ABI.instReprInteger.repr Miri.ABI.Integer.I128 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Integer.I128")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprInteger : Repr Integer

Equations

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

@[instance_reducible]

instance Miri.ABI.instInhabitedInteger : Inhabited Integer

Equations

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

inductive Miri.ABI.Float : Type

• F16 : Float
• F16B : Float
• F32 : Float
• F64 : Float
• F128 : Float
• PpcF128 : Float

@[instance_reducible]

instance Miri.ABI.instDecidableEqFloat : DecidableEq Float

Equations

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

def Miri.ABI.instReprFloat.repr : Float → Nat → Std.Format

Equations

• Miri.ABI.instReprFloat.repr Miri.ABI.Float.F16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Float.F16")).group prec✝
• Miri.ABI.instReprFloat.repr Miri.ABI.Float.F16B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Float.F16B")).group prec✝
• Miri.ABI.instReprFloat.repr Miri.ABI.Float.F32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Float.F32")).group prec✝
• Miri.ABI.instReprFloat.repr Miri.ABI.Float.F64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Float.F64")).group prec✝
• Miri.ABI.instReprFloat.repr Miri.ABI.Float.F128 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Float.F128")).group prec✝
• Miri.ABI.instReprFloat.repr Miri.ABI.Float.PpcF128 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Float.PpcF128")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprFloat : Repr Float

Equations

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

@[instance_reducible]

instance Miri.ABI.instInhabitedFloat : Inhabited Float

Equations

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

structure Miri.ABI.PointerSpec : Type

Pointer representation for one data address space, matching the source. pointerOffset can differ from the stored pointer size.

• pointerSize : Size
• pointerAlign : Align
• pointerOffset : Size
• isFat : Bool

@[instance_reducible]

instance Miri.ABI.instDecidableEqPointerSpec : DecidableEq PointerSpec

Equations

• Miri.ABI.instDecidableEqPointerSpec = Miri.ABI.instDecidableEqPointerSpec.decEq

def Miri.ABI.instDecidableEqPointerSpec.decEq (x✝ x✝¹ : PointerSpec) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprPointerSpec : Repr PointerSpec

Equations

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

def Miri.ABI.instReprPointerSpec.repr : PointerSpec → Nat → Std.Format

Equations

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

structure Miri.ABI.RuntimeTargetDataLayout : Type

Data needed by scalar runtime-layout methods in rustc_abi. base retains the existing target endian and object-size bound. Every alignment is supplied by the caller, and address spaces are explicit.

• base : TargetDataLayout
• i1Align : Align
• i8Align : Align
• i16Align : Align
• i32Align : Align
• i64Align : Align
• i128Align : Align
• f16Align : Align
• f32Align : Align
• f64Align : Align
• f128Align : Align
• aggregateAlign : Align
• vectorAlign : Array (Size × Align)
• defaultAddressSpace : AddressSpace
• defaultAddressSpacePointerSpec : PointerSpec
• addressSpaceInfo : Array (AddressSpace × PointerSpec)
• instructionAddressSpace : AddressSpace
• cEnumMinSize : Integer

def Miri.ABI.instDecidableEqRuntimeTargetDataLayout.decEq (x✝ x✝¹ : RuntimeTargetDataLayout) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqRuntimeTargetDataLayout : DecidableEq RuntimeTargetDataLayout

Equations

• Miri.ABI.instDecidableEqRuntimeTargetDataLayout = Miri.ABI.instDecidableEqRuntimeTargetDataLayout.decEq

def Miri.ABI.instReprRuntimeTargetDataLayout.repr : RuntimeTargetDataLayout → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprRuntimeTargetDataLayout : Repr RuntimeTargetDataLayout

Equations

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

inductive Miri.ABI.RuntimeLayoutError : Type

• invalidAlignment (where_ : String) (error : AlignError) : RuntimeLayoutError
• unknownAddressSpace (addressSpace : AddressSpace) : RuntimeLayoutError
• sizeFailure (error : SizeError) : RuntimeLayoutError
• unsupportedPointerOffsetWidth (size : Size) : RuntimeLayoutError
• unsupportedObjectSizePointerWidth (size : Size) : RuntimeLayoutError
• targetPointerWidthMismatch (configured : PointerWidth) (size : Size) : RuntimeLayoutError
• duplicateAddressSpace (addressSpace : AddressSpace) : RuntimeLayoutError
• missingInstructionAddressSpace (addressSpace : AddressSpace) : RuntimeLayoutError
• duplicateVectorSize (size : Size) : RuntimeLayoutError
• vectorAlignmentOverflow (size : Size) : RuntimeLayoutError

def Miri.ABI.instDecidableEqRuntimeLayoutError.decEq (x✝ x✝¹ : RuntimeLayoutError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqRuntimeLayoutError : DecidableEq RuntimeLayoutError

Equations

• Miri.ABI.instDecidableEqRuntimeLayoutError = Miri.ABI.instDecidableEqRuntimeLayoutError.decEq

def Miri.ABI.instReprRuntimeLayoutError.repr : RuntimeLayoutError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprRuntimeLayoutError : Repr RuntimeLayoutError

Equations

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

@[instance_reducible]

instance Miri.ABI.instToStringRuntimeLayoutError : ToString RuntimeLayoutError

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.default : RuntimeTargetDataLayout

The actual rustc_abi default layout, represented with the existing 64-bit arithmetic view. This is an explicit fixture, not a fallback for missing target alignment or address-space data.

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.validateAlign (where_ : String) (align : Align) : Except RuntimeLayoutError Unit

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.validate (layout : RuntimeTargetDataLayout) : Except RuntimeLayoutError Unit

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.cVectorAlign (layout : RuntimeTargetDataLayout) (vecSize : Size) : Option Align

Equations

• layout.cVectorAlign vecSize = Option.map Prod.snd (Array.find? (fun (entry : Miri.ABI.Size × Miri.ABI.Align) => entry.fst == vecSize) layout.vectorAlign)

def Miri.ABI.RuntimeTargetDataLayout.rustVectorAlign (layout : RuntimeTargetDataLayout) (vecSize : Size) : Except RuntimeLayoutError Align

Rust's source fallback is bytes.next_power_of_two() followed by an alignment unwrap. The Lean result makes both source panic points explicit.

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.pointerSpecIn (layout : RuntimeTargetDataLayout) (space : AddressSpace) : Except RuntimeLayoutError PointerSpec

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.pointerSizeIn (layout : RuntimeTargetDataLayout) (space : AddressSpace) : Except RuntimeLayoutError Size

Equations

• layout.pointerSizeIn space = do let __do_lift ← layout.pointerSpecIn space pure __do_lift.pointerSize

def Miri.ABI.RuntimeTargetDataLayout.pointerSize (layout : RuntimeTargetDataLayout) : Size

Equations

• layout.pointerSize = layout.defaultAddressSpacePointerSpec.pointerSize

def Miri.ABI.RuntimeTargetDataLayout.pointerOffsetIn (layout : RuntimeTargetDataLayout) (space : AddressSpace) : Except RuntimeLayoutError Size

Equations

• layout.pointerOffsetIn space = do let __do_lift ← layout.pointerSpecIn space pure __do_lift.pointerOffset

def Miri.ABI.RuntimeTargetDataLayout.pointerOffset (layout : RuntimeTargetDataLayout) : Size

Equations

• layout.pointerOffset = layout.defaultAddressSpacePointerSpec.pointerOffset

def Miri.ABI.RuntimeTargetDataLayout.pointerAlignIn (layout : RuntimeTargetDataLayout) (space : AddressSpace) : Except RuntimeLayoutError AbiAlign

Equations

• layout.pointerAlignIn space = do let spec ← layout.pointerSpecIn space Miri.ABI.RuntimeTargetDataLayout.validateAlign "pointer" spec.pointerAlign pure (Miri.ABI.AbiAlign.new spec.pointerAlign)

def Miri.ABI.RuntimeTargetDataLayout.pointerAlign (layout : RuntimeTargetDataLayout) : Except RuntimeLayoutError AbiAlign

Equations

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

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

Equations

• layout.objSizeBound = layout.base.objSizeBound

def Miri.ABI.RuntimeTargetDataLayout.ptrSizedIntegerIn (layout : RuntimeTargetDataLayout) (space : AddressSpace) : Except RuntimeLayoutError Integer

Equations

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

def Miri.ABI.RuntimeTargetDataLayout.ptrSizedInteger (layout : RuntimeTargetDataLayout) : Except RuntimeLayoutError Integer

Equations

• layout.ptrSizedInteger = layout.ptrSizedIntegerIn layout.defaultAddressSpace

Full runtime-layout contexts extend, rather than replace, the target view already used by Size's target-dependent arithmetic.

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

• dataLayout : α → TargetDataLayout
• runtimeDataLayout : α → RuntimeTargetDataLayout

@[instance_reducible]

instance Miri.ABI.instHasRuntimeDataLayoutRuntimeTargetDataLayout : HasRuntimeDataLayout RuntimeTargetDataLayout

Equations

• Miri.ABI.instHasRuntimeDataLayoutRuntimeTargetDataLayout = { dataLayout := Miri.ABI.RuntimeTargetDataLayout.base, runtimeDataLayout := id }

inductive Miri.ABI.IntegerType : Type

• Pointer (signed : Bool) : IntegerType
• Fixed (integer : Integer) (signed : Bool) : IntegerType

@[instance_reducible]

instance Miri.ABI.instDecidableEqIntegerType : DecidableEq IntegerType

Equations

• Miri.ABI.instDecidableEqIntegerType = Miri.ABI.instDecidableEqIntegerType.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqIntegerType.decEq (Miri.ABI.IntegerType.Pointer a) (Miri.ABI.IntegerType.Pointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqIntegerType.decEq (Miri.ABI.IntegerType.Pointer signed) (Miri.ABI.IntegerType.Fixed integer signed_1) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerType.decEq (Miri.ABI.IntegerType.Fixed integer signed) (Miri.ABI.IntegerType.Pointer signed_1) = isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instReprIntegerType : Repr IntegerType

Equations

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

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

Equations

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

def Miri.ABI.IntegerType.isSigned : IntegerType → Bool

Equations

• (Miri.ABI.IntegerType.Pointer a).isSigned = a
• (Miri.ABI.IntegerType.Fixed a a_1).isSigned = a_1

inductive Miri.ABI.IntegerError : Type

• layout (error : RuntimeLayoutError) : IntegerError
• size (error : SizeError) : IntegerError
• unsupportedBitWidth (bits : UInt64) : IntegerError

@[instance_reducible]

instance Miri.ABI.instDecidableEqIntegerError : DecidableEq IntegerError

Equations

• Miri.ABI.instDecidableEqIntegerError = Miri.ABI.instDecidableEqIntegerError.decEq

def Miri.ABI.instDecidableEqIntegerError.decEq (x✝ x✝¹ : IntegerError) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.layout a) (Miri.ABI.IntegerError.layout b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.layout error) (Miri.ABI.IntegerError.size error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.layout error) (Miri.ABI.IntegerError.unsupportedBitWidth bits) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.size error) (Miri.ABI.IntegerError.layout error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.size a) (Miri.ABI.IntegerError.size b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.size error) (Miri.ABI.IntegerError.unsupportedBitWidth bits) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.unsupportedBitWidth bits) (Miri.ABI.IntegerError.layout error) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.unsupportedBitWidth bits) (Miri.ABI.IntegerError.size error) = isFalse ⋯
• Miri.ABI.instDecidableEqIntegerError.decEq (Miri.ABI.IntegerError.unsupportedBitWidth a) (Miri.ABI.IntegerError.unsupportedBitWidth b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.ABI.instReprIntegerError.repr : IntegerError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprIntegerError : Repr IntegerError

Equations

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

@[instance_reducible]

instance Miri.ABI.instToStringIntegerError : ToString IntegerError

Equations

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

def Miri.ABI.Integer.intTyStr : Integer → String

Equations

• Miri.ABI.Integer.I8.intTyStr = "i8"
• Miri.ABI.Integer.I16.intTyStr = "i16"
• Miri.ABI.Integer.I32.intTyStr = "i32"
• Miri.ABI.Integer.I64.intTyStr = "i64"
• Miri.ABI.Integer.I128.intTyStr = "i128"

def Miri.ABI.Integer.uintTyStr : Integer → String

Equations

• Miri.ABI.Integer.I8.uintTyStr = "u8"
• Miri.ABI.Integer.I16.uintTyStr = "u16"
• Miri.ABI.Integer.I32.uintTyStr = "u32"
• Miri.ABI.Integer.I64.uintTyStr = "u64"
• Miri.ABI.Integer.I128.uintTyStr = "u128"

def Miri.ABI.Integer.size : Integer → Size

Equations

• Miri.ABI.Integer.I8.size = Miri.ABI.Size.ofBytes 1
• Miri.ABI.Integer.I16.size = Miri.ABI.Size.ofBytes 2
• Miri.ABI.Integer.I32.size = Miri.ABI.Size.ofBytes 4
• Miri.ABI.Integer.I64.size = Miri.ABI.Size.ofBytes 8
• Miri.ABI.Integer.I128.size = Miri.ABI.Size.ofBytes 16

def Miri.ABI.Integer.align {α : Type} [HasRuntimeDataLayout α] (integer : Integer) (cx : α) : Except RuntimeLayoutError AbiAlign

Equations

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

def Miri.ABI.Integer.fromAttr {α : Type} [HasRuntimeDataLayout α] (cx : α) (ity : IntegerType) : Except IntegerError Integer

Equations

• Miri.ABI.Integer.fromAttr cx (Miri.ABI.IntegerType.Pointer a) = Except.mapError Miri.ABI.IntegerError.layout (Miri.ABI.HasRuntimeDataLayout.runtimeDataLayout cx).ptrSizedInteger
• Miri.ABI.Integer.fromAttr cx (Miri.ABI.IntegerType.Fixed a a_1) = Except.ok a

def Miri.ABI.Integer.signedMax : Integer → Int

Equations

• Miri.ABI.Integer.I8.signedMax = 127
• Miri.ABI.Integer.I16.signedMax = 32767
• Miri.ABI.Integer.I32.signedMax = 2147483647
• Miri.ABI.Integer.I64.signedMax = 9223372036854775807
• Miri.ABI.Integer.I128.signedMax = 170141183460469231731687303715884105727

def Miri.ABI.Integer.signedMin : Integer → Int

Equations

• Miri.ABI.Integer.I8.signedMin = -128
• Miri.ABI.Integer.I16.signedMin = -32768
• Miri.ABI.Integer.I32.signedMin = -2147483648
• Miri.ABI.Integer.I64.signedMin = -9223372036854775808
• Miri.ABI.Integer.I128.signedMin = -170141183460469231731687303715884105728

def Miri.ABI.Integer.fitSigned (value : Int) : Integer

Equations

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

def Miri.ABI.Integer.fitUnsigned (value : U128) : Integer

Equations

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

def Miri.ABI.Integer.forAlign {α : Type} [HasRuntimeDataLayout α] (cx : α) (wanted : Align) : Except RuntimeLayoutError (Option Integer)

Equations

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

def Miri.ABI.Integer.approximateAlign {α : Type} [HasRuntimeDataLayout α] (cx : α) (wanted : Align) : Except RuntimeLayoutError Integer

Equations

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

def Miri.ABI.Integer.fromSize (size : Size) : Except IntegerError Integer

Equations

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

def Miri.ABI.Float.size : Float → Size

Equations

• Miri.ABI.Float.F16.size = Miri.ABI.Size.ofBytes 2
• Miri.ABI.Float.F16B.size = Miri.ABI.Size.ofBytes 2
• Miri.ABI.Float.F32.size = Miri.ABI.Size.ofBytes 4
• Miri.ABI.Float.F64.size = Miri.ABI.Size.ofBytes 8
• Miri.ABI.Float.F128.size = Miri.ABI.Size.ofBytes 16
• Miri.ABI.Float.PpcF128.size = Miri.ABI.Size.ofBytes 16

def Miri.ABI.Float.align {α : Type} [HasRuntimeDataLayout α] (float : Float) (cx : α) : Except RuntimeLayoutError AbiAlign

Equations

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

def Miri.ABI.Float.tyStr : Float → String

Equations

• Miri.ABI.Float.F16.tyStr = "f16"
• Miri.ABI.Float.F16B.tyStr = "f16b"
• Miri.ABI.Float.F32.tyStr = "f32"
• Miri.ABI.Float.F64.tyStr = "f64"
• Miri.ABI.Float.F128.tyStr = "f128"
• Miri.ABI.Float.PpcF128.tyStr = "ppcf128"

inductive Miri.ABI.Primitive : Type

• Int (integer : Integer) (signed : Bool) : Primitive
• Float (float : ABI.Float) : Primitive
• Pointer (addressSpace : AddressSpace) : Primitive

@[instance_reducible]

instance Miri.ABI.instDecidableEqPrimitive : DecidableEq Primitive

Equations

• Miri.ABI.instDecidableEqPrimitive = Miri.ABI.instDecidableEqPrimitive.decEq

def Miri.ABI.instDecidableEqPrimitive.decEq (x✝ x✝¹ : Primitive) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Int a a_1) (Miri.ABI.Primitive.Int b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Int integer signed) (Miri.ABI.Primitive.Float float) = isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Int integer signed) (Miri.ABI.Primitive.Pointer addressSpace) = isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Float float) (Miri.ABI.Primitive.Int integer signed) = isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Float a) (Miri.ABI.Primitive.Float b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Float float) (Miri.ABI.Primitive.Pointer addressSpace) = isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Pointer addressSpace) (Miri.ABI.Primitive.Int integer signed) = isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Pointer addressSpace) (Miri.ABI.Primitive.Float float) = isFalse ⋯
• Miri.ABI.instDecidableEqPrimitive.decEq (Miri.ABI.Primitive.Pointer a) (Miri.ABI.Primitive.Pointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instReprPrimitive : Repr Primitive

Equations

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

def Miri.ABI.instReprPrimitive.repr : Primitive → Nat → Std.Format

Equations

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

inductive Miri.ABI.RegKind : Type

• Integer : RegKind
• Float : RegKind
• PpcF128 : RegKind
• Vector {hintVectorElem : Primitive} : RegKind

def Miri.ABI.instDecidableEqRegKind.decEq (x✝ x✝¹ : RegKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Integer Miri.ABI.RegKind.Integer = isTrue ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Integer Miri.ABI.RegKind.Float = isFalse Miri.ABI.instDecidableEqRegKind.decEq._proof_1
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Integer Miri.ABI.RegKind.PpcF128 = isFalse Miri.ABI.instDecidableEqRegKind.decEq._proof_2
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Integer Miri.ABI.RegKind.Vector = isFalse ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Float Miri.ABI.RegKind.Integer = isFalse Miri.ABI.instDecidableEqRegKind.decEq._proof_4
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Float Miri.ABI.RegKind.Float = isTrue ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Float Miri.ABI.RegKind.PpcF128 = isFalse Miri.ABI.instDecidableEqRegKind.decEq._proof_5
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Float Miri.ABI.RegKind.Vector = isFalse ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.PpcF128 Miri.ABI.RegKind.Integer = isFalse Miri.ABI.instDecidableEqRegKind.decEq._proof_7
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.PpcF128 Miri.ABI.RegKind.Float = isFalse Miri.ABI.instDecidableEqRegKind.decEq._proof_8
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.PpcF128 Miri.ABI.RegKind.PpcF128 = isTrue ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.PpcF128 Miri.ABI.RegKind.Vector = isFalse ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Vector Miri.ABI.RegKind.Integer = isFalse ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Vector Miri.ABI.RegKind.Float = isFalse ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Vector Miri.ABI.RegKind.PpcF128 = isFalse ⋯
• Miri.ABI.instDecidableEqRegKind.decEq Miri.ABI.RegKind.Vector Miri.ABI.RegKind.Vector = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqRegKind : DecidableEq RegKind

Equations

• Miri.ABI.instDecidableEqRegKind = Miri.ABI.instDecidableEqRegKind.decEq

def Miri.ABI.instReprRegKind.repr : RegKind → Nat → Std.Format

Equations

• Miri.ABI.instReprRegKind.repr Miri.ABI.RegKind.Integer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.RegKind.Integer")).group prec✝
• Miri.ABI.instReprRegKind.repr Miri.ABI.RegKind.Float prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.RegKind.Float")).group prec✝
• Miri.ABI.instReprRegKind.repr Miri.ABI.RegKind.PpcF128 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.RegKind.PpcF128")).group prec✝
• Miri.ABI.instReprRegKind.repr Miri.ABI.RegKind.Vector prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.RegKind.Vector")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprRegKind : Repr RegKind

Equations

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

def Miri.ABI.RegKind.fromPrimitive : Primitive → RegKind

Equations

• Miri.ABI.RegKind.fromPrimitive (Miri.ABI.Primitive.Int integer signed) = Miri.ABI.RegKind.Integer
• Miri.ABI.RegKind.fromPrimitive (Miri.ABI.Primitive.Pointer addressSpace) = Miri.ABI.RegKind.Integer
• Miri.ABI.RegKind.fromPrimitive (Miri.ABI.Primitive.Float Miri.ABI.Float.PpcF128) = Miri.ABI.RegKind.PpcF128
• Miri.ABI.RegKind.fromPrimitive (Miri.ABI.Primitive.Float float) = Miri.ABI.RegKind.Float

inductive Miri.ABI.Numeric : Type

• Int (integer : Integer) (signed : Bool) : Numeric
• Float (float : ABI.Float) : Numeric

def Miri.ABI.instDecidableEqNumeric.decEq (x✝ x✝¹ : Numeric) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqNumeric.decEq (Miri.ABI.Numeric.Int a a_1) (Miri.ABI.Numeric.Int b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqNumeric.decEq (Miri.ABI.Numeric.Int integer signed) (Miri.ABI.Numeric.Float float) = isFalse ⋯
• Miri.ABI.instDecidableEqNumeric.decEq (Miri.ABI.Numeric.Float float) (Miri.ABI.Numeric.Int integer signed) = isFalse ⋯
• Miri.ABI.instDecidableEqNumeric.decEq (Miri.ABI.Numeric.Float a) (Miri.ABI.Numeric.Float b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqNumeric : DecidableEq Numeric

Equations

• Miri.ABI.instDecidableEqNumeric = Miri.ABI.instDecidableEqNumeric.decEq

@[instance_reducible]

instance Miri.ABI.instReprNumeric : Repr Numeric

Equations

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

def Miri.ABI.instReprNumeric.repr : Numeric → Nat → Std.Format

Equations

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

def Miri.ABI.Numeric.size : Numeric → Size

Equations

• (Miri.ABI.Numeric.Int a a_1).size = a.size
• (Miri.ABI.Numeric.Float a).size = a.size

def Miri.ABI.Numeric.regKind : Numeric → RegKind

Equations

• (Miri.ABI.Numeric.Int integer signed).regKind = Miri.ABI.RegKind.Integer
• (Miri.ABI.Numeric.Float Miri.ABI.Float.PpcF128).regKind = Miri.ABI.RegKind.PpcF128
• (Miri.ABI.Numeric.Float float).regKind = Miri.ABI.RegKind.Float

structure Miri.ABI.Reg : Type

• kind : RegKind
• size : Size

@[instance_reducible]

instance Miri.ABI.instDecidableEqReg : DecidableEq Reg

Equations

• Miri.ABI.instDecidableEqReg = Miri.ABI.instDecidableEqReg.decEq

def Miri.ABI.instDecidableEqReg.decEq (x✝ x✝¹ : Reg) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqReg.decEq { kind := a, size := a_1 } { kind := b, size := 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.ABI.instReprReg : Repr Reg

Equations

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

def Miri.ABI.instReprReg.repr : Reg → Nat → Std.Format

Equations

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

inductive Miri.ABI.RegLayoutError : Type

• size (error : SizeError) : RegLayoutError
• runtime (error : RuntimeLayoutError) : RegLayoutError
• unsupportedIntegerWidth (bits : UInt64) : RegLayoutError
• unsupportedFloatWidth (bits : UInt64) : RegLayoutError

@[instance_reducible]

instance Miri.ABI.instDecidableEqRegLayoutError : DecidableEq RegLayoutError

Equations

• Miri.ABI.instDecidableEqRegLayoutError = Miri.ABI.instDecidableEqRegLayoutError.decEq

def Miri.ABI.instDecidableEqRegLayoutError.decEq (x✝ x✝¹ : RegLayoutError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.size a) (Miri.ABI.RegLayoutError.size b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.size error) (Miri.ABI.RegLayoutError.runtime error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.size error) (Miri.ABI.RegLayoutError.unsupportedIntegerWidth bits) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.size error) (Miri.ABI.RegLayoutError.unsupportedFloatWidth bits) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.runtime error) (Miri.ABI.RegLayoutError.size error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.runtime a) (Miri.ABI.RegLayoutError.runtime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.runtime error) (Miri.ABI.RegLayoutError.unsupportedIntegerWidth bits) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.runtime error) (Miri.ABI.RegLayoutError.unsupportedFloatWidth bits) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedIntegerWidth bits) (Miri.ABI.RegLayoutError.size error) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedIntegerWidth bits) (Miri.ABI.RegLayoutError.runtime error) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedIntegerWidth bits) (Miri.ABI.RegLayoutError.unsupportedFloatWidth bits_1) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedFloatWidth bits) (Miri.ABI.RegLayoutError.size error) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedFloatWidth bits) (Miri.ABI.RegLayoutError.runtime error) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedFloatWidth bits) (Miri.ABI.RegLayoutError.unsupportedIntegerWidth bits_1) = isFalse ⋯
• Miri.ABI.instDecidableEqRegLayoutError.decEq (Miri.ABI.RegLayoutError.unsupportedFloatWidth a) (Miri.ABI.RegLayoutError.unsupportedFloatWidth b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.ABI.instReprRegLayoutError.repr : RegLayoutError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprRegLayoutError : Repr RegLayoutError

Equations

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

def Miri.ABI.Reg.i8 : Reg

Equations

• Miri.ABI.Reg.i8 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Integer 8

def Miri.ABI.Reg.i16 : Reg

Equations

• Miri.ABI.Reg.i16 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Integer 16

def Miri.ABI.Reg.i32 : Reg

Equations

• Miri.ABI.Reg.i32 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Integer 32

def Miri.ABI.Reg.i64 : Reg

Equations

• Miri.ABI.Reg.i64 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Integer 64

def Miri.ABI.Reg.i128 : Reg

Equations

• Miri.ABI.Reg.i128 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Integer 128

def Miri.ABI.Reg.f16 : Reg

Equations

• Miri.ABI.Reg.f16 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Float 16

def Miri.ABI.Reg.f32 : Reg

Equations

• Miri.ABI.Reg.f32 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Float 32

def Miri.ABI.Reg.f64 : Reg

Equations

• Miri.ABI.Reg.f64 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Float 64

def Miri.ABI.Reg.f128 : Reg

Equations

• Miri.ABI.Reg.f128 = Miri.ABI.Reg.numeric✝ Miri.ABI.RegKind.Float 128

def Miri.ABI.Reg.opaqueVector (size : Size) : Reg

Equations

• Miri.ABI.Reg.opaqueVector size = { kind := Miri.ABI.RegKind.Vector, size := size }

def Miri.ABI.Reg.align {α : Type} [HasRuntimeDataLayout α] (reg : Reg) (cx : α) : Except RegLayoutError Align

Equations

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

def Miri.ABI.Primitive.size {α : Type} [HasRuntimeDataLayout α] (primitive : Primitive) (cx : α) : Except RuntimeLayoutError Size

Equations

• (Miri.ABI.Primitive.Int a a_1).size cx = pure a.size
• (Miri.ABI.Primitive.Float a).size cx = pure a.size
• (Miri.ABI.Primitive.Pointer a).size cx = (Miri.ABI.HasRuntimeDataLayout.runtimeDataLayout cx).pointerSizeIn a

def Miri.ABI.Primitive.defaultAlign {α : Type} [HasRuntimeDataLayout α] (primitive : Primitive) (cx : α) : Except RuntimeLayoutError AbiAlign

Equations

• (Miri.ABI.Primitive.Int a a_1).defaultAlign cx = a.align cx
• (Miri.ABI.Primitive.Float a).defaultAlign cx = a.align cx
• (Miri.ABI.Primitive.Pointer a).defaultAlign cx = (Miri.ABI.HasRuntimeDataLayout.runtimeDataLayout cx).pointerAlignIn a

def Miri.ABI.Primitive.regKind : Primitive → RegKind

Equations

• Miri.ABI.Primitive.regKind = Miri.ABI.RegKind.fromPrimitive

inductive Miri.ABI.Scalar : Type

• Initialized {value : Primitive} {validRange : WrappingRange} : Scalar
• Union {value : Primitive} : Scalar

def Miri.ABI.instDecidableEqScalar.decEq (x✝ x✝¹ : Scalar) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqScalar.decEq Miri.ABI.Scalar.Initialized Miri.ABI.Scalar.Initialized = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqScalar.decEq Miri.ABI.Scalar.Initialized Miri.ABI.Scalar.Union = isFalse ⋯
• Miri.ABI.instDecidableEqScalar.decEq Miri.ABI.Scalar.Union Miri.ABI.Scalar.Initialized = isFalse ⋯
• Miri.ABI.instDecidableEqScalar.decEq Miri.ABI.Scalar.Union Miri.ABI.Scalar.Union = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqScalar : DecidableEq Scalar

Equations

• Miri.ABI.instDecidableEqScalar = Miri.ABI.instDecidableEqScalar.decEq

def Miri.ABI.instReprScalar.repr : Scalar → Nat → Std.Format

Equations

• Miri.ABI.instReprScalar.repr Miri.ABI.Scalar.Initialized prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Scalar.Initialized")).group prec✝
• Miri.ABI.instReprScalar.repr Miri.ABI.Scalar.Union prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Scalar.Union")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprScalar : Repr Scalar

Equations

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

inductive Miri.ABI.ScalarLayoutError : Type

• runtimeLayout (error : RuntimeLayoutError) : ScalarLayoutError
• wrappingRange (error : WrappingRangeError) : ScalarLayoutError
• cannotChangeUnionValidRange : ScalarLayoutError

def Miri.ABI.instDecidableEqScalarLayoutError.decEq (x✝ x✝¹ : ScalarLayoutError) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqScalarLayoutError.decEq (Miri.ABI.ScalarLayoutError.runtimeLayout a) (Miri.ABI.ScalarLayoutError.runtimeLayout b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq (Miri.ABI.ScalarLayoutError.runtimeLayout error) (Miri.ABI.ScalarLayoutError.wrappingRange error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq (Miri.ABI.ScalarLayoutError.runtimeLayout error) Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange = isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq (Miri.ABI.ScalarLayoutError.wrappingRange error) (Miri.ABI.ScalarLayoutError.runtimeLayout error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq (Miri.ABI.ScalarLayoutError.wrappingRange a) (Miri.ABI.ScalarLayoutError.wrappingRange b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq (Miri.ABI.ScalarLayoutError.wrappingRange error) Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange = isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange (Miri.ABI.ScalarLayoutError.runtimeLayout error) = isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange (Miri.ABI.ScalarLayoutError.wrappingRange error) = isFalse ⋯
• Miri.ABI.instDecidableEqScalarLayoutError.decEq Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange = isTrue ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqScalarLayoutError : DecidableEq ScalarLayoutError

Equations

• Miri.ABI.instDecidableEqScalarLayoutError = Miri.ABI.instDecidableEqScalarLayoutError.decEq

def Miri.ABI.instReprScalarLayoutError.repr : ScalarLayoutError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprScalarLayoutError : Repr ScalarLayoutError

Equations

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

def Miri.ABI.Scalar.isBool : Scalar → Bool

Equations

• Miri.ABI.Scalar.Initialized.isBool = (range.start == 0 && range.end == 1)
• x✝.isBool = false

def Miri.ABI.Scalar.primitive : Scalar → Primitive

Equations

• Miri.ABI.Scalar.Initialized.primitive = a
• Miri.ABI.Scalar.Union.primitive = a

def Miri.ABI.Scalar.defaultAlign {α : Type} [HasRuntimeDataLayout α] (scalar : Scalar) (cx : α) : Except ScalarLayoutError AbiAlign

Equations

• scalar.defaultAlign cx = Except.mapError Miri.ABI.ScalarLayoutError.runtimeLayout (scalar.primitive.defaultAlign cx)

def Miri.ABI.Scalar.size {α : Type} [HasRuntimeDataLayout α] (scalar : Scalar) (cx : α) : Except ScalarLayoutError Size

Equations

• scalar.size cx = Except.mapError Miri.ABI.ScalarLayoutError.runtimeLayout (scalar.primitive.size cx)

def Miri.ABI.Scalar.toUnion : Scalar → Scalar

Equations

• Miri.ABI.Scalar.Initialized.toUnion = Miri.ABI.Scalar.Union
• Miri.ABI.Scalar.Union.toUnion = Miri.ABI.Scalar.Union

def Miri.ABI.Scalar.validRange {α : Type} [HasRuntimeDataLayout α] (scalar : Scalar) (cx : α) : Except ScalarLayoutError WrappingRange

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.Scalar.Initialized.validRange cx = pure a_1

def Miri.ABI.Scalar.setValidRange (scalar : Scalar) (range : WrappingRange) : Except ScalarLayoutError Scalar

Equations

• Miri.ABI.Scalar.Initialized.setValidRange range = Except.ok Miri.ABI.Scalar.Initialized
• Miri.ABI.Scalar.Union.setValidRange range = Except.error Miri.ABI.ScalarLayoutError.cannotChangeUnionValidRange

def Miri.ABI.Scalar.isAlwaysValid {α : Type} [HasRuntimeDataLayout α] (scalar : Scalar) (cx : α) : Except ScalarLayoutError Bool

Equations

• Miri.ABI.Scalar.Initialized.isAlwaysValid cx = do let size ← Miri.ABI.Scalar.Initialized.size cx Except.mapError Miri.ABI.ScalarLayoutError.wrappingRange (a_1.isFullFor size)
• Miri.ABI.Scalar.Union.isAlwaysValid cx = pure true

def Miri.ABI.Scalar.isUninitValid : Scalar → Bool

Equations

• Miri.ABI.Scalar.Initialized.isUninitValid = false
• Miri.ABI.Scalar.Union.isUninitValid = true

def Miri.ABI.Scalar.isSigned : Scalar → Bool

Equations

• Miri.ABI.Scalar.Initialized.isSigned = signed
• Miri.ABI.Scalar.Union.isSigned = signed
• x✝.isSigned = false

structure Miri.ABI.BackendLaneCount : Type

• value : UInt16

@[instance_reducible]

instance Miri.ABI.instDecidableEqBackendLaneCount : DecidableEq BackendLaneCount

Equations

• Miri.ABI.instDecidableEqBackendLaneCount = Miri.ABI.instDecidableEqBackendLaneCount.decEq

def Miri.ABI.instDecidableEqBackendLaneCount.decEq (x✝ x✝¹ : BackendLaneCount) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.ABI.instReprBackendLaneCount.repr : BackendLaneCount → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprBackendLaneCount : Repr BackendLaneCount

Equations

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

def Miri.ABI.MAX_SIMD_LANES : UInt16

Equations

• Miri.ABI.MAX_SIMD_LANES = 32768

inductive Miri.ABI.BackendLaneCountError : Type

• zeroLength : BackendLaneCountError
• oversized (maxLanes : UInt16) : BackendLaneCountError

@[instance_reducible]

instance Miri.ABI.instDecidableEqBackendLaneCountError : DecidableEq BackendLaneCountError

Equations

• Miri.ABI.instDecidableEqBackendLaneCountError = Miri.ABI.instDecidableEqBackendLaneCountError.decEq

def Miri.ABI.instDecidableEqBackendLaneCountError.decEq (x✝ x✝¹ : BackendLaneCountError) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqBackendLaneCountError.decEq Miri.ABI.BackendLaneCountError.zeroLength Miri.ABI.BackendLaneCountError.zeroLength = isTrue ⋯
• Miri.ABI.instDecidableEqBackendLaneCountError.decEq Miri.ABI.BackendLaneCountError.zeroLength (Miri.ABI.BackendLaneCountError.oversized maxLanes) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendLaneCountError.decEq (Miri.ABI.BackendLaneCountError.oversized maxLanes) Miri.ABI.BackendLaneCountError.zeroLength = isFalse ⋯
• Miri.ABI.instDecidableEqBackendLaneCountError.decEq (Miri.ABI.BackendLaneCountError.oversized a) (Miri.ABI.BackendLaneCountError.oversized b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.ABI.instReprBackendLaneCountError.repr : BackendLaneCountError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprBackendLaneCountError : Repr BackendLaneCountError

Equations

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

def Miri.ABI.BackendLaneCount.new (count : UInt64) : Except BackendLaneCountError BackendLaneCount

Equations

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

def Miri.ABI.BackendLaneCount.isPowerOfTwo (count : BackendLaneCount) : Bool

Equations

• count.isPowerOfTwo = ((Miri.ABI.BackendLaneCount.value✝ count).toNat &&& (Miri.ABI.BackendLaneCount.value✝ count).toNat - 1 == 0)

def Miri.ABI.BackendLaneCount.asU64 (count : BackendLaneCount) : UInt64

Equations

• count.asU64 = (Miri.ABI.BackendLaneCount.value✝ count).toUInt64

def Miri.ABI.BackendLaneCount.asU32 (count : BackendLaneCount) : UInt32

Equations

• count.asU32 = (Miri.ABI.BackendLaneCount.value✝ count).toUInt32

structure Miri.ABI.NumScalableVectors : Type

• value : UInt8

@[instance_reducible]

instance Miri.ABI.instDecidableEqNumScalableVectors : DecidableEq NumScalableVectors

Equations

• Miri.ABI.instDecidableEqNumScalableVectors = Miri.ABI.instDecidableEqNumScalableVectors.decEq

def Miri.ABI.instDecidableEqNumScalableVectors.decEq (x✝ x✝¹ : NumScalableVectors) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprNumScalableVectors : Repr NumScalableVectors

Equations

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

def Miri.ABI.instReprNumScalableVectors.repr : NumScalableVectors → Nat → Std.Format

Equations

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

def Miri.ABI.NumScalableVectors.forNonTuple : NumScalableVectors

Equations

• Miri.ABI.NumScalableVectors.forNonTuple = { value := 1 }

def Miri.ABI.NumScalableVectors.fromFieldCount (count : Nat) : Option NumScalableVectors

Equations

• Miri.ABI.NumScalableVectors.fromFieldCount count = if (decide (2 ≤ count) && decide (count < 8)) = true then some { value := UInt8.ofNat count } else none

inductive Miri.ABI.BackendRepr : Type

• Scalar (scalar : ABI.Scalar) : BackendRepr
• ScalarPair {a b : ABI.Scalar} {bOffset : Size} : BackendRepr
• SimdScalableVector {element : ABI.Scalar} {count : BackendLaneCount} {numberOfVectors : NumScalableVectors} : BackendRepr
• SimdVector {element : ABI.Scalar} {count : BackendLaneCount} : BackendRepr
• Memory {sized : Bool} : BackendRepr

def Miri.ABI.instDecidableEqBackendRepr.decEq (x✝ x✝¹ : BackendRepr) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqBackendRepr.decEq (Miri.ABI.BackendRepr.Scalar a) (Miri.ABI.BackendRepr.Scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq (Miri.ABI.BackendRepr.Scalar scalar) Miri.ABI.BackendRepr.ScalarPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq (Miri.ABI.BackendRepr.Scalar scalar) Miri.ABI.BackendRepr.SimdScalableVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq (Miri.ABI.BackendRepr.Scalar scalar) Miri.ABI.BackendRepr.SimdVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq (Miri.ABI.BackendRepr.Scalar scalar) Miri.ABI.BackendRepr.Memory = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.ScalarPair (Miri.ABI.BackendRepr.Scalar scalar) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.ScalarPair Miri.ABI.BackendRepr.SimdScalableVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.ScalarPair Miri.ABI.BackendRepr.SimdVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.ScalarPair Miri.ABI.BackendRepr.Memory = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdScalableVector (Miri.ABI.BackendRepr.Scalar scalar) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdScalableVector Miri.ABI.BackendRepr.ScalarPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdScalableVector Miri.ABI.BackendRepr.SimdVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdScalableVector Miri.ABI.BackendRepr.Memory = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdVector (Miri.ABI.BackendRepr.Scalar scalar) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdVector Miri.ABI.BackendRepr.ScalarPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdVector Miri.ABI.BackendRepr.SimdScalableVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdVector Miri.ABI.BackendRepr.SimdVector = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.SimdVector Miri.ABI.BackendRepr.Memory = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.Memory (Miri.ABI.BackendRepr.Scalar scalar) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.Memory Miri.ABI.BackendRepr.ScalarPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.Memory Miri.ABI.BackendRepr.SimdScalableVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.Memory Miri.ABI.BackendRepr.SimdVector = isFalse ⋯
• Miri.ABI.instDecidableEqBackendRepr.decEq Miri.ABI.BackendRepr.Memory Miri.ABI.BackendRepr.Memory = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqBackendRepr : DecidableEq BackendRepr

Equations

• Miri.ABI.instDecidableEqBackendRepr = Miri.ABI.instDecidableEqBackendRepr.decEq

def Miri.ABI.instReprBackendRepr.repr : BackendRepr → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprBackendRepr : Repr BackendRepr

Equations

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

inductive Miri.ABI.BackendReprError : Type

• scalar (error : ScalarLayoutError) : BackendReprError
• size (error : SizeError) : BackendReprError
• alignment (error : AlignError) : BackendReprError
• alignmentUnavailableForPair : BackendReprError
• isSignedOnNonScalar : BackendReprError

@[instance_reducible]

instance Miri.ABI.instDecidableEqBackendReprError : DecidableEq BackendReprError

Equations

• Miri.ABI.instDecidableEqBackendReprError = Miri.ABI.instDecidableEqBackendReprError.decEq

def Miri.ABI.instDecidableEqBackendReprError.decEq (x✝ x✝¹ : BackendReprError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.scalar a) (Miri.ABI.BackendReprError.scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.scalar error) (Miri.ABI.BackendReprError.size error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.scalar error) (Miri.ABI.BackendReprError.alignment error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.scalar error) Miri.ABI.BackendReprError.alignmentUnavailableForPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.scalar error) Miri.ABI.BackendReprError.isSignedOnNonScalar = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.size error) (Miri.ABI.BackendReprError.scalar error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.size a) (Miri.ABI.BackendReprError.size b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.size error) (Miri.ABI.BackendReprError.alignment error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.size error) Miri.ABI.BackendReprError.alignmentUnavailableForPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.size error) Miri.ABI.BackendReprError.isSignedOnNonScalar = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.alignment error) (Miri.ABI.BackendReprError.scalar error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.alignment error) (Miri.ABI.BackendReprError.size error_1) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.alignment a) (Miri.ABI.BackendReprError.alignment b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.alignment error) Miri.ABI.BackendReprError.alignmentUnavailableForPair = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq (Miri.ABI.BackendReprError.alignment error) Miri.ABI.BackendReprError.isSignedOnNonScalar = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.alignmentUnavailableForPair (Miri.ABI.BackendReprError.scalar error) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.alignmentUnavailableForPair (Miri.ABI.BackendReprError.size error) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.alignmentUnavailableForPair (Miri.ABI.BackendReprError.alignment error) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.alignmentUnavailableForPair Miri.ABI.BackendReprError.alignmentUnavailableForPair = isTrue ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.isSignedOnNonScalar (Miri.ABI.BackendReprError.scalar error) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.isSignedOnNonScalar (Miri.ABI.BackendReprError.size error) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.isSignedOnNonScalar (Miri.ABI.BackendReprError.alignment error) = isFalse ⋯
• Miri.ABI.instDecidableEqBackendReprError.decEq Miri.ABI.BackendReprError.isSignedOnNonScalar Miri.ABI.BackendReprError.isSignedOnNonScalar = isTrue ⋯

def Miri.ABI.instReprBackendReprError.repr : BackendReprError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprBackendReprError : Repr BackendReprError

Equations

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

def Miri.ABI.BackendRepr.isUnsized : BackendRepr → Bool

Equations

• Miri.ABI.BackendRepr.Memory.isUnsized = !sized
• (Miri.ABI.BackendRepr.Scalar scalar).isUnsized = false
• Miri.ABI.BackendRepr.ScalarPair.isUnsized = false
• Miri.ABI.BackendRepr.SimdScalableVector.isUnsized = false
• Miri.ABI.BackendRepr.SimdVector.isUnsized = false

def Miri.ABI.BackendRepr.isSized (repr : BackendRepr) : Bool

Equations

• repr.isSized = !repr.isUnsized

def Miri.ABI.BackendRepr.isSigned : BackendRepr → Except BackendReprError Bool

Equations

• (Miri.ABI.BackendRepr.Scalar scalar).isSigned = Except.ok scalar.isSigned
• x✝.isSigned = Except.error Miri.ABI.BackendReprError.isSignedOnNonScalar

def Miri.ABI.BackendRepr.isScalar : BackendRepr → Bool

Equations

• (Miri.ABI.BackendRepr.Scalar scalar).isScalar = true
• x✝.isScalar = false

def Miri.ABI.BackendRepr.isScalarOrSimd : BackendRepr → Bool

Equations

• (Miri.ABI.BackendRepr.Scalar scalar).isScalarOrSimd = true
• Miri.ABI.BackendRepr.SimdVector.isScalarOrSimd = true
• Miri.ABI.BackendRepr.SimdScalableVector.isScalarOrSimd = true
• x✝.isScalarOrSimd = false

def Miri.ABI.BackendRepr.isBool : BackendRepr → Bool

Equations

• (Miri.ABI.BackendRepr.Scalar scalar).isBool = scalar.isBool
• x✝.isBool = false

def Miri.ABI.BackendRepr.scalarPlatformAlign {α : Type} [HasRuntimeDataLayout α] (repr : BackendRepr) (cx : α) : Except BackendReprError (Option Align)

Equations

• One or more equations did not get rendered due to their size.
• (Miri.ABI.BackendRepr.Scalar scalar).scalarPlatformAlign cx = do let align ← Except.mapError Miri.ABI.BackendReprError.scalar (scalar.defaultAlign cx) pure (some align.abi)
• Miri.ABI.BackendRepr.SimdVector.scalarPlatformAlign cx = pure none
• Miri.ABI.BackendRepr.Memory.scalarPlatformAlign cx = pure none
• Miri.ABI.BackendRepr.SimdScalableVector.scalarPlatformAlign cx = pure none

def Miri.ABI.BackendRepr.scalarSize {α : Type} [HasRuntimeDataLayout α] (repr : BackendRepr) (cx : α) : Except BackendReprError (Option Size)

Equations

• One or more equations did not get rendered due to their size.
• (Miri.ABI.BackendRepr.Scalar scalar).scalarSize cx = do let __do_lift ← Except.mapError Miri.ABI.BackendReprError.scalar (scalar.size cx) pure (some __do_lift)
• Miri.ABI.BackendRepr.SimdVector.scalarSize cx = pure none
• Miri.ABI.BackendRepr.Memory.scalarSize cx = pure none
• Miri.ABI.BackendRepr.SimdScalableVector.scalarSize cx = pure none

def Miri.ABI.BackendRepr.toUnion : BackendRepr → BackendRepr

Equations

• (Miri.ABI.BackendRepr.Scalar scalar).toUnion = Miri.ABI.BackendRepr.Scalar scalar.toUnion
• Miri.ABI.BackendRepr.ScalarPair.toUnion = Miri.ABI.BackendRepr.ScalarPair
• Miri.ABI.BackendRepr.SimdVector.toUnion = Miri.ABI.BackendRepr.SimdVector
• Miri.ABI.BackendRepr.Memory.toUnion = Miri.ABI.BackendRepr.Memory
• Miri.ABI.BackendRepr.SimdScalableVector.toUnion = Miri.ABI.BackendRepr.SimdScalableVector

def Miri.ABI.BackendRepr.eqUpToValidity : BackendRepr → BackendRepr → Bool

Equations

• (Miri.ABI.BackendRepr.Scalar left).eqUpToValidity (Miri.ABI.BackendRepr.Scalar right) = (left.primitive == right.primitive)
• Miri.ABI.BackendRepr.SimdVector.eqUpToValidity Miri.ABI.BackendRepr.SimdVector = (leftElement.primitive == rightElement.primitive && leftCount == rightCount)
• Miri.ABI.BackendRepr.ScalarPair.eqUpToValidity Miri.ABI.BackendRepr.ScalarPair = (leftA.primitive == rightA.primitive && leftB.primitive == rightB.primitive && leftOffset == rightOffset)
• x✝¹.eqUpToValidity x✝ = (x✝¹ == x✝)