src/crypto/ed25519/point.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/ed25519/point.bend as Point

3 imports

import Base
import ../curve25519/field.bend as F
import ../curve25519/x25519.bend as X

Types

type Pt source · line 12 · raw

Data

Pt

@x:List<&2, U32> -> @y:List<&2, U32> -> @z:List<&2, U32> -> @t:List<&2, U32> -> Pt

type Cs source · line 16 · raw

Data

d = -121665 / 121666, 2 d, sqrt(-1) = 2^((p - 1) / 4)

Cs

@d:List<&2, U32> -> @d2:List<&2, U32> -> @sqm1:List<&2, U32> -> Cs

Definitions

def c121665 source · line 19 · raw

List<&2, U32>

def c121666 source · line 23 · raw

List<&2, U32>

def pow_p14 source · line 28 · raw

@+x:List<&2, U32> -> List<&2, U32>

2^((p - 1) / 4), (p - 1) / 4 = 2^253 - 5: 250 one bits, then 0 1 1

def cs_d source · line 31 · raw

@c:Cs -> List<&2, U32>

def cs_d2 source · line 36 · raw

@c:Cs -> List<&2, U32>

def cs_s source · line 41 · raw

@c:Cs -> List<&2, U32>

def lit source · line 49 · raw

@xs:List<&2, U32> -> @k:List<&2, U32> -> List<&2, U32>

k itself; taking an input list xs keeps the proof checker from computing with the constant k while xs is unknown (it would otherwise evaluate the whole field arithmetic on constants whenever it compares two terms)

def cs_of source · line 56 · raw

@+d:List<&2, U32> -> @+xs:List<&2, U32> -> Cs

def consts source · line 60 · raw

@+xs:List<&2, U32> -> Cs

the curve constants, computed (xs is any input, see lit)

def identity source · line 63 · raw

Pt

def add source · line 67 · raw

@+c:Cs -> @p:Pt -> @q:Pt -> Pt

RFC 8032 5.1.4, addition

def double source · line 81 · raw

@p:Pt -> Pt

RFC 8032 5.1.4, doubling

def select source · line 95 · raw

@+s:U32 -> @p:Pt -> @q:Pt -> Pt

s == 0: p; s == 1: q

def smul source · line 101 · raw

@n:Nat -> @+c:Cs -> @+bs:List<&2, U32> -> @+p:Pt -> @q:Pt -> Pt

[bits t = n - 1 .. 0 of bs] p added to 2^n q: double, add, select

def mul source · line 110 · raw

@+c:Cs -> @+k:List<&2, U32> -> @+p:Pt -> Pt

[k] p for a byte-string scalar k

def set_top source · line 114 · raw

@xs:List<&2, U32> -> @+b:U32 -> List<&2, U32>

the last byte with bit 7 set to b (the canonical y has it clear)

def encode source · line 126 · raw

@p:Pt -> List<&2, U32>

RFC 8032 5.1.2

def ge_p source · line 133 · raw

@+y:List<&2, U32> -> Bool

y >= p: the carry of y + 2^256 - p is not 0

def dec_fin source · line 136 · raw

@+x:List<&2, U32> -> @+y:List<&2, U32> -> @+x0:U32 -> @fail:Bool -> Maybe<&2, Pt>

def dec_root source · line 144 · raw

@+c:Cs -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+x0:U32 -> @+u:List<&2, U32> -> @+vxx:List<&2, U32> -> @is_u:Bool -> @is_nu:Bool -> Maybe<&2, Pt>

def dec_y source · line 156 · raw

@+c:Cs -> @+y:List<&2, U32> -> @+x0:U32 -> @bad:Bool -> Maybe<&2, Pt>

def decode source · line 171 · raw

@+c:Cs -> @+bs:List<&2, U32> -> Maybe<&2, Pt>

RFC 8032 5.1.3 on 32 bytes below 256

def equal source · line 176 · raw

@p:Pt -> @q:Pt -> Bool

the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1

def base_of source · line 182 · raw

@m:Maybe<&2, Pt> -> Pt

the base point: y = 4 / 5, x even

def base source · line 189 · raw

@+c:Cs -> @+xs:List<&2, U32> -> Pt