hex

4.2. The residue type🔗

The bounds typeclass states the two facts an UInt64-backed modulus must satisfy: it is positive, and it does not exceed one machine word.

🔗type class
Hex.ZMod64.Bounds (p : ℕ) : Prop
Hex.ZMod64.Bounds (p : ℕ) : Prop

ZMod64 p is only valid when p is positive and strictly below 2^31. This small-modulus invariant keeps every residue and the modulus in a UInt64, makes the sum of two residues fit in a word without carry, and keeps the product of two residues below 2^62, so the modular multiply reduces a single word (no __uint128_t) and future convolution kernels can accumulate several products before one reduction (Barrett/lazy). Every current and anticipated application (Berlekamp-Zassenhaus, LLL, matrix work) uses small primes, so no needed generality is lost.

Instance Constructor

Hex.ZMod64.Bounds.mk

Methods

pPos : 0 < p

The modulus is positive.

pLtR : p < 2 ^ 31

The modulus is strictly below 2^31.

A residue is the backing word together with a proof that the word, read as a Nat, is already reduced below the modulus. Because that proof pins down a unique word for each residue value, structural equality on Hex.ZMod64 coincides with equality of representatives.

🔗structure
Hex.ZMod64 (p : ℕ) [Hex.ZMod64.Bounds p] : Type
Hex.ZMod64 (p : ℕ) [Hex.ZMod64.Bounds p] :
  Type

Residues mod p stored in a single machine word, with a proof of reduction.

Constructor

Hex.ZMod64.mk

Fields

val : UInt64

The backing machine word holding the standard representative.

isLt : self.val.toNat < p

Proof that the stored word is already reduced below the modulus.

The canonical view of a residue is its Nat representative, and the two extensionality principles let proofs reduce equality of residues to equality of those representatives.

🔗def
Hex.ZMod64.toNat {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) : ℕ
Hex.ZMod64.toNat {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) : ℕ

View a residue as its reduced Nat representative.

🔗theorem
Hex.ZMod64.ext_toNat {p : ℕ} [Hex.ZMod64.Bounds p] {a b : Hex.ZMod64 p}
  (h : a.toNat = b.toNat) : a = b
Hex.ZMod64.ext_toNat {p : ℕ}
  [Hex.ZMod64.Bounds p]
  {a b : Hex.ZMod64 p}
  (h : a.toNat = b.toNat) : a = b

Extensionality for residues via their canonical Nat representatives.

🔗theorem
Hex.ZMod64.eq_iff_toNat_eq {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : a = b ↔ a.toNat = b.toNat
Hex.ZMod64.eq_iff_toNat_eq {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  a = b ↔ a.toNat = b.toNat

Two residues are equal exactly when their canonical representatives agree.