Theory /Cortex /Pulse /Classify

Cortex.Pulse.Classify

proofs

On this page

Overview
Context
Theorem Split
Classification Surface
Classifier
Branch Equations
Well-Formed Classification

Imports

import Cortex.Pulse.Validity

Overview

Classification is the final pure phase of the fixed-topology Pulse kernel: accumulated facts are closed under failure propagation and then classified into a lifecycle decision. This module models the structural decision surface while keeping runtime diagnostics and payload details abstract.

Context

The Haskell runtime classifies by first applying propagateFailure, then checking for failed nodes, a nonempty executable frontier, completed settlement, suspension, and finally stuck diagnostics. Lean keeps that precedence for topology-valid states and states the theorem-level surface against wellFormedGraphState, where the stuck branch is impossible.

Theorem Split

The page defines classification predicates, the closed-state classifier, the closure-wrapping classifier, branch equations, and the well-formed-state exhaustiveness theorem.

namespace Cortex.Pulsevariable {ν : Type u} {payload : Type v}

Classification Surface

RunOutcome is the structural terminal outcome visible to the proof.

inductive RunOutcome : Type where
  | completed : RunOutcome
  | failed : RunOutcome
  deriving Repr, DecidableEq

StepResult is the pure classification result for a graph state.

The runtime StuckDiagnostic payload is intentionally erased: the Lean classification theorem only needs to prove that the stuck constructor is unreachable for well-formed structural states.

inductive StepResult (ν : Type u) (payload : Type v) :
    Type (max (u + 1) (v + 1)) where
  | progressing : GraphState ν payload → Finset ν → StepResult ν payload
  | settled : GraphState ν payload → RunOutcome → StepResult ν payload
  | suspended : GraphState ν payload → StepResult ν payload
  | stuck : GraphState ν payload → StepResult ν payload

pendingNodes G state is the topology-scoped pending-node set.

noncomputable def pendingNodes
    (G : DAG ν)
    (state : GraphState ν payload) : Finset ν := byν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ Finset ν
  classical
  exact G.nodes.filter fun node => state.status node = NodeStatus.pendingAll goals completed! 🐙

hasFailedNodes G state checks for a failed node in the topology.

def hasFailedNodes
    (G : DAG ν)
    (state : GraphState ν payload) : Prop :=
  ∃ node : ν, node ∈ G.nodes ∧ state.status node = NodeStatus.failed

allSettled G state says every topology node is terminal.

def allSettled
    (G : DAG ν)
    (state : GraphState ν payload) : Prop :=
  ∀ node : ν, node ∈ G.nodes → NodeStatus.terminal (state.status node)

hasWaitingNodes G state checks for topology-scoped waiting nodes.

Runtime correspondence for this predicate is intended under GraphState.topologyDomain, where off-topology statuses are normalized to pending.

def hasWaitingNodes
    (G : DAG ν)
    (state : GraphState ν payload) : Prop :=
  ∃ node : ν, node ∈ G.nodes ∧ state.status node = NodeStatus.waiting

hasAmbientWaitingNodes state models a raw status-map scan for waiting statuses.

def hasAmbientWaitingNodes
    (state : GraphState ν payload) : Prop :=
  ∃ node : ν, state.status node = NodeStatus.waiting

Topology-domain validity bridges topology-scoped and ambient waiting checks.

