Grant Application - Lean proof of the GLV recoding and ladder in pasta_curves (part 3 of pasta_curves#174)

Community Grants Applications
1

Hi all, I’m Athex. Rifat Ahmed and I work at Nirapod, and I’ve contributed to the Jasmin compiler, mostly its ARMv8-A back end.

We’ve finished a machine-checked Lean proof of part 3 of pasta_curves#174, the wNAF recoding and the Straus ladder in src/glv.rs. Orchard has used this code for batched trial decryption since 0.15.4, and so far it has only been tested, on chosen and random scalars. The proof is up as a pull request to pasta_curves. The recoding is proved against Aeneas’ translation of the Rust, and the ladder against a Lean model of it.

We’re asking for $7,000. None of it is paid unless the pasta_curves maintainers accept the proof: $5,500 on acceptance, then $1,500 for six months of upkeep after the merge.

Questions and criticism welcome, especially on whether the theorem statements say the right thing.

Application: Grant Application - Lean proof of the GLV recoding and ladder in pasta_curves (part 3 of pasta_curves#174) · Issue #507 · ZcashCommunityGrants/zcashcommunitygrants · GitHub

Pull request: lean: prove the GLV wNAF recoding and Straus ladder by athexweb3 · Pull Request #180 · zcash/pasta_curves · GitHub

Proofs, tests and the differential test: GitHub - nirapod-labs/pasta-glv-proofs: Machine-checked Lean 4 proof of the wNAF recoding and Straus ladder in pasta_curves' GLV scalar multiplication · GitHub

The full application is below, the same text as on GitHub.

Project Summary

We have completed a machine-checked Lean proof of the wNAF recoding and the Straus ladder in pasta_curves’ GLV scalar multiplication (part 3 of pasta_curves#174), and opened it as a pull request to pasta_curves. This is the code that Orchard’s batched trial decryption calls. The recoding is proved against Aeneas’ translation of the Rust, and the ladder against a Lean model of it. We request $7,000, paid only if the pasta_curves maintainers accept the proof: $5,500 on acceptance and $1,500 for six months of upkeep after the merge.

Project Description

pasta_curves#174, opened by daira, asks for a formal proof of the crate’s GLV scalar multiplication in three parts: the endomorphism, the scalar decomposition, and the wNAF recoding with the Straus ladder. It asks for a proof of whichever algorithm the crate settles on as the most efficient, and pasta_curves#125, currently a draft, proposes an alternative recoding based on Eisenstein integers. Our proof covers part 3 for the algorithm in the crate today (src/glv.rs at commit e3c0f02).

For wnaf_digits, we prove that every magnitude below 2^127 is recoded without a panic into at most 128 digits, each zero or odd with absolute value at most 7, that encode the signed input. This is proved about a Lean model and also about Aeneas’ machine translation of the Rust function.

For the four entry points (mul_glv, Table::mul, mul_decomposed on a decomposed scalar, and batch_mul_same_scalar_vartime), we prove that they return valid points that represent [k]P. We also prove what the ladder and the table builders compute. These results are about a Lean model that mirrors the Rust line by line and was checked against it by reading. They take four hypotheses, about the group order, the endomorphism (part 1), the scalar decomposition (part 2) and the curve primitives.

The proofs use only Lean’s three standard axioms. Run locally on the pull request branch, pasta’s own checks and the nanoda kernel checker pass.

Proposed Problem

The GLV code that Orchard’s wallet scanning runs has no proof: its constants are checked exactly, but its behaviour only by tests on sampled inputs. Since Orchard 0.15.4, batched trial decryption uses pasta_curves::glv (Table, Decomposed, Table::mul_decomposed): each incoming viewing key is decomposed and recoded once per batch, and the result is reused against every ephemeral key. pasta’s tests compare this code with native scalar multiplication on fixed sets of 64 deterministic scalars, on edge cases and boundary witnesses, and on randomized property tests. The digits depend only on the scalar, which here is the incoming viewing key. An error in the recoding or the ladder that affected only some scalars could therefore pass every sampled test while causing the affected wallets to miss their incoming notes in every batch.

The proof covers every scalar, under the stated hypotheses. It found no error in the path that callers use. It also establishes two boundary facts above the contract’s 2^127 bound: the least magnitude that needs a 129th digit is 0x88888888888888888888888888888889, and in a build without debug assertions or overflow checks, the u128 addition wraps on exactly four inputs (2^128 − 7, −5, −3 and −1). Neither affects a correct caller.

pasta’s CI regenerates the Aeneas translation and compares it with the committed copy, so a change to wnaf_digits fails CI until the translation is regenerated, and the proofs are then checked against the new translation.

Proposed Solution

Milestone 1 takes the proof to acceptance in pasta_curves (merged, or confirmed ready to merge): the changes that upstream review requires in the statements, proofs and layout, the branch kept current with main and its toolchain pins, and a theorem-to-source map that gives, for each theorem, the functions of src/glv.rs and src/curves.rs it covers, whether it is proved about the model or about the translation, and its hypotheses.

Milestone 2 keeps the proofs working for six months after the merge: a fix within three working days of any GLV failure in pasta’s Lean CI, and an update to the model within 14 days of any merged change to the Rust it mirrors.

The natural next step is to prove the ladder and tables against Aeneas’ translation as well, the route that pasta_curves#174 itself suggests. The pinned Charon and Aeneas cannot translate that code as written, because it is generic over the curve traits. We have built and checked a refactor of src/glv.rs that makes the ladder and most of the table code translatable: generic _with functions over private traits, as pasta’s invert_with is written, with blanket impls of the traits for every curve. The public API and tests are unchanged, and the release machine code on aarch64 is the same apart from references to panic-location records. The refactor is published in the proof package. pasta’s contribution rules ask that such a change to the Rust come at the maintainers’ request, so the pull request only offers it. If the maintainers want it, we will propose it to ZCG as a change of scope; it is not funded here. Composing this proof with parts 1 and 2, and any proof of the Eisenstein recoding, are also outside this application.

If it helps the committee, we are glad for it to consult the pasta_curves maintainers, or to wait for their first response on the pull request, before voting.

Solution Format

One pull request to pasta_curves’ lean/ package: the Lean files, one line in lean/scripts/gen_aeneas.sh, two paths in the CI translation filter, and no change to the Rust. The proofs in their original layout, with the Lean tests and the differential test, are published at GitHub - nirapod-labs/pasta-glv-proofs: Machine-checked Lean 4 proof of the wNAF recoding and Straus ladder in pasta_curves' GLV scalar multiplication · GitHub.

Dependencies

pasta_curves’ pinned toolchain: Lean v4.31.0, Mathlib, and Charon and Aeneas at b86120d. Maintainer review for milestone 1. Milestone 2 starts when the pull request is merged. Nothing from parts 1 and 2 is needed: their results enter as hypotheses, so this work stands on its own.

Technical Approach

A Lean model mirrors the Rust of the GLV path line by line, and the specifications are stated about it. The recoding is also proved about Aeneas’ machine translation of wnaf_digits, so for the recoding the result holds of the translated Rust, with Charon and Aeneas trusted. The ladder and table model was checked against the Rust by reading.

The evidence is public:

  • The Lean package builds with lake build, and #print axioms on the final theorems lists only propext, Classical.choice and Quot.sound. Its CI repeats the build, the axiom check and the differential test on every push.
  • Ten deliberately broken models each fail the statements they should (twelve refutations, checked by the kernel). One instance satisfies all four hypotheses at once, so the end-to-end theorems are not vacuous.
  • A differential test runs a verbatim copy of wnaf_digits against the Lean model: identical digits or an identical panic on 75,223 magnitudes with both signs, in all four combinations of debug assertions and overflow checks.
  • nanoda, an independent implementation of Lean’s kernel, accepts the whole library on the pull request branch (308,862 declarations, dependencies included).

Tools: Lean 4 and Mathlib, Charon and Aeneas, nanoda, and Claude (Anthropic).

Scope: variable-time code only, with no constant-time claims. All four hypotheses are arguments of the theorems, not axioms. The one on the curve primitives is trusted, the one on the group order is not proved here, and those on the endomorphism and the decomposition stand until parts 1 and 2 are proved.

License: the work is released under MIT OR Apache-2.0, pasta_curves’ own license, which includes MIT.

Upstream Merge Opportunities

The proof is proposed to zcash/pasta_curves as pasta_curves#180; the Lean tests, the differential test and the refactor trial stay in the public proof package. pasta_curves#174, opened by daira, is the tracking issue that pasta’s contribution rules ask for. Review will take place on the pull request. The change adds Lean files and touches no Rust, so it asks for review time but changes no shipped code. The refactor described under Proposed Solution would be a separate pull request, sent only if the maintainers ask for it.

Open Source License

MIT

Hardware/Software Costs (USD)

$0

Hardware/Software Justification

None. The builds run on our own machines.

Service Costs (USD)

$0

Service Costs Justification

None.

Compensation Costs (USD)

$7000

Compensation Costs Justification

Priced per accepted deliverable. Milestone 1, $5,500: $3,000 for the proof delivered with this application (the model, the statements, their proofs, including the proof against Aeneas’ translation of wnaf_digits, and the tests), and $2,500 for about 50 hours at $50 an hour to bring it to merge: the changes requested in upstream review, rebasing onto main and its pins, and the theorem-to-source map. Nothing in milestone 1 is paid until a maintainer accepts the proof. Milestone 2, $1,500: about 30 hours at $50 an hour over six months of upkeep after the merge.

Total Budget (USD)

$7000

Previous Funding

No

Previous Funding Details

None.

Other Funding Sources

No

Other Funding Sources Details

None. We will not apply to any other programme for this work.

Implementation Risks

The main risk is in review: a maintainer may find that a statement does not say what the Rust does, or may want it stated differently. Either way some proofs have to be reworked. That rework is what milestone 1 is priced for, and the differential test, the broken-model tests and the theorem-to-source map are there to bring such a problem to light early.

Review may also take longer than planned, since maintainer time on pasta_curves is limited. We will report any delay on the forum thread, and an open pull request does not count as delivered.

The code may move. src/glv.rs or the Lean, Mathlib and Aeneas pins can change while the pull request is open; we keep the branch current with main, and after the merge milestone 2 covers both. If pasta adopts the Eisenstein recoding of pasta_curves#125 in place of the current one, the recoding and ladder proofs would have to be redone, and we would propose that work separately.

Potential Side Effects

The main risk is false confidence: reading the result as “all of GLV is verified”. The application, the README and the pull request state which results are about the model and which are about the translated Rust, which hypotheses are assumed, and what is out of scope. The GLV modules add build time to pasta’s Lean CI, and the proofs add upkeep, which milestone 2 covers for the first six months. Nothing changes in consensus, funds or shipped code.

Success Metrics

  • The pull request is merged, or a maintainer confirms that it is ready to merge.
  • pasta’s Lean CI, nanoda included, passes on main with the GLV modules, using only the standard axioms.
  • For six months after the merge, every GLV failure in pasta’s Lean CI is fixed within three working days, and every merged change to the mirrored Rust is reflected in the model within 14 days, with links in the monthly updates.

Startup Funding (USD)

$0

Startup Funding Justification

None needed.

Milestone Details

- Milestone: 1
  Amount (USD): 5500
  Expected Completion Date: Eight weeks after the grant decision.
  User Stories:
    - "As a pasta_curves maintainer, I want a machine-checked proof of the GLV recoding and ladder in the crate's own lean/ package and CI, so that part 3 of pasta_curves#174 rests on a proof that pasta's CI rebuilds, not on sampled tests alone."
    - "As a reviewer of that proof, I want each theorem tied to the Rust functions it covers, with every assumption listed in one place, so that I can judge the statements without reading the proofs."
  Deliverables:
    - The pull request https://github.com/zcash/pasta_curves/pull/180 merged into pasta_curves' lean/ package, or confirmed ready to merge, with the changes requested in review incorporated: the Lean model, the statements and their proofs, using only Lean's standard axioms and passing pasta's Lean CI, nanoda included.
    - A theorem-to-source map in lean/README.md: for each theorem, the Rust functions it covers, whether it is proved about the model or about Aeneas' translation, and the hypotheses it takes; with a one-page summary in plain language.
  Acceptance Criteria: A pasta_curves maintainer (for example daira, str4d or nuttycom) merges the pull request, or confirms on it that the statements match part 3 of pasta_curves#174 and that it is ready to merge. $3,000 of this milestone pays for the proof as delivered with this application; nothing is paid without this acceptance. If no maintainer has reviewed by the expected date, we report that on the forum thread and ZCG decides whether to extend or close the milestone.

- Milestone: 2
  Amount (USD): 1500
  Expected Completion Date: Six months after the pull request is merged.
  User Stories:
    - "As a pasta_curves maintainer, I want the GLV proofs kept building and kept in step with src/glv.rs for six months after the merge, so that a toolchain update or an edit to the GLV code does not leave me a failing required check or a stale model."
  Deliverables:
    - A fix pull request within 3 working days of any GLV proof failure in pasta's Lean CI.
    - For every merged change to the Rust functions the model mirrors, an update to the model and proofs, or a note on that pull request that none is needed, within 14 days.
    - Monthly updates on the forum thread, and a closing report that links every event and its fix.
  Acceptance Criteria: The closing report is published, and a pasta_curves maintainer (for example daira, str4d or nuttycom), or a technical reviewer agreed with ZCG, confirms that no GLV proof failure stayed open beyond the times above. This milestone starts when the pull request is merged.

Supporting Documents