Cortex.Wire.RunTrace

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. Snapshots
  5. Closed Step Alphabet
  6. Finite Traces
Imports
import Cortex.Pulse.Classify import Cortex.Wire.SelectRecovery

Overview

Closed admitted-middle run traces for the Wire/Pulse proof boundary.

Context

Cortex.Wire.PulseSafety proves that each admitted recovery, execution, rewrite, and selected-branch step preserves SafeWireRunState. This module packages those local preservation theorems into one closed finite-trace surface. The compiler, parser, executor bodies, materialization, and durable lineage decoding remain boundary witnesses: once those witnesses are supplied, only the constructors below are admitted as proof-side middle transitions.

Theorem Split

The page defines:

  • WirePulseSnapshot, the changing state carried by the admitted middle;
  • AdmittedWirePulseStep, the closed alphabet of admitted middle transitions;
  • AdmittedWirePulseTrace, finite composition of admitted steps;
  • trace preservation from either an already-safe snapshot or persisted recovery preconditions;
  • final non-stuck classification theorems.
namespace Cortex.Wireopen Cortex.Pulse

Snapshots

section RunTracevariable {executor config contract authority payload : Type}variable [DecidableEq contract]variable [DecidableEq (StagedExecutorNode executor config authority)]

WirePulseSnapshot is the mutable proof-side state of the admitted runtime middle.

The executor registry and initial budget are fixed for a run, so they remain parameters of the safety predicate rather than fields of each snapshot.

structure WirePulseSnapshot (executor config authority payload : Type) where

Remaining rewrite budget at this point in the run.

remainingBudget : RewriteBudget

Current Wire planning context.

context : PlanningContext (WireNode executor config authority)

Current materialized Pulse DAG.

G : DAG (WireNode executor config authority)

Current persisted Pulse graph state.

state : GraphState (WireNode executor config authority) payloadnamespace WirePulseSnapshot

The snapshot reached by applying Pulse recovery to the persisted graph state.

noncomputable def recovered (snapshot : WirePulseSnapshot executor config authority payload) : WirePulseSnapshot executor config authority payload := { remainingBudget := snapshot.remainingBudget context := snapshot.context G := snapshot.G state := recoveredState snapshot.G snapshot.state }end WirePulseSnapshot

SafeWirePulseSnapshot applies the existing safe-run envelope to a snapshot.

abbrev SafeWirePulseSnapshot (registry : ExecutorRegistry executor config contract authority) (initialBudget : RewriteBudget) (snapshot : WirePulseSnapshot executor config authority payload) : Prop := SafeWireRunState registry initialBudget snapshot.remainingBudget snapshot.context snapshot.G snapshot.statenamespace WirePulseSnapshot

Persisted recovery preconditions establish the first safe snapshot of a run.

theorem runStart_establishes_safeRunState {registry : ExecutorRegistry executor config contract authority} {initialBudget : RewriteBudget} (snapshot : WirePulseSnapshot executor config authority payload) (hSourceValid : SourcePlanningContextValid snapshot.context) (hBoundary : _root_.Cortex.Wire.registryBoundary registry snapshot.context.topology) (hBridge : WireTopologyDAGBridge snapshot.context.topology snapshot.G) (hBudget : snapshot.remainingBudget.le initialBudget) (hPersisted : persistedRecoveryPreconditions snapshot.G snapshot.state) : SafeWirePulseSnapshot registry initialBudget snapshot.recovered := executor:Typeconfig:Typecontract:Typeauthority:Typepayload:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetsnapshot:WirePulseSnapshot executor config authority payloadhSourceValid:SourcePlanningContextValid snapshot.contexthBoundary:registryBoundary registry snapshot.context.topologyhBridge:WireTopologyDAGBridge snapshot.context.topology snapshot.GhBudget:snapshot.remainingBudget.le initialBudgethPersisted:persistedRecoveryPreconditions snapshot.G snapshot.state⊢ SafeWirePulseSnapshot registry initialBudget snapshot.recovered All goals completed! 🐙end WirePulseSnapshot

