@[instance_reducible]

instance Miri.Input.instBEqQueryDependencyRole : BEq Miri.Input.QueryDependencyRole✝

Equations

• Miri.Input.instBEqQueryDependencyRole = { beq := Miri.Input.instBEqQueryDependencyRole.beq }

def Miri.Input.instBEqQueryDependencyRole.beq : Miri.Input.QueryDependencyRole✝ → Miri.Input.QueryDependencyRole✝ → Bool

Equations

• Miri.Input.instBEqQueryDependencyRole.beq x✝ y✝ = (Miri.Input.QueryDependencyRole.ctorIdx✝ x✝ == Miri.Input.QueryDependencyRole.ctorIdx✝ y✝)

def Miri.Input.jsonAtPath (j : Lean.Json) (path : String) : Option Lean.Json

Equations

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

def Miri.Input.exactVtableProbeDiagnostic (j : Lean.Json) (path : String) : Bool

The exporter may retain its salt-zero CTFE vtable probe as diagnostic evidence, but it is not a runtime allocation identity. Only the exact probe leaf attached to a supported concrete Unsize Cast and backed by a supported exact-pair query is demand-local. The enclosing Cast must itself be supported; all other statuses and descendants remain structural blockers.

Equations

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

def Miri.Input.decodeJson (text : String) : Except String DecodeResult

Equations

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

def Miri.Input.decodeFile (path : System.FilePath) : IO (Except String DecodeResult)

Equations

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

def Miri.Input.decodeRuntimeJsonProfiled (text : String) (profile : Lean.Options) : Except String RuntimeDecodeResult

Runtime decoder with optional Lean profiler options. Profiling wrappers are kernel identity functions; with profiling disabled this preserves the ordinary decoder result and diagnostic order.

Equations

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

def Miri.Input.decodeRuntimeJsonReference (text : String) : Except String RuntimeDecodeResult

Regression oracle: identical validation with the structural-hash memo off. This is not a relaxed decoder and retains the full original error ordering.

Equations

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

def Miri.Input.decodeJsonReference (text : String) : Except String DecodeResult

Equations

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

def Miri.Input.decodeRuntimeJson (text : String) : Except String RuntimeDecodeResult

Runtime-only entry point, preserving validation and diagnostic precedence without retaining the full typed projection.

Equations

• Miri.Input.decodeRuntimeJson text = Miri.Input.decodeRuntimeJsonProfiled text ∅

def Miri.Input.decodeRuntimeFile (path : System.FilePath) : IO (Except String RuntimeDecodeResult)

Equations

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

def Miri.Input.decodeAllocationMemoryEvidence (j : Lean.Json) : Except String AllocationMemory

Typed metadata entrypoints for compiler-query adapters.

Equations

• Miri.Input.decodeAllocationMemoryEvidence j = Miri.Input.DecoderValues.parseAllocationMemory j "$allocation"