Actual compiler-selected primitive/lang-item/path types. Canonical source query references establish identity; display spelling or layout equality does not. In particular Ordering is tcx.ty_ordering_enum, and c_ulong is the source core::ffi path query, never derived from host or target triple.

def Miri.Input.CompilerPrimitiveFacts.primitiveLayout (runtime : RuntimeMetadata) (key : String) : Except String (ABI.TyAndLayout TypeId)

Read one exact compiler primitive query key; no type-name search occurs.

Equations

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

structure Miri.Input.CompilerPrimitiveFacts.Cache : Type

Exact primitive type references and layouts prepared for repeated hooks. Every entry retains its source-local failure instead of making preparation fail for an unused primitive. The index is tied to one complete immutable runtime value by Bound below.

• primitiveLayouts : Std.HashMap String (Except String (ABI.TyAndLayout TypeId))
• ordering : Except String (ABI.TyAndLayout TypeId)
• callerLocation : Except String TypeId

structure Miri.Input.CompilerPrimitiveFacts.Bound (runtime : RuntimeMetadata) : Type

A prepared primitive table carries an equality certificate to the exact cache derived from the indexed runtime. A record update to another runtime cannot reuse this certificate.

• value : Cache
• exact : self.value = Miri.Input.CompilerPrimitiveFacts.buildCache✝ runtime

def Miri.Input.CompilerPrimitiveFacts.bind (runtime : RuntimeMetadata) : Bound runtime

Equations

• Miri.Input.CompilerPrimitiveFacts.bind runtime = { value := Miri.Input.CompilerPrimitiveFacts.buildCache✝ runtime, exact := ⋯ }

def Miri.Input.CompilerPrimitiveFacts.primitiveLayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) (key : String) : Except String (ABI.TyAndLayout TypeId)

Use cached query outcomes when the requested key was in the source catalog; malformed or absent catalogs keep the original demand-time behavior.

Equations

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

def Miri.Input.CompilerPrimitiveFacts.orderingLayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerPrimitiveFacts.orderingLayoutBound runtime cache = cache.value.ordering

def Miri.Input.CompilerPrimitiveFacts.callerLocationTypeBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String TypeId

Equations

• Miri.Input.CompilerPrimitiveFacts.callerLocationTypeBound runtime cache = cache.value.callerLocation

def Miri.Input.CompilerPrimitiveFacts.u32LayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerPrimitiveFacts.u32LayoutBound runtime cache = Miri.Input.CompilerPrimitiveFacts.primitiveLayoutBound runtime cache "u32"

def Miri.Input.CompilerPrimitiveFacts.usizeLayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerPrimitiveFacts.usizeLayoutBound runtime cache = Miri.Input.CompilerPrimitiveFacts.primitiveLayoutBound runtime cache "usize"

def Miri.Input.CompilerPrimitiveFacts.unitLayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerPrimitiveFacts.unitLayoutBound runtime cache = Miri.Input.CompilerPrimitiveFacts.primitiveLayoutBound runtime cache "unit"

def Miri.Input.CompilerPrimitiveFacts.unitPointerConstLayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerPrimitiveFacts.unitPointerConstLayoutBound runtime cache = Miri.Input.CompilerPrimitiveFacts.primitiveLayoutBound runtime cache "unit_pointer_const"

def Miri.Input.CompilerPrimitiveFacts.unitPointerMutLayoutBound (runtime : RuntimeMetadata) (cache : Bound runtime) : Except String (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerPrimitiveFacts.unitPointerMutLayoutBound runtime cache = Miri.Input.CompilerPrimitiveFacts.primitiveLayoutBound runtime cache "unit_pointer_mut"

def Miri.Input.CompilerPrimitiveFacts.namedLayout (runtime : RuntimeMetadata) (key : String) : Except String (ABI.TyAndLayout TypeId)

Read one exact source path/constructor query key from the named catalog.

Equations

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

def Miri.Input.CompilerPrimitiveFacts.orderingLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.callerLocationType (runtime : RuntimeMetadata) : Except String TypeId

Exact tcx.caller_location_ty(): &'static Location<'static>, preserving both source reference/lifetime construction and canonical compiler identity.

Equations

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

def Miri.Input.CompilerPrimitiveFacts.cULongLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.offTLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.u32Layout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.usizeLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.unitLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.unitPointerConstLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerPrimitiveFacts.unitPointerMutLayout (runtime : RuntimeMetadata) : Except String (ABI.TyAndLayout TypeId)

Equations

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