def Miri.Input.DecoderValues.expectedMiriCommit : String

Equations

• Miri.Input.expectedMiriCommit = "7fa591d7d4dd9af8154becbc8332f8096f8323b1"

def Miri.Input.DecoderValues.expectedRustcCommit : String

Equations

• Miri.Input.expectedRustcCommit = "8144389c895da997dbdecaa635e41d6a50be6ffd"

def Miri.Input.DecoderValues.expectedSchema : String

Equations

• Miri.Input.expectedSchema = "lean-miri-rustc-mir"

def Miri.Input.DecoderValues.expectedSchemaVersion : Nat

Equations

• Miri.Input.expectedSchemaVersion = 3

def Miri.Input.DecoderValues.expectedCompilerAbiLayoutSchema : String

Equations

• Miri.Input.expectedCompilerAbiLayoutSchema = "physical_ty_and_layout_v1"

def Miri.Input.DecoderValues.escapePathKey (key : String) : String

Equations

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

def Miri.Input.DecoderValues.joinPath (path key : String) : String

Equations

• Miri.Input.DecoderValues.joinPath path key = if path.isEmpty = true then Miri.Input.DecoderValues.escapePathKey key else path ++ "." ++ Miri.Input.DecoderValues.escapePathKey key

def Miri.Input.DecoderValues.field (j : Lean.Json) (key path : String) : Except String Lean.Json

Equations

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

def Miri.Input.DecoderValues.fieldNat (j : Lean.Json) (key path : String) : Except String Nat

Equations

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

def Miri.Input.DecoderValues.fieldString (j : Lean.Json) (key path : String) : Except String String

Equations

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

def Miri.Input.DecoderValues.fieldBool (j : Lean.Json) (key path : String) : Except String Bool

Equations

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

def Miri.Input.DecoderValues.arrayField (j : Lean.Json) (key path : String) : Except String (Array Lean.Json)

Equations

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

def Miri.Input.DecoderValues.optionalNatField (j : Lean.Json) (key path : String) : Except String (Option Nat)

Equations

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

def Miri.Input.DecoderValues.optionalField (j : Lean.Json) (key : String) : Option Lean.Json

Equations

• Miri.Input.DecoderValues.optionalField j key = (j.getObjVal? key).toOption

def Miri.Input.DecoderValues.optionalString (j : Lean.Json) (key path : String) : Except String (Option String)

Equations

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

def Miri.Input.DecoderValues.objectFields (j : Lean.Json) : Except String (Array (String × Lean.Json))

Equations

• Miri.Input.DecoderValues.objectFields (Lean.Json.obj fields) = pure fields.toList.toArray
• Miri.Input.DecoderValues.objectFields j = throw "expected object"

def Miri.Input.DecoderValues.statusOf? (j : Lean.Json) : Option String

Equations

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

def Miri.Input.DecoderValues.parseStatus (value : String) : PayloadStatus

Equations

• Miri.Input.DecoderValues.parseStatus "supported" = Miri.Input.PayloadStatus.supported
• Miri.Input.DecoderValues.parseStatus "complete" = Miri.Input.PayloadStatus.supported
• Miri.Input.DecoderValues.parseStatus "unsupported" = Miri.Input.PayloadStatus.unsupported
• Miri.Input.DecoderValues.parseStatus "unknown" = Miri.Input.PayloadStatus.unknown
• Miri.Input.DecoderValues.parseStatus "incomplete" = Miri.Input.PayloadStatus.incomplete
• Miri.Input.DecoderValues.parseStatus "debug_payload" = Miri.Input.PayloadStatus.debugPayload
• Miri.Input.DecoderValues.parseStatus value = Miri.Input.PayloadStatus.unrecognized value

def Miri.Input.DecoderValues.sourceDebugString (j : Lean.Json) (key path : String) : Except String String

Equations

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

structure Miri.Input.DecoderValues.DecodeMemo : Type

Parsed successful shared payloads are memoized per input document. Keys use the canonical JSON encoding so inline copies and DAG references share entries; failed parses are never cached, preserving diagnostics at each occurrence.

• sourceSpans : Std.HashMap Lean.Json Miri.Input.SourceSpanData
• layouts : Std.HashMap Lean.Json Miri.Input.Layout
• functionAbis : Std.HashMap Lean.Json Miri.Input.FunctionAbi

def Miri.Input.DecoderValues.emptyDecodeMemo : DecodeMemo

Equations

• Miri.Input.DecoderValues.emptyDecodeMemo = { }

def Miri.Input.DecoderValues.parseSourcePosition (j : Lean.Json) (path : String) : Except String SourcePosition

Equations

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

def Miri.Input.DecoderValues.parseSourceSpanUncached (j : Lean.Json) (path : String) : Except String SourceSpanData

Equations

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

