[closed due to licencing issues] Verify pasta_curves' AArch64 Pasta Montgomery routines by daira · Pull Request #35 · daira/CompElliptic

daira · 2026-09-08T15:38:04Z

[Edit: This PR has been closed because Semolina is Apache-2.0-only — and therefore so is the derived code which includes PastaMul.lean and PastaMulSpec.lean. CompElliptic is dual-licenced under MIT and Apache-2.0, and I don't want to complicate its licencing story unnecessarily, especially when the plan had originally been to move this PR to pasta_curves in any case. I don't know whether that will happen now given the licencing issue. (Apache-2.0 and dual-licenced code can be mixed on a per-file basis but the details of that are off-topic here.)]

Groundwork for formalizing the AArch64 Montgomery routines that zcash/pasta_curves#100 vendors from Semolina v0.1.4 (mul_mont_pasta, sqr_mont_pasta, from_mont_pasta, and their shared reduction helper). The review of that PR found that mul's five-limb accumulator wraps for an unreduced left operand when lhs[3] and a right-operand limb are both 2^64 - 1, inside the range the PR documents as safe (the review comment); the routines' actual operand contracts are what this work is to establish.

What is here

CompElliptic/Asm/AArch64/Semantics.lean: the dozen AArch64 instructions the file uses (mul, umulh, the adds/adcs/adc and subs/sbcs carry chains, lsl/lsr, csel on lo), as functions on natural numbers reduced modulo 2^64, with the carry as a natural number in {0, 1}. Working in Nat rather than a fixed-width type keeps the vectors kernel-checkable with decide and the carry arithmetic inside omega's fragment.
scripts/gen_aarch64_pasta_mul.py, which generates PastaMul.lean from the vendored .S: one let per instruction with the instruction as an aligned comment, argument limbs read where the assembly loads them, result limbs bound where it stores them. The stack frame and the return address are outside the model, and the script checks that no instruction reads a register it does not model. Loads the routines never read (p[2], and p[3] in the helper) are left as comments; the code hard-codes p[2] = 0 and p[3] = 2^62.
PastaMulVectors.lean: 1052 outputs of the real routines, run on an Apple M-series machine at pasta_curves 8ad85e9fab7929f6236960e472f432a4bd9ccd74, on boundary, random canonical, and unreduced operands, each checked against the transcription by the kernel (decide +kernel, about five seconds in total). The unreduced-operand vectors record the routines' behaviour outside their contracts too.
PastaMulSpec.lean: the correctness theorems, proved over the transcription instruction by instruction. The mechanical part of each proof is generated too (gen_aarch64_pasta_mul.py --skeleton): for every instruction, the defining equation of its result by rfl, the linear facts that later steps need, and a clear_value. Hand-written -- BEGIN ... -- END blocks between the generated groups supply the rest: the Montgomery round invariants, a called routine's contract, and the final case analysis. Proved so far: mulBy1_spec, for the shared reduction helper (for every four-limb t, it returns limbs below 2^64 whose value r satisfies 2^256 * r = t + Q * p for some Q < 2^256); fromMont_spec (for every four-limb value, the result is below p and 2^256 * result ≡ value (mod p); no bound on value below p is needed); and mulMont_spec (the result is below p and 2^256 * result ≡ lhs * rhs (mod p), under two arithmetic conditions that keep the five-limb accumulator below 2^320 in each round and the final accumulator below 2 * p), with the two operand contracts as corollaries: mulMont_spec_of_lhs_lt for lhs < p and any four-limb rhs, and mulMont_spec_of_rhs_lt for any four-limb lhs and rhs < p whose limbs 1 to 3 are at most 2^64 - 3.
scripts/check_aarch64_pasta_mul.sh, added to the generators CI job: the vendored assembly and vectors match their recorded hashes, regeneration reproduces the committed Lean files, and the generated parts of the proofs are the current skeletons once the annotation blocks are stripped (--check-spec).
design/aarch64-pasta-mul-verification.md: the trust story, the operand contracts, the proof method, and the theorems.

What is not here yet

The remaining proof units follow in this PR: sqrMont, then the instantiation at the two Pasta primes with the crate's constants and the census entries in TrustBoundary.lean.

