AdeAtlas
Invariants / DC-EPOCH-38

DC-EPOCH-38

DC derived enforced

The Praos candidate-freeze / nonce surface must be proven across SEED-POSITION x VENUE, not once per venue. eta0(N+1) is committed from the candidate nonce, which tracks evolving until firstSlotNextEpoch - RSW and freezes there; a bootstrap seed BEFORE that slot projects from a candidate that is guaranteed to keep moving. So no durable epoch activation record may take its nonce from a seed-time projection: eta0(seed+1) is the boundary TICK over the live chain-dep -- identical to every later boundary -- and the bootstrap bridge's stored seed_time_eta0 is a CROSS-CHECK that MUST corroborate the tick when, and only when, the seed sat at/after the freeze. A finality decision that cannot be DERIVED (seed unlocatable, or venue RSW absent so the freeze is INERT) is terminal, never assumed either way. For every venue in the closed registry, BOTH sides of the freeze must be exercised against that venue's real k/f/epoch geometry, and a mismatch must localize to the operand that differs.

Source

docs/clusters/PREPROD-NONCE-AUTHORITY/SLICE-PREPROD-NONCE-1-eta0-boundary-equivalence.md; docs/clusters/PREPROD-NONCE-AUTHORITY/SLICE-PREPROD-NONCE-2-activation-waits-for-candidate-freeze.md (CE-N2-4)

Introduced in
PREPROD-NONCE-2

Enforcement trace

Code

Tests 10

  • dc_epoch_38_bridge_nonce_freeze_differential_covers_both_sides_per_venue
  • n2_pre_freeze_seed_binds_the_boundary_tick_not_the_stored_projection
  • n2_final_seed_must_corroborate_the_boundary_tick
  • n2_underivable_finality_is_terminal
  • n2_live_and_recovery_bind_the_same_view_byte_identically
  • n2_recovery_nonce_must_be_bound_to_the_target_epoch
  • preprod_snapshot_6009_seed_is_pending
  • seed_exactly_at_the_freeze_slot_is_final
  • preview_geometry_decides_identically_at_the_same_relative_position
  • oversized_rsw_saturates_and_is_final

CI 1

Cross-references

DC-EPOCH-16DC-EPOCH-15DC-EPOCH-37DC-STORE-12

Evidence notes

Opened AFTER the diagnosis so the gate encodes what was PROVEN rather than what was guessed. NONCE-1 measured the defect live on preprod 304->305: the bridge committed blake2b(candidate@SEED || leb) = e3402a2b.. while cardano-node's epochNonce(305) is 74f10bea.. = blake2b(candidate@FROZEN || leb), with the second operand BYTE-IDENTICAL on both sides -- so the entire disagreement localized to one operand, the candidate, 132,173 slots of movement apart. The same trace independently proved the freeze machinery CORRECT (candidate != evolving at the boundary), which is why the fix touches only WHERE the commitment comes from and leaves the tick, the freeze rule, the operand order and the venue geometry untouched -- all reference-proven against cardano-node. THE SURFACE IS SEED-POSITION, NOT VENUE: rsw/epoch_length is 0.4 on preprod (172800/432000) AND preview (34560/86400), so the freeze sits at 60% into the epoch on both and a once-per-venue differential passes straight through the defect; preview only ever worked because its snapshots landed after the freeze, preprod snapshot 6009 landed 29% in. The differential therefore asserts that ratio explicitly, so a future venue with different geometry fails loudly instead of silently invalidating the matrix. Negative-tested SIX ways: the pre-freeze side removed; the ratio assertion removed; the venue list hand-copied instead of read from resolve_network_profile; the differential test deleted; the binder rebound to the stored seed-time value (the original regression); and the Final cross-check disabled. The FIRST version of this gate was TOO WEAK and passed the last two -- its cargo test --exact filter used a bare fn name where the full module path is required, matched ZERO tests, and cargo exits 0 on an empty filter; every test invocation now asserts a nonzero passed-count. That is the fourth gate weakness in this cluster found by mutation testing, and the second of the same shape (a check that greps or filters for something it never actually reaches).