Documentation

CompPoly.Fields.KoalaBear.Basic

KoalaBear Field 2^{31} - 2^{24} + 1 #

This is the field used for lean Ethereum spec.

source
@[reducible]
def KoalaBear.fieldSize :
ℕ

The KoalaBear field modulus, 2^31 - 2^24 + 1.

Instances For
    source
    @[reducible, inline]
    abbrev KoalaBear.Field :
    Type

    The KoalaBear prime field as a ZMod.

    Instances For
      source
      theorem KoalaBear.is_prime :
      Nat.Prime fieldSize

      The KoalaBear modulus is prime.

      Constants #

      These are convenience constants to match the Python module:

      source
      @[reducible]
      def KoalaBear.pBits :
      ℕ

      Bit width of the KoalaBear modulus.

      Instances For
        source
        @[reducible]
        def KoalaBear.twoAdicity :
        ℕ

        The largest supported power-of-two root-of-unity exponent for KoalaBear.

        Instances For

          Provide instances so KoalaBear.Field = ZMod fieldSize is available as a Field and as a NonBinaryField (char ≠ 2).

          source
          instance KoalaBear.instFactPrimeFieldSize :
          Fact (Nat.Prime fieldSize)
          source
          @[implicit_reducible]
          instance KoalaBear.instFieldField :
          _root_.Field Field
          source
          @[implicit_reducible]
          instance KoalaBear.instNonBinaryFieldField :
          NonBinaryField Field

          Two-adicity and roots of unity table #

          We record the factorization of fieldSize - 1 and provide a precomputed table of 2^n-th roots of unity for 0 ≤ n ≤ twoAdicity.

          source
          theorem KoalaBear.fieldSize_sub_one_factorization :
          fieldSize - 1 = 2 ^ twoAdicity * 127

          The factorization fieldSize - 1 = 2^twoAdicity * 127.

          A table of 2^n-th roots of unity. The element at index n generates the multiplicative subgroup of order 2^n.

          The first entry n = 0 is 1.

          source
          def KoalaBear.twoAdicGenerators :
          List Field

          Precomputed generators for the KoalaBear two-adic subgroups.

          Instances For
            source
            @[simp]
            theorem KoalaBear.twoAdicGenerators_length :
            twoAdicGenerators.length = twoAdicity + 1
            source
            @[simp]
            theorem KoalaBear.twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
            twoAdicGenerators[↑idx + 1] ^ 2 = twoAdicGenerators[idx]
            source
            @[simp]
            theorem KoalaBear.twoAdicGenerators_succ_square_eq (idx : ℕ) (h : idx < twoAdicity) :
            twoAdicGenerators[idx + 1] ^ 2 = twoAdicGenerators[idx]

            Statements requested by the Python spec translation.

            source
            theorem KoalaBear.inv_eq_pow (a : Field) (ha : a ≠ 0) :
            a⁻¹ = a ^ (fieldSize - 2)

            Fermat-style inversion in ZMod fieldSize.

            source
            theorem KoalaBear.cube_map_bijective :
            Function.Bijective fun (x : Fieldˣ) => x ^ 3

            Bijectivity of the cube map on the unit group, using gcd(3, fieldSize-1)=1.

            The cube map x ↦ x^3 is an automorphism on the multiplicative group because Nat.coprime 3 (fieldSize - 1) holds. We record the coprimality here.

            source
            theorem KoalaBear.coprime_three_fieldSize_sub_one :
            Nat.Coprime 3 (fieldSize - 1)

            Additional statements matching the Python spec API.

            source
            theorem KoalaBear.twoAdicity_maximal :
            ¬2 ^ (twoAdicity + 1) ∣ fieldSize - 1

            twoAdicity is maximal: 2^(twoAdicity+1) does not divide fieldSize - 1.

            source
            theorem KoalaBear.twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) :
            twoAdicGenerators[bits] ^ 2 ^ ↑bits = 1

            The power (twoAdicGenerators[bits])^(2^bits) = 1.

            source
            theorem KoalaBear.twoAdicGenerators_pow_twoPow_ne_one_of_lt {bits : Fin (twoAdicity + 1)} {m : ℕ} (hm : m < ↑bits) :
            twoAdicGenerators[bits] ^ 2 ^ m ≠ 1

            If m < bits, then (twoAdicGenerators[bits])^(2^m) ≠ 1.

            source
            theorem KoalaBear.isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) :
            IsPrimitiveRoot twoAdicGenerators[n] (2 ^ ↑n)

            The precomputed element at index bits is a primitive 2^bits-th root of unity.

            source
            theorem KoalaBear.twoAdicGenerator_unit_mem_rootsOfUnity (bits : Fin (twoAdicity + 1)) (h : twoAdicGenerators[bits] ≠ 0) :
            Units.mk0 twoAdicGenerators[bits] h ∈ rootsOfUnity (2 ^ ↑bits) Field

            As a unit, the precomputed element is a member of rootsOfUnity (2^bits).

            source
            theorem KoalaBear.twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
            orderOf twoAdicGenerators[bits] = 2 ^ ↑bits

            The order of twoAdicGenerators[bits] equals 2^bits.

            source
            def KoalaBear.primitiveRoot :
            Field

            Primitive generator used by the smooth field-root splitter.

            Instances For
              source
              theorem KoalaBear.primitiveRoot_order :
              orderOf primitiveRoot = fieldSize - 1

              The smooth field-root splitter generator has full multiplicative order.

              source
              def KoalaBear.smoothRootSchedule :
              Array ℕ

              Smooth subgroup refinement schedule for fieldSize - 1 = 2^24 * 127.

              Instances For
                source
                theorem KoalaBear.smoothRootSchedule_fold_eq_one :
                List.foldl (fun (order ell : ℕ) => order / ell) (fieldSize - 1) smoothRootSchedule.toList = 1

                The KoalaBear smooth schedule refines the multiplicative group down to singleton cosets.