saymrwulf/pasta-pallas-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/pasta-pallas-verified.git synced 2026-09-04 20:03:39 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
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
1 commit 1 branch 0 tags 293 KiB
Lean 92.9%
Shell 7.1%
Find a file
mrwulf 14e6b74814 skeleton: proof-pyramid layout, honest status table, trusted-base doc 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-02 13:10:26 +02:00
.gitignore skeleton: proof-pyramid layout, honest status table, trusted-base doc 2026-07-02 13:10:26 +02:00
README.md skeleton: proof-pyramid layout, honest status table, trusted-base doc 2026-07-02 13:10:26 +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

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

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.