Required compiler facts for the fixed interpreter. Query evidence is keyed by exact compilation-local TyId and explicit fully_monomorphized typing_env. Sources: rustc_middle ty/{util,sty,inhabitedness}; interpret/{call,visitor,validity} and Miri helpers.rs UnsafeCellVisitor/tree_borrows/mod.rs NewPermission. No diagnostic type spelling establishes a semantic property.

@[reducible, inline]

abbrev Miri.Input.CompilerFacts.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.CompilerFacts.Result = Except String

structure Miri.Input.CompilerFacts.UnitLayoutCache (runtime : RuntimeMetadata.Indexed) : Type

• value : Result (ABI.TyAndLayout TypeId)
• exact : self.value = Miri.Input.CompilerFacts.computeUnitLayout✝ runtime

def Miri.Input.CompilerFacts.bindUnitLayout (runtime : RuntimeMetadata.Indexed) : UnitLayoutCache runtime

Equations

• Miri.Input.CompilerFacts.bindUnitLayout runtime = { value := Miri.Input.CompilerFacts.computeUnitLayout✝ runtime, exact := ⋯ }

structure Miri.Input.CompilerFacts.Context : Type

• runtime : RuntimeMetadata.Indexed
• primitiveQueries : Option (CompilerPrimitiveFacts.Bound self.runtime.toRuntimeMetadata)

  Exact direct primitive query results for the metadata owned by this context. Manual contexts may omit the cache.

• unitLayoutCache : Option (UnitLayoutCache self.runtime)

  The first-match unit query result is stored as data, including failure, and bound to this exact indexed metadata value.

• program : LoweredProgram
• lowering : Option (LowerContext.Bound self.program.input)

  Context caches are certified for this exact source document. Manual contexts may omit it and retain the uncached accessor fallback.

def Miri.Input.CompilerFacts.Context.loweringContext (context : Context) : LowerContext

Equations

• context.loweringContext = match context.lowering with | some prepared => prepared.value | none => Miri.Input.LowerContext.ofDocument context.program.input

def Miri.Input.CompilerFacts.Context.primitiveLayout (context : Context) (key : String) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerFacts.Context.orderingLayout (context : Context) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerFacts.Context.withProgram (context : Context) (program : LoweredProgram) : Context

Rebind every document-dependent cache when the owning lowered program changes.

Equations

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

def Miri.Input.CompilerFacts.ofProgram (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Result Context

Equations

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

def Miri.Input.CompilerFacts.boolean (context : Context) (id : TypeId) (query : String) : Result Bool

Equations

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

def Miri.Input.CompilerFacts.optionalType (context : Context) (id : TypeId) (query : String) : Result (Option TypeId)

Equations

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

def Miri.Input.CompilerFacts.requiredType (context : Context) (id : TypeId) (query : String) : Result TypeId

Equations

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

def Miri.Input.CompilerFacts.layoutOf (context : Context) (id : TypeId) : Result (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerFacts.layoutOf context id = Except.mapError toString (context.runtime.lookup id)

def Miri.Input.CompilerFacts.unitLayout (context : Context) : Result (ABI.TyAndLayout TypeId)

Equations

• Miri.Input.CompilerFacts.unitLayout context = match context.unitLayoutCache with | some cached => cached.value | none => Miri.Input.CompilerFacts.computeUnitLayout✝ context.runtime

def Miri.Input.CompilerFacts.builtinDeref (context : Context) (id : TypeId) (explicit : Bool) : Result (Option TypeId)

Equations

• Miri.Input.CompilerFacts.builtinDeref context id explicit = Miri.Input.CompilerFacts.optionalType context id (if explicit = true then "builtin_deref_explicit" else "builtin_deref_implicit")

def Miri.Input.CompilerFacts.referencePointee (context : Context) (id : TypeId) : Result (TypeId × MIR.Mutability)

Equations

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

def Miri.Input.CompilerFacts.retagTypeShape (context : Context) (id : TypeId) : Result TreeBorrows.RetagPipeline.RetagTypeShape

Equations

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

def Miri.Input.CompilerFacts.itemName (context : Context) (id : TypeId) : Result String

Equations

• Miri.Input.CompilerFacts.itemName context id = do let __do_lift ← Miri.Input.CompilerFacts.adtPayload✝ context id Miri.Input.CompilerFacts.string✝ __do_lift "item_name"

def Miri.Input.CompilerFacts.nonnullOptimizationGuaranteed (context : Context) (id : TypeId) : Result Bool

Equations

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

def Miri.Input.CompilerFacts.reprEqualUpToSeed (context : Context) (left right : TypeId) : Result Bool

Equations

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

def Miri.Input.CompilerFacts.adtInfo (context : Context) (id : TypeId) : Result (Interpreter.LayoutCompat.AdtInfo TypeId)

Equations

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

def Miri.Input.CompilerFacts.compatibilityKind (context : Context) (id : TypeId) : Result (Interpreter.LayoutCompat.TypeKind TypeId)

Equations

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

def Miri.Input.CompilerFacts.typedRetagHooks {K U : Type} (context : Context) (machine : Interpreter.TypedRetag.Hooks K U) : Interpreter.TypedRetag.Hooks K U

Replace only compiler leaves; all actual memory/projection/dyn operations retain their source implementation and stateful failure behavior.

Equations

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

def Miri.Input.CompilerFacts.compatibilityQueries {S : Type} (context : Context) : Interpreter.LayoutCompat.Queries TypeId S

Equations

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