Theory /Cortex /Pulse /State

Cortex.Pulse.State

proofs

On this page

Overview
Context
Theorem Split
Node Status Lattice
Extensional Graph State
Failure-Growth Order
Recovery Normalization
Normalization Theorem

Imports

import Cortex.Pulse.DAG

Overview

This module defines the extensional state used by the fixed-topology Pulse kernel. Runtime payloads, failure details, and signal contents stay abstract; the proofs only inspect lifecycle status and whether a node has an output.

Context

The Haskell runtime stores maps keyed by durable node identifiers. The Lean model uses total functions over the finite topology instead, so the proofs can focus on lifecycle invariants rather than map bookkeeping.

Theorem Split

The page introduces the status lattice, the extensional graph state, the topology-domain invariant, and the recovery normalization lemma that removes volatile running marks.

namespace Cortex.Pulse

Node Status Lattice

NodeStatus is the lifecycle status for a node in the fixed-topology kernel.

The constructors mirror the runtime states in Cortex.Pulse.GraphRuntime while erasing payload details that are irrelevant to structural safety.

inductive NodeStatus : Type where
  | pending : NodeStatus
  | running : NodeStatus
  | completed : NodeStatus
  | failed : NodeStatus
  | skipped : NodeStatus
  | interrupted : NodeStatus
  | waiting : NodeStatus
  | rewritten : NodeStatus
  deriving Repr, DecidableEq

namespace NodeStatus

NodeStatus.terminal status means the status cannot make another local transition.

def terminal : NodeStatus → Prop
  | completed => True
  | failed => True
  | skipped => True
  | rewritten => True
  | pending => False
  | running => False
  | interrupted => False
  | waiting => False

NodeStatus.propagatable status means failure closure may overwrite it with failed.

def propagatable : NodeStatus → Prop
  | pending => True
  | waiting => True
  | completed => False
  | failed => False
  | skipped => False
  | running => False
  | interrupted => False
  | rewritten => False

NodeStatus.mayHaveOutput status means the status owns a durable payload.

def mayHaveOutput : NodeStatus → Prop
  | completed => True
  | failed => False
  | skipped => False
  | rewritten => True
  | pending => False
  | running => False
  | interrupted => False
  | waiting => False

NodeStatus.requiresOutput status means the status must carry a durable payload.

def requiresOutput : NodeStatus → Prop
  | completed => True
  | rewritten => True
  | failed => False
  | skipped => False
  | pending => False
  | running => False
  | interrupted => False
  | waiting => False

NodeStatus.unblocksSuccessors status means direct successors may run past it.

def unblocksSuccessors : NodeStatus → Prop
  | completed => True
  | skipped => True
  | rewritten => True
  | failed => False
  | pending => False
  | running => False
  | interrupted => False
  | waiting => False

failureLe before after orders states by failure-propagation growth.

A status can stay unchanged, or a still-propagatable status can become failed. This is the order used for monotonicity of failure closure.

def failureLe : NodeStatus → NodeStatus → Prop
  | before, after => before = after ∨ (propagatable before ∧ after = failed)

unblocks_terminal says successor-unblocking statuses are terminal.

theorem unblocks_terminal {status : NodeStatus}
    (hUnblocks : unblocksSuccessors status) :
    terminal status := bystatus:NodeStatushUnblocks:status.unblocksSuccessors⊢ status.terminal
  cases statuspendinghUnblocks:pending.unblocksSuccessors⊢ pending.terminalrunninghUnblocks:running.unblocksSuccessors⊢ running.terminalcompletedhUnblocks:completed.unblocksSuccessors⊢ completed.terminalfailedhUnblocks:failed.unblocksSuccessors⊢ failed.terminalskippedhUnblocks:skipped.unblocksSuccessors⊢ skipped.terminalinterruptedhUnblocks:interrupted.unblocksSuccessors⊢ interrupted.terminalwaitinghUnblocks:waiting.unblocksSuccessors⊢ waiting.terminalrewrittenhUnblocks:rewritten.unblocksSuccessors⊢ rewritten.terminal <;>pendinghUnblocks:pending.unblocksSuccessors⊢ pending.terminalrunninghUnblocks:running.unblocksSuccessors⊢ running.terminalcompletedhUnblocks:completed.unblocksSuccessors⊢ completed.terminalfailedhUnblocks:failed.unblocksSuccessors⊢ failed.terminalskippedhUnblocks:skipped.unblocksSuccessors⊢ skipped.terminalinterruptedhUnblocks:interrupted.unblocksSuccessors⊢ interrupted.terminalwaitinghUnblocks:waiting.unblocksSuccessors⊢ waiting.terminalrewrittenhUnblocks:rewritten.unblocksSuccessors⊢ rewritten.terminal simp [unblocksSuccessors, terminal] at hUnblocks ⊢All goals completed! 🐙