theorem hasWaitingNodes_iff_hasAmbientWaitingNodes_of_topologyDomain
    (G : DAG ν)
    (state : GraphState ν payload)
    (hDomain : GraphState.topologyDomain G state) :
    hasWaitingNodes G state ↔ hasAmbientWaitingNodes state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ hasWaitingNodes G state ↔ hasAmbientWaitingNodes state
  constructormpν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ hasWaitingNodes G state → hasAmbientWaitingNodes statemprν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ hasAmbientWaitingNodes state → hasWaitingNodes G state
  ·mpν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ hasWaitingNodes G state → hasAmbientWaitingNodes state intro hWaitingmpν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehWaiting:hasWaitingNodes G state⊢ hasAmbientWaitingNodes state
    rcases hWaiting with ⟨node, _hNode, hStatus⟩mpν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:ν_hNode:node ∈ G.nodeshStatus:state.status node = NodeStatus.waiting⊢ hasAmbientWaitingNodes state
    exact ⟨node, hStatus⟩All goals completed! 🐙
  ·mprν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ hasAmbientWaitingNodes state → hasWaitingNodes G state intro hWaitingmprν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statehWaiting:hasAmbientWaitingNodes state⊢ hasWaitingNodes G state
    rcases hWaiting with ⟨node, hStatus⟩mprν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:state.status node = NodeStatus.waiting⊢ hasWaitingNodes G state
    by_cases hNode : node ∈ G.nodesposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:state.status node = NodeStatus.waitinghNode:node ∈ G.nodes⊢ hasWaitingNodes G statenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:state.status node = NodeStatus.waitinghNode:node ∉ G.nodes⊢ hasWaitingNodes G state
    ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:state.status node = NodeStatus.waitinghNode:node ∈ G.nodes⊢ hasWaitingNodes G state exact ⟨node, hNode, hStatus⟩All goals completed! 🐙
    ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:state.status node = NodeStatus.waitinghNode:node ∉ G.nodes⊢ hasWaitingNodes G state have hPending : state.status node = NodeStatus.pending :=
        (hDomain node hNode).1negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:state.status node = NodeStatus.waitinghNode:node ∉ G.nodeshPending:state.status node = NodeStatus.pending⊢ hasWaitingNodes G state
      rw [hPending] at hStatusnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhStatus:NodeStatus.pending = NodeStatus.waitinghNode:node ∉ G.nodeshPending:state.status node = NodeStatus.pending⊢ hasWaitingNodes G state
      cases hStatusAll goals completed! 🐙

Classifier

classifyClosedGraphState G state classifies a topology-valid failure-closed state.

noncomputable def classifyClosedGraphState
    (G : DAG ν)
    (state : GraphState ν payload) : StepResult ν payload := byν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ StepResult ν payload
  classical
  exact
    if hasFailedNodes G state then
      StepResult.settled state RunOutcome.failed
    else if (directReadyNodes G state).Nonempty then
      StepResult.progressing state (directReadyNodes G state)
    else if allSettled G state then
      StepResult.settled state RunOutcome.completed
    else if hasWaitingNodes G state then
      StepResult.suspended state
    else
      StepResult.stuck stateAll goals completed! 🐙

classifyGraphState G state is the topology-scoped classifier after failure closure.

noncomputable def classifyGraphState
    (G : DAG ν)
    (state : GraphState ν payload) : StepResult ν payload :=
  classifyClosedGraphState G (propagateFailure G state)

Branch Equations

Failed nodes take classification precedence over all other branches.

theorem classifyClosedGraphState_failed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hFailed : hasFailedNodes G state) :
    classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhFailed:hasFailedNodes G state⊢ classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed
  classical
  simp [classifyClosedGraphState, hFailed]All goals completed! 🐙

A nonempty frontier progresses when no failed node is present.

theorem classifyClosedGraphState_progressing
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hFrontier : (directReadyNodes G state).Nonempty) :
    classifyClosedGraphState G state =
      StepResult.progressing state (directReadyNodes G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoFailed:¬hasFailedNodes G statehFrontier:(directReadyNodes G state).Nonempty⊢ classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state)
  classical
  simp [classifyClosedGraphState, hNoFailed, hFrontier]All goals completed! 🐙

Settled completion applies after failed and frontier branches are absent.

theorem classifyClosedGraphState_settled_completed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hNoFrontier : ¬ (directReadyNodes G state).Nonempty)
    (hSettled : allSettled G state) :
    classifyClosedGraphState G state =
      StepResult.settled state RunOutcome.completed := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoFailed:¬hasFailedNodes G statehNoFrontier:¬(directReadyNodes G state).NonemptyhSettled:allSettled G state⊢ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed
  classical
  simp [classifyClosedGraphState, hNoFailed, hNoFrontier, hSettled]All goals completed! 🐙

Suspension applies when no earlier branch fires and a topology node is waiting.

