bend-collections-laws-math

Releases (1)

• 1.0.0.0 indexed

Definitions (5,526)

proofs/math/number/proof.bend

• def u64_overflowing_mul_flag
• def u64_overflowing_pow_value
• def u64_overflowing_pow_flag
• def u64_overflowing_shl_value
• def u64_overflowing_shl_flag
• def u64_overflowing_shr_value
• def u64_overflowing_shr_flag
• def u64_bit_count
• def u64_to_bytes_le
• def u64_to_bytes_be
• def u64_from_bytes_le
• def u64_from_bytes_be

proofs/math/pow2/pow2.bend

• def go_double
• def same

proofs/math/proof.bend

• def u32_divU32 long division (Base's U32.div / U32.mod), every nonzero divisor
• def u32_mod
• def u64_is_zerou64
• def u64_le_signed
• def u64_add
• def u64_add_modular
• def u64_neg
• def u64_div_small
• def u64_div_small_signed
• def u64_milliseconds
• def hash_bucket_lehash
• def hash_bucket_lt
• def pow2pow2

proofs/math/random/below.bend

• def and_lex & m <= m
• def high_lt_cx < 2^64 and n > 0: floor(x n / 2^64) < n
• def lt_plusa < n + a for n > 0
• def prod_ltx < 2^64: x n < 2^64 n
• def high_ltx < 2^64 and n > 0: floor(x n / 2^64) < n
• def pfst
• def some_or
• def is_some
• def none_some
• def some_inj
• def acc_lt
• def draw_pos_lt
• def draw_ltTHEOREM: an accepted draw is below n
• def go_ltthe bounded draw after a draw of x is below n > 0
• def below_ltTHEOREM: the bounded draw from any source is below n > 0

proofs/math/random/bits.bend

• def bv
• def and_stepone bit and the rest: (b + 2a) & (c + 2d) = b c + 2 (a & d)
• def bv_le
• def bv_and
• def to_nat_cona word's value, its low bit first
• def wandTHEOREM: Word.and is and_bits on the values
• def uand
• def and_joinTHEOREM: and on two limbs, (a1 + 2^k b1) & (a2 + 2^k b2) = a1 & a2 + 2^k (b1 & b2)
• def and64_valueTHEOREM: the 64-bit and of rand.bend is and_bits on the values

proofs/math/random/bounded.bend

• def fst_val
• def nz_pos
• def uint64n_lt

proofs/math/random/chacha8/block.bend

• def drsn double rounds, the model of the implementation's dr(dr(dr(dr(x))))
• def drs_correct
• def rounds_correctthe eight rounds on the initial state
• def block_correctTHEOREM: the implementation's block is C2SP's block ctr
• def group_correctTHEOREM: the implementation's group is C2SP's four permuted blocks ctr ..

proofs/math/random/chacha8/rounds.bend

• def vecthe state as the RFC list x[0..15]; like S.key_list on a key, it is stuck on an abstract state, so the checker never unfolds rounds of symbolic words it does not have to compare
• def dr_correctone double round is RFC 8439's inner_block
• def init_correct
• def cancelx + c - c = x
• def finish_correctthe key words added back, C2SP's subtractions of the constants and the counter, and the zero nonce words: the words the implementation keeps
• def interleave_correctthe interleaving is C2SP's permutation read as little-endian 64-bit words

proofs/math/random/chacha8/seed.bend

• def bytes_eq
• def seeded_ok
• def seeded_c
• def seededTHEOREM (ChaCha8.seeded)

proofs/math/random/chacha8/stream.bend

• def app
• def drop64
• def restthe outputs of the current iteration after the groups already produced
• def nkthe key of the iteration after them
• def gw
• def invthe invariant: from state C{k, p, buf} the generator outputs buf, the rest of the iteration keyed by k, then C2SP's stream from the next key
• def streamTHEOREM: the generator keyed by k outputs C2SP's ChaCha8Rand stream keyed by k's eight words, for every key and every number of outputs

proofs/math/random/float.bend

• def v
• def sub6363 - j = 11 + (52 - j)
• def shift_amtthe shift of the implementation: clz - 11 = 52 - j
• def exp_amt0the exponent field of the implementation: 1033 - clz = 970 + j
• def exp_amt
• def fits0
• def fits_up
• def fits_shiftx < 2^k gives x 2^a < 2^(a + k)
• def fits_lt11
• def hwthe high word the implementation builds: exponent field e, and the top 20 fraction bits of qh
• def bits
• def f12
• def hw_valueits value: 2^20 e + (qh mod 2^20), for e < 2^11
• def value_eta
• def encthe implementation's bits are encode(False, e, q mod 2^52) for the value q < 2^53 of the shifted significand
• def bl_le
• def x0
• def max_l
• def sub_add53
• def exX + r = 2947 for X = j + 2895, r = 52 - j
• def round_qround(q, X) for 2^52 <= q < 2^53 at the scale X = j + 2895 is pack(q, X)
• def pack_qpack(q, X) is the pattern with exponent field j + 970 and fraction q mod 2^52
• def Jthe bit length of 1 + np is 1 + J(np)
• def j52