AdeAtlas
Invariants / DC-CONS-20

DC-CONS-20

DC derived enforced

ChainDb-ledger-chain_dep lockstep: a successful receive-side admission updates ChainDb, LedgerState, and PraosChainDepState as one structural transition. A successful RollBackward rolls back all three to the same slot. No path leaves them out of sync; no partial admission; no partial rollback.

Source

docs/planning/receive-side-bridge-invariants.md §1 (I-3, I-4); docs/planning/ledger-snapshot-rollback-invariants.md §1 (I-6)

Cluster
PHASE4-N-H + PHASE4-N-I
Introduced in
PHASE4-N-H
Authority surface
receive-side atomic admit + rollback over ChainDb + LedgerState + PraosChainDepState

Enforcement trace

Code

Tests 8

  • receive_apply_block_delivered_with_matching_header_admits
  • commit_rollback_advances_chaindb_and_ledger_atomically
  • commit_rollback_chain_write_failure_leaves_state_unchanged
  • commit_rollback_resets_pending_headers
  • rollback_branch_returns_rolled_back_on_in_memory_snapshot
  • rollback_branch_returns_rollback_too_deep_when_no_snapshot
  • rollback_branch_state_unchanged_on_materialize_failure
  • rollback_then_continue_admit_equals_straight_line_admit

CI 3

Cross-references

CN-CONS-08DC-CONS-13CN-STORE-07DC-CONS-22

Strengthened in

PHASE4-N-IPHASE4-N-JPHASE4-N-YPHASE4-N-AIPHASE4-N-AO

Evidence

  • Admit-side (N-H): block_delivered atomically advances chain_write -> ledger -> chain_dep with staged-then-committed shape; failure leaves state unchanged (test receive_apply_block_delivered_validity_invalid_rejects).

  • Rollback-side (N-I): roll_backward calls materialize_rolled_back_state + commit_rollback; commit_rollback's irreversible-step-first shape leaves state unchanged on chain_write failure (commit_rollback_chain_write_failure_leaves_state_unchanged); pending headers reset on successful commit.

  • End-to-end: rollback_then_continue_admit_equals_straight_line_admit proves snapshot+rollback yields the same ledger fingerprint as straight-line admit — snapshotting is a pure cache.

  • Restart-safe rollback (N-J): PersistentSnapshotCache bridges framing::{encode,decode}_snapshot to SnapshotStore; cross-impl equivalence with InMemorySnapshotCache proven via persistent_cache_matches_in_memory_cache_semantics — restart-safe rollback now possible without weakening lockstep.