class Hex.ZMod64.Bounds (p : Nat) : 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.

• pPos : 0 < p

  The modulus is positive.

• pLtR : p < 2 ^ 31

  The modulus is strictly below 2^31.

theorem Hex.ZMod64.Bounds.pLtWord (p : Nat) [Bounds p] : p < UInt64.word

The modulus is strictly below the machine-word size 2^64, so it and every residue fit in a UInt64. Derived from the p < 2^31 bound.

instance Hex.ZMod64.boundsTwo : Bounds 2

The canonical Bounds 2, for the whole project.

Bounds has no general instance: the two conditions are decidable for a literal, but instance search cannot run decide on the goal, so every modulus needs its own witness. p = 2 is wanted almost everywhere (GF(2), the FpPoly 2 pow-chain checkers, the Conway table), and it used to be re-declared in each place: six public copies across five files, in HexBerlekamp, HexConway, HexGF2Mathlib (three) and HexGFqMathlib. Any module importing several saw that many equal-priority candidates, and further copies in test and guard modules were captured into emitted proof terms, producing errors naming constants nobody had written.

Declaring it here, alongside the class, gives every consumer one candidate reachable by the import they already have. A module needing some other modulus should use local instance, or a private theorem plus attribute [local instance] to keep the name unexported too. Never private instance: that leaves the instance visible to search in importing modules while making its name unreferenceable there.

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

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

• 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.

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

View a residue as its reduced Nat representative.

Equations

• a.toNat = a.val.toNat

def Hex.ZMod64.toUInt64 {p : Nat} [Bounds p] (a : ZMod64 p) : UInt64

View a residue as its underlying UInt64 word.

Equations

• a.toUInt64 = a.val

@[instance_reducible]

instance Hex.ZMod64.instDecidableEq {p : Nat} [Bounds p] : DecidableEq (ZMod64 p)

Equality of residues is equality of the stored words: the reduction proof is irrelevant.

Equations

• a.instDecidableEq b = if h : a.val = b.val then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.ZMod64.instCoeOutUInt64 {p : Nat} [Bounds p] : CoeOut (ZMod64 p) UInt64

Equations

• Hex.ZMod64.instCoeOutUInt64 = { coe := Hex.ZMod64.toUInt64 }

@[instance_reducible]

instance Hex.ZMod64.instCoeOutNat {p : Nat} [Bounds p] : CoeOut (ZMod64 p) Nat

Equations

• Hex.ZMod64.instCoeOutNat = { coe := Hex.ZMod64.toNat }

@[simp]

theorem Hex.ZMod64.toUInt64_eq_val {p : Nat} [Bounds p] (a : ZMod64 p) : a.toUInt64 = a.val

Converting a residue to UInt64 exposes exactly the stored word.

@[simp]

theorem Hex.ZMod64.toNat_eq_val {p : Nat} [Bounds p] (a : ZMod64 p) : a.toNat = a.val.toNat

Converting a residue to Nat reads the stored word as its canonical representative.

@[simp]

theorem Hex.ZMod64.toNat_lt {p : Nat} [Bounds p] (a : ZMod64 p) : a.toNat < p

The Nat view of a residue is always the canonical representative below the modulus.

theorem Hex.ZMod64.ext {p : Nat} [Bounds p] {a b : ZMod64 p} (h : a.val = b.val) : a = b

Extensionality for residues via equality of their stored machine words.

theorem Hex.ZMod64.ext_iff {p : Nat} [Bounds p] {a b : ZMod64 p} : a = b ↔ a.val = b.val

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

Extensionality for residues via their canonical Nat representatives.

def Hex.ZMod64.normalize (p n : Nat) : Nat

Reduce a Nat representative modulo p.

Equations

• Hex.ZMod64.normalize p n = n % p

theorem Hex.ZMod64.normalize_lt (p n : Nat) [Bounds p] : normalize p n < p

Normalization always returns a canonical representative below the modulus.

@[simp]

theorem Hex.ZMod64.normalize_of_lt {q n : Nat} (hn : n < q) : normalize q n = n

Normalizing an already canonical representative leaves it unchanged.

@[simp]

theorem Hex.ZMod64.normalize_toNat {p : Nat} [Bounds p] (a : ZMod64 p) : normalize p a.toNat = a.toNat

Normalizing a residue's canonical representative leaves it unchanged.

def Hex.ZMod64.ofNat (p n : Nat) [Bounds p] : ZMod64 p

Build a reduced residue by taking the Nat representative mod p.

