mrwulf
37bf01fc6f
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
|
||
|---|---|---|
| verification | ||
| .gitignore | ||
| README.md | ||
| TRUSTED-BASE.md | ||
dalek-ed25519-verified
Formal verification of the ed25519 implementation in dalek-cryptography/curve25519-dalek (upstream, v5.0.0-rc.1), built as a coherent proof pyramid in Lean 4 via the Charon/Aeneas transpilation pipeline:
┌──────────────────────────────┐
│ Signature (EdDSA verify) │ accepted ⇔ decompress(R) = [k](−A)+[s]B
├──────────────────────────────┤
│ Scalar arithmetic mod ℓ │ Scalar52 ops correct mod ℓ
├──────────────────────────────┤
│ Group law (twisted Edwards) │ point ops = complete addition law
├──────────────────────────────┤
│ Field 𝔽_p, p = 2²⁵⁵ − 19 │ FieldElement51 ops correct mod p
└──────────────────────────────┘
Every layer states its theorems about the actual Aeneas-transpiled Rust
code (never about a hand-written re-model), and every claim in the status
table below is backed by a compiled proof plus an axiom audit of the named
certificate. Files that do not compile under verification/check.sh are not
in this repository.
Layer status
| Layer | Certificate | Status | Axioms of certificate |
|---|---|---|---|
| Field 𝔽_p | fieldImplementation |
✅ proven | [propext, Classical.choice, Quot.sound] |
| Group law (Edwards) | edwardsImplementation |
✅ proven | [propext, Classical.choice, Quot.sound] |
| Scalar mod ℓ | scalarImplementation (add ✅ sub ✅ mul ✅) |
✅ proven | [propext, Classical.choice, Quot.sound] |
| Signature (EdDSA) | verify_accepts_iff … verify_accepts_iff_decompress (4 tiers) |
✅ proven (phases 1+2) | standard three + the button-enforced SHA-512/wire-format boundary — see The signature apex |
Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.
This table is updated only when verification/check.sh passes for the layer.
The signature apex (phases 1 and 2)
The byte-level apex certificate CurveFieldProofs.verify_accepts_iff is the
literal EdDSA acceptance criterion, proven about the extracted verifier:
For a signature that parses, the verifier returns
Ok(())iff the recomputed compressed pointcompress([s]·B − [k]·A)equals the signature'sR, byte-for-byte — wherekis whatever scalar the opaque SHA-512 oracle produces from(R, A, msg).
The recomputation runs entirely through the proven model: the vendored ed25519-dalek verify glue is extracted as gen/CurveSig, whose
hand-maintained externals import gen/CurveField — every curve and scalar call
resolves by fully-qualified name to a proven definition. Only SHA-512 (three
stateful wrapper calls) and the wire-format types stay opaque.
check.sh has a dedicated audit phase (Phase 3b) that fails the build unless
the apex certificate's axiom cone is exactly
[propext, Classical.choice, Quot.sound] + {ed25519.Signature, sha2.Sha512, verifying.sha512_new, verifying.sha512_update, verifying.sha512_finalize_bytes, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new}
— i.e. the three Lean foundations plus the documented SHA-512/wire-format
boundary. Zero curve, scalar, or backend axioms. The companion certificate
verify_loop_full (the 32-byte comparison loop computes array equality)
carries the standard three axioms only.
Phase 2 (complete): the point-level lift. Phase 3b enforces the SAME axiom boundary on three further tiers that lift the byte equation to points:
| Tier | Certificate | Statement |
|---|---|---|
| half-lift | verify_accepts_iff_point |
accepted ⇔ R = the canonical encoding of [k]·(−A) + [s]·B (compress semantics + to_bytes canonicity + hash-to-scalar, recompute chain inverted) |
| point equation | verify_accepts_iff_point_eq |
for any valid on-curve Q canonically encoded by R: accepted ⇔ Q = [k]·(−A) + [s]·B as points (encoding-injectivity: d non-square + parity root-selection) |
| full lift | verify_accepts_iff_decompress |
R decompresses to a valid on-curve Pt, and accepted ⇔ Pt = [k]·(−A) + [s]·B — the constructive capstone |
The full lift runs through the extracted CompressedEdwardsY::decompress
itself, proven end-to-end: from_bytes parses the y-residue exactly below
bit 255 (from_bytes_spec), sqrt_ratio_i returns the even square root of
(y²−1)/(dy²+1) (sqrt_ratio_i_sq_spec, Fermat-exponent square root), and
the sign bit selects the x-parity (decompress_of_canonical, standard three
axioms). Byte comparison ↔ encoding equality ↔ point equality ↔
decompressed-point equality: every link is machine-checked over the
extracted code, and check.sh fails the build if any of the four tiers'
cones deviates from the boundary above.
Source
- Upstream: dalek-cryptography/curve25519-dalek, commit
4cf8db2 - Pinned/patched source: saymrwulf/curve25519-dalek-source, commit
aa0f6ab(adds the decompress step_2 negate-then-assign patch) - Patches: minimal Aeneas-compatibility only (documented in the source repo)
- Verified backend:
backend/serial/u64(FieldElement51,Scalar52). SIMD/AVX backends are out of scope (marked opaque).
Toolchain (pinned)
| Component | Version |
|---|---|
| Aeneas | bf13c42e |
| Charon | 9dd7f23c |
| Lean | v4.30.0-rc2 |
| OCaml | 5.3.0 |
Reproducing
source ~/aeneas-toolchain/env.sh
cd verification
./extract.sh # Rust → LLBC → Lean (regenerates gen/)
./check.sh # compiles EVERY shipped file + axiom-audits EVERY certificate
The gen model is ONE merged universe (gen/CurveField: field + curve +
scalar + the verify path's reachable code), regenerated in full by
extract.sh. The scalar layer keeps its own check button:
./check-scalar.sh # compiles the merged gen + all scalar proofs (add, sub,
# Montgomery mul, byte-parsing) and kernel-audits the
# scalar certificates, incl. the scalarImplementation
# aggregate
Trusted base
See TRUSTED-BASE.md for the complete list of assumptions (Lean kernel, mathlib, Charon/Aeneas semantics, external-function models, and — in the signature layer only — an opaque SHA-512 model).