Explore AArch64 Pasta ASM register pressure without regressing large-batch verification

[ValarDragon]

Motivation

#66 moves Pasta multiplication and squaring to register-only AArch64 inline
assembly. The current implementation improves proving and the exact standalone
MSM workloads, but the batch-64 Orchard verifier screen did not show the
expected corresponding improvement.

This is worth revisiting, but it is lower priority than the next verifier
optimization. The goal is to preserve the inline-ASM benefits while finding a
better register-pressure/code-size boundary for large-batch verification.

What we already tried

The experiments were isolated so that compiler effects were attributable:

• specializing the full per-field P0, P1, and INV constants;
• deriving INV from P0 - 2 to remove an input operand;
• reusing the dead first RHS limb as the Montgomery quotient register;
• streaming RHS limbs to shorten their live ranges;
• reusing the low accumulator as the quotient register;
• further quotient/scratch-register coalescing;
• rolling the squaring reduction through dead product registers;
• combinations of the multiplication and squaring changes;
• forcing only multiplication or only squaring inline;
• forcing both raw field operations out of line; and
• removing the two #[inline(always)] hints.

Several variants reduced static instructions or stack references, but none
produced a consistent full-workload win. Streaming operands and globally
outlining the raw field leaves were clearly worse. Removing the forced-inline
hints was codegen-neutral in focused binaries and is useful source hygiene, but
is not a performance optimization.

Important current-code observation

In the batch-verifier binary, both best_multiexp and
BoothBuckets::sum are already emitted as separate functions. Adding
#[inline(never)] around the batch verifier, best_multiexp, or the entire
window sum is therefore unlikely to change the relevant code generation.

Bucket::add_assign, including the mixed projective-affine formula beneath
it, is currently inlined into BoothBuckets::sum. That is the narrowest
plausible boundary to investigate.

Proposed follow-up

1. Instrument the real Orchard batch verifier with a fixed authenticated corpus
   and separately time:

   • per-proof decoding/transcript/aggregation;
   • batch scaling and merging; and
   • the final MSM::eval / best_multiexp.

   First confirm whether the B64 difference is actually inside the final MSM.
   The exact 5,678-term standalone MSM already improves, so the discrepancy may
   instead be elsewhere in verification or simply screen noise.

2. If the final MSM is the source, prototype a large-MSM-only out-of-line mixed
   add:

   • retain the inline field-ASM leaves unchanged;
   • select the large-MSM loop once, outside the digit loop;
   • avoid a per-digit runtime branch;
   • keep the existing inline path for the prover and smaller MSMs; and
   • compare instruction count, stack traffic, text size, and call overhead.

   At B64 this may introduce roughly 164,000 calls, so it should only survive if
   reduced spills or instruction-cache pressure more than repay that cost.

3. If the slowdown is in per-proof verifier work, place an out-of-line boundary
   around the specific high-level curve formula identified by the phase timing,
   rather than outlining multiplication and squaring globally.

4. As the deeper option, implement a Pasta-specific fused mixed-add leaf for
   large MSM buckets. This would provide explicit register allocation and one
   call boundary while leaving the existing inline field ASM available
   elsewhere. Mixed addition is a more relevant B64 target than fused point
   doubling.

5. If none of those work, revisit the Montgomery kernel as a lower-live-range
   CIOS schedule rather than continuing local operand renames.

Benchmark gate

Use the standard laptop method:

• one authenticated corpus of 64 distinct valid proofs, loaded outside timing;
• short field, curve, exact MSM 2,150/5,678, prover, B1, and B64 screens;
• phase timing from the real Orchard verifier, not standalone MSM alone; and
• a balanced full-workload confirmation before claiming a speedup.

Do not promote a change that only improves static counts or a standalone
microbenchmark. Preserve the prover gain and require a reproducible B64
improvement or neutrality.

[ValarDragon]

Large-MSM out-of-line bucket addition

Source boundary

• Control: 9ee4283c4d33f7b0c6fe8ea9ba372861221c6102
• Candidate: 85ca347f9fbe26d2ffca57f64e690eba6e2c480b
• The candidate retains the inline AArch64 field ASM.
• MSMs with at least 4,096 terms call an out-of-line mixed bucket-add leaf.
• Smaller MSMs retain the existing inlined path.
• Public and crate-internal API delta: none.

Correctness

• Inlined-versus-outlined window sums match for every c=8 window.
• Focused multiexponentiation tests pass at one and three Rayon workers.
• Rust 1.88 formatting and diff checks pass.

Short laptop screen

This is diagnostic evidence, not a publishable performance claim. The laptop
was on AC power, and the pre/post competing-process snapshots were empty.

Workload	Mean change	Median change
MSM, 2,150 terms	+0.258%	-0.061%
MSM, 5,678 terms	-0.988%	-0.939%
Orchard one-action prover	+1.576%	+0.718%
Orchard verifier, batch 1	-0.162%	-0.074%
Orchard verifier, batch 64	+0.040%	+0.275%

Positive values mean lower candidate latency. Only the 5,678-term MSM and B64
cross the 4,096-term threshold. The direct large-MSM result shows roughly 1%
call overhead, while B64 is flat at the screen's noise scale. The candidate is
rejected.

The 5,678-term MSM is about 25.2 ms of the roughly 80.1 ms B64 verification
measurement. A 1% change inside that MSM therefore moves total B64 time by only
about 0.3%, which this short screen cannot resolve reliably. The apparent
prover improvement is also noise: the prover's roughly 2,049-term MSMs stay on
the unchanged inlined path.