The bound p < 2^64 ensures the reduced representative is stored faithfully in the backing UInt64.

Equations

• Hex.ZMod64.ofNat p n = { val := UInt64.ofNatLT (Hex.ZMod64.normalize p n) ⋯, isLt := ⋯ }

@[simp]

theorem Hex.ZMod64.toNat_ofNat {p : Nat} [Bounds p] (n : Nat) : (ofNat p n).toNat = n % p

The Nat representative of ofNat p n is n reduced modulo p.

@[simp]

theorem Hex.ZMod64.val_toNat_ofNat {p : Nat} [Bounds p] (n : Nat) : (ofNat p n).val.toNat = n % p

The stored word of ofNat p n, viewed as a Nat, is n reduced modulo p.

@[simp]

theorem Hex.ZMod64.ofNat_toNat {p : Nat} [Bounds p] (a : ZMod64 p) : ofNat p a.toNat = a

Constructing a residue from its canonical representative is the identity.

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

Two residues are equal exactly when their canonical representatives agree.

@[simp]

theorem Hex.ZMod64.ofNat_mod {p : Nat} [Bounds p] (n : Nat) : ofNat p (n % p) = ofNat p n

A reduced representative constructs the same residue as the original representative.

@[simp]

theorem Hex.ZMod64.ofNat_normalize {p : Nat} [Bounds p] (n : Nat) : ofNat p (normalize p n) = ofNat p n

Normalizing before constructing a residue does not change the residue.

theorem Hex.ZMod64.ofNat_eq_iff_toNat_eq {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) : ofNat p n = a ↔ n % p = a.toNat

Characterise when an arbitrary representative builds a given residue.

theorem Hex.ZMod64.eq_ofNat_iff_toNat_eq {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) : a = ofNat p n ↔ a.toNat = n % p

Characterise when a residue is built from an arbitrary representative.

theorem Hex.ZMod64.ofNat_eq_ofNat_iff_mod_eq {p : Nat} [Bounds p] (x y : Nat) : ofNat p x = ofNat p y ↔ x % p = y % p

Equality of residues built from arbitrary Nat representatives is equality modulo p.

def Hex.ZMod64.values (p : Nat) [Bounds p] : List (ZMod64 p)

All canonical residues modulo p, listed in representative order.

Equations

• Hex.ZMod64.values p = List.map (fun (n : Nat) => Hex.ZMod64.ofNat p n) (List.range p)

@[simp]

theorem Hex.ZMod64.values_length {p : Nat} [Bounds p] : (values p).length = p

The canonical list of residues modulo p has one entry for each representative.

theorem Hex.ZMod64.mem_values {p : Nat} [Bounds p] (a : ZMod64 p) : a ∈ values p

Every residue appears in values.

@[simp]

theorem Hex.ZMod64.mem_values_iff {p : Nat} [Bounds p] (a : ZMod64 p) : a ∈ values p ↔ True

Membership in the canonical residue list is automatic for every residue.

theorem Hex.ZMod64.ofNat_eq_ofNat_iff_of_lt {p : Nat} [Bounds p] {x y : Nat} (hx : x < p) (hy : y < p) : ofNat p x = ofNat p y ↔ x = y

Reduced representatives below p construct the same residue exactly when the representatives are equal.

theorem Hex.ZMod64.values_nodup {p : Nat} [Bounds p] : (values p).Nodup

The canonical residue list has no duplicate entries.

def Hex.ZMod64.zero {p : Nat} [Bounds p] : ZMod64 p

The zero residue class.

Equations

• Hex.ZMod64.zero = Hex.ZMod64.ofNat p 0

def Hex.ZMod64.one {p : Nat} [Bounds p] : ZMod64 p

The residue class of one.

Equations

• Hex.ZMod64.one = Hex.ZMod64.ofNat p 1

def Hex.ZMod64.modulusWord (p : Nat) (hp : p < UInt64.word) : UInt64

The modulus as a UInt64 word when p < 2^64.

Equations

• Hex.ZMod64.modulusWord p hp = UInt64.ofNatLT p ⋯

def Hex.ZMod64.complementWord (p : Nat) [Bounds p] (_hp : p < UInt64.word) : UInt64

The correction word 2^64 - p used when p < 2^64.

Equations

• Hex.ZMod64.complementWord p _hp = UInt64.ofNatLT (UInt64.word - p) ⋯

