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

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

.gitignore

@@ -0,0 +1,3 @@
+*.olean
+.lake/
+lake-manifest.json

README.md

@@ -0,0 +1,65 @@
+# risc0-ed25519-verified
+
+Formal verification of the ed25519 implementation in **risc0/curve25519-dalek (RISC Zero fork, v4.1.3)**, 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**: [risc0/curve25519-dalek](https://github.com/risc0/curve25519-dalek), commit `385adda`
+- **Pinned/patched source**: [saymrwulf/risc0-curve25519-dalek-source](https://github.com/saymrwulf/risc0-curve25519-dalek-source), commit `2643444`
+- **Patches**: minimal Aeneas-compatibility only (documented in the source repo)
+- **Scope caveat**: this verifies the fork's pure-Rust `serial/u64` path. The RISC Zero zkVM accelerator/syscall path 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).

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.