🤖 Claude Fable 5.1

zcash/pasta_curves#100 vendors Semolina v0.1.4's AArch64 Montgomery multiplication, squaring, and conversion for the Pasta fields. This adds the groundwork for proving those routines correct here. - `CompElliptic/Asm/AArch64/Semantics.lean`: the dozen instructions the file uses (`mul`, `umulh`, the `adds`/`adcs`/`adc` and `subs`/`sbcs` carry chains, `lsl`/`lsr`, `csel` on `lo`) as functions on natural numbers reduced modulo 2^64, so that the vectors are kernel-checkable with `decide` and the carry arithmetic stays in `omega`'s fragment. - `scripts/gen_aarch64_pasta_mul.py` generates `PastaMul.lean` from the vendored `.S`, one `let` per instruction with the instruction as a comment. Loads and stores become limb reads and result bindings; the stack frame and the return address are outside the model, and the script checks that no instruction reads a register it does not model. Loads the routines never read (`p[2]`, and `p[3]` in the helper) are left as comments: the code hard-codes `p[2] = 0` and `p[3] = 2^62`. - `PastaMulVectors.lean`: 1052 outputs of the real routines (pasta_curves 8ad85e9fab7929f6236960e472f432a4bd9ccd74 on an Apple M-series machine) on boundary, random canonical, and unreduced operands, each checked against the transcription by the kernel. They pass in about five seconds. - `scripts/check_aarch64_pasta_mul.sh`, run by CI: the vendored assembly and vectors match their recorded hashes, and regeneration reproduces the committed Lean files. - `design/aarch64-pasta-mul-verification.md`: the trust story, the operand contracts, and the theorems to be stated. Only the vectors are proved here. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

daira · 2026-09-08T15:44:34Z

This file is from zcash/pasta_curves#100; please review there.

`gen_aarch64_pasta_mul.py --skeleton NAME` prints the proof steps of a transcribed routine that follow from its instruction stream alone: unfold the definition, extract its `let`s under unique names, and for every instruction record the defining equation of the result by `rfl`, derive the linear facts that later steps need (the carry-chain equation, the range facts, the product and shift decompositions), clear the `%`/`/` equation, and make the local opaque with `clear_value`. Hand-written annotation blocks (`-- BEGIN ... -- END`) go between the generated groups. `--check-spec FILE` strips the blocks and requires the rest of each proof to be the current skeleton, so an edit to the assembly regenerates the skeleton and fails the check until the annotations are moved. For this, the emitter records with each binding a description of the instruction and its operands, a routine carries its emitter and result names, and the liveness pass is shared with the transcription. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

`mulBy1_spec`: for every four-limb `t`, a modulus with limbs `[p0, p1, 0, 2^62]`, and `inv * p0 ≡ -1 (mod 2^64)`, the helper returns limbs below `2^64` whose value `r` satisfies `2^256 * r = t + Q * p` for some `Q < 2^256`. The proof is the generated skeleton for `mulBy1` with four hand-written round blocks and a conclusion block. A round block rewrites the Montgomery cancellation fact to the linear equation `t0 + lo = 2^64 * c`, via the ghost low product limb and the carry of `subs xzr, t0, #1`; shows that neither `adc` wraps; and obtains the round invariant as a linear combination of the instruction equations, with `omega` run in a context cleared down to those equations. Keeping `%` and `/` out of the invariants' `omega` calls is what makes them fast: with the cancellation fact's `%` terms present, the same call ran for minutes without finishing. The CI check script also runs `--check-spec` on the spec file. The design document describes the proof method, records the helper's theorem as proved, gives the assembly's instruction count as 310 (the count it stated included labels and directives), and says that the FFI boundary is not modelled formally (it had said that the boundary was outside the trusted base); the README's list of what is present mentions the proof. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

`fromMont_spec`: for every four-limb `value`, the routine returns limbs below `2^64` whose value `r` is below `p` and satisfies `2^256 * r ≡ value (mod p)`. No bound on `value` below `p` is needed: by `mulBy1_spec` the helper's result is at most `p`, and the conditional subtraction removes the one excess case. The proof is the generated skeleton for `fromMont` with two blocks. The first applies the helper's theorem, which yields the bounds on the helper's output limbs and the equation `2^256 * r = value + Q * p`. The conclusion splits on the final carry, which is clear exactly when `r < p`, and reads the congruence off an equation `a + k * p = b + l * p` with `modEq_of_add_mul`. The spec module's doc says what the annotation blocks supply beyond the round invariants; the design document records the theorem as proved, and the README's list of what is present mentions it. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