theorem Hex.ZMod64.reduceOnce_reduce_lt {p : Nat} [Bounds p] (s : UInt64) (hs : s.toNat < 2 * p) (h : modulusWord p ⋯ ≤ s) : (s - modulusWord p ⋯).toNat < p

Reduce branch of reduceOnce: subtracting the modulus word from a faithful representative below 2 * p lands back in canonical range < p.

theorem Hex.ZMod64.reduceOnce_noReduce_lt {p : Nat} [Bounds p] (s : UInt64) (_hs : s.toNat < 2 * p) (h : ¬modulusWord p ⋯ ≤ s) : s.toNat < p

No-reduce branch of reduceOnce: a faithful representative already below the modulus word is already canonical.

def Hex.ZMod64.reduceOnce {p : Nat} [Bounds p] (s : UInt64) (hs : s.toNat < 2 * p) : ZMod64 p

Canonicalise a machine word whose value is a faithful representative in [0, 2*p) by one conditional subtraction of the modulus word.

Under the p < 2^31 bound add produces such a representative with no machine-word wraparound, so this single reduce branch replaces the former three-way carry analysis and keeps the runtime division-free.

Equations

• Hex.ZMod64.reduceOnce s hs = if h : Hex.ZMod64.modulusWord p ⋯ ≤ s then { val := s - Hex.ZMod64.modulusWord p ⋯, isLt := ⋯ } else { val := s, isLt := ⋯ }

noncomputable def Hex.ZMod64.add {p : Nat} [Bounds p] (a b : ZMod64 p) : 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.

Equations

• a.add b = Hex.ZMod64.ofNat p (a.toNat + b.toNat)

def Hex.ZMod64.addImpl {p : Nat} [Bounds p] (a b : ZMod64 p) : ZMod64 p

Runtime implementation of Hex.ZMod64.add: one faithful machine-word addition followed by a single conditional subtraction of the modulus (reduceOnce), with no carry branch and no division. Its correctness proof is the @[csimp] theorem add_eq_impl. Under p < 2^31 the sum a.val + b.val never overflows the word.

Equations

• a.addImpl b = Hex.ZMod64.reduceOnce (a.val + b.val) ⋯

noncomputable def Hex.ZMod64.sub {p : Nat} [Bounds p] (a b : ZMod64 p) : 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.

Equations

• a.sub b = Hex.ZMod64.ofNat p (a.toNat + (p - b.toNat))

theorem Hex.ZMod64.sub_noBorrow_lt {p : Nat} [Bounds p] (a b : ZMod64 p) (h : b.val ≤ a.val) : (a.val - b.val).toNat < p

No-borrow branch of sub: when b ≤ a the machine-word difference is already the canonical representative < p.

theorem Hex.ZMod64.sub_borrow_lt {p : Nat} [Bounds p] (a b : ZMod64 p) (h : ¬b.val ≤ a.val) : (a.val + (modulusWord p ⋯ - b.val)).toNat < p

Borrow branch of sub: when a < b the faithful word a + (p - b) has representative p - (b - a), which stays in canonical range < p.

def Hex.ZMod64.subImpl {p : Nat} [Bounds p] (a b : ZMod64 p) : ZMod64 p

Runtime implementation of Hex.ZMod64.sub: a single sign test picks the fast common path a - b (already canonical when b ≤ a) or the corrected a + (p - b), with no division and no wraparound reasoning. Its correctness proof is the @[csimp] theorem sub_eq_impl. Under p < 2^31 neither branch overflows the word.

Equations

• a.subImpl b = if h : b.val ≤ a.val then { val := a.val - b.val, isLt := ⋯ } else { val := a.val + (Hex.ZMod64.modulusWord p ⋯ - b.val), isLt := ⋯ }

@[extern lean_hex_zmod64_mul]

def Hex.ZMod64.mul {p : Nat} [Bounds p] (a b : ZMod64 p) : 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.

Equations

• a.mul b = Hex.ZMod64.ofNat p (a.toNat * b.toNat)

@[extern lean_hex_zmod64_pow]

def Hex.ZMod64.pow {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) : 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.

Equations

• a.pow n = Hex.ZMod64.pow.go a Hex.ZMod64.one n

@[irreducible]

def Hex.ZMod64.pow.go {p : Nat} [Bounds p] (base acc : ZMod64 p) (k : Nat) : ZMod64 p

Equations

• Hex.ZMod64.pow.go base acc 0 = acc
• Hex.ZMod64.pow.go base acc m.succ = Hex.ZMod64.pow.go (base.mul base) (if (m + 1) % 2 = 0 then acc else acc.mul base) ((m + 1) / 2)

