Source intrinsics/mod.rs fallback policy and machine.rs runtime_checks. Attribute membership and intrinsic override policy are actual rustc queries, never inferred from a spelling or absence of an implementation in Lean.

structure Miri.Input.CompilerIntrinsicFacts.Metadata : Type

• mustOverride : Bool
• fallbackIsSpec : Bool

structure Miri.Input.CompilerIntrinsicFacts.Entry : Type

• callee : Interpreter.CallInstance
• name : Except String String
• intrinsic : Except String (Option Metadata)
• payload : Lean.Json

structure Miri.Input.CompilerIntrinsicFacts.Prepared : Type

• program : LoweredProgram
• entries : Array Entry
• checks : Array (MIR.RuntimeChecks × Bool)

def Miri.Input.CompilerIntrinsicFacts.prepare (program : LoweredProgram) : Except String Prepared

Equations

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

def Miri.Input.CompilerIntrinsicFacts.itemName (prepared : Prepared) (callee : Interpreter.CallInstance) : Except String String

Equations

• Miri.Input.CompilerIntrinsicFacts.itemName prepared callee = do let __do_lift ← Miri.Input.CompilerIntrinsicFacts.entry✝ prepared callee __do_lift.name

def Miri.Input.CompilerIntrinsicFacts.mustOverride (prepared : Prepared) (callee : Interpreter.CallInstance) : Except String Bool

Equations

• Miri.Input.CompilerIntrinsicFacts.mustOverride prepared callee = do let __do_lift ← Miri.Input.CompilerIntrinsicFacts.metadata✝ prepared callee pure __do_lift.mustOverride

def Miri.Input.CompilerIntrinsicFacts.fallbackIsSpec (prepared : Prepared) (callee : Interpreter.CallInstance) : Except String Bool

Equations

• Miri.Input.CompilerIntrinsicFacts.fallbackIsSpec prepared callee = do let __do_lift ← Miri.Input.CompilerIntrinsicFacts.metadata✝ prepared callee pure __do_lift.fallbackIsSpec

def Miri.Input.CompilerIntrinsicFacts.runtimeChecks (prepared : Prepared) (kind : MIR.RuntimeChecks) : Except String Bool

Equations

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

def Miri.Input.CompilerIntrinsicFacts.operandHooks {K User C : Type} (prepared : Prepared) (base : Interpreter.OperandMachine.Hooks K User C) : Interpreter.OperandMachine.Hooks K User C

Equations

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