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

LeanSpec.lean

@@ -22,3 +22,4 @@ import LeanSpec.SSZ.Hash
 import LeanSpec.SSZ.Uint64
 import LeanSpec.SSZ.Utils
 import LeanSpec.SSZ.Vector
+import LeanSpec.Validator.Service

LeanSpec/Validator/Service.lean

@@ -0,0 +1,121 @@
+/-
+Validator attestation duty gate.
+
+Mirrors the attestation arm of `ValidatorService.run` in
+`src/lean_spec/node/validator/service.py` (post
+leanEthereum/leanSpec#1180, which typed the duty-path errors):
+  - `_attested_slots` — slots this service has already attested,
+    service-wide: one attestation pass covers every validator the node
+    manages, so the gate is per service, not per validator.
+  - the duty gate — attest only from interval 1 on, only when synced
+    for duties, and only when the slot is not already attested; a gated
+    slot stays unattested and retries on a later pass.
+  - the retention prune — after attesting, slots older than
+    `ATTESTED_SLOT_RETENTION` below the current slot are dropped to
+    bound memory (`max(0, slot - retention)`; the truncated `Nat`
+    subtraction is Python's clamp).
+
+The service around the gate is node runtime: the async clock loop, the
+sync service, the gossip publishers, and the metrics counters. The
+gate's two inputs from that runtime — the current interval and the
+`_is_synced_for_duties` verdict — enter as plain arguments, and the
+attestation production itself (signing, local import, publishing) is IO
+outside the modeled state step.
+
+Proves VAL-4 from `docs/lean4-proof-propositions.md`:
+  - VAL-4: double-voting in the same slot is impossible — the duty gate
+    never fires for an already-attested slot (`no_double_vote`); a
+    fired duty records its slot through the retention prune
+    (`attested_after_duty`); hence the gate can never fire twice for
+    one slot (`no_double_vote_after`).
+-/
+
+import LeanSpec.Forks.Lstar.Containers.Interval
+
+namespace LeanSpec.Validator
+
+open LeanSpec.Forks.Lstar (Interval)
+
+/-- Slots an attested slot is retained for after its own
+(`ATTESTED_SLOT_RETENTION`, an `int` upstream, defined in
+`service.py`). -/
+def ATTESTED_SLOT_RETENTION : Nat := 4
+
+/-- The duty-relevant validator-service state: the slots this service
+has already attested (`_attested_slots`). The runtime fields are IO —
+see the module docstring. -/
+structure ValidatorService where
+  attestedSlots : List Slot
+  deriving Inhabited, Repr
+
+namespace ValidatorService
+
+/-- Drop attested slots too old to attest again
+(`prune_threshold = Slot(max(0, int(slot) - ATTESTED_SLOT_RETENTION))`,
+then keep the slots at or above it). -/
+def pruneAttested (slot : Slot) (attested : List Slot) : List Slot :=
+  let threshold : Slot := UInt64.ofNat (slot.toNat - ATTESTED_SLOT_RETENTION)
+  attested.filter (fun s => threshold ≤ s)
+
+/-- Whether the attestation duty fires (`run`'s gate): from interval 1
+on, at most once per slot, and only when synced for duties. -/
+def attestationDue (svc : ValidatorService) (slot : Slot)
+    (interval : Interval) (synced : Bool) : Bool :=
+  decide ((1 : Interval) ≤ interval) &&
+  !(svc.attestedSlots.contains slot) &&
+  synced
+
+/-- One pass of the attestation arm of the duty loop: `none` when the
+gate holds the duty back (upstream falls through and may retry the slot
+on a later pass), `some` with the slot recorded and the retention
+window pruned when the duty fires. -/
+def attestationDutyStep (svc : ValidatorService) (slot : Slot)
+    (interval : Interval) (synced : Bool) : Option ValidatorService :=
+  if attestationDue svc slot interval synced then
+    some { svc with
+      attestedSlots := pruneAttested slot (slot :: svc.attestedSlots) }
+  else
+    none
+
+/-- VAL-4: the duty gate never fires for an already-attested slot — a
+second attestation for the same slot is impossible. -/
+theorem no_double_vote (svc : ValidatorService) (slot : Slot)
+    (interval : Interval) (synced : Bool)
+    (hin : svc.attestedSlots.contains slot = true) :
+    attestationDutyStep svc slot interval synced = none := by
+  unfold attestationDutyStep attestationDue
+  rw [hin]
+  simp
+
+/-- The freshly attested slot survives its own retention prune: the
+threshold sits at or below the slot itself. -/
+theorem attested_after_duty (svc svc' : ValidatorService) (slot : Slot)
+    (interval : Interval) (synced : Bool)
+    (h : attestationDutyStep svc slot interval synced = some svc') :
+    svc'.attestedSlots.contains slot = true := by
+  unfold attestationDutyStep at h
+  split at h
+  · injection h with h'
+    subst h'
+    have hth : (UInt64.ofNat (slot.toNat - ATTESTED_SLOT_RETENTION)) ≤ slot := by
+      have hlt := slot.toNat_lt
+      have hsz : UInt64.size = 2 ^ 64 := rfl
+      rw [UInt64.le_iff_toNat_le, UInt64.toNat_ofNat_of_lt' (by omega)]
+      omega
+    show (pruneAttested slot (slot :: svc.attestedSlots)).contains slot = true
+    unfold pruneAttested
+    rw [List.contains_iff_mem]
+    exact List.mem_filter.mpr ⟨List.mem_cons_self, by simpa using hth⟩
+  · exact absurd h (by simp)
+
+/-- VAL-4, sharpened: once the duty fired for a slot, no later pass can
+fire for that slot again — regardless of interval or sync verdict. -/
+theorem no_double_vote_after (svc svc' : ValidatorService) (slot : Slot)
+    (interval interval' : Interval) (synced synced' : Bool)
+    (h : attestationDutyStep svc slot interval synced = some svc') :
+    attestationDutyStep svc' slot interval' synced' = none :=
+  no_double_vote svc' slot interval' synced'
+    (attested_after_duty svc svc' slot interval synced h)
+
+end ValidatorService
+end LeanSpec.Validator

docs/lean4-proof-propositions.md

@@ -72,11 +72,11 @@ Format: `<DOMAIN>-<number>`. `DOMAIN` is the abbreviation of the owning area:
 | CONT | 2 | 0 | 0 | 2 |
 | ST | 6 | 0 | 0 | 6 |
 | FC | 5 | 0 | 0 | 5 |
-| VAL | 2 | 3 | 0 | 5 |
+| VAL | 3 | 2 | 0 | 5 |
 | NET | 0 | 2 | 0 | 2 |
 | STOR | 0 | 2 | 0 | 2 |
 | SYNC | 0 | 2 | 0 | 2 |
-| **Total** | **21** | **9** | **1** | **31** |
+| **Total** | **22** | **8** | **1** | **31** |
 
 ## SSZ & primitive types
 
@@ -409,9 +409,10 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr
     --    `ValidatorIndex.unique_proposer` (∃! expanded: ∃ vid, P vid ∧ ∀ vid', P vid' → vid' = vid)
     ```
 
-- [ ] **VAL-4: Double-voting in the same slot is impossible**
-  - Source: `ValidatorService.produce_attestation`
-  - Note: Checks the local history for "already attested in this slot"; produces a new attestation only if not yet voted (fails when it would be a double vote).
+- [x] **VAL-4: Double-voting in the same slot is impossible**
+  - Source: `ValidatorService.produce_attestation` (realized as the attestation arm of `ValidatorService.run` in `src/lean_spec/node/validator/service.py`: the duty gate over the service-wide `_attested_slots` set)
+  - Note: Checks the local history for "already attested in this slot"; produces a new attestation only if not yet voted. Upstream tracks attested slots per service — one attestation pass covers every validator the node manages — and the gate silently skips rather than failing, retrying gated slots on later passes; modeled as `attestationDutyStep = none`.
+  - Proved at: `LeanSpec/Validator/Service.lean` (`ValidatorService.no_double_vote`; `attested_after_duty` shows a fired duty records its slot through the retention prune, and `no_double_vote_after` sharpens VAL-4 to "once fired, never again for that slot")
   - Sample code:
 
     ```lean
@@ -420,6 +421,10 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr
         (hin : slot ∈ svc.attestedSlots vid)
         (h : ValidatorService.produceAttestation svc vid slot = .ok svc') :
         False := by sorry
+    -- ✅ proved in LeanSpec/Validator/Service.lean as
+    --    `ValidatorService.no_double_vote` (the attested set is
+    --    service-wide upstream, not per validator, and the gate skips
+    --    instead of erroring: `attestationDutyStep ... = none`)
     ```
 
 - [ ] **VAL-5: XMSS preparation state is monotonically increasing**