terminal_unblocks_of_not_failed recovers runtime-unblocking terminal statuses.

theorem terminal_unblocks_of_not_failed {status : NodeStatus}
    (hTerminal : terminal status)
    (hNotFailed : status ≠ failed) :
    unblocksSuccessors status := bystatus:NodeStatushTerminal:status.terminalhNotFailed:status ≠ failed⊢ status.unblocksSuccessors
  cases statuspendinghTerminal:pending.terminalhNotFailed:pending ≠ failed⊢ pending.unblocksSuccessorsrunninghTerminal:running.terminalhNotFailed:running ≠ failed⊢ running.unblocksSuccessorscompletedhTerminal:completed.terminalhNotFailed:completed ≠ failed⊢ completed.unblocksSuccessorsfailedhTerminal:failed.terminalhNotFailed:failed ≠ failed⊢ failed.unblocksSuccessorsskippedhTerminal:skipped.terminalhNotFailed:skipped ≠ failed⊢ skipped.unblocksSuccessorsinterruptedhTerminal:interrupted.terminalhNotFailed:interrupted ≠ failed⊢ interrupted.unblocksSuccessorswaitinghTerminal:waiting.terminalhNotFailed:waiting ≠ failed⊢ waiting.unblocksSuccessorsrewrittenhTerminal:rewritten.terminalhNotFailed:rewritten ≠ failed⊢ rewritten.unblocksSuccessors <;>pendinghTerminal:pending.terminalhNotFailed:pending ≠ failed⊢ pending.unblocksSuccessorsrunninghTerminal:running.terminalhNotFailed:running ≠ failed⊢ running.unblocksSuccessorscompletedhTerminal:completed.terminalhNotFailed:completed ≠ failed⊢ completed.unblocksSuccessorsfailedhTerminal:failed.terminalhNotFailed:failed ≠ failed⊢ failed.unblocksSuccessorsskippedhTerminal:skipped.terminalhNotFailed:skipped ≠ failed⊢ skipped.unblocksSuccessorsinterruptedhTerminal:interrupted.terminalhNotFailed:interrupted ≠ failed⊢ interrupted.unblocksSuccessorswaitinghTerminal:waiting.terminalhNotFailed:waiting ≠ failed⊢ waiting.unblocksSuccessorsrewrittenhTerminal:rewritten.terminalhNotFailed:rewritten ≠ failed⊢ rewritten.unblocksSuccessors simp [terminal, unblocksSuccessors] at hTerminal hNotFailed ⊢All goals completed! 🐙

pending_not_terminal states that a pending node is not terminal.

theorem pending_not_terminal :
    ¬ terminal pending := by⊢ ¬pending.terminal
  intro hTerminalhTerminal:pending.terminal⊢ False
  exact hTerminalAll goals completed! 🐙

failed_not_propagatable states that a failed node is not propagatable.

theorem failed_not_propagatable :
    ¬ propagatable failed := by⊢ ¬failed.propagatable
  intro hPropagatablehPropagatable:failed.propagatable⊢ False
  exact hPropagatableAll goals completed! 🐙

failureLe_refl says status failure-growth is reflexive.

theorem failureLe_refl (status : NodeStatus) :
    failureLe status status :=
  Or.inl rfl

failureLe_to_failed turns a propagatable status into a failure-growth step.

theorem failureLe_to_failed {status : NodeStatus}
    (hPropagatable : propagatable status) :
    failureLe status failed :=
  Or.inr ⟨hPropagatable, rfl⟩

failed_of_failureLe_failed says failed statuses cannot grow to another status.

theorem failed_of_failureLe_failed {after : NodeStatus}
    (hLe : failureLe failed after) :
    after = failed := byafter:NodeStatushLe:failed.failureLe after⊢ after = failed
  rcases hLe with hSame | hFailureinlafter:NodeStatushSame:failed = after⊢ after = failedinrafter:NodeStatushFailure:failed.propagatable ∧ after = failed⊢ after = failed
  ·inlafter:NodeStatushSame:failed = after⊢ after = failed exact hSame.symmAll goals completed! 🐙
  ·inrafter:NodeStatushFailure:failed.propagatable ∧ after = failed⊢ after = failed exact False.elim (failed_not_propagatable hFailure.1)All goals completed! 🐙

failureLe_preserves_failed says failure-growth preserves existing failures.

