bend-collections

Releases (1)

• 1.0.0.0 indexed

Definitions (4,483)

src/crypto/chacha/chacha20.bend

• def words
• def at
• def key_words
• def nonce_words
• def key
• def nonce
• def state
• def keystreamThe 64 keystream bytes of block `counter`, with r double rounds.
• def xor_frontXOR the keystream onto the front of xs, as far as both go.
• def skip
• def streamBlocks of 64 bytes, block j under counter + j; fuel bounds the number of blocks (the length of xs is enough).
• def encrypt_rounds
• def block_body
• def block_roundsThe block function entered through a match on the key's first cell: both arms are block_body; with a symbolic key the proof checker leaves the call unevaluated instead of unrolling the rounds when it compares types.
• def hstate
• def hchacha_body
• def hchacha_rounds
• def hchacha20_unchecked
• def take
• def xencrypt_uncheckedXChaCha20: ChaCha20 under the HChaCha20 subkey of nonce[0..16], with the nonce 0x00000000 || nonce[16..24].
• def has_length
• def valid
• def when
• def chacha20_blockchacha20_block(key, counter, nonce): 64 bytes, or None unless the key has 32 bytes and the nonce 12.
• def chacha20chacha20_encrypt(key, counter, nonce, plaintext) (encryption and decryption are the same operation).
• def hchacha20HChaCha20(key, nonce): the 32-byte subkey, or None unless 32 and 16 bytes.
• def xchacha20XChaCha20 with a 24-byte nonce.

src/crypto/chacha/core.bend

• type State
• def double_roundOne double round: QUARTERROUND on the columns (0,4,8,12) ..
• def roundsn double rounds (2n rounds).
• def addWord-wise sum of two states (the feed-forward).
• def blockThe block function with n double rounds: the rounds, then the input added.
• def initThe ChaCha20 input state: constants, key, block counter, nonce.
• def hinitThe HChaCha20 input state: constants, key, the four words of the 16-byte nonce.
• def bytesThe 64 little-endian bytes of a state.
• def hbytesHChaCha20's output: the little-endian bytes of words 0..3 and 12..15.

src/crypto/curve25519/field.bend

• def addllimbwise sum; the longer tail is kept
• def scalevery limb times a
• def convthe product polynomial: conv(x :: xs, ys) = x ys + 2^8 conv(xs, ys)
• def take
• def drop
• type Crlimbs and the carry out of the top one
• def cr_limbs
• def cr_out
• def carry_con
• def carryone carry pass: limbs below 2^8 and the carry out of the top limb
• def add0add k to the lowest limb
• def pass_fincarry, then fold the carry out back in: 2^256 == 38 (mod p)
• def pass
• def reduce32 limbs below 2^27 to a tight element of the same value mod p
• def zero
• def one
• def smalla small constant k < 2^8 as an element
• def eight_p8p limbwise: every limb at least 2^10 - 8, so a + 8p - b never borrows
• def comp_p2^256 - p = 2^255 + 19
• def subla + k - b limbwise
• def add
• def sub
• def widefold the product: low 32 limbs + 38 * high limbs
• def mul
• def sq
• def mul_smalla * k for a constant k < 2^17
• def neg
• def selects == 0: a; s == 1: b; limbwise a * (1 - s) + b * s
• def pow_onesacc^(2^n) * x^(2^n - 1): n steps of acc = acc^2 * x
• def pow_bitone bit of a public exponent, most significant first: acc^2 (* x)
• def pow_bits
• def invx^(p - 2) = x^(2^255 - 21): 250 one bits (x, then 249 steps), then 0 1 0 1 1
• def pow_p58x^((p - 5) / 8) = x^(2^252 - 3): 250 one bits, then 0 1
• def csub_fin
• def csubx - p when x >= p, else x (x tight): x + 2^256 - p carries out iff x >= p
• def freezethe canonical representative, below p: 2^256 < 3p
• def to_bytesthe 32-byte little-endian encoding of a canonical element is its limbs
• def mask_topthe last byte with its top bit cleared (RFC 7748 decodeUCoordinate)
• def of_bytesbytes to an element, bit 255 ignored
• def sum_allthe sum of the limbs (below 2^13 for 32 bytes); no early exit
• def is_zerox == 0 in the field: every byte of the canonical form is 0
• def eqa == b in the field
• def low_bitthe parity of the canonical representative (RFC 8032 x_0)
• def parity

src/crypto/curve25519/x25519.bend

• type St
• def kbitbit t of a little-endian byte string
• def clamp_topRFC 7748 decodeScalar25519's clamping: k[0] &= 248, k[31] &= 127, k[31] |= 64
• def clamp
• def a24a24 = 121665 as a field element
• def stepone ladder step on the swapped pair (x2 : z2), (x3 : z3); c24 is a24
• def rungswap ^= k_t; cswap; the step; swap = k_t
• def lenthe ladder's bit count, 8 len(k) - 1: 255 for a 32-byte scalar (RFC 7748 `bits`).
• def bitlen8 len(xs), the bit count of a byte string
• def nbits
• def ladderbits t = n - 1 down to 0
• def finishthe final cswap, then x2 * z2^(p - 2), encoded
• def x25519_rawX25519 on two 32-byte strings of bytes below 256
• def valid_bytes32 values, each below 256
• def x25519_if
• def x25519X25519(k, u); None unless both are 32 bytes below 256
• def basethe base point u = 9

src/crypto/ed25519/ed25519.bend

• def cat
• def hramk = SHA-512(R || A || M) mod L
• def secretthe secret scalar s (pruned lower half of SHA-512(seed)) and the prefix