Closed Step Alphabet

One admitted transition inside the Wire/Pulse proof boundary.

This is a closed proof-side alphabet. Any runtime action that cannot be represented by one of these constructors is outside the admitted middle until a new constructor and preservation theorem are added.

Each trace fixes one payload type. The CorePure-success constructor is therefore available only for traces whose payload is CorePure.Name → Option CorePure.Value; the other constructors are polymorphic in the trace payload.

inductive AdmittedWirePulseStep (registry : ExecutorRegistry executor config contract authority) (initialBudget : RewriteBudget) : (payload : Type) → WirePulseSnapshot executor config authority payload → WirePulseSnapshot executor config authority payload → Prop where | recovery {payload : Type} (snapshot : WirePulseSnapshot executor config authority payload) : AdmittedWirePulseStep registry initialBudget payload snapshot snapshot.recovered | frontierFacts {payload : Type} (snapshot : WirePulseSnapshot executor config authority payload) (results : List (NodeResult (WireNode executor config authority) payload)) (hResults : NodeResult.AllAdmissibleFold snapshot.G snapshot.state results) : AdmittedWirePulseStep registry initialBudget payload snapshot { remainingBudget := snapshot.remainingBudget context := snapshot.context G := snapshot.G state := recoveredState snapshot.G (NodeResult.applyNodeFacts results snapshot.state) }

Successful CorePure evaluation emits the proof-side CorePure payload shape.

| corePureSuccess {ctx : CorePure.StaticContext} {env : CorePure.Env} {pureNode : CorePure.PureNode} {lookup : CorePure.Name → Option CorePure.Value} {contracts : CorePure.OutputValueContracts} {node : WireNode executor config authority} (snapshot : WirePulseSnapshot executor config authority (CorePure.Name → Option CorePure.Value)) (hNode : CorePure.PureNodeAdmitted ctx pureNode) (hEval : pureNode.evalOutputs env = Except.ok lookup) (hContracts : ∀ outerEnv localEnv, CorePure.evalBindings env pureNode.bindings = Except.ok outerEnv → CorePure.evalWhereEnv outerEnv pureNode.whereExpr = Except.ok localEnv → CorePure.OutputExpressionsSatisfyContracts (CorePure.outputValueContractOk contracts) localEnv pureNode.outputs) (hAdmissible : NodeResult.Admissible snapshot.G snapshot.state { node := node outcome := NodeOutcome.succeeded lookup }) : AdmittedWirePulseStep registry initialBudget (CorePure.Name → Option CorePure.Value) snapshot { remainingBudget := snapshot.remainingBudget context := snapshot.context G := snapshot.G state := recoveredState snapshot.G (NodeResult.applyNodeFacts [ { node := node outcome := NodeOutcome.succeeded lookup } ] snapshot.state) } | constructedRewrite {payload : Type} (snapshot : WirePulseSnapshot executor config authority payload) {policy : RuntimeNamespacePolicy (WireNode executor config authority)} {rawRewrite : GraphRewrite (WireNode executor config authority)} {insertedDepth : Nat} {nextBudget : RewriteBudget} {nextG : DAG (WireNode executor config authority)} {nextState : GraphState (WireNode executor config authority) payload} (step : ConstructedPlanningStep policy (_root_.Cortex.Wire.registryBoundary registry) snapshot.context snapshot.remainingBudget rawRewrite insertedDepth nextBudget) (hDelta : RegistryBoundaryDeltaAdmitted registry step.delta) (hMaterialized : MaterializedPulseState step.nextContext nextG nextState) : AdmittedWirePulseStep registry initialBudget payload snapshot { remainingBudget := nextBudget context := step.nextContext G := nextG state := nextState } | selectActualize {payload : Type} (snapshot : WirePulseSnapshot executor config authority payload) {policy : RuntimeNamespacePolicy (WireNode executor config authority)} {arm : Type} {family : LatentBranchFamily (WireNode executor config authority) arm} {actualize : SelectActualize family} {insertedDepth : Nat} {nextBudget : RewriteBudget} {nextG : DAG (WireNode executor config authority)} {nextState : GraphState (WireNode executor config authority) payload} (step : ConstructedPlanningStep policy (_root_.Cortex.Wire.registryBoundary registry) snapshot.context snapshot.remainingBudget actualize.toGraphRewrite insertedDepth nextBudget) (hDelta : RegistryBoundaryDeltaAdmitted registry step.delta) (hMaterialized : MaterializedPulseState step.nextContext nextG nextState) : AdmittedWirePulseStep registry initialBudget payload snapshot { remainingBudget := nextBudget context := step.nextContext G := nextG state := nextState }

