DC-WAL-03
DC derived enforcedAnchor + WAL replay-equivalence: replaying (BootstrapAnchor + WAL entries 1..N) against (initial_ledger from import + per-entry block bytes) produces a final ledger whose fingerprint equals WAL[N].post_fp byte-identically across two runs. The runtime contract "same anchor + same inputs + same WAL → byte-identical outputs" is mechanically proven by integration test.
- Source
docs/planning/phase4-n-m-ledger-seed-invariants.md §1 (I-A6)
Enforcement trace
Tests 5
- crates/ade_runtime/tests/wal_replay_from_anchor.rs::wal_replay_from_anchor_two_runs_byte_identical
- crates/ade_runtime/tests/wal_replay_from_anchor.rs::wal_replay_from_anchor_post_fp_matches_wal_tail
- crates/ade_runtime/tests/wal_replay_from_anchor.rs::wal_replay_from_anchor_persists_across_reopen
- crates/ade_ledger/src/wal/replay.rs::tests::replay_from_anchor_three_entry_chain_ok
- crates/ade_ledger/src/wal/replay.rs::tests::replay_from_anchor_two_runs_byte_identical
CI 0
no CI script — gap
Cross-references
Strengthened in
Evidence notes
PHASE4-N-M-A S4 (2026-05-26): integration test wal_replay_from_anchor_two_runs_byte_identical proves the runtime contract same anchor + same inputs + same WAL → byte-identical outputs. Final ledger fingerprint equals WAL[N].post_fp; persists across FileWalStore reopen. PHASE4-N-M-B (2026-05-26): strengthened by admission_replay_equivalence_byte_identical_wal_after_two_runs — same property holds when the WAL is driven by the live admission runner (run_admission) over an identical peer-event stream. PHASE4-N-F-C (2026-05-31): the --mode node lifecycle owner is the FIRST PRODUCTION caller of replay_from_anchor — warm_start_recovery replays (BootstrapAnchor + WAL) at restart, and L4c (node_sync_kill_then_warm_start_recovers_same_tip) proves a peer-synced + pump_block-advanced tip is recovered byte-identically by that anchor+WAL replay across a kill boundary.