src/crypto/curve25519/field.bend checks

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

1 import

import Base

Types

type Cr source · line 79 · raw

Data

limbs and the carry out of the top one

Cr
```
@limbs:List<&2, U32> -> @out:U32 -> Cr
```

Definitions

def addl source · line 27 · raw

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

limbwise sum; the longer tail is kept

def scal source · line 39 · raw

@+a:U32 -> @ys:List<&2, U32> -> List<&2, U32>

every limb times a

def conv source · line 47 · raw

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

the product polynomial: conv(x :: xs, ys) = x ys + 2^8 conv(xs, ys)

def take source · line 54 · raw

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

def drop source · line 65 · raw

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

def cr_limbs source · line 82 · raw

@r:Cr -> List<&2, U32>

def cr_out source · line 87 · raw

@r:Cr -> U32

def carry_con source · line 92 · raw

@l:U32 -> @r:Cr -> Cr

def carry source · line 98 · raw

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

one carry pass: limbs below 2^8 and the carry out of the top limb

def add0 source · line 107 · raw

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

add k to the lowest limb

def pass_fin source · line 115 · raw

@r:Cr -> List<&2, U32>

carry, then fold the carry out back in: 2^256 == 38 (mod p)

def pass source · line 120 · raw

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

def reduce source · line 124 · raw

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

32 limbs below 2^27 to a tight element of the same value mod p

def zero source · line 129 · raw

List<&2, U32>

def one source · line 133 · raw

List<&2, U32>

def small source · line 138 · raw

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

a small constant k < 2^8 as an element

def eight_p source · line 143 · raw

List<&2, U32>

8p limbwise: every limb at least 2^10 - 8, so a + 8p - b never borrows

def comp_p source · line 150 · raw

List<&2, U32>

2^256 - p = 2^255 + 19

def subl source · line 157 · raw

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

a + k - b limbwise

def add source · line 172 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> List<&2, U32>

def sub source · line 175 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> List<&2, U32>

def wide source · line 179 · raw

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

fold the product: low 32 limbs + 38 * high limbs

def mul source · line 182 · raw

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

def sq source · line 185 · raw

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

def mul_small source · line 189 · raw

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

a * k for a constant k < 2^17

def neg source · line 192 · raw

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

def select source · line 198 · raw

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

s == 0: a; s == 1: b; limbwise a * (1 - s) + b * s

def pow_ones source · line 216 · raw

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

acc^(2^n) * x^(2^n - 1): n steps of acc = acc^2 * x

def pow_bit source · line 228 · raw

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

one bit of a public exponent, most significant first: acc^2 (* x)

def pow_bits source · line 235 · raw

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

def inv source · line 247 · raw

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

x^(p - 2) = x^(2^255 - 21): 250 one bits (x, then 249 steps), then 0 1 0 1 1

def pow_p58 source · line 251 · raw

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

x^((p - 5) / 8) = x^(2^252 - 3): 250 one bits, then 0 1

def csub_fin source · line 256 · raw

@r:Cr -> @x:List<&2, U32> -> List<&2, U32>

def csub source · line 262 · raw

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

x - p when x >= p, else x (x tight): x + 2^256 - p carries out iff x >= p

def freeze source · line 266 · raw

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

the canonical representative, below p: 2^256 < 3p

def to_bytes source · line 272 · raw

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

the 32-byte little-endian encoding of a canonical element is its limbs

def mask_top source · line 276 · raw

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

the last byte with its top bit cleared (RFC 7748 decodeUCoordinate)

def of_bytes source · line 288 · raw

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

bytes to an element, bit 255 ignored

def sum_all source · line 292 · raw

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

the sum of the limbs (below 2^13 for 32 bytes); no early exit

def is_zero source · line 300 · raw

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

x == 0 in the field: every byte of the canonical form is 0

def eq source · line 304 · raw

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

a == b in the field

def low_bit source · line 308 · raw

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

the parity of the canonical representative (RFC 8032 x_0)

def parity source · line 315 · raw

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