Selected-branch recovery requires durable provenance before the constructor is available.

Safety preservation itself uses the recovered record; the persisted admission and provenance are load-bearing for replay identity and determinism rather than for the safe-run projection.

| selectedBranchRecovery {payload : Type} (snapshot : WirePulseSnapshot executor config authority payload) {policy : RuntimeNamespacePolicy (WireNode executor config authority)} {arm : Type} {family : LatentBranchFamily (WireNode executor config authority) arm} {nextG : DAG (WireNode executor config authority)} {nextState : GraphState (WireNode executor config authority) payload} (persisted : PersistedSelectedBranchAdmission family policy (_root_.Cortex.Wire.registryBoundary registry) snapshot.context snapshot.remainingBudget) (record : SelectedBranchRecoveryRecord family policy (_root_.Cortex.Wire.registryBoundary registry) snapshot.context snapshot.remainingBudget) (hProvenance : SelectedBranchRecoveryRecord.Provenance persisted.toRecoveryRecord record) (hDelta : RegistryBoundaryDeltaAdmitted registry record.step.delta) (hMaterialized : MaterializedPulseState record.step.nextContext nextG nextState) : AdmittedWirePulseStep registry initialBudget payload snapshot { remainingBudget := record.remaining context := record.step.nextContext G := nextG state := nextState }namespace AdmittedWirePulseStep

Every admitted middle step preserves the Wire/Pulse safe-run envelope.

