AdeAtlas
Invariants / DC-EPOCH-07

DC-EPOCH-07

DC derived enforced

A missing / stale / conflicting / mismatched candidate view causes TERMINAL fail-closed behaviour, NEVER fallback consensus (S3f-4b). The activation predicate (activation_predicate) is the only gate: Promote requires transition-eligible AND bindings-verify AND selected-point-correct AND wal-durable, in that order; any failure is NoPromotion(ActivationReject) -- the seed view simply stays authoritative on its seed-epoch path (no flag, no fallback to an epoch-WRONG view past the boundary). The terminal states are EpochViewActivationError{EpochViewActivationFailed (WAL not durable -> halt before promotion), EpochViewActivationConflict (a conflicting activation for the target epoch -> halt), EpochViewPostPromotionMismatch (the active view != the WAL record after publication -> halt)}. Falling back to the seed view past the boundary is forbidden because it is known epoch-wrong and header validation / follow could then observe stale inputs.

Source

docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-3f4-activation-flip.md (S3f-4b); user directive 2026-06-21 (halt on activation failure or mismatch; no seed-view fallback)

Introduced in
EPOCH-CONSENSUS-VIEW-S3f-4b

Enforcement trace

Code

Tests 3

  • predicate_promotes_only_when_every_precondition_holds
  • predicate_rejects_each_failed_precondition
  • active_view_conflicting_promotion_is_terminal

CI 1

Cross-references

DC-EPOCH-04DC-EPOCH-05DC-EVIEW-11DC-EPOCH-03

Attack rationale

A failed/conflicting/mismatched activation must HALT, never silently continue on the epoch-wrong seed view. The predicate is conjunctive (every precondition required) and ordered, so a partial/unverified/non-durable candidate yields NoPromotion -- the seed stays on its own epoch path (correct pre-boundary), and the live wiring (S3f-4c/d) turns a durability/post-promotion failure into a terminal EpochViewActivation* state, not a fallback. 'No leadership' alone is insufficient past the boundary (header validation/follow could read stale inputs), so the outcome is a structured terminal halt.

Evidence notes

Introduced at EPOCH-CONSENSUS-VIEW S3f-4b (2026-06-21). The predicate + terminal-state types only -- 3 hermetic tests + the gate. cargo test -p ade_node --lib (epoch_activation 5) green. The live HALT wiring (returning the terminal states on WAL failure / post-promotion mismatch) is S3f-4c/d, gated on the live proofs. Next: S3f-4c (durable-before-visible + replay application + crash recovery).