Cortex.Pulse.Validity

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. Frontier Bridge
  5. Recovered-State Validity
Imports
import Cortex.Pulse.Closure

Overview

The Paper 1 recovery claim depends on a named validity predicate rather than a prose bundle of assumptions. This module collects the parts of that predicate that are already mechanized in the fixed-topology kernel.

Context

Validity is intentionally small at this stage. Domain exactness is carried by the finite DAG node set, payload semantics remain abstract, and this page packages the structural invariants that recovery can prove today.

Theorem Split

The page first records the bridge between proof-level and executable frontiers, then combines topology-domain, output, volatile-state, closure, causal-history, and frontier obligations into wellFormedGraphState.

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

Frontier Bridge

frontierBridge G state says proof and runtime frontiers coincide.

def frontierBridge (G : DAG ν) (state : GraphState ν payload) : Prop := readyNodes G state = directReadyNodes G state

directReady_sound proves executable-direct readiness implies proof readiness.

theorem directReady_sound (G : DAG ν) (state : GraphState ν payload) (hCausal : CausalHistoryClosed G state) : ∀ node : ν, DirectReady G state node → Ready G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G state⊢ ∀ (node : ν), DirectReady G state node → Ready G state node intro node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhCausal:CausalHistoryClosed G statenode:νhDirect:DirectReady G state node⊢ Ready G state node All goals completed! 🐙

ready_directReady_of_failureClosureComplete proves proof readiness is executable.

theorem ready_directReady_of_failureClosureComplete (G : DAG ν) (state : GraphState ν payload) (hClosure : failureClosureComplete G state) : ∀ node : ν, Ready G state node → DirectReady G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G state⊢ ∀ (node : ν), Ready G state node → DirectReady G state node intro node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ DirectReady G state node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ node ∈ G.nodesν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ state.status node = NodeStatus.pending ∧ ∀ (predecessor : ν), G.predecessor predecessor node → (state.status predecessor).unblocksSuccessors ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ node ∈ G.nodes All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ state.status node = NodeStatus.pendingν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ ∀ (predecessor : ν), G.predecessor predecessor node → (state.status predecessor).unblocksSuccessors ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ state.status node = NodeStatus.pending All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state node⊢ ∀ (predecessor : ν), G.predecessor predecessor node → (state.status predecessor).unblocksSuccessors intro predecessor ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state nodepredecessor:νhEdge:G.predecessor predecessor node⊢ (state.status predecessor).unblocksSuccessors ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state nodepredecessor:νhEdge:G.predecessor predecessor nodehReach:G.reaches predecessor node⊢ (state.status predecessor).unblocksSuccessors ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state nodepredecessor:νhEdge:G.predecessor predecessor nodehReach:G.reaches predecessor nodehTerminal:(state.status predecessor).terminal⊢ (state.status predecessor).unblocksSuccessors have hNotFailed : state.status predecessor ≠ NodeStatus.failed := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G state⊢ ∀ (node : ν), Ready G state node → DirectReady G state node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state nodepredecessor:νhEdge:G.predecessor predecessor nodehReach:G.reaches predecessor nodehTerminal:(state.status predecessor).terminalhFailed:state.status predecessor = NodeStatus.failed⊢ False have hNodeFailed : state.status node = NodeStatus.failed := hClosure predecessor node hFailed hReach (ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state nodepredecessor:νhEdge:G.predecessor predecessor nodehReach:G.reaches predecessor nodehTerminal:(state.status predecessor).terminalhFailed:state.status predecessor = NodeStatus.failed⊢ (state.status node).propagatable All goals completed! 🐙) ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statenode:νhReady:Ready G state nodepredecessor:νhEdge:G.predecessor predecessor nodehReach:G.reaches predecessor nodehTerminal:(state.status predecessor).terminalhFailed:state.status predecessor = NodeStatus.failedhNodeFailed:NodeStatus.pending = NodeStatus.failed⊢ False All goals completed! 🐙 All goals completed! 🐙

ready_iff_directReady_of_closed_causal bridges proof and runtime readiness.

theorem ready_iff_directReady_of_closed_causal (G : DAG ν) (state : GraphState ν payload) (hClosure : failureClosureComplete G state) (hCausal : CausalHistoryClosed G state) (node : ν) : Ready G state node ↔ DirectReady G state node := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ Ready G state node ↔ DirectReady G state node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ Ready G state node → DirectReady G state nodeν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ DirectReady G state node → Ready G state node ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ Ready G state node → DirectReady G state node All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ DirectReady G state node → Ready G state node All goals completed! 🐙

readyNodes_eq_directReadyNodes connects the proof frontier to the runtime frontier.

theorem readyNodes_eq_directReadyNodes (G : DAG ν) (state : GraphState ν payload) (hClosure : failureClosureComplete G state) (hCausal : CausalHistoryClosed G state) : readyNodes G state = directReadyNodes G state := ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G state⊢ readyNodes G state = directReadyNodes G state classical ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ node ∈ readyNodes G state ↔ node ∈ directReadyNodes G state ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ node ∈ readyNodes G state → node ∈ directReadyNodes G stateν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ node ∈ directReadyNodes G state → node ∈ readyNodes G state ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ node ∈ readyNodes G state → node ∈ directReadyNodes G state ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:νhNode:node ∈ readyNodes G state⊢ node ∈ directReadyNodes G state ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:νhNode:node ∈ readyNodes G statehMem:node ∈ G.nodeshReady:Ready G state node⊢ node ∈ directReadyNodes G state All goals completed! 🐙 ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:ν⊢ node ∈ directReadyNodes G state → node ∈ readyNodes G state ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:νhNode:node ∈ directReadyNodes G state⊢ node ∈ readyNodes G state ν:Type upayload:Type vG:DAG νstate:GraphState ν payloadhClosure:failureClosureComplete G statehCausal:CausalHistoryClosed G statenode:νhNode:node ∈ directReadyNodes G statehMem:node ∈ G.nodeshDirect:DirectReady G state node⊢ node ∈ readyNodes G state All goals completed! 🐙

frontierBridge_of_closed_causal packages the non-trivial frontier bridge.

theorem frontierBridge_of_closed_causal (G : DAG ν) (state : GraphState ν payload) (hClosure : failureClosureComplete G state) (hCausal : CausalHistoryClosed G state) : frontierBridge G state := readyNodes_eq_directReadyNodes G state hClosure hCausal

Recovered-State Validity

WellFormedGraphState G state is validity for normalized recovered graph states.

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

Persisted status/output maps mention only topology nodes.

topologyDomain : GraphState.topologyDomain G state

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

outputsRespectStatuses : GraphState.outputsRespectStatuses state

Payload-owning statuses have their required outputs present.

outputsCompleteForStatuses : GraphState.outputsCompleteForStatuses state

Recovery normalization removes in-flight running nodes.

noRunningNodes : GraphState.noRunningNodes state

Recovery normalization removes interrupted nodes.

noInterruptedNodes : GraphState.noInterruptedNodes state

Failed nodes have propagated through reachable propagatable descendants.

failureClosureComplete : failureClosureComplete G state

Successor-unblocking nodes have terminal strict ancestors.

causalHistoryClosed : CausalHistoryClosed G state

Proof-level and runtime-style frontiers coincide.

frontierBridge : frontierBridge G state

wellFormedGraphState G state keeps the published predicate name stable.

abbrev wellFormedGraphState (G : DAG ν) (state : GraphState ν payload) : Prop := WellFormedGraphState G stateend Cortex.Pulse