feat: add modular UInt64 arithmetic operations by kim-em · Pull Request #15077 · leanprover/lean4

kim-em · 2026-09-09T01:29:48Z

This PR adds UInt64.mulMod, UInt64.powMod, and UInt64.invMod? for fixed-width modular arithmetic without overflowing intermediate products. powMod accepts an arbitrary Nat exponent, and invMod? returns none for a zero modulus or noncoprime inputs.

The kernel-visible definitions use natural-number arithmetic. mulMod is overridden by a C implementation using 128-bit intermediates where available and a portable double-and-add fallback otherwise; no Lean primitive exposes a widening 64-by-64 multiply. powMod and invMod? are instead overridden by word-sized Lean loops installed with @[csimp], so their compiled behaviour is proved equal to the definitions rather than trusted. powMod consumes the exponent 64 bits at a time, costing one Nat division per word rather than one per bit.

toNat_mulMod, toNat_powMod and their zero-modulus counterparts characterize the results of mulMod and powMod, and mulMod_lt and powMod_lt bound them. For invMod?, isSome_invMod? says an inverse exists exactly when Nat.gcd of the inputs is one, and invMod?_eq_some_iff identifies the returned value by its defining equation together with the bound that makes it unique.

The operations are tested against independent exact-Nat references over a boundary matrix that includes exponents on both sides of the scalar and big-Nat representation boundary, exponents whose middle 64-bit chunks are zero, and Fermat's little theorem for known primes. A separate C test forces the portable multiplication branch and compares it with 128-bit arithmetic on one million deterministic pseudorandom inputs.

These operations provide reusable runtime primitives for UInt64-backed residue and finite-field libraries.

🤖 Generated with Claude Code

mathlib-lean-pr-testing · 2026-09-09T01:49:57Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9e3f6c6c8671b3270684c4ce46b40449929f93f2 --onto d359ee1694e7e93efbcf2a23a56ea92340ccd001. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-09 01:49:57)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9e3f6c6c8671b3270684c4ce46b40449929f93f2 --onto fe53f21e05980b97d7bbb6717cf7566e3700e576. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-10 06:40:46)

leanprover-bot · 2026-09-09T01:49:59Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9e3f6c6c8671b3270684c4ce46b40449929f93f2 --onto c155094f54eab345cca3da867dbd888a34fbf0d2. You can force reference manual CI using the force-manual-ci label. (2026-09-09 01:49:59)

TwoFX

Codex believes that power and inverse do not really need native implementations, see https://gist.github.com/TwoFX/fbbe5362c992e509a4044cd6f8c50172 and https://gist.github.com/TwoFX/a81c8df6b457eed0a44da36b5e0c8ff5

Replace the `lean_uint64_pow_mod` and `lean_uint64_inv_mod` externs with word-sized Lean loops installed via `@[csimp]`, so the compiled behaviour is proved equal to the natural-number definitions rather than trusted. `powModImpl` consumes a `Nat` exponent 64 bits at a time, costing one division per word rather than one per bit; the previous extern halved an mpz exponent on every bit and never returned to machine-word arithmetic. `invModImpl` runs the extended Euclidean loop entirely in `UInt64`. `mulMod` keeps its extern, since no Lean primitive exposes a widening 64-by-64 multiply. Add `toNat_mulMod` and `toNat_powMod`, which the equivalence proofs need. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

kim-em · 2026-09-10T06:20:05Z

Codex believes that power and inverse do not really need native implementations, see https://gist.github.com/TwoFX/fbbe5362c992e509a4044cd6f8c50172 and https://gist.github.com/TwoFX/a81c8df6b457eed0a44da36b5e0c8ff5

Thank you, good catch. I've double checked this, and agree. So mulMod survives as an extern, and powMod and invMod? now have @[csimp]'d implementations.