def Miri.Input.DecoderValues.parseSourceSpan (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String SourceSpanData

Equations

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

def Miri.Input.DecoderValues.parseSourceInfo (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String SourceInfo

Equations

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

def Miri.Input.DecoderValues.hasField (j : Lean.Json) (key : String) : Bool

Equations

• Miri.Input.DecoderValues.hasField j key = (j.getObjVal? key).isOk

def Miri.Input.DecoderValues.isSourceSpanJson (j : Lean.Json) : Bool

Equations

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

def Miri.Input.DecoderValues.statementVariant (tag : String) : StatementVariant

Equations

• Miri.Input.DecoderValues.statementVariant "Assign" = Miri.Input.StatementVariant.assign
• Miri.Input.DecoderValues.statementVariant "FakeRead" = Miri.Input.StatementVariant.fakeRead
• Miri.Input.DecoderValues.statementVariant "SetDiscriminant" = Miri.Input.StatementVariant.setDiscriminant
• Miri.Input.DecoderValues.statementVariant "StorageLive" = Miri.Input.StatementVariant.storageLive
• Miri.Input.DecoderValues.statementVariant "StorageDead" = Miri.Input.StatementVariant.storageDead
• Miri.Input.DecoderValues.statementVariant "PlaceMention" = Miri.Input.StatementVariant.placeMention
• Miri.Input.DecoderValues.statementVariant "AscribeUserType" = Miri.Input.StatementVariant.ascribeUserType
• Miri.Input.DecoderValues.statementVariant "Coverage" = Miri.Input.StatementVariant.coverage
• Miri.Input.DecoderValues.statementVariant "Intrinsic" = Miri.Input.StatementVariant.intrinsic
• Miri.Input.DecoderValues.statementVariant "ConstEvalCounter" = Miri.Input.StatementVariant.constEvalCounter
• Miri.Input.DecoderValues.statementVariant "Nop" = Miri.Input.StatementVariant.nop
• Miri.Input.DecoderValues.statementVariant "BackwardIncompatibleDropHint" = Miri.Input.StatementVariant.backwardIncompatibleDropHint
• Miri.Input.DecoderValues.statementVariant tag = Miri.Input.StatementVariant.unknown tag

def Miri.Input.DecoderValues.terminatorVariant (tag : String) : TerminatorVariant

Equations

• Miri.Input.DecoderValues.terminatorVariant "Goto" = Miri.Input.TerminatorVariant.goto
• Miri.Input.DecoderValues.terminatorVariant "SwitchInt" = Miri.Input.TerminatorVariant.switchInt
• Miri.Input.DecoderValues.terminatorVariant "UnwindResume" = Miri.Input.TerminatorVariant.unwindResume
• Miri.Input.DecoderValues.terminatorVariant "UnwindTerminate" = Miri.Input.TerminatorVariant.unwindTerminate
• Miri.Input.DecoderValues.terminatorVariant "Return" = Miri.Input.TerminatorVariant.return
• Miri.Input.DecoderValues.terminatorVariant "Unreachable" = Miri.Input.TerminatorVariant.unreachable
• Miri.Input.DecoderValues.terminatorVariant "Drop" = Miri.Input.TerminatorVariant.drop
• Miri.Input.DecoderValues.terminatorVariant "Call" = Miri.Input.TerminatorVariant.call
• Miri.Input.DecoderValues.terminatorVariant "TailCall" = Miri.Input.TerminatorVariant.tailCall
• Miri.Input.DecoderValues.terminatorVariant "Assert" = Miri.Input.TerminatorVariant.assert
• Miri.Input.DecoderValues.terminatorVariant "Yield" = Miri.Input.TerminatorVariant.yield
• Miri.Input.DecoderValues.terminatorVariant "CoroutineDrop" = Miri.Input.TerminatorVariant.coroutineDrop
• Miri.Input.DecoderValues.terminatorVariant "FalseEdge" = Miri.Input.TerminatorVariant.falseEdge
• Miri.Input.DecoderValues.terminatorVariant "FalseUnwind" = Miri.Input.TerminatorVariant.falseUnwind
• Miri.Input.DecoderValues.terminatorVariant "InlineAsm" = Miri.Input.TerminatorVariant.inlineAsm
• Miri.Input.DecoderValues.terminatorVariant tag = Miri.Input.TerminatorVariant.unknown tag

def Miri.Input.DecoderValues.rvalueVariant (tag : String) : RvalueVariant

Equations

• Miri.Input.DecoderValues.rvalueVariant "Use" = Miri.Input.RvalueVariant.use
• Miri.Input.DecoderValues.rvalueVariant "Repeat" = Miri.Input.RvalueVariant.repeat
• Miri.Input.DecoderValues.rvalueVariant "Ref" = Miri.Input.RvalueVariant.ref
• Miri.Input.DecoderValues.rvalueVariant "ThreadLocalRef" = Miri.Input.RvalueVariant.threadLocalRef
• Miri.Input.DecoderValues.rvalueVariant "RawPtr" = Miri.Input.RvalueVariant.rawPtr
• Miri.Input.DecoderValues.rvalueVariant "Cast" = Miri.Input.RvalueVariant.cast
• Miri.Input.DecoderValues.rvalueVariant "BinaryOp" = Miri.Input.RvalueVariant.binaryOp
• Miri.Input.DecoderValues.rvalueVariant "UnaryOp" = Miri.Input.RvalueVariant.unaryOp
• Miri.Input.DecoderValues.rvalueVariant "Discriminant" = Miri.Input.RvalueVariant.discriminant
• Miri.Input.DecoderValues.rvalueVariant "Aggregate" = Miri.Input.RvalueVariant.aggregate
• Miri.Input.DecoderValues.rvalueVariant "CopyForDeref" = Miri.Input.RvalueVariant.copyForDeref
• Miri.Input.DecoderValues.rvalueVariant "WrapUnsafeBinder" = Miri.Input.RvalueVariant.wrapUnsafeBinder
• Miri.Input.DecoderValues.rvalueVariant "Reborrow" = Miri.Input.RvalueVariant.reborrow
• Miri.Input.DecoderValues.rvalueVariant tag = Miri.Input.RvalueVariant.unknown tag

def Miri.Input.DecoderValues.operandVariant (tag : String) : OperandVariant

Equations

• Miri.Input.DecoderValues.operandVariant "Copy" = Miri.Input.OperandVariant.copy
• Miri.Input.DecoderValues.operandVariant "Move" = Miri.Input.OperandVariant.move
• Miri.Input.DecoderValues.operandVariant "Constant" = Miri.Input.OperandVariant.constant
• Miri.Input.DecoderValues.operandVariant "RuntimeChecks" = Miri.Input.OperandVariant.runtimeChecks
• Miri.Input.DecoderValues.operandVariant tag = Miri.Input.OperandVariant.unknown tag

def Miri.Input.DecoderValues.projectionVariant (tag : String) : ProjectionVariant

Equations

• Miri.Input.DecoderValues.projectionVariant "Deref" = Miri.Input.ProjectionVariant.deref
• Miri.Input.DecoderValues.projectionVariant "Field" = Miri.Input.ProjectionVariant.field
• Miri.Input.DecoderValues.projectionVariant "Index" = Miri.Input.ProjectionVariant.index
• Miri.Input.DecoderValues.projectionVariant "ConstantIndex" = Miri.Input.ProjectionVariant.constantIndex
• Miri.Input.DecoderValues.projectionVariant "Subslice" = Miri.Input.ProjectionVariant.subslice
• Miri.Input.DecoderValues.projectionVariant "Downcast" = Miri.Input.ProjectionVariant.downcast
• Miri.Input.DecoderValues.projectionVariant "OpaqueCast" = Miri.Input.ProjectionVariant.opaqueCast
• Miri.Input.DecoderValues.projectionVariant "UnwrapUnsafeBinder" = Miri.Input.ProjectionVariant.unwrapUnsafeBinder
• Miri.Input.DecoderValues.projectionVariant "PhantomDeref" = Miri.Input.ProjectionVariant.phantomDeref
• Miri.Input.DecoderValues.projectionVariant tag = Miri.Input.ProjectionVariant.unknown tag

def Miri.Input.DecoderValues.typeShapeKind (tag : String) : TypeShapeKind

Equations

• Miri.Input.DecoderValues.typeShapeKind "bool" = Miri.Input.TypeShapeKind.bool
• Miri.Input.DecoderValues.typeShapeKind "char" = Miri.Input.TypeShapeKind.char
• Miri.Input.DecoderValues.typeShapeKind "int" = Miri.Input.TypeShapeKind.int
• Miri.Input.DecoderValues.typeShapeKind "uint" = Miri.Input.TypeShapeKind.uint
• Miri.Input.DecoderValues.typeShapeKind "float" = Miri.Input.TypeShapeKind.float
• Miri.Input.DecoderValues.typeShapeKind "adt" = Miri.Input.TypeShapeKind.adt
• Miri.Input.DecoderValues.typeShapeKind "foreign" = Miri.Input.TypeShapeKind.foreign
• Miri.Input.DecoderValues.typeShapeKind "str" = Miri.Input.TypeShapeKind.str
• Miri.Input.DecoderValues.typeShapeKind "array" = Miri.Input.TypeShapeKind.array
• Miri.Input.DecoderValues.typeShapeKind "pattern_type" = Miri.Input.TypeShapeKind.patternType
• Miri.Input.DecoderValues.typeShapeKind "slice" = Miri.Input.TypeShapeKind.slice
• Miri.Input.DecoderValues.typeShapeKind "raw_pointer" = Miri.Input.TypeShapeKind.rawPointer
• Miri.Input.DecoderValues.typeShapeKind "reference" = Miri.Input.TypeShapeKind.reference
• Miri.Input.DecoderValues.typeShapeKind "function_definition" = Miri.Input.TypeShapeKind.functionDefinition
• Miri.Input.DecoderValues.typeShapeKind "function_pointer" = Miri.Input.TypeShapeKind.functionPointer
• Miri.Input.DecoderValues.typeShapeKind "unsafe_binder" = Miri.Input.TypeShapeKind.unsafeBinder
• Miri.Input.DecoderValues.typeShapeKind "dynamic_trait_object" = Miri.Input.TypeShapeKind.dynamicTraitObject
• Miri.Input.DecoderValues.typeShapeKind "closure" = Miri.Input.TypeShapeKind.closure
• Miri.Input.DecoderValues.typeShapeKind "coroutine_closure" = Miri.Input.TypeShapeKind.coroutineClosure
• Miri.Input.DecoderValues.typeShapeKind "coroutine" = Miri.Input.TypeShapeKind.coroutine
• Miri.Input.DecoderValues.typeShapeKind "coroutine_witness" = Miri.Input.TypeShapeKind.coroutineWitness
• Miri.Input.DecoderValues.typeShapeKind "never" = Miri.Input.TypeShapeKind.never
• Miri.Input.DecoderValues.typeShapeKind "tuple" = Miri.Input.TypeShapeKind.tuple
• Miri.Input.DecoderValues.typeShapeKind "alias" = Miri.Input.TypeShapeKind.alias
• Miri.Input.DecoderValues.typeShapeKind "parameter" = Miri.Input.TypeShapeKind.parameter
• Miri.Input.DecoderValues.typeShapeKind "bound_type" = Miri.Input.TypeShapeKind.boundType
• Miri.Input.DecoderValues.typeShapeKind "placeholder_type" = Miri.Input.TypeShapeKind.placeholderType
• Miri.Input.DecoderValues.typeShapeKind "inference_type" = Miri.Input.TypeShapeKind.inferenceType
• Miri.Input.DecoderValues.typeShapeKind "error_type" = Miri.Input.TypeShapeKind.errorType
• Miri.Input.DecoderValues.typeShapeKind tag = Miri.Input.TypeShapeKind.unknown tag

inductive Miri.Input.DecoderValues.Domain : Type

• any : Domain
• statement : Domain
• terminator : Domain
• rvalue : Domain
• operand : Domain
• projection : Domain
• statementWrapper : Domain
• terminatorWrapper : Domain

@[instance_reducible]

instance Miri.Input.DecoderValues.instBEqDomain : BEq Domain

Equations

• Miri.Input.DecoderValues.instBEqDomain = { beq := Miri.Input.DecoderValues.instBEqDomain.beq }

def Miri.Input.DecoderValues.instBEqDomain.beq : Domain → Domain → Bool

Equations

• Miri.Input.DecoderValues.instBEqDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Miri.Input.DecoderValues.instHashableDomain.hash : Domain → UInt64

Equations

• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.any = 0
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.statement = 1
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.terminator = 2
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.rvalue = 3
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.operand = 4
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.projection = 5
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.statementWrapper = 6
• Miri.Input.DecoderValues.instHashableDomain.hash Miri.Input.DecoderValues.Domain.terminatorWrapper = 7

@[instance_reducible]

instance Miri.Input.DecoderValues.instHashableDomain : Hashable Domain

Equations

• Miri.Input.DecoderValues.instHashableDomain = { hash := Miri.Input.DecoderValues.instHashableDomain.hash }

structure Miri.Input.DecoderValues.DecodeValueKey : Type

• json : Lean.Json
• domain : Domain
• tagCategory : Option TypedEnumTag
• isRegionPath : Bool
• isHirIdPath : Bool
• isCoveragePath : Bool
• isCastCoercionPath : Bool

def Miri.Input.DecoderValues.instBEqDecodeValueKey.beq : DecodeValueKey → DecodeValueKey → Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.instBEqDecodeValueKey.beq x✝¹ x✝ = false

@[instance_reducible]

instance Miri.Input.DecoderValues.instBEqDecodeValueKey : BEq DecodeValueKey

Equations

• Miri.Input.DecoderValues.instBEqDecodeValueKey = { beq := Miri.Input.DecoderValues.instBEqDecodeValueKey.beq }

@[instance_reducible]

instance Miri.Input.DecoderValues.instHashableDecodeValueKey : Hashable DecodeValueKey

Equations

• Miri.Input.DecoderValues.instHashableDecodeValueKey = { hash := Miri.Input.DecoderValues.instHashableDecodeValueKey.hash }

def Miri.Input.DecoderValues.instHashableDecodeValueKey.hash : DecodeValueKey → UInt64

Equations

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

def Miri.Input.DecoderValues.decodeValueKey (j : Lean.Json) (path : String) (domain : Domain) (tagCategory : Option TypedEnumTag) : DecodeValueKey

Equations

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

def Miri.Input.DecoderValues.asTag? (j : Lean.Json) (key : String) : Option String

Equations

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

def Miri.Input.DecoderValues.singletonRef (j : Lean.Json) (key : String) : Option Nat

Equations

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

def Miri.Input.DecoderValues.isTypeRef (j : Lean.Json) : Option Nat

Equations

• Miri.Input.DecoderValues.isTypeRef j = Miri.Input.DecoderValues.singletonRef j "type_id"

def Miri.Input.DecoderValues.isAllocationRef (j : Lean.Json) : Option Nat

Equations

• Miri.Input.DecoderValues.isAllocationRef j = Miri.Input.DecoderValues.singletonRef j "allocation_id"

def Miri.Input.DecoderValues.childDomain (parent : Domain) (key : String) : Domain

Equations

• Miri.Input.DecoderValues.childDomain Miri.Input.DecoderValues.Domain.statementWrapper "kind" = Miri.Input.DecoderValues.Domain.statement
• Miri.Input.DecoderValues.childDomain Miri.Input.DecoderValues.Domain.terminatorWrapper "kind" = Miri.Input.DecoderValues.Domain.terminator
• Miri.Input.DecoderValues.childDomain parent "rvalue" = Miri.Input.DecoderValues.Domain.rvalue
• Miri.Input.DecoderValues.childDomain parent "operand" = Miri.Input.DecoderValues.Domain.operand
• Miri.Input.DecoderValues.childDomain parent "function" = Miri.Input.DecoderValues.Domain.operand
• Miri.Input.DecoderValues.childDomain parent "condition" = Miri.Input.DecoderValues.Domain.operand
• Miri.Input.DecoderValues.childDomain parent "discriminant" = Miri.Input.DecoderValues.Domain.operand
• Miri.Input.DecoderValues.childDomain parent "projection" = Miri.Input.DecoderValues.Domain.projection
• Miri.Input.DecoderValues.childDomain parent "statements" = Miri.Input.DecoderValues.Domain.statementWrapper
• Miri.Input.DecoderValues.childDomain parent "terminator" = Miri.Input.DecoderValues.Domain.terminatorWrapper
• Miri.Input.DecoderValues.childDomain parent key = Miri.Input.DecoderValues.Domain.any

def Miri.Input.DecoderValues.isKnownStatement (tag : String) : Bool

Equations

• Miri.Input.DecoderValues.isKnownStatement tag = match Miri.Input.DecoderValues.statementVariant tag with | Miri.Input.StatementVariant.unknown value => false | x => true

def Miri.Input.DecoderValues.isKnownTerminator (tag : String) : Bool

Equations

• Miri.Input.DecoderValues.isKnownTerminator tag = match Miri.Input.DecoderValues.terminatorVariant tag with | Miri.Input.TerminatorVariant.unknown value => false | x => true

def Miri.Input.DecoderValues.isKnownRvalue (tag : String) : Bool

Equations

• Miri.Input.DecoderValues.isKnownRvalue tag = match Miri.Input.DecoderValues.rvalueVariant tag with | Miri.Input.RvalueVariant.unknown value => false | x => true

def Miri.Input.DecoderValues.isKnownOperand (tag : String) : Bool

Equations

• Miri.Input.DecoderValues.isKnownOperand tag = match Miri.Input.DecoderValues.operandVariant tag with | Miri.Input.OperandVariant.unknown value => false | x => true

def Miri.Input.DecoderValues.isKnownProjection (tag : String) : Bool

Equations

• Miri.Input.DecoderValues.isKnownProjection tag = match Miri.Input.DecoderValues.projectionVariant tag with | Miri.Input.ProjectionVariant.unknown value => false | x => true

def Miri.Input.DecoderValues.recognizedAutoDomain (j : Lean.Json) : Option Domain

Equations

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

def Miri.Input.DecoderValues.domainTag (j : Lean.Json) (domain : Domain) : Option String

Equations

• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.statement = Miri.Input.DecoderValues.asTag? j "variant"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.terminator = Miri.Input.DecoderValues.asTag? j "variant"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.statementWrapper = Miri.Input.DecoderValues.asTag? j "variant"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.terminatorWrapper = Miri.Input.DecoderValues.asTag? j "variant"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.rvalue = Miri.Input.DecoderValues.asTag? j "kind"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.operand = Miri.Input.DecoderValues.asTag? j "kind"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.projection = Miri.Input.DecoderValues.asTag? j "kind"
• Miri.Input.DecoderValues.domainTag j Miri.Input.DecoderValues.Domain.any = none

def Miri.Input.DecoderValues.isStringJson (j : Lean.Json) : Bool

Equations

• Miri.Input.DecoderValues.isStringJson (Lean.Json.str s) = true
• Miri.Input.DecoderValues.isStringJson j = false

def Miri.Input.DecoderValues.integerTypeTag (text : String) : IntegerTypeTag

Equations

• Miri.Input.DecoderValues.integerTypeTag "i8" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.i8
• Miri.Input.DecoderValues.integerTypeTag "i16" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.i16
• Miri.Input.DecoderValues.integerTypeTag "i32" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.i32
• Miri.Input.DecoderValues.integerTypeTag "i64" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.i64
• Miri.Input.DecoderValues.integerTypeTag "i128" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.i128
• Miri.Input.DecoderValues.integerTypeTag "isize" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.isize
• Miri.Input.DecoderValues.integerTypeTag "u8" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.u8
• Miri.Input.DecoderValues.integerTypeTag "u16" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.u16
• Miri.Input.DecoderValues.integerTypeTag "u32" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.u32
• Miri.Input.DecoderValues.integerTypeTag "u64" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.u64
• Miri.Input.DecoderValues.integerTypeTag "u128" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.u128
• Miri.Input.DecoderValues.integerTypeTag "usize" = Miri.Input.IntegerTypeTag.known Miri.MIR.IntegerKind.usize
• Miri.Input.DecoderValues.integerTypeTag text = Miri.Input.IntegerTypeTag.unknown text

def Miri.Input.DecoderValues.floatTypeTag (text : String) : FloatTypeTag

Equations

• Miri.Input.DecoderValues.floatTypeTag "f16" = Miri.Input.FloatTypeTag.f16
• Miri.Input.DecoderValues.floatTypeTag "f16b" = Miri.Input.FloatTypeTag.f16b
• Miri.Input.DecoderValues.floatTypeTag "f32" = Miri.Input.FloatTypeTag.f32
• Miri.Input.DecoderValues.floatTypeTag "f64" = Miri.Input.FloatTypeTag.f64
• Miri.Input.DecoderValues.floatTypeTag "f128" = Miri.Input.FloatTypeTag.f128
• Miri.Input.DecoderValues.floatTypeTag "ppcf128" = Miri.Input.FloatTypeTag.ppcf128
• Miri.Input.DecoderValues.floatTypeTag text = Miri.Input.FloatTypeTag.unknown text

def Miri.Input.DecoderValues.adtKindTag (text : String) : AdtKind

Equations

• Miri.Input.DecoderValues.adtKindTag "struct" = Miri.Input.AdtKind.structKind
• Miri.Input.DecoderValues.adtKindTag "union" = Miri.Input.AdtKind.unionKind
• Miri.Input.DecoderValues.adtKindTag "enum" = Miri.Input.AdtKind.enumKind
• Miri.Input.DecoderValues.adtKindTag text = Miri.Input.AdtKind.unknown text

def Miri.Input.DecoderValues.binOpFromExportTag (tag : String) : Option MIR.BinOp

Equations

• Miri.Input.DecoderValues.binOpFromExportTag "add" = some Miri.MIR.BinOp.Add
• Miri.Input.DecoderValues.binOpFromExportTag "add_unchecked" = some Miri.MIR.BinOp.AddUnchecked
• Miri.Input.DecoderValues.binOpFromExportTag "add_with_overflow" = some Miri.MIR.BinOp.AddWithOverflow
• Miri.Input.DecoderValues.binOpFromExportTag "sub" = some Miri.MIR.BinOp.Sub
• Miri.Input.DecoderValues.binOpFromExportTag "sub_unchecked" = some Miri.MIR.BinOp.SubUnchecked
• Miri.Input.DecoderValues.binOpFromExportTag "sub_with_overflow" = some Miri.MIR.BinOp.SubWithOverflow
• Miri.Input.DecoderValues.binOpFromExportTag "mul" = some Miri.MIR.BinOp.Mul
• Miri.Input.DecoderValues.binOpFromExportTag "mul_unchecked" = some Miri.MIR.BinOp.MulUnchecked
• Miri.Input.DecoderValues.binOpFromExportTag "mul_with_overflow" = some Miri.MIR.BinOp.MulWithOverflow
• Miri.Input.DecoderValues.binOpFromExportTag "div" = some Miri.MIR.BinOp.Div
• Miri.Input.DecoderValues.binOpFromExportTag "rem" = some Miri.MIR.BinOp.Rem
• Miri.Input.DecoderValues.binOpFromExportTag "bit_xor" = some Miri.MIR.BinOp.BitXor
• Miri.Input.DecoderValues.binOpFromExportTag "bit_and" = some Miri.MIR.BinOp.BitAnd
• Miri.Input.DecoderValues.binOpFromExportTag "bit_or" = some Miri.MIR.BinOp.BitOr
• Miri.Input.DecoderValues.binOpFromExportTag "shift_left" = some Miri.MIR.BinOp.Shl
• Miri.Input.DecoderValues.binOpFromExportTag "shift_left_unchecked" = some Miri.MIR.BinOp.ShlUnchecked
• Miri.Input.DecoderValues.binOpFromExportTag "shift_right" = some Miri.MIR.BinOp.Shr
• Miri.Input.DecoderValues.binOpFromExportTag "shift_right_unchecked" = some Miri.MIR.BinOp.ShrUnchecked
• Miri.Input.DecoderValues.binOpFromExportTag "equal" = some Miri.MIR.BinOp.Eq
• Miri.Input.DecoderValues.binOpFromExportTag "less_than" = some Miri.MIR.BinOp.Lt
• Miri.Input.DecoderValues.binOpFromExportTag "less_equal" = some Miri.MIR.BinOp.Le
• Miri.Input.DecoderValues.binOpFromExportTag "not_equal" = some Miri.MIR.BinOp.Ne
• Miri.Input.DecoderValues.binOpFromExportTag "greater_equal" = some Miri.MIR.BinOp.Ge
• Miri.Input.DecoderValues.binOpFromExportTag "greater_than" = some Miri.MIR.BinOp.Gt
• Miri.Input.DecoderValues.binOpFromExportTag "compare" = some Miri.MIR.BinOp.Cmp
• Miri.Input.DecoderValues.binOpFromExportTag "pointer_offset" = some Miri.MIR.BinOp.Offset
• Miri.Input.DecoderValues.binOpFromExportTag tag = Miri.MIR.BinOp.ofString tag

def Miri.Input.DecoderValues.unOpFromExportTag (tag : String) : Option MIR.UnOp

Equations

• Miri.Input.DecoderValues.unOpFromExportTag "not" = some Miri.MIR.UnOp.Not
• Miri.Input.DecoderValues.unOpFromExportTag "negate" = some Miri.MIR.UnOp.Neg
• Miri.Input.DecoderValues.unOpFromExportTag "pointer_metadata" = some Miri.MIR.UnOp.PtrMetadata
• Miri.Input.DecoderValues.unOpFromExportTag tag = Miri.MIR.UnOp.ofString tag

def Miri.Input.DecoderValues.statusField (j : Lean.Json) (path : String) (optional : Bool := false) : Except String PayloadStatus

Equations

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

def Miri.Input.DecoderValues.parseOperatorTag (j : Lean.Json) (path : String) : Except String (String × PayloadStatus)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.parseOperatorTag (Lean.Json.str text) path = pure (text, Miri.Input.PayloadStatus.supported)
• Miri.Input.DecoderValues.parseOperatorTag j path = throw (toString path ++ toString ": expected tagged operator object")

def Miri.Input.DecoderValues.typedEnumCategory? (key path : String) (parentTag : Option String) (j : Lean.Json) : Option TypedEnumTag

Equations

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

def Miri.Input.DecoderValues.parseInlineTag (j : Lean.Json) (path : String) : Except String TaggedNode

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.parseInlineTag (Lean.Json.str text) path = pure { status := Miri.Input.PayloadStatus.supported, tag := text, payload := Lean.Json.str text }
• Miri.Input.DecoderValues.parseInlineTag j path = throw (toString path ++ toString ": expected enum tag object or string")

def Miri.Input.DecoderValues.userTypeProjectionKind (j : Lean.Json) (path : String) : Except String UserTypeProjectionKind

Equations

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

def Miri.Input.DecoderValues.parseUserTypeProjection (j : Lean.Json) (path : String) : Except String UserTypeProjection

Equations

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

@[reducible, inline]

abbrev Miri.Input.DecoderValues.DecodeValueM (α : Type) : Type

Equations

• Miri.Input.DecoderValues.DecodeValueM = StateT (Std.HashMap Miri.Input.DecoderValues.DecodeValueKey Miri.Input.TypedValue) (Except String)

partial def Miri.Input.DecoderValues.decodeValueM (j : Lean.Json) (path : String) (domain : Domain) (tagCategory : Option TypedEnumTag) (memo : DecodeMemo) : DecodeValueM TypedValue

partial def Miri.Input.DecoderValues.decodeValueBody (j : Lean.Json) (path : String) (domain : Domain) (tagCategory : Option TypedEnumTag) (memo : DecodeMemo) : DecodeValueM TypedValue

def Miri.Input.DecoderValues.decodeValue (j : Lean.Json) (path : String) (domain : Domain := Domain.any) (tagCategory : Option TypedEnumTag := none) (memo : DecodeMemo := { }) : Except String TypedValue

Equations

• Miri.Input.DecoderValues.decodeValue j path domain tagCategory memo = StateT.run' (Miri.Input.DecoderValues.decodeValueM j path domain tagCategory memo) ∅

def Miri.Input.DecoderValues.statusObligation? (status : PayloadStatus) (path : String) : Option Obligation

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.statusObligation? Miri.Input.PayloadStatus.supported path = none
• Miri.Input.DecoderValues.statusObligation? Miri.Input.PayloadStatus.debugPayload path = none
• Miri.Input.DecoderValues.statusObligation? Miri.Input.PayloadStatus.unknown path = some { path := path, message := "exporter could not resolve this payload; it is an unresolved obligation" }
• Miri.Input.DecoderValues.statusObligation? Miri.Input.PayloadStatus.incomplete path = some { path := path, message := "exporter marked this payload incomplete; it is an unresolved obligation" }
• Miri.Input.DecoderValues.statusObligation? (Miri.Input.PayloadStatus.unrecognized value) path = some { path := path, message := toString "unrecognized status `" ++ toString value ++ toString "`" }

def Miri.Input.DecoderValues.unknownTagObligation (tag path : String) : Obligation

Equations

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

def Miri.Input.DecoderValues.enumTagKnown (category : TypedEnumTag) (tag : String) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.safety tag = (tag == "safe" || tag == "unsafe")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.borrowKind tag = (tag == "shared" || tag == "mutable" || tag == "fake")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.fakeBorrowKind tag = (tag == "shallow" || tag == "deep")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.mutBorrowKind tag = (tag == "default" || tag == "two_phase" || tag == "closure_capture")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.mutability tag = (tag == "mutable" || tag == "immutable")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.coercionSource tag = (tag == "as_cast" || tag == "implicit")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.unwindReason tag = (tag == "abi" || tag == "in_cleanup")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.unwindAction tag = (tag == "Continue" || tag == "Unreachable" || tag == "Terminate" || tag == "Cleanup")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.mirPhase tag = (tag == "built" || tag == "analysis" || tag == "runtime")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.mirPhaseStage tag = (tag == "initial" || tag == "post_cleanup" || tag == "optimized")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.withRetag tag = (tag == "yes" || tag == "no")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.runtimeCheck tag = (tag == "ub_checks" || tag == "contract_checks" || tag == "overflow_checks")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.backwardDropReason tag = (tag == "edition_2024")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.boundRegionKind tag = (tag == "anonymous" || tag == "named_for_printing" || tag == "named" || tag == "closure_environment")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.boundVarIndexKind tag = (tag == "bound" || tag == "canonical")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.lateParamRegionKind tag = (tag == "anonymous" || tag == "named_anonymous" || tag == "named" || tag == "closure_environment")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.integerType tag = ["i8", "i16", "i32", "i64", "i128", "isize", "u8", "u16", "u32", "u64", "u128", "usize"].contains tag
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.floatType tag = ["f16", "f16b", "f32", "f64", "f128", "ppcf128"].contains tag
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.adtKind tag = (tag == "struct" || tag == "union" || tag == "enum")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.variance tag = (tag == "covariant" || tag == "contravariant" || tag == "invariant" || tag == "bivariant")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.coverageKind tag = (tag == "point" || tag == "block_marker" || tag == "virtual_counter")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.coveragePointKind tag = (tag == "expr" || tag == "implicit_else" || tag == "function_end")
• Miri.Input.DecoderValues.enumTagKnown Miri.Input.TypedEnumTag.fakeBorrowRetagMode tag = (tag == "default")
• Miri.Input.DecoderValues.enumTagKnown (Miri.Input.TypedEnumTag.other value) tag = false

def Miri.Input.DecoderValues.valueLocalObligationsInto (value : TypedValue) (path : String) (initial : Array Obligation) : Array Obligation

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.scalar value_2) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.diagnostic value_2) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.typeRef id) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.allocationRef id) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.instanceRef id) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.localRef id) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.blockRef id) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.sourceSpan value_2) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.sourceInfo value_2) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.array values) path initial = (pure initial).run
• Miri.Input.DecoderValues.valueLocalObligationsInto (Miri.Input.TypedValue.object fields) path initial = (have out := initial; pure out).run

