From 587d5b7f6fe246a63236932886cb9e8b464dbb87 Mon Sep 17 00:00:00 2001 From: adust09 Date: Fri, 3 Jul 2026 01:03:59 +0900 Subject: [PATCH 1/2] feat(val): prove VAL-1 proposers are selected round-robin Extract ValidatorIndex.proposerForSlot mirroring proposer_for_slot in upstream containers/identifiers.py and refactor processBlockHeader's proposer check to consume it (semantics unchanged: the UInt64 construction never wraps since slot % n <= slot < 2^64, recorded as proposerForSlot_toNat). Prove proposer_index_round_robin, the catalog form of the round-robin selection. Axiom-free, no Mathlib. --- LeanSpec.lean | 1 + .../Forks/Lstar/Containers/Identifiers.lean | 49 +++++++++++++++++++ LeanSpec/Forks/Lstar/StateTransition.lean | 5 +- docs/lean4-proof-propositions.md | 13 +++-- 4 files changed, 61 insertions(+), 7 deletions(-) create mode 100644 LeanSpec/Forks/Lstar/Containers/Identifiers.lean diff --git a/LeanSpec.lean b/LeanSpec.lean index 3306163..71cfbdb 100644 --- a/LeanSpec.lean +++ b/LeanSpec.lean @@ -4,6 +4,7 @@ import LeanSpec.Forks.Lstar.Containers.Attestation import LeanSpec.Forks.Lstar.Containers.Block import LeanSpec.Forks.Lstar.Containers.Checkpoint import LeanSpec.Forks.Lstar.Containers.Genesis +import LeanSpec.Forks.Lstar.Containers.Identifiers import LeanSpec.Forks.Lstar.Containers.State import LeanSpec.Forks.Lstar.Containers.Validator import LeanSpec.Forks.Lstar.Errors diff --git a/LeanSpec/Forks/Lstar/Containers/Identifiers.lean b/LeanSpec/Forks/Lstar/Containers/Identifiers.lean new file mode 100644 index 0000000..8e8f564 --- /dev/null +++ b/LeanSpec/Forks/Lstar/Containers/Identifiers.lean @@ -0,0 +1,49 @@ +/- +Scalar identifiers naming validators and the registry index space. + +Mirrors `src/lean_spec/spec/forks/lstar/containers/identifiers.py` in +leanSpec: + - `ValidatorIndex.proposer_for_slot(slot, num_validators)`: round-robin + proposer selection — the proposer is `slot % num_validators`. Upstream + raises `EMPTY_VALIDATOR_REGISTRY` for an empty registry; in Lean the + callers guard (`processBlockHeader` rejects before selecting). + +`SubnetId` / `compute_subnet_id` and `is_within_registry` are added when a +proposition consumes them. + +Proves VAL-1 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. +-/ + +import LeanSpec.Aliases + +namespace LeanSpec.Forks.Lstar + +namespace ValidatorIndex + +/-- Round-robin proposer selection (`proposer_for_slot`): the validator +responsible for proposing at `slot` in a registry of `numValidators`. -/ +def proposerForSlot (slot : Slot) (numValidators : Nat) : ValidatorIndex := + UInt64.ofNat (slot.toNat % numValidators) + +/-- VAL-1: proposers are selected round-robin. The catalog's +`ValidatorIndex.mk` is realized as `UInt64.ofNat` (`ValidatorIndex` is a +`Uint64`, as upstream). -/ +theorem proposer_index_round_robin (slot : Slot) (n : Nat) (_h : 0 < n) : + proposerForSlot slot n = UInt64.ofNat (slot.toNat % n) := rfl + +/-- The round-robin index at the `Nat` level: the `UInt64` construction +never wraps, since `slot % n ≤ slot < 2^64`. -/ +theorem proposerForSlot_toNat (slot : Slot) (n : Nat) : + (proposerForSlot slot n).toNat = slot.toNat % n := by + have h1 : slot.toNat % n ≤ slot.toNat := Nat.mod_le _ _ + have h2 : slot.toNat < 2 ^ 64 := slot.toNat_lt + have h3 : UInt64.size = 2 ^ 64 := rfl + exact UInt64.toNat_ofNat_of_lt' (by omega) + +end ValidatorIndex + +end LeanSpec.Forks.Lstar diff --git a/LeanSpec/Forks/Lstar/StateTransition.lean b/LeanSpec/Forks/Lstar/StateTransition.lean index 849a7c9..2243626 100644 --- a/LeanSpec/Forks/Lstar/StateTransition.lean +++ b/LeanSpec/Forks/Lstar/StateTransition.lean @@ -59,6 +59,7 @@ exactly what reachability from genesis guarantees (ST-4's `Reachable`). -/ import LeanSpec.Forks.Lstar.Config +import LeanSpec.Forks.Lstar.Containers.Identifiers import LeanSpec.Forks.Lstar.Containers.State import LeanSpec.Forks.Lstar.Errors @@ -154,9 +155,9 @@ def processBlockHeader (s : State) (b : Block) : ST.Result State := .error .headerSlotNotNewer else if s.validators.size = 0 then .error .emptyValidatorRegistry - else if b.proposerIndex.toNat ≠ b.slot.toNat % s.validators.size then + else if b.proposerIndex ≠ ValidatorIndex.proposerForSlot b.slot s.validators.size then .error (.proposerMismatch - (UInt64.ofNat (b.slot.toNat % s.validators.size)) b.proposerIndex) + (ValidatorIndex.proposerForSlot b.slot s.validators.size) b.proposerIndex) else -- Genesis is justified and finalized by definition, so the first block -- forces its parent to both; later blocks keep their checkpoints. diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index 3278971..43ba1f9 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 | 0 | 5 | 0 | 5 | -| VAL | 0 | 5 | 0 | 5 | +| VAL | 1 | 4 | 0 | 5 | | NET | 0 | 2 | 0 | 2 | | STOR | 0 | 2 | 0 | 2 | | SYNC | 0 | 2 | 0 | 2 | -| **Total** | **14** | **16** | **1** | **31** | +| **Total** | **15** | **15** | **1** | **31** | ## SSZ & primitive types @@ -348,14 +348,17 @@ A **Validator** is an entity that stakes ETH and participates in consensus. At e The propositions here guarantee **duty correctness and slashing prevention**: proposer selection is round-robin via `slot mod n`, with exactly one proposer per slot; the proposal key and attestation key are distinct (so key compromise stays local); no double-voting in the same slot (double voting is slashable); the stateful XMSS signing key never moves its used index backwards (key reuse leaks the secret key); and so on. These are the conditions for a validator to avoid penalties while letting the network advance safely. Implementations live in `LeanSpec/Validator/*`. -- [ ] **VAL-1: Proposers are selected round-robin** - - Source: `proposer_index` (in `process_block_header`) +- [x] **VAL-1: Proposers are selected round-robin** + - Source: `proposer_index` (in `process_block_header`; realized as `ValidatorIndex.proposer_for_slot` in `src/lean_spec/spec/forks/lstar/containers/identifiers.py`) - Note: Returns the proposer index for a given slot from the slot and the number of active validators `n` (round-robin). - - Sample code: + - Proved at: `LeanSpec/Forks/Lstar/Containers/Identifiers.lean` (`ValidatorIndex.proposer_index_round_robin`; `proposerForSlot_toNat` shows the `UInt64` construction never wraps). `processBlockHeader` consumes `proposerForSlot`, so the theorem speaks about the deployed selection. + - Sample code (`proposerFor` realized as `proposerForSlot` mirroring the Python name; `ValidatorIndex.mk` as `UInt64.ofNat`): ```lean theorem proposer_index_round_robin (slot : Slot) (n : Nat) (h : 0 < n) : ValidatorIndex.proposerFor slot n = ValidatorIndex.mk (slot.toNat % n) := by sorry + -- ✅ proved in LeanSpec/Forks/Lstar/Containers/Identifiers.lean as + -- `ValidatorIndex.proposer_index_round_robin` ``` - [ ] **VAL-2: Proposal key and attestation key are distinct** From 32e3aaec67fa3bef3308084116890838ad898178 Mon Sep 17 00:00:00 2001 From: adust09 Date: Fri, 3 Jul 2026 01:06:21 +0900 Subject: [PATCH 2/2] feat(val): prove VAL-3 each slot has exactly one proposer Define isProposerFor (equality with the round-robin index, phrased on Fin n so registry membership is carried by the type) and prove unique_proposer: the proposer slot % n exists and any proposer equals it. The catalog's exists-unique is written in expanded form since ExistsUnique is Mathlib-only. Axiom-free. --- .../Forks/Lstar/Containers/Identifiers.lean | 21 ++++++++++++++++++- docs/lean4-proof-propositions.md | 11 ++++++---- 2 files changed, 27 insertions(+), 5 deletions(-) diff --git a/LeanSpec/Forks/Lstar/Containers/Identifiers.lean b/LeanSpec/Forks/Lstar/Containers/Identifiers.lean index 8e8f564..cf3c545 100644 --- a/LeanSpec/Forks/Lstar/Containers/Identifiers.lean +++ b/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 diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index 43ba1f9..b47a0ea 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 | 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**