theorem failureLe_preserves_failed {before after : NodeStatus}
    (hLe : failureLe before after)
    (hFailed : before = failed) :
    after = failed := bybefore:NodeStatusafter:NodeStatushLe:before.failureLe afterhFailed:before = failed⊢ after = failed
  subst beforeafter:NodeStatushLe:failed.failureLe after⊢ after = failed
  exact failed_of_failureLe_failed hLeAll goals completed! 🐙

failureLe_reflects_propagatable pulls propagatability back through failure-growth.

theorem failureLe_reflects_propagatable {before after : NodeStatus}
    (hLe : failureLe before after)
    (hPropagatable : propagatable after) :
    propagatable before := bybefore:NodeStatusafter:NodeStatushLe:before.failureLe afterhPropagatable:after.propagatable⊢ before.propagatable
  rcases hLe with hSame | hFailureinlbefore:NodeStatusafter:NodeStatushPropagatable:after.propagatablehSame:before = after⊢ before.propagatableinrbefore:NodeStatusafter:NodeStatushPropagatable:after.propagatablehFailure:before.propagatable ∧ after = failed⊢ before.propagatable
  ·inlbefore:NodeStatusafter:NodeStatushPropagatable:after.propagatablehSame:before = after⊢ before.propagatable cases hSameinl.reflbefore:NodeStatushPropagatable:before.propagatable⊢ before.propagatable
    exact hPropagatableAll goals completed! 🐙
  ·inrbefore:NodeStatusafter:NodeStatushPropagatable:after.propagatablehFailure:before.propagatable ∧ after = failed⊢ before.propagatable exact hFailure.1All goals completed! 🐙

failureLe_trans says status failure-growth is transitive.

theorem failureLe_trans {left middle right : NodeStatus}
    (hLeft : failureLe left middle)
    (hRight : failureLe middle right) :
    failureLe left right := byleft:NodeStatusmiddle:NodeStatusright:NodeStatushLeft:left.failureLe middlehRight:middle.failureLe right⊢ left.failureLe right
  rcases hLeft with hSame | hFailureinlleft:NodeStatusmiddle:NodeStatusright:NodeStatushRight:middle.failureLe righthSame:left = middle⊢ left.failureLe rightinrleft:NodeStatusmiddle:NodeStatusright:NodeStatushRight:middle.failureLe righthFailure:left.propagatable ∧ middle = failed⊢ left.failureLe right
  ·inlleft:NodeStatusmiddle:NodeStatusright:NodeStatushRight:middle.failureLe righthSame:left = middle⊢ left.failureLe right cases hSameinl.reflleft:NodeStatusright:NodeStatushRight:left.failureLe right⊢ left.failureLe right
    exact hRightAll goals completed! 🐙
  ·inrleft:NodeStatusmiddle:NodeStatusright:NodeStatushRight:middle.failureLe righthFailure:left.propagatable ∧ middle = failed⊢ left.failureLe right rcases hFailure with ⟨hPropagatable, hMiddleFailed⟩inrleft:NodeStatusmiddle:NodeStatusright:NodeStatushRight:middle.failureLe righthPropagatable:left.propagatablehMiddleFailed:middle = failed⊢ left.failureLe right
    cases hMiddleFailedinr.reflleft:NodeStatusright:NodeStatushPropagatable:left.propagatablehRight:failed.failureLe right⊢ left.failureLe right
    have hRightFailed : right = failed :=
      failed_of_failureLe_failed hRightinr.reflleft:NodeStatusright:NodeStatushPropagatable:left.propagatablehRight:failed.failureLe righthRightFailed:right = failed⊢ left.failureLe right
    cases hRightFailedinr.refl.reflleft:NodeStatushPropagatable:left.propagatablehRight:failed.failureLe failed⊢ left.failureLe failed
    exact failureLe_to_failed hPropagatableAll goals completed! 🐙

end NodeStatus

Extensional Graph State

GraphState ν payload is node statuses plus optional node outputs.

structure GraphState (ν : Type u) (payload : Type v) where

status node is the current lifecycle status for a node.

status : ν → NodeStatus

output node is the optional node output. Payload contents remain abstract.

output : ν → Option payloadnamespace GraphStatevariable {ν : Type u} {payload : Type v}

