Skip to content

Commit 2b41b03

Browse files
adust09adust09
committed
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.
1 parent 15466f8 commit 2b41b03

2 files changed

Lines changed: 72 additions & 42 deletions

File tree

‎LeanSpec/Validator/Registry.lean‎

Lines changed: 66 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -11,15 +11,19 @@ Mirrors `src/lean_spec/node/validator/registry.py`:
1111
`entry.index` at every insertion site, so the model stores the
1212
entries directly and looks them up by their own index.
1313
14-
Upstream states the dual-key separation but does not enforce it:
15-
`add` is a bare assignment and `from_yaml` raises only for missing
16-
files and decode failures — a same-key manifest loads silently and
17-
then signs a proposal and an attestation for one slot with one
18-
stateful XMSS key (OTS state reuse; found by attempting VAL-2, an
19-
"invariant maintained only by convention" of the same class as
20-
leanEthereum/leanSpec#1176, reported as #1184). The distinctness
21-
therefore enters as `WellFormed`, and `WellFormed.add` shows the
22-
suggested fix — validating at insertion — preserves it.
14+
Upstream originally stated the dual-key separation but did not
15+
enforce it: `add` was a bare assignment and `from_yaml` raised only
16+
for missing files and decode failures — a same-key manifest loaded
17+
silently and then signed a proposal and an attestation for one slot
18+
with one stateful XMSS key (OTS state reuse; found by attempting
19+
VAL-2, an "invariant maintained only by convention" of the same class
20+
as leanEthereum/leanSpec#1176, reported as #1184). Since
21+
leanEthereum/leanSpec#1185 the loader rejects such a manifest by
22+
comparing its two public keys (the secret bytes stay untouched), so
23+
every loaded registry satisfies the distinctness by construction.
24+
The distinctness enters the theorems as `WellFormed`; `WellFormed.add`
25+
shows unchecked insertion preserves it, and `addChecked` mirrors the
26+
merged load-time check.
2327
2428
Proves VAL-2 from `docs/lean4-proof-propositions.md`:
2529
- VAL-2: on a well-formed registry, every lookup returns an entry
@@ -63,11 +67,11 @@ def get? (reg : ValidatorRegistry) (index : ValidatorIndex) :
6367
Option ValidatorEntry :=
6468
reg.validators.find? (fun e => e.index == index)
6569

66-
/-- The dual-key separation `ValidatorEntry` documents but upstream
67-
does not enforce: every entry's proposal key differs from its
68-
attestation key. A same-key entry would let one slot's proposal and
69-
attestation signatures consume overlapping XMSS one-time-signature
70-
state (see the module docstring). -/
70+
/-- The dual-key separation `ValidatorEntry` documents and the loader
71+
enforces since leanEthereum/leanSpec#1185: every entry's proposal key
72+
differs from its attestation key. A same-key entry would let one
73+
slot's proposal and attestation signatures consume overlapping XMSS
74+
one-time-signature state (see the module docstring). -/
7175
def WellFormed (reg : ValidatorRegistry) : Prop :=
7276
∀ e ∈ reg.validators, e.proposalSecretKey ≠ e.attestationSecretKey
7377

@@ -93,36 +97,42 @@ theorem WellFormed.add (reg : ValidatorRegistry) (entry : ValidatorEntry)
9397
| inl heq => rw [heq]; exact hentry
9498
| inr hmem => exact hwf e (List.mem_filter.mp hmem).1
9599

96-
/-! ## Checked insertion (the fix shape of leanEthereum/leanSpec#1184)
97-
98-
Tracks the fix suggested in leanEthereum/leanSpec#1184 (invited by the
99-
maintainers): reject a same-key entry where the check is one
100-
comparison, at insertion. Every one-time key of an XMSS secret key
101-
derives from its master PRF seed, so two keys collide in OTS state
102-
exactly when their seeds coincide — the check compares the seeds
103-
(upstream will compare the manifest's two public keys, which
104-
equivalently fingerprint the seeds). Re-align the shape with the merged
105-
fix when it lands upstream. -/
106-
107-
/-- Add a validator entry only when its two keys are distinct — the
108-
load-time validation of leanEthereum/leanSpec#1184. `none` mirrors the
109-
`ValueError` the loader raises on a same-seed manifest. -/
110-
def addChecked (reg : ValidatorRegistry) (entry : ValidatorEntry) :
100+
/-! ## Checked insertion (the merged fix of leanEthereum/leanSpec#1185)
101+
102+
Mirrors the fix merged upstream as leanEthereum/leanSpec#1185 (closes
103+
#1184): `from_yaml` rejects a manifest entry whose attestation and
104+
proposal public keys coincide, before any secret key is decoded. The
105+
public-key derivation is Arklib-side crypto, so it enters the model as
106+
the `publicKeyOf` parameter. Distinct public keys imply distinct
107+
secret keys for *every* derivation (a function maps equal inputs to
108+
equal outputs), so `WellFormed` follows with no cryptographic
109+
assumption; the OTS-level content — distinct master seeds — follows
110+
for derivations that fingerprint the seed
111+
(`addChecked_seed_distinct`). -/
112+
113+
/-- Add a validator entry only when its two public keys differ — the
114+
load-time validation of leanEthereum/leanSpec#1185. `none` mirrors the
115+
`ValueError` the loader raises on a same-key manifest; the comparison
116+
touches only public material. -/
117+
def addChecked (publicKeyOf : SecretKey → ByteArray)
118+
(reg : ValidatorRegistry) (entry : ValidatorEntry) :
111119
Option ValidatorRegistry :=
112-
if entry.proposalSecretKey.prfKey.data ==
113-
entry.attestationSecretKey.prfKey.data then
120+
if (publicKeyOf entry.attestationSecretKey).data ==
121+
(publicKeyOf entry.proposalSecretKey).data then
114122
none
115123
else
116124
some (reg.add entry)
117125

118126
/-- The checked insertion discharges the `WellFormed` distinctness at
119-
construction: an accepted entry passed the seed comparison, and keys
120-
sharing no seed are distinct. Once upstream enforces the check, every
121-
loaded registry is well-formed by construction — closing the loop the
122-
way leanEthereum/leanSpec#1179 did for the store invariants. -/
123-
theorem addChecked_wellFormed (reg reg' : ValidatorRegistry)
127+
construction, for every public-key derivation: an accepted entry has
128+
distinct public keys, and equal secret keys cannot derive distinct
129+
public keys. Upstream now enforces the check, so every loaded registry
130+
is well-formed by construction — closing the loop the way
131+
leanEthereum/leanSpec#1179 did for the store invariants. -/
132+
theorem addChecked_wellFormed (publicKeyOf : SecretKey → ByteArray)
133+
(reg reg' : ValidatorRegistry)
124134
(entry : ValidatorEntry) (hwf : WellFormed reg)
125-
(h : addChecked reg entry = some reg') :
135+
(h : addChecked publicKeyOf reg entry = some reg') :
126136
WellFormed reg' := by
127137
unfold addChecked at h
128138
split at h
@@ -133,5 +143,24 @@ theorem addChecked_wellFormed (reg reg' : ValidatorRegistry)
133143
exact WellFormed.add reg entry hwf fun hc =>
134144
hne (by rw [hc]; exact beq_self_eq_true _)
135145

146+
/-- The OTS-reuse core of leanEthereum/leanSpec#1184: when the
147+
derivation fingerprints the master seed (Arklib derives the public
148+
root from the PRF seed), an accepted entry's two keys have distinct
149+
seeds, so one slot's proposal and attestation signatures can never
150+
consume overlapping one-time-signature state. -/
151+
theorem addChecked_seed_distinct (publicKeyOf : SecretKey → ByteArray)
152+
(hdet : ∀ k₁ k₂ : SecretKey, k₁.prfKey.data = k₂.prfKey.data →
153+
publicKeyOf k₁ = publicKeyOf k₂)
154+
(reg reg' : ValidatorRegistry) (entry : ValidatorEntry)
155+
(h : addChecked publicKeyOf reg entry = some reg') :
156+
entry.proposalSecretKey.prfKey.data ≠
157+
entry.attestationSecretKey.prfKey.data := by
158+
unfold addChecked at h
159+
split at h
160+
· simp at h
161+
· next hne =>
162+
intro hseed
163+
exact hne (by rw [hdet _ _ hseed]; exact beq_self_eq_true _)
164+
136165
end ValidatorRegistry
137166
end LeanSpec.Validator

‎docs/lean4-proof-propositions.md‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
---
22
title: leanSpec → Lean4 Theorem Proving Proposition Catalog
3-
last_updated: 2026-07-05
3+
last_updated: 2026-07-20
44
tags:
55
- lean4
66
- formal-verification
@@ -388,17 +388,18 @@ The propositions here guarantee **duty correctness and slashing prevention**: pr
388388
389389
- [x] **VAL-2: Proposal key and attestation key are distinct**
390390
- Source: `proposalKey` / `attestationKey` (ValidatorService; realized as the `attestation_secret_key` / `proposal_secret_key` fields of `ValidatorEntry`, `src/lean_spec/node/validator/registry.py`)
391-
- 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`.
392-
- 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)
391+
- 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.
392+
- 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)
393393
- Sample code:
394394
395395
```lean
396396
theorem dual_key_distinct (vid : ValidatorIndex) (reg : KeyRegistry) :
397397
reg.proposalKey vid ≠ reg.attestationKey vid := by sorry
398398
-- ✅ proved in LeanSpec/Validator/Registry.lean as
399399
-- `ValidatorRegistry.dual_key_distinct` (relative to
400-
-- `ValidatorRegistry.WellFormed` — upstream does not enforce the
401-
-- distinctness, so it cannot be derived from construction)
400+
-- `ValidatorRegistry.WellFormed` — established at load time by
401+
-- upstream since leanEthereum/leanSpec#1185, mirrored as
402+
-- `addChecked_wellFormed`)
402403
```
403404
404405
- [x] **VAL-3: Each slot has exactly one proposer**

0 commit comments

Comments
 (0)