Invariants / DC-WAL-03

DC-WAL-03

DC derived enforced

Anchor + 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.