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

A raw transform word in the redundant interval [0, 2p).

• val : UInt64
• isLt : self.val.toNat < 2 * p

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

A raw transform word in the redundant interval [0, 4p).

• val : UInt64
• isLt : self.val.toNat < 4 * p

theorem Hex.ZMod64.NttRaw2.ext {p : Nat} [Bounds p] {left right : NttRaw2 p} (h : left.val = right.val) : left = right

Raw forward words are equal when their backing words agree.

theorem Hex.ZMod64.NttRaw2.ext_iff {p : Nat} [Bounds p] {left right : NttRaw2 p} : left = right ↔ left.val = right.val

def Hex.ZMod64.NttRaw2.ofZMod {p : Nat} [Bounds p] (value : ZMod64 p) : NttRaw2 p

Enter the forward transform's redundant domain.

Equations

• Hex.ZMod64.NttRaw2.ofZMod value = { val := value.val, isLt := ⋯ }

def Hex.ZMod64.NttRaw2.normalize {p : Nat} [Bounds p] (value : NttRaw2 p) : ZMod64 p

Canonical residue represented by a raw forward word.

Equations

• value.normalize = Hex.ZMod64.ofNat p value.val.toNat

@[simp]

theorem Hex.ZMod64.NttRaw2.normalize_ofZMod {p : Nat} [Bounds p] (value : ZMod64 p) : (ofZMod value).normalize = value

Entering the forward raw domain and normalizing is the identity.

theorem Hex.ZMod64.NttRaw4.ext {p : Nat} [Bounds p] {left right : NttRaw4 p} (h : left.val = right.val) : left = right

Raw inverse words are equal when their backing words agree.

theorem Hex.ZMod64.NttRaw4.ext_iff {p : Nat} [Bounds p] {left right : NttRaw4 p} : left = right ↔ left.val = right.val

def Hex.ZMod64.NttRaw4.ofZMod {p : Nat} [Bounds p] (value : ZMod64 p) : NttRaw4 p

Enter the inverse transform's redundant domain.

Equations

• Hex.ZMod64.NttRaw4.ofZMod value = { val := value.val, isLt := ⋯ }

def Hex.ZMod64.NttRaw4.normalize {p : Nat} [Bounds p] (value : NttRaw4 p) : ZMod64 p

Canonical residue represented by a raw inverse word.

Equations

• value.normalize = Hex.ZMod64.ofNat p value.val.toNat

@[simp]

theorem Hex.ZMod64.NttRaw4.normalize_ofZMod {p : Nat} [Bounds p] (value : ZMod64 p) : (ofZMod value).normalize = value

Entering the inverse raw domain and normalizing is the identity.

def Hex.ZMod64.Ntt.shoupQuot (w t p : Nat) : Nat

Nat-level quotient in Shoup multiplication.

Equations

• Hex.ZMod64.Ntt.shoupQuot w t p = w * UInt64.word / p * t / UInt64.word

def Hex.ZMod64.Ntt.shoupValue (w t p : Nat) : Nat

Redundant Shoup product w*t - floor(floor(w*β/p)*t/β)*p.

Equations

• Hex.ZMod64.Ntt.shoupValue w t p = w * t - Hex.ZMod64.Ntt.shoupQuot w t p * p

theorem Hex.ZMod64.Ntt.shoupValue_lt {w t p : Nat} (hp : 0 < p) (hpWord : 4 * p < UInt64.word) (_hw : w < p) (ht : t < 4 * p) : shoupValue w t p < 2 * p

Shoup multiplication without its final adjustment returns a representative below 2p when the multiplicand is below 4p.

theorem Hex.ZMod64.Ntt.shoupValue_mod {w t p : Nat} : shoupValue w t p % p = w * t % p

The redundant Shoup product represents the ordinary product modulo p.

theorem Hex.ZMod64.Ntt.four_mul_lt_word (p : Nat) [Bounds p] : 4 * p < UInt64.word

The small-modulus class leaves enough word room for a fourfold redundant representative.

def Hex.ZMod64.Ntt.twiceModulusWord (p : Nat) [Bounds p] : UInt64

Twice the modulus as a faithful machine word.

Equations

• Hex.ZMod64.Ntt.twiceModulusWord p = UInt64.ofNatLT (2 * p) ⋯

@[simp]

theorem Hex.ZMod64.Ntt.twiceModulusWord_toNat (p : Nat) [Bounds p] : (twiceModulusWord p).toNat = 2 * p

Observation of the doubled modulus word.

def Hex.ZMod64.Ntt.reduceTwice (p : Nat) [Bounds p] (value : UInt64) : UInt64

Reduce a faithful representative below 4p into [0, 2p) by at most one word subtraction.

Equations

• Hex.ZMod64.Ntt.reduceTwice p value = if Hex.ZMod64.Ntt.twiceModulusWord p ≤ value then value - Hex.ZMod64.Ntt.twiceModulusWord p else value

