bend-collections

Releases (1)

• 1.0.0.0 indexed

Definitions (4,483)

spec/crypto/secp256k1/curve.bend

• def pick_ify = (x^3 + 7)^((p + 1) / 4), then y or p - y to get the wanted parity; no point when that y does not square to x^3 + 7
• def pick_parity
• def decompress_if
• def decompress_y
• def decompress
• def decode_c_if
• def decode_c
• def decode_u
• def decode_lena compressed (33 bytes) or uncompressed (65 bytes) public key; None when malformed, a coordinate is not below p, or the point is not on the curve
• def decode

spec/crypto/secp256k1/ecdsa.bend

• def p
• def n
• def cat
• def fill
• def i2osp32
• def scalar_ok1 <= x < n
• def hash_scalare = bits2int(H) mod n (SEC 1 4.1.3 step 5; RFC 6979 2.3.2)
• type Drbg
• def hmacHMAC-SHA256 (the key is looked at first; the value is HM.hmac's)
• def update_v
• def updateK = HMAC_K(V || tag || seed), V = HMAC_K(V)
• def update2
• def drbg_initsteps b-g, with seed = int2octets(x) || bits2octets(h1)
• type Attempt
• def flip0 or 1 when b is
• def low
• def ge2
• def finish_if
• def finishR = (x, y) = [k] G, r = x mod n, s = k^-1 (e + r d) mod n; r = 0 or s = 0 means another k.
• def attempt_ok
• def attemptstep h.3: k = bits2int(T) with T = V, used when 1 <= k < n
• def sign_loopstep h, with the retry of step h.3 (K = HMAC_K(V || 0x00), V = HMAC_K(V)) before the next V = HMAC_K(V); at most `fuel` candidates
• def sign_drbg
• def sign_d
• def signsign(sk, H): d = OS2IP(sk) must be a 32-byte key with 1 <= d < n, H 32 bytes
• def pk_of
• def public_d
• def public_keythe SEC 1 encoding of Q = [d] G
• def verify_rsu1 = e s^-1, u2 = r s^-1, R = [u1] G + [u2] Q; valid when R is not the point at infinity and x(R) mod n = r
• def verify_ok
• def verify_qr and s in [1, n - 1]; strict verification also rejects s > n / 2
• def verify_len
• def verifyverify(Q, H, r || s): Q a SEC 1 public key, H 32 bytes, r || s 64 bytes
• def recover_q_if
• def recover_q
• def recover_rQ = r^-1 (s R - e G) = [-e r^-1] G + [s r^-1] R
• def recover_x_ifR: the point of x-coordinate x = r + j n (j = id / 2, x < p) whose y has parity id mod 2
• def recover_x
• def recover_ok
• def recover_len
• def recoverthe 65-byte uncompressed key recovered from H (32 bytes) and r || s || id (65 bytes, id in 0..3)
• def wordKeccak-256 (spec/crypto/keccak/main.bend) of bytes packed into little-endian U32 words, as its interface takes them
• def words
• def pack
• def unpack
• def digest_bytes
• type HashThe hash of addresses: Keccak-256 (spec/crypto/keccak/main.bend, 24 rounds), named by a value so that the proofs can keep it folded
• def hash
• def keccak64
• def eth_ifaddress = the last 20 bytes of Keccak-256(x || y) of an uncompressed key
• def eth_go
• def eth_with(the key is looked at first, so that the proof checker keeps an unknown address folded)
• def eth_address
• def word_of
• def addr_word
• def all_zero
• def ecrecover_v
• def ecrecover_in
• def ecrecoverECRECOVER (precompile 0x01): the input zero-padded or cut to 128 bytes is H || v || r || s, v a 32-byte big-endian word that must be 27 or 28; the output is the address word (12 zero bytes, then the address) of the key recovered with id v - 27, or nothing

spec/crypto/secp256k1/field.bend

• def digitsa number from its little-endian radix-2^16 digits, each scaled by one: digits(1, [d0, d1, ...]) = d0 + 2^16 d1 + ...
• def w2562^256
• def cp2^256 - p = 2^32 + 977, and p
• def prime
• def cn2^256 - n = 432420386565659656852420866390673177327, and n
• def order
• def madd
• def msuba - b mod m
• def mneg
• def mmul
• def mpow
• def minva^(m - 2): for a prime m the inverse of a nonzero a (Fermat); 0 for 0
• def fsqrta^((p + 1) / 4): a square root of a whenever a is a square mod p (p = 3 mod 4)
• def valuethe value of little-endian radix-2^16 limbs
• def limbs16exactly 16 limbs, each below 2^16
• def reduceda reduced element mod m: 16 limbs below 2^16 of value below m

spec/crypto/secp256k1/schnorr.bend

• def p
• def n
• def cat
• def bytes32
• def tagged_h
• def taggedhash_name(x) = SHA256(SHA256(name) || SHA256(name) || x), name in ASCII
• def tag_aux"BIP0340/aux", "BIP0340/nonce", "BIP0340/challenge"
• def tag_nonce
• def tag_challenge
• def xor_bytes
• def even_bn - x when y is odd (the key or nonce whose point has even y)
• def even
• def lift_iflift_x(x): the point with x-coordinate x and even y, if x < p and x^3 + 7 is a square
• def lift_x
• def check_rfail if is_infinite(R) or not has_even_y(R) or x(R) != r