Shared JSON payload graph transport. Nodes are resolved once in topological order, and resolved Json values are reused directly at every reference site.

structure Miri.Input.SharedPayloads.ResolvedGraph : Type

Resolved graph output. nodeResolutionCount is the number of catalog nodes processed by the one-pass topological resolver.

• nodes : Array Lean.Json
• root : Lean.Json
• nodeResolutionCount : Nat

@[instance_reducible]

instance Miri.Input.SharedPayloads.instInhabitedResolvedGraph : Inhabited ResolvedGraph

Equations

• Miri.Input.SharedPayloads.instInhabitedResolvedGraph = { default := Miri.Input.SharedPayloads.instInhabitedResolvedGraph.default }

def Miri.Input.SharedPayloads.resolveGraph (document : Lean.Json) : Except String ResolvedGraph

Resolve the mandatory v2 shared-payload graph and strip its transport field. Every node is resolved exactly once in array order; node references can only point to earlier entries, while document references can point anywhere.

Equations

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

def Miri.Input.SharedPayloads.resolveCatalog (document : Lean.Json) : Except String Lean.Json

Resolve a shared graph, returning only its business document for decoder callers that do not need the resolved node table.

Equations

• Miri.Input.SharedPayloads.resolveCatalog document = do let __do_lift ← Miri.Input.SharedPayloads.resolveGraph document pure __do_lift.root