Theory /Cortex /Pulse /Closure

Cortex.Pulse.Closure

proofs

On this page

Overview
Context
Theorem Split
Failed-Ancestor Model
Closure Operator
Closure Facts
Normalization Preservation
Idempotence

Imports

import Cortex.Pulse.Frontier

Overview

Failure closure propagates failed status through the fixed topology while leaving terminal successes and skipped/rewritten nodes intact. This is the structural part of the runtime's propagateFailure: it says nothing about failure payloads, retry policy, or operator-facing diagnostics.

Context

The closure operator is the main Paper 1 recovery law: once a node fails, every still-propagatable descendant must fail too. The model keeps the operator extensional and proves the closure/fixed-point facts needed by recovery.

Theorem Split

The page defines failed ancestors, defines the closure operator, proves that one pass is failure-complete, and finishes with idempotence.

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

Failed-Ancestor Model

hasFailedAncestor G state node means the node has a strict failed ancestor.

def hasFailedAncestor
    (G : DAG ν)
    (state : GraphState ν payload)
    (node : ν) : Prop :=
  ∃ failedNode : ν,
    state.status failedNode = NodeStatus.failed ∧ G.reaches failedNode node

failureClosureComplete G state means failure is closed over propagatable descendants.

A state is failure-closed when propagatable descendants of failed nodes are already marked failed.

def failureClosureComplete
    (G : DAG ν)
    (state : GraphState ν payload) : Prop :=
  ∀ failedNode node : ν,
    state.status failedNode = NodeStatus.failed →
      G.reaches failedNode node →
        NodeStatus.propagatable (state.status node) →
          state.status node = NodeStatus.failed

Closure Operator

propagateStatus G state node is the single-node failure-closure status update.

noncomputable def propagateStatus
    (G : DAG ν)
    (state : GraphState ν payload)
    (node : ν) : NodeStatus := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:ν⊢ NodeStatus
  classical
  exact
    if NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state node then
      NodeStatus.failed
    else
      state.status nodeAll goals completed! 🐙

propagateFailure G state propagates failure to pending or waiting descendants.

noncomputable def propagateFailure
    (G : DAG ν)
    (state : GraphState ν payload) : GraphState ν payload where
  status := fun node => propagateStatus G state node
  output := state.output

Closure Facts

propagateFailure_preserves_failed shows existing failed nodes stay failed.

theorem propagateFailure_preserves_failed
    (G : DAG ν)
    (state : GraphState ν payload)
    {node : ν}
    (hFailed : state.status node = NodeStatus.failed) :
    (propagateFailure G state).status node = NodeStatus.failed := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:state.status node = NodeStatus.failed⊢ (propagateFailure G state).status node = NodeStatus.failed
  classical
  simp [propagateFailure, propagateStatus, hFailed, NodeStatus.propagatable]All goals completed! 🐙

propagateFailure_marks_failed_descendant marks propagatable failed descendants.

theorem propagateFailure_marks_failed_descendant
    (G : DAG ν)
    (state : GraphState ν payload)
    {node : ν}
    (hPropagatable : NodeStatus.propagatable (state.status node))
    (hAncestor : hasFailedAncestor G state node) :
    (propagateFailure G state).status node = NodeStatus.failed := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhPropagatable:(state.status node).propagatablehAncestor:hasFailedAncestor G state node⊢ (propagateFailure G state).status node = NodeStatus.failed
  classical
  simp [propagateFailure, propagateStatus, hPropagatable, hAncestor]All goals completed! 🐙

propagatable_of_propagate recovers original propagatability after propagation.

theorem propagatable_of_propagate
    (G : DAG ν)
    (state : GraphState ν payload)
    {node : ν}
    (hPropagatable :
      NodeStatus.propagatable ((propagateFailure G state).status node)) :
    NodeStatus.propagatable (state.status node) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhPropagatable:((propagateFailure G state).status node).propagatable⊢ (state.status node).propagatable
  classical
  by_cases hClosed :
    NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhPropagatable:((propagateFailure G state).status node).propagatablehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (state.status node).propagatablenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhPropagatable:((propagateFailure G state).status node).propagatablehClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (state.status node).propagatable
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhPropagatable:((propagateFailure G state).status node).propagatablehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (state.status node).propagatable exact hClosed.1All goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhPropagatable:((propagateFailure G state).status node).propagatablehClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (state.status node).propagatable simpa [propagateFailure, propagateStatus, hClosed] using hPropagatableAll goals completed! 🐙

