bend-collections-laws-math

Releases (1)

• 1.0.0.0 indexed

Definitions (5,526)

proofs/math/random/float.bend

• def r52
• def impl_eqthe implementation: shift by 52 - j, exponent field j + 970, for the bit length 1 + j of the significand (j a variable, so no bit length is ever evaluated inside a comparison)
• def hj_ofj <= 52 from the bit length 1 + j <= 53
• def main_g
• def main_j
• def bl_nz
• def main_b
• def main_v
• def mmthe low 53 bits of the source output
• def m_val
• def iz
• def hl_of
• def round0
• def value_z
• def value_s
• def value_c
• def valueTHEOREM (Float64.value)
• def and_f
• def hv_onethe value of the high word of 1.0 without its sign bit: k * 2^20 (k = 1023, kept a variable so no 30-bit constant is ever expanded)
• def below_onea double Bits{l, hw(E, qh)} with E < k <= 2047 is below Bits{0, H} whose high word (without sign) is k * 2^20
• def lt_z_case
• def lt_s_case
• def lt_c
• def lt_oneTHEOREM (Float64.lt_one)

proofs/math/random/fround.bend

• def bits
• def enc_bits
• def rne_c
• def rne_cmp
• def fz
• def fits_add1
• def sub_add_r
• def parq
• def subm
• def rp_c
• def bl_gt
• def bl_c
• def fits_hc
• def succ_le
• def nfit_c
• def nfit
• def lt_fit
• def efv
• def ef2v
• def hi_one
• def f53h
• def top_q
• def pkg_c
• def pkg
• def hsp
• def mod_sh
• def fsub_c
• def fpk
• def le1
• def R_le
• def p2
• def sub_cancel_r
• def lt0f
• def rne_exact
• def rne_shift
• def bl_fit
• def bl_nfit
• def fits_sh
• def bl_shift
• def a1
• def qeq_f
• def qeq_c
• def rs_c
• def round_shift

proofs/math/random/lemire.bend

• def b2n
• def and_false
• def and_ltlo < n and lo < t is lo < t, when t < n
• def hit_accthe hit of an accepted or rejected hi
• def le_pluss <= t + s
• def fin_lt
• def term_lthi < k: rejected or not, x n lies below both thresholds
• def fin_eq
• def term_eqhi == k: x n is below the upper threshold, and below the lower one exactly when it is rejected
• def fin_gt
• def term_gthi > k: x n is at or above both thresholds
• def term_cases
• def termTHEOREM (one output, Lemire's branch): with t = 2^w mod n < n and k 2^w + t <= (k + 1) 2^w, y = x n draws k exactly when k 2^w + t <= y < (k + 1) 2^w
• def cnt_lt#{x < N : x n < c}
• def draw_lemirethe draw is Lemire's when n is not a power of two
• def add4(a + h) + (b + e) == (a + b) + (h + e)
• def sum_lemirethe Lemire outputs below N plus those with x n below the lower threshold are those with x n below the upper one
• def le_succ_lta + 1 <= b is a < b
• def lt_ceilx n < c is x < ceil(c / n) = (c + n - 1) / n, n = 1 + bp
• def min_zero
• def min_succmin(N + 1, C) = min(N, C) + [N < C]
• def cnt_minTHEOREM: #{x < N : x n < c} = min(N, ceil(c / n))
• def dbl_add
• def pmGo's -n % n: 2^w mod n
• def div_add_mul(q n + r) / n = q + r / n
• def min_le
• def lt_add2a <= b and c < d give a + c < b + d
• def cb_leceil((k + 1) 2^w / n) <= 2^w for k < n
• def hab_oft <= 2^w for t < n <= 2^w
• def bm_eq(k + 1) 2^w + m = q n + (t + k 2^w + m), q n + t = 2^w
• def lemire_countTHEOREM (Lemire's branch): floor(2^w / n) outputs draw k
• def cm#{x < N : and_bits(w, x, m) == k}