Correctness of GF(2) circular convolution via NTT

theorem circular_convolution_gf2_correct {n : ℕ} (a b : BitVec n) (hn : n < 2 ^ 29) : circularConvolutionGf2 a b = a.circConvolutionBruteforce b