theorem classifyClosedGraphState_suspended
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hNoFrontier : ¬ (directReadyNodes G state).Nonempty)
    (hNotSettled : ¬ allSettled G state)
    (hWaiting : hasWaitingNodes G state) :
    classifyClosedGraphState G state = StepResult.suspended state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoFailed:¬hasFailedNodes G statehNoFrontier:¬(directReadyNodes G state).NonemptyhNotSettled:¬allSettled G statehWaiting:hasWaitingNodes G state⊢ classifyClosedGraphState G state = StepResult.suspended state
  classical
  simp [classifyClosedGraphState, hNoFailed, hNoFrontier, hNotSettled, hWaiting]All goals completed! 🐙

The stuck branch records the structural complement of the earlier branches.

theorem classifyClosedGraphState_stuck
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hNoFrontier : ¬ (directReadyNodes G state).Nonempty)
    (hNotSettled : ¬ allSettled G state)
    (hNoWaiting : ¬ hasWaitingNodes G state) :
    classifyClosedGraphState G state = StepResult.stuck state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoFailed:¬hasFailedNodes G statehNoFrontier:¬(directReadyNodes G state).NonemptyhNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ classifyClosedGraphState G state = StepResult.stuck state
  classical
  simp [classifyClosedGraphState, hNoFailed, hNoFrontier, hNotSettled, hNoWaiting]All goals completed! 🐙

Well-Formed Classification

ClassificationNormalized state is the minimal volatile-state bundle for classification.

The minimal-pending-node argument only needs running and interrupted statuses to be absent; topology, output, closure, and frontier-bridge facts enter later correspondence theorems.

structure ClassificationNormalized
    (state : GraphState ν payload) : Prop where

No node is still in the active runtime state.

noRunningNodes : GraphState.noRunningNodes state

No node still carries an interrupted runtime marker.

noInterruptedNodes : GraphState.noInterruptedNodes state

Well-formed graph states are classification-normalized.

theorem classificationNormalized_of_wellFormed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hWellFormed : wellFormedGraphState G state) :
    ClassificationNormalized state :=
  { noRunningNodes := hWellFormed.noRunningNodes
    noInterruptedNodes := hWellFormed.noInterruptedNodes }

Nonterminal topology nodes are pending under normalized, nonfailed, nonwaiting validity.

theorem status_eq_pending_of_not_terminal
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNormalized : ClassificationNormalized state)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hNoWaiting : ¬ hasWaitingNodes G state)
    {node : ν}
    (hNode : node ∈ G.nodes)
    (hNotTerminal : ¬ NodeStatus.terminal (state.status node)) :
    state.status node = NodeStatus.pending := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminal⊢ state.status node = NodeStatus.pending
  cases hStatus : state.status nodependingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.pending⊢ NodeStatus.pending = NodeStatus.pendingrunningν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.running⊢ NodeStatus.running = NodeStatus.pendingcompletedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.completed⊢ NodeStatus.completed = NodeStatus.pendingfailedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.failed⊢ NodeStatus.failed = NodeStatus.pendingskippedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.skipped⊢ NodeStatus.skipped = NodeStatus.pendinginterruptedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.interrupted⊢ NodeStatus.interrupted = NodeStatus.pendingwaitingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.waiting⊢ NodeStatus.waiting = NodeStatus.pendingrewrittenν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.rewritten⊢ NodeStatus.rewritten = NodeStatus.pending
  ·pendingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.pending⊢ NodeStatus.pending = NodeStatus.pending rflAll goals completed! 🐙
  ·runningν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.running⊢ NodeStatus.running = NodeStatus.pending exact False.elim (hNormalized.noRunningNodes node hStatus)All goals completed! 🐙
  ·completedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.completed⊢ NodeStatus.completed = NodeStatus.pending exact False.elim (hNotTerminal (byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.completed⊢ (state.status node).terminal simp [hStatus, NodeStatus.terminal]All goals completed! 🐙))
  ·failedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.failed⊢ NodeStatus.failed = NodeStatus.pending exact False.elim (hNoFailed ⟨node, hNode, hStatus⟩)All goals completed! 🐙
  ·skippedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.skipped⊢ NodeStatus.skipped = NodeStatus.pending exact False.elim (hNotTerminal (byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.skipped⊢ (state.status node).terminal simp [hStatus, NodeStatus.terminal]All goals completed! 🐙))
  ·interruptedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.interrupted⊢ NodeStatus.interrupted = NodeStatus.pending exact False.elim (hNormalized.noInterruptedNodes node hStatus)All goals completed! 🐙
  ·waitingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.waiting⊢ NodeStatus.waiting = NodeStatus.pending exact False.elim (hNoWaiting ⟨node, hNode, hStatus⟩)All goals completed! 🐙
  ·rewrittenν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.rewritten⊢ NodeStatus.rewritten = NodeStatus.pending exact False.elim (hNotTerminal (byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNoWaiting:¬hasWaitingNodes G statenode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminalhStatus:state.status node = NodeStatus.rewritten⊢ (state.status node).terminal simp [hStatus, NodeStatus.terminal]All goals completed! 🐙))

