bend-osdev-algo

Releases (1)

• 0.1.0.0 indexed

Definitions (367)

PROOF.bend

• def bitw.fls_le.h
• def bitw.fls_le
• def bitw.ffs_le_fls.fffs <= fls
• def bitw.ffs_le_fls.t
• def bitw.ffs_le_fls
• def bitw.ctz_spec
• def bitw.ctz_ffs.h
• def bitw.ctz_ffs
• def bitw.index_some
• def bitw.index_none
• def bitw.first_set_is_set
• def bitw.first_set_lowest
• def bitw.first_set_none
• def bitw.last_set_is_set
• def bitw.last_set_highest
• def bitw.last_set_none
• def bitw.ctz_first_set
• def bitw.last_lewith the highest set bit at k, k <= m in a word of width 1 + m
• def bitw.clz_last_set
• def bitw.first_le_last
• def bitw.ctz_clz.h
• def bitw.ffs_fls_k
• def bitw.ctz_clz
• def u32.zero
• def w64.lo_cat
• def w64.hi_cat
• def w64.zero
• def bitseq.next_le
• def bitseq.next_hit
• def bitseq.next_ge
• def bitseq.lt0
• def bitseq.next_miss
• def w64.first_set_none
• def absurd.maybe32
• def absurd.ns32
• def maybe32.get
• def some_inj32
• def absurd.sn_nat
• def bool.and_l
• def bool.and_r
• def nat.dbit
• def word.cmp_nat.d
• def word.cmp_nat.h
• def word.cmp_nat
• def u32.cmp_nat
• def u32.mv_lea hypothesis about U32's order, as one about Nat's
• def u32.mv_lt
• def u32.mv_eq
• def nat.le_trans
• def nat.nlt_lenot a < c, a <= b: not b < c
• def nat.gt_le_nek < a (not a < k, a != k), a <= b: b != k
• def u32.le_trans
• def u32.nlt_le
• def u32.gt_le_ne
• def cmp.lt_ne
• def u32.lt_ne
• def word.eq_tail
• def word.eq_head
• def word.eq
• def u32.eq
• def bs.sorted_tail
• def bs.head_lethe head of a sorted list is at most each of its elements
• def bs.le_len.h
• def bs.le_len
• def bs.step0
• def bs.step1
• def bs.below
• def bs.above0
• def bs.above1
• def bs.above
• def bs.hit_none
• def bs.hit_shift
• def bs.check_shift
• def bs.some.h
• def bs.some
• def bs.none0
• def bs.none1
• def bs.none
• def bs.find_some
• def ba.kcthe element read at m is below the key exactly when m is below LB
• def ba.key_cmp
• def ba.jz_eqafter a halving that keeps the upper half: hi - (mid + 1) is (hi - lo) - (1 + (hi - lo) / 2)
• def ba.adv2one halving, with the element at mid below the key (b) or not
• def ba.advone halving of [lo, hi): active when lo < hi (c)
• def ba.runf halvings from lo <= LB <= hi <= n with hi - lo < 2^f end at LB
• def ba.hz33n < 2^32 < 2^33: the 33 halvings suffice (stated so that 2^33 is never expanded)
• def ba.lb_lethe lower bound is at most n
• def ba.answerthe search's answer is the lower bound
• def ba.hsa sorted prefix of the reflected array is a sorted prefix of l
• def ba.hit
• def ba.fd
• def ba.fs
• def ba.lb.body
• def ba.lb.ref
• def ba.lbs.body
• def ba.lbs.ref
• def ba.fl.body
• def ba.fl.ref
• def ba.fls.body
• def ba.fls.ref