@[extern lean_hex_zmod64_inv]

def Hex.ZMod64.inv {p : Nat} [Bounds p] (a : ZMod64 p) : 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.

Equations

• a.inv = match HexArith.Int.extGcd (Int.ofNat a.toNat) (Int.ofNat p) with | (fst, s, snd) => Hex.ZMod64.ofNat p (s % Int.ofNat p).toNat

@[simp]

theorem Hex.ZMod64.toNat_add {p : Nat} [Bounds p] (a b : ZMod64 p) : (a.add b).toNat = (a.toNat + b.toNat) % p

Addition agrees with addition of canonical representatives modulo p.

@[csimp]

theorem Hex.ZMod64.add_eq_impl : @add = @addImpl

The kernel-facing add and the runtime addImpl compute the same residue. Registered @[csimp], so compiled code runs the division-free machine-word implementation while kernel reduction sees the one-line specification.

@[simp]

theorem Hex.ZMod64.toNat_sub {p : Nat} [Bounds p] (a b : ZMod64 p) : (a.sub b).toNat = (a.toNat + (p - b.toNat)) % p

Subtraction agrees with modular subtraction of canonical representatives.

@[csimp]

theorem Hex.ZMod64.sub_eq_impl : @sub = @subImpl

The kernel-facing sub and the runtime subImpl compute the same residue. Registered @[csimp], so compiled code runs the division-free machine-word implementation while kernel reduction sees the one-line specification.

@[instance_reducible]

instance Hex.ZMod64.instZero {p : Nat} [Bounds p] : Zero (ZMod64 p)

Equations

• Hex.ZMod64.instZero = { zero := Hex.ZMod64.zero }

@[instance_reducible]

instance Hex.ZMod64.instOne {p : Nat} [Bounds p] : One (ZMod64 p)

Equations

• Hex.ZMod64.instOne = { one := Hex.ZMod64.one }

@[instance_reducible]

instance Hex.ZMod64.instAdd {p : Nat} [Bounds p] : Add (ZMod64 p)

Equations

• Hex.ZMod64.instAdd = { add := Hex.ZMod64.add }

@[instance_reducible]

instance Hex.ZMod64.instSub {p : Nat} [Bounds p] : Sub (ZMod64 p)

Equations

• Hex.ZMod64.instSub = { sub := Hex.ZMod64.sub }

@[instance_reducible]

instance Hex.ZMod64.instMul {p : Nat} [Bounds p] : Mul (ZMod64 p)

Equations

• Hex.ZMod64.instMul = { mul := Hex.ZMod64.mul }

@[instance_reducible]

instance Hex.ZMod64.instPowNat {p : Nat} [Bounds p] : Pow (ZMod64 p) Nat

Equations

• Hex.ZMod64.instPowNat = { pow := Hex.ZMod64.pow }

@[instance_reducible]

instance Hex.ZMod64.instInv {p : Nat} [Bounds p] : Inv (ZMod64 p)

Equations

• Hex.ZMod64.instInv = { inv := Hex.ZMod64.inv }

@[simp]

theorem Hex.ZMod64.toNat_zero {p : Nat} [Bounds p] : ZMod64.zero.toNat = 0

The canonical representative of the zero residue is 0.

@[simp]

theorem Hex.ZMod64.toNat_one {p : Nat} [Bounds p] : ZMod64.one.toNat = 1 % p

The canonical representative of the one residue is 1 % p.

theorem Hex.ZMod64.add_eq_ofNat {p : Nat} [Bounds p] (a b : ZMod64 p) : a.add b = ofNat p (a.toNat + b.toNat)

Addition is the residue built from the sum of canonical representatives.

theorem Hex.ZMod64.add_op_eq_ofNat {p : Nat} [Bounds p] (a b : ZMod64 p) : a + b = ofNat p (a.toNat + b.toNat)

Operator-level form of add_eq_ofNat.

theorem Hex.ZMod64.sub_eq_ofNat {p : Nat} [Bounds p] (a b : ZMod64 p) : a.sub b = ofNat p (a.toNat + (p - b.toNat))

Subtraction is the residue built from the modular difference of representatives.

theorem Hex.ZMod64.sub_op_eq_ofNat {p : Nat} [Bounds p] (a b : ZMod64 p) : a - b = ofNat p (a.toNat + (p - b.toNat))

Operator-level form of sub_eq_ofNat.

