lawful-bytes

Search uses release 0.1.1.0 · 578 definitions

Releases (2)

def P0The place of the first zero byte of v (4 when there is none).
law tko1The k = 1 test of the or of two flag words.
law tko2The k = 2 test of the or of two flag words.
law tko3The k = 3 test of the or of two flag words.
law zb_noneThe zero-byte flags are all clear exactly when no byte is zero.
law zb_bidxbidx finds the first zero byte.
law zb2_noneThe same for the flags of two words or-ed (find2).
law zb2_bidx
law p0_xorSearching w for c is searching w xor rep(c) for a zero byte.
law plk0
law plk1
law plk2
law plk3
law plThe first word for a start place a (0 to 3, given as r).
law p0_lowThe first word of a search: the bytes below i's place are set to 0xFF, so the first zero byte is the first c at or above that place.

def is_some_t
law none_ne_some
law drop_zero
law drop_consDropping j elements from a list with x at j leaves x in front.
law slice_cons
law lt_add_succ
law add11(j + 1) + 1 is j + 2, for every word j (no range needed: through from_nat).
law fgo_pair
law find_pair_t
law fgo2_pair
law find2_pair_t
law step_ltWith j + 1 + k = to <= len, byte j is in range.
law step_lt4
law step_get
law step_n
law fgo_viewhit says byte j is c, r holds byte j + 1, j + n = to.
law le_ftfrom <= to as numbers.
law find_view_t
law fgo2_viewhit says byte j is c1 or c2, r holds byte j + 1, j + n = to.
law find2_view_t