Fail-closed bridge from decoded compiler data to the fixed interpreter AST. Successful lowering is syntax construction, not execution readiness or UB freedom. The original envelope and source scopes remain available beside the MIR body.

@[reducible, inline]

abbrev Miri.Input.LowerResult (α : Type u_1) : Type u_1

Equations

• Miri.Input.LowerResult = Except String

structure Miri.Input.LowerContextTypeIndex (source : Array TypeId) : Type

Membership acceleration whose type ties it to the exact source array. Its constructor is private, and the exactness field proves that its value is the corresponding index built from that array. Any update must preserve this equality.

• values : Std.HashSet TypeId
• exact : self.values = Miri.Input.buildTypeSet✝ source

structure Miri.Input.LowerContextAllocationIndex (source : Array AllocationId) : Type

• values : Std.HashSet AllocationId
• exact : self.values = Miri.Input.buildAllocationSet✝ source

structure Miri.Input.LowerContextScalarIndex (source : Array (TypeId × Nat)) : Type

• values : Std.HashMap TypeId Nat
• exact : self.values = Miri.Input.buildScalarMap✝ source

structure Miri.Input.LowerContext : Type

• typeIds : Array TypeId

  Each supplied type ID must refer to this compilation's metadata graph.

• scalarSizes : Array (TypeId × Nat)

  Exact byte widths from compiler layout metadata; required for scalar constants.

• allocationIds : Array AllocationId
• obligations : Array Obligation
• sourceDocument : Option Lean.Json

  Raw source document used only to revalidate exact source-path roles while lowering. A bare caller-supplied path never discharges an obligation.

• compilerValueMemo : Option CompilerValueMemo
• typeIndex : Option (LowerContextTypeIndex self.typeIds)

  Optional exact-array certificates; hand-built contexts default to the original linear lookup behavior.

• allocationIndex : Option (LowerContextAllocationIndex self.allocationIds)
• scalarIndex : Option (LowerContextScalarIndex self.scalarSizes)

def Miri.Input.LowerContext.decodeCompilerValue (ctx : LowerContext) (raw : Lean.Json) : Except String TypedValue

Consume complete import-time compiler values; manual contexts decode directly.

Equations

• ctx.decodeCompilerValue raw = Miri.Input.decodeCompilerValueWithMemo raw ctx.compilerValueMemo

def Miri.Input.LowerContext.containsTypeId (ctx : LowerContext) (id : TypeId) : Bool

Equations

• ctx.containsTypeId id = match ctx.typeIndex with | some index => index.values.contains id | none => ctx.typeIds.contains id

def Miri.Input.LowerContext.containsAllocationId (ctx : LowerContext) (id : AllocationId) : Bool

Equations

• ctx.containsAllocationId id = match ctx.allocationIndex with | some index => index.values.contains id | none => ctx.allocationIds.contains id

def Miri.Input.LowerContext.scalarSize (ctx : LowerContext) (id : TypeId) : Option Nat

Equations

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

def Miri.Input.LowerContext.withTypeIds (ctx : LowerContext) (ids : Array TypeId) : LowerContext

Rebase the source type universe and rebuild its private membership cache.

Equations

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

def Miri.Input.LowerContext.withAllocationIds (ctx : LowerContext) (ids : Array AllocationId) : LowerContext

Rebase the allocation universe and rebuild its private membership cache.

Equations

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

def Miri.Input.LowerContext.withScalarSizes (ctx : LowerContext) (sizes : Array (TypeId × Nat)) : LowerContext

Rebase scalar layouts and rebuild the first-row-preserving width cache.

Equations

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

def Miri.Input.LowerContext.ofTypes (types : Array TypeNode) : LowerContext

Derive scalar widths from compiler metadata, never from bits or host types.

Equations

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

def Miri.Input.LowerContext.ofDocument (document : ImportDocumentCore) : LowerContext

Resolve graph identities from the same decoded compilation. Metadata semantics remain independent from syntax lowering and its obligations.

Equations

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

structure Miri.Input.LowerContext.Bound (document : ImportDocumentCore) : Type

A prepared lowering context tied to one exact decoded source document. The private constructor and equality field prevent reusing it for a different document, even when the documents serialize to equal JSON.

• value : LowerContext
• exact : self.value = ofDocument document

def Miri.Input.LowerContext.bindDocument (document : ImportDocumentCore) : Bound document

Prepare the context and retain its exact document identity in the type.

Equations

• Miri.Input.LowerContext.bindDocument document = { value := Miri.Input.LowerContext.ofDocument document, exact := ⋯ }

