Invariants / DC-SNAPSHOT-01

DC-SNAPSHOT-01

DC derived enforced

ServedChainHandle::push_atomic is deterministic in its argument order: the same sequence of push_atomic(a₀), push_atomic(a₁), ..., push_atomic(aₙ) produces a byte-identical ServedChainView (fingerprint equals over BTreeMap insertion order). Replay-equivalence anchor for the broadcast → serve path.

Source: docs/planning/phase4-n-r-invariants.md §3 (D6); §4 (R2)
Cluster: PHASE4-N-R-B
Introduced in: PHASE4-N-R-B

Enforcement trace

Code

crates/ade_runtime/src/producer/served_chain_handle.rs
crates/ade_runtime/src/producer/broadcast_to_served.rs

Tests 3

drain_and_admit_is_deterministic_over_arrival_sequence
drain_and_admit_no_io_no_clock
drain_and_admit_admits_every_queued_block

CI 0

no CI script — gap

DC-SNAPSHOT-01

Enforcement trace

Code

Tests 3

CI 0

Cross-references