feat(val): prove VAL-3 each slot has exactly one proposer

LeanSpec/Forks/Lstar/Containers/Identifiers.lean

@@ -11,11 +11,12 @@ leanSpec:
 `SubnetId` / `compute_subnet_id` and `is_within_registry` are added when a
 proposition consumes them.
 
-Proves VAL-1 from `docs/lean4-proof-propositions.md`:
+Proves VAL-1 and VAL-3 from `docs/lean4-proof-propositions.md`:
   - VAL-1: proposers are selected round-robin —
     `proposerForSlot slot n` is the validator index `slot % n`
     (`proposer_index_round_robin`), with the `toNat`-level corollary
     showing the `UInt64` construction never wraps.
+  - VAL-3: each slot has exactly one proposer (`unique_proposer`).
 -/
 
 import LeanSpec.Aliases
@@ -44,6 +45,24 @@ theorem proposerForSlot_toNat (slot : Slot) (n : Nat) :
   have h3 : UInt64.size = 2 ^ 64 := rfl
   exact UInt64.toNat_ofNat_of_lt' (by omega)
 
+/-- Whether validator `vid`, in a registry of `n` validators, is the
+scheduled proposer of `slot` (`is_proposer`: equality with
+`proposer_for_slot`). Phrased on `Fin n` so registry membership is carried
+by the type, per the catalog. -/
+def isProposerFor {n : Nat} (vid : Fin n) (slot : Slot) : Prop :=
+  vid.val = slot.toNat % n
+
+/-- VAL-3: each slot has exactly one proposer — the round-robin index
+exists and any proposer equals it. The catalog's `∃!` is written in its
+expanded form (`ExistsUnique` lives in Mathlib, which this repo does not
+depend on). -/
+theorem unique_proposer (slot : Slot) (n : Nat) (h : 0 < n) :
+    ∃ vid : Fin n, isProposerFor vid slot ∧
+      ∀ vid' : Fin n, isProposerFor vid' slot → vid' = vid := by
+  refine ⟨⟨slot.toNat % n, Nat.mod_lt _ h⟩, rfl, ?_⟩
+  intro vid hvid
+  exact Fin.ext hvid
+
 end ValidatorIndex
 
 end LeanSpec.Forks.Lstar

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 | 0 | 5 | 0 | 5 |
-| VAL | 1 | 4 | 0 | 5 |
+| VAL | 2 | 3 | 0 | 5 |
 | NET | 0 | 2 | 0 | 2 |
 | STOR | 0 | 2 | 0 | 2 |
 | SYNC | 0 | 2 | 0 | 2 |
-| **Total** | **15** | **15** | **1** | **31** |
+| **Total** | **16** | **14** | **1** | **31** |
 
 ## SSZ & primitive types
 
@@ -371,14 +371,17 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr
         reg.proposalKey vid ≠ reg.attestationKey vid := by sorry
     ```
 
-- [ ] **VAL-3: Each slot has exactly one proposer**
-  - Source: `is_proposer` / `proposer_index` (ValidatorService)
+- [x] **VAL-3: Each slot has exactly one proposer**
+  - Source: `is_proposer` / `proposer_index` (ValidatorService; the check in use is equality with `proposer_for_slot`, e.g. in `validator_duties.py`)
   - Note: Decides whether validator `vid` is the proposer of `slot` (equivalent to `vid = slot mod n`).
+  - Proved at: `LeanSpec/Forks/Lstar/Containers/Identifiers.lean` (`ValidatorIndex.unique_proposer`; `∃!` written in expanded form since `ExistsUnique` is Mathlib-only)
   - Sample code:
 
     ```lean
     theorem unique_proposer (slot : Slot) (n : Nat) (h : 0 < n) :
         ∃! vid : Fin n, ValidatorIndex.isProposerFor vid slot := by sorry
+    -- ✅ proved in LeanSpec/Forks/Lstar/Containers/Identifiers.lean as
+    --    `ValidatorIndex.unique_proposer` (∃! expanded: ∃ vid, P vid ∧ ∀ vid', P vid' → vid' = vid)
     ```
 
 - [ ] **VAL-4: Double-voting in the same slot is impossible**