AdeAtlas
Invariants / DC-SYNC-01

DC-SYNC-01

DC derived enforced

During network forward-sync, a block's preserved wire bytes and its WAL entry MUST be durable before the chain tip advances to it, and admission is chokepoint-only (decode -> validate_and_apply_header -> block_validity -> fork-choice). The GREEN forward-sync lifecycle reducer emits a closed SyncEffect set; AdvanceTip is constructible only after StoreBlockBytes+AppendWal (private AdmitPlan, single durable() emit site), and the RED pump fail-closes (TipBeforeDurable) on any out-of-order apply. Because tip is derived from stored blocks, recovery reconciles the chaindb to the WAL tail so a torn put_block/wal-append crash cannot incorporate an un-WAL'd orphan (S6).

Source

docs/clusters/PHASE4-N-Y/S2-network-forward-sync.md; S6-torn-write-recovery-reconciliation.md

Cluster
PHASE4-N-Y
Introduced in
PHASE4-N-Y

Enforcement trace

Code

Tests 7

  • forward_sync_wal_and_bytes_precede_tip_advance
  • forward_sync_replay_two_runs_byte_identical
  • forward_sync_admission_through_chokepoints
  • recovery_torn_put_block_before_wal_append_drops_orphan
  • node_sync_pump_advances_recoverable_tip
  • node_sync_fails_closed_on_undecodable_block
  • node_sync_kill_then_warm_start_recovers_same_tip

CI 2

Cross-references

DC-CONS-20DC-STORE-01DC-STORE-02DC-STORE-05T-DET-01

Strengthened in

PHASE4-N-F-CPHASE4-N-F-D

Attack rationale

If the tip advanced before the WAL recorded a block, a power-loss crash would leave the chaindb tip ahead of the WAL; recovery (warm-start from chaindb.tip) would silently incorporate the un-admitted orphan, diverging from a clean run and breaking replay-equivalence. The type-encoded ordering + WAL-tail recovery reconciliation close it.

Evidence notes

PHASE4-N-F-C (2026-05-31, L4b): the --mode node lifecycle is the FIRST PRODUCTION driver of forward_sync::pump_block — run_node_sync feeds peer-fetched block bytes (L4a NodeBlockSource, decoupled from the admission verdict loop) into pump_block, advancing the recoverable tip durable-before-tip and failing closed on an undecodable block. New gate ci/ci_check_node_sync_via_pump.sh isolates the run_node_sync body and fences it positive on pump_block( while forbidding follow/derive_verdict/manual tip-advance/run_real_forge — so peer tip-agreement (ade_core_interop::follow) can never masquerade as validating sync.