feat(val): prove VAL-4 double-voting in the same slot is impossible

[adust09]

Summary

Opens the Validator domain (LeanSpec/Validator/) with VAL-4, modeling the attestation duty gate of ValidatorService.run (src/lean_spec/node/validator/service.py, post leanEthereum/leanSpec#1180).

Upstream reality vs the catalog sample

The catalog sample imagined a per-validator attestedSlots map and an erroring produceAttestation. Upstream instead:

• tracks attested slots per service (_attested_slots) — one attestation pass covers every validator the node manages
• the gate silently skips an already-attested slot (no error), and a gated slot retries on a later pass
• after firing, a retention prune (max(0, slot - ATTESTED_SLOT_RETENTION), retention = 4) bounds the set

The model mirrors that shape; the catalog entry documents the divergence.

What is modeled

• ValidatorService — the duty-relevant state (_attested_slots); the async runtime (clock loop, sync service, publishers, counters) is IO, its two gate inputs (current interval, _is_synced_for_duties verdict) enter as arguments
• attestationDue — the gate: from interval 1 on, at most once per slot, only when synced
• attestationDutyStep — one pass: none when gated, some with the slot recorded and the window pruned when the duty fires
• pruneAttested — truncated-Nat subtraction mirrors Python's max(0, ·) clamp

Theorems

• no_double_vote (VAL-4) — the gate never fires for an already-attested slot
• attested_after_duty — a fired duty records its slot (the fresh slot survives its own retention prune)
• no_double_vote_after — sharpened VAL-4: once fired for a slot, no later pass can fire for it again, regardless of interval or sync verdict

Catalog: VAL-4 checked, progress table 22/8/1 (VAL 3 proved / 2 open — remaining: VAL-2 dual keys, VAL-5 XMSS preparation monotonicity). lake build passes with no sorry.