mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
skeleton: proof-pyramid layout, honest status table, trusted-base doc
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
commit
0736f51d1f
3 changed files with 101 additions and 0 deletions
3
.gitignore
vendored
Normal file
3
.gitignore
vendored
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
*.olean
|
||||
.lake/
|
||||
lake-manifest.json
|
||||
73
README.md
Normal file
73
README.md
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
# 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).
|
||||
|
||||
## 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.
|
||||
25
TRUSTED-BASE.md
Normal file
25
TRUSTED-BASE.md
Normal file
|
|
@ -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.
|
||||
Loading…
Reference in a new issue