structure Miri.Input.ImportDocumentCore : Type

• compilerPredicates : Array CompilerPredicateEvidence
• compilerAbiLayoutSchema : Option String

  Version tag for source physical ArgAbi layouts in FnAbi evidence.

• producer : Producer
• runtimeTargetDataLayout : Option TargetDataLayoutEvidence
• completenessStatus : PayloadStatus
• types : Array TypeNode
• allocations : Array AllocationNode
• compilerAllocIdWorld : Option CompilerAllocIdWorld
• instances : Array InstanceNode
• selectedScope : Option SelectedScope
• functionAbis : Array FunctionAbi
• bodies : Array Body
• obligations : Array Obligation
• raw : Lean.Json
• sharedNodes : Array Lean.Json

  Resolved source nodes from the mandatory shared-payload graph. Each node is retained once so downstream consumers can reuse the document's DAG.

• compilerFunctionAbiTable : Option (CompilerFunctionAbiTable self.sharedNodes)

  Checked import-time ABI queries; failures remain deferred until demand.

• compilerValueMemo : Option CompilerValueMemo

structure Miri.Input.ImportDocument : Type

Full diagnostic import retained for callers that inspect the typed JSON projection. Runtime decoding uses ImportDocumentCore and does not retain this duplicate tree.

• compilerPredicates : Array CompilerPredicateEvidence
• compilerAbiLayoutSchema : Option String

  Version tag for source physical ArgAbi layouts in FnAbi evidence.

• producer : Producer
• runtimeTargetDataLayout : Option TargetDataLayoutEvidence
• completenessStatus : PayloadStatus
• types : Array TypeNode
• allocations : Array AllocationNode
• compilerAllocIdWorld : Option CompilerAllocIdWorld
• instances : Array InstanceNode
• selectedScope : Option SelectedScope
• functionAbis : Array FunctionAbi
• bodies : Array Body
• typedTree : TypedValue
• obligations : Array Obligation
• raw : Lean.Json
• sharedNodes : Array Lean.Json

  Resolved source nodes from the mandatory shared-payload graph.

def Miri.Input.ImportDocument.toCore (document : ImportDocument) : ImportDocumentCore

Diagnostic/reflected imports contain schema data only. Their runtime view uses the uncached compatibility path; the native runtime importer retains the checked compiler projections directly in ImportDocumentCore.

Equations

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

@[instance_reducible]

instance Miri.Input.instCoeImportDocumentImportDocumentCore : Coe ImportDocument ImportDocumentCore

Diagnostic clients may pass their full document to core-only consumers without retaining the generic tree in the resulting runtime metadata.

Equations

• Miri.Input.instCoeImportDocumentImportDocumentCore = { coe := Miri.Input.ImportDocument.toCore }

def Miri.Input.ImportDocumentCore.withTypedTree (core : ImportDocumentCore) (typedTree : TypedValue) : ImportDocument

Equations

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

structure Miri.Input.ExecutionInput : Type

A structurally complete input accepted by the decoder. This is still not a semantic model or a proof of Miri equivalence.

• document : ImportDocument

structure Miri.Input.RuntimeExecutionInput : Type

• document : ImportDocumentCore

structure Miri.Input.DecodeResult : Type

• document : ImportDocument
• executionInput : Option ExecutionInput
• blockingObligations : Array Obligation

  Exact obligations that make executionInput unavailable under the decoder's existing readiness predicate. This is diagnostic evidence only; it does not relax or otherwise define execution readiness.

structure Miri.Input.RuntimeDecodeResult : Type

• document : ImportDocumentCore
• executionInput : Option RuntimeExecutionInput
• blockingObligations : Array Obligation