A normalized nonfailed, nonsettled, nonwaiting state has a proof frontier.

theorem readyNodes_nonempty_of_normalized
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNormalized : ClassificationNormalized state)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hNotSettled : ¬ allSettled G state)
    (hNoWaiting : ¬ hasWaitingNodes G state) :
    (readyNodes G state).Nonempty := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
  classical
  have hExistsNonterminal :
      ∃ node : ν, node ∈ G.nodes ∧ ¬ NodeStatus.terminal (state.status node) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
    by_contra hNoneν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G statehNone:¬∃ node ∈ G.nodes, ¬(state.status node).terminal⊢ False
    apply hNotSettledν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G statehNone:¬∃ node ∈ G.nodes, ¬(state.status node).terminal⊢ allSettled G state
    intro node hNodeν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G statehNone:¬∃ node ∈ G.nodes, ¬(state.status node).terminalnode:νhNode:node ∈ G.nodes⊢ (state.status node).terminal
    by_contra hNotTerminalν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G statehNone:¬∃ node ∈ G.nodes, ¬(state.status node).terminalnode:νhNode:node ∈ G.nodeshNotTerminal:¬(state.status node).terminal⊢ False
    exact hNone ⟨node, hNode, hNotTerminal⟩All goals completed! 🐙
  rcases hExistsNonterminal with ⟨seed, hSeedMem, hSeedNotTerminal⟩ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminal⊢ (readyNodes G state).Nonempty
  have hSeedPending : state.status seed = NodeStatus.pending :=
    status_eq_pending_of_not_terminal
      G
      state
      hNormalized
      hNoFailed
      hNoWaiting
      hSeedMem
      hSeedNotTerminalν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pending⊢ (readyNodes G state).Nonempty
  have hPendingNonempty : (pendingNodes G state).Nonempty := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
    exact ⟨seed, byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pending⊢ seed ∈ pendingNodes G state simp [pendingNodes, hSeedMem, hSeedPending]All goals completed! 🐙⟩
  rcases G.exists_reaches_minimal (pendingNodes G state) hPendingNonempty with
    ⟨node, hNodePending, hMinimal⟩ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor node⊢ (readyNodes G state).Nonempty
  have hPendingInfo :
      node ∈ G.nodes ∧ state.status node = NodeStatus.pending := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
    simpa [pendingNodes] using hNodePendingAll goals completed! 🐙
  have hReady : Ready G state node := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
    constructorleftν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ node ∈ G.nodesrightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ state.status node = NodeStatus.pending ∧
  ∀ (predecessor : ν), G.reaches predecessor node → (state.status predecessor).terminal
    ·leftν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ node ∈ G.nodes exact hPendingInfo.1All goals completed! 🐙
    constructorright.leftν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ state.status node = NodeStatus.pendingright.rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ ∀ (predecessor : ν), G.reaches predecessor node → (state.status predecessor).terminal
    ·right.leftν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ state.status node = NodeStatus.pending exact hPendingInfo.2All goals completed! 🐙
    ·right.rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pending⊢ ∀ (predecessor : ν), G.reaches predecessor node → (state.status predecessor).terminal intro predecessor hReachright.rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pendingpredecessor:νhReach:G.reaches predecessor node⊢ (state.status predecessor).terminal
      by_contra hPredecessorNotTerminalright.rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pendingpredecessor:νhReach:G.reaches predecessor nodehPredecessorNotTerminal:¬(state.status predecessor).terminal⊢ False
      have hPredecessorMem : predecessor ∈ G.nodes :=
        G.reaches_source_mem hReachright.rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pendingpredecessor:νhReach:G.reaches predecessor nodehPredecessorNotTerminal:¬(state.status predecessor).terminalhPredecessorMem:predecessor ∈ G.nodes⊢ False
      have hPredecessorPendingStatus :
          state.status predecessor = NodeStatus.pending :=
        status_eq_pending_of_not_terminal
          G
          state
          hNormalized
          hNoFailed
          hNoWaiting
          hPredecessorMem
          hPredecessorNotTerminalright.rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G stateseed:νhSeedMem:seed ∈ G.nodeshSeedNotTerminal:¬(state.status seed).terminalhSeedPending:state.status seed = NodeStatus.pendinghPendingNonempty:(pendingNodes G state).Nonemptynode:νhNodePending:node ∈ pendingNodes G statehMinimal:∀ predecessor ∈ pendingNodes G state, ¬G.reaches predecessor nodehPendingInfo:node ∈ G.nodes ∧ state.status node = NodeStatus.pendingpredecessor:νhReach:G.reaches predecessor nodehPredecessorNotTerminal:¬(state.status predecessor).terminalhPredecessorMem:predecessor ∈ G.nodeshPredecessorPendingStatus:state.status predecessor = NodeStatus.pending⊢ False
      have hPredecessorPending : predecessor ∈ pendingNodes G state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNormalized:ClassificationNormalized statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
        simp [pendingNodes, hPredecessorMem, hPredecessorPendingStatus]All goals completed! 🐙
      exact hMinimal predecessor hPredecessorPending hReachAll goals completed! 🐙
  exact ⟨node, (mem_readyNodes G state node).mpr ⟨hPendingInfo.1, hReady⟩⟩All goals completed! 🐙

