Documentation

CompPoly.Univariate.NTTFast.Correctness.Pipeline

NTTFast multiplication correctness #

Plan-level and one-shot correctness theorems for NTTFast multiplication.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.forwardImpl_correct {R : Type u_1} [Field R] (P : Plan R) (hP : P.WellFormed) (p : Raw R) :
P.forwardImpl p = NTT.Transform.bitRevPermute P.domain (NTT.Forward.forwardSpec P.domain p)

A well-formed plan's forward transform computes the bit-reversed forward NTT.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.forwardImpl_ofDomain_correct {R : Type u_1} [Field R] (D : NTT.Domain R) (p : Raw R) :
(ofDomain D).forwardImpl p = NTT.Transform.bitRevPermute D (NTT.Forward.forwardSpec D p)

A plan built from a domain has a correct forward transform.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.forwardPairImpl_eq_pair {R : Type u_1} [Field R] (P : Plan R) (hP : P.WellFormed) (p q : Raw R) :
P.forwardPairImpl p q = (P.forwardImpl p, P.forwardImpl q)

The paired forward transform equals the pair of individual forward transforms.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.forwardPairImpl_correct {R : Type u_1} [Field R] (P : Plan R) (hP : P.WellFormed) (p q : Raw R) :
P.forwardPairImpl p q = (NTT.Transform.bitRevPermute P.domain (NTT.Forward.forwardSpec P.domain p), NTT.Transform.bitRevPermute P.domain (NTT.Forward.forwardSpec P.domain q))

The paired forward transform computes the two bit-reversed forward NTT outputs.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.normalize_eq_ntt_normalize {R : Type u_1} [Field R] (P : Plan R) (hP : P.WellFormed) (a : Array R) :
P.normalize a = NTT.Inverse.normalize P.domain a

Plan normalization agrees with NTT.Inverse.normalize for the same domain.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.inverseImpl_correct {R : Type u_1} [Field R] (P : Plan R) (hP : P.WellFormed) (v : Array R) :
P.inverseImpl (NTT.Transform.bitRevPermute P.domain v) = NTT.Inverse.inverseSpec P.domain v

A well-formed plan's inverse transform computes the inverse NTT spec.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.pointwiseMul_bitRevPermute_forwardSpec_eq {R : Type u_1} [Field R] (D : NTT.Domain R) (p q : Raw R) :
NTT.FastMul.pointwiseMul D (NTT.Transform.bitRevPermute D (NTT.Forward.forwardSpec D p)) (NTT.Transform.bitRevPermute D (NTT.Forward.forwardSpec D q)) = NTT.Transform.bitRevPermute D (NTT.FastMul.pointwiseMul D (NTT.Forward.forwardSpec D p) (NTT.Forward.forwardSpec D q))

Pointwise multiplication commutes with applying the bit-reversal permutation.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.Raw.fastMulImpl_correct {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (P : Plan R) (hP : P.WellFormed) (p q : Raw R) :
fastMulImpl P p q = NTT.FastMul.Raw.fastMulSpec P.domain p q

The planned raw multiplication implementation computes the raw NTT multiplication spec.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.Raw.fastMulImpl_trim_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (P : Plan R) (hP : P.WellFormed) (p q : Raw R) (hfit : P.domain.fits p q) :
(fastMulImpl P p q).trim = p * q

The planned raw multiplication implementation trims to ordinary multiplication.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.fastMulImpl_correct {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (P : Plan R) (hP : P.WellFormed) (p q : CPolynomial R) :
P.fastMulImpl p q = NTT.FastMul.fastMulSpec P.domain p q

The planned multiplication implementation computes the NTT multiplication spec.

source
theorem CompPoly.CPolynomial.NTTFast.Plan.fastMulImpl_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (P : Plan R) (hP : P.WellFormed) (p q : CPolynomial R) (hfit : P.domain.fits ↑p ↑q) :
P.fastMulImpl p q = p * q

The planned multiplication implementation agrees with ordinary multiplication.

source
theorem CompPoly.CPolynomial.NTTFast.Raw.fastMulImpl_correct {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : Raw R) :
fastMulImpl D p q = NTT.FastMul.Raw.fastMulSpec D p q

The one-shot raw multiplication implementation computes the raw NTT multiplication spec.

source
theorem CompPoly.CPolynomial.NTTFast.Raw.fastMulImpl_trim_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : Raw R) (hfit : D.fits p q) :
(fastMulImpl D p q).trim = p * q

The one-shot raw multiplication implementation trims to ordinary multiplication.

source
theorem CompPoly.CPolynomial.NTTFast.fastMulImpl_correct {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : CPolynomial R) :
fastMulImpl D p q = NTT.FastMul.fastMulSpec D p q

The one-shot multiplication implementation computes the NTT multiplication spec.

source
theorem CompPoly.CPolynomial.NTTFast.fastMulImpl_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : CPolynomial R) (hfit : D.fits ↑p ↑q) :
fastMulImpl D p q = p * q

The one-shot multiplication implementation agrees with ordinary multiplication.

source
theorem CompPoly.CPolynomial.NTTFast.safeFastMul_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : NTT.Domain R) (p q : CPolynomial R) (hfit : D.fits ↑p ↑q) :
safeFastMul D p q hfit = p * q

The safe one-shot wrapper agrees with ordinary multiplication.

source
theorem CompPoly.CPolynomial.NTTFast.withFallback_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) (p q : CPolynomial R) :
withFallback bestDomainForLength? p q = p * q

withFallback agrees with canonical polynomial multiplication.