@[ext]
theorem ext {s t : GraphState ν payload}
    (hStatus : ∀ n : ν, s.status n = t.status n)
    (hOutput : ∀ n : ν, s.output n = t.output n) :
    s = t := byν:Type upayload:Type vs:GraphState ν payloadt:GraphState ν payloadhStatus:∀ (n : ν), s.status n = t.status nhOutput:∀ (n : ν), s.output n = t.output n⊢ s = t
  cases s with
  | mk sStatus sOutput =>mkν:Type upayload:Type vt:GraphState ν payloadsStatus:ν → NodeStatussOutput:ν → Option payloadhStatus:∀ (n : ν), { status := sStatus, output := sOutput }.status n = t.status nhOutput:∀ (n : ν), { status := sStatus, output := sOutput }.output n = t.output n⊢ { status := sStatus, output := sOutput } = t
      cases t with
      | mk tStatus tOutput =>mk.mkν:Type upayload:Type vsStatus:ν → NodeStatussOutput:ν → Option payloadtStatus:ν → NodeStatustOutput:ν → Option payloadhStatus:∀ (n : ν), { status := sStatus, output := sOutput }.status n = { status := tStatus, output := tOutput }.status nhOutput:∀ (n : ν), { status := sStatus, output := sOutput }.output n = { status := tStatus, output := tOutput }.output n⊢ { status := sStatus, output := sOutput } = { status := tStatus, output := tOutput }
          simp only at hStatus hOutputmk.mkν:Type upayload:Type vsStatus:ν → NodeStatussOutput:ν → Option payloadtStatus:ν → NodeStatustOutput:ν → Option payloadhStatus:∀ (n : ν), sStatus n = tStatus nhOutput:∀ (n : ν), sOutput n = tOutput n⊢ { status := sStatus, output := sOutput } = { status := tStatus, output := tOutput }
          cases funext hStatusmk.mk.reflν:Type upayload:Type vsStatus:ν → NodeStatussOutput:ν → Option payloadtOutput:ν → Option payloadhOutput:∀ (n : ν), sOutput n = tOutput nhStatus:∀ (n : ν), sStatus n = sStatus n⊢ { status := sStatus, output := sOutput } = { status := sStatus, output := tOutput }
          cases funext hOutputmk.mk.refl.reflν:Type upayload:Type vsStatus:ν → NodeStatussOutput:ν → Option payloadhStatus:∀ (n : ν), sStatus n = sStatus nhOutput:∀ (n : ν), sOutput n = sOutput n⊢ { status := sStatus, output := sOutput } = { status := sStatus, output := sOutput }
          rflAll goals completed! 🐙

GraphState.initial sets every node to pending with no output.

def initial : GraphState ν payload where
  status := fun _ => NodeStatus.pending
  output := fun _ => none

Failure-Growth Order

GraphState.failureLe left right lifts status failure-growth pointwise.

Outputs are intentionally outside this order because failure propagation does not inspect them; output ownership and preservation are separate invariants.

def failureLe (left right : GraphState ν payload) : Prop :=
  ∀ node : ν, NodeStatus.failureLe (left.status node) (right.status node)

failureLe_refl says graph-state failure-growth is reflexive.

theorem failureLe_refl (state : GraphState ν payload) :
    failureLe state state := byν:Type upayload:Type vstate:GraphState ν payload⊢ state.failureLe state
  intro nodeν:Type upayload:Type vstate:GraphState ν payloadnode:ν⊢ (state.status node).failureLe (state.status node)
  exact NodeStatus.failureLe_refl (state.status node)All goals completed! 🐙

failureLe_trans says graph-state failure-growth is transitive.

theorem failureLe_trans {left middle right : GraphState ν payload}
    (hLeft : failureLe left middle)
    (hRight : failureLe middle right) :
    failureLe left right := byν:Type upayload:Type vleft:GraphState ν payloadmiddle:GraphState ν payloadright:GraphState ν payloadhLeft:left.failureLe middlehRight:middle.failureLe right⊢ left.failureLe right
  intro nodeν:Type upayload:Type vleft:GraphState ν payloadmiddle:GraphState ν payloadright:GraphState ν payloadhLeft:left.failureLe middlehRight:middle.failureLe rightnode:ν⊢ (left.status node).failureLe (right.status node)
  exact NodeStatus.failureLe_trans (hLeft node) (hRight node)All goals completed! 🐙

failureLe_preserves_failed lifts failed-status preservation to graph states.

theorem failureLe_preserves_failed {left right : GraphState ν payload}
    (hLe : failureLe left right)
    {node : ν}
    (hFailed : left.status node = NodeStatus.failed) :
    right.status node = NodeStatus.failed :=
  NodeStatus.failureLe_preserves_failed (hLe node) hFailed

Recovery Normalization

resetStatus status resets only volatile execution statuses before resumption.

