Optional structural-hash memo for already resolved transport graphs. The authoritative resolver still owns all input checks. Cached keys use the same Json equality and hash; collisions are never treated as equality. A raw noncanonical object, or an unexpected shape, disables this optimization.

structure Miri.Input.JsonTraversalCache.Key : Type

• value : Lean.Json
• digest : UInt64
• id : Option Nat

  Existing exporter node ID. Inline nodes are not independently memoized.

@[instance_reducible]

instance Miri.Input.JsonTraversalCache.instBEqKey : BEq Key

Equations

• Miri.Input.JsonTraversalCache.instBEqKey = { beq := fun (a b : Miri.Input.JsonTraversalCache.Key) => a.value == b.value }

@[instance_reducible]

instance Miri.Input.JsonTraversalCache.instHashableKey : Hashable Key

Equations

• Miri.Input.JsonTraversalCache.instHashableKey = { hash := fun (a : Miri.Input.JsonTraversalCache.Key) => a.digest }

theorem Miri.Input.JsonTraversalCache.Key.beq_eq (a b : Key) : (a == b) = (a.value == b.value)

inductive Miri.Input.JsonTraversalCache.Node : Type

• cached (key : Key) (children : Array Node) : Node
• uncached (value : Lean.Json) : Node

def Miri.Input.JsonTraversalCache.Node.value : Node → Lean.Json

Equations

• (Miri.Input.JsonTraversalCache.Node.cached key children).value = key.value
• (Miri.Input.JsonTraversalCache.Node.uncached value).value = value

def Miri.Input.JsonTraversalCache.Node.key : Node → Key

Equations

• (Miri.Input.JsonTraversalCache.Node.cached key children).key = key
• (Miri.Input.JsonTraversalCache.Node.uncached value).key = { value := value, digest := hash value, id := none }

inductive Miri.Input.JsonTraversalCache.IdentityKey : Type

Identity keys are confined to a single document traversal. Sharing is supplied by the exporter, never inferred from hashes.

• node (id : Nat) : IdentityKey
• raw (key : Key) : IdentityKey

@[instance_reducible]

instance Miri.Input.JsonTraversalCache.instBEqIdentityKey : BEq IdentityKey

Equations

• Miri.Input.JsonTraversalCache.instBEqIdentityKey = { beq := Miri.Input.JsonTraversalCache.instBEqIdentityKey.beq }

def Miri.Input.JsonTraversalCache.instBEqIdentityKey.beq : IdentityKey → IdentityKey → Bool

Equations

• Miri.Input.JsonTraversalCache.instBEqIdentityKey.beq (Miri.Input.JsonTraversalCache.IdentityKey.node a) (Miri.Input.JsonTraversalCache.IdentityKey.node b) = (a == b)
• Miri.Input.JsonTraversalCache.instBEqIdentityKey.beq (Miri.Input.JsonTraversalCache.IdentityKey.raw a) (Miri.Input.JsonTraversalCache.IdentityKey.raw b) = (a == b)
• Miri.Input.JsonTraversalCache.instBEqIdentityKey.beq x✝¹ x✝ = false

@[instance_reducible]

instance Miri.Input.JsonTraversalCache.instHashableIdentityKey : Hashable IdentityKey

Equations

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

def Miri.Input.JsonTraversalCache.Node.identity : Node → IdentityKey

Equations

• One or more equations did not get rendered due to their size.
• (Miri.Input.JsonTraversalCache.Node.uncached value).identity = Miri.Input.JsonTraversalCache.IdentityKey.raw { value := value, digest := hash value, id := none }

def Miri.Input.JsonTraversalCache.Node.shouldMemo : Node → Bool

Inline children are traversed under their shared parent, without creating unique memo entries that can never be hit. Raw fallback keeps structural reuse.

Equations

• (Miri.Input.JsonTraversalCache.Node.cached key children).shouldMemo = key.id.isSome
• (Miri.Input.JsonTraversalCache.Node.uncached value).shouldMemo = true

theorem Miri.Input.JsonTraversalCache.uncached_hash_eq (value : Lean.Json) : hash (Node.uncached value).key = hash value

def Miri.Input.JsonTraversalCache.Node.child (node : Node) (index : Nat) (fallback : Lean.Json) : Node

Child positions follow the actual array or object's inorder traversal. Only the internal builder supplies cached children; an absent child falls back to the real JSON value, preserving checks rather than treating it as visited.

Equations

• (Miri.Input.JsonTraversalCache.Node.cached key children).child index fallback = children[index]?.getD (Miri.Input.JsonTraversalCache.Node.uncached fallback)
• (Miri.Input.JsonTraversalCache.Node.uncached value).child index fallback = Miri.Input.JsonTraversalCache.Node.uncached fallback

def Miri.Input.JsonTraversalCache.Node.field (node : Node) (name : String) (fallback : Lean.Json) : Node

Equations

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

def Miri.Input.JsonTraversalCache.resolve (input : Lean.Json) (enabled : Bool := true) (profile : Lean.Options := ∅) : Except String (SharedPayloads.ResolvedGraph × Node)

Only this constructor path creates the optional cache from the same input and resolver result. Fallback preserves arbitrary manually constructed Raw JSON. The cache performs no readiness or semantic validation of its own.

Equations

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

partial def Miri.Input.JsonTraversalCache.Node.audit (node : Node) : Bool

Diagnostic consistency check; deliberately expensive, never used as a readiness shortcut. It checks every cached child independently.