Theory /Cortex /Pulse /Recovery

Cortex.Pulse.Recovery

proofs

On this page

Overview
Context
Theorem Split
Recovery Operator
Normalization Theorems
Structural Safety

Imports

import Cortex.Pulse.Fact
import Cortex.Pulse.Validity

Overview

Recovery first resets volatile execution state and then reapplies failure closure. The theorem statements here are intentionally structural: they prove the normalized-state pieces that do not depend on payload-specific business semantics.

Context

The runtime persists prefixes of execution state. After a crash, in-flight work is reset and failure is reclosed before classification. This page is the Lean counterpart of that recovery normalization pipeline.

Theorem Split

The page defines the recovered state, proves each structural invariant, and packages them into persistence_safety under explicit persisted topology, output-ownership, output-completeness, and causal-history preconditions.

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

Recovery Operator

recoveredState G state is crash-recovery normalization for the fixed-topology kernel.

noncomputable def recoveredState
    (G : DAG ν)
    (state : GraphState ν payload) : GraphState ν payload :=
  propagateFailure G (GraphState.resetRunningToPending state)

Normalization Theorems

recovered_noRunning proves recovery normalization removes running nodes.

theorem recovered_noRunning
    (G : DAG ν)
    (state : GraphState ν payload) :
    GraphState.noRunningNodes (recoveredState G state) :=
  propagateFailure_preserves_noRunning
    G
    (GraphState.resetRunningToPending state)
    (GraphState.resetRunning_no_running state)

recovered_noInterrupted proves recovery normalization removes interrupted nodes.

theorem recovered_noInterrupted
    (G : DAG ν)
    (state : GraphState ν payload) :
    GraphState.noInterruptedNodes (recoveredState G state) :=
  propagateFailure_preserves_noInterrupted
    G
    (GraphState.resetRunningToPending state)
    (GraphState.resetRunning_no_interrupted state)

recovered_topologyDomain preserves the persisted topology-domain invariant.

theorem recovered_topologyDomain
    (G : DAG ν)
    (state : GraphState ν payload)
    (hDomain : GraphState.topologyDomain G state) :
    GraphState.topologyDomain G (recoveredState G state) :=
  propagateFailure_preserves_topologyDomain
    G
    (GraphState.resetRunningToPending state)
    (GraphState.resetRunning_preserves_topologyDomain G state hDomain)

recovered_failureClosureComplete proves recovery normalization is failure-closed.

theorem recovered_failureClosureComplete
    (G : DAG ν)
    (state : GraphState ν payload) :
    failureClosureComplete G (recoveredState G state) :=
  propagateFailure_failureClosureComplete G (GraphState.resetRunningToPending state)

resetRunning_preserves_causalHistoryClosed preserves causal history closure.

