fast.bend

lawful-bytes@0.1.1.0 · 144 lines · 19 definitions

1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-bytes@0.1.1.0/defs.bend as D
4import lawful-bytes@0.1.1.0/bytes.bend as B
5
6# lawful-bytes operations a word at a time: the same names, signatures and
7# results as bytes.bend's (a later pass proves each equal to it). Loops read
8# whole words; reads past the block's end wrap (Base wraps indexes) and what
9# they read never reaches a result.
10
11# 0x80 at each byte of v that is 0, exact at the lowest such byte (a byte
12# above a 0 byte may be flagged too).
13def zb(+v: U32) -> U32:
14  ((v - 16843009 : U32) .&. (U32.not(v) .&. 2155905152 : U32) : U32)
15
16# c in all four bytes of a word.
17def rep(+c: U32) -> U32:
18  (c * 16843009 : U32)
19
20def b2u(b: Bool) -> U32:
21  match b:
22    case True{}:
23      1
24    case False{}:
25      0
26
27# The place (0-3) of the lowest flagged byte of a nonzero mask.
28def bidx(+m: U32) -> U32:
29  (b2u(U32.is_zero((m .&. 128 : U32))) + b2u(U32.is_zero((m .&. 32896 : U32))) + b2u(U32.is_zero((m .&. 8421504 : U32))) : U32)
30
31# The bytes of a word at or above byte i's place. The first word of a search
32# sets the bytes below the start to 0xFF before the zero-byte test (not the
33# flags after it): zb is exact only at its lowest zero byte, and a match below
34# the start would otherwise borrow and flag the byte at the start (found by the
35# proof agent: "A@BC" searched for 'A' from 1).
36def low(+i: U32) -> U32:
37  U32.shln(4294967295, U32.to_nat(((i .&. 3 : U32) << 3n : U32)))
38
39# How many words hold bytes from .. to-1 (0 when to <= from).
40def words(+from: U32, +to: U32) -> Nat:
41  Bool.pick(Nat, U32.is_le(to, from), 0n, U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32)))
42
43# ---------------------------------------------------------------------------
44# find, find2
45# ---------------------------------------------------------------------------
46
47def find.fin(+to: U32, r: Array<U32> & U32) -> Array<U32> & U32:
48  (a, +j) = r
49  (a, U32.min(j, to))
50
51# m flags word wi's hits; z: m is 0; r holds word wi + 1; n counts the words
52# left, wi's included. Answers the offset of the first hit, or 2^32 - 1.
53def find.go(n: Nat, z: Bool, r: Array<U32> & U32, +wi: U32, +m: U32, +rc: U32) -> Array<U32> & U32:
54  match n z:
55    case 0n _:
56      (a, w) = r
57      (a, 4294967295)
58    case 1n+k True{}:
59      (a, +w) = r
60      +m2 = zb((w .^. rc : U32))
61      find.go(k, U32.is_zero(m2), Array.get(U32, a, (wi + 2 : U32)), (wi + 1 : U32), m2, rc)
62    case 1n+k False{}:
63      (a, w) = r
64      (a, ((wi << 2n : U32) + bidx(m) : U32))
65
66def find.start(n: Nat, r: Array<U32> & U32, +from: U32, +rc: U32) -> Array<U32> & U32:
67  (a, +w) = r
68  +wi = (from >> 2n : U32)
69  +lo = U32.not(low(from))
70  +m = zb(((w .^. rc : U32) .|. lo : U32))
71  find.go(n, U32.is_zero(m), Array.get(U32, a, (wi + 1 : U32)), wi, m, rc)
72
73def find.k(+len: U32, r: Array<U32> & U32) -> D.Bytes & U32:
74  (buf, +j) = r
75  (D.Bytes{len, buf}, j)
76
77# The first index j with from <= j < to where byte j is c; to if none.
78def find(b: D.Bytes, +from: U32, +to: U32, +c: U32) -> D.Bytes & U32:
79  D.Bytes{+len, buf} = b
80  find.k(len, find.fin(to, find.start(words(from, to), Array.get(U32, buf, (from >> 2n : U32)), from, rep(c))))
81
82def find2.go(n: Nat, z: Bool, r: Array<U32> & U32, +wi: U32, +m: U32, +r1: U32, +r2: U32) -> Array<U32> & U32:
83  match n z:
84    case 0n _:
85      (a, w) = r
86      (a, 4294967295)
87    case 1n+k True{}:
88      (a, +w) = r
89      +m2 = (zb((w .^. r1 : U32)) .|. zb((w .^. r2 : U32)) : U32)
90      find2.go(k, U32.is_zero(m2), Array.get(U32, a, (wi + 2 : U32)), (wi + 1 : U32), m2, r1, r2)
91    case 1n+k False{}:
92      (a, w) = r
93      (a, ((wi << 2n : U32) + bidx(m) : U32))
94
95def find2.start(n: Nat, r: Array<U32> & U32, +from: U32, +r1: U32, +r2: U32) -> Array<U32> & U32:
96  (a, +w) = r
97  +wi = (from >> 2n : U32)
98  +lo = U32.not(low(from))
99  +m = (zb(((w .^. r1 : U32) .|. lo : U32)) .|. zb(((w .^. r2 : U32) .|. lo : U32)) : U32)
100  find2.go(n, U32.is_zero(m), Array.get(U32, a, (wi + 1 : U32)), wi, m, r1, r2)
101
102# The first index j with from <= j < to where byte j is c1 or c2; to if none.
103def find2(b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32:
104  D.Bytes{+len, buf} = b
105  find.k(len, find.fin(to, find2.start(words(from, to), Array.get(U32, buf, (from >> 2n : U32)), from, rep(c1), rep(c2))))
106
107# ---------------------------------------------------------------------------
108# append
109# ---------------------------------------------------------------------------
110
111# n words to dst from word di on, taken from src's bytes at a shift of sh
112# bits: lo is src word si, r holds word si + 1.
113def append.words(n: Nat, r: Array<U32> & U32, +lo: U32, dst: Array<U32>, +si: U32, +di: U32, +sh: Nat) -> Array<U32> & Array<U32>:
114  match n:
115    case 0n:
116      (src, w) = r
117      (dst, src)
118    case 1n+k:
119      (src, +hi) = r
120      append.words(k, Array.get(U32, src, (si + 2 : U32)), hi, Array.set(U32, dst, di, (U32.shrn(lo, sh) .|. U32.shln(hi, Nat.sub(32n, sh)) : U32)), (si + 1 : U32), (di + 1 : U32), sh)
121
122def append.fin(+dl: U32, +sl: U32, r: Array<U32> & Array<U32>) -> D.Bytes & D.Bytes:
123  (db, sb) = r
124  (D.Bytes{dl, db}, D.Bytes{sl, sb})
125
126def append.w(+dl: U32, +n: U32, +q: U32, db: Array<U32>, +sl: U32, r: Array<U32> & U32) -> D.Bytes & D.Bytes:
127  (sb, +lo) = r
128  append.fin((dl + n : U32), sl, append.words(U32.to_nat(((n + 3 : U32) >> 2n : U32)), Array.get(U32, sb, ((q >> 2n : U32) + 1 : U32)), lo, db, (q >> 2n : U32), (dl >> 2n : U32), U32.to_nat(((q .&. 3 : U32) << 3n : U32))))
129
130# dst's length is now a multiple of 4: n more bytes of src from q, a word at a
131# time (up to 3 bytes past the new length are overwritten too).
132def append.k(+n: U32, +q: U32, r: D.Bytes & D.Bytes) -> D.Bytes & D.Bytes:
133  (dst, src) = r
134  D.Bytes{+dl, db} = dst
135  D.Bytes{+sl, sb} = src
136  append.w(dl, n, q, db, sl, Array.get(U32, sb, (q >> 2n : U32)))
137
138# dst with bytes s .. s+n-1 of src added at the end; src handed back. The
139# first bytes, up to dst's next word boundary, go one at a time, the rest a
140# word at a time.
141def append(dst: D.Bytes, src: D.Bytes, +s: U32, +n: U32) -> D.Bytes & D.Bytes:
142  D.Bytes{+dl, db} = dst
143  +h = U32.min(((4 - (dl .&. 3 : U32) : U32) .&. 3 : U32), n)
144  append.k((n - h : U32), (s + h : U32), B.append(D.Bytes{dl, db}, src, s, h))