theorem Hex.ZMod64.Ntt.reduceTwice_toNat {p : Nat} [Bounds p] (value : UInt64) (hvalue : value.toNat < 4 * p) : (reduceTwice p value).toNat = value.toNat % (2 * p)

One-subtraction reduction agrees with reduction modulo 2p.

def Hex.ZMod64.Ntt.reduceTwiceRaw2 {p : Nat} [Bounds p] (value : UInt64) (hvalue : value.toNat < 4 * p) : NttRaw2 p

Reduce a faithful representative below 4p into a bounded raw word.

Equations

• Hex.ZMod64.Ntt.reduceTwiceRaw2 value hvalue = { val := Hex.ZMod64.Ntt.reduceTwice p value, isLt := ⋯ }

@[simp]

theorem Hex.ZMod64.Ntt.reduceTwiceRaw2_toNat {p : Nat} [Bounds p] (value : UInt64) (hvalue : value.toNat < 4 * p) : (reduceTwiceRaw2 value hvalue).val.toNat = value.toNat % (2 * p)

Raw observation of one-subtraction reduction.

def Hex.ZMod64.Ntt.addTwiceSubWord (p : Nat) [Bounds p] (left right : UInt64) : UInt64

Add 2p and subtract a smaller raw representative without word wrap or borrow.

Equations

• Hex.ZMod64.Ntt.addTwiceSubWord p left right = left + Hex.ZMod64.Ntt.twiceModulusWord p - right

theorem Hex.ZMod64.Ntt.addTwiceSubWord_toNat {p : Nat} [Bounds p] (left right : UInt64) (hleft : left.toNat < 2 * p) (hright : right.toNat < 2 * p) : (addTwiceSubWord p left right).toNat = left.toNat + 2 * p - right.toNat

Observation of the faithful left + 2p - right word expression.