def resetStatus : NodeStatus → NodeStatus
  | NodeStatus.running => NodeStatus.pending
  | NodeStatus.interrupted => NodeStatus.pending
  | NodeStatus.pending => NodeStatus.pending
  | NodeStatus.completed => NodeStatus.completed
  | NodeStatus.failed => NodeStatus.failed
  | NodeStatus.skipped => NodeStatus.skipped
  | NodeStatus.waiting => NodeStatus.waiting
  | NodeStatus.rewritten => NodeStatus.rewritten

resetStatus_preserves_terminal preserves terminal status through recovery reset.

theorem resetStatus_preserves_terminal {status : NodeStatus}
    (hTerminal : NodeStatus.terminal status) :
    NodeStatus.terminal (resetStatus status) := bystatus:NodeStatushTerminal:status.terminal⊢ (resetStatus status).terminal
  cases statuspendinghTerminal:NodeStatus.pending.terminal⊢ (resetStatus NodeStatus.pending).terminalrunninghTerminal:NodeStatus.running.terminal⊢ (resetStatus NodeStatus.running).terminalcompletedhTerminal:NodeStatus.completed.terminal⊢ (resetStatus NodeStatus.completed).terminalfailedhTerminal:NodeStatus.failed.terminal⊢ (resetStatus NodeStatus.failed).terminalskippedhTerminal:NodeStatus.skipped.terminal⊢ (resetStatus NodeStatus.skipped).terminalinterruptedhTerminal:NodeStatus.interrupted.terminal⊢ (resetStatus NodeStatus.interrupted).terminalwaitinghTerminal:NodeStatus.waiting.terminal⊢ (resetStatus NodeStatus.waiting).terminalrewrittenhTerminal:NodeStatus.rewritten.terminal⊢ (resetStatus NodeStatus.rewritten).terminal <;>pendinghTerminal:NodeStatus.pending.terminal⊢ (resetStatus NodeStatus.pending).terminalrunninghTerminal:NodeStatus.running.terminal⊢ (resetStatus NodeStatus.running).terminalcompletedhTerminal:NodeStatus.completed.terminal⊢ (resetStatus NodeStatus.completed).terminalfailedhTerminal:NodeStatus.failed.terminal⊢ (resetStatus NodeStatus.failed).terminalskippedhTerminal:NodeStatus.skipped.terminal⊢ (resetStatus NodeStatus.skipped).terminalinterruptedhTerminal:NodeStatus.interrupted.terminal⊢ (resetStatus NodeStatus.interrupted).terminalwaitinghTerminal:NodeStatus.waiting.terminal⊢ (resetStatus NodeStatus.waiting).terminalrewrittenhTerminal:NodeStatus.rewritten.terminal⊢ (resetStatus NodeStatus.rewritten).terminal simp [resetStatus, NodeStatus.terminal] at hTerminal ⊢All goals completed! 🐙

resetStatus_reflects_unblocks recovers original unblocking from reset unblocking.

theorem resetStatus_reflects_unblocks {status : NodeStatus}
    (hUnblocks : NodeStatus.unblocksSuccessors (resetStatus status)) :
    NodeStatus.unblocksSuccessors status := bystatus:NodeStatushUnblocks:(resetStatus status).unblocksSuccessors⊢ status.unblocksSuccessors
  cases statuspendinghUnblocks:(resetStatus NodeStatus.pending).unblocksSuccessors⊢ NodeStatus.pending.unblocksSuccessorsrunninghUnblocks:(resetStatus NodeStatus.running).unblocksSuccessors⊢ NodeStatus.running.unblocksSuccessorscompletedhUnblocks:(resetStatus NodeStatus.completed).unblocksSuccessors⊢ NodeStatus.completed.unblocksSuccessorsfailedhUnblocks:(resetStatus NodeStatus.failed).unblocksSuccessors⊢ NodeStatus.failed.unblocksSuccessorsskippedhUnblocks:(resetStatus NodeStatus.skipped).unblocksSuccessors⊢ NodeStatus.skipped.unblocksSuccessorsinterruptedhUnblocks:(resetStatus NodeStatus.interrupted).unblocksSuccessors⊢ NodeStatus.interrupted.unblocksSuccessorswaitinghUnblocks:(resetStatus NodeStatus.waiting).unblocksSuccessors⊢ NodeStatus.waiting.unblocksSuccessorsrewrittenhUnblocks:(resetStatus NodeStatus.rewritten).unblocksSuccessors⊢ NodeStatus.rewritten.unblocksSuccessors <;>pendinghUnblocks:(resetStatus NodeStatus.pending).unblocksSuccessors⊢ NodeStatus.pending.unblocksSuccessorsrunninghUnblocks:(resetStatus NodeStatus.running).unblocksSuccessors⊢ NodeStatus.running.unblocksSuccessorscompletedhUnblocks:(resetStatus NodeStatus.completed).unblocksSuccessors⊢ NodeStatus.completed.unblocksSuccessorsfailedhUnblocks:(resetStatus NodeStatus.failed).unblocksSuccessors⊢ NodeStatus.failed.unblocksSuccessorsskippedhUnblocks:(resetStatus NodeStatus.skipped).unblocksSuccessors⊢ NodeStatus.skipped.unblocksSuccessorsinterruptedhUnblocks:(resetStatus NodeStatus.interrupted).unblocksSuccessors⊢ NodeStatus.interrupted.unblocksSuccessorswaitinghUnblocks:(resetStatus NodeStatus.waiting).unblocksSuccessors⊢ NodeStatus.waiting.unblocksSuccessorsrewrittenhUnblocks:(resetStatus NodeStatus.rewritten).unblocksSuccessors⊢ NodeStatus.rewritten.unblocksSuccessors simp [resetStatus, NodeStatus.unblocksSuccessors] at hUnblocks ⊢All goals completed! 🐙

