bend-osdev-word64

Releases (2)

• 0.1.1.0 indexed
• 0.1.0.0 unindexed

Definitions (425)

proof_value.bend

• def wn.succ_cong
• def wn.add_swap(a + b) + c = (a + c) + b
• def wn.swap_mid(a + b) + (c + d) = (a + c) + (b + d)
• def wn.sub_add_l
• def wn.sub_add
• def wn.lt_rw
• def wn.lt_rw2
• def wn.le_rw
• def wn.le_succ
• def wn.le_zero
• def wn.not_lt_zero
• def wn.lt_le
• def wn.le_rw2
• def wn.lt_irrefl
• def wn.lt_add_lk + x < k + y, k + x <= k + y, cmp(k + x, k + y): as for x and y
• def wn.le_add_l
• def wn.cmp_add_l
• def wn.lt_add_r
• def wn.add_lt_monoa < b and c < d: a + c < b + d
• def wn.not_lt_adda + b < a never holds, nor s + b < b
• def wn.not_lt_add_l
• def wn.le_not_lt
• def wn.lt_of
• def wn.cmp_gt
• def wn.cmp_eq
• def wn.cmp_refl
• def wv.Vlo + 2^n * hi
• def wv.Qx * 2^(2n), the weight of a carry out of the high half
• def wv.lexthe order of two halves: the high halves, then the low halves
• def wv.bitwa carry as a word: 1 or 0
• def wv.bitw_value
• def wv.q0
• def wv.qsQ(1 + x) = Q(1) + Q(x)
• def wv.val_lt2lo < 2^n and hi < 2^n: lo + 2^n * hi < 2^(2n)
• def wv.ncmp0
• def wv.nltal < 2^n <= bl + 2^n * (1 + q)
• def wv.ncmp
• def wv.gcmp
• def wv.lex_eq_l
• def wv.lex_eq_r
• def wv.halves_eqequal values: equal halves
• def wv.q_two
• def wv.char_add
• def wv.char_sub
• def wv.nowrap
• def wv.pre(l + 2^n h) + 2^n z = l + 2^n (h + z)
• def wv.tail
• def wv.nadd
• def wv.nsubSubtraction: the halves with their borrows put together
• def wv.c1add
• def wv.addhi
• def wv.c1sub
• def wv.subhi
• def wv.gadd.gothe value of the sum of two words of two halves, with its carry out
• def wv.gadd.sum
• def wv.gsub.go
• def wv.gsub.sum
• def wv.gaddW64.add at width n: the sum of the values, less 2^(2n) when it wraps, which is when the result is below the first operand
• def wv.gadd_nowrapwith the sum no more than another word's value, nothing wraps
• def wv.gsubW64.sub at width n: the difference plus the subtrahend is the minuend, plus 2^(2n) when the subtrahend is the larger

word64.bend

• type W64
• def W64.zero
• def W64.one
• def W64.max
• def W64.from_u32
• def W64.bits.loSplitting a Word(m + n) into its low m and high n bits (bits are stored least significant first), and joining them back.
• def W64.bits.hi
• def W64.bits.cat
• def W64.lothe low 32 bits
• def W64.hithe high 32 bits
• def W64.from_partsthe word whose high and low 32 bits are hi and lo
• def W64.two322^32, built from literals Bend reads (a literal is at most 2^32 - 1)
• def W64.dblx * 2^n: x doubled n times
• def W64.to_natlo + hi * 2^32.
• def W64.from_nat.pair
• def W64.from_natk mod 2^64
• def W64.bit
• def W64.sel
• def W64.add.go
• def W64.add
• def W64.sub
• def W64.mulhi.gothe high 32 bits of the 64-bit product of two 32-bit words, from their 16-bit halves (every partial product fits in 32 bits)
• def W64.mulhi
• def W64.mul
• def W64.and
• def W64.or
• def W64.xor
• def W64.not
• def W64.shl.pickshifts by k bits: 0 leaves the word, 64 or more gives 0
• def W64.shl
• def W64.shr.pick
• def W64.shr
• def W64.cmp.pick
• def W64.cmp
• def W64.is_eq
• def W64.is_lt
• def W64.is_le
• def W64.is_gt
• def W64.is_ge
• def W64.is_zero