AdeAtlas
Invariants / DC-WAL-04

DC-WAL-04

DC derived enforced

Forged-block WAL chain integrity. A forged AdmitBlock WAL entry's prior_fp MUST equal the current durable post_fp (the BootstrapAnchor's initial_ledger_fingerprint for a genesis-successor block 0; the previous entry's post_fp otherwise). A forged block that would ChainBreak (prior_fp mismatch) is rejected fail-closed (authority-fatal). The WAL binds the EXACT canonical self-accepted bytes (no re-encode; I-10). Warm-start recovery reconciles durable block storage and the WAL tail so a torn forge-admit crash leaves no un-WAL'd forged orphan at or ahead of the durable tip.

Source

docs/planning/phase4-n-u-forged-block-durability-invariants.md

Introduced in
PHASE4-N-U

Enforcement trace

Code

Tests 3

  • forged_admit_wal_prior_fp_chains
  • warm_start_drops_orphan_block_above_wal_tail
  • forge_tip_successor_kill_then_warm_start_recovers_block_one

CI 1

Cross-references

DC-WAL-01DC-WAL-02DC-WAL-03DC-SYNC-01T-REC-05DC-NODE-12

Strengthened in

PHASE4-N-AD

Evidence notes

PHASE4-N-U S1+S2 (2026-06-05). ENFORCED. CHAINING (S1): a forged AdmitBlock's prior_fp chains from the anchor initial_ledger_fingerprint and the forged WAL verifies from it (forged_admit_wal_prior_fp_chains), because admit_forged_block_durably routes through the SAME pump_block / forward_sync_step that sets prior_fp = state.prior_fp and post_fp = the post-admit fingerprint. NO-ORPHAN-RECOVERY (S2): production warm_start_recovery reconciles the ChainDb to the WAL tail (rollback_to_slot before warm-start), so a torn StoreBlockBytes-before-AppendWal crash leaves no un-WAL'd orphan at or ahead of the durable tip (warm_start_drops_orphan_block_above_wal_tail). Full byte-identical forward-replay equivalence over forged blocks is T-REC-05 (its forward-replay test is the remaining S2 work). PHASE4-N-AD (2026-06-06) STRENGTHENS: the tip-successor prior_fp clause (prior_fp == the previous entry post_fp, the non-genesis-successor case) is now replay-tested by forge_tip_successor_kill_then_warm_start_recovers_block_one -- block 1 forged on the durable NON-Origin block-0 tip (prior_fp = block-0 real post_fp) recovers across a kill via warm_start_recovery with no ChainBreak. The C1 cold-start seed -> block-0 ChainBreak (seed ledger fp vs PrevHash::Genesis/null) is a C1 genesis-successor-only limitation, NOT a C2 blocker.