AdeAtlas
Invariants / DC-EPOCH-24

DC-EPOCH-24

DC derived enforced

Snapshot pool-set inclusion = cardano's ssActiveStake NonZero membership (CE-3d). The per-epoch stake snapshot (mark/set/go) INCLUDES a registered+delegated stake credential IFF its combined active stake (base-address UTxO coin + reward-account balance) is NON-ZERO, and OMITS it otherwise -- so a pool whose ONLY delegators are all zero-stake is structurally ABSENT from the snapshot (no delegations entry, no pool_stakes entry). This is cardano-ledger's resolveActiveInstantStakeCredentials (Stake.hs): ssActiveStake is a NonZero-typed VMap -- getNonZeroActiveStakeWithDelegation drops a delegated credential whose account balance is zero when it has no UTxO, and a credential WITH a UTxO is >= minUTxO (always non-zero). It is the SERIALIZED go/set/mark SnapShot representation, DISTINCT from the DERIVED PoolDistr whose explicit numDelegators>0 count keeps a 0-stake pool that has a delegator. (a) DECIDED AT CONSTRUCTION, NOT A POST-FILTER: the membership guard lives INSIDE build_boundary_mark_snapshot (the authoritative boundary mark that rotates into set then go) and aggregate_pool_stake (the reduced-checkpoint projection, DC-EVIEW-05) -- a credential with zero combined stake is never inserted, so no finished map is filtered after the fact. (b) BYTE-EQUAL TO THE DECODED REFERENCE: Ade's own decoder read_stake_snapshot_full reads cardano's serialized ssStake (map(cred -> [coin, pool]), always non-zero) and aggregates it, so the self-derived snapshot's pool SET, per-pool values, per-credential delegations, and the canonical snapshot fingerprint (write_stake_snapshot over delegations + pool_stakes) all equal the cardano reference. (c) REWARD / LEADERSHIP NEUTRAL: a zero-stake credential earns zero member reward (floor((f-c)*(1-m)*0/sigma)=0, gated by if member_reward > 0) and a zero-stake pool has zero leader probability, so the omission changes NO reward and NO leader schedule and leaves the go TOTAL unchanged -- only the canonical map cardinality, the serialized snapshot bytes, and the hash. (d) PERSISTED-SEMANTICS REJECT (compatibility/recovery slice): the (b) construction change makes a PERSISTED mark/set/go an authoritative serialized artifact whose inclusion semantics is version-bound. A v3 store's marks were built under the prior numDelegators>0 rule (phantom 0-stake pools), so EPOCH_ACCUMULATOR_SCHEMA_VERSION is bumped 3 -> 4; a pre-C v3 (or v1/v2/unversioned) store fails closed on decode (UnknownVersion, surfaced fail-closed by EpochAccumulatorStore::load_current). A warm-start therefore NEVER RELOADS a stale snapshot-inclusion semantics and never carries it forward (a reloaded pre-C mark would otherwise stay non-reference-equivalent until it rotates out two boundaries later). Persisted authority has ONE unambiguous replay meaning; the only migration is an explicit fresh re-bootstrap under v4 -- never a silent reinterpretation.

Source

CE-3d go pool-set inclusion slice (residual C). The differential exposed 32 phantom pools present ONLY in Ade's self-derived go (each a registered pool with a registered, zero-stake delegator), absent from the cardano reference decoded by Ade's own read_stake_snapshot_full. Root cause: build_boundary_mark_snapshot + aggregate_pool_stake inserted Coin(0) for every delegation -- a deliberately-encoded but WRONG numDelegators>0 rule that conflated the derived PoolDistr with the serialized ssActiveStake. cardano-ledger libs/cardano-ledger-core Stake.hs resolveActiveInstantStakeCredentials / getNonZeroActiveStakeWithDelegation; SnapShots.hs snapShotFromInstantStake.

Introduced in
CE3D-GO-POOLSET-INCLUSION-C

Enforcement trace

Code

Tests 5

  • ade_ledger::epoch_accumulator::tests::build_boundary_mark_snapshot_omits_zero_stake_credential
  • ade_ledger::reduced_aggregate::tests::delegated_zero_stake_pool_is_omitted
  • ade_ledger::reduced_aggregate::tests::ssactivestake_membership_decision_table
  • ade_ledger::epoch_accumulator::tests::cross_epoch_boundary_per_credential_mark_pays_member_rewards
  • ade_ledger::epoch_accumulator::tests::codec_rejects_pre_c_v3_store_rebootstrap_required

CI 1

Cross-references

DC-EPOCH-18DC-EPOCH-19DC-EPOCH-23DC-EVIEW-05

Strengthened in

CE3D-GO-POOLSET-SCHEMA-REJECT

Attack rationale

The tempting shortcut is a COSMETIC POST-FILTER -- strip 0-stake pools off the finished map before comparison -- which leaves the authoritative construction still emitting them (so the persisted snapshot, its fingerprint, and any downstream consumer disagree with the compared view) and silently diverges the moment the filter and the builder drift. This rule forbids that: the membership decision is MADE in the builder, so the persisted bytes, the fingerprint, and the compared map are one artifact. A second shortcut is to keep the WRONG numDelegators>0 rule (include a 0-stake pool because it has a delegator) -- correct for the derived PoolDistr, WRONG for the serialized ssActiveStake Ade decodes byte-for-byte; the frozen decision-table test pins the four (UTxO, reward) -> present/absent cases against the cardano source so a future edit cannot reintroduce it. The rule is reward/leadership neutral by construction (a 0-stake credential/pool contributes 0 to every reward and 0 leader probability), so it cannot be used to smuggle a stake or reward change. A THIRD shortcut is to warm-start-RELOAD a pre-C persisted mark under the corrected binary ('no production store predates the fix' -- operational, not constitutional): but a persisted mark is authoritative serialized state whose inclusion semantics is version-bound, so reloading a v3 mark silently carries a stale interpretation forward (non-reference-equivalent until it rotates out two boundaries later). The schema bump 3->4 forbids it -- a pre-C store fails closed (UnknownVersion), re-bootstrap is the only migration -- because persisted authority must have one unambiguous replay meaning.

Open obligation