failed_after_propagate_origin identifies why a node is failed after propagation.

Every failed node after propagation either was failed already or had an original failed ancestor.

theorem failed_after_propagate
    (G : DAG ν)
    (state : GraphState ν payload)
    {node : ν}
    (hFailed : (propagateFailure G state).status node = NodeStatus.failed) :
    state.status node = NodeStatus.failed ∨ hasFailedAncestor G state node := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:(propagateFailure G state).status node = NodeStatus.failed⊢ state.status node = NodeStatus.failed ∨ hasFailedAncestor G state node
  classical
  by_cases hClosed :
    NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:(propagateFailure G state).status node = NodeStatus.failedhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ state.status node = NodeStatus.failed ∨ hasFailedAncestor G state nodenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:(propagateFailure G state).status node = NodeStatus.failedhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ state.status node = NodeStatus.failed ∨ hasFailedAncestor G state node
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:(propagateFailure G state).status node = NodeStatus.failedhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ state.status node = NodeStatus.failed ∨ hasFailedAncestor G state node exact Or.inr hClosed.2All goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:(propagateFailure G state).status node = NodeStatus.failedhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ state.status node = NodeStatus.failed ∨ hasFailedAncestor G state node have hOriginal : state.status node = NodeStatus.failed := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:(propagateFailure G state).status node = NodeStatus.failed⊢ state.status node = NodeStatus.failed ∨ hasFailedAncestor G state node
      simpa [propagateFailure, propagateStatus, hClosed] using hFailedAll goals completed! 🐙
    exact Or.inl hOriginalAll goals completed! 🐙

failed_after_propagate_has_original_failed_ancestor traces propagated failures.

A failed node produced by propagation still traces back to an original failed ancestor for every descendant it reaches.

theorem hasFailedAncestor_of_failed_after_reaches
    (G : DAG ν)
    (state : GraphState ν payload)
    {failedNode node : ν}
    (hFailed : (propagateFailure G state).status failedNode = NodeStatus.failed)
    (hReach : G.reaches failedNode node) :
    hasFailedAncestor G state node := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode node⊢ hasFailedAncestor G state node
  rcases failed_after_propagate G state hFailed with hOriginalFailed | hAncestorinlν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehOriginalFailed:state.status failedNode = NodeStatus.failed⊢ hasFailedAncestor G state nodeinrν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehAncestor:hasFailedAncestor G state failedNode⊢ hasFailedAncestor G state node
  ·inlν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehOriginalFailed:state.status failedNode = NodeStatus.failed⊢ hasFailedAncestor G state node exact ⟨failedNode, hOriginalFailed, hReach⟩All goals completed! 🐙
  ·inrν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehAncestor:hasFailedAncestor G state failedNode⊢ hasFailedAncestor G state node rcases hAncestor with ⟨root, hRootFailed, hRootReach⟩inrν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode noderoot:νhRootFailed:state.status root = NodeStatus.failedhRootReach:G.reaches root failedNode⊢ hasFailedAncestor G state node
    exact ⟨root, hRootFailed, G.reaches_trans hRootReach hReach⟩All goals completed! 🐙

hasFailedAncestor_monotone lifts failed ancestors through failure-growth.

theorem hasFailedAncestor_monotone
    (G : DAG ν)
    {left right : GraphState ν payload}
    (hLe : GraphState.failureLe left right)
    {node : ν}
    (hAncestor : hasFailedAncestor G left node) :
    hasFailedAncestor G right node := byν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhAncestor:hasFailedAncestor G left node⊢ hasFailedAncestor G right node
  rcases hAncestor with ⟨failedNode, hFailed, hReach⟩ν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νfailedNode:νhFailed:left.status failedNode = NodeStatus.failedhReach:G.reaches failedNode node⊢ hasFailedAncestor G right node
  exact ⟨failedNode, GraphState.failureLe_preserves_failed hLe hFailed, hReach⟩All goals completed! 🐙

