Documentation

Cryptlib.Primitives.Sign.Ed25519_facts

Arithmetic facts about p = 2^255 - 19 #

The non-squareness of d is Euler's criterion evaluated by decide +kernel, with fuelled square-and-multiply so the exponent never unfolds in unary.

source
@[reducible, inline]
abbrev Cryptlib.Primitives.Sign.Ed25519Facts.F :
Type
Equations
Instances For
    source
    instance Cryptlib.Primitives.Sign.Ed25519Facts.instFactPrimeP :
    Fact (Nat.Prime NIKE.X25519Common.p)
    source
    def Cryptlib.Primitives.Sign.Ed25519Facts.powModAux (m : ℕ) :
    ℕ → ℕ → ℕ → ℕ → ℕ

    Square-and-multiply modulo m, structural on fuel so the kernel can evaluate it.

    Equations
    Instances For
      source
      theorem Cryptlib.Primitives.Sign.Ed25519Facts.powModAux_modEq (m fuel b e acc : ℕ) :
      e < 2 ^ fuel → powModAux m fuel b e acc ≡ acc * b ^ e [MOD m]
      source
      theorem Cryptlib.Primitives.Sign.Ed25519Facts.pow_eq_powModAux (m a e fuel : ℕ) (he : e < 2 ^ fuel) :
      ↑a ^ e = ↑(powModAux m fuel a e 1)

      a ^ e in ZMod m computed by binary exponentiation.

      source
      def Cryptlib.Primitives.Sign.Ed25519Facts.n0 :
      ℕ

      The small integer -121665 * 121666 mod p; d = -121665/121666 is this over 121666^2.

      Equations
      Instances For
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.powMod_n0 :
        powModAux NIKE.X25519Common.p 256 n0 (NIKE.X25519Common.p / 2) 1 = NIKE.X25519Common.p - 1
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.p_odd :
        NIKE.X25519Common.p % 2 = 1
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.p_lt_fuel :
        NIKE.X25519Common.p / 2 < 2 ^ 256
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.natCast_ne_zero {n : ℕ} (h0 : n ≠ 0) (hlt : n < NIKE.X25519Common.p) :
        ↑n ≠ 0
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.two_ne :
        2 ≠ 0
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.n0_cast :
        ↑n0 = -121665 * 121666
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.minus_one_ne_one :
        -1 ≠ 1
        source
        theorem Cryptlib.Primitives.Sign.Ed25519Facts.n0_nonsquare :
        ¬IsSquare ↑n0
        source
        def Cryptlib.Primitives.Sign.Ed25519Facts.d :
        F

        Edwards d for Ed25519.

        Equations
        Instances For
          source
          theorem Cryptlib.Primitives.Sign.Ed25519Facts.h121666 :
          121666 ≠ 0
          source
          theorem Cryptlib.Primitives.Sign.Ed25519Facts.d_ne_zero :
          d ≠ 0
          source
          theorem Cryptlib.Primitives.Sign.Ed25519Facts.d_rel :
          d * 121666 = -121665
          source
          theorem Cryptlib.Primitives.Sign.Ed25519Facts.d_nonsquare :
          ¬IsSquare d

          d is not a square in F.

          source
          theorem Cryptlib.Primitives.Sign.Ed25519Facts.not_sq_of_d_mul {t s : F} (ht : t ≠ 0) (h : d * t ^ 2 = s ^ 2) :
          False

          d times a nonzero square is never a square.

          source
          def Cryptlib.Primitives.Sign.Ed25519Facts.i :
          F

          √-1 in F.

          Equations
          Instances For
            source
            theorem Cryptlib.Primitives.Sign.Ed25519Facts.i_sq :
            i ^ 2 = -1
            source
            def Cryptlib.Primitives.Sign.Ed25519Facts.c :
            F

            c = √-486664, the constant of the birational map.

            Equations
            Instances For
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Facts.c_sq :
              c ^ 2 = -486664
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Facts.c_ne_zero :
              c ≠ 0
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Facts.d_mul_c_sq :
              d * c ^ 2 = 486660

              d * c^2 = 486660, i.e. A - 2 for A = 486662.

              source
              theorem Cryptlib.Primitives.Sign.Ed25519Facts.no_u_minus_one (v : F) :
              v ^ 2 ≠ 486660

              No point of Curve25519 has u = -1: that would need 486660 to be a square.

              source
              theorem Cryptlib.Primitives.Sign.Ed25519Facts.i_ne_zero :
              i ≠ 0
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Facts.no_other_two_torsion (u : F) :
              u ^ 2 + 486662 * u + 1 ≠ 0

              (0,0) is the only point of Curve25519 with v = 0: u² + 486662u + 1 has no root.