AdeAtlas
Invariants / DC-EVIDENCE-04

DC-EVIDENCE-04

DC derived enforced

Closed fork-choice convergence evidence (PHASE4-N-AO S9; promotes the live SELECT proof from stderr diagnostics to registry-grade evidence). The live multi-candidate SELECT path emits a CLOSED, observe-only convergence-evidence sequence proving the WHOLE path: needs_fork_choice -> lca_discovered -> candidate_fragment_built -> fork_choice_selected -> branch_fetch_started -> branch_fetch_completed -> branch_prevalidated -> fork_switch_applied | fork_switch_failed | fork_switch_superseded. The 10 event discriminators EQUAL the emit-only allow-list (an unknown/added variant fails closed at the allow-list test, the NodeSchedEvent pattern); every field is bounded + typed (no free-form error strings -- failure_code is a closed enum mapping BranchProofError/LcaError; fork_switch_id is a bounded deterministic id = blake2b(winning_peer || fork_anchor.slot || fork_anchor.hash || winner_tip.slot || winner_tip.hash) hex-prefix, never free-form text). For a given fork_switch_id, a fork_choice_selected{result=win} is followed by EXACTLY ONE terminal event (fork_switch_applied OR fork_switch_failed OR fork_switch_superseded -- the last when a newer win on the same fork overwrites this provisional pending before the relay loop applies it) -- never zero, never two, never dangling. The evidence OBSERVES already-computed authority outcomes: NO evidence event/type is ever consumed by select_best_chain / walk_to_durable_lca / apply_fork_switch / the forge fence, and a transcript write failure (flips incomplete, DC-EVIDENCE-01) cannot alter selection / apply / fence behavior. CN-CONS-03 flips ONLY when a committed two-producer transcript passes the refined bounded post-switch window (S10): the hard fork-switch proof (both-peer block_received -> the SELECT middle -> fork_switch_applied{rollback_reason=ForkChoiceWin} at X -> block_admitted X) then PostSwitchContinuity::ContinuesSelectedBranch within the bounded window with a terminal of agreement_verdict{agreed, our_hash==peer_hash} at X-or-descendant OR a validated-prefix-of-peer (continuity holds + peer observed ahead), 0 diverged -- never on stderr diagnostics, and never on a lucky exact-tip moment (see DC-EVIDENCE-05 for the replayable continuity verdict the terminal is derived from).

Source

docs/planning/phase4-n-ao-ce-ao-6-live-gap.md (S9 evidence finding) + docs/clusters/PHASE4-N-AO/S9-closed-fork-choice-evidence.md

Introduced in
PHASE4-N-AO

Enforcement trace

Code

Tests 4

  • fork_choice_win_paired_with_exactly_one_terminal_applied
  • fork_choice_win_failed_terminal_carries_closed_code
  • superseded_win_pairs_to_superseded_terminal
  • fork_switch_id_is_deterministic_and_bounded

CI 1

Cross-references

DC-EVIDENCE-01DC-EVIDENCE-02DC-EVIDENCE-03DC-NODE-34DC-NODE-36DC-NODE-37DC-NODE-38CN-CONS-01CN-CONS-03

Attack rationale

Without closed-vocabulary evidence for the SELECT middle, a CN-CONS-03 flip would rest on stderr diagnostics + a transcript that only proves the beginning (block_received) and end (agreement) -- leaving the actual fork-choice (did Ade DISCOVER the LCA, SELECT a winner, FETCH+PREVALIDATE the branch, and APPLY the fork-switch, or did it merely follow a single peer?) unaudited. A decide-only transcript leaves the same ambiguity: selected vs applied. The fork_switch_id win->terminal pairing forces every WIN to resolve to a durable apply or a structured failure, so agreement{agreed} only supports the invariant when the winning branch was actually adopted. Closed discriminants + an emit-only allow-list + no free-form strings keep the evidence from silently widening or smuggling unaudited claims; observe-only containment keeps the evidence from ever becoming authority (a write failure must never alter selection/apply).

Evidence notes

Declared at PHASE4-N-AO S9. The 2026-06-12 diverged live run informally proved the mechanism (both peers delivered, S7 LCA walk resolved forks of depth 1-7 at the durable anchor, 7 fork-choice WINs, agreed exact-hash, 0 diverged, no UnexpectedRollback) but via temporary FCDIAG stderr markers (reverted) -- NOT registry-grade. Enforced at S9 close (CE-AO-10) via ci_check_fork_choice_evidence_closed.sh + hermetic tests (vocabulary==allow-list negative test, closed-typed-fields, win-paired-with-exactly-one-terminal-by-fork_switch_id, observe-only containment, field-presence). The live CE-AO-6 flip of CN-CONS-03 is gated on a committed two-producer transcript that passes the refined BOUNDED, BRANCH-BOUND post-switch convergence window (ci/ci_check_post_switch_convergence_window.sh -- RELEASE/evidence-tier, NO BLUE change; S10/DC-EVIDENCE-05): the hard fork-switch proof (fork_choice_selected{win} -> branch_fetch_* -> branch_prevalidated -> fork_switch_applied{ForkChoiceWin} at X -> block_admitted X) then PostSwitchContinuity::ContinuesSelectedBranch within a bounded window (max_slots=200, max_admitted_blocks=20, fixed up front) -- unbroken prev_hash lineage from X across every post-X block_admitted, no diverged, every win terminal -- with a convergence terminal of agreement_verdict{agreed,our==peer} at X-or-descendant OR a validated-prefix-of-peer (continuity holds + an in-window lagging with peer_slot>our_slot). This proves Ade switched, STAYED on the adopted valid branch, and did not diverge while catching up -- a real correctness property, not a lucky exact-tip moment or a frozen venue. RATIONALE for moving off exact-tip: a clean healthy follow run emits ONLY lagging (the solo producer never pauses for the follower to touch its exact tip), so exact-tip agreement is a test-harness artifact. The bounds + terminal are an evidence-ACCEPTANCE rule only; the continuity verdict reads ONLY Ade's own admitted-block lineage (peer tip never an input); consensus authority (select_best_chain, S4 prevalidate-before-commit, pump_block admit, WAL ForkChoiceWin, replay) is unchanged.