lawful-words

Releases (1)

• 0.1.0.0 indexed

Definitions (468)

defs.bend

• def two322^32, for prose and tests.
• def wrapn modulo 2^32: the number U32.from_nat(n) stands for (the laws write Nat.mod(n, Nat.pow(2n, 32n)) inline, for the same reason).
• def bitBit k of a word (bit 0 is the lowest; every bit from 32 up is 0).
• def byteByte j of a word (byte 0 is the lowest): (w >> 8j) & 255.
• def put_bytew with byte j replaced by b: (w & ~(255 << 8j)) | (b << 8j).
• def pack4The word whose bytes 0 to 3 are b0 to b3: b0 | b1 << 8 | b2 << 16 | b3 << 24.
• def nth4The j-th of four values (j = 0 to 3; b3 from 3 up).
• def mergeThe word that starts r bytes into the pair (lo, hi), r from 0 to 4: (lo >> 8r) | (hi << 8(4 - r)).
• def zbThe zero-byte flags: (v - 0x01010101) & ~v & 0x80808080.
• def bcastA byte repeated in all four bytes: searching for b is searching xor(w, bcast(b)) for a zero byte.

LAWS.bend

• law to_nat_ltEvery word stands for a number below 2^32.
• law to_nat_injTwo words that stand for the same number are the same word.
• law from_nat_to_nat
• law to_nat_from_nat
• law wrap_smallA number below 2^32 is unchanged by wrapping.
• law cmp_to_natWords compare as their numbers; every U32.is_* test follows from this one.
• law is_eq_to_nat
• law is_lt_to_nat
• law is_le_to_nat
• law is_gt_to_nat
• law is_ge_to_nat
• law is_ne_to_nat
• law is_zero_to_nat
• law is_zero_xorTwo words are equal exactly when their xor is zero.
• law is_eq_trueA passed equality test gives equal words.
• law to_nat_inc
• law to_nat_add
• law to_nat_suba - b wraps: it is a + 2^32 - b, modulo 2^32.
• law to_nat_mul
• law from_nat_add
• law from_nat_mul
• law to_nat_inc_ltA counter below some word steps up by exactly one.
• law to_nat_add_fits
• law to_nat_sub_le
• law to_nat_mul_fits
• law to_nat_divAs in Base, dividing by 0 gives 0 and the remainder is a; so does Nat.
• law to_nat_mod
• law to_nat_min
• law to_nat_max
• law to_nat_shr
• law to_nat_shl
• law to_nat_shrn
• law to_nat_shln
• law to_nat_shln_fits
• law to_nat_shln_modA left shift by k leaves the low k bits zero.
• law to_nat_shrn_ltA right shift by k leaves a number below 2^(32-k) (below 1 from k = 32 up).
• law to_nat_splitA word splits into its high part (a >> k) and its low k bits (a & m).
• law shrn_lt_wordsAn index below 2^k * w words-worth has its word index below w.
• law to_nat_and_maskAnd with a mask of the low k bits takes the number modulo 2^k.
• law to_nat_not
• law to_nat_or_splitOr of a word with only bits from k up and a word below 2^k is their sum (no bit in common).
• law to_nat_xor_split
• law bit_and
• law bit_or
• law bit_xor
• law bit_notnot flips the 32 bits, and only those.
• law bit_extTwo words with the same bits are the same word.
• law to_nat_byte
• law byte_put_sameByte j of a word whose byte j was set to b (below 256) is b.
• law byte_put_otherSetting byte j leaves every other byte as it was (from j = 4 up, put_byte changes nothing).
• law to_nat_pack4The number a packed word stands for.
• law byte_pack4Unpacking a packed word gives its bytes back.
• law pack4_bytesPacking a word's four bytes gives the word back.
• law byte_extTwo words with the same four bytes are the same word.
• law byte_andBitwise operations work byte by byte.
• law byte_or
• law byte_xor
• law byte_not
• law byte_shrnShifting by whole bytes moves bytes.
• law byte_shln_high
• law byte_shln_low
• law byte_merge_loA word read r bytes into the pair (lo, hi): bytes r..
• law byte_merge_hi
• law zb_zeroThe zero-byte test: zb(v) is zero exactly when no byte of v is zero.
• law byte_ltEvery byte is below 256.
• law nat_mod_lt
• law nat_mod_small
• law nat_div_small
• law nat_div_moda = (a / b) * b + a % b (also for b = 0: a / 0 = 0 and a % 0 = a).
• law nat_pow_add
• law nat_div_divDividing by 2^j then by 2^k is dividing by 2^(j+k).
• law nat_add_comm
• law nat_add_assoc
• law nat_mul_comm
• law nat_mul_assoc
• law nat_mul_add
• law nat_lt_le_trans
• law nat_le_trans
• law nat_div_lta < b * c with b > 0 gives a / b < c.
• law nat_div_mul_add(q * b + r) / b = q and (q * b + r) % b = r, for r < b.
• law nat_mod_mul_add
• law nat_mul_mod
• law nat_mod_mod_pow(a % 2^m) % 2^k = a % 2^k for k <= m.

proof_bytes.bend

• law and_comm
• law band_permand(a, and(b, and(c, d))) = and(b, and(a, d)) when a implies c.
• law bimpand(l, and(i, x)) = and(l, x) when l implies i.
• law lt_succ_self
• law bit_zero_divA word below 2^k has bit k clear.
• law bit_lt_pow
• law bit_ge32