From 2b41b036a752f7c43a060cf38ce127a7bb56212d Mon Sep 17 00:00:00 2001 From: adust09 Date: Mon, 20 Jul 2026 20:08:49 +0900 Subject: [PATCH] feat(val): re-align VAL-2 checked insertion with merged leanSpec#1185 Upstream leanEthereum/leanSpec#1185 (closes #1184) now rejects a manifest whose attestation and proposal public keys coincide, at load time and without touching secret bytes. The model's addChecked previously compared PRF seeds as a placeholder for the invited fix; re-align it with the merged shape: - addChecked now compares public keys, with the Arklib-side derivation entering as the publicKeyOf parameter (the repo's crypto-as-parameter pattern). - addChecked_wellFormed holds for every derivation: distinct public keys imply distinct secret keys by congruence alone. - addChecked_seed_distinct keeps the OTS-reuse core of #1184: for seed-fingerprinting derivations an accepted entry's keys have distinct master seeds. - Registry.lean and catalog docstrings drop the stale 'upstream does not enforce' caveat: WellFormed is established by construction since #1185. --- LeanSpec/Validator/Registry.lean | 103 ++++++++++++++++++++----------- docs/lean4-proof-propositions.md | 11 ++-- 2 files changed, 72 insertions(+), 42 deletions(-) diff --git a/LeanSpec/Validator/Registry.lean b/LeanSpec/Validator/Registry.lean index c6ae6e6..2275f7f 100644 --- a/LeanSpec/Validator/Registry.lean +++ b/LeanSpec/Validator/Registry.lean @@ -11,15 +11,19 @@ Mirrors `src/lean_spec/node/validator/registry.py`: `entry.index` at every insertion site, so the model stores the entries directly and looks them up by their own index. -Upstream states the dual-key separation but does not enforce it: -`add` is a bare assignment and `from_yaml` raises only for missing -files and decode failures — a same-key manifest loads silently and -then signs a proposal and an attestation for one slot with one -stateful XMSS key (OTS state reuse; found by attempting VAL-2, an -"invariant maintained only by convention" of the same class as -leanEthereum/leanSpec#1176, reported as #1184). The distinctness -therefore enters as `WellFormed`, and `WellFormed.add` shows the -suggested fix — validating at insertion — preserves it. +Upstream originally stated the dual-key separation but did not +enforce it: `add` was a bare assignment and `from_yaml` raised only +for missing files and decode failures — a same-key manifest loaded +silently and then signed a proposal and an attestation for one slot +with one stateful XMSS key (OTS state reuse; found by attempting +VAL-2, an "invariant maintained only by convention" of the same class +as leanEthereum/leanSpec#1176, reported as #1184). Since +leanEthereum/leanSpec#1185 the loader rejects such a manifest by +comparing its two public keys (the secret bytes stay untouched), so +every loaded registry satisfies the distinctness by construction. +The distinctness enters the theorems as `WellFormed`; `WellFormed.add` +shows unchecked insertion preserves it, and `addChecked` mirrors the +merged load-time check. Proves VAL-2 from `docs/lean4-proof-propositions.md`: - VAL-2: on a well-formed registry, every lookup returns an entry @@ -63,11 +67,11 @@ def get? (reg : ValidatorRegistry) (index : ValidatorIndex) : Option ValidatorEntry := reg.validators.find? (fun e => e.index == index) -/-- The dual-key separation `ValidatorEntry` documents but upstream -does not enforce: every entry's proposal key differs from its -attestation key. A same-key entry would let one slot's proposal and -attestation signatures consume overlapping XMSS one-time-signature -state (see the module docstring). -/ +/-- The dual-key separation `ValidatorEntry` documents and the loader +enforces since leanEthereum/leanSpec#1185: every entry's proposal key +differs from its attestation key. A same-key entry would let one +slot's proposal and attestation signatures consume overlapping XMSS +one-time-signature state (see the module docstring). -/ def WellFormed (reg : ValidatorRegistry) : Prop := ∀ e ∈ reg.validators, e.proposalSecretKey ≠ e.attestationSecretKey @@ -93,36 +97,42 @@ theorem WellFormed.add (reg : ValidatorRegistry) (entry : ValidatorEntry) | inl heq => rw [heq]; exact hentry | inr hmem => exact hwf e (List.mem_filter.mp hmem).1 -/-! ## Checked insertion (the fix shape of leanEthereum/leanSpec#1184) - -Tracks the fix suggested in leanEthereum/leanSpec#1184 (invited by the -maintainers): reject a same-key entry where the check is one -comparison, at insertion. Every one-time key of an XMSS secret key -derives from its master PRF seed, so two keys collide in OTS state -exactly when their seeds coincide — the check compares the seeds -(upstream will compare the manifest's two public keys, which -equivalently fingerprint the seeds). Re-align the shape with the merged -fix when it lands upstream. -/ - -/-- Add a validator entry only when its two keys are distinct — the -load-time validation of leanEthereum/leanSpec#1184. `none` mirrors the -`ValueError` the loader raises on a same-seed manifest. -/ -def addChecked (reg : ValidatorRegistry) (entry : ValidatorEntry) : +/-! ## Checked insertion (the merged fix of leanEthereum/leanSpec#1185) + +Mirrors the fix merged upstream as leanEthereum/leanSpec#1185 (closes +#1184): `from_yaml` rejects a manifest entry whose attestation and +proposal public keys coincide, before any secret key is decoded. The +public-key derivation is Arklib-side crypto, so it enters the model as +the `publicKeyOf` parameter. Distinct public keys imply distinct +secret keys for *every* derivation (a function maps equal inputs to +equal outputs), so `WellFormed` follows with no cryptographic +assumption; the OTS-level content — distinct master seeds — follows +for derivations that fingerprint the seed +(`addChecked_seed_distinct`). -/ + +/-- Add a validator entry only when its two public keys differ — the +load-time validation of leanEthereum/leanSpec#1185. `none` mirrors the +`ValueError` the loader raises on a same-key manifest; the comparison +touches only public material. -/ +def addChecked (publicKeyOf : SecretKey → ByteArray) + (reg : ValidatorRegistry) (entry : ValidatorEntry) : Option ValidatorRegistry := - if entry.proposalSecretKey.prfKey.data == - entry.attestationSecretKey.prfKey.data then + if (publicKeyOf entry.attestationSecretKey).data == + (publicKeyOf entry.proposalSecretKey).data then none else some (reg.add entry) /-- The checked insertion discharges the `WellFormed` distinctness at -construction: an accepted entry passed the seed comparison, and keys -sharing no seed are distinct. Once upstream enforces the check, every -loaded registry is well-formed by construction — closing the loop the -way leanEthereum/leanSpec#1179 did for the store invariants. -/ -theorem addChecked_wellFormed (reg reg' : ValidatorRegistry) +construction, for every public-key derivation: an accepted entry has +distinct public keys, and equal secret keys cannot derive distinct +public keys. Upstream now enforces the check, so every loaded registry +is well-formed by construction — closing the loop the way +leanEthereum/leanSpec#1179 did for the store invariants. -/ +theorem addChecked_wellFormed (publicKeyOf : SecretKey → ByteArray) + (reg reg' : ValidatorRegistry) (entry : ValidatorEntry) (hwf : WellFormed reg) - (h : addChecked reg entry = some reg') : + (h : addChecked publicKeyOf reg entry = some reg') : WellFormed reg' := by unfold addChecked at h split at h @@ -133,5 +143,24 @@ theorem addChecked_wellFormed (reg reg' : ValidatorRegistry) exact WellFormed.add reg entry hwf fun hc => hne (by rw [hc]; exact beq_self_eq_true _) +/-- The OTS-reuse core of leanEthereum/leanSpec#1184: when the +derivation fingerprints the master seed (Arklib derives the public +root from the PRF seed), an accepted entry's two keys have distinct +seeds, so one slot's proposal and attestation signatures can never +consume overlapping one-time-signature state. -/ +theorem addChecked_seed_distinct (publicKeyOf : SecretKey → ByteArray) + (hdet : ∀ k₁ k₂ : SecretKey, k₁.prfKey.data = k₂.prfKey.data → + publicKeyOf k₁ = publicKeyOf k₂) + (reg reg' : ValidatorRegistry) (entry : ValidatorEntry) + (h : addChecked publicKeyOf reg entry = some reg') : + entry.proposalSecretKey.prfKey.data ≠ + entry.attestationSecretKey.prfKey.data := by + unfold addChecked at h + split at h + · simp at h + · next hne => + intro hseed + exact hne (by rw [hdet _ _ hseed]; exact beq_self_eq_true _) + end ValidatorRegistry end LeanSpec.Validator diff --git a/docs/lean4-proof-propositions.md b/docs/lean4-proof-propositions.md index 6784a95..e87bd44 100644 --- a/docs/lean4-proof-propositions.md +++ b/docs/lean4-proof-propositions.md @@ -1,6 +1,6 @@ --- title: leanSpec → Lean4 Theorem Proving Proposition Catalog -last_updated: 2026-07-05 +last_updated: 2026-07-20 tags: - lean4 - formal-verification @@ -388,8 +388,8 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr - [x] **VAL-2: Proposal key and attestation key are distinct** - Source: `proposalKey` / `attestationKey` (ValidatorService; realized as the `attestation_secret_key` / `proposal_secret_key` fields of `ValidatorEntry`, `src/lean_spec/node/validator/registry.py`) - - Note: Each validator manages two separate signing keys, one for block proposal and one for attestations — documented upstream as "without OTS conflict", but **not enforced**: `ValidatorRegistry.add` assigns without validation and `from_yaml` compares nothing, so a same-key manifest loads silently and one slot's proposal + attestation signatures would consume overlapping XMSS one-time-signature state. Found by attempting this proposition; reported upstream as leanEthereum/leanSpec#1184 (the "invariant maintained only by convention" class of #1176). The theorem is therefore proved relative to `ValidatorRegistry.WellFormed`. - - Proved at: `LeanSpec/Validator/Registry.lean` (`ValidatorRegistry.dual_key_distinct`, relative to `WellFormed`; `WellFormed.add` shows the suggested fix — validate at insertion — preserves the invariant) + - Note: Each validator manages two separate signing keys, one for block proposal and one for attestations — documented upstream as "without OTS conflict". Originally **not enforced** (`ValidatorRegistry.add` assigned without validation, `from_yaml` compared nothing, so a same-key manifest loaded silently and one slot's proposal + attestation signatures would consume overlapping XMSS one-time-signature state); found by attempting this proposition and reported upstream as leanEthereum/leanSpec#1184 (the "invariant maintained only by convention" class of #1176). **Enforced since leanEthereum/leanSpec#1185**: the loader rejects a manifest whose two public keys coincide, before touching secret bytes, so every loaded registry satisfies `WellFormed` by construction. + - Proved at: `LeanSpec/Validator/Registry.lean` (`ValidatorRegistry.dual_key_distinct`, relative to `WellFormed`; `WellFormed.add` shows unchecked insertion preserves the invariant; `addChecked` mirrors the merged #1185 public-key check with the derivation as a parameter — `addChecked_wellFormed` for every derivation, `addChecked_seed_distinct` for seed-fingerprinting ones) - Sample code: ```lean @@ -397,8 +397,9 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr reg.proposalKey vid ≠ reg.attestationKey vid := by sorry -- ✅ proved in LeanSpec/Validator/Registry.lean as -- `ValidatorRegistry.dual_key_distinct` (relative to - -- `ValidatorRegistry.WellFormed` — upstream does not enforce the - -- distinctness, so it cannot be derived from construction) + -- `ValidatorRegistry.WellFormed` — established at load time by + -- upstream since leanEthereum/leanSpec#1185, mirrored as + -- `addChecked_wellFormed`) ``` - [x] **VAL-3: Each slot has exactly one proposer**