A well-formed nonfailed, nonsettled, nonwaiting state has a runtime frontier.

theorem directReadyNodes_nonempty_of_wellFormed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hWellFormed : wellFormedGraphState G state)
    (hNoFailed : ¬ hasFailedNodes G state)
    (hNotSettled : ¬ allSettled G state)
    (hNoWaiting : ¬ hasWaitingNodes G state) :
    (directReadyNodes G state).Nonempty := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (directReadyNodes G state).Nonempty
  rw [← hWellFormed.frontierBridge]ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehNoFailed:¬hasFailedNodes G statehNotSettled:¬allSettled G statehNoWaiting:¬hasWaitingNodes G state⊢ (readyNodes G state).Nonempty
  exact
    readyNodes_nonempty_of_normalized
      G
      state
      (classificationNormalized_of_wellFormed G state hWellFormed)
      hNoFailed
      hNotSettled
      hNoWaitingAll goals completed! 🐙

Well-formed closed states classify into one of the non-stuck branches.

theorem classifyClosedGraphState_exhaustive_of_wellFormed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hWellFormed : wellFormedGraphState G state) :
    (hasFailedNodes G state ∧
        classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed) ∨
      (¬ hasFailedNodes G state ∧
        (directReadyNodes G state).Nonempty ∧
          classifyClosedGraphState G state =
            StepResult.progressing state (directReadyNodes G state)) ∨
        (¬ hasFailedNodes G state ∧
          ¬ (directReadyNodes G state).Nonempty ∧
            allSettled G state ∧
              classifyClosedGraphState G state =
                StepResult.settled state RunOutcome.completed) ∨
          (¬ hasFailedNodes G state ∧
            ¬ (directReadyNodes G state).Nonempty ∧
              ¬ allSettled G state ∧
                hasWaitingNodes G state ∧
                  classifyClosedGraphState G state = StepResult.suspended state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G state⊢ hasFailedNodes G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed ∨
  ¬hasFailedNodes G state ∧
      (directReadyNodes G state).Nonempty ∧
        classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
    ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
      ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
  classical
  by_cases hFailed : hasFailedNodes G stateposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:hasFailedNodes G state⊢ hasFailedNodes G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed ∨
  ¬hasFailedNodes G state ∧
      (directReadyNodes G state).Nonempty ∧
        classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
    ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
      ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended statenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G state⊢ hasFailedNodes G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed ∨
  ¬hasFailedNodes G state ∧
      (directReadyNodes G state).Nonempty ∧
        classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
    ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
      ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:hasFailedNodes G state⊢ hasFailedNodes G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed ∨
  ¬hasFailedNodes G state ∧
      (directReadyNodes G state).Nonempty ∧
        classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
    ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
      ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state exact Or.inl ⟨hFailed, classifyClosedGraphState_failed G state hFailed⟩All goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G state⊢ hasFailedNodes G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.failed ∨
  ¬hasFailedNodes G state ∧
      (directReadyNodes G state).Nonempty ∧
        classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
    ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
      ¬hasFailedNodes G state ∧
        ¬(directReadyNodes G state).Nonempty ∧
          ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state rightneg.hν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G state⊢ ¬hasFailedNodes G state ∧
    (directReadyNodes G state).Nonempty ∧
      classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
  ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
    ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
    by_cases hFrontier : (directReadyNodes G state).Nonemptyposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:(directReadyNodes G state).Nonempty⊢ ¬hasFailedNodes G state ∧
    (directReadyNodes G state).Nonempty ∧
      classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
  ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
    ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended statenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).Nonempty⊢ ¬hasFailedNodes G state ∧
    (directReadyNodes G state).Nonempty ∧
      classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
  ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
    ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
    ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:(directReadyNodes G state).Nonempty⊢ ¬hasFailedNodes G state ∧
    (directReadyNodes G state).Nonempty ∧
      classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
  ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
    ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state exact Or.inl
        ⟨hFailed, hFrontier, classifyClosedGraphState_progressing G state hFailed hFrontier⟩All goals completed! 🐙
    ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).Nonempty⊢ ¬hasFailedNodes G state ∧
    (directReadyNodes G state).Nonempty ∧
      classifyClosedGraphState G state = StepResult.progressing state (directReadyNodes G state) ∨
  ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
    ¬hasFailedNodes G state ∧
      ¬(directReadyNodes G state).Nonempty ∧
        ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state rightneg.hν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).Nonempty⊢ ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
  ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
      by_cases hSettled : allSettled G stateposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:allSettled G state⊢ ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
  ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended statenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G state⊢ ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
  ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
      ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:allSettled G state⊢ ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
  ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state exact Or.inl
          ⟨ hFailed
          , hFrontier
          , hSettled
          , classifyClosedGraphState_settled_completed G state hFailed hFrontier hSettled
          ⟩All goals completed! 🐙
      ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G state⊢ ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      allSettled G state ∧ classifyClosedGraphState G state = StepResult.settled state RunOutcome.completed ∨
  ¬hasFailedNodes G state ∧
    ¬(directReadyNodes G state).Nonempty ∧
      ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state rightneg.hν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G state⊢ ¬hasFailedNodes G state ∧
  ¬(directReadyNodes G state).Nonempty ∧
    ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
        by_cases hWaiting : hasWaitingNodes G stateposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:hasWaitingNodes G state⊢ ¬hasFailedNodes G state ∧
  ¬(directReadyNodes G state).Nonempty ∧
    ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended statenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:¬hasWaitingNodes G state⊢ ¬hasFailedNodes G state ∧
  ¬(directReadyNodes G state).Nonempty ∧
    ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
        ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:hasWaitingNodes G state⊢ ¬hasFailedNodes G state ∧
  ¬(directReadyNodes G state).Nonempty ∧
    ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state exact
            ⟨ hFailed
            , hFrontier
            , hSettled
            , hWaiting
            , classifyClosedGraphState_suspended G state hFailed hFrontier hSettled hWaiting
            ⟩All goals completed! 🐙
        ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:¬hasWaitingNodes G state⊢ ¬hasFailedNodes G state ∧
  ¬(directReadyNodes G state).Nonempty ∧
    ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state have hFrontierNonempty :
              (directReadyNodes G state).Nonempty :=
            directReadyNodes_nonempty_of_wellFormed
              G
              state
              hWellFormed
              hFailed
              hSettled
              hWaitingnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statehFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:¬hasWaitingNodes G statehFrontierNonempty:(directReadyNodes G state).Nonempty⊢ ¬hasFailedNodes G state ∧
  ¬(directReadyNodes G state).Nonempty ∧
    ¬allSettled G state ∧ hasWaitingNodes G state ∧ classifyClosedGraphState G state = StepResult.suspended state
          exact False.elim (hFrontier hFrontierNonempty)All goals completed! 🐙

