Invariants / DC-EPOCH-06

DC-EPOCH-06

DC derived enforced

Activation is durable-before-visible and replay-identical (S3f-4c). The activation WAL record (EpochConsensusViewActivated) is written and made durable BEFORE the active view is published: activate_durable_before_visible publishes Promoted(view) ONLY when the WAL write is durable; a non-durable write is the terminal EpochViewActivationFailed (halt before promotion), never a publish. Recovery is replay-identical: recover_active_view(record, candidate) returns Seed when there is NO durable activation record (crash before the WAL: the old epoch stays active); Promoted(candidate) when a record exists AND the re-derived candidate reproduces its ENTIRE identity -- every binding + the stake-view hash + the full-view hash + verify_canonical_hash, via activation_record_matches -- so the recovered active view equals the WAL record (crash after the WAL or after publication); and the terminal EpochViewPostPromotionMismatch when a record exists but the candidate mismatches or cannot be re-derived (NEVER a fallback to the epoch-wrong seed view). resolve_activation_record folds repeated records via the DC-EPOCH-04 idempotence/conflict rule (same epoch byte-identical => keep; differing => terminal conflict; a different epoch => the later supersedes).

Source

docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-3f4-activation-flip.md (S3f-4c); user directive 2026-06-21 (durable-before-visible; crash before/after WAL; recovered must match WAL)

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

Enforcement trace

Tests 5

  • crash_before_durable_wal_keeps_seed
  • crash_after_wal_republishes_same_view
  • recovered_view_mismatch_is_terminal
  • durable_before_visible_halts_on_wal_failure
  • resolve_activation_idempotent_conflict_supersede

Cross-references

Attack rationale

The active view must never become visible before its activation is durable (else a crash loses the promotion while leadership already acted on it): activate_durable_before_visible gates publication on wal_write_durable and halts (terminal) otherwise. Recovery must reproduce EXACTLY the activated view: activation_record_matches requires the re-derived candidate to reproduce every binding + the stake-view hash + the full-view hash AND self-verify, so a divergent re-derivation is a terminal PostPromotionMismatch, not a silent acceptance. No durable record => Seed (the old epoch), which is correct (the promotion never committed). A record with a non-re-derivable or mismatched candidate is terminal, NEVER a fallback to the epoch-wrong seed. Repeated records fold deterministically (DC-EPOCH-04), so replay is idempotent or fails closed -- never two different active views.

Evidence notes

Introduced at EPOCH-CONSENSUS-VIEW S3f-4c (2026-06-21), the third sub-slice of the activation flip. The PURE ordering + recovery logic -- 5 hermetic proofs (crash before WAL -> Seed; crash after WAL -> republish same view; mismatch/absent -> terminal; durable-before-visible halts on WAL failure; resolve idempotent/conflict/supersede) + ci_check_eview_activation_recovery.sh. cargo test -p ade_node --lib (epoch_activation 10) green. The LIVE orchestration (write WAL durably then publish; warm-start re-derive + recover) is S3f-4d, gated on the live proofs. Next: S3f-4d (the live flip) -- the ONLY remaining sub-slice, gated on the boundary-aligned stake oracle + the leadership-schedule proof.