Documentation

MIPRE.Foundations.SAT.NormalElementProg

A polynomial-time constructor of a normal basis #

source
theorem MIPRE.SAT.instFactPrimeOfNatNat_mIPRE_6 :
Fact (Nat.Prime 2)
source
noncomputable def MIPRE.SAT.shoupZeroProg :
Cost.PolyTimeFun Cost.Unary Cost.BitStr
Equations
Instances For
    source
    theorem MIPRE.SAT.shoupZeroProg_correct (k : ℕ) (hk : 1 ≤ k) :
    shoupZeroProg.toFun (Cost.unary k) = (shoupBinField k hk).toBits 0
    source
    theorem MIPRE.SAT.shoupNonzeroRow_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) :
    LowDegree.BinaryLinear.nonzeroRow ((shoupBinField k hk).toBits a) = decide (a ≠ 0)
    source
    theorem MIPRE.SAT.shoupXorBits_correct (k : ℕ) (hk : 1 ≤ k) (a b : (shoupBinField k hk).carrier) :
    LowDegree.BinaryPolynomial.xorBits ((shoupBinField k hk).toBits a) ((shoupBinField k hk).toBits b) = (shoupBinField k hk).toBits (a + b)
    source
    noncomputable def MIPRE.SAT.selectNonzeroStep :
    Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr
    Equations
    Instances For
      source
      noncomputable def MIPRE.SAT.firstNonzeroBitsProg :
      Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr) Cost.BitStr

      Scan right to left, retaining each nonzero row; the result is the first such row.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.SAT.firstNonzeroBitsProg_correct (k : ℕ) (hk : 1 ≤ k) (l : List (shoupBinField k hk).carrier) :
        firstNonzeroBitsProg.toFun (List.map (shoupBinField k hk).toBits l, (shoupBinField k hk).toBits 0) = (shoupBinField k hk).toBits (firstNonzero l)
        source
        noncomputable def MIPRE.SAT.shoupProjectionImagesProg :
        Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) (List Cost.BitStr)

        Apply the supplied projection to each vector of the polynomial basis.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.SAT.shoupProjectionImagesProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (e : AddMonoidAlgebra (ZMod 2) (Fin k)) :
          shoupProjectionImagesProg.toFun (Cost.unary k, LowDegree.BinaryLinear.vectorBits ((LowDegree.BinaryLinear.groupCoordinates k) e)) = List.ofFn fun (j : Fin k) => (shoupBinField k hk).toBits (((shoupFrobeniusAction k hk) e) ((shoupPowerBasis k hk) j))
          source
          noncomputable def MIPRE.SAT.shoupProjectedVectorProg :
          Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr
          Equations
          Instances For
            source
            theorem MIPRE.SAT.shoupProjectedVectorProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (e : AddMonoidAlgebra (ZMod 2) (Fin k)) :
            shoupProjectedVectorProg.toFun (Cost.unary k, LowDegree.BinaryLinear.vectorBits ((LowDegree.BinaryLinear.groupCoordinates k) e)) = (shoupBinField k hk).toBits (shoupProjectedVector k hk e)
            source
            theorem MIPRE.SAT.shoupArithmeticFold_add_correct (k : ℕ) (hk : 1 ≤ k) (l : List (shoupBinField k hk).carrier) (a : (shoupBinField k hk).carrier) (p : Cost.BitStr) :
            LowDegree.BinaryPolynomial.arithmeticFold false p ((shoupBinField k hk).toBits a) (List.map (shoupBinField k hk).toBits l) = (shoupBinField k hk).toBits (a + l.sum)
            source
            noncomputable def MIPRE.SAT.shoupSumProg :
            Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) Cost.BitStr
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MIPRE.SAT.shoupSumProg_correct (k : ℕ) (hk : 1 ≤ k) (l : List (shoupBinField k hk).carrier) :
              shoupSumProg.toFun (Cost.unary k, List.map (shoupBinField k hk).toBits l) = (shoupBinField k hk).toBits l.sum
              source
              noncomputable def MIPRE.SAT.shoupNormalElementProg :
              Cost.PolyTimeFun Cost.Unary Cost.BitStr

              Compute all primitive projections, select their first nonzero images, and sum them.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPRE.SAT.shoupNormalElementProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] :
                shoupNormalElementProg.toFun (Cost.unary k) = (shoupBinField k hk).toBits (shoupNormalElement k hk)
                source
                noncomputable def MIPRE.SAT.shoupNormalBasisProg :
                Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

                Print the constructed normal basis in Frobenius order.

                Equations
                Instances For
                  source
                  theorem MIPRE.SAT.shoupNormalBasisProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) :
                  shoupNormalBasisProg.toFun (Cost.unary k) = List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits ((shoupNormalBasis k hk hodd) i)