Well-formed closed states cannot classify as stuck.

theorem classifyClosedGraphState_not_stuck_of_wellFormed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hWellFormed : wellFormedGraphState G state)
    (stuckState : GraphState ν payload) :
    classifyClosedGraphState G state ≠ StepResult.stuck stuckState := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payload⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
  classical
  by_cases hFailed : hasFailedNodes G stateposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:hasFailedNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckStatenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:hasFailedNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState intro hClassposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:hasFailedNodes G statehClass:classifyClosedGraphState G state = StepResult.stuck stuckState⊢ False
    simp [classifyClosedGraphState, hFailed] at hClassAll goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState by_cases hFrontier : (directReadyNodes G state).Nonemptyposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:(directReadyNodes G state).Nonempty⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckStatenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).Nonempty⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
    ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:(directReadyNodes G state).Nonempty⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState intro hClassposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:(directReadyNodes G state).NonemptyhClass:classifyClosedGraphState G state = StepResult.stuck stuckState⊢ False
      simp [classifyClosedGraphState, hFailed, hFrontier] at hClassAll goals completed! 🐙
    ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).Nonempty⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState by_cases hSettled : allSettled G stateposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:allSettled G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckStatenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
      ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:allSettled G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState intro hClassposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:allSettled G statehClass:classifyClosedGraphState G state = StepResult.stuck stuckState⊢ False
        simp [classifyClosedGraphState, hFailed, hFrontier, hSettled] at hClassAll goals completed! 🐙
      ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState by_cases hWaiting : hasWaitingNodes G stateposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:hasWaitingNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckStatenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:¬hasWaitingNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
        ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:hasWaitingNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState intro hClassposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:hasWaitingNodes G statehClass:classifyClosedGraphState G state = StepResult.stuck stuckState⊢ False
          simp
            [ classifyClosedGraphState
            , hFailed
            , hFrontier
            , hSettled
            , hWaiting
            ] at hClassAll goals completed! 🐙
        ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:¬hasWaitingNodes G state⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState have hFrontierNonempty :
              (directReadyNodes G state).Nonempty :=
            directReadyNodes_nonempty_of_wellFormed
              G
              state
              hWellFormed
              hFailed
              hSettled
              hWaitingnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payloadhFailed:¬hasFailedNodes G statehFrontier:¬(directReadyNodes G state).NonemptyhSettled:¬allSettled G statehWaiting:¬hasWaitingNodes G statehFrontierNonempty:(directReadyNodes G state).Nonempty⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
          exact False.elim (hFrontier hFrontierNonempty)All goals completed! 🐙

