bend-osdev-word64
Search uses release 0.1.1.0 · 425 definitions
Definitions (425)
- def trillion10^12 = 0xE8_D4A51000
- def dma / b and a mod b, as decimal text
- def main
- def ns.nd
- def ns.sz
- def ns.tf
- def ns.pred
- def ns.succ_inj
- def ns.double_add
- def ns.add_sub_lek <= n: k + (n - k) = n
- def ns.sub_subk <= n: n - (n - k) = k
- def ns.le_succ_self
- def ns.sub_len - k <= n
- def ns.le_of_not_lt
- def ns.eq_zero
- def ns.lt_one
- def ns.lt_succ_self
- def ns.odd_even1 + 2a = 2b never holds; 2a = 2b gives a = b
- def ns.double_inj
- def ns.lt_dbl
- def ns.lt_dbl1
- def ns.half_le2 * (x / 2) <= x < 2 + 2 * (x / 2)
- def ns.half_lt
- def ns.le_add_mono_r
- def ns.d0z + 2^n * 0 = z
- def ns.dbl_double
- def ns.dkmk <= n: 2^k * 2^(n - k) = 2^n, either way round
- def ns.dmk
- def ns.dnjn <= k: x * 2^k = (x * 2^(k - n)) * 2^n
- def ws.shl
- def ws.shr
- def ws.topcthe bit Word.shl.put(n, c, w) shifts out at the top, and Word.shl's
- def ws.top
- def ws.ovthe bits ws.shl(n, k, w) carries out, as a number
- def ws.wcon_cong
- def ws.putva shift left by one bit, a bit c coming in: the doubled value plus c, less 2^n for the bit shifted out
- def ws.shlvWord.shl: the doubled value, less 2^n for the top bit
- def ws.shlkk shifts left: the value times 2^k, less 2^n times the bits carried out
- def ws.uniqx, y < 2^n and x + 2^n p = y + 2^n q: x = y
- def ws.shr_lek shifts right: the floor of the value divided by 2^k
- def ws.shr_lt
- def ws.or_zero
- def ws.or_disx's value a multiple of 2^k and y's below 2^k: or(x, y) is x + y
- def ws.g1wThe bits a shift left by k carries out are the shift right by n - k: 2^k * w = shl(w, k) + 2^n * shr(w, n - k), and shl(w, k) is 2^k times the remainder of w by 2^(n - k)
- def ws.g1a
- def ws.g1b
- def ws.ea2^k * (lo + 2^n hi) = 2^k lo + 2^n (2^k hi)
- def ws.hb
- def ws.gshl_loa shift left by k < n: the high half takes the low half's top k bits
- def ws.gshl_hia shift left by n <= k: the high half is the low half shifted by k - n, the high half's bits all carried out (and 0, if nothing overflows)
- def ws.gshr_va shift right by k < n: the low half takes the high half's low k bits
- def ws.gshr_lo_le
- def ws.gshr_lo_lt
- def ws.gshr_hi_va shift right by n <= k: the low half is the high half shifted by k - n
- def ws.gshr_hi_le
- def ws.gshr_hi_lt