AdeAtlas
Invariants / DC-EPOCH-32

DC-EPOCH-32

DC derived enforced

Boundary seal reads a POSITIONED checkpoint. The boundary mark and the reduced-checkpoint commitment sealed into a frozen-leadership object are captured with the checkpoint positioned EXACTLY at the boundary point s_prev -- verified, never assumed. A checkpoint sitting PAST s_prev is rewound onto it (re-materialize from the sealed seed, then replay forward; the reduced delta is not invertible); a boundary point that cannot be reached stalls the crossing observe-only and seals NOTHING. The forward-only advance alone does not satisfy this: asked to go backward it returns Ok(()) having moved nothing, so the mark and commitment would be read at whatever slot the cursor happened to hold.

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

Code

Tests 3

  • positioning_rewinds_a_checkpoint_that_sits_past_the_boundary_point
  • a_bare_forward_advance_asked_to_go_backward_silently_moves_nothing
  • a_boundary_point_before_the_sealed_seed_is_unreachable

CI 1

Cross-references

DC-EPOCH-11DC-EPOCH-22DC-EPOCH-33

Evidence notes

The proof positions a checkpoint at a boundary point, records its commitment and mark, drives it past that point with state the ChainDB does not hold, then re-positions and asserts BOTH are reproduced byte for byte -- and asserts the drive genuinely moved the checkpoint first, so it cannot pass vacuously (every block in the fixture is the same raw Conway block and re-application is idempotent). A companion NEGATIVE test pins the bare forward advance's silent no-op so the seal path cannot regress to calling it. The gate additionally asserts ORDERING (positioning precedes both the mark capture and the finalize), which no compiler check covers. Enforcement rests on the named tests + ci/ci_check_eview_refold_reseal.sh.