8.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 fits in one machine word.

Instance Constructor

Hex.ZMod64.Bounds.mk

Methods

pPos : 0 < p

The modulus is positive.

pLeR : p ≤ UInt64.word

The modulus fits in one machine word.

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.