partial def Miri.Input.DecoderValues.valueObligationsInto (value : TypedValue) (path : String) (initial : Array Obligation) : Array Obligation

def Miri.Input.DecoderValues.valueObligations (value : TypedValue) (path : String) : Array Obligation

Equations

• Miri.Input.DecoderValues.valueObligations value path = Miri.Input.DecoderValues.valueObligationsInto value path #[]

inductive Miri.Input.DecoderValues.RuntimeObligationSequence : Type

• leaf (items : Array Obligation) : RuntimeObligationSequence
• append (left right : RuntimeObligationSequence) : RuntimeObligationSequence
• rebase (oldPath newPath : String) (inner : RuntimeObligationSequence) : RuntimeObligationSequence

@[instance_reducible]

instance Miri.Input.DecoderValues.instInhabitedRuntimeObligationSequence : Inhabited RuntimeObligationSequence

Equations

• Miri.Input.DecoderValues.instInhabitedRuntimeObligationSequence = { default := Miri.Input.DecoderValues.instInhabitedRuntimeObligationSequence.default }

def Miri.Input.DecoderValues.appendRuntimeObligations (left right : Option RuntimeObligationSequence) : Option RuntimeObligationSequence

Equations

• Miri.Input.DecoderValues.appendRuntimeObligations none right = right
• Miri.Input.DecoderValues.appendRuntimeObligations left none = left
• Miri.Input.DecoderValues.appendRuntimeObligations (some left_2) (some right_2) = some (left_2.append right_2)