theorem preserves_safeRunState {registry : ExecutorRegistry executor config contract authority} {initialBudget : RewriteBudget} {payload : Type} {before after : WirePulseSnapshot executor config authority payload} (transition : AdmittedWirePulseStep registry initialBudget payload before after) (hSafe : SafeWirePulseSnapshot registry initialBudget before) : SafeWirePulseSnapshot registry initialBudget after := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typebefore:WirePulseSnapshot executor config authority payloadafter:WirePulseSnapshot executor config authority payloadtransition:AdmittedWirePulseStep registry initialBudget payload before afterhSafe:SafeWirePulseSnapshot registry initialBudget before⊢ SafeWirePulseSnapshot registry initialBudget after cases transition with executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typebefore:WirePulseSnapshot executor config authority payloadhSafe:SafeWirePulseSnapshot registry initialBudget before⊢ SafeWirePulseSnapshot registry initialBudget before.recovered All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typebefore:WirePulseSnapshot executor config authority payloadhSafe:SafeWirePulseSnapshot registry initialBudget beforeresults:List (NodeResult (WireNode executor config authority) payload)hResults:NodeResult.AllAdmissibleFold before.G before.state results⊢ SafeWirePulseSnapshot registry initialBudget { remainingBudget := before.remainingBudget, context := before.context, G := before.G, state := recoveredState before.G (NodeResult.applyNodeFacts results before.state) } All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetctx✝:CorePure.StaticContextenv✝:CorePure.EnvpureNode✝:CorePure.PureNodelookup✝:CorePure.Name → Option CorePure.Valuecontracts✝:CorePure.OutputValueContractsnode✝:WireNode executor config authoritysnapshot:WirePulseSnapshot executor config authority (CorePure.Name → Option CorePure.Value)hNode:CorePure.PureNodeAdmitted ctx✝ pureNode✝hEval:CorePure.PureNode.evalOutputs env✝ pureNode✝ = Except.ok lookup✝hContracts:∀ (outerEnv localEnv : CorePure.Env), CorePure.evalBindings env✝ pureNode✝.bindings = Except.ok outerEnv → CorePure.evalWhereEnv outerEnv pureNode✝.whereExpr = Except.ok localEnv → CorePure.OutputExpressionsSatisfyContracts (CorePure.outputValueContractOk contracts✝) localEnv pureNode✝.outputshAdmissible:NodeResult.Admissible snapshot.G snapshot.state { node := node✝, outcome := NodeOutcome.succeeded lookup✝ }hSafe:SafeWirePulseSnapshot registry initialBudget snapshot⊢ SafeWirePulseSnapshot registry initialBudget { remainingBudget := snapshot.remainingBudget, context := snapshot.context, G := snapshot.G, state := recoveredState snapshot.G (NodeResult.applyNodeFacts [{ node := node✝, outcome := NodeOutcome.succeeded lookup✝ }] snapshot.state) } All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typebefore:WirePulseSnapshot executor config authority payloadhSafe:SafeWirePulseSnapshot registry initialBudget beforepolicy✝:RuntimeNamespacePolicy (WireNode executor config authority)rawRewrite✝:GraphRewrite (WireNode executor config authority)insertedDepth✝:ℕnextBudget✝:RewriteBudgetnextG✝:DAG (WireNode executor config authority)nextState✝:GraphState (WireNode executor config authority) payloadstep:ConstructedPlanningStep policy✝ (registryBoundary registry) before.context before.remainingBudget rawRewrite✝ insertedDepth✝ nextBudget✝hDelta:RegistryBoundaryDeltaAdmitted registry step.deltahMaterialized:MaterializedPulseState step.nextContext nextG✝ nextState✝⊢ SafeWirePulseSnapshot registry initialBudget { remainingBudget := nextBudget✝, context := step.nextContext, G := nextG✝, state := nextState✝ } All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typebefore:WirePulseSnapshot executor config authority payloadhSafe:SafeWirePulseSnapshot registry initialBudget beforepolicy✝:RuntimeNamespacePolicy (WireNode executor config authority)arm✝:Typefamily✝:LatentBranchFamily (WireNode executor config authority) arm✝actualize✝:SelectActualize family✝insertedDepth✝:ℕnextBudget✝:RewriteBudgetnextG✝:DAG (WireNode executor config authority)nextState✝:GraphState (WireNode executor config authority) payloadstep:ConstructedPlanningStep policy✝ (registryBoundary registry) before.context before.remainingBudget actualize✝.toGraphRewrite insertedDepth✝ nextBudget✝hDelta:RegistryBoundaryDeltaAdmitted registry step.deltahMaterialized:MaterializedPulseState step.nextContext nextG✝ nextState✝⊢ SafeWirePulseSnapshot registry initialBudget { remainingBudget := nextBudget✝, context := step.nextContext, G := nextG✝, state := nextState✝ } All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typebefore:WirePulseSnapshot executor config authority payloadhSafe:SafeWirePulseSnapshot registry initialBudget beforepolicy✝:RuntimeNamespacePolicy (WireNode executor config authority)arm✝:Typefamily✝:LatentBranchFamily (WireNode executor config authority) arm✝nextG✝:DAG (WireNode executor config authority)nextState✝:GraphState (WireNode executor config authority) payloadpersisted:PersistedSelectedBranchAdmission family✝ policy✝ (registryBoundary registry) before.context before.remainingBudgetrecord:SelectedBranchRecoveryRecord family✝ policy✝ (registryBoundary registry) before.context before.remainingBudgethProvenance:persisted.toRecoveryRecord.Provenance recordhDelta:RegistryBoundaryDeltaAdmitted registry ⋯.deltahMaterialized:MaterializedPulseState ⋯.nextContext nextG✝ nextState✝⊢ SafeWirePulseSnapshot registry initialBudget { remainingBudget := record.remaining, context := ⋯.nextContext, G := nextG✝, state := nextState✝ } All goals completed! 🐙end AdmittedWirePulseStep