propagateFailure_extensive proves propagation is extensive over failed nodes.

Use this closure-law theorem when a proof only needs preservation of the already-failed set. Use propagateFailure_monotone for whole-state failure-growth reasoning through GraphState.failureLe.

theorem propagateFailure_extensive
    (G : DAG ν)
    (state : GraphState ν payload) :
    ∀ node : ν,
      state.status node = NodeStatus.failed →
        (propagateFailure G state).status node = NodeStatus.failed := byν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ ∀ (node : ν), state.status node = NodeStatus.failed → (propagateFailure G state).status node = NodeStatus.failed
  intro node hFailedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadnode:νhFailed:state.status node = NodeStatus.failed⊢ (propagateFailure G state).status node = NodeStatus.failed
  exact propagateFailure_preserves_failed G state hFailedAll goals completed! 🐙

propagateStatus_monotone proves node-local failure propagation is monotone.

theorem propagateStatus_monotone
    (G : DAG ν)
    {left right : GraphState ν payload}
    (hLe : GraphState.failureLe left right)
    (node : ν) :
    NodeStatus.failureLe (propagateStatus G left node) (propagateStatus G right node) := byν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:ν⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
  classical
  by_cases hLeftClosed :
    NodeStatus.propagatable (left.status node) ∧ hasFailedAncestor G left nodeposν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left node⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)negν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
  ·posν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left node⊢ (propagateStatus G left node).failureLe (propagateStatus G right node) have hRightFailed : propagateStatus G right node = NodeStatus.failed := byν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:ν⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
      rcases hLe node with hSame | hFailureinlν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehSame:left.status node = right.status node⊢ propagateStatus G right node = NodeStatus.failedinrν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehFailure:(left.status node).propagatable ∧ right.status node = NodeStatus.failed⊢ propagateStatus G right node = NodeStatus.failed
      ·inlν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehSame:left.status node = right.status node⊢ propagateStatus G right node = NodeStatus.failed have hRightClosed :
          NodeStatus.propagatable (right.status node) ∧ hasFailedAncestor G right node := byν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:ν⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
          constructorleftν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehSame:left.status node = right.status node⊢ (right.status node).propagatablerightν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehSame:left.status node = right.status node⊢ hasFailedAncestor G right node
          ·leftν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehSame:left.status node = right.status node⊢ (right.status node).propagatable simpa [hSame] using hLeftClosed.1All goals completed! 🐙
          ·rightν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehSame:left.status node = right.status node⊢ hasFailedAncestor G right node exact hasFailedAncestor_monotone G hLe hLeftClosed.2All goals completed! 🐙
        simp [propagateStatus, hRightClosed]All goals completed! 🐙
      ·inrν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehFailure:(left.status node).propagatable ∧ right.status node = NodeStatus.failed⊢ propagateStatus G right node = NodeStatus.failed rcases hFailure with ⟨_hLeftPropagatable, hRightStatus⟩inrν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left node_hLeftPropagatable:(left.status node).propagatablehRightStatus:right.status node = NodeStatus.failed⊢ propagateStatus G right node = NodeStatus.failed
        simp [propagateStatus, hRightStatus, NodeStatus.propagatable]All goals completed! 🐙
    have hLeftFailed : propagateStatus G left node = NodeStatus.failed := byν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:ν⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
      simp [propagateStatus, hLeftClosed]All goals completed! 🐙
    rw [hLeftFailed, hRightFailed]posν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:(left.status node).propagatable ∧ hasFailedAncestor G left nodehRightFailed:propagateStatus G right node = NodeStatus.failedhLeftFailed:propagateStatus G left node = NodeStatus.failed⊢ NodeStatus.failed.failureLe NodeStatus.failed
    exact NodeStatus.failureLe_refl NodeStatus.failedAll goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)⊢ (propagateStatus G left node).failureLe (propagateStatus G right node) by_cases hRightClosed :
      NodeStatus.propagatable (right.status node) ∧ hasFailedAncestor G right nodeposν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)hRightClosed:(right.status node).propagatable ∧ hasFailedAncestor G right node⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)negν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)hRightClosed:¬((right.status node).propagatable ∧ hasFailedAncestor G right node)⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
    ·posν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)hRightClosed:(right.status node).propagatable ∧ hasFailedAncestor G right node⊢ (propagateStatus G left node).failureLe (propagateStatus G right node) have hLeftPropagatable :
          NodeStatus.propagatable (left.status node) :=
        NodeStatus.failureLe_reflects_propagatable (hLe node) hRightClosed.1posν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)hRightClosed:(right.status node).propagatable ∧ hasFailedAncestor G right nodehLeftPropagatable:(left.status node).propagatable⊢ (propagateStatus G left node).failureLe (propagateStatus G right node)
      simpa [propagateStatus, hLeftClosed, hRightClosed] using
        NodeStatus.failureLe_to_failed hLeftPropagatableAll goals completed! 🐙
    ·negν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:νhLeftClosed:¬((left.status node).propagatable ∧ hasFailedAncestor G left node)hRightClosed:¬((right.status node).propagatable ∧ hasFailedAncestor G right node)⊢ (propagateStatus G left node).failureLe (propagateStatus G right node) simpa [propagateStatus, hLeftClosed, hRightClosed] using hLe nodeAll goals completed! 🐙

