AdeAtlas
Invariants / T-REC-05

T-REC-05

T true enforced

Replay/recovery equivalence including forged admits. Same BootstrapAnchor + same WAL (including forged AdmitBlock entries) -> byte-identical recovered durable tip and ledger fingerprint. Same recovered/bootstrapped state + same ordered canonical block feed + same deterministic clock-tick schedule + same leadership/key inputs + same shutdown schedule -> byte-identical durable outputs (tip, WAL image, checkpoints, halt state), INCLUDING forged-then-admitted blocks. Extends T-REC-01/02/03 from received-only to forged+received durable progression; rides the existing snapshot + forward-replay recovery law (NOT full-genesis replay) -- no new durability law.

Source

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

Introduced in
PHASE4-N-U

Enforcement trace

Code

Tests 6

  • forge_kill_then_warm_start_recovers_same_tip_via_forward_replay
  • forge_tip_successor_kill_then_warm_start_recovers_block_one
  • recover_follow_forge_two_runs_byte_identical
  • recover_follow_kill_warm_start_chains_from_ledger_fp
  • recover_follow_two_runs_byte_identical
  • same_store_same_anchor_point_same_findintersect_start

CI 0

no CI script — gap

Cross-references

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

Strengthened in

PHASE4-N-ADPHASE4-N-AEPHASE4-N-AHPHASE4-N-AIPHASE4-N-AK

Evidence notes

PHASE4-N-U S2 (2026-06-05). ENFORCED (test-enforced; no dedicated CI gate). A forged-block durable tip carries NO snapshot-at-tip (admit_forged_block_durably captures none); warm_start_recovery recovers it by FORWARD-REPLAY from the genesis slot-0 snapshot over the durable WAL block, and its fingerprint guard asserts the recovered ledger fp == the WAL-tail post_fp -- so reaching Ok with the same tip is byte-identical replay equivalence (forge_kill_then_warm_start_recovers_same_tip_via_forward_replay: forge block 0 -> admit -> kill -> reopen -> warm_start_recovery -> recovered tip slot+hash == the pre-kill durable tip). Rides the existing snapshot + forward-replay recovery law (the bootstrap_initial_state warm-start branch, already proven by recover_node_state's recovery_crash_at_phase_sync_byte_identical) -- no new durability law. True-tier: extends T-REC-01/02/03 from received-only to forged+received durable progression. PHASE4-N-AD (2026-06-06) STRENGTHENS: forge_tip_successor_kill_then_warm_start_recovers_block_one extends the proof from a single block-0 forge to a multi-block forged progression -- forge block 0 -> admit -> forge block 1 on the durable NON-Origin tip -> admit -> kill -> warm_start_recovery recovers block 1 byte-identically (no ChainBreak), proving the block-N -> block-N+1 prior_fp chains across WAL replay. The C1 cold-start seed -> block-0 ChainBreak (seed ledger fp vs the PrevHash::Genesis/null prior) is a C1 genesis-successor-only durability limitation, NOT a C2 tip-successor blocker -- C2 enters from a non-Origin recovered tip. PHASE4-N-AE.C (2026-06-07) STRENGTHENS to recover->FOLLOW->warm-start: the CE-A5 live run found node_lifecycle seeding the follow ForwardSyncState prior_fp with zero (not fingerprint(&state.ledger).combined), breaking replay-equivalence of a recover->followed store (warm-start ChainBreak@1, exit 42). recover_follow_kill_warm_start_chains_from_ledger_fp proves warm-start recovers the same followed tip; recover_follow_two_runs_byte_identical proves same recover base + same followed block -> byte-identical recovered tip + WAL image, after the fix.