lawful-words

Releases (1)

• 0.1.0.0 indexed

Definitions (468)

proof_word.bend

• law wltEvery word stands for a number below 2^n.
• law carry_modr + c * m = x with r < m gives x % m = r.
• law cmp_dbl
• law wcmpWords compare as their numbers.
• def Cmp.disc_eq
• def lt_ne_eq
• def gt_ne_eq
• def bool_cmp_eq
• def word_fin_t
• def word_fin_b
• def word_cmp_eq
• law winjTwo words that stand for the same number are the same word.
• def inccThe carry out of Word.inc: set when every bit is set.
• law winc
• def coutThe carry out of Word.adc without inversion (f = False).
• law adc_stepOne bit of the sum, as numbers.
• law wadcThe sum with its carry out: r + co * 2^n = c + a + b.
• def adc_t.conSubtraction is addition of the complement with carry in.
• law adc_t
• law wnotnot w and w add up to 2^n - 1.
• law wsub_val(a + 2^n) - b = 1 + a + not b.
• def stopThe bit shifted out of the top by Word.shl.put.
• law wput
• def shtopThe bit shifted out of the top by Word.shl.
• law wshl
• law wshl_mod
• law wpad
• law wdiv2
• law wshr
• law wadd_mod
• law modmulin
• law wmul_go
• def wbitBit k of a word (False from n up).
• law is_eq_bn
• law wbit_numThe numeric bit (as in D.bit) is the word's bit.
• law wbit_and
• law wbit_or
• law wbit_xor
• law wbit_not
• def wdiffThe lowest bit where two words differ (0 if they are equal).
• law wextTwo words with the same bit where they would first differ are equal.
• law moddbl_w
• law lt_w
• law mask_step
• law and_maskAnd with a word standing for 2^k - 1 keeps the low k bits.
• law lt_onex < 1 gives x = 0.
• law or_zero
• law xor_zero
• law split_stepy + 2r = 2a + (y + 2b) when r = a + b.
• def or_split.s
• law or_splitOr of a word with only bits from k up and a word below 2^k is their sum.
• def xor_split.s
• law xor_splitXor likewise.

proof_zb.bend

• def allzAll bits clear.
• def app8Eight bits x in front of r.
• def one8
• def h8
• def ones8
• def zfThe zero-byte flags of v with subtrahend k, flag mask h and carry in c.
• law allz_cmp
• law allz_andz
• law zb_byteOne byte of the zero-byte test, with no borrow in.
• law allz_maskA byte masked with 255.
• law zb_zero
• def zb_ne0
• def zb_ne1
• def zb_ne2
• def zb_ne3