resetStatus_reflects_requiresOutput recovers original output requirements.

theorem resetStatus_reflects_requiresOutput {status : NodeStatus}
    (hRequiresOutput : NodeStatus.requiresOutput (resetStatus status)) :
    NodeStatus.requiresOutput status := bystatus:NodeStatushRequiresOutput:(resetStatus status).requiresOutput⊢ status.requiresOutput
  cases statuspendinghRequiresOutput:(resetStatus NodeStatus.pending).requiresOutput⊢ NodeStatus.pending.requiresOutputrunninghRequiresOutput:(resetStatus NodeStatus.running).requiresOutput⊢ NodeStatus.running.requiresOutputcompletedhRequiresOutput:(resetStatus NodeStatus.completed).requiresOutput⊢ NodeStatus.completed.requiresOutputfailedhRequiresOutput:(resetStatus NodeStatus.failed).requiresOutput⊢ NodeStatus.failed.requiresOutputskippedhRequiresOutput:(resetStatus NodeStatus.skipped).requiresOutput⊢ NodeStatus.skipped.requiresOutputinterruptedhRequiresOutput:(resetStatus NodeStatus.interrupted).requiresOutput⊢ NodeStatus.interrupted.requiresOutputwaitinghRequiresOutput:(resetStatus NodeStatus.waiting).requiresOutput⊢ NodeStatus.waiting.requiresOutputrewrittenhRequiresOutput:(resetStatus NodeStatus.rewritten).requiresOutput⊢ NodeStatus.rewritten.requiresOutput <;>pendinghRequiresOutput:(resetStatus NodeStatus.pending).requiresOutput⊢ NodeStatus.pending.requiresOutputrunninghRequiresOutput:(resetStatus NodeStatus.running).requiresOutput⊢ NodeStatus.running.requiresOutputcompletedhRequiresOutput:(resetStatus NodeStatus.completed).requiresOutput⊢ NodeStatus.completed.requiresOutputfailedhRequiresOutput:(resetStatus NodeStatus.failed).requiresOutput⊢ NodeStatus.failed.requiresOutputskippedhRequiresOutput:(resetStatus NodeStatus.skipped).requiresOutput⊢ NodeStatus.skipped.requiresOutputinterruptedhRequiresOutput:(resetStatus NodeStatus.interrupted).requiresOutput⊢ NodeStatus.interrupted.requiresOutputwaitinghRequiresOutput:(resetStatus NodeStatus.waiting).requiresOutput⊢ NodeStatus.waiting.requiresOutputrewrittenhRequiresOutput:(resetStatus NodeStatus.rewritten).requiresOutput⊢ NodeStatus.rewritten.requiresOutput simp [resetStatus, NodeStatus.requiresOutput] at hRequiresOutput ⊢All goals completed! 🐙

resetRunningToPending state makes in-flight nodes pending again after a crash.

def resetRunningToPending (s : GraphState ν payload) : GraphState ν payload where
  status := fun n => resetStatus (s.status n)
  output := s.output

noRunningNodes state means no node is still marked as running.

def noRunningNodes (s : GraphState ν payload) : Prop :=
  ∀ n : ν, s.status n ≠ NodeStatus.running

noInterruptedNodes state means recovery has removed interrupted markers.

def noInterruptedNodes (s : GraphState ν payload) : Prop :=
  ∀ n : ν, s.status n ≠ NodeStatus.interrupted

outputsRespectStatuses state constrains outputs to statuses that may retain them.

def outputsRespectStatuses (s : GraphState ν payload) : Prop :=
  ∀ (n : ν) (value : payload),
    s.output n = some value → NodeStatus.mayHaveOutput (s.status n)

