AdeAtlas
Invariants / CN-FORGE-02

CN-FORGE-02

CN derived enforced

Leader-check splits across the RED/BLUE color boundary: RED produces a VRF proof/output for the slot using the operator's VRF signing key; BLUE verifies the proof and evaluates leader eligibility from canonical inputs only (slot, eta0, stake_distribution, leader_threshold, vrf_vk, vrf_proof_or_output, LeaderScheduleAnswer). BLUE never sees the VRF / KES / cold signing keys. The BLUE evaluator (verify_and_evaluate_leader) lives at ade_core::consensus::leader_check and has no dependency on LedgerView, EraSchedule, ChainDepState, wall-clock, storage, or RED crates. Caller derives LeaderScheduleAnswer via the authority path (query_leader_schedule) and passes it in. The closed two-variant LeaderCheckVerdict (Eligible carries forge-capable material; NotEligible carries only bounded vrf_output_fingerprint evidence) makes illegal observation of forge-capable material structurally impossible.

Source

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

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

Enforcement trace

Code

Tests 10

  • eligible_on_threshold_with_high_stake_emits_eligible_verdict
  • not_eligible_with_zero_stake_emits_not_eligible_verdict
  • malformed_proof_emits_verification_failed
  • wrong_vk_emits_verification_failed
  • answer_slot_mismatch_emits_structured_error
  • vrf_input_mismatch_emits_structured_error
  • zero_stake_denominator_emits_structured_error
  • verdict_is_byte_identical_across_two_runs
  • vrf_output_fingerprint_is_first_8_bytes_of_output
  • zero_stake_answer_emits_forge_not_leader

CI 1

Cross-references

T-KEY-01CN-FORGE-01DC-FORGE-01DC-CRYPTO-04DC-CRYPTO-05

Attack rationale

Cardano-specific: a BLUE component that owns or reads VRF signing keys could forge proofs for non-leader slots — the foundation of the eligibility security model. The RED/BLUE split makes BLUE structurally incapable of producing forge-capable material, even in the presence of bugs.

Evidence notes

Enforcement combines (a) the closed enum shape of LeaderCheckVerdict making NotEligible -> vrf_output access structurally impossible (type-level), (b) ci/ci_check_leader_check_authority.sh enforcing the allow-list for is_leader_for_vrf_output callers — no external caller may bypass LeaderCheckVerdict, and (c) ci/ci_check_producer_coordinator_no_secrets.sh enforcing the GREEN coordinator never imports signing-key types. The new BLUE module has NO dependency on LedgerView / EraSchedule / PraosChainDepState / wall-clock / storage / RED crates — verified by direct import inspection (CE-A-6b).