bend-osdev-word64
Search uses release 0.1.1.0 · 425 definitions
Definitions (425)
- law add_wraps
- law sub_wraps
- law hi_of_parts
- law lo_of_parts
- law shl_crosses_halves
- law shr_crosses_halves
- law mul_of_max_halves(2^32 - 1)^2 = 2^64 - 2^33 + 1
- law show_max
- law show_hex_parts
- law show_hex_zero
- law lo_from_u32For every 32-bit a: from_u32 then lo gives a back.
- law hi_from_partsFor every pair of halves: splitting the joined word gives them back.
- law lo_from_parts
- law from_parts_zero_hiInterface laws: a word whose high half is 0 is the word of its low half, and the word of halves 0 and 0 is zero.
- law from_parts_zero
- law parts_ofInterface law: a word is its two halves joined (for every word).
- law to_nat_partsThe value of a word (for every word): lo + hi * 2^32, the weight 2^32 being 32 doublings (U32Nat.dbl, from bend-osdev-u32).
- law value_eqTwo words with the same value are the same word.
- law cmp_valueComparison is the order of the values (for every pair of words).
- law lt_value
- law le_value
- law eq_value
- law cmp_hi_ltComparison is by the high halves, then the low halves (for dependents that order words through W64.hi and W64.lo).
- law cmp_hi_gt
- law cmp_hi_eq
- law add_wrapAddition, for every pair of words: the sum of the values, less 2^64 when it wraps, which is exactly when the result is below the first operand; and with the sum no more than a word's value, it does not wrap.
- law add_value
- law sub_wrapSubtraction, for every pair of words: the difference plus the subtrahend is the minuend, plus 2^64 when the subtrahend is the larger; when it is not, the difference is the Nat difference.
- law sub_value
- law shl_valueShifts, as Nat facts.
- law shr_value_le
- law shr_value_lt
- law shl_big
- law shr_big
- law and_commThe bits: and, or and xor commute; and + or is the sum of the values, and so is xor + 2 and; with no bit in common (and is 0), or is the sum; not is the subtraction from 2^64 - 1.
- law or_comm
- law xor_comm
- law and_or
- law xor_and
- law or_disjoint
- law not_sub
- law shl_one_wrapA shift left by one bit: twice the value, less 2^64 for the top bit (bit 31 of the high half) going out.
- law divmod_valueDivision (shift and subtract, 64 steps): for b not 0, the quotient and the remainder are the Nat ones, a = q b + r with r < b; by 0, the quotient is 0 and the remainder a.
- law mod_lt
- law div_zero
- law mod_zero
- law show_readsDecimal text: the digits of W64.show(a), read back one by one (Base's Nat.read.go, the reader without Nat.read's 2^48 gate), are the value.