bend-collections-laws-math

Releases (1)

• 1.0.0.0 indexed

Definitions (5,526)

proofs/math/random/uint64n.bend

• def one64
• def q_one
• def add_eq0_r
• def q_nz_c
• def q_nz
• def neg_suma nonzero word and its negation add up to 2^64
• def pm_onepow2mod through a symbolic one (2^64 is never a closed term)
• def thresh_m
• def pred_valuen - 1 for a nonzero n
• def pow2_valuethe power-of-two test is n & (n - 1) == 0
• def mask_valuethe mask is x & (n - 1)
• def m128_lothe halves of the 128-bit product
• def m128_hi
• def contthe specification's bounded draw after a draw of x with state s
• def below_cont
• def fixpoint
• def decLemire's decision of the specification: accept unless lo < 2^64 mod n
• def last_acc
• def pm_lt
• def lt_lowthe implementation's rejection test is the specification's
• def hi_value
• def hd_of
• def step_falseone retry step, accepted
• def step_trueone retry step, rejected: the next draw
• def step_case
• def loopTHEOREM (the rejection loop): f retries from the draw p follow the specification's draws
• def lt_low_n
• def first_falselo >= n: the first draw is accepted by the specification too
• def first_casethe first draw: accepted at once when lo >= n, else the loop
• def mask_pair
• def all1
• def and_true
• def and_all1
• def uand_all
• def zero_pairn == 0 is read as 2^64: the whole word
• def top_first
• def value_nz
• def zero_word
• def value_vn
• def uint64n_valueTHEOREM (Uint64n.value)

proofs/math/random/wrappers.bend

• def v
• def val
• def u32_p
• def uint32_value
• def low63_v
• def i64_p
• def int64_value
• def half_bv
• def shr_halfx >> 1 is half of x
• def i32_p
• def int32_value
• def lo_le
• def nz_word
• def uint32n_lt
• def vv
• def s32
• def n48v
• def fits0
• def fits_shiftx < 2^k gives x 2^a < 2^(a + k)
• def sh8
• def div256
• def mod256
• def byte_v
• def wgothe words of w_go are the low 8k bits, for 8k <= 32
• def skip_vskip(k, n) = n div 2^(8k)
• def nat64_vTHEOREM: nat64(n) denotes n, for n < 2^64
• def n48_p
• def intn_pos
• def intn_lt
• def plus_fst
• def lt_pos
• def int_range_bounds

proofs/math/typed/bgcdnat.bend

• def dvd2
• def Transferevery common divisor of (x, y), given by its quotients, divides u and v
• def into3
• def into2
• def into1
• def into
• def gcd_eq2
• def gcd_eq
• def swap_t
• def gcd_comm
• def sub_t1_at
• def sub_t2_at
• def gcd_sub
• def rec_t2_at
• def gcd_rec
• def odd
• def dmul2q * d = 2 (q d)
• def even_form
• def odd_form
• def odd_eq
• def mod2_bign mod 2 is 0 or 1
• def odd_dvd_ra divisor of an odd number is odd
• def odd2_man odd d dividing 2 m divides m
• def odd2_t1_at
• def odd2_t2_at
• def gcd_odd2a odd: gcd(a, 2 m) = gcd(a, m)
• def iz
• def nstrip_go