Toeplitz hashing via NTT-based binary circular convolution

Computing the Toeplitz hash toeplitzHash by school-book matrix-vector multiplication takes time quadratic in the block size. The Toeplitz structure allows an O(N log N) algorithm ( see, e.g., [HT16] Appendix B.).

• embed the m × n Toeplitz matrix T into a circulant matrix C_T of size L × L with L = m + n - 1, zero-pad the input vector to length L,
• compute the circulant-vector product as a circular convolution via the NTT (circularConvolutionGf2).
• the first m entries of the result are T x; discard the rest.

A circulant matrix is determined by its first column c_C; its product with a vector is the circular convolution of c_C with that vector. Writing the Toeplitz matrix's first column as c_T and its first row (excluding the corner) as r_T, the embedding is c_C = c_T ++ reverse r_T.

In the parameter layout of ToeplitzMatrix.from_params (where T i j = param (i + (n-1) - j)) we have c_T i = param (n-1+i) and r_T j = param (n-2-j), so the reversal cancels and

c_C i = if i < m then param (n-1+i) else param (i-m).

Main definitions:

• toeplitzCirculantColumn: first column of the circulant embedding, from the seed.
• toeplitzHashNTT: the Toeplitz hash family computed via circularConvolutionGf2, with seeds/inputs/outputs represented as BitVecs. This is the definition to state theorems about; thanks to a @[csimp] replacement, compiled calls to it run the fast implementation toeplitzHashNTTFast.
• toeplitzHashNTTFast: the same computation with O(N log N) divide-and-conquer BitVec bit extraction/assembly instead of quadratic per-bit big-integer accesses.

Main results:

• toeplitzHashNTT_eq_toeplitzHash: on the domain where the NTT convolution is proven correct (m + n - 1 < 2 ^ 29), toeplitzHashNTT computes exactly toeplitzHash under the evident BitVec ↔ Fin _ → ZMod 2 correspondence (BitVec.toZMod2Fun).
• toeplitzHashNTTFast_eq: the fast implementation equals toeplitzHashNTT, unconditionally, as functions.
• toeplitzHashNTT_eq_fast (@[csimp]): the bare-constant form of that equality, which instructs the compiler to run toeplitzHashNTTFast wherever compiled code calls toeplitzHashNTT — kernel-checked, unlike @[implemented_by].

Tests/ToeplitzNTT.lean additionally checks toeplitzHashNTT (running the fast implementation via the @[csimp] replacement) against the school-book toeplitzHash for small matrices.

def toeplitzCirculantColumn (m n : ℕ) (param : BitVec (m + n - 1)) : BitVec (m + n - 1)

First column of the circulant matrix that the Toeplitz matrix with parameter vector param (in the layout of ToeplitzMatrix.from_params) embeds into: the Toeplitz matrix's first column followed by its reversed first row (sans corner).

Equations

• toeplitzCirculantColumn m n param = BitVec.ofFnLE fun (i : Fin (m + n - 1)) => if h : ↑i < m then param.getLsb ⟨n - 1 + ↑i, ⋯⟩ else param.getLsb ⟨↑i - m, ⋯⟩

def toeplitzHashNTT (m n : ℕ) : HashFamily (BitVec (m + n - 1)) (BitVec n) (BitVec m)

The Toeplitz hash family, computed via the NTT-based binary circular convolution circularConvolutionGf2: embed the seed's Toeplitz matrix into a circulant matrix (toeplitzCirculantColumn), zero-pad the input to length m + n - 1, convolve, and keep the low m bits.

Bit k of the seed corresponds to param k in toeplitzHash; bits of input/output correspond to vector entries, 1 : ZMod 2 ↔ true.

This is the reference definition, written for auditability and proofs. As written it has quadratic BitVec boundary cost, but compiled code never pays it: a @[csimp] replacement (toeplitzHashNTT_eq_fast) makes compiled calls run the equivalent O(N log N) implementation toeplitzHashNTTFast.

Equations

• toeplitzHashNTT m n param x = BitVec.setWidth m (circularConvolutionGf2 (toeplitzCirculantColumn m n param) (BitVec.setWidth (m + n - 1) x))

Correctness

def BitVec.toZMod2Fun {w : ℕ} (v : BitVec w) : Fin w → ZMod 2

Decode a bit vector into a ZMod 2 vector (LSB-first, true ↦ 1).

Equations

• v.toZMod2Fun k = if v.getLsb k = true then 1 else 0

def boolToZMod2 : Bool →+* ZMod 2