Finite Traces

Finite admitted run traces are reflexive-transitive closure with named constructors.

inductive AdmittedWirePulseTrace (registry : ExecutorRegistry executor config contract authority) (initialBudget : RewriteBudget) : (payload : Type) → WirePulseSnapshot executor config authority payload → WirePulseSnapshot executor config authority payload → Prop where | done {payload : Type} (snapshot : WirePulseSnapshot executor config authority payload) : AdmittedWirePulseTrace registry initialBudget payload snapshot snapshot | step {payload : Type} {first second third : WirePulseSnapshot executor config authority payload} (head : AdmittedWirePulseStep registry initialBudget payload first second) (tail : AdmittedWirePulseTrace registry initialBudget payload second third) : AdmittedWirePulseTrace registry initialBudget payload first thirdnamespace AdmittedWirePulseTrace

Every finite admitted middle trace preserves the Wire/Pulse safe-run envelope.

theorem preserves_safeRunState {registry : ExecutorRegistry executor config contract authority} {initialBudget : RewriteBudget} {payload : Type} {first last : WirePulseSnapshot executor config authority payload} (trace : AdmittedWirePulseTrace registry initialBudget payload first last) (hSafe : SafeWirePulseSnapshot registry initialBudget first) : SafeWirePulseSnapshot registry initialBudget last := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typefirst:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadtrace:AdmittedWirePulseTrace registry initialBudget payload first lasthSafe:SafeWirePulseSnapshot registry initialBudget first⊢ SafeWirePulseSnapshot registry initialBudget last induction trace with executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typefirst:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadsnapshot:WirePulseSnapshot executor config authority payloadhSafe:SafeWirePulseSnapshot registry initialBudget snapshot⊢ SafeWirePulseSnapshot registry initialBudget snapshot All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typefirst:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadfirst✝:WirePulseSnapshot executor config authority payloadsecond✝:WirePulseSnapshot executor config authority payloadthird✝:WirePulseSnapshot executor config authority payloadhead:AdmittedWirePulseStep registry initialBudget payload first✝ second✝tail:AdmittedWirePulseTrace registry initialBudget payload second✝ third✝ih:SafeWirePulseSnapshot registry initialBudget second✝ → SafeWirePulseSnapshot registry initialBudget third✝hSafe:SafeWirePulseSnapshot registry initialBudget first✝⊢ SafeWirePulseSnapshot registry initialBudget third✝ All goals completed! 🐙

A trace from the recovered run-start snapshot preserves the safe-run envelope.

theorem preserves_safeRunState_from_runStart {registry : ExecutorRegistry executor config contract authority} {initialBudget : RewriteBudget} {payload : Type} {start last : WirePulseSnapshot executor config authority payload} (trace : AdmittedWirePulseTrace registry initialBudget payload start.recovered last) (hSourceValid : SourcePlanningContextValid start.context) (hBoundary : _root_.Cortex.Wire.registryBoundary registry start.context.topology) (hBridge : WireTopologyDAGBridge start.context.topology start.G) (hBudget : start.remainingBudget.le initialBudget) (hPersisted : persistedRecoveryPreconditions start.G start.state) : SafeWirePulseSnapshot registry initialBudget last := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typestart:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadtrace:AdmittedWirePulseTrace registry initialBudget payload start.recovered lasthSourceValid:SourcePlanningContextValid start.contexthBoundary:registryBoundary registry start.context.topologyhBridge:WireTopologyDAGBridge start.context.topology start.GhBudget:start.remainingBudget.le initialBudgethPersisted:persistedRecoveryPreconditions start.G start.state⊢ SafeWirePulseSnapshot registry initialBudget last All goals completed! 🐙

