Documentation

Cryptlib.Primitives.Sign.Ed25519_order

The basepoint has order ℓ #

Computed by decide +kernel on a mirror of Ed25519Math.add/scalarMul over naturals, with Fermat inversion; cast_eAdd and cast_eScalar prove the mirror equal to the original.

source
def Cryptlib.Primitives.Sign.Ed25519Order.d0 :
ℕ

d as a natural number.

Equations
Instances For
    source
    theorem Cryptlib.Primitives.Sign.Ed25519Order.d0_cast :
    ↑d0 = Ed25519Facts.d
    source
    def Cryptlib.Primitives.Sign.Ed25519Order.inv' (x : ℕ) :
    ℕ

    x⁻¹ by Fermat.

    Equations
    Instances For
      source
      theorem Cryptlib.Primitives.Sign.Ed25519Order.p_sub_two_lt :
      NIKE.X25519Common.p - 2 < 2 ^ 256
      source
      theorem Cryptlib.Primitives.Sign.Ed25519Order.cast_inv' (x : ℕ) :
      ↑(inv' x) = (↑x)⁻¹
      source
      def Cryptlib.Primitives.Sign.Ed25519Order.eAdd (a b : ℕ × ℕ) :
      ℕ × ℕ

      Edwards addition on naturals.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cryptlib.Primitives.Sign.Ed25519Order.eScalar :
        ℕ → ℕ → ℕ × ℕ → ℕ × ℕ

        Double-and-add on naturals, structural on fuel.

        Equations
        Instances For
          source
          def Cryptlib.Primitives.Sign.Ed25519Order.toE (a : ℕ × ℕ) :
          Ed25519Math.Point
          Equations
          Instances For
            source
            theorem Cryptlib.Primitives.Sign.Ed25519Order.cast_one_add (t : ℕ) (T : Ed25519Facts.F) (h : ↑t = T) :
            ↑((1 + t) % NIKE.X25519Common.p) = 1 + T
            source
            theorem Cryptlib.Primitives.Sign.Ed25519Order.cast_one_sub (t : ℕ) (T : Ed25519Facts.F) (ht : t < NIKE.X25519Common.p) (h : ↑t = T) :
            ↑((1 + NIKE.X25519Common.p - t) % NIKE.X25519Common.p) = 1 - T
            source
            theorem Cryptlib.Primitives.Sign.Ed25519Order.cast_eAdd (a b : ℕ × ℕ) :
            toE (eAdd a b) = Ed25519Math.add (toE a) (toE b)
            source
            theorem Cryptlib.Primitives.Sign.Ed25519Order.scalarMul_eq (n : ℕ) (q : Ed25519Math.Point) :
            Ed25519Math.scalarMul n q = if n = 0 then Ed25519Math.zero else if n % 2 = 0 then Ed25519Math.add (Ed25519Math.scalarMul (n / 2) q) (Ed25519Math.scalarMul (n / 2) q) else Ed25519Math.add q (Ed25519Math.add (Ed25519Math.scalarMul (n / 2) q) (Ed25519Math.scalarMul (n / 2) q))
            source
            theorem Cryptlib.Primitives.Sign.Ed25519Order.cast_eScalar (fuel n : ℕ) (q : ℕ × ℕ) :
            n < 2 ^ fuel → toE (eScalar fuel n q) = Ed25519Math.scalarMul n (toE q)
            source
            def Cryptlib.Primitives.Sign.Ed25519Order.basepointNat :
            ℕ × ℕ

            The RFC 8032 basepoint on naturals.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Order.toE_basepointNat :
              toE basepointNat = Ed25519Math.basepoint
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Order.eScalar_ell :
              eScalar 253 Ed25519Math.ell basepointNat = (0, 1)
              source
              theorem Cryptlib.Primitives.Sign.Ed25519Order.scalarMul_ell_basepoint :
              Ed25519Math.scalarMul Ed25519Math.ell Ed25519Math.basepoint = Ed25519Math.zero

              The basepoint has order ℓ.