TL;DR
ValidatorEntry documents that the attestation and proposal keys are separate "so one validator can sign both within the same slot without OTS conflict" — but nothing enforces it. ValidatorRegistry.add assigns without validation, and from_yaml never compares the two keys it loads. A node whose manifest carries the same key in both fields signs a block proposal and an attestation for the same slot with the same stateful XMSS key — exactly the one-time-signature state reuse the separation exists to prevent, and nothing in the node surfaces it. This requires an operator misconfiguration, so it is a robustness gap rather than a remotely triggerable bug — the same "invariant maintained only by convention" class as #1176.
How this was found: from the Lean 4 formalization of this spec (NyxFoundation/formal-leanSpec), attempting its VAL-2 proposition ("proposal key and attestation key are distinct"). The theorem is unprovable from the spec as written: the model has to assume distinctness as a Registry.WellFormed clause instead of deriving it from construction.
Reviewed at leanSpec 57d43399.
The invariant is stated but never checked
registry.py#L95-L110 carries the invariant in prose:
Attestation and proposal keys are separate.
This lets one validator sign both within the same slot without OTS conflict.
registry.py#L120-L122 — add is a bare dict assignment. registry.py#L173-L246 — from_yaml raises only for missing files and decode failures. Neither compares attestation_secret_key with proposal_secret_key, nor the manifest's two public keys.
What a same-key manifest does
A proposer runs both signing paths in one slot: _maybe_produce_block signs with proposal_secret_key at interval 0 (service.py#L313), _produce_attestations signs with attestation_secret_key at interval 1 (service.py#L260). Each goes through _sign_with_key (service.py#L372-L396), which advances the chosen key's prepared window and writes back only that field:
self.registry.add(replace(validator_entry, **{key_field: secret_key}))With identical key material in both fields, the slot's second signature starts from the other field's copy — the pre-advance state. The two signatures consume overlapping OTS state. For hash-based schemes that is a key-compromise-class failure, and both loads succeed and both signatures verify individually, so the misconfiguration stays invisible.
Suggested
Reject the misconfiguration at construction, where the check is one comparison: in from_yaml (or add), fail when the two keys coincide — comparing the manifest's two public keys suffices and avoids touching secret bytes. That turns the docstring's invariant into a client-checkable rule, and the formal model's WellFormed distinctness clause becomes discharged at load time, as #1179 did for the store invariants.
TL;DR
ValidatorEntrydocuments that the attestation and proposal keys are separate "so one validator can sign both within the same slot without OTS conflict" — but nothing enforces it.ValidatorRegistry.addassigns without validation, andfrom_yamlnever compares the two keys it loads. A node whose manifest carries the same key in both fields signs a block proposal and an attestation for the same slot with the same stateful XMSS key — exactly the one-time-signature state reuse the separation exists to prevent, and nothing in the node surfaces it. This requires an operator misconfiguration, so it is a robustness gap rather than a remotely triggerable bug — the same "invariant maintained only by convention" class as #1176.How this was found: from the Lean 4 formalization of this spec (
NyxFoundation/formal-leanSpec), attempting its VAL-2 proposition ("proposal key and attestation key are distinct"). The theorem is unprovable from the spec as written: the model has to assume distinctness as aRegistry.WellFormedclause instead of deriving it from construction.Reviewed at leanSpec
57d43399.The invariant is stated but never checked
registry.py#L95-L110carries the invariant in prose:registry.py#L120-L122—addis a bare dict assignment.registry.py#L173-L246—from_yamlraises only for missing files and decode failures. Neither comparesattestation_secret_keywithproposal_secret_key, nor the manifest's two public keys.What a same-key manifest does
A proposer runs both signing paths in one slot:
_maybe_produce_blocksigns withproposal_secret_keyat interval 0 (service.py#L313),_produce_attestationssigns withattestation_secret_keyat interval 1 (service.py#L260). Each goes through_sign_with_key(service.py#L372-L396), which advances the chosen key's prepared window and writes back only that field:With identical key material in both fields, the slot's second signature starts from the other field's copy — the pre-advance state. The two signatures consume overlapping OTS state. For hash-based schemes that is a key-compromise-class failure, and both loads succeed and both signatures verify individually, so the misconfiguration stays invisible.
Suggested
Reject the misconfiguration at construction, where the check is one comparison: in
from_yaml(oradd), fail when the two keys coincide — comparing the manifest's two public keys suffices and avoids touching secret bytes. That turns the docstring's invariant into a client-checkable rule, and the formal model'sWellFormeddistinctness clause becomes discharged at load time, as #1179 did for the store invariants.