A safe final snapshot reached by an admitted trace cannot classify as stuck.

theorem final_not_stuck {registry : ExecutorRegistry executor config contract authority} {initialBudget : RewriteBudget} {payload : Type} {first last : WirePulseSnapshot executor config authority payload} (trace : AdmittedWirePulseTrace registry initialBudget payload first last) (hSafe : SafeWirePulseSnapshot registry initialBudget first) (stuckState : GraphState (WireNode executor config authority) payload) : classifyGraphState last.G last.state ≠ StepResult.stuck stuckState := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typefirst:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadtrace:AdmittedWirePulseTrace registry initialBudget payload first lasthSafe:SafeWirePulseSnapshot registry initialBudget firststuckState:GraphState (WireNode executor config authority) payload⊢ classifyGraphState last.G last.state ≠ StepResult.stuck stuckState executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typefirst:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadtrace:AdmittedWirePulseTrace registry initialBudget payload first lasthSafe:SafeWirePulseSnapshot registry initialBudget firststuckState:GraphState (WireNode executor config authority) payloadhFinalSafe:SafeWirePulseSnapshot registry initialBudget last⊢ classifyGraphState last.G last.state ≠ StepResult.stuck stuckState All goals completed! 🐙

A run that starts from persisted recovery preconditions and follows an admitted trace cannot finish stuck.

theorem final_not_stuck_from_runStart {registry : ExecutorRegistry executor config contract authority} {initialBudget : RewriteBudget} {payload : Type} {start last : WirePulseSnapshot executor config authority payload} (trace : AdmittedWirePulseTrace registry initialBudget payload start.recovered last) (hSourceValid : SourcePlanningContextValid start.context) (hBoundary : _root_.Cortex.Wire.registryBoundary registry start.context.topology) (hBridge : WireTopologyDAGBridge start.context.topology start.G) (hBudget : start.remainingBudget.le initialBudget) (hPersisted : persistedRecoveryPreconditions start.G start.state) (stuckState : GraphState (WireNode executor config authority) payload) : classifyGraphState last.G last.state ≠ StepResult.stuck stuckState := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typestart:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadtrace:AdmittedWirePulseTrace registry initialBudget payload start.recovered lasthSourceValid:SourcePlanningContextValid start.contexthBoundary:registryBoundary registry start.context.topologyhBridge:WireTopologyDAGBridge start.context.topology start.GhBudget:start.remainingBudget.le initialBudgethPersisted:persistedRecoveryPreconditions start.G start.statestuckState:GraphState (WireNode executor config authority) payload⊢ classifyGraphState last.G last.state ≠ StepResult.stuck stuckState executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authorityinitialBudget:RewriteBudgetpayload:Typestart:WirePulseSnapshot executor config authority payloadlast:WirePulseSnapshot executor config authority payloadtrace:AdmittedWirePulseTrace registry initialBudget payload start.recovered lasthSourceValid:SourcePlanningContextValid start.contexthBoundary:registryBoundary registry start.context.topologyhBridge:WireTopologyDAGBridge start.context.topology start.GhBudget:start.remainingBudget.le initialBudgethPersisted:persistedRecoveryPreconditions start.G start.statestuckState:GraphState (WireNode executor config authority) payloadhStartSafe:SafeWirePulseSnapshot registry initialBudget start.recovered⊢ classifyGraphState last.G last.state ≠ StepResult.stuck stuckState All goals completed! 🐙end AdmittedWirePulseTraceend RunTraceend Cortex.Wire