fix(lstar): reject malformed justification state with typed errors

[tcoratger]

What

Turns three incidental crashes on precondition violations into total functions or typed domain rejections, closing #1174. Two of the three are reachable on a state reconstructed from untrusted bytes (sync / database); the third is defence-in-depth.

Framing: robustness, not a consensus change

This does not change which blocks or states any correct client accepts. Every rejection path already funnels to "drop the block" (the sync driver wraps the transition in a catch-all), so an AssertionError, a ValueError, and a SpecRejectionError are consensus-equivalent — they reject the same block. The value is a defined, language-neutral rejection in place of a crash whose type differs per transliterating language. It should not be labelled safety- or liveness-critical.

The problems

1. Slot.is_justifiable_after guarded self >= finalized_slot with a bare assert. Not reachable with a bad value in the honest flow (all callers guard it), but a public partial function that crashes rather than answering.
2. process_attestations unpacked the flat justification vote list with batched(..., validator_count) and zip(..., strict=True), plus a bare zero-hash assert. A validly SSZ-decoded State can still violate the cross-field invariant that the vote list is exactly one registry-sized segment per tracked root — the State container has no cross-field length validator — so a state from untrusted bytes could crash here with an untyped ValueError, and a non-multiple length could even produce a silently short final segment.

The fix

• is_justifiable_after is now total: it returns False for any slot before the finalized boundary. The equal-slot case still returns True via the immediate-justification window. The misleading Raises clause is gone.
• process_attestations validates the justification bookkeeping before the unpack, with typed rejections:
  • empty validator registry (reuses EMPTY_VALIDATOR_REGISTRY; belt-and-suspenders, since the header stage already rejects this first),
  • vote-list length not equal to tracked-root count times validator count (new JUSTIFICATION_VOTES_LENGTH_MISMATCH),
  • a zero hash among the tracked roots (new ZERO_HASH_JUSTIFICATION_ROOT).
  • zip(strict=True) is kept as a cheap belt-and-suspenders behind the guards.

This follows the existing reference pattern in this repo — ValidatorIndex.proposer_for_slot already rejects an empty registry with a typed SpecRejectionError.

Tests

Consensus vectors only, per the forks-are-vectors rule (no pytests, no tests/spec/forks/ tree):

• Justifiability gains two cases below the finalized boundary (delta -1 and -10, is_justifiable=false), which the previous assert could not emit at all.
• Two state_transition rejection vectors craft a decoded State that violates the length invariant and one that carries a zero-hash root, each asserting the full rejection message with string equality.

The empty-registry guard inside attestation processing is unreachable through any vector (the header proposer guard intercepts first) and pytest is disallowed for forks, so it stays as documented belt-and-suspenders; the reachable header path is already covered elsewhere.

uv run fill generates the new fixtures deterministically, and just check passes.

Credit

Found via the Lean 4 formalization of this spec (NyxFoundation/formal-leanSpec): these are the call sites where the proofs needed an explicit side hypothesis to discharge — the tell-tale of an implicit precondition.

Closes #1174

🤖 Generated with Claude Code