From f38564bcd0b77dc3a298d5e4eb14c53c0eebab2f Mon Sep 17 00:00:00 2001
From: adust09 <shoukitsuda@icloud.com>
Date: Mon, 6 Jul 2026 23:57:12 +0900
Subject: [PATCH] feat(val): add checked registry insertion tracking
 leanSpec#1184

The maintainers invited a fix PR for leanEthereum/leanSpec#1184; this
prepares the Lean side of that loop. addChecked rejects a same-seed
entry 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 (upstream will compare the manifest's two
public keys, which equivalently fingerprint the seeds).

addChecked_wellFormed: an accepted entry passed the comparison, so
checked insertion discharges the WellFormed distinctness at
construction - once upstream enforces the check, every loaded
registry is well-formed by construction, closing the loop the way
#1179 did for the store invariants. Re-align the shape with the
merged fix when it lands.
---
 LeanSpec/Validator/Registry.lean | 40 ++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/LeanSpec/Validator/Registry.lean b/LeanSpec/Validator/Registry.lean
index b7158a5..c6ae6e6 100644
--- a/LeanSpec/Validator/Registry.lean
+++ b/LeanSpec/Validator/Registry.lean
@@ -93,5 +93,45 @@ 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) :
+    Option ValidatorRegistry :=
+  if entry.proposalSecretKey.prfKey.data ==
+      entry.attestationSecretKey.prfKey.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)
+    (entry : ValidatorEntry) (hwf : WellFormed reg)
+    (h : addChecked reg entry = some reg') :
+    WellFormed reg' := by
+  unfold addChecked at h
+  split at h
+  · simp at h
+  · next hne =>
+    injection h with h'
+    subst h'
+    exact WellFormed.add reg entry hwf fun hc =>
+      hne (by rw [hc]; exact beq_self_eq_true _)
+
 end ValidatorRegistry
 end LeanSpec.Validator