def Hex.ZMod64.Ntt.shoupMul {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : NttRaw2 p

Logical Shoup multiplication, returning the unadjusted representative in [0, 2p).

Equations

• Hex.ZMod64.Ntt.shoupMul twiddle value = { val := UInt64.ofNatLT (Hex.ZMod64.Ntt.shoupValue twiddle.value.toNat value.val.toNat p) ⋯, isLt := ⋯ }

@[simp]

theorem Hex.ZMod64.Ntt.toNat_shoupMul {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : (shoupMul twiddle value).val.toNat = shoupValue twiddle.value.toNat value.val.toNat p

Nat observation of logical Shoup multiplication.

def Hex.ZMod64.Ntt.shoupWord {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : UInt64

Word implementation of Shoup multiplication, using the existing verified high-word primitive.

Equations

• Hex.ZMod64.Ntt.shoupWord twiddle value = twiddle.value.val * value.val - twiddle.precon.mulHi value.val * Hex.ZMod64.modulusWord p ⋯

theorem Hex.ZMod64.Ntt.toNat_shoupWord {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : (shoupWord twiddle value).toNat = shoupValue twiddle.value.toNat value.val.toNat p

The word implementation agrees with the Nat-level Shoup formula.

def Hex.ZMod64.Ntt.shoupMulImpl {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : NttRaw2 p

Compiled Shoup multiplication.

Equations

• Hex.ZMod64.Ntt.shoupMulImpl twiddle value = { val := Hex.ZMod64.Ntt.shoupWord twiddle value, isLt := ⋯ }

@[simp]

theorem Hex.ZMod64.Ntt.toNat_shoupMulImpl {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : (shoupMulImpl twiddle value).val.toNat = shoupValue twiddle.value.toNat value.val.toNat p

Nat observation of compiled Shoup multiplication.

@[csimp]

theorem Hex.ZMod64.Ntt.shoupMul_eq_impl : @shoupMul = @shoupMulImpl

Kernel-reducible and word-level Shoup multiplication agree.

theorem Hex.ZMod64.Ntt.normalize_shoupMul {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (value : NttRaw4 p) : (shoupMul twiddle value).normalize = twiddle.value * ofNat p value.val.toNat

Shoup multiplication has the canonical product residue.

def Hex.ZMod64.Ntt.raw2OfNat {p : Nat} [Bounds p] (value : Nat) (h : value < 2 * p) : NttRaw2 p

Equations

• Hex.ZMod64.Ntt.raw2OfNat value h = { val := UInt64.ofNatLT value ⋯, isLt := ⋯ }

@[simp]

theorem Hex.ZMod64.Ntt.raw2OfNat_toNat {p : Nat} [Bounds p] (value : Nat) (h : value < 2 * p) : (raw2OfNat value h).val.toNat = value

def Hex.ZMod64.Ntt.raw4OfNat {p : Nat} [Bounds p] (value : Nat) (h : value < 4 * p) : NttRaw4 p

Equations

• Hex.ZMod64.Ntt.raw4OfNat value h = { val := UInt64.ofNatLT value ⋯, isLt := ⋯ }

@[simp]

theorem Hex.ZMod64.Ntt.raw4OfNat_toNat {p : Nat} [Bounds p] (value : Nat) (h : value < 4 * p) : (raw4OfNat value h).val.toNat = value

def Hex.ZMod64.Ntt.forwardButterfly {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : NttRaw2 p × NttRaw2 p

Harvey's forward butterfly. Inputs and outputs remain in [0, 2p); the second output uses an unadjusted Shoup product.

Equations

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

def Hex.ZMod64.Ntt.forwardButterflyImpl {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : NttRaw2 p × NttRaw2 p

Division-free word implementation of the forward butterfly.

Equations

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

@[simp]

theorem Hex.ZMod64.Ntt.toNat_forwardButterfly_fst {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : (forwardButterfly twiddle x y).fst.val.toNat = (x.val.toNat + y.val.toNat) % (2 * p)

Raw observation of the logical forward sum.

@[simp]

theorem Hex.ZMod64.Ntt.toNat_forwardButterfly_snd {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : (forwardButterfly twiddle x y).snd.val.toNat = shoupValue twiddle.value.toNat (x.val.toNat + 2 * p - y.val.toNat) p

Raw observation of the logical forward twiddled difference.

@[simp]

theorem Hex.ZMod64.Ntt.toNat_forwardButterflyImpl_fst {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : (forwardButterflyImpl twiddle x y).fst.val.toNat = (x.val.toNat + y.val.toNat) % (2 * p)

Raw observation of the compiled forward sum.

@[simp]

theorem Hex.ZMod64.Ntt.toNat_forwardButterflyImpl_snd {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : (forwardButterflyImpl twiddle x y).snd.val.toNat = shoupValue twiddle.value.toNat (x.val.toNat + 2 * p - y.val.toNat) p

Raw observation of the compiled forward twiddled difference.

@[csimp]

theorem Hex.ZMod64.Ntt.forwardButterfly_eq_impl : @forwardButterfly = @forwardButterflyImpl

The forward butterfly's kernel-reducible and division-free word implementations agree.

theorem Hex.ZMod64.Ntt.normalize_forward_fst {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : (forwardButterfly twiddle x y).fst.normalize = x.normalize + y.normalize

The first forward output is the sum residue.

theorem Hex.ZMod64.Ntt.normalize_forward_snd {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw2 p) : (forwardButterfly twiddle x y).snd.normalize = twiddle.value * (x.normalize - y.normalize)

The second forward output is the twiddled difference residue.

def Hex.ZMod64.Ntt.inverseButterfly {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : NttRaw4 p × NttRaw4 p

Harvey's inverse butterfly. Inputs and outputs remain in [0, 4p); only the left input is reduced to [0, 2p) before the add/subtract pair.

Equations

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

def Hex.ZMod64.Ntt.inverseButterflyImpl {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : NttRaw4 p × NttRaw4 p

Division-free word implementation of the inverse butterfly.

Equations

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

@[simp]

theorem Hex.ZMod64.Ntt.toNat_inverseButterfly_fst {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : (inverseButterfly twiddle x y).fst.val.toNat = x.val.toNat % (2 * p) + shoupValue twiddle.value.toNat y.val.toNat p

Raw observation of the logical inverse sum.

@[simp]

theorem Hex.ZMod64.Ntt.toNat_inverseButterfly_snd {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : (inverseButterfly twiddle x y).snd.val.toNat = x.val.toNat % (2 * p) + 2 * p - shoupValue twiddle.value.toNat y.val.toNat p

Raw observation of the logical inverse difference.

@[simp]

theorem Hex.ZMod64.Ntt.toNat_inverseButterflyImpl_fst {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : (inverseButterflyImpl twiddle x y).fst.val.toNat = x.val.toNat % (2 * p) + shoupValue twiddle.value.toNat y.val.toNat p

Raw observation of the compiled inverse sum.

@[simp]

theorem Hex.ZMod64.Ntt.toNat_inverseButterflyImpl_snd {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : (inverseButterflyImpl twiddle x y).snd.val.toNat = x.val.toNat % (2 * p) + 2 * p - shoupValue twiddle.value.toNat y.val.toNat p

Raw observation of the compiled inverse difference.

@[csimp]

theorem Hex.ZMod64.Ntt.inverseButterfly_eq_impl : @inverseButterfly = @inverseButterflyImpl

The inverse butterfly's kernel-reducible and division-free word implementations agree.

theorem Hex.ZMod64.Ntt.normalize_inverse_fst {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : (inverseButterfly twiddle x y).fst.normalize = x.normalize + twiddle.value * y.normalize

The first inverse output is the sum with the twiddled right input.

theorem Hex.ZMod64.Ntt.normalize_inverse_snd {p : Nat} [Bounds p] (twiddle : NttTwiddle p) (x y : NttRaw4 p) : (inverseButterfly twiddle x y).snd.normalize = x.normalize - twiddle.value * y.normalize

The second inverse output is the corresponding difference.