The canonical prime word

An element x : ZMod p of a prime field with p ≤ 2 ^ 64 is carried on one 64-bit word as its canonical representative BitVec.ofNat 64 x.val. This module fixes that encoding, primeWord p, and its decoder primeDec p w = (w.toNat : ZMod p), which is the relation of the single-limb retraction Transfer.Param.limbFieldParam: the encoding is the section of that retraction (primeWord_eq_section), and a word is related to a field element exactly when it decodes to it (limbFieldParam_R_iff).

The operation squares are registered along both maps.

• Along the encoding primeWord p (field to word) the squares are total: the reference word operations addModW, subModW, mulModW, negModW realize +, -, * and negation, and word equality and word order agree with equality and with the order of ZMod.val.
• Along the decoder primeDec p (word to field) the wrapping word operations realize the field operations under a no-overflow guard (+, *) or an order guard (-), and the reduction modW p realizes the identity. Word equality agrees with field equality on canonical words.

The instances take the bound p ≤ 2 ^ 64 as a Fact, as Transfer.Param.instTransferDomLimbField does.

Main definitions

• primeWord p, primeDec p: the canonical encoding and its decoder.
• addModW p, subModW p, mulModW p, negModW p, modW p: the reference word operations modulo p.

Main results

• primeWord_toNat, primeWord_injective, eq_primeWord_of_toNat, primeDec_primeWord, primeWord_primeDec, primeWord_natCast: the encoding API.
• addRelated, subRelated, mulRelated, negRelated, eqRelated, valLtRelated: the total squares along primeWord p.
• decAddRelatedOn, decMulRelatedOn, decSubRelatedOn, decModRelated, decEqRelatedOn: the squares along primeDec p.

def Transfer.PrimeWord.primeWord (p : ℕ) (x : ZMod p) : BitVec 64

The canonical prime word: a field element as the 64-bit word of its canonical representative.

Equations

• Transfer.PrimeWord.primeWord p x = BitVec.ofNat 64 x.val

def Transfer.PrimeWord.primeDec (p : ℕ) (w : BitVec 64) : ZMod p

The decoder of the canonical prime word: a 64-bit word read modulo p.

Equations

• Transfer.PrimeWord.primeDec p w = ↑w.toNat

def Transfer.PrimeWord.addModW (p : ℕ) (a b : BitVec 64) : BitVec 64

The word sum reduced modulo p.

Equations

• Transfer.PrimeWord.addModW p a b = BitVec.ofNat 64 ((a.toNat + b.toNat) % p)

def Transfer.PrimeWord.subModW (p : ℕ) (a b : BitVec 64) : BitVec 64

The word difference modulo p, computed as a + (p - b) reduced modulo p.

Equations

• Transfer.PrimeWord.subModW p a b = BitVec.ofNat 64 ((a.toNat + (p - b.toNat)) % p)

def Transfer.PrimeWord.mulModW (p : ℕ) (a b : BitVec 64) : BitVec 64

The word product reduced modulo p.

Equations

• Transfer.PrimeWord.mulModW p a b = BitVec.ofNat 64 (a.toNat * b.toNat % p)

def Transfer.PrimeWord.negModW (p : ℕ) (a : BitVec 64) : BitVec 64

The word negation modulo p, computed as p - a reduced modulo p.

Equations

• Transfer.PrimeWord.negModW p a = BitVec.ofNat 64 ((p - a.toNat) % p)

def Transfer.PrimeWord.modW (p : ℕ) (a : BitVec 64) : BitVec 64

The reduction of a word modulo p.

Equations

• Transfer.PrimeWord.modW p a = BitVec.ofNat 64 (a.toNat % p)

The encoding and the retraction

