Documentation

CompPoly.Univariate.NTT.Transform

Shared radix-2 NTT transform #

This file provides the root-parametric bit-reversal and butterfly machinery used by forward and inverse radix-2 NTTs.

source
def CompPoly.CPolynomial.NTT.Transform.bitRevNat :
ℕ → ℕ → ℕ

Reverse the lowest bits bits of i.

Instances For
    source
    theorem CompPoly.CPolynomial.NTT.Transform.bitRevNat_lt (bits i : ℕ) :
    bitRevNat bits i < 2 ^ bits
    source
    theorem CompPoly.CPolynomial.NTT.Transform.bitRevNat_even (bits b : ℕ) :
    bitRevNat (bits + 1) (2 * b) = bitRevNat bits b
    source
    theorem CompPoly.CPolynomial.NTT.Transform.bitRevNat_odd_or (bits b : ℕ) :
    bitRevNat (bits + 1) (2 * b + 1) = 1 <<< bits ||| bitRevNat bits b
    source
    theorem CompPoly.CPolynomial.NTT.Transform.bitRevNat_odd (bits b : ℕ) :
    bitRevNat (bits + 1) (2 * b + 1) = 2 ^ bits + bitRevNat bits b
    source
    def CompPoly.CPolynomial.NTT.Transform.bitRevPermute {R : Type u_1} [Field R] (D : Domain R) (a : Array R) :
    Array R

    Apply bit-reversal permutation to an evaluation array.

    Instances For
      source
      def CompPoly.CPolynomial.NTT.Transform.butterflyInnerStep {R : Type u_1} [Field R] (blockSize half : ℕ) (wm : R) (block j : ℕ) (st : Array R × R) :
      Array R × R
      Instances For
        source
        def CompPoly.CPolynomial.NTT.Transform.butterflyBlockStep {R : Type u_1} [Field R] (blockSize half : ℕ) (wm : R) (block : ℕ) (acc : Array R) :
        Array R
        Instances For
          source
          def CompPoly.CPolynomial.NTT.Transform.butterflyStage {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) :
          Array R

          One butterfly stage of the iterative radix-2 transform.

          Instances For
            source
            def CompPoly.CPolynomial.NTT.Transform.butterflyStageSpec {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) :
            Array R

            Pure structural-recursive specification of one butterfly stage.

            This matches the imperative control flow of butterflyStage, but replaces the for loops with explicit Nat.rec recursors.

            Instances For
              source
              theorem CompPoly.CPolynomial.NTT.Transform.butterflyStage_eq_butterflyStageSpec {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) :
              butterflyStage D stage a = butterflyStageSpec D stage a

              The imperative butterfly loop agrees with the pure pointwise butterfly stage specification.

              This is where the local set! bookkeeping for one stage belongs.

              source
              @[simp]
              theorem CompPoly.CPolynomial.NTT.Transform.size_butterflyInnerStep {R : Type u_1} [Field R] (blockSize half : ℕ) (wm : R) (block j : ℕ) (st : Array R × R) :
              (butterflyInnerStep blockSize half wm block j st).1.size = st.1.size
              source
              @[simp]
              theorem CompPoly.CPolynomial.NTT.Transform.size_butterflyBlockStep {R : Type u_1} [Field R] (blockSize half : ℕ) (wm : R) (block : ℕ) (acc : Array R) :
              (butterflyBlockStep blockSize half wm block acc).size = acc.size
              source
              theorem CompPoly.CPolynomial.NTT.Transform.size_butterflyStageSpec {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) :
              (butterflyStageSpec D stage a).size = a.size
              source
              theorem CompPoly.CPolynomial.NTT.Transform.size_butterflyStage {R : Type u_1} [Field R] (D : Domain R) (stage : ℕ) (a : Array R) :
              (butterflyStage D stage a).size = a.size
              source
              def CompPoly.CPolynomial.NTT.Transform.runStages {R : Type u_1} [Field R] (D : Domain R) (a : Array R) :
              Array R

              Run all radix-2 butterfly stages (complexity: O(n log n)).

              Instances For
                source
                theorem CompPoly.CPolynomial.NTT.Transform.runStages_eq_rec {R : Type u_1} [Field R] (D : Domain R) (a : Array R) :
                runStages D a = Nat.rec a (fun (stage : ℕ) (acc : Array R) => butterflyStage D stage acc) D.logN

                The imperative stage loop agrees with the corresponding Nat.rec.