def Miri.Input.DecoderValues.rebaseRuntimeObligation (issue : Obligation) (oldPath newPath : String) : Obligation

Equations

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

def Miri.Input.DecoderValues.flattenRuntimeObligations (sequence : Option RuntimeObligationSequence) : Array Obligation

Equations

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

structure Miri.Input.DecoderValues.RuntimeValueDecode : Type

• summary : TypedValue

  Only the direct fields consumed by the parent's local invariants.

• obligations : Option RuntimeObligationSequence

structure Miri.Input.DecoderValues.RuntimeValueKey : Type

Document-local node identity plus every decoding context flag. Only successful results are memoized; diagnostics are rebased separately for each occurrence.

• json : JsonTraversalCache.IdentityKey
• domain : Domain
• tagCategory : Option TypedEnumTag
• isRegionPath : Bool
• isHirIdPath : Bool
• isCoveragePath : Bool
• isCastCoercionPath : Bool

@[instance_reducible]

instance Miri.Input.DecoderValues.instBEqRuntimeValueKey : BEq RuntimeValueKey

Equations

• Miri.Input.DecoderValues.instBEqRuntimeValueKey = { beq := Miri.Input.DecoderValues.instBEqRuntimeValueKey.beq }

def Miri.Input.DecoderValues.instBEqRuntimeValueKey.beq : RuntimeValueKey → RuntimeValueKey → Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.instBEqRuntimeValueKey.beq x✝¹ x✝ = false

