Documentation

CompPoly.Fields.KoalaBear.Fast

Fast KoalaBear Field #

A native-word Montgomery implementation of KoalaBear arithmetic. The shared algorithms and proofs live in CompPoly.Fields.Montgomery.Native32Field; this module supplies the KoalaBear constants and its concrete API.

Parameters and carrier #

source
@[instance_reducible]
instance KoalaBear.Fast.instMont32Field :
Montgomery.Native32.Mont32Field fieldSize

The per-field data realizing KoalaBear as a fast 32-bit-word Montgomery field.

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

The fast native-word KoalaBear field carrier, stored as a Montgomery residue.

Instances For

    Conversions #

    source
    @[inline]
    def KoalaBear.Fast.ofUInt32 (x : UInt32) :
    Field

    Convert a 32-bit word into fast Montgomery representation.

    Instances For
      source
      @[inline]
      def KoalaBear.Fast.ofField (x : KoalaBear.Field) :
      Field

      Convert from the canonical ZMod KoalaBear field into fast Montgomery form.

      Instances For

        Canonical bridge #

        source
        def KoalaBear.Fast.ringEquiv :
        Field ≃+* KoalaBear.Field

        Ring equivalence between the fast Montgomery representation and canonical KoalaBear.Field.

        Instances For

          Two-adic roots #

          source
          def KoalaBear.Fast.twoAdicGenerators :
          List Field

          Precomputed KoalaBear two-adic generators in Montgomery representation.

          Instances For
            source
            theorem KoalaBear.Fast.twoAdicGenerators_eq_map :
            twoAdicGenerators = List.map ofField KoalaBear.twoAdicGenerators

            The Montgomery root table represents the canonical KoalaBear roots.