Each generated step now proves its range fact, carry-chain equation, product or shift decomposition, and ghost witness by instantiating one lemma (`Nat.mod_add_div`, `Nat.mod_lt`, `Nat.div_lt_of_lt_mul`, `Nat.mul_lt_mul''`, or one of five small lemmas in the spec file's preamble) instead of calling `omega`. Every `omega` sees the whole local context, so in a long proof the per-step calls slowed as facts accumulated, and the multiplication routine's proof exhausted the per-declaration heartbeat budget. The skeleton's cost is now independent of its position in the proof, `omega` is left to the annotation blocks, and the spec module compiles in 7 s instead of 20. `lsr` results, bounded by `2^62`, are weakened where a `2^64` bound is needed, and the `csel` bounds name their hypotheses instead of searching the context. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

The design document's status list marked only its first two items as present or proved, so the other three read as done; it now separates what is present from what remains, and the two theorems not yet proved are marked as such. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

daira · 2026-09-09T10:17:05Z

Note that the nanoda check failing is not concerning; it's just because there are new top-level modules that the script hasn't been updated for yet.

dannywillems · 2026-09-09T10:51:40Z

+
+GENERATED by `scripts/gen_aarch64_pasta_mul.py` from
+`CompElliptic/Asm/AArch64/vendor/pasta_mul-armv8-vectors.txt`; do not edit by hand. Each
+vector is the output of the real assembly (pasta_curves `8ad85e9fab7929f6236960e472f432a4bd9ccd74`,


Nit: efc0c69533f491743162f3263acfb6c23603ad91 is the new commit upstream in zcash/pasta_curves#100

dannywillems · 2026-09-09T11:05:58Z

+on the Pasta fields, under the operand contracts they actually have. The proof is
+about the instruction stream of `src/asm/pasta_mul-armv8.S` (310 instructions, blob
+`4321cf159d9814a14afbdc5cf42265384150822f`, sha256
+`0bcd5fa67d4aef5043eb536fdefd41ce16e6f7fbac3e5e6ac4f7619b35fd5e85`), not about a


Reviewer note: checked from commit 8ad85e9 on pasta_curves, sha256 src/asm/pasta_mul-armv8.S.

dannywillems · 2026-09-09T11:25:31Z

+2. `sqr`: the cross-term schoolbook, the doubling, and the "can't overflow" claims.
+3. The Pasta instantiation and the census entries in `TrustBoundary.lean`.
+
+Out of scope for now: Zakura's inline-`asm!` transcription (provable later by


Note: this is now in pasta_curves!100

The generated skeleton records every instruction's defining equation first, then clears all the locals' values in one `clear_value`, last local first, and only then derives the per-instruction facts. Clearing a local's value reverts every later local whose value mentions it, so one `clear_value` per instruction was quadratic in the length of the chain: harmless for the helper's 150 locals, over a minute for the multiplication routine's 380. Annotation blocks now follow the group they need, identified by its marker comment `-- <register>: <instruction>`, instead of the `clear_value` line that used to end it, and the round blocks of the helper's proof no longer clear the context at their end, which would now remove equations that later groups use. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

dannywillems · 2026-09-09T12:31:22Z

Note (as discussed): inline assembly (zcash/pasta_curves@7481e92) and carry drop (zcash/pasta_curves@7567e4b#r3968300623) are after the commit pinned in the current state. This would require some changes, if this patch aims to be in line with the final (future) approved state of !100.

daira · 2026-09-09T18:32:57Z

+   instructions modelled over 64-bit registers and the carry flag. Small, reviewable,
+   and cross-checked by executing the model on vectors produced by the real binary.
+2. The transcription of the `.S` into Lean. Generated by a script from the vendored
+   file, never hand-typed; CI regenerates and diffs (same pattern as the field-file


Suggested change

file, never hand-typed; CI regenerates and diffs (same pattern as the field-file

file; CI regenerates and diffs (same pattern as the field-file

If it's generated then it's not hand-typed, so that's redundant.

daira · 2026-09-09T18:37:48Z

+Not modelled formally: the calling convention, stack frame, and memory-safety of
+the FFI boundary. The model treats loads and stores as limb inputs and outputs.


When we switch to the inline assembly form, we should link to the inline assembly RFC and docs, and explain briefly how the Rust compiler uses in/out and other annotations.

The generated skeleton unfolds the routine in the hypothesis that names its result and then, instruction by instruction, extracts that instruction's lets from it (`extract_lets +onlyGivenNames`), records their defining equations, clears their values, and derives the facts. With every let extracted up front, each `clear_value` reverted and re-checked all the later locals and equations, which is quadratic in the length of the chain and exhausted the heartbeat budget on the multiplication routine's 264 locals; with the rest of the chain still folded in the hypothesis, a clear reverts one small equation and one hypothesis. The carry lemmas are applied with their operands explicit, since a literal operand left as a placeholder is not inferred. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

`mulMont_spec`: the result is below `p` and `2^256 * r ≡ lhs * rhs (mod p)`, under two arithmetic conditions. The first, for each of `rhs_1`, `rhs_2`, `rhs_3`, is `lhs * (rhs_i + 1) + p + 3 * 2^254 + 2^128 ≤ 2^320`: it keeps the five-limb accumulator, which enters each round below `lhs + p`, below `2^320` through the round's `adc`s, the last of which discards its carry. The second, `lhs * rhs < 2^256 * p`, keeps the final accumulator below `2 * p`, which one conditional subtraction reduces. The corollaries `mulMont_spec_of_lhs_lt` (`lhs < p`, any four-limb `rhs`) and `mulMont_spec_of_rhs_lt` (any four-limb `lhs`, `rhs < p` with limbs 1 to 3 at most `2^64 - 3`) are the two operand contracts. The proof is the generated skeleton with a fold block and a reduction block per round and a conclusion block: each fold block sums the two carry chains, shows that neither `adc` wraps, and states the accumulator as the previous one plus `lhs * rhs_i`; each reduction block rewrites the cancellation fact to a linear equation, shows that the reduction's `adc`s do not wrap, states the round invariant, and bounds the shifted accumulator below `lhs + p`. The theorem raises its heartbeat budget: its sixty-odd `clear * -` calls in a context of a thousand hypotheses exceed the default in total although none is slow. The design document records the theorem and the sharpened limb bound, and the README's list of what is present mentions the proof. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

daira · 2026-09-09T23:19:40Z

+-- BEGIN mulMont_spec statement
+-- The proof is about 1600 lines of small steps: the generated skeleton is cheap, but its
+-- annotation blocks run some sixty `clear * -` calls in a context of a thousand hypotheses,
+-- and their total exceeds the default per-declaration budget.
+set_option maxHeartbeats 1000000 in
+/-- Montgomery multiplication: the result is below `p` and `2^256 * result ≡ lhs * rhs (mod p)`,
+under two arithmetic conditions that each operand contract implies (`mulMont_spec_of_lhs_lt` and
+`mulMont_spec_of_rhs_lt`). `hsafe` keeps the five-limb accumulator below `2^320` in rounds 1 to 3,
+where it holds the previous round's result (below `lhs + p`) plus `lhs * rhs_i`, and then the low
+limbs of the reduction; without it the `adc` that closes each fold can drop a carry. `hfinal` keeps
+the final accumulator below `2 * p`, which one conditional subtraction reduces. -/


[followed by ~1600 lines of mostly boilerplate]

Ok, so, this may look terrible, but what Claude has done here is actually not unreasonable given the completely ridiculous task it was asked to perform. I think the issue is that the assembler we're trying to prove things about can't have been written by hand. It must have been generated, and we don't have that generator. If we did then we could prove things about the generator, and then the results we want from the generated code would follow, in a nice structured way. As it is, we're forced to do this very silly thing because we've lost the structure in the problem.

I think this is not a blocker to merge this proof. None of the boilerplate has to be checked by hand; to see what it's doing, you check the proof-generator. Most of the 1600 lines are just context management to stop the cost of Lean's proof checking from blowing up, and the method of doing that is well motivated.

It's pretty amazing that it was able to prove this at all in a general theorem prover just using built-in/Mathlib tactics, as opposed to something more specialized to scalable analysis of code in a register-transfer language.

aha. Apparently we do have the code generator:

I'm confirming that the generator exists: Semolina's pasta_mul-armv8.pl, a 644-line Perl script in the Supranational blst-style code-generation pattern, which loops through multiplication and squaring rounds using register arrays for accumulators, moduli, and temporaries.

I'm going to see if we can figure out the pattern and produce a better proof.

Hopefully we don't have to prove anything about Perl. But I think we don't: just translate the Perl to Lean, check that it produces the same code, and then prove stuff about the Lean.

daira mentioned this pull request Sep 8, 2026

Apple AArch64 assembly backend for the Pasta fields zcash/pasta_curves#100

Open

daira commented Sep 8, 2026

View reviewed changes

Comment thread design/aarch64-pasta-mul-verification.md Outdated

daira commented Sep 8, 2026

View reviewed changes

Comment thread design/aarch64-pasta-mul-verification.md

daira and others added 2 commits September 9, 2026 03:06

daira force-pushed the aarch64-pasta-mul branch from a1ca951 to 6afd636 Compare September 9, 2026 02:31

daira and others added 2 commits September 9, 2026 03:40

daira commented Sep 9, 2026

View reviewed changes

Comment thread design/aarch64-pasta-mul-verification.md Outdated

dannywillems reviewed Sep 9, 2026

View reviewed changes

Comment thread scripts/check_aarch64_pasta_mul.sh

daira commented Sep 9, 2026

View reviewed changes

daira and others added 2 commits September 9, 2026 22:36

daira commented Sep 9, 2026

View reviewed changes

daira closed this Sep 10, 2026

daira deleted the aarch64-pasta-mul branch September 10, 2026 04:02

daira changed the title ~~Verify pasta_curves' AArch64 Pasta Montgomery routines~~ [closed due to licencing issues] Verify pasta_curves' AArch64 Pasta Montgomery routines Sep 10, 2026

daira added the wontfix This will not be worked on label Sep 10, 2026

Navigation Menu

[closed due to licencing issues] Verify pasta_curves' AArch64 Pasta Montgomery routines - #35

[closed due to licencing issues] Verify pasta_curves' AArch64 Pasta Montgomery routines#35
daira wants to merge 9 commits into
mainfrom
aarch64-pasta-mul

daira commented Sep 8, 2026 •

edited

Loading

Uh oh!

daira Sep 8, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

daira commented Sep 9, 2026

Uh oh!

dannywillems Sep 9, 2026

Uh oh!

dannywillems Sep 9, 2026

Uh oh!

dannywillems Sep 9, 2026

Uh oh!

Uh oh!

dannywillems commented Sep 9, 2026

Uh oh!

daira Sep 9, 2026

Uh oh!

daira Sep 9, 2026 •

edited

Loading

Uh oh!

daira Sep 9, 2026 •

edited

Loading

Uh oh!

daira Sep 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	file, never hand-typed; CI regenerates and diffs (same pattern as the field-file
	file; CI regenerates and diffs (same pattern as the field-file

		Not modelled formally: the calling convention, stack frame, and memory-safety of
		the FFI boundary. The model treats loads and stores as limb inputs and outputs.

Conversation

daira commented Sep 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What is here

What is not here yet

Uh oh!

daira Sep 8, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

daira commented Sep 9, 2026

Uh oh!

dannywillems Sep 9, 2026

Choose a reason for hiding this comment

Uh oh!

dannywillems Sep 9, 2026

Choose a reason for hiding this comment

Uh oh!

dannywillems Sep 9, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dannywillems commented Sep 9, 2026

Uh oh!

daira Sep 9, 2026

Choose a reason for hiding this comment

Uh oh!

daira Sep 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

daira Sep 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

daira Sep 9, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

daira commented Sep 8, 2026 •

edited

Loading

daira Sep 9, 2026 •

edited

Loading

daira Sep 9, 2026 •

edited

Loading