propagateFailure_monotone proves failure closure is monotone over failure-growth.

theorem propagateFailure_monotone
    (G : DAG ν)
    {left right : GraphState ν payload}
    (hLe : GraphState.failureLe left right) :
    GraphState.failureLe (propagateFailure G left) (propagateFailure G right) := byν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe right⊢ (propagateFailure G left).failureLe (propagateFailure G right)
  intro nodeν:Type upayload:Type vG:DAG νleft:GraphState ν payloadright:GraphState ν payloadhLe:left.failureLe rightnode:ν⊢ ((propagateFailure G left).status node).failureLe ((propagateFailure G right).status node)
  exact propagateStatus_monotone G hLe nodeAll goals completed! 🐙

propagateFailure_failureClosureComplete proves propagation reaches closure.

theorem propagateFailure_failureClosureComplete
    (G : DAG ν)
    (state : GraphState ν payload) :
    failureClosureComplete G (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ failureClosureComplete G (propagateFailure G state)
  intro failedNode nodeν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:ν⊢ (propagateFailure G state).status failedNode = NodeStatus.failed →
  G.reaches failedNode node →
    ((propagateFailure G state).status node).propagatable → (propagateFailure G state).status node = NodeStatus.failed hFailedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failed⊢ G.reaches failedNode node →
  ((propagateFailure G state).status node).propagatable → (propagateFailure G state).status node = NodeStatus.failed hReachν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode node⊢ ((propagateFailure G state).status node).propagatable → (propagateFailure G state).status node = NodeStatus.failed hPropagatableν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehPropagatable:((propagateFailure G state).status node).propagatable⊢ (propagateFailure G state).status node = NodeStatus.failed
  have hAncestor : hasFailedAncestor G state node :=
    hasFailedAncestor_of_failed_after_reaches G state hFailed hReachν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehPropagatable:((propagateFailure G state).status node).propagatablehAncestor:hasFailedAncestor G state node⊢ (propagateFailure G state).status node = NodeStatus.failed
  have hOriginalPropagatable : NodeStatus.propagatable (state.status node) :=
    propagatable_of_propagate G state hPropagatableν:Type upayload:Type vG:DAG νstate:GraphState ν payloadfailedNode:νnode:νhFailed:(propagateFailure G state).status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehPropagatable:((propagateFailure G state).status node).propagatablehAncestor:hasFailedAncestor G state nodehOriginalPropagatable:(state.status node).propagatable⊢ (propagateFailure G state).status node = NodeStatus.failed
  exact propagateFailure_marks_failed_descendant G state hOriginalPropagatable hAncestorAll goals completed! 🐙

Normalization Preservation

propagateFailure_preserves_noRunning preserves the absence of running nodes.

theorem propagateFailure_preserves_noRunning
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNoRunning : GraphState.noRunningNodes state) :
    GraphState.noRunningNodes (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodes⊢ (propagateFailure G state).noRunningNodes
  classical
  intro nodeν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:ν⊢ (propagateFailure G state).status node ≠ NodeStatus.running
  by_cases hClosed :
    NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (propagateFailure G state).status node ≠ NodeStatus.runningnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (propagateFailure G state).status node ≠ NodeStatus.running
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (propagateFailure G state).status node ≠ NodeStatus.running intro hRunningposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehRunning:(propagateFailure G state).status node = NodeStatus.running⊢ False
    simp [propagateFailure, propagateStatus, hClosed] at hRunningAll goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoRunning:state.noRunningNodesnode:νhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (propagateFailure G state).status node ≠ NodeStatus.running simpa [propagateFailure, propagateStatus, hClosed] using hNoRunning nodeAll goals completed! 🐙

propagateFailure_preserves_noInterrupted preserves the absence of interrupted nodes.

theorem propagateFailure_preserves_noInterrupted
    (G : DAG ν)
    (state : GraphState ν payload)
    (hNoInterrupted : GraphState.noInterruptedNodes state) :
    GraphState.noInterruptedNodes (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodes⊢ (propagateFailure G state).noInterruptedNodes
  classical
  intro nodeν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodesnode:ν⊢ (propagateFailure G state).status node ≠ NodeStatus.interrupted
  by_cases hClosed :
    NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodesnode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (propagateFailure G state).status node ≠ NodeStatus.interruptednegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodesnode:νhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (propagateFailure G state).status node ≠ NodeStatus.interrupted
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodesnode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (propagateFailure G state).status node ≠ NodeStatus.interrupted intro hInterruptedposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodesnode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehInterrupted:(propagateFailure G state).status node = NodeStatus.interrupted⊢ False
    simp [propagateFailure, propagateStatus, hClosed] at hInterruptedAll goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhNoInterrupted:state.noInterruptedNodesnode:νhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (propagateFailure G state).status node ≠ NodeStatus.interrupted simpa [propagateFailure, propagateStatus, hClosed] using hNoInterrupted nodeAll goals completed! 🐙

propagateFailure_preserves_topologyDomain preserves off-topology absence.

theorem propagateFailure_preserves_topologyDomain
    (G : DAG ν)
    (state : GraphState ν payload)
    (hDomain : GraphState.topologyDomain G state) :
    GraphState.topologyDomain G (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ GraphState.topologyDomain G (propagateFailure G state)
  classical
  intro node hNotMemν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodes⊢ (propagateFailure G state).status node = NodeStatus.pending ∧ (propagateFailure G state).output node = none
  rcases hDomain node hNotMem with ⟨hStatus, hOutput⟩ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none⊢ (propagateFailure G state).status node = NodeStatus.pending ∧ (propagateFailure G state).output node = none
  have hNoAncestor : ¬ hasFailedAncestor G state node := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G state⊢ GraphState.topologyDomain G (propagateFailure G state)
    intro hAncestorν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = nonehAncestor:hasFailedAncestor G state node⊢ False
    rcases hAncestor with ⟨_failedNode, _hFailed, hReach⟩ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = none_failedNode:ν_hFailed:state.status _failedNode = NodeStatus.failedhReach:G.reaches _failedNode node⊢ False
    exact hNotMem (G.reaches_target_mem hReach)All goals completed! 🐙
  constructorleftν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = nonehNoAncestor:¬hasFailedAncestor G state node⊢ (propagateFailure G state).status node = NodeStatus.pendingrightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = nonehNoAncestor:¬hasFailedAncestor G state node⊢ (propagateFailure G state).output node = none
  ·leftν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = nonehNoAncestor:¬hasFailedAncestor G state node⊢ (propagateFailure G state).status node = NodeStatus.pending simp [propagateFailure, propagateStatus, hStatus, hNoAncestor]All goals completed! 🐙
  ·rightν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhDomain:GraphState.topologyDomain G statenode:νhNotMem:node ∉ G.nodeshStatus:state.status node = NodeStatus.pendinghOutput:state.output node = nonehNoAncestor:¬hasFailedAncestor G state node⊢ (propagateFailure G state).output node = none simpa [propagateFailure] using hOutputAll goals completed! 🐙

propagateFailure_preserves_outputsRespectStatuses preserves output ownership.

theorem propagateFailure_preserves_outputsRespectStatuses
    (G : DAG ν)
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsRespectStatuses state) :
    GraphState.outputsRespectStatuses (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatuses⊢ (propagateFailure G state).outputsRespectStatuses
  classical
  intro node valueν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payload⊢ (propagateFailure G state).output node = some value → ((propagateFailure G state).status node).mayHaveOutput hOutputν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some value⊢ ((propagateFailure G state).status node).mayHaveOutput
  by_cases hClosed :
    NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ ((propagateFailure G state).status node).mayHaveOutputnegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ ((propagateFailure G state).status node).mayHaveOutput
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ ((propagateFailure G state).status node).mayHaveOutput have hMayHaveOutput : NodeStatus.mayHaveOutput (state.status node) :=
      hOutputs node value hOutputposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutput⊢ ((propagateFailure G state).status node).mayHaveOutput
    cases hStatus : state.status nodepos.pendingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.pending⊢ ((propagateFailure G state).status node).mayHaveOutputpos.runningν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.running⊢ ((propagateFailure G state).status node).mayHaveOutputpos.completedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.completed⊢ ((propagateFailure G state).status node).mayHaveOutputpos.failedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.failed⊢ ((propagateFailure G state).status node).mayHaveOutputpos.skippedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.skipped⊢ ((propagateFailure G state).status node).mayHaveOutputpos.interruptedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.interrupted⊢ ((propagateFailure G state).status node).mayHaveOutputpos.waitingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.waiting⊢ ((propagateFailure G state).status node).mayHaveOutputpos.rewrittenν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.rewritten⊢ ((propagateFailure G state).status node).mayHaveOutput <;>pos.pendingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.pending⊢ ((propagateFailure G state).status node).mayHaveOutputpos.runningν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.running⊢ ((propagateFailure G state).status node).mayHaveOutputpos.completedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.completed⊢ ((propagateFailure G state).status node).mayHaveOutputpos.failedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.failed⊢ ((propagateFailure G state).status node).mayHaveOutputpos.skippedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.skipped⊢ ((propagateFailure G state).status node).mayHaveOutputpos.interruptedν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.interrupted⊢ ((propagateFailure G state).status node).mayHaveOutputpos.waitingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.waiting⊢ ((propagateFailure G state).status node).mayHaveOutputpos.rewrittenν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodehMayHaveOutput:(state.status node).mayHaveOutputhStatus:state.status node = NodeStatus.rewritten⊢ ((propagateFailure G state).status node).mayHaveOutput
      simp
        [ NodeStatus.propagatable
        , NodeStatus.mayHaveOutput
        , hClosed
        , hStatus
        ] at hClosed hMayHaveOutput ⊢All goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsRespectStatusesnode:νvalue:payloadhOutput:(propagateFailure G state).output node = some valuehClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ ((propagateFailure G state).status node).mayHaveOutput simpa [propagateFailure, propagateStatus, hClosed] using hOutputs node value hOutputAll goals completed! 🐙

propagateFailure_preserves_outputsCompleteForStatuses preserves required outputs.

theorem propagateFailure_preserves_outputsCompleteForStatuses
    (G : DAG ν)
    (state : GraphState ν payload)
    (hOutputs : GraphState.outputsCompleteForStatuses state) :
    GraphState.outputsCompleteForStatuses (propagateFailure G state) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuses⊢ (propagateFailure G state).outputsCompleteForStatuses
  classical
  intro node hRequiresOutputν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutput⊢ ∃ value, (propagateFailure G state).output node = some value
  by_cases hClosed :
    NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutputhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ ∃ value, (propagateFailure G state).output node = some valuenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutputhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ ∃ value, (propagateFailure G state).output node = some value
  ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutputhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ ∃ value, (propagateFailure G state).output node = some value simp
      [ propagateFailure
      , propagateStatus
      , NodeStatus.requiresOutput
      , hClosed
      ] at hRequiresOutputAll goals completed! 🐙
  ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutputhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ ∃ value, (propagateFailure G state).output node = some value have hOriginalRequires :
        NodeStatus.requiresOutput (state.status node) := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatuses⊢ (propagateFailure G state).outputsCompleteForStatuses
      simpa [propagateFailure, propagateStatus, hClosed] using hRequiresOutputAll goals completed! 🐙
    rcases hOutputs node hOriginalRequires with ⟨value, hOutput⟩negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutputhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)hOriginalRequires:(state.status node).requiresOutputvalue:payloadhOutput:state.output node = some value⊢ ∃ value, (propagateFailure G state).output node = some value
    exact ⟨value, byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhOutputs:state.outputsCompleteForStatusesnode:νhRequiresOutput:((propagateFailure G state).status node).requiresOutputhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)hOriginalRequires:(state.status node).requiresOutputvalue:payloadhOutput:state.output node = some value⊢ (propagateFailure G state).output node = some value simpa [propagateFailure] using hOutputAll goals completed! 🐙⟩

Idempotence

propagateFailure_of_failureClosureComplete makes failure-closed states fixed points.

theorem propagateFailure_of_failureClosureComplete
    (G : DAG ν)
    (state : GraphState ν payload)
    (hComplete : failureClosureComplete G state) :
    propagateFailure G state = state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G state⊢ propagateFailure G state = state
  classical
  ext nodehStatusν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:ν⊢ (propagateFailure G state).status node = state.status nodehOutput.aν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νa✝:payload⊢ (propagateFailure G state).output node = some a✝ ↔ state.output node = some a✝
  ·hStatusν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:ν⊢ (propagateFailure G state).status node = state.status node by_cases hClosed :
      NodeStatus.propagatable (state.status node) ∧ hasFailedAncestor G state nodeposν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (propagateFailure G state).status node = state.status nodenegν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (propagateFailure G state).status node = state.status node
    ·posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state node⊢ (propagateFailure G state).status node = state.status node rcases hClosed.2 with ⟨failedNode, hFailed, hReach⟩posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodefailedNode:νhFailed:state.status failedNode = NodeStatus.failedhReach:G.reaches failedNode node⊢ (propagateFailure G state).status node = state.status node
      have hNodeFailed : state.status node = NodeStatus.failed :=
        hComplete failedNode node hFailed hReach hClosed.1posν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νhClosed:(state.status node).propagatable ∧ hasFailedAncestor G state nodefailedNode:νhFailed:state.status failedNode = NodeStatus.failedhReach:G.reaches failedNode nodehNodeFailed:state.status node = NodeStatus.failed⊢ (propagateFailure G state).status node = state.status node
      simp [propagateFailure, propagateStatus, hClosed, hNodeFailed]All goals completed! 🐙
    ·negν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νhClosed:¬((state.status node).propagatable ∧ hasFailedAncestor G state node)⊢ (propagateFailure G state).status node = state.status node simp [propagateFailure, propagateStatus, hClosed]All goals completed! 🐙
  ·hOutput.aν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhComplete:failureClosureComplete G statenode:νa✝:payload⊢ (propagateFailure G state).output node = some a✝ ↔ state.output node = some a✝ simp [propagateFailure]All goals completed! 🐙

propagateFailure_idempotent proves failure propagation is idempotent.

theorem propagateFailure_idempotent
    (G : DAG ν)
    (state : GraphState ν payload) :
    propagateFailure G (propagateFailure G state) = propagateFailure G state := byν:Type upayload:Type vG:DAG νstate:GraphState ν payload⊢ propagateFailure G (propagateFailure G state) = propagateFailure G state
  exact
    propagateFailure_of_failureClosureComplete
      G
      (propagateFailure G state)
      (propagateFailure_failureClosureComplete G state)All goals completed! 🐙

end Cortex.Pulse

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Pulse.Classify Next →Cortex.Pulse.DAG