Add `toNat_mulMod_zero`, `toNat_powMod_zero` and `powMod_lt`, and prove that `invMod?` computes a multiplicative inverse: `isSome_invMod?` characterizes when one exists in terms of `Nat.gcd`, `mulMod_of_invMod?_eq_some` gives the defining equation, and `lt_of_invMod?_eq_some` gives the range. The `invMod?` proofs go through `invMod?_go_spec`, the loop invariant of the extended Euclidean algorithm: the coefficient sequence satisfies `oldS * a ≡ oldR` and `s * a ≡ r` modulo the modulus while `Nat.gcd oldR r` is preserved. Reorder the module so the specification precedes the runtime implementations. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Add `invMod?_eq_some_iff`, identifying the result of `invMod?` by its defining equation: `invMod? a modulus = some x` exactly when `x < modulus` and `mulMod a x modulus = 1 % modulus`. The bound is part of the characterization, since the equation alone also admits representatives shifted by `modulus`. Also run fixed vectors unconditionally in the portable multiplication test. Every assertion was previously guarded by the presence of a 128-bit type, so on a compiler that genuinely lacks one the test did nothing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Rework the private lemmas supporting the modular `UInt64` operations, cutting the module from 617 to 480 lines. The public statements, the compiled definitions, and the generated C are unchanged. The coefficient step of the extended Euclidean loop no longer needs a modular cancellation lemma: since `nextS` is congruent to `oldS + (modulus - product)`, multiplying through leaves a multiple of the modulus, which vanishes. `nextS_mul_mod` states that step directly, replacing two helpers. `invMod?_eq_some_spec` factors out the unfolding that the three `invMod?` characterization lemmas each repeated, and `mul_pow_step` does the same for the squaring step shared by the word and chunk loops. `gcd_eq_one_of_mul_mod` no longer requires a positive modulus. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Reduce the module from 480 to 454 lines. The public statements, the compiled definitions, and the generated C are unchanged. `invMod?_go_spec` and `invMod?_spec` now destructure the returned pair with a `let`, so the conclusions name their components instead of repeating the call, and `invMod?_go_spec` takes its invariants as arguments rather than introducing them. `gcd_eq_one_of_mul_mod` goes through `Nat.gcd_dvd_gcd_mul_right_left`, which absorbs the modulus-one case. Correct the runtime implementation comment: `powMod` already multiplies through the `mulMod` extern, so it is the one-bit-at-a-time exponent handling that is slow there, not intermediate products. That description applies to the Euclidean loop in `invMod?`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

TwoFX · 2026-09-11T08:33:29Z

+  if exponent = 0 then
+    1 % modulus
+  else
+    let result := powMod (mulMod base base modulus) (exponent / 2) modulus
+    if exponent % 2 = 1 then mulMod result base modulus else result
+termination_by exponent
+decreasing_by omega


If you're going to csimp it away anyway, why not just make this .ofNat ((base.toNat ^ exponent) % modulus.toNat))?

TwoFX · 2026-09-11T08:36:05Z

+  if modulus = 0 then
+    none
+  else
+    let rec go (oldR r oldS s : Nat) : Nat × Nat :=


This is fine for now, but eventually we'll probably want an extended Euclidean algorithm as a public API on Nat (mathlib already has this) and go through that.

I'll do this as a follow up, but not in this PR.

Use direct division and remainder lemmas for termination, simplify inverse existence, and combine the inverse implementation’s base cases.

feat: add modular UInt64 arithmetic operations

b3a1bc3

kim-em added the changelog-library Library label Sep 9, 2026

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 9, 2026

kim-em added 4 commits September 9, 2026 02:16

test: strengthen UInt64 modular arithmetic validation

a6eca62

test: avoid C++ runtime in mulMod fallback check

1bb228f

test: select portable C compiler in mulMod check

3b0e3f7

test: compile mulMod check with stage toolchain

1855cb3

TwoFX reviewed Sep 9, 2026

View reviewed changes

kim-em and others added 4 commits September 10, 2026 06:34

TwoFX reviewed Sep 11, 2026

View reviewed changes

refactor: simplify UInt64.powMod specification

4943d87

kim-em mentioned this pull request Sep 15, 2026

feat: add a public extended Euclidean algorithm for natural numbers #15160

Draft

kim-em added 2 commits September 15, 2026 06:22

test: remove redundant UInt64 lemma examples

269f088

refactor: simplify UInt64 modular arithmetic proofs

fe5fb0f

Use direct division and remainder lemmas for termination, simplify inverse existence, and combine the inverse implementation’s base cases.

Navigation Menu

feat: add modular UInt64 arithmetic operations - #15077

feat: add modular UInt64 arithmetic operations#15077
kim-em wants to merge 13 commits into
leanprover:masterfrom
kim-em:feat/uint64-modular-arithmetic

kim-em commented Sep 9, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing Bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Sep 9, 2026

Uh oh!

TwoFX left a comment

Uh oh!

kim-em commented Sep 10, 2026

Uh oh!

TwoFX Sep 11, 2026

Uh oh!

kim-em Sep 15, 2026

Uh oh!

TwoFX Sep 11, 2026

Uh oh!

kim-em Sep 15, 2026

Uh oh!

kim-em Sep 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

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

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Sep 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Sep 9, 2026

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

kim-em commented Sep 10, 2026

Uh oh!

TwoFX Sep 11, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em Sep 15, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Sep 11, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em Sep 15, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em Sep 15, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

kim-em commented Sep 9, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Sep 9, 2026 •

edited

Loading