skeleton: proof-pyramid layout, honest status table, trusted-base doc

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-09-04 20:24:12 +00:00 · 2026-07-02 13:10:26 +02:00 · 2026-07-02 13:10:26 +02:00 · 549bef148b
commit 549bef148b
3 changed files with 101 additions and 0 deletions
--- a/.gitignore
+++ b/.gitignore
@ -0,0 +1,3 @@
+*.olean
+.lake/
+lake-manifest.json
--- a/README.md
+++ b/README.md
@ -0,0 +1,73 @@
+# 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 ⇒ [8][S]B = [8]R + [8][k]A
+        ├──────────────────────────────┤
+        │  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`    | ⏳ in progress | — |
+| Group law (Edwards) | `edwardsImplementation`  | ⏳ in progress | — |
+| Scalar mod ℓ        | `scalarImplementation`   | ⏳ in progress | — |
+| 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**: [dalek-cryptography/curve25519-dalek](https://github.com/dalek-cryptography/curve25519-dalek), commit `4cf8db2`
+- **Pinned/patched source**: [saymrwulf/curve25519-dalek-source](https://github.com/saymrwulf/curve25519-dalek-source), commit `135ed70`
+- **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
+
+```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.
--- a/TRUSTED-BASE.md
+++ b/TRUSTED-BASE.md
@ -0,0 +1,25 @@
+# Trusted base
+
+What you must believe for the theorems in this repository to transfer to the
+running Rust code. Everything else is machine-checked.
+
+1. **Lean 4 kernel** (v4.30.0-rc2) and its three foundational axioms
+   `[propext, Classical.choice, Quot.sound]`. Every certificate is
+   `#print axioms`-audited against exactly this list.
+2. **mathlib** (prebuilt oleans fetched by `lake exe cache get`).
+3. **Charon + Aeneas** (pinned `9dd7f23c` / `bf13c42e`): the translation
+   from Rust MIR to the Lean model is assumed faithful. The generated
+   `gen/` files are never edited (comments only); proofs are stated ABOUT them.
+4. **External-function models** (`gen/*/FunsExternal.lean`): Rust items that
+   Aeneas cannot translate (constant-time `subtle` primitives, iterator
+   plumbing, formatting) are axiomatized as opaque symbols. The axiom audit
+   proves none of these axioms enters the dependency cone of any certificate,
+   except where a model is explicitly listed below.
+5. **SHA-512 (signature layer only)**: the hash is modeled as an opaque
+   function ℬ* → ℬ⁶⁴ with no algebraic properties assumed. The signature
+   certificate has the shape "IF the hash model computes SHA-512, THEN an
+   accepted signature satisfies the EdDSA verification equation". The hash
+   implementation itself is NOT verified.
+6. **Compilation of Rust to machine code** (rustc backend) is out of scope,
+   as is side-channel behaviour (timing, speculation). The proofs are about
+   functional correctness at the MIR/LLBC level.