Documentation

Cryptlib.Primitives.NIKE.X25519Common

X25519 primitives shared by both implementations #

The field prime, RFC 7748 byte decoding and clamping, the basepoint, and the private key type.

source
@[reducible, inline]
abbrev Cryptlib.Primitives.NIKE.X25519Common.keySize :
ℕ
Equations
Instances For
    source
    def Cryptlib.Primitives.NIKE.X25519Common.p :
    ℕ

    The Curve25519 prime, 2^255 - 19.

    Equations
    Instances For
      source
      instance Cryptlib.Primitives.NIKE.X25519Common.instNeZeroNatP :
      NeZero p
      source
      def Cryptlib.Primitives.NIKE.X25519Common.basepoint :
      ZMod p

      The x-coordinate of the standard basepoint.

      Equations
      Instances For
        source
        def Cryptlib.Primitives.NIKE.X25519Common.toField (v : Vector UInt8 keySize) :
        ZMod p

        Little-endian byte decoding, with bit 255 masked per RFC 7748.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cryptlib.Primitives.NIKE.X25519Common.clampScalar (v : Vector UInt8 keySize) :
          Vector UInt8 keySize

          RFC 7748 clamping: clear the low three bits, clear bit 255, set bit 254.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            structure Cryptlib.Primitives.NIKE.X25519Common.PrivateKey :
            Type

            A private key: a 32-byte scalar seed, clamped on use.

            Instances For