On well-formed states, runtime-style classification is already closed-state classification.

theorem classifyGraphState_eq_closed_of_wellFormed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hWellFormed : wellFormedGraphState G state) :
    classifyGraphState G state = classifyClosedGraphState G state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G state⊢ classifyGraphState G state = classifyClosedGraphState G state
  unfold classifyGraphStateν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G state⊢ classifyClosedGraphState G (propagateFailure G state) = classifyClosedGraphState G state
  rw [propagateFailure_of_failureClosureComplete G state hWellFormed.failureClosureComplete]All goals completed! 🐙

Well-formed graph states cannot classify as stuck after the runtime closure step.

theorem classifyGraphState_not_stuck_of_wellFormed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hWellFormed : wellFormedGraphState G state)
    (stuckState : GraphState ν payload) :
    classifyGraphState G state ≠ StepResult.stuck stuckState := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payload⊢ classifyGraphState G state ≠ StepResult.stuck stuckState
  rw [classifyGraphState_eq_closed_of_wellFormed G state hWellFormed]ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhWellFormed:wellFormedGraphState G statestuckState:GraphState ν payload⊢ classifyClosedGraphState G state ≠ StepResult.stuck stuckState
  exact classifyClosedGraphState_not_stuck_of_wellFormed G state hWellFormed stuckStateAll goals completed! 🐙

end Cortex.Pulse

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Graph.Safety Next →Cortex.Pulse.Closure