theorem resetRunning_preserves_causalHistoryClosed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hCausal : CausalHistoryClosed G state) :
    CausalHistoryClosed G (GraphState.resetRunningToPending state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G state⊢ CausalHistoryClosed G state.resetRunningToPending
  intro node hUnblocksν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:(state.resetRunningToPending.status node).unblocksSuccessors⊢ ∀ (predecessor : ν), G.reaches predecessor node → (state.resetRunningToPending.status predecessor).terminal predecessorν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:(state.resetRunningToPending.status node).unblocksSuccessorspredecessor:ν⊢ G.reaches predecessor node → (state.resetRunningToPending.status predecessor).terminal hReachν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:(state.resetRunningToPending.status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor node⊢ (state.resetRunningToPending.status predecessor).terminal
  have hResetUnblocks :
      NodeStatus.unblocksSuccessors (GraphState.resetStatus (state.status node)) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G state⊢ CausalHistoryClosed G state.resetRunningToPending
    simpa [GraphState.resetRunningToPending] using hUnblocksAll goals completed! 🐙
  have hOriginalUnblocks : NodeStatus.unblocksSuccessors (state.status node) :=
    GraphState.resetStatus_reflects_unblocks hResetUnblocksν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:(state.resetRunningToPending.status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehResetUnblocks:(GraphState.resetStatus (state.status node)).unblocksSuccessorshOriginalUnblocks:(state.status node).unblocksSuccessors⊢ (state.resetRunningToPending.status predecessor).terminal
  have hOriginalTerminal : NodeStatus.terminal (state.status predecessor) :=
    hCausal node hOriginalUnblocks predecessor hReachν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:(state.resetRunningToPending.status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehResetUnblocks:(GraphState.resetStatus (state.status node)).unblocksSuccessorshOriginalUnblocks:(state.status node).unblocksSuccessorshOriginalTerminal:(state.status predecessor).terminal⊢ (state.resetRunningToPending.status predecessor).terminal
  simpa [GraphState.resetRunningToPending] using
    GraphState.resetStatus_preserves_terminal hOriginalTerminalAll goals completed! 🐙

propagateFailure_preserves_causalHistoryClosed preserves causal history closure.

theorem propagateFailure_preserves_causalHistoryClosed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hCausal : CausalHistoryClosed G state) :
    CausalHistoryClosed G (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G state⊢ CausalHistoryClosed G (propagateFailure G state)
  classical
  intro node hUnblocksν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessors⊢ ∀ (predecessor : ν), G.reaches predecessor node → ((propagateFailure G state).status predecessor).terminal predecessorν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:ν⊢ G.reaches predecessor node → ((propagateFailure G state).status predecessor).terminal hReachν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor node⊢ ((propagateFailure G state).status predecessor).terminal
  have hOriginalUnblocks : NodeStatus.unblocksSuccessors (state.status node) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G state⊢ CausalHistoryClosed G (propagateFailure G state)
    by_cases hClosed :
      NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (state.status node).unblocksSuccessorsnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (state.status node).unblocksSuccessors
    ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (state.status node).unblocksSuccessors simp
        [ propagateFailure
        , propagateStatus
        , NodeStatus.unblocksSuccessors
        , hClosed
        ] at hUnblocksAll goals completed! 🐙
    ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (state.status node).unblocksSuccessors simpa [propagateFailure, propagateStatus, hClosed] using hUnblocksAll goals completed! 🐙
  have hOriginalTerminal : NodeStatus.terminal (state.status predecessor) :=
    hCausal node hOriginalUnblocks predecessor hReachν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehOriginalUnblocks:(state.status node).unblocksSuccessorshOriginalTerminal:(state.status predecessor).terminal⊢ ((propagateFailure G state).status predecessor).terminal
  by_cases hClosed :
    NodeStatus.propagatable (state.status predecessor) ∧ hasFailedAncestor G state predecessorposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehOriginalUnblocks:(state.status node).unblocksSuccessorshOriginalTerminal:(state.status predecessor).terminalhClosed:(state.status predecessor).propagatable ∧ hasFailedAncestor G state predecessor⊢ ((propagateFailure G state).status predecessor).terminalnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehOriginalUnblocks:(state.status node).unblocksSuccessorshOriginalTerminal:(state.status predecessor).terminalhClosed:¬((state.status predecessor).propagatable ∧ hasFailedAncestor G state predecessor)⊢ ((propagateFailure G state).status predecessor).terminal
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehOriginalUnblocks:(state.status node).unblocksSuccessorshOriginalTerminal:(state.status predecessor).terminalhClosed:(state.status predecessor).propagatable ∧ hasFailedAncestor G state predecessor⊢ ((propagateFailure G state).status predecessor).terminal simp [propagateFailure, propagateStatus, NodeStatus.terminal, hClosed]All goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhUnblocks:((propagateFailure G state).status node).unblocksSuccessorspredecessor:νhReach:G.reaches predecessor nodehOriginalUnblocks:(state.status node).unblocksSuccessorshOriginalTerminal:(state.status predecessor).terminalhClosed:¬((state.status predecessor).propagatable ∧ hasFailedAncestor G state predecessor)⊢ ((propagateFailure G state).status predecessor).terminal simpa [propagateFailure, propagateStatus, hClosed] using hOriginalTerminalAll goals completed! 🐙

recovered_causalHistoryClosed preserves causal history through recovery.

theorem recovered_causalHistoryClosed
    (G : DAG ν)
    (state : GraphState ν payload)
    (hCausal : CausalHistoryClosed G state) :
    CausalHistoryClosed G (recoveredState G state) :=
  propagateFailure_preserves_causalHistoryClosed
    G
    (GraphState.resetRunningToPending state)
    (resetRunning_preserves_causalHistoryClosed G state hCausal)

recovered_frontierBridge proves recovery aligns proof and runtime frontiers.

theorem recovered_frontierBridge
    (G : DAG ν)
    (state : GraphState ν payload)
    (hCausal : CausalHistoryClosed G state) :
    frontierBridge G (recoveredState G state) :=
  frontierBridge_of_closed_causal
    G
    (recoveredState G state)
    (recovered_failureClosureComplete G state)
    (recovered_causalHistoryClosed G state hCausal)

recovered_outputsRespectStatuses preserves output ownership through recovery.

theorem recovered_outputsRespectStatuses
    (G : DAG ν)
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsRespectStatuses state) :
    GraphState.outputsRespectStatuses (recoveredState G state) :=
  propagateFailure_preserves_outputsRespectStatuses
    G
    (GraphState.resetRunningToPending state)
    (GraphState.resetRunning_preserves_outputsRespectStatuses state hOutputs)

recovered_outputsCompleteForStatuses preserves required outputs through recovery.

theorem recovered_outputsCompleteForStatuses
    (G : DAG ν)
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsCompleteForStatuses state) :
    GraphState.outputsCompleteForStatuses (recoveredState G state) :=
  propagateFailure_preserves_outputsCompleteForStatuses
    G
    (GraphState.resetRunningToPending state)
    (GraphState.resetRunning_preserves_outputsCompleteForStatuses state hOutputs)

Structural Safety

PersistedRecoveryPreconditions G state is what recovery must trust or validate.

structure PersistedRecoveryPreconditions
    (G : DAG ν)
    (state : GraphState ν payload) : Prop where

Persisted state has no status/output entries outside the topology.

topologyDomain : GraphState.topologyDomain G state

Persisted outputs are attached only to statuses that may own payloads.

outputsRespectStatuses : GraphState.outputsRespectStatuses state

Persisted payload-owning statuses have their required outputs present.

outputsCompleteForStatuses : GraphState.outputsCompleteForStatuses state

Persisted terminal/unblocking history is causally closed.

causalHistoryClosed : CausalHistoryClosed G state

persistedRecoveryPreconditions G state keeps the published predicate name stable.

abbrev persistedRecoveryPreconditions
    (G : DAG ν)
    (state : GraphState ν payload) : Prop :=
  PersistedRecoveryPreconditions G state

persistence_safety packages structural recovery safety.

Structural recovery safety is conditional on persisted topology-domain, payload/output, output-completeness, and causal-history preconditions. Recovery then preserves those preconditions while establishing no-running, no-interrupted, failure-closure, and the proof/runtime frontier bridge.

theorem persistence_safety
    (G : DAG ν)
    (state : GraphState ν payload)
    (hPersisted : persistedRecoveryPreconditions G state) :
    wellFormedGraphState G (recoveredState G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhPersisted:persistedRecoveryPreconditions G state⊢ wellFormedGraphState G (recoveredState G state)
  exact
    { topologyDomain := recovered_topologyDomain G state hPersisted.topologyDomain
      outputsRespectStatuses :=
        recovered_outputsRespectStatuses G state hPersisted.outputsRespectStatuses
      outputsCompleteForStatuses :=
        recovered_outputsCompleteForStatuses G state hPersisted.outputsCompleteForStatuses
      noRunningNodes := recovered_noRunning G state
      noInterruptedNodes := recovered_noInterrupted G state
      failureClosureComplete := recovered_failureClosureComplete G state
      causalHistoryClosed := recovered_causalHistoryClosed G state hPersisted.causalHistoryClosed
      frontierBridge := recovered_frontierBridge G state hPersisted.causalHistoryClosed }All goals completed! 🐙

frontierFacts_recovered_wellFormedGraphState safely recovers admissible fact folds.

theorem frontierFacts_recovered_wellFormedGraphState [DecidableEq ν]
    (G : DAG ν)
    (state : GraphState ν payload)
    (results : List (NodeResult ν payload))
    (hWellFormed : wellFormedGraphState G state)
    (hResults : NodeResult.AllAdmissibleFold G state results) :
    wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state)) := byν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadresults:List (NodeResult ν payload)hWellFormed:wellFormedGraphState G statehResults:NodeResult.AllAdmissibleFold G state results⊢ wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state))
  have hAccumulatedDomain :
      GraphState.topologyDomain G (NodeResult.applyNodeFacts results state) :=
    NodeResult.applyNodeFacts_preserves_topologyDomain
      G
      results
      state
      hWellFormed.topologyDomain
      hResultsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadresults:List (NodeResult ν payload)hWellFormed:wellFormedGraphState G statehResults:NodeResult.AllAdmissibleFold G state resultshAccumulatedDomain:GraphState.topologyDomain G (NodeResult.applyNodeFacts results state)⊢ wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state))
  have hAccumulatedOutputs :
      GraphState.outputsRespectStatuses (NodeResult.applyNodeFacts results state) :=
    NodeResult.applyNodeFacts_preserves_outputsRespectStatuses
      G
      results
      state
      hWellFormed.outputsRespectStatuses
      hResultsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadresults:List (NodeResult ν payload)hWellFormed:wellFormedGraphState G statehResults:NodeResult.AllAdmissibleFold G state resultshAccumulatedDomain:GraphState.topologyDomain G (NodeResult.applyNodeFacts results state)hAccumulatedOutputs:(NodeResult.applyNodeFacts results state).outputsRespectStatuses⊢ wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state))
  have hAccumulatedOutputsComplete :
      GraphState.outputsCompleteForStatuses (NodeResult.applyNodeFacts results state) :=
    NodeResult.applyNodeFacts_preserves_outputsCompleteForStatuses
      G
      results
      state
      hWellFormed.outputsCompleteForStatuses
      hResultsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadresults:List (NodeResult ν payload)hWellFormed:wellFormedGraphState G statehResults:NodeResult.AllAdmissibleFold G state resultshAccumulatedDomain:GraphState.topologyDomain G (NodeResult.applyNodeFacts results state)hAccumulatedOutputs:(NodeResult.applyNodeFacts results state).outputsRespectStatuseshAccumulatedOutputsComplete:(NodeResult.applyNodeFacts results state).outputsCompleteForStatuses⊢ wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state))
  have hAccumulatedCausal :
      CausalHistoryClosed G (NodeResult.applyNodeFacts results state) :=
    NodeResult.applyNodeFacts_preserves_causalHistoryClosed
      G
      results
      state
      hWellFormed.causalHistoryClosed
      hResultsν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadresults:List (NodeResult ν payload)hWellFormed:wellFormedGraphState G statehResults:NodeResult.AllAdmissibleFold G state resultshAccumulatedDomain:GraphState.topologyDomain G (NodeResult.applyNodeFacts results state)hAccumulatedOutputs:(NodeResult.applyNodeFacts results state).outputsRespectStatuseshAccumulatedOutputsComplete:(NodeResult.applyNodeFacts results state).outputsCompleteForStatuseshAccumulatedCausal:CausalHistoryClosed G (NodeResult.applyNodeFacts results state)⊢ wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state))
  have hPersisted :
      persistedRecoveryPreconditions G (NodeResult.applyNodeFacts results state) :=
    { topologyDomain := hAccumulatedDomain
      outputsRespectStatuses := hAccumulatedOutputs
      outputsCompleteForStatuses := hAccumulatedOutputsComplete
      causalHistoryClosed := hAccumulatedCausal }ν:Type upayload:Type vinst✝:DecidableEq νG:DAG νstate:GraphState ν payloadresults:List (NodeResult ν payload)hWellFormed:wellFormedGraphState G statehResults:NodeResult.AllAdmissibleFold G state resultshAccumulatedDomain:GraphState.topologyDomain G (NodeResult.applyNodeFacts results state)hAccumulatedOutputs:(NodeResult.applyNodeFacts results state).outputsRespectStatuseshAccumulatedOutputsComplete:(NodeResult.applyNodeFacts results state).outputsCompleteForStatuseshAccumulatedCausal:CausalHistoryClosed G (NodeResult.applyNodeFacts results state)hPersisted:persistedRecoveryPreconditions G (NodeResult.applyNodeFacts results state)⊢ wellFormedGraphState G (recoveredState G (NodeResult.applyNodeFacts results state))
  exact persistence_safety G (NodeResult.applyNodeFacts results state) hPersistedAll goals completed! 🐙

end Cortex.Pulse

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

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