lawful-bytes
Search uses release 0.1.1.0 · 578 definitions
Definitions (578)
- def bmirror.go
- def bmirror
- def trTransport of a hypothesis about b to its mirror.
- law ok_fullThe three parts of ok.
- law ok_d
- law ok_len
- law ok_mkok from its three parts.
- def L4
- law wbp0The four bytes of a word with byte k set to v (k a literal).
- law wbp1
- law wbp2
- law wbp3
- law wbp
- law unpack_setByte 4q + r of the word list after word q is written with its byte r set.
- law unpack_set_iThe same for a U32 index.
- law wd_getWord k (in range) is the k-th of the word list.
- law wl_setWriting word k (in range) sets the k-th of the word list.
- law full_set
- law four_lt_e4 * 2^d < 2^e for d + 2 < e (e stays a variable here: 2^32 must never be unfolded, so the callers instantiate e = 32n only in the final type).
- law fits_e
- law he32
- law add_fitsA sum of two words that stays within 4 * 2^d does not wrap.
- law succ_le
- law inc_fitsAn index below 4 * 2^d steps up by one.
- law drop_drop
- law tconsA list whose first element is b.
- law tg1The first m (<= 4) elements of ys are b0 ..
- law tg2
- law tg3
- law tg4
- law us1Writing word q replaces bytes 4q ..
- law take_split
- law slice_split
- law slice_takeA slice of the first l elements, inside them.
- law slice_length
- law le_antisym
- law min_l
- law min_r
- law min_le
- law lt_w
- law lt8
- law sub4_lt
- law idx_upIndex 4w + x for x >= 4 is index 4(w + 1) + (x - 4).
- def AWTThe tree append.words leaves: p is the word read next (hi), lo the word before it, td the dst block, di the dst word written, sh the shift in bits.
- law aw_eq
- law mrg2The code's shifted pair is lawful-words' merge.
- law mrg
- law and3_lt
- law shq2
- law shqThe shift of append.w is 8 * (q & 3).
- def US
- law mb_lo
- law mb_hi
- law gsel
- law gjByte j of the window at 4 si + r, for j below m.
- law winThe first m bytes of a merged word are the m src bytes from 4 si + r.
- law lt_w0
- law le_x4
- law four_alg
- law c4
- law w2_bound
- law sub_le_of
- law step
- law avfThe last word, when fewer than 4 bytes are left.
- law avAfter the words written so far (o bytes, o <= np), the bytes in use agree with v1 then src from qn; the k words left finish the np bytes.
- law ag_sizeThe length after the reference append's pushes.
- law aw_full
- law mul4div
- law al_kx = 4a + k with k + h = 4 gives x + h = 4(a + 1).
- def H0
- law exk
- law align2
- law aligndst's length after the first h0 bytes is a multiple of 4.
- law x3_lt_ex + y < 2^e for x <= 4 * 2^d and y <= 3, when d + 2 < e (e a variable: the callers put 32n only in the final type).
- law cnt1The word count (np + 3) >> 2 covers np bytes with less than one word left.
- law cnt2
- def HHThe bytes done one at a time, the bytes left, and where they start.
- def NPw
- def QQ
- def NW
- def SH
- def TF
- law fa_eqWith BT(l1, t1) the result of the first bytes, fast append is these mirrors.
- law fin_eqThe last list step: the bytes of the prefix and of the words make the slice.
- def D1
- law hh_le
- law hc_h
- law ok1
- law el1
- law enp
- law esuml1 + (n - h) = ld + n.
- law hlen0
- def fap.go
- law fast_append_pair_t
- def fao.go
- law fast_append_ok_t
- law esum_n
- law avcWhat the word loop leaves: the bytes in use after the prefix, then src from q.
- def fav.go
- law fast_append_view_t