Documentation

CompPoly.Fields.Binary.AdditiveNTT.Correctness

Additive NTT Correctness #

The stage-wise correctness argument and the final correctness theorem for the Additive NTT.

source
theorem AdditiveNTT.initial_tiled_coeffs_correctness {r : β„•} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (Ξ² : Fin r β†’ L) [hΞ²_lin_indep : Fact (LinearIndependent 𝔽q Ξ²)] [h_Ξ²β‚€_eq_1 : Fact (Ξ² 0 = 1)] {β„“ R_rate : β„•} (h_β„“_add_R_rate : β„“ + R_rate < r) (h_β„“ : β„“ ≀ r) (a : Fin (2 ^ β„“) β†’ L) :
have b := tileCoeffs a; additiveNTTInvariant 𝔽q Ξ² h_β„“_add_R_rate b a βŸ¨β„“, β‹―βŸ©
source
theorem AdditiveNTT.NTTStage_correctness {r : β„•} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (Ξ² : Fin r β†’ L) [hΞ²_lin_indep : Fact (LinearIndependent 𝔽q Ξ²)] {β„“ R_rate : β„•} (h_β„“_add_R_rate : β„“ + R_rate < r) (i : Fin β„“) (input_buffer : Fin (2 ^ (β„“ + R_rate)) β†’ L) (original_coeffs : Fin (2 ^ β„“) β†’ L) :
additiveNTTInvariant 𝔽q Ξ² h_β„“_add_R_rate input_buffer original_coeffs βŸ¨β†‘i + 1, β‹―βŸ© β†’ additiveNTTInvariant 𝔽q Ξ² h_β„“_add_R_rate (NTTStage 𝔽q Ξ² h_β„“_add_R_rate βŸ¨β†‘i, β‹―βŸ© input_buffer) original_coeffs βŸ¨β†‘i, β‹―βŸ©
source
theorem AdditiveNTT.foldl_NTTStage_inductive_aux {r : β„•} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (Ξ² : Fin r β†’ L) [hΞ²_lin_indep : Fact (LinearIndependent 𝔽q Ξ²)] [h_Ξ²β‚€_eq_1 : Fact (Ξ² 0 = 1)] {β„“ R_rate : β„•} (h_β„“_add_R_rate : β„“ + R_rate < r) (h_β„“ : β„“ ≀ r) (k : Fin (β„“ + 1)) (original_coeffs : Fin (2 ^ β„“) β†’ L) :
additiveNTTInvariant 𝔽q Ξ² h_β„“_add_R_rate (Fin.foldl (↑k) (fun (current_b : Fin (2 ^ (β„“ + R_rate)) β†’ L) (i : Fin ↑k) => NTTStage 𝔽q Ξ² h_β„“_add_R_rate βŸ¨β„“ - ↑i - 1, β‹―βŸ© current_b) (tileCoeffs original_coeffs)) original_coeffs βŸ¨β„“ - ↑k, β‹―βŸ©
source
theorem AdditiveNTT.additiveNTT_correctness {r : β„•} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (Ξ² : Fin r β†’ L) [hΞ²_lin_indep : Fact (LinearIndependent 𝔽q Ξ²)] [h_Ξ²β‚€_eq_1 : Fact (Ξ² 0 = 1)] {β„“ R_rate : β„•} (h_β„“_add_R_rate : β„“ + R_rate < r) (h_β„“ : β„“ ≀ r) (original_coeffs : Fin (2 ^ β„“) β†’ L) (output_buffer : Fin (2 ^ (β„“ + R_rate)) β†’ L) (h_alg : output_buffer = additiveNTT 𝔽q Ξ² h_β„“_add_R_rate original_coeffs) :
have P := polynomialFromNovelCoeffs 𝔽q Ξ² β„“ h_β„“ original_coeffs; βˆ€ (j : Fin (2 ^ (β„“ + R_rate))), output_buffer j = Polynomial.eval (evaluationPointΟ‰ 𝔽q Ξ² h_β„“_add_R_rate ⟨0, β‹―βŸ© j) P