Invariants / DC-EVIEW-06

DC-EVIEW-06

DC derived enforced

Snapshot formation + the k-immutability stability gate (S3d). form_mark_snapshot converts the S3c per-pool aggregate (StakeByPool) into the MARK StakeSnapshot's pool_stakes (the value leader election consumes). The mark/set/go rotation already exists (epoch::rotate_snapshots: mark<-new_mark, set<-old mark, go<-old set), encoding the lag -- leader election for epoch L reads the SET snapshot (the MARK captured at the previous boundary), a 2-epoch lag (LEADERSHIP_SNAPSHOT_PHASE = Set); GO drives rewards (3-epoch). S3d ADDS the STABILITY GATE Ade lacked: a boundary snapshot/view is FINALIZABLE (usable) ONLY once its boundary block is STRICTLY more than k (the SecurityParam, 2160) deep -- is_boundary_stable(boundary, tip, k) = (tip - boundary) > k (saturating; a boundary ahead of the tip is never stable). A boundary not yet > k deep can still be rolled back (DC-NODE-29), so a snapshot derived from it must NOT be used; cardano forces the lazy MARK only after one stability window for exactly this reason. Pure, total, deterministic. OBSERVE-ONLY: not wired to live leader election or the boundary authority (DC-EVIEW-08 activation); no live-path change.

Source

docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-3-scope.md (S3d); docs/clusters/EPOCH-CONSENSUS-VIEW/EPOCH-CONSENSUS-VIEW-design-analysis.md (Deliverable 4)

Introduced in
EPOCH-CONSENSUS-VIEW-S3d

Enforcement trace

Tests 5

  • forms_mark_snapshot_from_aggregate
  • stability_gate_requires_more_than_k_deep
  • boundary_ahead_of_tip_is_not_stable
  • leadership_reads_the_set_snapshot
  • formed_mark_rotates_into_set

Cross-references

Attack rationale

The stability gate must (a) require STRICTLY > k depth -- a boundary exactly k deep is NOT yet stable (a snapshot finalized at the k-boundary could be invalidated by a maximal honest rollback -> a leader schedule built on rolled-back stake); the test pins k-not-stable / (k+1)-stable; (b) saturate so a boundary ahead of the tip (degenerate / pre-genesis) is never stable, never a wrapped huge depth; and (c) name the SET snapshot as the leadership phase (the 2-epoch lag) -- reading MARK (not yet stable) or the wrong phase would use unsettled or mis-aged stake. Observe-only: the gate is not yet consulted by live leader election (that is DC-EVIEW-08), so no live decision depends on it until activation, when it fences finalization of the EpochConsensusView.

Evidence notes

Introduced at EPOCH-CONSENSUS-VIEW S3d (2026-06-20). The genuinely-new piece is the k-immutability stability gate (the grounding flagged it ABSENT in Ade -- mark/set/go rotation existed but no finality gate). Pure BLUE, observe-only. 5 hermetic tests (mark formation from the aggregate, the stability boundary k-vs-k+1, boundary-ahead-of-tip saturating, leadership-reads-SET, formed-mark-rotates-into-set). Reuses epoch::rotate_snapshots + SecurityParam (the same k the rollback authority DC-NODE-29 uses). cargo test -p ade_ledger green. NO emission (S3e), NO live wiring, NO leader/header use. Next: S3e (EpochConsensusView emission/binding, observe-only -- bind the formed+stable snapshot to network/era/epoch/point/checkpoint/nonce/phase/canonical-hash), then DC-EVIEW-08 (the ONLY activation slice: rewire new_mark to the aggregate, consult the stability gate, feed the bound view to live leader election, the differential oracle + leadership-schedule live proof).