mirror of https://github.com/saymrwulf/pasta-pallas-verified.git synced 2026-09-04 20:03:39 +00:00

Formally verifying Pallas (zcash/pasta_curves) field arithmetic in Lean 4 via Charon/Aeneas — real extraction, no bridge axioms; field layer under construction, group law + scalar mul planned

Find a file

mrwulf c864ad5afe lean-guard: Guard 3a retry ladder (coherence pass 3, estate-wide guard update) Same change as the four ed25519 repos: a clamped run that dies on memory (rc 134/137) retries under the single-flight lock as headroom improves materially, when LEAN_MEM_WAIT_SEC>0. Default 0: behavior unchanged. Button green in the pass-3 sweep (check.sh OK, 117s). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>		2026-07-05 11:48:48 +02:00
verification	lean-guard: Guard 3a retry ladder (coherence pass 3, estate-wide guard update)	2026-07-05 11:48:48 +02:00
.gitignore	skeleton: proof-pyramid layout, honest status table, trusted-base doc	2026-07-02 13:10:26 +02:00
README.md	pasta field FOUNDATION proven + honest status; check.sh green	2026-07-02 20:16:07 +02:00
TRUSTED-BASE.md	skeleton: proof-pyramid layout, honest status table, trusted-base doc	2026-07-02 13:10:26 +02:00

README.md

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

Construction status (2026-07-02). The field FOUNDATION is proven and compiles (verification/check.sh is green): PPallas (Lucas/Pratt primality certificate for the 255-bit Pallas modulus), Denote (the Montgomery denotation ⟪a⟫ = feVal a·R⁻¹ and the Canon invariant), HelperSpecs (exact ℕ specs for the adc/sbb/mac u64 primitives, proven against the transpiled code), SubNegSpec (sub/neg), and ConstSpecs (R, R², INV, zero, one). Every one is stated about the REAL Aeneas-extracted code with no bridge axioms.

In progress: add, mul, montgomery_reduce, square, invert, and the aggregate fieldImplementation certificate. These are drafted in verification/Proofs/drafts/ and the Montgomery accounting is proven standalone, but the full theorems currently overflow the Lean kernel's proof-checking memory: omega certificates with 2²⁵⁶/2⁵¹²-scale coefficients (unavoidable in 4×64 Montgomery arithmetic) are too large for the kernel, whereas the ed25519 5×51 field (2⁵¹-scale, ×19 folding) stays small. The fix — reformulating every arithmetic step via linear_combination and isolating each big-coefficient step into a context-free lemma (the montgomery_rows_conclusion accounting lemma already does this and compiles) — is mechanical but not yet complete. Tracked honestly here rather than shipped behind an axiom.

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, commit fe08536
Pinned/patched source: 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

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.