AdeAtlas
Invariants / DC-EVIEW-13

DC-EVIEW-13

DC derived enforced

Cardano-faithful pool lifecycle in the reduced window (ECA-0a). The cert-state pool lifecycle matches cardano-ledger (Pool.hs/PoolReap.hs/Epoch.hs/SnapShots.hs @ 226b002d) so a windowed replay reproduces the mark snapshot's pool set + VRF keys byte-faithfully: (1) PoolState gains future_pools (psFutureStakePoolParams); apply_pool_registration STAGES a re-registration of an already-registered pool into future_pools -- the active pools entry AND its VRF are UNCHANGED until adoption (a first registration still inserts into pools immediately) -- and cancels a pending retirement. (2) apply_pool_reap (POOLREAP, over the whole CertState) adopts future_pools into pools (dropping an orphan future with no active pool, Map.dropMissing), reaps pools with retiring == entered_epoch, CLEARS the delegations targeting reaped pools (removeStakePoolDelegations -- a credential delegated to a reaped pool is un-delegated so it cannot silently reattach if that pool id re-registers later; the credential's registration + reward account are preserved), and removes the reaped pools from pools + retiring. (3) drive_window_consensus_inputs applies apply_pool_reap at EACH epoch boundary crossed within the replayed block range (slot/slots_per_epoch) and surfaces the window-end {stake, pool_params} -- the MARK, captured BEFORE any further reap (SNAP precedes POOLREAP, Epoch.hs:292-297). Pure + deterministic (replay-equivalent). A re-registration's new VRF governs leadership one epoch later, never the current mark.

Source

docs/clusters/EPOCH-CONSENSUS-VIEW/SLICE-ECA-0a-pool-lifecycle-fidelity.md; user directive 2026-06-21 (correctness-first, no narrow shortcut; delegation-clearing NOT deferred)

Introduced in
EPOCH-CONTINUITY-ACTIVATION-ECA-0a

Enforcement trace

Code

Tests 7

  • re_registration_keeps_old_vrf_until_reap
  • pool_re_registration_stages_params_adopted_at_reap
  • reaped_pool_delegation_cleared_no_silent_reattach_on_reregistration
  • pool_reap_reaps_matching_epoch_only
  • drive_boundary_adopts_futures_reaps_retiring_clears_delegations
  • drive_boundary_is_deterministic
  • cert_state_round_trip_populated

CI 1

Cross-references

DC-EVIEW-10DC-EVIEW-07DC-EVIEW-05DC-EVIEW-09

Attack rationale

The candidate's pool set + VRF keys must match cardano's mark byte-faithfully or Ade diverges (rejects a valid pool's blocks / leads with the wrong identity). The three faithfulness risks are closed: (a) a re-registration must NOT change the active VRF until the boundary -- apply_pool_registration stages to future_pools (the contains_key branch; re_registration_keeps_old_vrf_until_reap proves the active VRF stays old until apply_pool_reap), so the mark carries the old VRF as cardano does, and the new VRF governs +1 epoch later; (b) a credential delegated to a reaped pool must NOT silently reattach if that pool id re-registers -- apply_pool_reap clears its delegation (reaped_pool_delegation_cleared_no_silent_reattach_on_reregistration), the delayed-divergence the user flagged; (c) the boundary POOLREAP must run at EACH crossed epoch (adopt + reap + clear) and the mark must be captured BEFORE the window-end reap -- drive_window_consensus_inputs applies apply_pool_reap per crossed boundary and aggregates after the last block (drive_boundary_adopts_futures_reaps_retiring_clears_delegations). Pure/deterministic (drive_boundary_is_deterministic), so a reorg re-materialize re-derives the same mark. apply_pool_reap drops an orphan future (Map.dropMissing) -- faithful + defensive even though future_pools subset pools holds by construction.

Evidence notes

Introduced at EPOCH-CONTINUITY-ACTIVATION ECA-0a (2026-06-21), the lifecycle-fidelity prerequisite for the leadership-complete view (ECA-0b, DC-EVIEW-12). Grounded in direct reads of cardano-ledger @ 226b002d: Pool.hs:266-310 (RegPool new-vs-reregister staging + retiring cancel), PoolReap.hs:151-241 (adopt futures / reap == e / clear delegators delegsToClear+removeStakePoolDelegations), Epoch.hs:292-297 (SNAP before POOLREAP), SnapShots.hs:425,449-462 (mark reads psStakePools only + numDelegators>0). 7 hermetic proofs (4 lifecycle in delegation.rs + 2 boundary-driver in reduced_window_driver.rs + the 6-field codec round-trip) + ci_check_eview_pool_lifecycle.sh; ade_ledger 637 lib + ade_runtime + ade_node 364 lib + ade_testkit all green (full affected-crate suites exit 0). User-directed correctness-first (no narrow 0b shortcut; delegation-clearing NOT deferred -- a stale delegation reattaching on pool-id re-registration is a delayed divergence). Strengthens DC-EVIEW-10 (the window driver now applies boundary POOLREAP via drive_window_consensus_inputs; drive_window_aggregate is a per-block wrapper). Next: ECA-0b (freeze pool_params VRF + protocol_params_commitment into EpochConsensusView -> DC-EVIEW-12 + DC-EPOCH-12).