1	import Base
2	import lawful-words@0.1.0.0/defs.bend as W
3	import ./defs.bend as D
4	import ./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).
13	def zb(+v: U32) -> U32:
14	  ((v - 16843009 : U32) .&. (U32.not(v) .&. 2155905152 : U32) : U32)
15	
16	# c in all four bytes of a word.
17	def rep(+c: U32) -> U32:
18	  (c * 16843009 : U32)
19	
20	def 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.
28	def 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).
36	def 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).
40	def 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	
47	def 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.
53	def 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	
66	def 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	
73	def 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.
78	def 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	
82	def 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	
95	def 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.
103	def 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.
113	def 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	
122	def 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	
126	def 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).
132	def 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.
141	def 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))