Invariants / DC-EPOCH-33

DC-EPOCH-33

DC derived enforced

Refold re-seal identity. Re-deriving an epoch boundary the node has already crossed re-seals a frozen-leadership object byte-identical to the one the original crossing sealed -- target epoch, source point, source_checkpoint_commitment, and the whole pool map. Re-derivation is byte-identical because the original crossing folded the same (seed, s_prev] prefix in the same order and that prefix is immutable: s_prev belongs to a boundary already deeper than k, and rollback admission refuses anything deeper than k. Without this a refold leaves the durable eview activation record UNREPRODUCIBLE -- latently, since a running node never compares -- and the next restart halts terminally on EpochViewPostPromotionMismatch.

Source

docs/clusters/EVIEW-RECOVERY-LINEAGE/SLICE-R2-refold-reseals-frozen-leadership-byte-identically.md (INV-ER-2)

Introduced in
EVIEW-RECOVERY-LINEAGE-R2

Enforcement trace

Cross-references

Evidence notes

The proof crosses a boundary through the PRODUCTION co-advancer, captures the sealed leadership set, then forces the live refold shape -- accumulator reset to bootstrap, reduced checkpoint left at the durable tip (and deliberately not ahead of it, so the tip-only reset does not fire) -- and asserts the re-sealed set is equal. It was verified to DISCRIMINATE: with the seal path reverted to the bare forward advance it fails on exactly the field the live node halted on. SUPPORTING live evidence only (never the reason for enforcement): the 2026-08-02 70-second preview reproducer halted with differing=[checkpoint_commitment, stake_view_canonical_hash, view_canonical_hash] while target_epoch, transition_point and the eta0 nonce all matched -- every accumulator-derived field agreeing and every checkpoint-derived field disagreeing. CE-R2-4 is now MET LIVE (2026-08-02): a fresh preview store crossed 1375->1376 and 1376->1377, took a genuine peer rollback -> reset_to_settled -> reset_and_refold, and the refold re-crossed the boundary with the checkpoint 153,565 slots ahead of it in a later epoch -- the exact poisoning condition -- logging 'reduced checkpoint REWOUND onto boundary point 118886384 before sealing'. After a second such refold the node was SIGKILLed mid-refold and restarted clean, past 200s, with no EpochViewPostPromotionMismatch. The pass is NOT vacuous: the store's WAL activation record binds cbb12da0 / 88c236d6 / b35be7b6 / 091b1881 -- every field the poisoned store's record bound -- and none of the corrupted de32979c / 42681f92 / 18892c1b, so recovery took the (Some,Some)+matches => Promoted arm and a separate bootstrap independently reproduced the correct values byte for byte. Negative control: the poisoned store still halts identically under the same fixed binary, so the terminal was not weakened. CE-R2-5 is now MET LIVE (2026-08-03 00:28Z), closing the slice: after 3.5h of live following and three refolds the same store caught up to tip and crossed 1377->1378 at slot 119059222 LIVE -- labelled CROSSED not REFOLD, with anchor == durable_tip at the crossing -- was then restarted and came up on forward_fold with anchor == tip == 119060626, which is the EXACT signature that killed the poisoned store at ~70s, and ran on clean with 0 mismatches. Positive control again non-vacuous: the WAL now carries a record bound to the NEW boundary point 119059157 and to epoch 1379, so recovery compared rather than resolving (None,_) => Seed, and the corrupted de32979c/42681f92/18892c1b remain absent. Full run tally: 3 rewinds across 3 refolds, 1 live boundary crossing, 2 restarts (one SIGKILL mid-refold), 0 eview mismatches, 0 unplanned exits. Negative control retained: the poisoned store still halts identically under the same fixed binary, so the terminal was not weakened. Enforcement rests on the named test + ci/ci_check_eview_refold_reseal.sh.