Blocks may carry two AttestationData for one slot, which no leanVM proof can express

[dimka90]

Summary

The spec permits a block whose proof cannot be built. A block may carry several distinct AttestationData for the same slot, but a leanVM aggregate carries at most one message per epoch, and the epoch is the slot. The proposer then fails to produce its block proof and the slot is lost.

Two of three clients on a mixed devnet are losing slots to this today.

Where the spec stands

The block rules constrain the number of distinct data and forbid repeats, but say nothing about two different data sharing a slot:

• spec/forks/lstar/config.py:58 — MAX_ATTESTATIONS_DATA = 8
• spec/forks/lstar/state_transition.py:218-221 — rejects a block whose distinct data exceed the cap (TOO_MANY_ATTESTATION_DATA)
• spec/forks/lstar/fork_choice.py:619 — rejects a block that repeats an AttestationData (DUPLICATE_ATTESTATION_DATA)
• spec/forks/lstar/block_production.py:129 — candidates are ordered by target slot, with the cap applied at line 148; nothing restricts two candidates that share data.slot

Validators disagreeing within a slot is ordinary: some have seen the slot's block and some have not, so they vote for different heads, or different targets, at the same slot. Each such vote is a distinct, valid AttestationData at one slot, and the spec invites a proposer to include them all.

Where the proof system stands

leanVM 022ec377:

• crates/rec_aggregation/src/aggregation.rs check_signer_set requires strictly increasing epochs across XMSS claim groups, so one message per epoch
• plan_coverage keeps "the epoch-to-message function every contributor must agree on" and keys XMSS claims as (epoch, key), with the message derived from the epoch
• a second, different message at one epoch returns AggregationError::ConflictingMessages

The proposer's own signature occupies the block's own slot, so an attestation for that slot collides with it too.

Observed

Three-client devnet (gean, ethlambda, lantern), 14 validators, 4 committees, all on leanVM 022ec377, 8 hours:

client	slots lost to this
lantern	186 (leanvm: merge_many_type_1 failed: two claims at one epoch carry different messages)
ethlambda	41 (failed to merge single-message aggregates into a multi-message aggregate: prover failure: two claims at one epoch carry different messages)
gean	0 — it keeps one AttestationData per slot, a rule it added itself

Traced example: two aggregates for slot 86 with targets 82 and 83 arrived, both went into the block for slot 87, and sealing failed. Reported as lambdaclass/ethlambda#617 and bitminetech/lantern#196.

What should the rule be?

The spec needs to settle what a block may carry, so every client filters identically. Today it is silent, so each client decides for itself: gean keeps one AttestationData per slot, ethlambda and lantern do not, and they lose slots for it.

The shape we implemented in gean, offered as a starting point rather than a conclusion:

• a block carries at most one AttestationData per slot, and none at the block's own slot
• build_block (block_production.py) selects accordingly
• block validation says whether a block breaking the rule is invalid, or valid but unprovable

Note that filtering has a cost of its own: the dropped votes are honest, and they are exactly the votes cast when validators disagree, so justification slows at the moment the network most needs it. If that cost is unacceptable, the alternative is on the leanVM side, below.

Longer term

The restriction is stricter than XMSS requires. The signature rule is one message per key per epoch; leanVM enforces one message per epoch across all keys. SPHINCS in the same file keys claims on (key, message) ("one key signing two messages is two claims") while XMSS derives the message from the epoch. Whether that can be relaxed is a question for leanVM, raised separately; if it is relaxed, this spec rule can be dropped again.

[gopikannappan]

One thing worth adding now that leanVM#278 has landed.

At 48a90420, plan_coverage groups XMSS claims by (epoch, message) and de-duplicates on the full (epoch, message, key) triple. ConflictingMessages is gone. So the blocks this issue describes, with several distinct AttestationData at one slot or an attestation at the block's own slot, can now be proven. With MAX_EPOCHS = 1024 groups against MAX_ATTESTATIONS_DATA = 8, the cap is nowhere near binding. The one-AttestationData-per-slot rule is no longer needed for provability, as the issue anticipated.

The relaxation goes one step further than "one message per key per epoch", though. Nothing checks for the same key across two groups. I tried it with a small test against leanVM's aggregation API: one key signing two different messages at epoch 7.

• At 022ec377 the aggregate is rejected (ConflictingMessages).
• At 48a90420 it is accepted and verifies, as two claims in groups (7, msg0) and (7, msg1).

That is sound as a proof, since each signature really does verify. But it means an aggregate can now carry an equivocation: one validator's attestation key signing two different AttestationData for one slot. The old rule blocked this as a side effect. Now the only guard against XMSS leaf reuse is the signer-side one (#1203/#1204).

I don't think this is a problem for consensus. Fork choice already expects equivocators (fork_choice.py:682), and attestation and proposal use separate keypairs (containers.py:181-196), so a proposer signing its block never collides with its own attestation key. But the spec should say which behaviour is intended, so clients don't split on it again:

1. May a block's aggregates include two different AttestationData signed by the same validator for one slot?
2. If not, should that be a block-validity rule in state_transition.py / fork_choice.py, or left to aggregators?

Either answer is fine. The point is to write it down, because leanVM no longer decides it for us.