The ring homomorphism from Bool (with xor as + and and as *) to ZMod 2.

Equations

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

theorem toeplitzHashNTT_eq_toeplitzHash (m n : ℕ) [NeZero m] [NeZero n] (hL : m + n - 1 < 2 ^ 29) (param : BitVec (m + n - 1)) (x : BitVec n) : (toeplitzHashNTT m n param x).toZMod2Fun = toeplitzHash m n param.toZMod2Fun x.toZMod2Fun

Correctness of NTT-based Toeplitz hashing. On the domain where the NTT convolution is proven correct (m + n - 1 < 2 ^ 29), toeplitzHashNTT computes exactly the school-book Toeplitz hash toeplitzHash, under the correspondence BitVec.toZMod2Fun between bit vectors and ZMod 2 vectors.

Fast implementation

toeplitzHashNTT is algorithmically O(N log N), but its BitVec boundary work is quadratic: every per-bit getLsb/ofFnLE access shifts the whole underlying big integer. toeplitzHashNTTFast performs the same computation with divide-and-conquer bit extraction and assembly (O(N log N) overall) and is proven equal as a function to toeplitzHashNTT (toeplitzHashNTTFast_eq), so toeplitzHashNTT_eq_toeplitzHash applies to it verbatim (toeplitzHashNTTFast_eq_toeplitzHash).

The @[csimp] theorem toeplitzHashNTT_eq_fast then closes the loop: compiled code that calls toeplitzHashNTT actually runs toeplitzHashNTTFast, so there is no slow path at runtime and no reason to call the fast implementation by name.

@[irreducible]

def BitVec.toBoolVector {w : ℕ} (v : BitVec w) : Vector Bool w

Divide-and-conquer extraction of all bits of a BitVec (LSB first) in O(w log w): each level splits the vector with one whole-vector shift instead of shifting per bit.

Equations

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

theorem BitVec.toBoolVector_getElem {w : ℕ} (v : BitVec w) (i : ℕ) (hi : i < w) : v.toBoolVector[i] = v.getLsbD i

@[irreducible]

def BitVec.ofBoolFnLE (w : ℕ) : (Fin w → Bool) → BitVec w

Divide-and-conquer assembly of a BitVec from a bit function (LSB first) in O(w log w): each level concatenates two halves with one whole-vector shift instead of inserting bits one at a time (as BitVec.ofFnLE's Nat.ofBits does).

Equations

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

theorem BitVec.ofBoolFnLE_eq_ofFnLE (w : ℕ) (f : Fin w → Bool) : ofBoolFnLE w f = ofFnLE f

def toeplitzHashNTTFast (m n : ℕ) : HashFamily (BitVec (m + n - 1)) (BitVec n) (BitVec m)

Fast implementation of toeplitzHashNTT: the same circulant-embedding NTT convolution pipeline, but with divide-and-conquer BitVec bit extraction/assembly instead of per-bit big-integer accesses. Proven equal to toeplitzHashNTT in toeplitzHashNTTFast_eq.

Equations

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

theorem BitVec.toBoolVector_get_eq_getLsb {w : ℕ} (v : BitVec w) (i : Fin w) : v.toBoolVector.get i = v.getLsb i

The divide-and-conquer bit extraction agrees with getLsb.

theorem toeplitzHashNTTFast_eq (m n : ℕ) : toeplitzHashNTTFast m n = toeplitzHashNTT m n

The fast implementation is the reference implementation — unconditionally, as an equality of functions. Together with toeplitzHashNTT_eq_toeplitzHash this transfers all correctness statements to toeplitzHashNTTFast.

@[csimp]

theorem toeplitzHashNTT_eq_fast : toeplitzHashNTT = toeplitzHashNTTFast

Compiler replacement (@[csimp]): compiled code that calls toeplitzHashNTT runs toeplitzHashNTTFast instead. This is justified by the kernel-checked equality toeplitzHashNTTFast_eq — proofs continue to see the reference definition, while execution is O(N log N).

theorem toeplitzHashNTTFast_eq_toeplitzHash (m n : ℕ) [NeZero m] [NeZero n] (hL : m + n - 1 < 2 ^ 29) (param : BitVec (m + n - 1)) (x : BitVec n) : (toeplitzHashNTTFast m n param x).toZMod2Fun = toeplitzHash m n param.toZMod2Fun x.toZMod2Fun

Correctness of the fast NTT-based Toeplitz hash, transferred from toeplitzHashNTT_eq_toeplitzHash via toeplitzHashNTTFast_eq.