def Hex.ZMod64.IsPowTwo (n : Nat) : Prop

Executable characterization of a nonzero power of two.

Equations

• Hex.ZMod64.IsPowTwo n = (n ≠ 0 ∧ n = 2 ^ n.log2)

@[instance_reducible]

instance Hex.ZMod64.instDecidableIsPowTwo (n : Nat) : Decidable (IsPowTwo n)

Equations

• Hex.ZMod64.instDecidableIsPowTwo n = Hex.ZMod64.instDecidableIsPowTwo._aux_1 n

def Hex.ZMod64.ExactOrder {p : Nat} [Bounds p] (root : ZMod64 p) (n : Nat) : Prop

Exact-order certificate specialized to a power-of-two order. For a power-of-two n, an nth root has exact order n precisely when it is not already an (n / 2)th root (with the order-one case separated).

Equations

• root.ExactOrder n = (root ^ n = 1 ∧ (n = 1 ∨ root ^ (n / 2) ≠ 1))

@[instance_reducible]

instance Hex.ZMod64.instDecidableExactOrder {p : Nat} [Bounds p] (root : ZMod64 p) (n : Nat) : Decidable (root.ExactOrder n)

Equations

• root.instDecidableExactOrder n = Hex.ZMod64.instDecidableExactOrder._aux_1 root n

theorem Hex.ZMod64.ExactOrder.pow_eq_one {p n : Nat} [Bounds p] {root : ZMod64 p} (h : root.ExactOrder n) : root ^ n = 1

An exact-order certificate includes the root-of-unity equation.

theorem Hex.ZMod64.ExactOrder.half {p n : Nat} [Bounds p] {root : ZMod64 p} (h : root.ExactOrder n) : n = 1 ∨ root ^ (n / 2) ≠ 1

The nontrivial half-order clause of a power-of-two exact-order certificate.

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

A transform twiddle and the quotient preconditioner floor(value * 2^64 / p) used by Shoup multiplication.

• value : ZMod64 p

  Canonical twiddle value.

• precon : UInt64

  Shoup quotient preconditioner.

• precon_eq : self.precon.toNat = self.value.toNat * UInt64.word / p

  The preconditioner stores the exact one-word quotient.

def Hex.ZMod64.NttTwiddle.ofValue {p : Nat} [Bounds p] (value : ZMod64 p) : NttTwiddle p

Build a twiddle and its Shoup preconditioner.

Equations

• Hex.ZMod64.NttTwiddle.ofValue value = { value := value, precon := UInt64.ofNat (value.toNat * UInt64.word / p), precon_eq := ⋯ }

@[simp]

theorem Hex.ZMod64.NttTwiddle.precon_toNat {p : Nat} [Bounds p] (value : ZMod64 p) : (ofValue value).precon.toNat = value.toNat * UInt64.word / p

The Shoup quotient fits in one word and is stored without wraparound.

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

A reusable radix-two NTT plan.

• length_pow_two : ∃ (k : Nat), n = 2 ^ k

  The requested transform length is a power of two.

• length_dvd : n ∣ p - 1

  The transform length divides the order of the prime field's unit group.

• root : ZMod64 p

  Primitive transform root.

• root_order : self.root.ExactOrder n

  The root has exact power-of-two order n.

• invRoot : ZMod64 p

  Inverse transform root.

• invRoot_eq : self.invRoot = self.root⁻¹

  The stored inverse root is the multiplicative inverse of root.

• invLength : ZMod64 p

  Inverse of the transform length modulo p.

• invLength_eq : self.invLength = (↑n)⁻¹

  The stored length inverse is the inverse of the natural cast of n.

• forwardTwiddles : Array (NttTwiddle p)

  Reusable forward root powers and Shoup preconditioners.

• forward_size : self.forwardTwiddles.size = n

  There is one forward power for every exponent below n.

• forward_value (i : Nat) (hi : i < n) : self.forwardTwiddles[i].value = self.root ^ i

  Every stored forward twiddle is the corresponding root power.

• inverseTwiddles : Array (NttTwiddle p)

  Reusable inverse-root powers and Shoup preconditioners.

• inverse_size : self.inverseTwiddles.size = n

  There is one inverse power for every exponent below n.

• inverse_value (i : Nat) (hi : i < n) : self.inverseTwiddles[i].value = self.invRoot ^ i

  Every stored inverse twiddle is the corresponding inverse-root power.

def Hex.ZMod64.NttPlan.Valid {p : Nat} [Bounds p] (n : Nat) (root : ZMod64 p) : Prop

Everything checked by NTT plan construction.

Equations

• Hex.ZMod64.NttPlan.Valid n root = (Hex.ZMod64.IsPowTwo n ∧ n ∣ p - 1 ∧ root.ExactOrder n)

@[instance_reducible]

instance Hex.ZMod64.NttPlan.instDecidableValid {p n : Nat} [Bounds p] (root : ZMod64 p) : Decidable (Valid n root)

Equations

• Hex.ZMod64.NttPlan.instDecidableValid root = Hex.ZMod64.NttPlan.instDecidableValid._aux_1 root

def Hex.ZMod64.NttPlan.twiddles {p : Nat} [Bounds p] (root : ZMod64 p) (n : Nat) : Array (NttTwiddle p)

Table of the first n powers of a root, with Shoup preconditioners.

Equations

• Hex.ZMod64.NttPlan.twiddles root n = Array.ofFn fun (i : Fin n) => Hex.ZMod64.NttTwiddle.ofValue (root ^ ↑i)

@[simp]

theorem Hex.ZMod64.NttPlan.twiddles_size {p : Nat} [Bounds p] (root : ZMod64 p) (n : Nat) : (twiddles root n).size = n

The twiddle table has the requested length.

@[simp]

theorem Hex.ZMod64.NttPlan.twiddles_value {p : Nat} [Bounds p] (root : ZMod64 p) (n i : Nat) (hi : i < n) : (twiddles root n)[i].value = root ^ i

Looking up a twiddle exposes the corresponding root power.

def Hex.ZMod64.NttPlan.build? {p n : Nat} [Bounds p] [PrimeModulus p] (root : ZMod64 p) : Option (NttPlan p n)

Validate a requested root and build all reusable transform data.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.ZMod64.NttPlan.build?_isSome {p n : Nat} [Bounds p] [PrimeModulus p] (root : ZMod64 p) : (build? root).isSome = decide (Valid n root)

Plan construction succeeds exactly when the requested length and root pass all validation checks.

theorem Hex.ZMod64.NttPlan.build?_root {p n : Nat} [Bounds p] [PrimeModulus p] {root : ZMod64 p} {plan : NttPlan p n} (h : build? root = some plan) : plan.root = root

A successful plan records the supplied root.

theorem Hex.ZMod64.NttPlan.invRoot_mul_root {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (hroot : plan.root ≠ 0) : plan.invRoot * plan.root = 1

A successful plan exposes the validated inverse root.