@[simp]

theorem Hex.ZMod64.toNat_mul {p : Nat} [Bounds p] (a b : ZMod64 p) : (a.mul b).toNat = a.toNat * b.toNat % p

Multiplication agrees with multiplication of canonical representatives modulo p.

theorem Hex.ZMod64.mul_eq_ofNat {p : Nat} [Bounds p] (a b : ZMod64 p) : a.mul b = ofNat p (a.toNat * b.toNat)

Multiplication is the residue built from the product of canonical representatives.

theorem Hex.ZMod64.mul_op_eq_ofNat {p : Nat} [Bounds p] (a b : ZMod64 p) : a * b = ofNat p (a.toNat * b.toNat)

Operator-level form of mul_eq_ofNat.

theorem Hex.ZMod64.toNat_inv_def {p : Nat} [Bounds p] (a : ZMod64 p) : a.inv.toNat = ((match HexArith.Int.extGcd (Int.ofNat a.toNat) (Int.ofNat p) with | (fst, s, snd) => s) % Int.ofNat p).toNat % p

Definition-level representative equation for the extended-GCD inverse candidate.

Most callers should prefer inv_mul_eq_one_of_coprime; this lemma exposes the exact executable residue produced by inv. It is intentionally not tagged as a default simplification rule, since unfolding inv exposes the extended-GCD implementation body.

theorem Hex.ZMod64.inv_eq_ofNat {p : Nat} [Bounds p] (a : ZMod64 p) : a.inv = ofNat p ((match HexArith.Int.extGcd (Int.ofNat a.toNat) (Int.ofNat p) with | (fst, s, snd) => s) % Int.ofNat p).toNat

Inversion is the residue built from the extended-GCD inverse representative.

theorem Hex.ZMod64.inv_op_eq_ofNat {p : Nat} [Bounds p] (a : ZMod64 p) : a⁻¹ = ofNat p ((match HexArith.Int.extGcd (Int.ofNat a.toNat) (Int.ofNat p) with | (fst, s, snd) => s) % Int.ofNat p).toNat

Operator-level form of inv_eq_ofNat.

@[simp]

theorem Hex.ZMod64.toNat_pow {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) : (a.pow n).toNat = a.toNat ^ n % p

Exponentiation agrees with natural-power reduction of the canonical representative.

theorem Hex.ZMod64.pow_eq_ofNat {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) : a.pow n = ofNat p (a.toNat ^ n)

Exponentiation is the residue built from the representative's natural power.

theorem Hex.ZMod64.pow_op_eq_ofNat {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) : a ^ n = ofNat p (a.toNat ^ n)

Operator-level form of pow_eq_ofNat.

theorem Hex.ZMod64.inv_mul_eq_one {p : Nat} [Bounds p] (a : ZMod64 p) (hcop : a.toNat.Coprime p) : (a.inv.mul a).toNat = 1 % p

The extended-GCD inverse candidate is a left inverse whenever the representative is coprime to the modulus.

theorem Hex.ZMod64.inv_mul_eq_one_of_coprime {p : Nat} [Bounds p] (a : ZMod64 p) (hcop : a.toNat.Coprime p) : a.inv.mul a = ZMod64.one

Coprime residues multiply by their computed inverse to the unit residue.

theorem Hex.ZMod64.inv_op_mul_eq_one_of_coprime {p : Nat} [Bounds p] (a : ZMod64 p) (hcop : a.toNat.Coprime p) : a⁻¹ * a = 1

Operator-level form of inv_mul_eq_one_of_coprime.

theorem Hex.ZMod64.add_lt_modulus {p : Nat} [Bounds p] (a b : ZMod64 p) : (a.add b).toNat < p

Addition produces a canonical representative below the modulus.

theorem Hex.ZMod64.sub_lt_modulus {p : Nat} [Bounds p] (a b : ZMod64 p) : (a.sub b).toNat < p

Subtraction produces a canonical representative below the modulus.

theorem Hex.ZMod64.mul_lt_modulus {p : Nat} [Bounds p] (a b : ZMod64 p) : (a.mul b).toNat < p

Multiplication produces a canonical representative below the modulus.

theorem Hex.ZMod64.pow_lt_modulus {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) : (a.pow n).toNat < p

Exponentiation produces a canonical representative below the modulus.

theorem Hex.ZMod64.inv_lt_modulus {p : Nat} [Bounds p] (a : ZMod64 p) : a.inv.toNat < p

Inversion produces a canonical representative below the modulus.