AdeAtlas
Invariants / DC-EPOCH-40

DC-EPOCH-40

DC derived partial

Leadership sigma denominator authority (SLICE LV-1). The leader-check sigma denominator is the SNAPSHOT's total active stake -- cardano's pdTotalActiveStake -- captured at freeze time as the CREDENTIAL-side sum of the boundary mark and carried on FrozenLeadershipPoolDistr as its own field. (a) IT IS INVARIANT UNDER THE LEADERSHIP MEMBERSHIP FILTER: adding a pool to, or removing one from, FrozenLeadershipPoolDistr::pools MUST NOT change it. (b) IT IS NEVER RE-DERIVED by summing the surviving entries, at freeze time or at read time, and there is no sum-based fallback for a missing value -- a missing total fails closed. (c) THERE IS ONE DEFINITION, StakeSnapshot::total_active_stake, which folds delegations (cardano's ssStake), never pool_stakes and never any filtered pool set; the boundary freeze and the bootstrap mark import both call it. (d) IT IS CAPTURED BEFORE the membership filter runs. (e) IT IS INSIDE THE CANONICAL ENCODING and therefore inside canonical_hash: it is authority, not diagnostics, because it changes leader schedules.

Source

docs/clusters/PREPROD-LIVE-2-FORGE-READINESS/SLICE-LV-1-sigma-denominator-authority.md; docs/evidence/run-stores/preprod-live2c/leadervalue-oracle-extraction-sigma-denominator.md; docs/evidence/run-stores/preprod-live2c/leadervalue-census-sigma-denominator.txt; docs/evidence/run-stores/preprod-live2c/b12-ce10-BLOCKED-leader-value-above-threshold.txt.

Cluster
PREPROD-LIVE-2-FORGE-READINESS
Introduced in
PREPROD-LIVE-2-LV-1
Authority surface
BLUE leadership authority. The frozen leadership object is durable, canonically encoded and hash-committed; this field changes leader schedules. STORE SEMANTICS 6 -> 7 (a v6 object carries no total and reconstructing one by summing its entries is the defect), FROZEN_LEADERSHIP_SCHEMA_VERSION 6 -> 7.

Enforcement trace

Code

Tests 4

  • adding_or_removing_a_pool_does_not_move_the_denominator
  • the_retired_pool_no_longer_deflates_every_other_pools_sigma
  • the_credential_side_sum_includes_stake_the_membership_filter_would_drop
  • the_total_round_trips_and_is_committed_to

CI 2

Cross-references

DC-EPOCH-24DC-EPOCH-25DC-EPOCH-19DC-EPOCH-32DC-NODE-47DC-STORE-12

Evidence notes

STATUS IS partial DELIBERATELY. The in-tree proof is complete -- 4 CE tests green, both gates passing, four required mutations each breaking something (restoring the summing loop breaks the GATE and the TESTS; folding the pool side, not bumping STORE_SEMANTICS_VERSION, and sourcing the total from anywhere but the mark each break the gate) -- but CE-LV1-9 (live) is not met. WRONG IN BOTH DIRECTIONS, and this is why the rule exists rather than a patch: a pool in Ade's set whose delegators' stake cardano does not count inflates the denominator, deflates every sigma and every threshold, and Ade spuriously REJECTS (the observed preprod halt); the INVERSE -- stake cardano counts behind a pool Ade filtered out -- deflates the denominator, inflates every sigma and threshold, and Ade would spuriously ACCEPT a header cardano rejects, a silent consensus divergence on the receive path that has never been observed and that nothing in the pre-LV-1 code prevented. MEMBERSHIP IS NOT CHANGED AND IS CORRECT per the same oracle (numDelegators > 0 intersected with the registered VRFs, retaining pools retiring at the boundary): DC-EPOCH-24/25 are not re-opened, and the retired pool STAYS in the set -- the_retired_pool_no_longer_deflates_every_other_pools_sigma asserts contains_key precisely so a future edit cannot 'fix' this by deleting it. THE LIVE BAR IS WEAKER THAN THE IN-TREE ONE AND THAT WAS STATED BEFORE THE RUN: a fresh v7 bootstrap anchors near the current tip (epoch ~310), far past slot 130,739,648, so it never validates the header that failed; a green live run is evidence of NO REGRESSION, not evidence the defect is fixed. The bar is CE-LV1-2, on the real sealed epoch-306 operands. THIS SLICE RETIRES ITS OWN REPRODUCER, knowingly: the v6 preprod store halts on the failing header in ~2 minutes and a v7 binary refuses to open it. NOT CLAIMED: the VALUE of ssTotalActiveStake at the 304->305 boundary is not confirmed against a reference (the epoch-306 nesPd no longer exists on disk -- the live peer reached epoch 310 during the investigation, closing that window), and the census's separate ~0.8% epoch-306 NUMERATOR gap is unexplained and NOT addressed here; a green header must not be read as settling either. ID NOTE: first drafted as DC-EPOCH-47 and corrected to the next free id 40 before landing -- the BND line already cost one ID-collision fix (eb55a637).

Evidence

  • ORACLE, cardano-ledger quoted at TWO points in its history so the property is not an artefact of one release. Conway (cardano-ledger-conway-1.17.0.0, contemporary with cardano-node 11.0.1, the venue): let total = sumAllStakeCompact stake where sumAllStakeCompact = VMap.foldl (<>) mempty . unStake. master: ssTotalActiveStake = sumAllActiveStake ssActiveStake in mkSnapShot, and calculatePoolDistr' includeHash (SnapShot _ activeStake stakePoolSnapShot) = ... PoolDistr { unPoolDistr = ... mapMaybeWithKey toIndividualPoolStake ..., pdTotalActiveStake = activeStake } with toIndividualPoolStake guarding on includeHash poolId and spssNumDelegators spss > 0. In BOTH the denominator is folded over the STAKE/credential map and the membership guards filter unPoolDistr ONLY, running after the total is fixed.

  • MEASURED on preprod (leadervalue-census-sigma-denominator.txt): at epoch 306 the sealed leadership set contains a RETIRED pool 8ed5ab11e76094fa2a2ab29fc3a57498d07e68f6fde6f326162eea88 worth 63,075,223,742,053 = 3.879% of the summed total; it is absent from Ade's epoch 307 and from cardano's nesPd at epoch 310 (bech32-checked with two controls present), and cardano-cli query pool-state returns {}. Summing the entries therefore inflated the epoch-306 denominator by 3.879%, deflating every pool's sigma by 2.87%.

  • The consequence, measured: the issuer 0ed90e52db2166b3a80e0711885b94f7950fc0e3898a573a8b98b0e9 got sigma 0.10642836% where cardano's stable value across three consecutive snapshots is 0.10958% / 0.10960% / 0.10966%, and a real preprod header was DETERMINISTICALLY rejected with LeaderValueAboveThreshold { value: [0,3,148,36,101,52,221,219], threshold: [0,3,147,218,125,24,43,26] } -- three byte-identical occurrences across two binaries and thirteen days. Only +0.031523% of sigma was required.

  • The control that localizes it to the denominator rather than the numerator: Ade's epoch-307 sigma for the same pool is 0.10957157%, matching cardano's 0.10958% to five significant figures. 307 has no membership change to expose the defect.