src/crypto/secp256k1/limbs.bend checks

s mod 2^16 and s div 2^16

2^16 - 1 - x for x below 2^16

limb-wise sum; the longer tail is kept

every limb times a

the schoolbook product without carries: conv(x :: xs, ys) = x ys + 2^16 conv(xs, ys)

the value of the limbs (only ever of an empty list at run time: see carry)

A carry pass: n limbs, each below 2^16, then one limb holding the carry u out of them plus the value of whatever is left of xs past n limbs (on every call below xs has at most n limbs, so that is the carry alone). Every function here looks at its list before producing anything, so that on a symbolic argument the proof checker stops at once.

every limb x becomes 2^16 - 1 - x

b x + (1 - b) y, limb-wise, for b in {0, 1}

the normalized form of a value below 2^256: exactly 16 limbs below 2^16

lo + c hi, for x = lo + 2^256 hi: congruent to x modulo m

the part of a carried value above 2^256 (0 or 1 below)

t (16 limbs, value below 2^256) mod m: t + c has bit 256 set exactly when t >= m, and then its low 256 bits are t - m

x mod m for x below 2^512, in k folds (x is looked at first, so that the proof checker keeps an unknown reduction folded)

m - b = (2^256 - 1 - (b + c)) + 1, for b < m (so b + c < 2^256); no constant but c is ever formed

x < m, i.e. x + c < 2^256, for x of 16 limbs below 2^16

1 when the value of xs is below the value of ys plus br, else 0 (the borrow out of xs - ys - br), for lists of the same length

OR of all limbs being nonzero, without an early exit

the k low bits of x, most significant first

every bit flipped: the bits of 2^k - 1 - x from those of x

all bits of a limb list, most significant first (16 per limb)