AdeAtlas
Invariants / DC-EVIEW-05

DC-EVIEW-05

DC derived enforced drift

Per-pool stake aggregation (S3c, the linchpin). aggregate_pool_stake computes the next-epoch per-pool active stake from the single ledger authority's own projection: the reduced checkpoint's per-base-credential UTxO coin sums (ReducedUtxoCheckpoint::sum_base_credential_stake -- folds ONLY ReducedStakeRef::Base entries; NonContributing is skipped) and the delegation map + reward balances (DelegationState, accumulated by the window's advance_cert_state via the ledger's own process_block_certificates). The cardano-ledger snapshot rule, Conway-specialized: iterate the REGISTERED+DELEGATED credentials (the delegations map -- an unregistered credential cannot delegate), and for each, active stake = sum(its base-address UTxO coin) + its reward-account balance, accumulated into its delegated pool; a credential with UTxO but no delegation contributes nothing; a delegated credential with a reward balance but no UTxO still contributes (Conway); a pool with >=1 delegator is INCLUDED even at 0 stake (ECA-0b: cardano numDelegators>0, count-not-amount, so the derived pool SET matches cardano's PoolDistr, not merely the likely-leader outcome); total_active_stake = the sum over pools. Pure, total, deterministic, FAIL-CLOSED on overflow (AggregateError::StakeOverflow via checked_add -- never a silently wrapped stake total; unreachable under the max-supply bound). OBSERVE-ONLY: the rewire of apply_epoch_boundary's new_mark stub (rules.rs:1098) to consume this aggregate, and feeding it to live leader election, are the activation slice (DC-EVIEW-08) -- NO live-path change here. ACCEPTANCE is the DIFFERENTIAL ORACLE: stake_by_pool == cardano-cli query stake-snapshot (stakeSet per pool) + total at >=2 Conway boundaries -- a LIVE gate, DECLARED (owed, run at activation; NOT faked green by the hermetic tests).

Source

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

Introduced in
EPOCH-CONSENSUS-VIEW-S3c

Enforcement trace

Code

Tests 8

  • sums_utxo_plus_reward_per_delegated_pool
  • reward_without_utxo_contributes
  • undelegated_credential_contributes_nothing
  • delegated_zero_stake_pool_is_included_with_zero not on disk
  • multiple_pools_aggregate_independently
  • overflow_is_fail_closed
  • aggregation_is_deterministic
  • sum_base_credential_stake_skips_non_contributing

CI 2

Cross-references

DC-EVIEW-04DC-EVIEW-04bDC-EVIEW-02

Strengthened in

EPOCH-CONTINUITY-ACTIVATION-ECA-0b

Attack rationale

The aggregation must not (a) count undelegated or unregistered stake -- it iterates ONLY the delegations map (registered+delegated creds), so a credential's UTxO that is not delegated contributes 0 (a divergent leader schedule otherwise); (b) drop a delegated credential's reward balance -- reward-without-UTxO still contributes (Conway), proven by reward_without_utxo_contributes; (c) count NonContributing outputs -- sum_base_credential_stake folds only Base(cred), so pointer-retired/enterprise/Byron coins never enter (the era gate already applied in the reduced record); (d) silently wrap a stake total -- checked_add fail-closes to StakeOverflow; or (e) be claimed correct-vs-network from hermetic tests alone -- the cardano-cli stake-snapshot differential oracle is an explicit DECLARED live gate (open_obligations), not faked green. False stake -> wrong leader schedule is release-blocking, hence the oracle is the true acceptance.

Evidence notes

Introduced at EPOCH-CONSENSUS-VIEW S3c (2026-06-20), the aggregation linchpin. Pure BLUE, OBSERVE-ONLY (no live-path change; the new_mark rewire + leader feed are DC-EVIEW-08). 8 hermetic tests prove the LOGIC: UTxO+reward per delegated pool, reward-without-UTxO contributes, undelegated excluded + a 0-stake delegated pool INCLUDED (ECA-0b numDelegators>0), multiple pools independent, overflow fail-closed, deterministic, Base-only fold skips NonContributing. Reuses the single ledger authority's own state: the reduced checkpoint (DC-EVIEW-04/04b) + the delegation map (process_block_certificates). The heaviest dependency is CE-71 (the reward accounting that populates DelegationState.rewards) -- correct vs the test corpus (0-lovelace) but NEVER live; its first live-path use is gated (per the S3c scope CE-71 gate) on deterministic replay + crash/recovery + differential results + no change to live consensus decisions, all at activation. THE acceptance gate (open_obligations): stake_by_pool == cardano-cli query stake-snapshot stakeSet at >=2 Conway boundaries -- a LIVE differential oracle, declared, run at activation. cargo test -p ade_ledger + -p ade_runtime green. NO snapshot/emission (S3d/e), NO live wiring, NO leader/header use, NO track_utxo=true on live. Next: S3d (mark/set/go rotation + the k-immutability stability gate), S3e (EpochConsensusView emission/binding, observe-only), DC-EVIEW-08 (the ONLY activation slice -- the rewire + live oracle + leadership-schedule proof).