Documentation

CompPoly.Fields.KoalaBear

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

This is the field used for lean Ethereum spec.

source
@[reducible]
def KoalaBear.fieldSize :
ℕ
Equations
    Instances For
      source
      @[reducible, inline]
      abbrev KoalaBear.Field :
      Type
      Equations
        Instances For
          source
          theorem KoalaBear.is_prime :
          Nat.Prime fieldSize

          Constants #

          These are convenience constants to match the Python module:

          source
          @[reducible]
          def KoalaBear.pBits :
          ℕ
          Equations
            Instances For
              source
              @[reducible]
              def KoalaBear.twoAdicity :
              ℕ
              Equations
                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
                  instance KoalaBear.instFieldField :
                  _root_.Field Field
                  Equations
                    source
                    instance KoalaBear.instNonBinaryFieldField :
                    NonBinaryField Field
                    Equations

                      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

                      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
                      Equations
                        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. We leave them with sorry proofs to be filled later.

                          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, left as sorry per request.

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

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

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

                          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_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.twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
                          orderOf twoAdicGenerators[bits] = 2 ^ ↑bits

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