bend-osdev-algo

Releases (1)

• 0.1.0.0 indexed

Definitions (367)

proof_bsearch.bend

• def bq.add_sub
• def bq.sub_cancel
• def bq.sub_pos
• def bq.sub_le0
• def bq.sub0_le
• def bq.sub_step
• def bq.half_le
• def bq.half_lt
• def bq.half_lt_pws < 2p: s / 2 < p
• def bq.hr_lt_pws < 2p: s - (1 + s / 2) < p
• def bq.get_take
• def bq.get_nth
• def bq.len_take
• def bq.get_len

proof_u32.bend

• def uq.pw2^n
• def uq.halfn / 2, rounded down
• def uq.bvthe value of a word's lowest bit and the rest
• def uq.bt
• def uq.ft
• def uq.tf
• def uq.succ_cong
• def uq.double_cong
• def uq.add_zero
• def uq.add_succ
• def uq.add_comm
• def uq.double_add
• def uq.sub_add_l
• def uq.sub_add
• def uq.le_succ
• def uq.lt_dbl
• def uq.lt_dbl1
• def uq.lt_rw
• def uq.val_lt
• def uq.lt_succ_r
• def uq.le_lt_trans
• def uq.lt_dbl_self
• def uq.lt_succ_pwx < 2^f: x2 < 2^g, for x == x2 and g == 1 + f (stated so that a fixed g, such as the search's 33, is never expanded)
• def uq.nc
• def uq.cb
• def uq.fin_le_ff
• def uq.fin_le_tf
• def uq.fin_le_ft
• def uq.le_bits
• def uq.ha
• def uq.hb
• def uq.hc
• def uq.alg2
• def uq.alg4
• def uq.alg6
• def uq.sub_wfor b <= a (b < a when the carry in c is False): a = adc(a, b, True, c) + (1 - c) + b
• def uq.u32_sub
• def uq.cv
• def uq.hk0the bound for the bits above the lowest, from the bound for the word
• def uq.hk1
• def uq.hk2
• def uq.hk3
• def uq.add_wc + a + b < 2^n: adc(a, b, False, c) is c + a + b
• def uq.add_wzthe bound given by a word's value, so that 2^n is never expanded
• def uq.u32_adda + b <= c: U32.add(a, b) is a + b
• def uq.inc_w
• def uq.inc_wz
• def uq.u32_inc1 + a <= c: U32.inc(a) is 1 + a
• def uq.half_dbl
• def uq.half_dbl1
• def uq.padpadding a word with a zero top bit keeps its value
• def uq.shr_w
• def uq.u32_shr