@[instance_reducible]

instance Miri.Input.DecoderValues.instHashableRuntimeValueKey : Hashable RuntimeValueKey

Equations

• Miri.Input.DecoderValues.instHashableRuntimeValueKey = { hash := Miri.Input.DecoderValues.instHashableRuntimeValueKey.hash }

def Miri.Input.DecoderValues.instHashableRuntimeValueKey.hash : RuntimeValueKey → UInt64

Equations

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

def Miri.Input.DecoderValues.runtimeValueKey (node : JsonTraversalCache.Node) (path : String) (domain : Domain) (tagCategory : Option TypedEnumTag) : RuntimeValueKey

Equations

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

theorem Miri.Input.DecoderValues.runtimeValueKey_uncached_beq_eq (a b : Lean.Json) (pathA pathB : String) (domainA domainB : Domain) (tagA tagB : Option TypedEnumTag) : (runtimeValueKey (JsonTraversalCache.Node.uncached a) pathA domainA tagA == runtimeValueKey (JsonTraversalCache.Node.uncached b) pathB domainB tagB) = (decodeValueKey a pathA domainA tagA == decodeValueKey b pathB domainB tagB)

The raw fallback retains the original key comparison and hash exactly, including manually constructed JSON whose BEq need not be lawful.

theorem Miri.Input.DecoderValues.runtimeValueKey_uncached_hash_eq (value : Lean.Json) (path : String) (domain : Domain) (tag : Option TypedEnumTag) : hash (runtimeValueKey (JsonTraversalCache.Node.uncached value) path domain tag) = hash (decodeValueKey value path domain tag)

@[reducible, inline]

abbrev Miri.Input.DecoderValues.RuntimeDecodeCache : Type

Equations

• Miri.Input.DecoderValues.RuntimeDecodeCache = Std.HashMap Miri.Input.DecoderValues.RuntimeValueKey (String × Miri.Input.DecoderValues.RuntimeValueDecode)

def Miri.Input.DecoderValues.runtimeLocalObligations (value : TypedValue) (path : String) (children : Option RuntimeObligationSequence := none) : Option RuntimeObligationSequence

Equations

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

opaque Miri.Input.DecoderValues.runtimeSummaryKeys : Std.HashSet String

def Miri.Input.DecoderValues.runtimeSummaryChild (key : String) (value : TypedValue) : TypedValue

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.runtimeSummaryChild key (Miri.Input.TypedValue.object fields) = if (key == "hir_id") = true then Miri.Input.TypedValue.object fields else Miri.Input.TypedValue.object #[]
• Miri.Input.DecoderValues.runtimeSummaryChild key (Miri.Input.TypedValue.array values) = if (key == "hir_id") = true then Miri.Input.TypedValue.array values else Miri.Input.TypedValue.array #[]
• Miri.Input.DecoderValues.runtimeSummaryChild key value = if (key == "hir_id") = true then value else value

@[reducible, inline]

abbrev Miri.Input.DecoderValues.RuntimeDecodeM (α : Type) : Type

Equations

• Miri.Input.DecoderValues.RuntimeDecodeM = StateT Miri.Input.DecoderValues.RuntimeDecodeCache (Except String)

partial def Miri.Input.DecoderValues.decodeRuntimeValueM (node : JsonTraversalCache.Node) (path : String) (domain : Domain) (tagCategory : Option TypedEnumTag) (memo : DecodeMemo) : RuntimeDecodeM RuntimeValueDecode

partial def Miri.Input.DecoderValues.decodeRuntimeValueBody (node : JsonTraversalCache.Node) (path : String) (domain : Domain) (tagCategory : Option TypedEnumTag) (memo : DecodeMemo) : RuntimeDecodeM RuntimeValueDecode

def Miri.Input.DecoderValues.decodeRuntimeValue (node : JsonTraversalCache.Node) (path : String) (domain : Domain := Domain.any) (tagCategory : Option TypedEnumTag := none) (memo : DecodeMemo := { }) : Except String RuntimeValueDecode

Equations

• Miri.Input.DecoderValues.decodeRuntimeValue node path domain tagCategory memo = StateT.run' (Miri.Input.DecoderValues.decodeRuntimeValueM node path domain tagCategory memo) ∅

def Miri.Input.DecoderValues.jsonArray (j : Lean.Json) (path : String) : Except String (Array Lean.Json)

Equations

• Miri.Input.DecoderValues.jsonArray j path = Except.mapError (fun (e : String) => toString path ++ toString ": expected array (" ++ toString e ++ toString ")") j.getArr?

def Miri.Input.DecoderValues.natArray (j : Lean.Json) (path : String) : Except String (Array Nat)

Equations

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

def Miri.Input.DecoderValues.optionalNat (j : Lean.Json) (key path : String) : Except String (Option Nat)

Equations

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

def Miri.Input.DecoderValues.optionalJson (j : Lean.Json) (key : String) : Option Lean.Json

Equations

• Miri.Input.DecoderValues.optionalJson j key = Option.filter (fun (x : Lean.Json) => x != Lean.Json.null) (Miri.Input.DecoderValues.optionalField j key)

def Miri.Input.DecoderValues.parseTagged (j : Lean.Json) (path : String) : Except String TaggedNode

Equations

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

