AdeAtlas
Invariants / CN-SNAPSHOT-01

CN-SNAPSHOT-01

CN derived declared

A forged block becomes visible to peers only AFTER ServedChainHandle::push_atomic succeeds. The push_atomic call covers the full served_chain_admit call inside a watch::Sender::send_modify closure — no observer can read a torn snapshot mid-insertion. Coordinator emits BroadcastBlock; RED effect handler calls push_atomic; only on Ok(ServedTip) may per-peer reducers serve the block. Fail-closed shutdown on PushError.

Source

docs/planning/phase4-n-r-invariants.md §1 (I4); §2 (N11); §3 (D6)

Introduced in
PHASE4-N-R-B

Enforcement trace

Code

no enforcing code — gap

Tests 3

  • handle_construction_yields_empty_snapshot
  • view_subscribe_creates_independent_receiver
  • served_tip_is_closed_value_type

CI 0

no CI script — gap

Cross-references

CN-FORGE-01DC-SNAPSHOT-01DC-CONS-17

Strengthened in

PHASE4-N-T