bend-kit-lemmas
Releases (2)
Definitions (45)
lemmas.bend
- def pow22^n, by the doubling that Word.to_nat uses.
- def bitThe value of a word whose low bit is x and whose upper bits have value t.
- law to_nat_con
- law cmp_bit
- law word_cmp_natComparing two words compares their values.
- law u32_cmp_nat
- law u32_is_lt_nat
- law u32_is_le_nat
- law u32_is_eq_nat
- law odd_lt_double
- law word_to_nat_ltA word of n bits has a value below 2^n.
- law u32_to_nat_word
- law u32_to_nat_lt
- law double_inj
- law double_ne_odd
- law word_to_nat_injTwo words with the same value are the same word.
- law u32_to_nat_inj
- def b2n
- def scalem when q is set, else 0.
- def majThe carry out of a full adder: set when two or three of the bits are set.
- def carryThe carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.
- law scale_double
- law adc_stepOne bit of the adder: s + 2k is the sum c + x + y of the three input bits.
- law word_adc_natThe adder is exact: the word sum plus the carry-out weight 2^n is c + a + b.
- law lt_rwMoves a strict upper bound across an equation without a conversion check.
- law add_no_carry
- law add_mod_carry
- law word_add_natAddition without overflow is exact.
- law word_add_modAddition wraps modulo 2^n.
- law u32_add_word
- law u32_add_nat
- law u32_add_mod
- law word_not_natThe bitwise complement of w has value 2^n - 1 - w.
- law word_sub_notSubtraction is addition of the complement with a carry in.
- law sub_arith
- law sub_fin
- law word_sub_natSubtraction without wrap is exact.
- law u32_sub_nat
- law lt_of_double_lt
- law word_inc_natIncrementing without overflow adds one.
- law u32_inc_nat
- law u32_to_from_nat
- law u32_from_to_nat
- law and_le_sub
- law u32_fits_natThe overflow-safe bounds check n <= len and i <= len - n holds exactly when i + n <= len.