def Miri.Input.DecoderValues.parseAbiTag (j : Lean.Json) (path : String) : Except String TaggedNode

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.parseAbiTag (Lean.Json.str text) path = pure { status := Miri.Input.PayloadStatus.supported, tag := text, payload := Lean.Json.str text }
• Miri.Input.DecoderValues.parseAbiTag j path = throw (toString path ++ toString ": expected enum tag string or tagged object")

def Miri.Input.DecoderValues.layoutVariantsKind (tag : String) : LayoutVariantsKind

Equations

• Miri.Input.DecoderValues.layoutVariantsKind "single" = Miri.Input.LayoutVariantsKind.single
• Miri.Input.DecoderValues.layoutVariantsKind "multiple" = Miri.Input.LayoutVariantsKind.multiple
• Miri.Input.DecoderValues.layoutVariantsKind "empty" = Miri.Input.LayoutVariantsKind.empty
• Miri.Input.DecoderValues.layoutVariantsKind tag = Miri.Input.LayoutVariantsKind.unknown tag

def Miri.Input.DecoderValues.backendReprKind (tag : String) : BackendReprKind

Equations

• Miri.Input.DecoderValues.backendReprKind "scalar" = Miri.Input.BackendReprKind.scalar
• Miri.Input.DecoderValues.backendReprKind "scalar_pair" = Miri.Input.BackendReprKind.scalarPair
• Miri.Input.DecoderValues.backendReprKind "memory" = Miri.Input.BackendReprKind.memory
• Miri.Input.DecoderValues.backendReprKind "simd_vector" = Miri.Input.BackendReprKind.simdVector
• Miri.Input.DecoderValues.backendReprKind "scalable_simd_vector" = Miri.Input.BackendReprKind.scalableSimdVector
• Miri.Input.DecoderValues.backendReprKind tag = Miri.Input.BackendReprKind.unknown tag

def Miri.Input.DecoderValues.optionalNatBefore (j : Lean.Json) (key path : String) : Except String (Option Nat)

Equations

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

def Miri.Input.DecoderValues.parsePrimitiveLayout (j : Lean.Json) (path : String) : Except String PrimitiveLayout

Equations

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

def Miri.Input.DecoderValues.parseU128Natural (j : Lean.Json) (path : String) : Except String Nat

Exact compiler u128 encoding; preserve legacy JSON naturals while allowing full-width decimal strings that serde_json cannot represent as numbers.

Equations

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

def Miri.Input.DecoderValues.parseScalarLayout (j : Lean.Json) (path : String) : Except String ScalarLayout

Equations

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

def Miri.Input.DecoderValues.parseBackendRepr (j : Lean.Json) (path : String) : Except String BackendRepr

Equations

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

def Miri.Input.DecoderValues.parseFieldShape (j : Lean.Json) (path : String) : Except String FieldShape

Equations

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

def Miri.Input.DecoderValues.parseLayoutVariant (j : Lean.Json) (path : String) : Except String LayoutVariant

Equations

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

def Miri.Input.DecoderValues.decimalNat (text path : String) : Except String Nat

Equations

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

def Miri.Input.DecoderValues.parseTagEncoding (j : Lean.Json) (path : String) : Except String TagEncoding

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.DecoderValues.parseTagEncoding j path = throw (toString path ++ toString ": expected structured tag encoding")

def Miri.Input.DecoderValues.parseVariantsLayout (j : Lean.Json) (path : String) : Except String VariantsLayout

Equations

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

def Miri.Input.DecoderValues.parseLayoutUncached (j : Lean.Json) (path : String) : Except String Layout

Equations

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

