Native Ed25519 arithmetic #

RFC 8032 arithmetic over ZMod p, with the affine twisted-Edwards addition formula.

source

@[reducible, inline]

abbrev Cryptlib.Primitives.Sign.Ed25519Math.p :

ℕ

Equations

Cryptlib.Primitives.Sign.Ed25519Math.p = Cryptlib.Primitives.NIKE.X25519Common.p

Instances For

source

@[reducible, inline]

abbrev Cryptlib.Primitives.Sign.Ed25519Math.ell :

ℕ

Equations

Cryptlib.Primitives.Sign.Ed25519Math.ell = 2 ^ 252 + 27742317777372353535851937790883648493

Instances For

source

theorem Cryptlib.Primitives.Sign.Ed25519Math.p_prime :

Nat.Prime p

source

instance Cryptlib.Primitives.Sign.Ed25519Math.instFactPrimeP :

Fact (Nat.Prime p)

source

@[reducible, inline]

abbrev Cryptlib.Primitives.Sign.Ed25519Math.F :

Type

Equations

Cryptlib.Primitives.Sign.Ed25519Math.F = ZMod Cryptlib.Primitives.Sign.Ed25519Math.p

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.d :

Equations

Cryptlib.Primitives.Sign.Ed25519Math.d = -121665 / 121666

Instances For

source

structure Cryptlib.Primitives.Sign.Ed25519Math.Point :

Type

x : F
y : F

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.instDecidableEqPoint.decEq (x✝ x✝¹ : Point) :

Decidable (x✝ = x✝¹)

Equations

Cryptlib.Primitives.Sign.Ed25519Math.instDecidableEqPoint.decEq { x := a, y := a_1 } { x := b, y := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

source

@[instance_reducible]

instance Cryptlib.Primitives.Sign.Ed25519Math.instDecidableEqPoint :

DecidableEq Point

Equations

Cryptlib.Primitives.Sign.Ed25519Math.instDecidableEqPoint = Cryptlib.Primitives.Sign.Ed25519Math.instDecidableEqPoint.decEq

source

def Cryptlib.Primitives.Sign.Ed25519Math.onCurve (q : Point) :

Prop

Equations

Cryptlib.Primitives.Sign.Ed25519Math.onCurve q = (-q.x ^ 2 + q.y ^ 2 = 1 + Cryptlib.Primitives.Sign.Ed25519Math.d * q.x ^ 2 * q.y ^ 2)

Instances For

source

@[instance_reducible]

instance Cryptlib.Primitives.Sign.Ed25519Math.decidableOnCurve (q : Point) :

Decidable (onCurve q)

Equations

Cryptlib.Primitives.Sign.Ed25519Math.decidableOnCurve q = Cryptlib.Primitives.Sign.Ed25519Math.decidableOnCurve._aux_1 q

source

def Cryptlib.Primitives.Sign.Ed25519Math.zero :

Point

Equations

Cryptlib.Primitives.Sign.Ed25519Math.zero = { x := 0, y := 1 }

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.add (q r : Point) :

Point

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[irreducible]

def Cryptlib.Primitives.Sign.Ed25519Math.scalarMul (n : ℕ) (q : Point) :

Point

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.basepoint :

Point

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.bytesToNat (bs : List UInt8) :

ℕ

Equations

Cryptlib.Primitives.Sign.Ed25519Math.bytesToNat bs = Nat.ofDigits 256 (List.map UInt8.toNat bs)

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.natToBytes (width n : ℕ) :

List UInt8

Equations

Cryptlib.Primitives.Sign.Ed25519Math.natToBytes width n = List.map (fun (i : ℕ) => (n >>> (8 * i)).toUInt8) (List.range width)

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.vectorToByteArray {n : ℕ} (v : Vector UInt8 n) :

ByteArray

Equations

Cryptlib.Primitives.Sign.Ed25519Math.vectorToByteArray v = { data := v.toArray }

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.leBytes (z : F) (width : ℕ) :

List UInt8

Equations

Cryptlib.Primitives.Sign.Ed25519Math.leBytes z width = Cryptlib.Primitives.Sign.Ed25519Math.natToBytes width (ZMod.val z)

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.encodePoint (q : Point) :

Vector UInt8 32

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[irreducible]

def Cryptlib.Primitives.Sign.Ed25519Math.powAux (base : F) (e : ℕ) :

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.sqrtMinusOne :

Equations

Cryptlib.Primitives.Sign.Ed25519Math.sqrtMinusOne = 19681161376707505956807079304988542015446066515923890162744021073123829784752

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.decodePoint (v : Vector UInt8 32) :

Option Point

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.scalarFromSeed (seed : Vector UInt8 32) :

ℕ

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.publicKey (seed : Vector UInt8 32) :

Vector UInt8 32

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.hashNat (parts : List ByteArray) :

ℕ

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.signNative (seed : Vector UInt8 32) (message : ByteArray) :

Vector UInt8 64

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cryptlib.Primitives.Sign.Ed25519Math.verifyNative (pk : Vector UInt8 32) (message : ByteArray) (sig : Vector UInt8 64) :

Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

Documentation

Cryptlib.Primitives.Sign.Ed25519_math

Native Ed25519 arithmetic #