Exact compiler query closure for interpret/cast.rs. Query results are compiler evidence keyed by complete source types/arguments; this module is not an instance solver and does not guess trait relationships from layouts.

@[reducible, inline]

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

Equations

• Miri.Input.CompilerCastQueries.Result = Except String

def Miri.Input.CompilerCastQueries.resolveFunction (p : CompilerProviders.Prepared) (definition : MIR.DefId) (args : Array MIR.GenericArg) : Result (Option Interpreter.CallInstance)

Equations

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

def Miri.Input.CompilerCastQueries.resolveClosureFnOnce (p : CompilerProviders.Prepared) (definition : MIR.DefId) (args : Array MIR.GenericArg) : Result Interpreter.CallInstance

Equations

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

def Miri.Input.CompilerCastQueries.noBoundVars (p : CompilerProviders.Prepared) (args : Array MIR.GenericArg) : Result Bool

Equations

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

def Miri.Input.CompilerCastQueries.lockstepTails (p : CompilerProviders.Prepared) (source target : MIR.TyId) : Result (MIR.TyId × MIR.TyId)

Equations

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

def Miri.Input.CompilerCastQueries.boxLayout (p : CompilerProviders.Prepared) (pointee : MIR.TyId) : Result Interpreter.LocalLayout

Equations

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

def Miri.Input.CompilerCastQueries.supertraitSlot (p : CompilerProviders.Prepared) (source target : MIR.TyId) : Result (Option Nat)

Equations

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

def Miri.Input.CompilerCastQueries.principal (p : CompilerProviders.Prepared) (token : Nat) : Result (Option Nat)

Full predicate-list identity is the key. The principal is exported by the compiler, not reconstructed by picking the first non-auto predicate.

Equations

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

def Miri.Input.CompilerCastQueries.normalizePrincipal (p : CompilerProviders.Prepared) (token : Nat) : Result (Option Nat)

Equations

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

def Miri.Input.CompilerCastQueries.eraseSelfTraitRef (p : CompilerProviders.Prepared) (token : Nat) : Result Nat

The runtime VTableEntry representation stores the target principal. The source relation is validated by the same exact allocation-to-query resolver used to build that entry, including query-backed source vtables that do not appear as .vtable nodes in the allocation graph.

Equations

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

def Miri.Input.CompilerCastQueries.required {S C : Type} (p : CompilerProviders.Prepared) : CompilerCastLeaves.Required S C

Equations

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