bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

def pp = 2^130 - 5
def foldx = lo + 2^130 hi is congruent to lo + 5 hi mod p (2^130 = p + 5); the fold strictly decreases x while hi > 0, so x folds bring x below 2^130.
def folds
def pick
def canony < 2^130: y itself when y < p, else y - p = (y + 5) - 2^130.
def modpx mod p
def le_numle_bytes_to_num
def le_bytesnum_to_n_le_bytes: the low n bytes of x.
def prefix
def suffix
def clamp_maskclamp(r): r &= 0x0ffffffc0ffffffc0ffffffc0fffffff, i.e.
def clamp_from
def clamp
def blocksThe message cut into 16-byte blocks, the last one possibly shorter; fuel bounds the number of blocks (the length of the message is enough).
def absorbfor each block: n = le_bytes_to_num(block | [0x01]); a += n; a = (r * a) % p
def poly1305_macpoly1305_mac(msg, key): r = clamp(key[0..16]), s = key[16..32]; a = 0, absorb every block, a += s; the tag is num_to_16_le_bytes(a).
def macThe same function, split on the message first so that a proof about an unknown message does not unfold it.
def coeffRFC 8439 2.5 describes the accumulator as the evaluation, at r and modulo p, of the polynomial whose coefficients are the blocks (each with its 0x01 byte): with q blocks n_1 ..
def poly

type SPoint
type SOp
def nth
def exec
def run_gorun a program: each instruction appends its result as a new register
def run(the first register is looked at first; the result is run_go's)
def add_progRCB Algorithm 7 (a = 0).
def dbl_progRCB Algorithm 9 (a = 0).
def b3
def add_out
def padd
def dbl_out
def pdbl
def infinity
def is_inf
def bitbit i of k
def step
def bits_gobits i - 1, ..., 0 of k, most significant first (k is looked at first, so that on an unknown k nothing is unfolded)
def bits
def lmulleft-to-right double-and-add: for each bit b, R = 2 R, then R = R + A when b is set
def pmul[k] A for 0 <= k < 2^256
def gG (SEC 2), with z = 1
type SAffine
def aff_z
def to_affine(X / Z, Y / Z), (0, 0) for the point at infinity
def aff_x
def aff_y
def rhsx^3 + 7
def on_curve
def byte
def os2ip_goOS2IP (big-endian)
def os2ip
def i2osp_leI2OSP: the n low bytes of x, big-endian
def i2osp_go
def i2osp(x is looked at first, so that on an unknown x nothing is unfolded)
def length_is
def first
def after
def head
def enc_c
def encode_compressedcompressed: 02 or 03 (the parity of y), then x
def enc_u
def encode_uncompresseduncompressed: 04, x, y