bend-collections-laws-math

Releases (1)

• 1.0.0.0 indexed

Definitions (5,526)

proofs/lib/two_list.bend

• def len_rev

proofs/lib/u32.bend

• def to_nat_word
• def pow2_scale
• def double_pow
• def pow2_pow
• def word_from_unsignedEvery word is recovered from its unsigned interpretation (reconstruct at 0).
• def injective
• def pow2_le_pow
• def pow2_le_scale
• def from_nat_value_kWidth-generic wrappers: bounds are 2^k with k <= n, never a closed 2^32.
• def shl_exact_k
• def inc_fromone increment over an abstract width (the checker never expands a literal-width word here)
• def from_nat_stepthe U32 step over abstract words a (for p) and b (for p + 1)
• def from_nat_word
• def to_nat_from_nat
• def is_lt_nat
• def sub_nat
• def WB_unsigned
• def shl_bound
• def shl_value
• def pad_value
• def low_bit
• def shr_split
• def pow2u2^d as the U32 built by Base Array.size (1, then shl per level).
• def pow2u_shl_bound
• def pow2u_value
• def shr_pow2u
• def and_true
• def lt_one_zero
• def and_low_prev
• def and_low_hy
• def and_low_hyb
• def and_low_hx
• def and_low_hxb
• def and_low_step
• def and_low
• def mask_hx
• def mask_word
• def one_le_pow2uBase Array masks every index with size - 1; below the size this is the identity.
• def mask_pow2u
• def u32_cmp
• def fin_refl
• def cmp_refl_eq
• def u32_eq_refl

proofs/lib/u32alg.bend

• def sc
• def uw
• def cy
• def add_cancel_r
• def add_rot(a + b) + c == (a + c) + b
• def sc_zero
• def sc_add
• def le_shiftM <= r + (M + s)
• def sc_succ
• def uniq_gapr1 < 2^n cannot equal r2 + 2^n (1 + q).
• def uniqr1 + 2^n x == r2 + 2^n y with r1, r2 < 2^n forces r1 == r2.
• def w_inj
• def cons
• def uw_zero
• def w_zero_add
• def w_assoc
• def adc_con_not
• def adc_notSubtraction is addition of the complement with an incoming carry.
• def not_value1 + unsigned(not b) + unsigned(b) == 2^n
• def cons_sub
• def arith_sub(a + b) - a == b
• def w_add_sub(v - a) + a == v
• def w_sub_add(v - a) + a == v
• def shl_adcDoubling by shifting: shl.put n c w == w + w + c.
• def w_shl
• def assoc
• def comm
• def zero_add
• def add_zero
• def add_sub
• def sub_add
• def shl_add
• def swapa + (b + c) == b + (a + c)
• def eq_of
• def eq_refl
• def eq_true

proofs/lib/u32div.bend

• def v
• def dq
• def dr
• def invthe long-division invariant of a partial result r for the prefix a
• def digit_onea subtracting digit: (1 + 2q) b + d == a + 2 (q b + r) when b + d == a + 2 r
• def digit_zeroa zero digit: 2q b + (a + 2 r) == a + 2 (q b + r)
• def vw
• def vb
• def sub32
• def fin_true
• def fin_ge
• def fin_lt
• def fin_false
• def shl_ts
• def shl_ok
• def rec_ok
• def go_okthe invariant holds for every prefix of the dividend
• def pos_nat
• def pos
• def dm_fin