Skip to content

Simplify 32-bit Montgomery fields#1

Merged
graikos merged 24 commits into
graikos:fast_kb_bb_fieldsfrom
mitschabaude:fast_kb_bb_fields-gregor
Jul 15, 2026
Merged

Simplify 32-bit Montgomery fields#1
graikos merged 24 commits into
graikos:fast_kb_bb_fieldsfrom
mitschabaude:fast_kb_bb_fields-gregor

Conversation

@mitschabaude

@mitschabaude mitschabaude commented Jul 13, 2026

Copy link
Copy Markdown

Summary

  • clean up the generic and native single-word Montgomery reduction APIs, naming, statements, and proofs
  • remove definitions, helpers and theorems that weren't used
  • shorten proofs
  • Fast BabyBear and KoalaBear APIs are reduced enough that I consolidated them into a single file each
  • streamline Mont32Field API
  • make an effort to put the most interesting definitions near the top of large files, in a way that makes it readable. For example, reduceRaw in Native32.lean.

This is a review-by-editing follow-up stacked on graikos/fast_kb_bb_fields (Verified-zkEVM#258).

Performance

The large KoalaBear univariate multiplication benchmark remains at the established baseline:

  • NTT over KoalaBear.Fast.Field: about 4.18 ms
  • fast NTT over KoalaBear.Fast.Field: about 1.11 ms
  • cached-plan fast NTT over KoalaBear.Fast.Field: about 1.11 ms

Generated C was inspected to confirm that field operations remain direct native Montgomery arithmetic with specialized constants and no transported-field calls or division/remainder in the hot conversion path.

@mitschabaude mitschabaude changed the title refactor(fields): clarify Montgomery reduction core Simplify 32-bit Montgomery fields Jul 14, 2026
@mitschabaude
mitschabaude marked this pull request as ready for review July 15, 2026 06:26
@graikos
graikos merged commit e423dee into graikos:fast_kb_bb_fields Jul 15, 2026
1 check failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants