bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

1.0.0.0 indexed

Definitions (4,483)

src/crypto/secp256k1/ecdsa.bend

def verify_len
def verify_with
def verifySEC 1 verification of a 64-byte r || s against a SEC 1 public key (33 or 65 bytes); high s is accepted, as SEC 1 and OpenSSL do
def verify_strictthe same, rejecting s > n / 2 (Bitcoin's BIP 62/146 LOW_S rule, Ethereum's homestead rule for transactions)
def recover_q
def recover_rQ = r^-1 (s R - z G), with R the point of x-coordinate r + n j (j = id / 2) and y parity id mod 2
def recover_x
def cn_fec_n = 2^256 - n and c_p = 2^256 - p as 16-limb field elements
def cp_fe
def rn_fe(r + n) mod p = (r - c_n + 2^256) mod p = (r - c_n + c_p) mod p
def recover_okx = r + j n with j = id / 2.
def recover_sig
def recover_len
def recoverthe 65-byte uncompressed public key that signed the 32-byte hash, from a 65-byte r || s || id with id in 0..3 (go-ethereum's crypto.Ecrecover; Ethereum's precompile passes id = v - 27); None when r or s is not in [1, n - 1], x(R) is not a field element on the curve, or Q is infinity.
def wordlittle-endian U32 words of bytes (a missing byte reads as 0)
def words
def pack
def unpack
def digest_bytes
type HashThe hash of addresses, as a value (only Keccak-256 exists), so that the proofs can keep it folded
def hash
def keccak64the hash of 64 bytes
def eth_if
def eth_go
def eth_with(the key is looked at first, so that the proof checker keeps an unknown address folded)
def eth_addressthe 20-byte Ethereum address of a 65-byte uncompressed public key: the last 20 bytes of Keccak-256 of its 64 coordinate bytes
def zeros_ok
def eth_word
def addr_word
def ecrecover_v
def ecrecover_in
def ecrecoverThe precompile's semantics (Ethereum yellow paper appendix E): the input, zero-padded or cut to 128 bytes, is hash || v || r || s (32 bytes each, big-endian); v must be 27 or 28.

src/crypto/secp256k1/field.bend

def c2^256 - p = 2^32 + 977
def reduce
def small
def zero
def one
def add_u
def add_b
def add
def suba - b = a + (p - b); the first argument is looked at first, so that a constant b is never unfolded while a is unknown
def neg_u
def neg(one argument: nothing to look at first)
def mul_u
def mul_b
def mul
def sq
def pow_stepx^e for the exponent e given by its bits, most significant first
def pow_go
def powx is looked at first, so that on an unknown x nothing is unfolded
def inv_bitsthe bits of p - 2 = 2^256 - 1 - (c + 1): those of c + 1, flipped
def init2
def sqrt_bitsthe bits of (p + 1) / 4: p + 1 = 2^256 - 1 - (c - 2), without its last two bits
def inva^(p - 2): the inverse of a nonzero a, 0 for 0
def sqrta^((p + 1) / 4): a square root of a when a is a square (p = 3 mod 4)
def is_zero
def eq_b
def eq
def paritya mod 2 (the parity of the canonical representative)
def lt_pa < p, for 16 limbs below 2^16
def selectb ?

src/crypto/secp256k1/limbs.bend

def lo16s mod 2^16 and s div 2^16
def hi16
def comp12^16 - 1 - x for x below 2^16
def hd0
def tl
def addlimb-wise sum; the longer tail is kept
def scalevery limb times a
def convthe schoolbook product without carries: conv(x :: xs, ys) = x ys + 2^16 conv(xs, ys)
def take
def drop
def hornerthe value of the limbs (only ever of an empty list at run time: see carry)
def carryA 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).
def compevery limb x becomes 2^16 - 1 - x
def pick1b x + (1 - b) y, limb-wise, for b in {0, 1}
def select
def norm16the normalized form of a value below 2^256: exactly 16 limbs below 2^16
def foldlo + c hi, for x = lo + 2^256 hi: congruent to x modulo m
def rounds
def topthe part of a carried value above 2^256 (0 or 1 below)
def canont (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
def reduce_go
def reducex 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)
def neg_rawm - b = (2^256 - 1 - (b + c)) + 1, for b < m (so b + c < 2^256); no constant but c is ever formed
def ltmx < m, i.e.
def b2n
def borrow1 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
def lt
def nonzeroOR of all limbs being nonzero, without an early exit
def is_zero
def diff
def eq
def bits_ofthe k low bits of x, most significant first
def cbitsevery bit flipped: the bits of 2^k - 1 - x from those of x
def bitsall bits of a limb list, most significant first (16 per limb)

src/crypto/secp256k1/point.bend

type Op
type Point
def nth
def exec
def run_go