outputsCompleteForStatuses state requires payload-owning statuses to have outputs.

def outputsCompleteForStatuses (s : GraphState ν payload) : Prop :=
  ∀ n : ν, NodeStatus.requiresOutput (s.status n) → ∃ value : payload, s.output n = some value

topologyDomain G state says off-topology nodes are absent from durable state.

def topologyDomain (G : DAG ν) (s : GraphState ν payload) : Prop :=
  ∀ n : ν, n ∉ G.nodes → s.status n = NodeStatus.pending ∧ s.output n = none

Normalization Theorem

resetRunning_no_running proves status reset removes every running marker.

theorem resetRunning_no_running (s : GraphState ν payload) :
    noRunningNodes (resetRunningToPending s) := byν:Type upayload:Type vs:GraphState ν payload⊢ s.resetRunningToPending.noRunningNodes
  intro nν:Type upayload:Type vs:GraphState ν payloadn:ν⊢ s.resetRunningToPending.status n ≠ NodeStatus.running
  cases hStatus : s.status npendingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.pending⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningrunningν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.running⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningcompletedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.completed⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningfailedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.failed⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningskippedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.skipped⊢ s.resetRunningToPending.status n ≠ NodeStatus.runninginterruptedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.interrupted⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningwaitingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.waiting⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningrewrittenν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.rewritten⊢ s.resetRunningToPending.status n ≠ NodeStatus.running <;>pendingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.pending⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningrunningν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.running⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningcompletedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.completed⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningfailedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.failed⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningskippedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.skipped⊢ s.resetRunningToPending.status n ≠ NodeStatus.runninginterruptedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.interrupted⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningwaitingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.waiting⊢ s.resetRunningToPending.status n ≠ NodeStatus.runningrewrittenν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.rewritten⊢ s.resetRunningToPending.status n ≠ NodeStatus.running
    simp [resetRunningToPending, resetStatus, hStatus]All goals completed! 🐙

resetRunning_no_interrupted proves status reset removes every interrupted marker.

theorem resetRunning_no_interrupted (s : GraphState ν payload) :
    noInterruptedNodes (resetRunningToPending s) := byν:Type upayload:Type vs:GraphState ν payload⊢ s.resetRunningToPending.noInterruptedNodes
  intro nν:Type upayload:Type vs:GraphState ν payloadn:ν⊢ s.resetRunningToPending.status n ≠ NodeStatus.interrupted
  cases hStatus : s.status npendingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.pending⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedrunningν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.running⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedcompletedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.completed⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedfailedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.failed⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedskippedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.skipped⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedinterruptedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.interrupted⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedwaitingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.waiting⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedrewrittenν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.rewritten⊢ s.resetRunningToPending.status n ≠ NodeStatus.interrupted <;>pendingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.pending⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedrunningν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.running⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedcompletedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.completed⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedfailedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.failed⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedskippedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.skipped⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedinterruptedν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.interrupted⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedwaitingν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.waiting⊢ s.resetRunningToPending.status n ≠ NodeStatus.interruptedrewrittenν:Type upayload:Type vs:GraphState ν payloadn:νhStatus:s.status n = NodeStatus.rewritten⊢ s.resetRunningToPending.status n ≠ NodeStatus.interrupted
    simp [resetRunningToPending, resetStatus, hStatus]All goals completed! 🐙

resetRunning_preserves_topologyDomain preserves the off-topology invariant.

theorem resetRunning_preserves_topologyDomain
    (G : DAG ν)
    (s : GraphState ν payload)
    (hDomain : topologyDomain G s) :
    topologyDomain G (resetRunningToPending s) := byν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G s⊢ topologyDomain G s.resetRunningToPending
  intro node hNotMemν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G snode:νhNotMem:node ∉ G.nodes⊢ s.resetRunningToPending.status node = NodeStatus.pending ∧ s.resetRunningToPending.output node = none
  rcases hDomain node hNotMem with ⟨hStatus, hOutput⟩ν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G snode:νhNotMem:node ∉ G.nodeshStatus:s.status node = NodeStatus.pendinghOutput:s.output node = none⊢ s.resetRunningToPending.status node = NodeStatus.pending ∧ s.resetRunningToPending.output node = none
  constructorleftν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G snode:νhNotMem:node ∉ G.nodeshStatus:s.status node = NodeStatus.pendinghOutput:s.output node = none⊢ s.resetRunningToPending.status node = NodeStatus.pendingrightν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G snode:νhNotMem:node ∉ G.nodeshStatus:s.status node = NodeStatus.pendinghOutput:s.output node = none⊢ s.resetRunningToPending.output node = none
  ·leftν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G snode:νhNotMem:node ∉ G.nodeshStatus:s.status node = NodeStatus.pendinghOutput:s.output node = none⊢ s.resetRunningToPending.status node = NodeStatus.pending simp [resetRunningToPending, resetStatus, hStatus]All goals completed! 🐙
  ·rightν:Type upayload:Type vG:DAG νs:GraphState ν payloadhDomain:topologyDomain G snode:νhNotMem:node ∉ G.nodeshStatus:s.status node = NodeStatus.pendinghOutput:s.output node = none⊢ s.resetRunningToPending.output node = none simpa [resetRunningToPending] using hOutputAll goals completed! 🐙

