src/crypto/curve25519/x25519.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/curve25519/x25519.bend as X25519

2 imports

import Base
import ./field.bend as F

Types

type St source · line 15 · raw

Data

St

@x2:List<&2, U32> -> @z2:List<&2, U32> -> @x3:List<&2, U32> -> @z3:List<&2, U32> -> @swap:U32 -> St

Definitions

def kbit source · line 19 · raw

@bs:List<&2, U32> -> @t:Nat -> U32

bit t of a little-endian byte string

def clamp_top source · line 45 · raw

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

RFC 7748 decodeScalar25519's clamping: k[0] &= 248, k[31] &= 127, k[31] |= 64

def clamp source · line 56 · raw

@bs:List<&2, U32> -> List<&2, U32>

def a24 source · line 64 · raw

List<&2, U32>

a24 = 121665 as a field element

def step source · line 69 · raw

@+c24:List<&2, U32> -> @+x1:List<&2, U32> -> @+x2:List<&2, U32> -> @+z2:List<&2, U32> -> @+x3:List<&2, U32> -> @+z3:List<&2, U32> -> @kt:U32 -> St

one ladder step on the swapped pair (x2 : z2), (x3 : z3); c24 is a24

def rung source · line 82 · raw

@+c24:List<&2, U32> -> @+x1:List<&2, U32> -> @st:St -> @+kt:U32 -> St

swap ^= k_t; cswap; the step; swap = k_t

def len source · line 91 · raw

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

the ladder's bit count, 8 len(k) - 1: 255 for a 32-byte scalar (RFC 7748 bits). Taken from the scalar, it keeps the proof checker from unfolding the 255 steps for an unknown scalar.

def bitlen source · line 99 · raw

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

8 len(xs), the bit count of a byte string

def nbits source · line 106 · raw

@+k:List<&2, U32> -> Nat

def ladder source · line 110 · raw

@n:Nat -> @+c24:List<&2, U32> -> @+k:List<&2, U32> -> @+x1:List<&2, U32> -> @st:St -> St

bits t = n - 1 down to 0

def finish source · line 118 · raw

@st:St -> List<&2, U32>

the final cswap, then x2 * z2^(p - 2), encoded

def x25519_raw source · line 124 · raw

@+k:List<&2, U32> -> @u:List<&2, U32> -> List<&2, U32>

X25519 on two 32-byte strings of bytes below 256

def valid_bytes source · line 129 · raw

@n:Nat -> @xs:List<&2, U32> -> Bool

32 values, each below 256

def x25519_if source · line 144 · raw

@ok:Bool -> @k:List<&2, U32> -> @u:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def x25519 source · line 152 · raw

@+k:List<&2, U32> -> @+u:List<&2, U32> -> Maybe<&2, List<&2, U32>>

X25519(k, u); None unless both are 32 bytes below 256

def base source · line 156 · raw

List<&2, U32>

the base point u = 9