spec/crypto/curve25519/x25519.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as X25519

4 imports

import Base
import ../../lib/common.bend as C
import ./field.bend as FS
import ../../../src/crypto/curve25519/x25519.bend as X

Types

type LSt source · line 94 · raw

Data

LSt

@x2:Nat -> @z2:Nat -> @x3:Nat -> @z3:Nat -> @swap:Nat -> LSt

Definitions

def clamp_last source · line 19 · raw

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

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

def clamp source · line 30 · raw

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

def decode_scalar source · line 37 · raw

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

def mask_last source · line 41 · raw

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

decodeUCoordinate: the last byte's top bit masked (bits = 255)

def decode_u source · line 52 · raw

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

def le_bytes source · line 56 · raw

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

encodeUCoordinate: u mod p as 32 little-endian bytes

def encode_u source · line 63 · raw

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

def kbit source · line 67 · raw

@+k:Nat -> @t:Nat -> Nat

k_t = (k >> t) & 1

def bxor source · line 71 · raw

@a:Nat -> @b:Nat -> Nat

swap ^= k_t, on bits

def cs_fst source · line 80 · raw

@swap:Nat -> @a:Nat -> @b:Nat -> Nat

cswap(swap, a, b), RFC 7748: (a, b) when swap is 0, (b, a) when it is 1; cs_fst and cs_snd are its two components

def cs_snd source · line 87 · raw

@swap:Nat -> @a:Nat -> @b:Nat -> Nat

def a24 source · line 98 · raw

@+one:Nat -> Nat

a24 = 121665

def step source · line 101 · raw

@+one:Nat -> @+p:Nat -> @+x1:Nat -> @+x2:Nat -> @+z2:Nat -> @+x3:Nat -> @+z3:Nat -> @kt:Nat -> LSt

def rung source · line 115 · raw

@+one:Nat -> @+p:Nat -> @+x1:Nat -> @st:LSt -> @+kt:Nat -> LSt

def ladder source · line 122 · raw

@+one:Nat -> @+p:Nat -> @n:Nat -> @+k:Nat -> @+x1:Nat -> @st:LSt -> LSt

for t = n - 1 down to 0

def finish source · line 129 · raw

@+p:Nat -> @st:LSt -> List<&2, U32>

def bits source · line 135 · raw

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

RFC 7748's bits (255 for X25519) as 8 * len(k) - 1 of the 32-byte scalar

def x25519_p source · line 138 · raw

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

def x25519 source · line 142 · raw

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

def X25519.value source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(k) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(u) == True{} : Bool} -> Type

def X25519.checked source · line 150 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> Type