resetRunning_preserves_outputsRespectStatuses preserves output ownership.

theorem resetRunning_preserves_outputsRespectStatuses
    (s : GraphState ν payload)
    (hOutputs : outputsRespectStatuses s) :
    outputsRespectStatuses (resetRunningToPending s) := byν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatuses⊢ s.resetRunningToPending.outputsRespectStatuses
  intro node valueν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payload⊢ s.resetRunningToPending.output node = some value → (s.resetRunningToPending.status node).mayHaveOutput hOutputν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some value⊢ (s.resetRunningToPending.status node).mayHaveOutput
  have hMayHaveOutput : NodeStatus.mayHaveOutput (s.status node) :=
    hOutputs node value hOutputν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutput⊢ (s.resetRunningToPending.status node).mayHaveOutput
  cases hStatus : s.status nodependingν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.pending⊢ (s.resetRunningToPending.status node).mayHaveOutputrunningν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.running⊢ (s.resetRunningToPending.status node).mayHaveOutputcompletedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.completed⊢ (s.resetRunningToPending.status node).mayHaveOutputfailedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.failed⊢ (s.resetRunningToPending.status node).mayHaveOutputskippedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.skipped⊢ (s.resetRunningToPending.status node).mayHaveOutputinterruptedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.interrupted⊢ (s.resetRunningToPending.status node).mayHaveOutputwaitingν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.waiting⊢ (s.resetRunningToPending.status node).mayHaveOutputrewrittenν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.rewritten⊢ (s.resetRunningToPending.status node).mayHaveOutput <;>pendingν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.pending⊢ (s.resetRunningToPending.status node).mayHaveOutputrunningν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.running⊢ (s.resetRunningToPending.status node).mayHaveOutputcompletedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.completed⊢ (s.resetRunningToPending.status node).mayHaveOutputfailedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.failed⊢ (s.resetRunningToPending.status node).mayHaveOutputskippedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.skipped⊢ (s.resetRunningToPending.status node).mayHaveOutputinterruptedν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.interrupted⊢ (s.resetRunningToPending.status node).mayHaveOutputwaitingν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.waiting⊢ (s.resetRunningToPending.status node).mayHaveOutputrewrittenν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsRespectStatusesnode:νvalue:payloadhOutput:s.resetRunningToPending.output node = some valuehMayHaveOutput:(s.status node).mayHaveOutputhStatus:s.status node = NodeStatus.rewritten⊢ (s.resetRunningToPending.status node).mayHaveOutput
    simp
      [ resetRunningToPending
      , resetStatus
      , NodeStatus.mayHaveOutput
      , hStatus
      ] at hMayHaveOutput ⊢All goals completed! 🐙

resetRunning_preserves_outputsCompleteForStatuses preserves required outputs.

theorem resetRunning_preserves_outputsCompleteForStatuses
    (s : GraphState ν payload)
    (hOutputs : outputsCompleteForStatuses s) :
    outputsCompleteForStatuses (resetRunningToPending s) := byν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsCompleteForStatuses⊢ s.resetRunningToPending.outputsCompleteForStatuses
  intro node hRequiresOutputν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsCompleteForStatusesnode:νhRequiresOutput:(s.resetRunningToPending.status node).requiresOutput⊢ ∃ value, s.resetRunningToPending.output node = some value
  have hResetRequires :
      NodeStatus.requiresOutput (resetStatus (s.status node)) := byν:Type upayload:Type vs:GraphState ν payloadhOutputs:s.outputsCompleteForStatuses⊢ s.resetRunningToPending.outputsCompleteForStatuses
    simpa [resetRunningToPending] using hRequiresOutputAll goals completed! 🐙
  exact hOutputs node (resetStatus_reflects_requiresOutput hResetRequires)All goals completed! 🐙

end GraphStateend Cortex.Pulse

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Pulse.RunSafety Next →Cortex.Pulse.Validity