structure Miri.Input.LoweredBody : Type

• body : MIR.Body
• spans : Array SourceSpanData
• input : BodyCore
• definitions : Array DefinitionId
• typeConstants : Array MIR.TypeConst
• obligations : Array Obligation

def Miri.Input.lookupDefinitionId (definitions : Array DefinitionId) (sourceId : DefinitionId) : LowerResult MIR.DefId

Resolve a crate-qualified compiler definition into this bundle's dense identity. Raw rustc definition indices are never runtime definition IDs.

Equations

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

def Miri.Input.LoweredBody.ownDefinitionId (body : LoweredBody) : LowerResult MIR.DefId

Equations

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

def Miri.Input.rvalueLoweringBranch : RvalueVariant → Bool

Constructor inventory. true means a lowering branch exists, subject to child metadata checks; it does not mean execution semantics is implemented. Exhaustive matches make newly added input constructors require a decision.

Equations

• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.use = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.binaryOp = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.unaryOp = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.discriminant = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.copyForDeref = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.wrapUnsafeBinder = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.repeat = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.ref = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.threadLocalRef = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.rawPtr = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.cast = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.aggregate = true
• Miri.Input.rvalueLoweringBranch Miri.Input.RvalueVariant.reborrow = true
• Miri.Input.rvalueLoweringBranch (Miri.Input.RvalueVariant.unknown value) = false

def Miri.Input.statementLoweringBranch : StatementVariant → Bool

Equations

• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.assign = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.setDiscriminant = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.storageLive = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.storageDead = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.placeMention = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.constEvalCounter = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.nop = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.fakeRead = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.ascribeUserType = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.coverage = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.intrinsic = true
• Miri.Input.statementLoweringBranch Miri.Input.StatementVariant.backwardIncompatibleDropHint = true
• Miri.Input.statementLoweringBranch (Miri.Input.StatementVariant.unknown value) = false

def Miri.Input.terminatorLoweringBranch : TerminatorVariant → Bool

Equations

• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.goto = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.unwindResume = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.return = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.unreachable = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.assert = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.coroutineDrop = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.falseEdge = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.switchInt = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.unwindTerminate = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.drop = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.call = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.tailCall = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.yield = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.falseUnwind = true
• Miri.Input.terminatorLoweringBranch Miri.Input.TerminatorVariant.inlineAsm = true
• Miri.Input.terminatorLoweringBranch (Miri.Input.TerminatorVariant.unknown value) = false

def Miri.Input.lowerBody (ctx : LowerContext) (input : BodyCore) : LowerResult LoweredBody

A standalone body's definition/type-constant/span IDs are local to this result. Use lowerBodies or lowerProgram for cross-function linking.

Equations

• Miri.Input.lowerBody ctx input = Except.map Prod.fst (Miri.Input.lowerBodyState✝ ctx input { })

structure Miri.Input.LoweredBodies : Type

• bodies : Array LoweredBody
• spans : Array SourceSpanData
• definitions : Array DefinitionId
• typeConstants : Array MIR.TypeConst

