2026-07-02 11:10:26 +00:00
# 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 ⇒ [8][S]B = [8]R + [8][k]A
├──────────────────────────────┤
│ Scalar arithmetic mod ℓ ℓ
├──────────────────────────────┤
│ Group law (twisted Edwards) │ point ops = complete addition law
├──────────────────────────────┤
│ Field 𝔽 −
└──────────────────────────────┘
```
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 |
|-------|-------------|--------|-----------------------|
2026-07-02 12:38:53 +00:00
| Field 𝔽 `fieldImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
2026-07-02 14:23:31 +00:00
| Group law (Edwards) | `edwardsImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
Add scalar-layer foundation (Scalar52 arithmetic mod ℓ)
Transpile the Scalar52 limb backend (backend::serial::u64::scalar
add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas,
scoped at the function level to the iterator-free arithmetic core.
- verification/extract-scalar.sh: function-level Charon/Aeneas extraction
- verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (27 defs).
This fork (v4.1.2) implements Scalar52::sub's constant-time conditional add
with a pure arithmetic mask (constants::L[i] & underflow_mask), so the
extraction pulls in NO external functions or types (unlike v5 dalek, which
routes sub through subtle, and v4.1.3, which uses a local black_box).
- verification/gen/CurveScalar/{TypesExternal,FunsExternal}.lean: decl-free
stub modules kept so the check manifest is uniform across forks.
- verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52
denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled
constants::L denotes exactly the group order ℓ, kernel-checked).
- verification/check-scalar.sh: guarded compile of the gen modules plus the
denotation foundation.
check-scalar.sh passes: gen compiles; denotation + L = ℓ proven.
add/sub/mul remain in progress.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-02 19:27:33 +00:00
| Scalar mod ℓ `scalarImplementation` | 🔨 foundation | denotation + L=ℓ
2026-07-02 11:10:26 +00:00
| Signature (EdDSA) | `verifyEquation` | ⏳ in progress | — |
Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.
This table is updated only when `verification/check.sh` passes for the layer.
## Source
- **Upstream**: [betrusted-io/curve25519-dalek ](https://github.com/betrusted-io/curve25519-dalek ), commit `16e087a`
- **Pinned/patched source**: [saymrwulf/betrusted-curve25519-dalek-source ](https://github.com/saymrwulf/betrusted-curve25519-dalek-source ), commit `64ee8f0`
- **Patches**: minimal Aeneas-compatibility only (documented in the source repo)
- **Scope caveat**: this verifies the fork's pure-Rust `serial/u64` path. 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
```bash
source ~/aeneas-toolchain/env.sh
cd verification
./extract.sh # Rust → LLBC → Lean (regenerates gen/)
./check.sh # compiles EVERY shipped file + axiom-audits EVERY certificate
```
## Trusted base
See [TRUSTED-BASE.md ](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).
## Provenance
Proof engineering in this repository builds on the verification methodology
and proof architecture of
[PlanetMacro/ed25519-verificationtest ](https://github.com/PlanetMacro/ed25519-verificationtest )
(the reference solution). All proofs here are checked against **this fork's
own extracted code**; nothing is claimed that the check script does not compile.
