bits.bend checks
raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/bits.bend as Bits
2 imports
import Base import ./logic.bend as Lg
Laws
law word_cmp_refl provedsource · line 99 · raw
@n:Nat -> @w:Word(n) -> {Word.cmp(n, w, w) == EQ{} : Cmp}word_cmp_refl: cmp(n, w, w) == EQ (induction on n + w).
law u32_eq_refl provedsource · line 118 · raw
@a:U32 -> {U32.is_eq(a, a) == True{} : Bool}u32_eq_refl: (x == x) == True.
Definitions
def pop_go source · line 20 · raw
@fuel:Nat -> @+x:U32 -> @acc:U32 -> U32
popcount: number of set bits. Fixed 32 steps.
def pop source · line 27 · raw
@+x:U32 -> U32
def ctz_go source · line 32 · raw
@fuel:Nat -> @+x:U32 -> @+acc:U32 -> U32
ctz: count trailing zeros. ctz(0) == 32. Fixed 32 steps, state frozen with picks once the first set bit is seen.
def ctz source · line 43 · raw
@+x:U32 -> U32
def clz source · line 47 · raw
@+x:U32 -> U32
clz: count leading zeros. clz(0) == 32. Via Base U32.log2 (no loop).
def rotl source · line 52 · raw
@+x:U32 -> @+k:Nat -> U32
rotl / rotr by k bits (k: Nat). Straight-line, no loop.
def rotr source · line 55 · raw
@+x:U32 -> @+k:Nat -> U32
def is_pow2 source · line 59 · raw
@+x:U32 -> Bool
is_pow2: True for 1, 2, 4, ... (and False for 0).
def next_pow2_big source · line 65 · raw
@p:U32 -> U32
next_pow2: smallest power of two >= x (with next_pow2(0) == 1). Wraps to 0 for x > 0x80000000 (no 33-bit values exist).
def next_pow2 source · line 68 · raw
@+x:U32 -> U32
def ceil_div source · line 72 · raw
@a:U32 -> @+b:U32 -> U32
ceil_div: (a + b - 1) / b. Returns 0 when b == 0.
def abs_diff source · line 76 · raw
@+a:U32 -> @+b:U32 -> U32
abs_diff: |a - b| without signed types (sub wraps, pick keeps the good side).
def avg source · line 80 · raw
@+a:U32 -> @+b:U32 -> U32
avg: (a + b) / 2 with no overflow: (a & b) + ((a ^ b) >> 1).
def parity source · line 84 · raw
@+x:U32 -> U32
parity: popcount mod 2 (0 or 1). is_odd: lowest bit set.
def is_odd source · line 87 · raw
@+x:U32 -> Bool
def mix32 source · line 91 · raw
@+x:U32 -> U32
mix32: Murmur3 fmix32 avalanche. Use to hash U32 keys.
def fnv_step source · line 129 · raw
@h:U32 -> @b:U32 -> U32
fnv_step: one FNV-1a byte fold. h = (h ^ byte) * 16777619.
def sat_add source · line 133 · raw
@+a:U32 -> @b:U32 -> U32
sat_add / sat_sub: saturating arithmetic (clamp instead of wrap).
def sat_sub source · line 137 · raw
@+a:U32 -> @+b:U32 -> U32
def lowbit source · line 141 · raw
@+x:U32 -> U32
lowbit: lowest set bit as a mask (lowbit(12) == 4).
def bswap32 source · line 145 · raw
@+x:U32 -> U32
bswap32: reverse byte order.
def mul_hi source · line 153 · raw
@+a:U32 -> @+b:U32 -> U32
mul_hi: upper 32 bits of the 64-bit product (16-bit splitting, exact).