AdeAtlas
Invariants / DC-FORGE-01

DC-FORGE-01

DC derived enforced

Given the same canonical input set (slot, eta0, vrf_vk, vrf_proof_or_output, LeaderScheduleAnswer), verify_and_evaluate_leader produces a byte-identical LeaderCheckVerdict across runs. Replay-equivalence anchor for the BLUE leader-check evaluator. Strengthens the existing leader-check determinism (DC-CONS-13 family) by exposing leader eligibility as a callable, replay-anchored function — not just an internal step in forge_block.

Source

docs/planning/phase4-n-r-invariants.md §3 (D1); §4 (R3)

Cluster
PHASE4-N-R-A
Introduced in
PHASE4-N-R-A

Enforcement trace

Code

Tests 3

  • verdict_is_byte_identical_across_two_runs
  • run_real_forge_is_byte_identical_across_two_runs
  • forge_from_recovered_is_deterministic_across_two_runs

CI 0

no CI script — gap

Cross-references

DC-CONS-13DC-CONS-14DC-PROD-02CN-FORGE-02

Strengthened in

PHASE4-N-F-C

Evidence notes

PHASE4-N-F-C (2026-05-31, L5): strengthened by forge_from_recovered_is_deterministic_across_two_runs — the leader-check evaluator produces a byte-identical CoordinatorEvent across two runs when the forge base is built from the RECOVERED SeedEpochConsensusInputs surface (via PoolDistrView::from_seed_epoch_consensus_inputs), extending the replay-equivalence anchor to the node-lifecycle forge handoff.