def Miri.Input.lowerBodies (ctx : LowerContext) (inputs : Array BodyCore) (seedDefinitions : Array DefinitionId := #[]) : LowerResult LoweredBodies

Lower a compilation's bodies through one shared interner, including mutually recursive references. Every returned body uses the same ID tables.

Equations

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

structure Miri.Input.LoweredProgram : Type

• bundle : LoweredBodies
• roots : Array Nat

  Root body indices into bundle.bodies, in the original document order.

• instances : Array (InstanceId × Nat)

  Instance graph identity to body index; the source graph is retained below.

• promoted : Array (Nat × Nat × Nat)

  (parent body index, promoted index, body index).

• input : ImportDocumentCore

def Miri.Input.LoweredProgram.rootDefinitionId (program : LoweredProgram) (rootIndex : Nat) : LowerResult MIR.DefId

Look up a document root's frame identity without assuming it was called or that source and runtime definition indices coincide.

Equations

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

def Miri.Input.lowerCoreProgram (input : ImportDocumentCore) : LowerResult LoweredProgram

Lower all present root, instance, and promoted bodies with global compiler identity tables. Unavailable bodies remain explicit source graph obligations.

Equations

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

def Miri.Input.lowerProgram (input : ImportDocument) : LowerResult LoweredProgram

Compatibility entrypoint for full diagnostic documents. Runtime clients that decode without retaining the typed JSON tree should call lowerCoreProgram.

Equations

• Miri.Input.lowerProgram input = Miri.Input.lowerCoreProgram input.toCore

structure Miri.Input.CompilerTables : Type

Interner state shared by metadata-query lowering and MIR syntax. Appending entries preserves every previously lowered ID.

• spans : Array SourceSpanData
• definitions : Array DefinitionId
• typeConstants : Array MIR.TypeConst

def Miri.Input.LoweredProgram.compilerTables (program : LoweredProgram) : CompilerTables

Equations

• program.compilerTables = { spans := program.bundle.spans, definitions := program.bundle.definitions, typeConstants := program.bundle.typeConstants }

def Miri.Input.LoweredProgram.withCompilerTables (program : LoweredProgram) (tables : CompilerTables) : LoweredProgram

Equations

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

def Miri.Input.lowerCompilerGenericArgs (ctx : LowerContext) (tables : CompilerTables) (value : TypedValue) : LowerResult (Array MIR.GenericArg × CompilerTables)

Equations

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

def Miri.Input.lowerCompilerConstOperand (ctx : LowerContext) (tables : CompilerTables) (value : TypedValue) : LowerResult (MIR.ConstOperand × CompilerTables)

Equations

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

def Miri.Input.lowerCompilerConstValue (ctx : LowerContext) (ty : MIR.TyId) (value : TypedValue) : LowerResult MIR.ConstValue

Equations

• Miri.Input.lowerCompilerConstValue ctx ty value = Miri.Input.constValue✝ ctx ty value

def Miri.Input.lowerCompilerTypeConst (ctx : LowerContext) (tables : CompilerTables) (value : TypedValue) : LowerResult (MIR.TypeConstId × CompilerTables)

Canonical type-constant interning for compiler pattern/query metadata.

Equations

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

def Miri.Input.lowerCompilerSpan (tables : CompilerTables) (value : TypedValue) : LowerResult (MIR.SpanRef × CompilerTables)

Intern a compiler span without synthesizing a source location.

Equations

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

structure Miri.Input.CompilerSpanInterner : Type

Incremental exact span interning for compiler source-map batches. The candidate index is seeded once from the existing table; buckets only narrow the search and full span equality remains authoritative.

• tables : Miri.Input.CompilerTables
• candidates : Std.HashMap (String × Nat × Nat) (Array Nat)
• spanReflexivity : SpanArrayReflexivity (tables self).spans

def Miri.Input.CompilerSpanInterner.ofTables (tables : CompilerTables) : CompilerSpanInterner

Equations

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

def Miri.Input.CompilerSpanInterner.rebind (interner : CompilerSpanInterner) (tables : CompilerTables) : CompilerSpanInterner

Reuse an index only when the complete span arrays compare equal. The certificate makes the common same-array case constant time while preserving a full equality check for independently allocated or reordered tables.

Equations

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

def Miri.Input.CompilerSpanInterner.getTables (interner : CompilerSpanInterner) : CompilerTables

Equations

• interner.getTables = Miri.Input.CompilerSpanInterner.tables✝ interner

def Miri.Input.lowerCompilerSpanWithInterner (interner : CompilerSpanInterner) (value : TypedValue) : LowerResult (MIR.SpanRef × CompilerSpanInterner)

Equations

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

def Miri.Input.CompilerSpanInterner.sameSpansAs (result base : CompilerSpanInterner) : Bool

Compare the result of an independent lowering against the unchanged base. The checked pointer shortcut retains the full original array comparator.

Equations

• result.sameSpansAs base = Miri.Input.SpanArrayReflexivity.matchesRight✝ ⋯ (Miri.Input.CompilerSpanInterner.tables✝ result).spans

theorem Miri.Input.CompilerSpanInterner.sameSpansAs_eq (result base : CompilerSpanInterner) : result.sameSpansAs base = (base.getTables.spans == result.getTables.spans)

def Miri.Input.lowerCompilerConstOperandWithInterner (ctx : LowerContext) (interner : CompilerSpanInterner) (value : TypedValue) : LowerResult (MIR.ConstOperand × CompilerSpanInterner)

Lower a compiler constant operand using an exact, persistent span index.

Equations

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

def Miri.Input.lowerCompilerPlace (ctx : LowerContext) (value : TypedValue) : LowerResult MIR.Place

Decode the source place key for compiler query evidence. Projection types must already belong to the shared input type graph.

Equations

• Miri.Input.lowerCompilerPlace ctx value = Miri.Input.place✝ ctx value