Malachite for Azurite Users: Integers Modulo a Natural
This page maps the operations of Azurite’s AzZMod m type,
its ring of integers modulo an arbitrary natural \(m\), onto their Malachite counterparts, which
are the mod_* operations on
Natural from the
malachite-nz crate. It is a companion of
Malachite for Azurite Users: Naturals, whose
Conventions carry over, and of
Malachite for Azurite Users: Integers Modulo a Power of 2,
which maps the power-of-two specialization AzZModPow2 k and whose conventions this page shares;
only what differs for a general modulus is repeated here. The page covers Azurite as of commit
b5da19d (2026-10-04). The mapping index lists the whole family of pages.
Conventions
The types
An AzZMod m is a structure holding an AzNat residue val together with a proof that val is
less than m, so every value is canonical and equality is structural. The modulus is an AzNat
value index: it is part of the type, but as a limb-level value rather than a Lean Nat, so that
reduction (AzNat.mod against m) never routes a large modulus through Nat arithmetic. A
nonzero modulus is required wherever a residue is constructed, as the instance argument
[NeZero m.toNat], mirroring Mathlib’s ZMod. Malachite has no residue type; its modular
arithmetic is the family of traits
ModAdd,
ModMul,
and so on, which take the modulus as a runtime Natural argument m, require their inputs to be
reduced, and panic otherwise. As on the power-of-two page, the type invariant and the precondition
are the same statement, and each row below maps a method of the type onto the trait method applied
to a reduced Natural with m passed along. A zero modulus is a type with no values in Azurite
and a panic in Malachite.
Typeclasses and traits
AzZMod m is a verified Mathlib CommRing with Neg, Add, Sub, Mul, Azurite’s Square,
OfNat literals, NatCast/IntCast, a LinearOrder by residue value, and a Fintype
instance; for a prime modulus it is a Field. Malachite’s traits stand in for the ring
structure, and Natural’s own Ord for the order.
Categories
Each definition falls into one of five categories:
| meaning | |
|---|---|
| ✓ | A Malachite function does the same thing. |
| ≈ | A Malachite function serves the same purpose, but its specification differs. The notes say how. |
| ⚙ | Malachite does not expose this algorithm or helper; the Malachite column or the notes say what to call instead. |
| — | No counterpart is needed, either because Rust handles it for you or because it is outside Malachite’s scope. The notes say which. |
| ✗ | Malachite does not fully support this yet, but will in a future version. |
Construction and conversion
| Azurite | Malachite | |
|---|---|---|
| ✓ | ofAzNat (m : AzNat) [NeZero m.toNat] (n : AzNat) : AzZMod m |
Mod |
| ⚙ | ofAzInt (m : AzNat) [NeZero m.toNat] (z : AzInt) : AzZMod m |
Mod for Integer, then UnsignedAbs |
| ✓ | ofNat (m : AzNat) [NeZero m.toNat] (a : Nat) : AzZMod m, instance : OfNat (AzZMod m) a, instance : NatCast (AzZMod m) |
Natural::from then Mod |
| ⚙ | instance : IntCast (AzZMod m) |
Integer::from then Mod and UnsignedAbs |
| ✓ | instance : Zero (AzZMod m), instance : One (AzZMod m) |
Natural::ZERO, Natural::ONE |
| — | toAzNat (a : AzZMod m) : AzNat, AzZMod.val : AzNat |
|
| ⚙ | AzZMod.isLt : val.toNat < m.toNat |
ModIsReduced |
| — | instance instNeZeroToNatOfNat (n : Nat) [NeZero n] : NeZero (AzNat.ofNat n).toNat |
|
| ✓ | deriving DecidableEq |
Eq, EqMod |
| ✓ | instance instLinearOrder : LinearOrder (AzZMod m) |
Ord |
| — | ofAzNatRingHom : AzNat →+* AzZMod m, ofAzIntRingHom : AzInt →+* AzZMod m |
|
| — | finEquiv (m : AzNat) : AzZMod m ≃ Fin m.toNat, instance instFintype : Fintype (AzZMod m) |
Reduction. ofAzNat m n is n % m, which is n.mod_op(&m) (or n % &m, the same operation
on naturals); the result is the Natural that stands for the residue from then on. ofAzInt m z
reduces the magnitude and negates it in the ring when z is negative, giving the representative
in \([0, m)\) of a negative integer. Malachite’s Integer has mod_op with an Integer modulus,
whose result takes the modulus’s sign, so for a positive modulus it is nonnegative and
z.mod_op(Integer::from(&m)).unsigned_abs() is the Natural residue, hence ⚙; the IntCast
instance is the same route from a machine integer.
The residue, its proof, and its order. val is the Natural itself in Malachite; the proof
isLt has no value counterpart, but the property it states is n.mod_is_reduced(&m), which
Malachite’s modular operations assert on their inputs. Two residues are equal when their vals
are, so == compares two reduced Naturals and x.eq_mod(&y, &m) two unreduced ones, as
ofAzNat m x = ofAzNat m y does. The LinearOrder compares residues by value, which is
Natural’s Ord; it is a sorting order for canonical forms, not a ring order, on both sides. The
ring homomorphisms package ofAzNat and ofAzInt for mapping polynomial coefficients, and the
Fintype instance states that there are m residues; neither has a Malachite counterpart.
Arithmetic
| Azurite | Malachite | |
|---|---|---|
| ✓ | add (a b : AzZMod m) : AzZMod m, instance : Add (AzZMod m) |
ModAdd, ModAddAssign |
| ✓ | sub (a b : AzZMod m) : AzZMod m, instance : Sub (AzZMod m) |
ModSub, ModSubAssign |
| ✓ | neg (a : AzZMod m) : AzZMod m, instance : Neg (AzZMod m) |
ModNeg, ModNegAssign |
| ✓ | mul (a b : AzZMod m) : AzZMod m, instance : Mul (AzZMod m) |
ModMul, ModMulAssign |
| ✓ | instance instSquare : Square (AzZMod m) |
ModSquare, ModSquareAssign |
| ✓ | pow (a : AzZMod m) (n : ℕ) : AzZMod m, the CommRing npow |
ModPow, ModPowAssign |
| ✓ | powAzNat (a : AzZMod m) (n : AzNat) : AzZMod m |
ModPow |
| ✓ | inv (a : AzZMod m) (h : Nat.Coprime a.val.toNat m.toNat) : AzZMod m |
ModInverse |
| ✓ | tryInv (x : AzZMod m) : Option (AzZMod m) |
ModInverse |
| ⚙ | fieldInv [Fact (Nat.Prime p.toNat)] (a : AzZMod p) : AzZMod p |
ModInverse |
| ≈ | instance instField [Fact (Nat.Prime p.toNat)] : Field (AzZMod p) |
ModDiv, ModInverse |
| — | instance instCommRing : CommRing (AzZMod m), instance instNeZeroToNatOfPrime |
Ring operations. a + b is a.mod_add(b, &m), and likewise sub, mul, and neg, with
\(-0 = 0\) on both sides; the Square instance is mod_square, and pow and powAzNat are
both mod_pow, whose exponent is a Natural, so powAzNat is the exact match and pow the
same function on a Lean Nat. Malachite additionally offers
ModMulPrecomputed,
ModSquarePrecomputed,
and
ModPowPrecomputed,
which take precomputed data about the modulus (from precompute_mod_mul_data and
precompute_mod_pow_data) to speed up repeated operations with the same m; they return the same
values as the plain versions. Azurite reduces by AzNat division each time and has no
precomputed variants.
Inverses and division. A residue is a unit exactly when it is coprime to m. inv takes a
proof of coprimality; tryInv tests it and returns none otherwise, which is exactly
mod_inverse’s Option<Natural>. fieldInv is the total inverse of the field case, prime p,
with the convention \(0^{-1} = 0\); mod_inverse returns None there (and panics on an input of
0 when the modulus is composite), so the spelling is n.mod_inverse(&p).unwrap_or(Natural::ZERO).
The Field instance’s a / b is a · b⁻¹ for a prime modulus;
ModDiv
works for any modulus and returns Some(q) with \(qb \equiv a\) whenever \(\gcd(b, m)\) divides
\(a\), choosing one quotient when b is not a unit, and None otherwise, hence ≈: the two agree
for a prime modulus and b ≠ 0, and differ at b = 0, where the field gives 0 and mod_div
gives Some(0) for a = 0 and None for other a.
Shifts and square roots. Malachite also has
ModShl
and
ModShr,
multiplication and floor division by a power of 2 modulo m with a negative count reversing the
direction, spelled ofAzNat m (a.val <<< s) and ofAzNat m (a.val >>> s) in Azurite, and
ModSqrt,
a modular square root, which AzZMod does not have.
Strings
| Azurite | Malachite | |
|---|---|---|
| ✓ | toString (a : AzZMod m) : String, instance : ToString (AzZMod m) |
Display |
| ≈ | parse (s : String) : Option (AzZMod m) |
FromStr then Mod |
| — | toChars, parseChars, instance : ParsableElement (AzZMod m) |
Formatting and parsing. toString prints the representative in decimal, which is Display
on the Natural. parse reads a natural with AzNat.parse’s rules and reduces it, so "19" is
5 in AzZMod 7; Natural::from_str(s) followed by mod_op(&m) is the same computation, with
the differences in what the two parsers accept
noted on the naturals page. ParsableElement is
Azurite’s typeclass for parsing a coefficient inside a vector, matrix, or polynomial literal.
Internals and the bridge to ZMod
| Azurite | Malachite | |
|---|---|---|
| — | QuadT (m : AzNat) (u a : AzZMod m) and its operations, NormOne, normOneCandidate |
|
| — | toZMod, ofZMod, equivZMod, ringEquivZMod, toZModRingHom |
The quadratic ring. AzZMod.QuadT is the ring \((\mathbb{Z}/m)[T]/(T^2 - uT - a)\) used by
Azurite’s APR-CL primality proof, with its norm, conjugate, and norm-one powering. Malachite’s
primality testing exposes no such intermediate structure, so it is outside the mapping.
Proofs. The ZMod m.toNat bridge is the specification side of the type’s theorems, as
toNat is for AzNat on the naturals page; it has no
counterpart, Malachite’s specification being its documentation and tests. The equivalence lemmas
in Azurite/AzZMod/Equiv/ are likewise not mapped.