mrwulf
f09aa2ca73
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
||
|---|---|---|
| verification | ||
| .gitignore | ||
| README.md | ||
| TRUSTED-BASE.md | ||
betrusted-ed25519-verified
Formal verification of the ed25519 implementation in betrusted-io/curve25519-dalek (Precursor/Xous fork, v4.1.2), 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 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 (a
single monomorphic sha512_hash3(R, A, m) oracle — this fork's sha2-0.10 stack
makes the incremental-hasher types untranslatable) and the wire-format types
stay opaque.
check.sh has a dedicated audit phase (Phase 3b) that fails the build unless
each apex-tier certificate's axiom cone is exactly
[propext, Classical.choice, Quot.sound] + {ed25519.Signature, verifying.sha512_hash3, 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 + as_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: betrusted-io/curve25519-dalek, commit
16e087a - Pinned/patched source: saymrwulf/betrusted-curve25519-dalek-source, commit
cee0e17(adds the decompress step_2 negate-then-assign patch) - Patches: minimal Aeneas-compatibility only (documented in the source repo)
- Scope caveat: this verifies the fork's pure-Rust
serial/u64path. The Engine25519 hardware-accelerator path on Precursor is different code and is NOT covered by these proofs.
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).