Documentation

UniversalHashing.BinConvolution.ConvolutionHelpers.OuterLoopHelpersPreproc

Bit-reversal and preprocessing invariant #

Bit-reversal permutation lemmas and preprocessing_establishes_inv, split out from OuterLoopHelpersForward to keep per-file elaboration memory bounded.

Bit-reversal helper lemmas #

source
@[simp]
theorem bitRev_zero (n : ℕ) :
bitRev n 0 = 0
source
theorem bitRev_msb (n b c : ℕ) (hb : b ≤ 1) (hc : c < 2 ^ n) :
bitRev (n + 1) (2 ^ n * b + c) = 2 * bitRev n c + b

bitRev (n+1) (2^n*b + c) = 2 * bitRev n c + b when b ≤ 1 and c < 2^n.

source
theorem bitRev_invol (n x : ℕ) (hx : x < 2 ^ n) :
bitRev n (bitRev n x) = x

Bit reversal is an involution on [0, 2^n).

source
theorem and_two_pow_decompose (n b c : ℕ) (hb : b ≤ 1) (hc : c < 2 ^ n) :
2 ^ n * b + c &&& 2 ^ n = 2 ^ n * b

(2^n * b + c) AND 2^n = 2^n * b for b ≤ 1 and c < 2^n.

source
theorem xor_two_pow_decompose (n b c : ℕ) (hb : b ≤ 1) (hc : c < 2 ^ n) :
2 ^ n * b + c ^^^ 2 ^ n = 2 ^ n * (1 - b) + c

(2^n * b + c) XOR 2^n = 2^n * (1 - b) + c for b ≤ 1 and c < 2^n.

source
theorem bitRevNext_spec (n i : ℕ) (hn1 : 1 ≤ n) (hn64 : n ≤ 64) (hi : i + 1 < 2 ^ n) (f : ℕ) (hf : n - 1 ≤ f) (j bit : ℕ) (hj : j = bitRev n i) (hbit : bit = 2 ^ (n - 1)) :
bitRevNext f j bit = bitRev n (i + 1)

bitRevNext f j bit correctly increments the bit-reversed counter j of width n, provided fuel f ≥ n - 1.

source
def bitRevLoop_inv_pred (n step : ℕ) (v0 a : Vector UInt32 (2 ^ n)) :
Prop

The invariant maintained by bitRevLoop: after step iterations starting from the identity (with the i counter at step and the bit-reversed counter at bitRev n step), position p holds either v0[bitRev n p] (when p or its mirror has been processed) or v0[p] (when neither has been processed).

Equations
Instances For
    source
    theorem bitRevLoop_spec {N : ℕ} (hN64 : N < 64) (v : Vector UInt32 (2 ^ N)) (p : ℕ) (hp : p < 2 ^ N) :
    (bitRevLoop (2 ^ N - 1) 0 v 0)[p] = v[bitRev N p]

    The main correctness theorem for bitRevLoop: starting from the identity, after running 2^N - 1 steps, position p holds v[bitRev N p].

    source
    theorem bitRevLoop_spec_m {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (hn64 : n < 64) (v : Vector UInt32 m) (p : ℕ) (hp : p < m) (hbr_lt : bitRev n p < m) :
    (bitRevLoop (m - 1) 0 v 0)[p] = v[bitRev n p]

    Helper: convert bitRevLoop spec from Vector UInt32 (2^n) to Vector UInt32 m.

    source
    theorem preprocessing_establishes_inv {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (h_dvd : m ∣ mod64.toNat - 1) (v : Vector UInt32 m) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (roots : Vector UInt32 m) (_hroots : ntt_roots_correct m roots) :
    have a1 := bitRevLoop (m - 1) 0 (Vector.map toMont v) 0; have parity := nttInplace.go 64 m 0 &&& 1 != 0; have a_in := if parity = true then radix2Pass (m / 2) 0 a1 else a1; have start_q := if parity = true then 1 else 0; ∃ (hle : start_q ≤ n), outerLoop_inv n start_q hle hm_eq v a_in