4.4. Principal operations🔗

The ring operations add, subtract, negate, and multiply residues, re-reducing each result so the output is again a standard representative. The standard Add, Sub, Neg, and Mul instances on Hex.ZMod64 dispatch to these, so a + b, a - b, -a, and a * b work directly, and a Lean.Grind.CommRing instance lets the grind tactic reason about them.

def

Hex.ZMod64.add {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.ZMod64 p) :
  Hex.ZMod64 p
Hex.ZMod64.add {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : Hex.ZMod64 p

Add two reduced residues: the residue of the sum of canonical representatives.

This is the kernel-reduction-friendly specification: reducing it unfolds to a single Nat addition and mod, so decide-style proofs walk a straight-line computation. Compiled code instead runs the branchy machine-word implementation addImpl, registered by the @[csimp] theorem add_eq_impl.

def

Hex.ZMod64.sub {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.ZMod64 p) :
  Hex.ZMod64 p
Hex.ZMod64.sub {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : Hex.ZMod64 p

Subtract two residues: the residue of a.toNat + (p - b.toNat), the canonical representative of the modular difference.

Like Hex.ZMod64.add, this is the kernel-reduction-friendly specification; compiled code runs subImpl through the @[csimp] theorem sub_eq_impl.

def

Hex.ZMod64.neg {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) :
  Hex.ZMod64 p
Hex.ZMod64.neg {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) : Hex.ZMod64 p

The additive inverse represented by the complementary residue mod p.

def

Hex.ZMod64.mul {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.ZMod64 p) :
  Hex.ZMod64 p
Hex.ZMod64.mul {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : Hex.ZMod64 p

Multiply two reduced residues and reduce the product mod p.

The trusted runtime contract is the lean_hex_zmod64_mul extern, whose C body must agree with this pure Lean fallback.

Exponentiation uses repeated squaring, and inversion runs the extended-GCD helper from HexArith. For an element coprime to the modulus the result is the modular inverse.

def

Hex.ZMod64.pow {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p)
  (n : ℕ) : Hex.ZMod64 p
Hex.ZMod64.pow {p : ℕ}
  [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p)
  (n : ℕ) : Hex.ZMod64 p

Raise a residue to a natural power using exponentiation by squaring.

The accumulator form keeps the executable path close to the intended downstream runtime usage while preserving a simple semantic contract.

def

Hex.ZMod64.inv {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) :
  Hex.ZMod64 p
Hex.ZMod64.inv {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) : Hex.ZMod64 p

Compute a modular inverse candidate via the integer extended-GCD helper from hex-arith.

When a is coprime to p, this is the canonical inverse mod p; otherwise it still exposes the executable Bezout-derived residue needed by later algebraic layers. The trusted runtime contract is lean_hex_zmod64_inv, which runs the same Euclidean remainder and cofactor recurrence directly in bounded word arithmetic and returns the cofactor modulo p.

4.4.1. Worked example: ring arithmetic🔗

The block below works in ZMod64 7. After supplying the Bounds 7 instance it builds two residues and runs the ring operations on them.

open Hex Hex.ZMod64

namespace HexModArithChapterRing

instance : Bounds 7 := ⟨by⊢ 0 < 7 decideAll goals completed! 🐙, by⊢ 7 < 2 ^ 31 decideAll goals completed! 🐙⟩

-- a = 3 and b = 5 as residues mod 7.
def a : ZMod64 7 := ofNat 7 3
def b : ZMod64 7 := ofNat 7 5

-- Literals reduce: 10 ≡ 3 (mod 7).
#guard a.toNat = 3
#guard (10 : ZMod64 7).toNat = 3

-- 3 + 5 = 8 ≡ 1.
#guard (a + b).toNat = 1
-- 3 - 5 ≡ -2 ≡ 5.
#guard (a - b).toNat = 5
-- 3 · 5 = 15 ≡ 1.
#guard (a * b).toNat = 1
-- 3^5 = 243 ≡ 5.
#guard (a ^ 5).toNat = 5
-- 3⁻¹ ≡ 5, since 3 · 5 ≡ 1.
#guard (inv a).toNat = 5
#guard (inv a * a).toNat = 1

end HexModArithChapterRing