From 14e6b748148742f5a2f7fbcddb87fe45d21971b7 Mon Sep 17 00:00:00 2001
From: mrwulf <mrwulf.cleaner@gmail.com>
Date: Thu, 2 Jul 2026 13:10:26 +0200
Subject: [PATCH] skeleton: proof-pyramid layout, honest status table,
 trusted-base doc

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .gitignore      |  3 +++
 README.md       | 61 +++++++++++++++++++++++++++++++++++++++++++++++++
 TRUSTED-BASE.md | 24 +++++++++++++++++++
 3 files changed, 88 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 README.md
 create mode 100644 TRUSTED-BASE.md

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..24f9b74
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+*.olean
+.lake/
+lake-manifest.json
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..29de976
--- /dev/null
+++ b/README.md
@@ -0,0 +1,61 @@
+# pasta-pallas-verified
+
+Formal verification of Pallas (Pasta curve cycle, Zcash Halo 2) arithmetic in
+**zcash/pasta_curves**, built as a coherent proof pyramid in Lean 4 via the
+Charon/Aeneas transpilation pipeline:
+
+```
+        ┌────────────────────────────────────┐
+        │  Scalar multiplication             │   [n]P correct over the group
+        ├────────────────────────────────────┤
+        │  Group law (short Weierstrass)     │   point ops = curve group law
+        ├────────────────────────────────────┤
+        │  Field 𝔽_p (Montgomery form)       │   4×64-limb Fp ops correct mod p
+        └────────────────────────────────────┘
+   p = 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
+```
+
+Every theorem is stated about the **actual Aeneas-transpiled Rust code** from
+`src/fields/fp.rs` / `src/curves.rs`. There are **no bridge axioms**: the
+correctness of add/sub/neg/mul/square/montgomery_reduce/invert is *proven*,
+not assumed. (A previous attempt at this target axiomatized exactly those
+statements; this repository exists to do it properly.)
+
+## Layer status
+
+| Layer | Certificate | Status | Axioms of certificate |
+|-------|-------------|--------|-----------------------|
+| Field 𝔽_p (Montgomery) | `fieldImplementation` | ⏳ in progress | — |
+| Group law (Pallas)      | `curveImplementation` | ⏳ in progress | — |
+| Scalar multiplication   | `scalarMulCorrect`    | ⏳ 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**: [zcash/pasta_curves](https://github.com/zcash/pasta_curves), commit `fe08536`
+- **Pinned/patched source**: [saymrwulf/pasta_curves-source](https://github.com/saymrwulf/pasta_curves-source), commit `7f32788`
+- Representation: 4×64-bit limbs, Montgomery form (a·R mod p, R = 2²⁵⁶)
+
+## 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).
diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md
new file mode 100644
index 0000000..f6a6ebc
--- /dev/null
+++ b/TRUSTED-BASE.md
@@ -0,0 +1,24 @@
+# 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. **u64 primitive helpers** (`adc`/`sbb`/`mac`, if not translatable): where a
+   helper must be modeled externally, its model is a *definition* with proven
+   arithmetic content (not an opaque axiom), or an axiom provably outside every
+   certificate cone. The axiom audit enforces this.
+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.