def Miri.Input.DecoderValues.parseLayout (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String Layout

Equations

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

def Miri.Input.DecoderValues.isLayoutPayload (j : Lean.Json) : Bool

Equations

• Miri.Input.DecoderValues.isLayoutPayload j = (Miri.Input.DecoderValues.hasField j "status" && Miri.Input.DecoderValues.hasField j "field_offsets_bytes")

partial def Miri.Input.DecoderValues.hasCanonicalJsonObjectKeys : Lean.Json → Bool

JSON equality and hashing are only used as memo keys for canonical object trees. In particular, never cache a Raw object whose inorder keys are not strictly increasing, since malformed raw object trees can violate BEq symmetry.

def Miri.Input.DecoderValues.collectSharedDecodeMemo (j : Lean.Json) (path : String) (memo : DecodeMemo) : DecodeMemo

Equations

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

def Miri.Input.DecoderValues.sharedDecodeMemo (nodes : Array Lean.Json) : DecodeMemo

Equations

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

def Miri.Input.DecoderValues.compilerFunctionAbiDecodeMemo (nodes : Array Lean.Json) : DecodeMemo

Equations

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

structure Miri.Input.DecoderValues.CompilerFunctionAbiMemo : Type

Opaque success-only layout memo for repeated decoding of compiler FnAbi payloads from one shared-payload node table. The constructor ensures callers can prepare only the decoder's checked memo representation.

• memo : Miri.Input.DecoderValues.DecodeMemo

def Miri.Input.DecoderValues.prepareCompilerFunctionAbiMemo (nodes : Array Lean.Json) : CompilerFunctionAbiMemo

Prepare a reusable FnAbi decoder memo from a runtime's shared payloads. Malformed layouts are deliberately not cached, preserving occurrence paths.

Equations

• Miri.Input.prepareCompilerFunctionAbiMemo nodes = { memo := Miri.Input.DecoderValues.compilerFunctionAbiDecodeMemo nodes }

def Miri.Input.DecoderValues.parseFunctionSignature (j : Lean.Json) (path : String) : Except String FunctionSignature

Equations

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

def Miri.Input.DecoderValues.decodeCompilerPredicateEvidence (j : Lean.Json) : Except String CompilerPredicateEvidence

Equations

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

partial def Miri.Input.DecoderValues.decodeCompilerPattern (j : Lean.Json) : Except String CompilerPattern

Decode all source PatternKind branches; unknown kinds fail explicitly.

def Miri.Input.DecoderValues.decodeTypeCompilerFacts (j : Lean.Json) (path : String := "$compiler_facts") : Except String TypeCompilerFacts

Preserve the compiler query's exact type and typing-environment key.

Equations

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

def Miri.Input.DecoderValues.parseTypeNode (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String TypeNode

Equations

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

def Miri.Input.DecoderValues.hexDigit (c : Char) : Bool

Equations

• Miri.Input.DecoderValues.hexDigit c = (c.isDigit || decide ('a' ≤ c) && decide (c ≤ 'f') || decide ('A' ≤ c) && decide (c ≤ 'F'))

def Miri.Input.DecoderValues.validHex (value : String) : Bool

Equations

• Miri.Input.DecoderValues.validHex value = (value.toList.all Miri.Input.DecoderValues.hexDigit && value.length % 2 == 0)

def Miri.Input.DecoderValues.parseInitRange (j : Lean.Json) (path : String) : Except String InitRange

Equations

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

def Miri.Input.DecoderValues.parseRelocation (j : Lean.Json) (path : String) : Except String Relocation

Equations

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

def Miri.Input.DecoderValues.parseAllocationMemory (j : Lean.Json) (path : String) : Except String AllocationMemory

Equations

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

def Miri.Input.DecoderValues.allocationKind (kind : String) : AllocationKind

Equations

• Miri.Input.DecoderValues.allocationKind "memory" = Miri.Input.AllocationKind.memory
• Miri.Input.DecoderValues.allocationKind "function" = Miri.Input.AllocationKind.function
• Miri.Input.DecoderValues.allocationKind "static" = Miri.Input.AllocationKind.static
• Miri.Input.DecoderValues.allocationKind "vtable" = Miri.Input.AllocationKind.vtable
• Miri.Input.DecoderValues.allocationKind "type_id" = Miri.Input.AllocationKind.typeId
• Miri.Input.DecoderValues.allocationKind "" = Miri.Input.AllocationKind.unknown
• Miri.Input.DecoderValues.allocationKind kind = Miri.Input.AllocationKind.other kind

def Miri.Input.DecoderValues.parseDefinitionId (j : Lean.Json) (path : String) : Except String DefinitionId

Equations

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

def Miri.Input.DecoderValues.parseSelectedScope (j : Lean.Json) (path : String) : Except String SelectedScope

Equations

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

def Miri.Input.DecoderValues.vtablePredicateKind (tag : String) : VtablePredicateKind

Equations

• Miri.Input.DecoderValues.vtablePredicateKind "trait" = Miri.Input.VtablePredicateKind.trait
• Miri.Input.DecoderValues.vtablePredicateKind "auto_trait" = Miri.Input.VtablePredicateKind.autoTrait
• Miri.Input.DecoderValues.vtablePredicateKind "projection" = Miri.Input.VtablePredicateKind.projection
• Miri.Input.DecoderValues.vtablePredicateKind tag = Miri.Input.VtablePredicateKind.unknown tag

def Miri.Input.DecoderValues.parseVtablePredicate (j : Lean.Json) (path : String) : Except String VtablePredicate

Equations

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

def Miri.Input.DecoderValues.vtableEntryKind (tag : String) : VtableEntryKind

Equations

• Miri.Input.DecoderValues.vtableEntryKind "drop_in_place_null" = Miri.Input.VtableEntryKind.dropInPlaceNull
• Miri.Input.DecoderValues.vtableEntryKind "drop_in_place" = Miri.Input.VtableEntryKind.dropInPlace
• Miri.Input.DecoderValues.vtableEntryKind "size_bytes" = Miri.Input.VtableEntryKind.sizeBytes
• Miri.Input.DecoderValues.vtableEntryKind "align_bytes" = Miri.Input.VtableEntryKind.alignBytes
• Miri.Input.DecoderValues.vtableEntryKind "vacant" = Miri.Input.VtableEntryKind.vacant
• Miri.Input.DecoderValues.vtableEntryKind "method" = Miri.Input.VtableEntryKind.method
• Miri.Input.DecoderValues.vtableEntryKind "supertrait_vtable_pointer" = Miri.Input.VtableEntryKind.supertraitVtablePointer
• Miri.Input.DecoderValues.vtableEntryKind tag = Miri.Input.VtableEntryKind.unknown tag

def Miri.Input.DecoderValues.parseVtableEntry (j : Lean.Json) (path : String) : Except String VtableEntry

Equations

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

def Miri.Input.DecoderValues.decodeVtableEntry (j : Lean.Json) (path : String := "$compiler_vtable_entry") : Except String VtableEntry

Decode a source tcx.vtable_entries row retained outside a GlobalAlloc image. Runtime-created vtables use this exact metadata without borrowing the CTFE probe's allocation identity.

Equations

• Miri.Input.decodeVtableEntry j path = Miri.Input.DecoderValues.parseVtableEntry j path

def Miri.Input.DecoderValues.decodeStaticGlobalInfo (j : Lean.Json) (path : String := "$static_global_info") : Except String StaticGlobalInfo

Decode compiler-query static metadata, retaining the original evidence.

Equations

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

def Miri.Input.DecoderValues.parseAllocation (j : Lean.Json) (path : String) : Except String AllocationNode

Equations

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

def Miri.Input.DecoderValues.parseSourceAllocIdKind (value path : String) : Except String SourceAllocIdKind

Equations

• Miri.Input.DecoderValues.parseSourceAllocIdKind "dangling" path = pure Miri.Input.SourceAllocIdKind.dangling
• Miri.Input.DecoderValues.parseSourceAllocIdKind "memory" path = pure Miri.Input.SourceAllocIdKind.memory
• Miri.Input.DecoderValues.parseSourceAllocIdKind "function" path = pure Miri.Input.SourceAllocIdKind.function
• Miri.Input.DecoderValues.parseSourceAllocIdKind "vtable" path = pure Miri.Input.SourceAllocIdKind.vtable
• Miri.Input.DecoderValues.parseSourceAllocIdKind "static" path = pure Miri.Input.SourceAllocIdKind.static
• Miri.Input.DecoderValues.parseSourceAllocIdKind "type_id" path = pure Miri.Input.SourceAllocIdKind.typeId
• Miri.Input.DecoderValues.parseSourceAllocIdKind value path = throw (toString path ++ toString ": unknown source AllocId kind `" ++ toString value ++ toString "`")

def Miri.Input.DecoderValues.canonicalLowerHex (value : String) : Bool

Equations

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

def Miri.Input.DecoderValues.allocationNodeMatchesSourceKind (sourceKind : SourceAllocIdKind) (nodeKind : AllocationKind) : Bool

Equations

• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind Miri.Input.SourceAllocIdKind.memory Miri.Input.AllocationKind.memory = true
• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind Miri.Input.SourceAllocIdKind.function Miri.Input.AllocationKind.function = true
• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind Miri.Input.SourceAllocIdKind.vtable Miri.Input.AllocationKind.vtable = true
• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind Miri.Input.SourceAllocIdKind.static Miri.Input.AllocationKind.static = true
• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind Miri.Input.SourceAllocIdKind.typeId Miri.Input.AllocationKind.typeId = true
• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind Miri.Input.SourceAllocIdKind.static (Miri.Input.AllocationKind.other "static_initializer_error") = true
• Miri.Input.DecoderValues.allocationNodeMatchesSourceKind sourceKind nodeKind = false

def Miri.Input.DecoderValues.parseSourceAllocIdDedupKind (value path : String) : Except String SourceAllocIdDedupKind

Equations

• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "function" path = pure Miri.Input.SourceAllocIdDedupKind.function
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "vtable" path = pure Miri.Input.SourceAllocIdDedupKind.vtable
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "static" path = pure Miri.Input.SourceAllocIdDedupKind.static
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "type_id" path = pure Miri.Input.SourceAllocIdDedupKind.typeId
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "memory" path = pure Miri.Input.SourceAllocIdDedupKind.memory
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "memory_const_allocation" path = pure Miri.Input.SourceAllocIdDedupKind.memory
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "bytes" path = pure Miri.Input.SourceAllocIdDedupKind.bytes
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind "byte_memory" path = pure Miri.Input.SourceAllocIdDedupKind.bytes
• Miri.Input.DecoderValues.parseSourceAllocIdDedupKind value path = throw (toString path ++ toString ": unknown source AllocId dedup key kind `" ++ toString value ++ toString "`")

def Miri.Input.DecoderValues.parseSourceAllocIdPoolRow (j : Lean.Json) (path : String) : Except String SourceAllocIdPoolRow

Equations

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

def Miri.Input.DecoderValues.parseSourceAllocIdSaltResult (j : Lean.Json) (path : String) : Except String SourceAllocIdSaltResult

Equations

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

def Miri.Input.DecoderValues.parseSourceAllocIdDedupRow (j : Lean.Json) (path : String) : Except String SourceAllocIdDedupRow

Equations

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

def Miri.Input.DecoderValues.parseCompilerAllocIdWorld (j : Lean.Json) (nodes : Array AllocationNode) : Except String CompilerAllocIdWorld

Equations

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

def Miri.Input.DecoderValues.validateCompilerAllocIdWorldRaw (raw : Lean.Json) (nodes : Array AllocationNode) (world : Option CompilerAllocIdWorld) : Except String Unit

Revalidate allocation identity metadata against the exact retained raw document. Public model records can be assembled or updated by callers, so the prepared runtime must not trust the decoder's prior validation as a flag.

Equations

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

def Miri.Input.DecoderValues.parseLocal (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String LocalDecl

Equations

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

def Miri.Input.DecoderValues.parseMirNode (wrapper : Lean.Json) (path : String) (domain : Domain) (memo : DecodeMemo := { }) : Except String MirNode

Equations

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

def Miri.Input.DecoderValues.parseBasicBlock (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String BasicBlock

Equations

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

def Miri.Input.DecoderValues.parseBodyCore (j : Lean.Json) (path fallbackName : String) (memo : DecodeMemo := { }) : Except String BodyCore

Equations

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

def Miri.Input.DecoderValues.parsePromotedBodies (j : Lean.Json) (path fallbackName : String) (memo : DecodeMemo := { }) : Except String (Array PromotedBody)

Equations

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

def Miri.Input.DecoderValues.parseBody (j : Lean.Json) (path fallbackName : String) (memo : DecodeMemo := { }) : Except String Body

Equations

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

def Miri.Input.DecoderValues.parseInstance (j : Lean.Json) (path : String) : Except String InstanceNode

Equations

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

def Miri.Input.DecoderValues.passModeKind (tag : String) : PassModeKind

Equations

• Miri.Input.DecoderValues.passModeKind "Ignore" = Miri.Input.PassModeKind.ignore
• Miri.Input.DecoderValues.passModeKind "Direct" = Miri.Input.PassModeKind.direct
• Miri.Input.DecoderValues.passModeKind "Pair" = Miri.Input.PassModeKind.pair
• Miri.Input.DecoderValues.passModeKind "Cast" = Miri.Input.PassModeKind.cast
• Miri.Input.DecoderValues.passModeKind "Indirect" = Miri.Input.PassModeKind.indirect
• Miri.Input.DecoderValues.passModeKind "IndirectUnsized" = Miri.Input.PassModeKind.indirectUnsized
• Miri.Input.DecoderValues.passModeKind tag = Miri.Input.PassModeKind.unknown tag

def Miri.Input.DecoderValues.parseAbiAttributes (j : Lean.Json) (path : String) : Except String AbiAttributes

Equations

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

def Miri.Input.DecoderValues.abiRegisterKind (tag : String) : AbiRegisterKind

Equations

• Miri.Input.DecoderValues.abiRegisterKind "integer" = Miri.Input.AbiRegisterKind.integer
• Miri.Input.DecoderValues.abiRegisterKind "float" = Miri.Input.AbiRegisterKind.float
• Miri.Input.DecoderValues.abiRegisterKind "ppc_f128" = Miri.Input.AbiRegisterKind.ppcF128
• Miri.Input.DecoderValues.abiRegisterKind "vector" = Miri.Input.AbiRegisterKind.vector
• Miri.Input.DecoderValues.abiRegisterKind tag = Miri.Input.AbiRegisterKind.unknown tag

def Miri.Input.DecoderValues.canonicalAbiKind (tag : String) : CanonicalAbiKind

Equations

• Miri.Input.DecoderValues.canonicalAbiKind "c" = Miri.Input.CanonicalAbiKind.c
• Miri.Input.DecoderValues.canonicalAbiKind "rust" = Miri.Input.CanonicalAbiKind.rust
• Miri.Input.DecoderValues.canonicalAbiKind "rust_cold" = Miri.Input.CanonicalAbiKind.rustCold
• Miri.Input.DecoderValues.canonicalAbiKind "rust_preserve_none" = Miri.Input.CanonicalAbiKind.rustPreserveNone
• Miri.Input.DecoderValues.canonicalAbiKind "rust_tail" = Miri.Input.CanonicalAbiKind.rustTail
• Miri.Input.DecoderValues.canonicalAbiKind "custom" = Miri.Input.CanonicalAbiKind.custom
• Miri.Input.DecoderValues.canonicalAbiKind "swift" = Miri.Input.CanonicalAbiKind.swift
• Miri.Input.DecoderValues.canonicalAbiKind "arm" = Miri.Input.CanonicalAbiKind.arm
• Miri.Input.DecoderValues.canonicalAbiKind "gpu_kernel" = Miri.Input.CanonicalAbiKind.gpuKernel
• Miri.Input.DecoderValues.canonicalAbiKind "interrupt" = Miri.Input.CanonicalAbiKind.interrupt
• Miri.Input.DecoderValues.canonicalAbiKind "x86" = Miri.Input.CanonicalAbiKind.x86
• Miri.Input.DecoderValues.canonicalAbiKind tag = Miri.Input.CanonicalAbiKind.unknown tag

def Miri.Input.DecoderValues.armCallKind (tag : String) : ArmCallKind

Equations

• Miri.Input.DecoderValues.armCallKind "aapcs" = Miri.Input.ArmCallKind.aapcs
• Miri.Input.DecoderValues.armCallKind "cmse_nonsecure_call" = Miri.Input.ArmCallKind.cmseNonSecureCall
• Miri.Input.DecoderValues.armCallKind "cmse_nonsecure_entry" = Miri.Input.ArmCallKind.cmseNonSecureEntry
• Miri.Input.DecoderValues.armCallKind tag = Miri.Input.ArmCallKind.unknown tag

def Miri.Input.DecoderValues.interruptCallKind (tag : String) : InterruptCallKind

Equations

• Miri.Input.DecoderValues.interruptCallKind "avr" = Miri.Input.InterruptCallKind.avr
• Miri.Input.DecoderValues.interruptCallKind "avr_non_blocking" = Miri.Input.InterruptCallKind.avrNonBlocking
• Miri.Input.DecoderValues.interruptCallKind "msp430" = Miri.Input.InterruptCallKind.msp430
• Miri.Input.DecoderValues.interruptCallKind "riscv_machine" = Miri.Input.InterruptCallKind.riscvMachine
• Miri.Input.DecoderValues.interruptCallKind "riscv_supervisor" = Miri.Input.InterruptCallKind.riscvSupervisor
• Miri.Input.DecoderValues.interruptCallKind "x86" = Miri.Input.InterruptCallKind.x86
• Miri.Input.DecoderValues.interruptCallKind tag = Miri.Input.InterruptCallKind.unknown tag

def Miri.Input.DecoderValues.x86CallKind (tag : String) : X86CallKind

Equations

• Miri.Input.DecoderValues.x86CallKind "fastcall" = Miri.Input.X86CallKind.fastcall
• Miri.Input.DecoderValues.x86CallKind "stdcall" = Miri.Input.X86CallKind.stdcall
• Miri.Input.DecoderValues.x86CallKind "sysv64" = Miri.Input.X86CallKind.sysv64
• Miri.Input.DecoderValues.x86CallKind "thiscall" = Miri.Input.X86CallKind.thiscall
• Miri.Input.DecoderValues.x86CallKind "vectorcall" = Miri.Input.X86CallKind.vectorcall
• Miri.Input.DecoderValues.x86CallKind "win64" = Miri.Input.X86CallKind.win64
• Miri.Input.DecoderValues.x86CallKind tag = Miri.Input.X86CallKind.unknown tag

def Miri.Input.DecoderValues.parseCanonicalAbi (j : Lean.Json) (path : String) : Except String CanonicalAbi

Equations

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

def Miri.Input.DecoderValues.parseAbiRegister (j : Lean.Json) (path : String) : Except String AbiRegister

Equations

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

def Miri.Input.DecoderValues.parseAbiCastTarget (j : Lean.Json) (path : String) : Except String AbiCastTarget

Equations

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

def Miri.Input.DecoderValues.parseAbiPassMode (j : Lean.Json) (path : String) : Except String AbiPassMode

Equations

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

def Miri.Input.DecoderValues.parseAbiArgument (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String AbiArgument

Equations

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

def Miri.Input.DecoderValues.parseFunctionAbi (j : Lean.Json) (path : String) (memo : DecodeMemo := { }) : Except String FunctionAbi

Equations

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

def Miri.Input.DecoderValues.decodeCompilerLayout (j : Lean.Json) : Except String Layout

Decode an exact compiler projection layout using the canonical schema.

Equations

• Miri.Input.decodeCompilerLayout j = Miri.Input.DecoderValues.parseLayout j "$.compiler_projection_layout"

def Miri.Input.DecoderValues.decodeCompilerFunctionAbi (j : Lean.Json) : Except String FunctionAbi

Decode an independently keyed compiler FnAbi query using the canonical schema.

Equations

• Miri.Input.decodeCompilerFunctionAbi j = Miri.Input.DecoderValues.parseFunctionAbi j "$.compiler_fn_abi"

def Miri.Input.DecoderValues.decodeCompilerFunctionAbiWithMemo (j : Lean.Json) (memo : CompilerFunctionAbiMemo) : Except String FunctionAbi

Decode a compiler FnAbi using successful layouts collected from the same shared-payload table. Failures and diagnostics follow the uncached decoder.

Equations

• Miri.Input.decodeCompilerFunctionAbiWithMemo j memo = Miri.Input.DecoderValues.parseFunctionAbi j "$.compiler_fn_abi" (Miri.Input.DecoderValues.CompilerFunctionAbiMemo.memo✝ memo)

def Miri.Input.DecoderValues.isFunctionAbiCandidate (raw : Lean.Json) : Bool

Equations

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

structure Miri.Input.DecoderValues.CompilerFunctionAbiTable (nodes : Array Lean.Json) : Type

A typed projection bound to the exact immutable shared-node table. The constructor cannot install results from another decoder or another document.

• entries : Array (Lean.Json × Except String FunctionAbi)
• exact : ∃ (memo : Miri.Input.CompilerFunctionAbiMemo), self.entries = buildCompilerFunctionAbiEntries nodes memo

def Miri.Input.DecoderValues.prepareCompilerFunctionAbiTableUsing (nodes : Array Lean.Json) (memo : DecodeMemo) : CompilerFunctionAbiTable nodes

Reuse the importer's successful layout memo. Failed query decodes are values, not import failures, and keep the canonical demand-time diagnostic path.

Equations

• Miri.Input.DecoderValues.prepareCompilerFunctionAbiTableUsing nodes memo = { entries := Miri.Input.DecoderValues.buildCompilerFunctionAbiEntries✝ nodes { memo := memo }, exact := ⋯ }

def Miri.Input.DecoderValues.CompilerFunctionAbiTable.extendDecodeMemo {nodes : Array Lean.Json} (table : CompilerFunctionAbiTable nodes) (base : DecodeMemo) : DecodeMemo

Successful projections can also serve the occurrence-sensitive collector. Failures deliberately fall through so its original path and first error survive.

Equations

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

def Miri.Input.DecoderValues.decodeCompilerValue (j : Lean.Json) : Except String TypedValue

The context used by compiler adapters is separate from runtime-readiness summaries. These are complete typed values, including source coordinates.

Equations

• Miri.Input.decodeCompilerValue j = Miri.Input.DecoderValues.decodeValue j "$compiler_value"

structure Miri.Input.DecoderValues.CompilerValueMemo : Type

Every entry is a checked decoder outcome for its JSON key. Unlike an instance/type lookup, this cache may safely survive a document record update: its immutable keys include the entire source value, never only a local ID.

• entries : Std.HashMap Lean.Json (Except String Miri.Input.TypedValue)
• exact : ∃ (nodes : Array Lean.Json), ∃ (memo : Miri.Input.DecoderValues.DecodeMemo), entries self = buildCompilerValueEntries nodes memo

def Miri.Input.DecoderValues.prepareCompilerValueMemoUsing (nodes : Array Lean.Json) (memo : DecodeMemo) : CompilerValueMemo

Equations

• Miri.Input.DecoderValues.prepareCompilerValueMemoUsing nodes memo = { entries := Miri.Input.DecoderValues.buildCompilerValueEntries✝ nodes memo, exact := ⋯ }

def Miri.Input.DecoderValues.decodeCompilerValueWithMemo (raw : Lean.Json) (memo : Option CompilerValueMemo) : Except String TypedValue

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.decodeCompilerValueWithMemo raw none = Miri.Input.decodeCompilerValue raw