bend-osdev-u32

Releases (1)

• 0.1.0.0 indexed

Definitions (397)

check.bend

• def add_lhsthe two sides of u32_add_wrap and u32_sub_wrap, at run time
• def sub_lhs
• def sub_rhs
• def main

PROOF.bend

• def ur.r42
• def un.and_zero
• def ur.r43
• def un.lts
• def un.u32_shl_low
• def un.u32_low_self
• def ur.r44
• def ur.r45

PROOF_div.bend

• def ud.sub_zero
• def ud.pred
• def ud.succ_inj
• def ud.add_cancela + r == b + r gives a == b
• def ud.bool_disc
• def ud.bool_clash
• def ud.ex_falso
• def ud.no_lt_one
• def ud.sub_addr < bp + 1 gives (bp - r) + r == bp
• def ud.dm_lhs
• def ud.dm_sum
• def ud.div_mod
• def ud.lt_add
• def ud.dm_lt
• def ud.mod_lt
• def ud.dm_smallfewer steps than m left in the round: the remainder grows by n
• def ud.dm_roundfinishing a round: m steps, then one more starts the next
• def ud.dm_rounds
• def ud.cover_suma + bp == (a + (bp - r)) + r, for r < 1 + bp
• def ud.cover

PROOF_order.bend

• def ab.bool
• def ab.tf
• def ab.ft
• def ab.is_lt
• def ab.is_eq
• def ab.is_gt
• def ab.eq_lt
• def ab.gt_lt
• def ab.lt_eq
• def ab.gt_eq
• def cm.flip
• def cm.lt_of
• def cm.is_lt_of
• def cm.le_of_lt
• def cm.eq_of_leis_le(c) and not is_lt(c): c is EQ
• def cm.le_flipflipping turns not-less into at-most and the other way
• def cm.lt_flip
• def cm.not_le_flip
• def cm.not_lt_flip
• def wd.fin_refl
• def wd.refl
• def wd.fin_eq_tail
• def wd.bool_eq
• def wd.fin_eq_head
• def wd.eq
• def wd.bool_flip
• def wd.fin_flip
• def wd.flip
• def wd.bool_trans
• def wd.fin_trans
• def wd.lt_trans
• def ult
• def ule
• def u.refl
• def u.eq
• def u.flip
• def u.cmp_lt_trans
• def u.le_refl
• def ab.lt_eqc
• def u.lt_irrefl
• def u.le_of_lt
• def u.lt_trans
• def u.not_lt
• def u.not_le
• def u.lt_not_lea < b: not b <= a
• def u.le_not_lta <= b: not b < a
• def u.le_lt.go
• def u.le_lta <= b < c
• def u.lt_le.go
• def u.lt_lea < b <= c
• def u.le_le.go
• def u.le_transa <= b <= c
• def u.antisyma <= b and b <= a: a == b
• def nt.le_trans
• def nt.lt_trans
• def nt.lt_le_trans
• def nt.le_lt_trans
• def nt.le_add_r

u32.bend

• def U32Nat.dblx times 2^n: x doubled n times
• def U32Nat.bit1 for True, 0 for False
• def U32Nat.halfn / 2, rounded down
• def U32Nat.oddx mod 2: 1 for an odd x, 0 for an even one
• def U32Nat.lowthe low k bits of x (x mod 2^k), and the rest (x / 2^k, rounded down): x = low(k, x) + 2^k high(k, x)
• def U32Nat.high
• def U32Word.maskthe word of width n whose low k bits are set (2^k - 1, for k <= n): the mask that U32.and(x, m) takes x's low k bits with