feat(val): re-align VAL-2 checked insertion with merged leanSpec#1185

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

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,17 +388,18 @@ 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
     theorem dual_key_distinct (vid : ValidatorIndex) (reg : KeyRegistry) :
         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**