theorem Transfer.PrimeWord.primeWord_eq_section {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (x : ZMod p) : primeWord p x = (Param.limbFieldParam p hp).bwd.map x

The canonical prime word is the section of the retraction limbFieldParam.

theorem Transfer.PrimeWord.limbFieldParam_R_iff {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (w : BitVec 64) (x : ZMod p) : (Param.limbFieldParam p hp).R w x ↔ primeDec p w = x

A word is related to a field element by limbFieldParam exactly when it decodes to it.

theorem Transfer.PrimeWord.primeWord_toNat {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (x : ZMod p) : (primeWord p x).toNat = x.val

The value of the canonical prime word is the canonical representative.

theorem Transfer.PrimeWord.primeWord_toNat_lt {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (x : ZMod p) : (primeWord p x).toNat < p

The value of the canonical prime word is below p.

theorem Transfer.PrimeWord.primeWord_lt {p : ℕ} [NeZero p] (hp : p < 2 ^ 64) (x : ZMod p) : primeWord p x < BitVec.ofNat 64 p

The canonical prime word lies below the word of p.

theorem Transfer.PrimeWord.primeWord_injective {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) : Function.Injective (primeWord p)

The canonical prime word is injective.

theorem Transfer.PrimeWord.eq_primeWord_of_toNat {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (w : BitVec 64) (z : ZMod p) (h : w.toNat = z.val) : w = primeWord p z

A word whose value is z.val is the canonical prime word of z.

theorem Transfer.PrimeWord.primeWord_natCast {p : ℕ} [NeZero p] (n : ℕ) (h : n < p) : primeWord p ↑n = BitVec.ofNat 64 n

The canonical prime word of the cast of n < p is the word of n.

theorem Transfer.PrimeWord.primeDec_primeWord {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (x : ZMod p) : primeDec p (primeWord p x) = x

Decoding the canonical prime word returns the field element.

theorem Transfer.PrimeWord.primeWord_primeDec {p : ℕ} [NeZero p] (w : BitVec 64) : primeWord p (primeDec p w) = modW p w

The canonical prime word of a decoded word is its reduction modulo p.

theorem Transfer.PrimeWord.primeWord_primeDec_of_lt {p : ℕ} [NeZero p] (w : BitVec 64) (h : w.toNat < p) : primeWord p (primeDec p w) = w

A word below p is the canonical prime word of its decoding.

theorem Transfer.PrimeWord.limbFieldParam_R_primeWord {p : ℕ} [NeZero p] (hp : p ≤ 2 ^ 64) (x : ZMod p) : (Param.limbFieldParam p hp).R (primeWord p x) x

The canonical prime word is related to its field element by limbFieldParam.

Total squares along the encoding

instance Transfer.PrimeWord.addRelated {p : ℕ} [NeZero p] [hp : Fact (p ≤ 2 ^ 64)] : RelatedBinOp (primeWord p) (fun (x1 x2 : ZMod p) => x1 + x2) (addModW p)

addModW p realizes + along primeWord p.

instance Transfer.PrimeWord.subRelated {p : ℕ} [NeZero p] [hp : Fact (p ≤ 2 ^ 64)] : RelatedBinOp (primeWord p) (fun (x1 x2 : ZMod p) => x1 - x2) (subModW p)

subModW p realizes - along primeWord p.

instance Transfer.PrimeWord.mulRelated {p : ℕ} [NeZero p] [hp : Fact (p ≤ 2 ^ 64)] : RelatedBinOp (primeWord p) (fun (x1 x2 : ZMod p) => x1 * x2) (mulModW p)

mulModW p realizes * along primeWord p.

instance Transfer.PrimeWord.negRelated {p : ℕ} [NeZero p] [hp : Fact (p ≤ 2 ^ 64)] : RelatedUnOp (primeWord p) (fun (x : ZMod p) => -x) (negModW p)

negModW p realizes negation along primeWord p.

instance Transfer.PrimeWord.eqRelated {p : ℕ} [NeZero p] [hp : Fact (p ≤ 2 ^ 64)] : RelatedRelOn (primeWord p) (fun (x x_1 : ZMod p) => True) (fun (x1 x2 : ZMod p) => x1 = x2) fun (x1 x2 : BitVec 64) => x1 = x2

Word equality agrees with field equality along primeWord p.

instance Transfer.PrimeWord.valLtRelated {p : ℕ} [NeZero p] [hp : Fact (p ≤ 2 ^ 64)] : RelatedRelOn (primeWord p) (fun (x x_1 : ZMod p) => True) (fun (x y : ZMod p) => x.val < y.val) fun (x1 x2 : BitVec 64) => x1 < x2

The word order agrees with the order of canonical representatives along primeWord p.

Guarded squares along the decoder

instance Transfer.PrimeWord.decAddRelatedOn {p : ℕ} : RelatedBinOpOn (primeDec p) (fun (a b : BitVec 64) => a.toNat + b.toNat < 2 ^ 64) (fun (x1 x2 : BitVec 64) => x1 + x2) fun (x1 x2 : ZMod p) => x1 + x2

The wrapping word sum realizes + along primeDec p when the sum does not overflow.

instance Transfer.PrimeWord.decMulRelatedOn {p : ℕ} : RelatedBinOpOn (primeDec p) (fun (a b : BitVec 64) => a.toNat * b.toNat < 2 ^ 64) (fun (x1 x2 : BitVec 64) => x1 * x2) fun (x1 x2 : ZMod p) => x1 * x2

The wrapping word product realizes * along primeDec p when the product does not overflow.

instance Transfer.PrimeWord.decSubRelatedOn {p : ℕ} : RelatedBinOpOn (primeDec p) (fun (a b : BitVec 64) => b.toNat ≤ a.toNat) (fun (x1 x2 : BitVec 64) => x1 - x2) fun (x1 x2 : ZMod p) => x1 - x2

The wrapping word difference realizes - along primeDec p when the subtrahend is at most the minuend.

instance Transfer.PrimeWord.decModRelated {p : ℕ} : RelatedUnOp (primeDec p) (modW p) id

The reduction modW p realizes the identity along primeDec p.

instance Transfer.PrimeWord.decEqRelatedOn {p : ℕ} [NeZero p] : RelatedRelOn (primeDec p) (fun (a b : BitVec 64) => a.toNat < p ∧ b.toNat < p) (fun (x1 x2 : BitVec 64) => x1 = x2) fun (x1 x2 : ZMod p) => x1 = x2

Field equality agrees with word equality along primeDec p on words below p.

Descent through the squares

theorem Transfer.PrimeWord.primeDec_mul_add {p : ℕ} (a b c : BitVec 64) (h1 : a.toNat * b.toNat < 2 ^ 64) (h2 : (a * b).toNat + c.toNat < 2 ^ 64) : primeDec p (a * b + c) = primeDec p a * primeDec p b + primeDec p c

The decoded field expression x * y + z is the decoding of the wrapping word expression, under the no-overflow guards param_guard returns.

theorem Transfer.PrimeWord.primeWord_mul_add {p : ℕ} [NeZero p] [Fact (p ≤ 2 ^ 64)] (x y z : ZMod p) : Related (primeWord p) (x * y + z) (addModW p (mulModW p (primeWord p x) (primeWord p y)) (primeWord p z))

A field expression over encoded operands, closed by param_solve along primeWord p.