From 9c5d965d04251ff0920e5173a6f46732a47814d5 Mon Sep 17 00:00:00 2001 From: adust09 Date: Mon, 6 Jul 2026 00:53:10 +0900 Subject: [PATCH] feat(val): prove VAL-4 double-voting in the same slot is impossible Open the Validator domain: LeanSpec/Validator/Service.lean models the attestation arm of ValidatorService.run (node/validator/service.py, post leanEthereum/leanSpec#1180). Upstream guards double voting with the service-wide _attested_slots set - one attestation pass covers every validator the node manages - and the gate silently skips an already-attested slot rather than failing, retrying gated slots on later passes. The retention prune (max(0, slot - 4)) bounds the set. The runtime around the gate (async clock loop, sync service, gossip publishers, counters) is IO; the gate's inputs from it - the current interval and the _is_synced_for_duties verdict - enter as arguments. no_double_vote: the gate never fires for an attested slot. attested_after_duty: a fired duty records its slot through the prune. no_double_vote_after: once fired, never again for that slot. --- LeanSpec.lean | 1 + LeanSpec/Validator/Service.lean | 121 +++++++++++++++++++++++++++++++ docs/lean4-proof-propositions.md | 15 ++-- 3 files changed, 132 insertions(+), 5 deletions(-) create mode 100644 LeanSpec/Validator/Service.lean diff --git a/LeanSpec.lean b/LeanSpec.lean index 44c4a7a..2e7c7fc 100644 --- a/LeanSpec.lean +++ b/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 diff --git a/LeanSpec/Validator/Service.lean b/LeanSpec/Validator/Service.lean new file mode 100644 index 0000000..f0e910b --- /dev/null +++ b/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 diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index b326218..29e964f 100644 --- a/docs/lean4-proof-propositions.md +++ b/docs/lean4-proof-propositions.md @@ -72,11 +72,11 @@ Format: `-`. `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**