1 import Base 2 import lawful-words@0.1.0.0/defs.bend as W 3 import ./defs.bend as D 4 5 # lawful-bytes operations. This is the reference version: a byte at a time, 6 # simple to prove. Faster versions (a word at a time) replace these bodies 7 # under the same laws. Loops here read one byte ahead and discard it at the 8 # end; reads past len stay inside the block (Base wraps indexes), and the 9 # value read never reaches a result. 10 11 # An empty Bytes with room for 4 * 2^d bytes. 12 def empty(+d: Nat) -> D.Bytes: 13 D.Bytes{0, Array.new(U32, d, 0)} 14 15 def at.fin(+len: U32, +i: U32, r: Array & U32) -> D.Bytes & U32: 16 (buf, +w) = r 17 (D.Bytes{len, buf}, W.byte(w, U32.to_nat((i .&. 3 : U32)))) 18 19 # Byte i (for i < len). 20 def at(b: D.Bytes, +i: U32) -> D.Bytes & U32: 21 D.Bytes{+len, buf} = b 22 at.fin(len, i, Array.get(U32, buf, (i >> 2n : U32))) 23 24 def set.fin(+len: U32, +i: U32, +v: U32, r: Array & U32) -> D.Bytes: 25 (buf, +w) = r 26 D.Bytes{len, Array.set(U32, buf, (i >> 2n : U32), W.put_byte(w, U32.to_nat((i .&. 3 : U32)), v))} 27 28 # Byte i set to v (for i < len and v < 256). 29 def set(b: D.Bytes, +i: U32, +v: U32) -> D.Bytes: 30 D.Bytes{+len, buf} = b 31 set.fin(len, i, v, Array.get(U32, buf, (i >> 2n : U32))) 32 33 def push.fin(+len: U32, +v: U32, r: Array & U32) -> D.Bytes: 34 (buf, +w) = r 35 D.Bytes{(len + 1 : U32), Array.set(U32, buf, (len >> 2n : U32), W.put_byte(w, U32.to_nat((len .&. 3 : U32)), v))} 36 37 # v added at the end (for len < cap and v < 256). 38 def push(b: D.Bytes, +v: U32) -> D.Bytes: 39 D.Bytes{+len, buf} = b 40 push.fin(len, v, Array.get(U32, buf, (len >> 2n : U32))) 41 42 # n more bytes of src, from s; r holds src's byte s. 43 def append.go(n: Nat, dst: D.Bytes, r: D.Bytes & U32, +s: U32) -> D.Bytes & D.Bytes: 44 match n: 45 case 0n: 46 (src, x) = r 47 (dst, src) 48 case 1n+k: 49 (src, +x) = r 50 append.go(k, push(dst, x), at(src, (s + 1 : U32)), (s + 1 : U32)) 51 52 # dst with bytes s .. s+n-1 of src added at the end; src handed back. 53 def append(dst: D.Bytes, src: D.Bytes, +s: U32, +n: U32) -> D.Bytes & D.Bytes: 54 append.go(U32.to_nat(n), dst, at(src, s), s) 55 56 # Word i onwards copied into dst; r holds word i of the old block. 57 def grow.go(n: Nat, r: Array & U32, dst: Array, +i: U32) -> Array: 58 match n: 59 case 0n: 60 (src, w) = r 61 dst 62 case 1n+k: 63 (src, +w) = r 64 grow.go(k, Array.get(U32, src, (i + 1 : U32)), Array.set(U32, dst, i, w), (i + 1 : U32)) 65 66 def grow.fin(+len: U32, +e: Nat, r: Array & U32) -> D.Bytes: 67 (buf, +n) = r 68 D.Bytes{len, grow.go(U32.to_nat(n), Array.get(U32, buf, 0), Array.new(U32, e, 0), 0)} 69 70 # The same bytes in a block of 2^e words (for e at least the current depth). 71 def grow(b: D.Bytes, +e: Nat) -> D.Bytes: 72 D.Bytes{+len, buf} = b 73 grow.fin(len, e, Array.size(U32, buf)) 74 75 # hit says byte j is c; r holds byte j + 1; n counts positions left from j. 76 def find.go(n: Nat, hit: Bool, r: D.Bytes & U32, +j: U32, +to: U32, +c: U32) -> D.Bytes & U32: 77 match n hit: 78 case 0n _: 79 (b, x) = r 80 (b, to) 81 case 1n+k True{}: 82 (b, x) = r 83 (b, j) 84 case 1n+k False{}: 85 (b, +x) = r 86 find.go(k, U32.is_eq(x, c), at(b, (j + 2 : U32)), (j + 1 : U32), to, c) 87 88 def find.start(n: Nat, r: D.Bytes & U32, +from: U32, +to: U32, +c: U32) -> D.Bytes & U32: 89 (b, +x) = r 90 find.go(n, U32.is_eq(x, c), at(b, (from + 1 : U32)), from, to, c) 91 92 # The first index j with from <= j < to where byte j is c; to if none. 93 def find(b: D.Bytes, +from: U32, +to: U32, +c: U32) -> D.Bytes & U32: 94 find.start(Nat.sub(U32.to_nat(to), U32.to_nat(from)), at(b, from), from, to, c) 95 96 def find2.go(n: Nat, hit: Bool, r: D.Bytes & U32, +j: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32: 97 match n hit: 98 case 0n _: 99 (b, x) = r 100 (b, to) 101 case 1n+k True{}: 102 (b, x) = r 103 (b, j) 104 case 1n+k False{}: 105 (b, +x) = r 106 find2.go(k, U32.is_eq(x, c1) || U32.is_eq(x, c2), at(b, (j + 2 : U32)), (j + 1 : U32), to, c1, c2) 107 108 def find2.start(n: Nat, r: D.Bytes & U32, +from: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32: 109 (b, +x) = r 110 find2.go(n, U32.is_eq(x, c1) || U32.is_eq(x, c2), at(b, (from + 1 : U32)), from, to, c1, c2) 111 112 # The first index j with from <= j < to where byte j is c1 or c2; to if none. 113 def find2(b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32: 114 find2.start(Nat.sub(U32.to_nat(to), U32.to_nat(from)), at(b, from), from, to, c1, c2) 115 116 # ra, rb hold byte i of a and byte j of b; acc says all bytes so far matched. 117 def same.go(n: Nat, ra: D.Bytes & U32, rb: D.Bytes & U32, +i: U32, +j: U32, acc: Bool) -> D.Bytes & (D.Bytes & Bool): 118 match n: 119 case 0n: 120 (a, x) = ra 121 (b, y) = rb 122 (a, (b, acc)) 123 case 1n+k: 124 (a, +x) = ra 125 (b, +y) = rb 126 same.go(k, at(a, (i + 1 : U32)), at(b, (j + 1 : U32)), (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(x, y)) 127 128 # Bytes i .. i+n-1 of a equal bytes j .. j+n-1 of b; both handed back. 129 def same(a: D.Bytes, +i: U32, b: D.Bytes, +j: U32, +n: U32) -> D.Bytes & (D.Bytes & Bool): 130 same.go(U32.to_nat(n), at(a, i), at(b, j), i, j, True{}) 131 132 # The number of bytes in use. 133 def len(b: D.Bytes) -> D.Bytes & U32: 134 D.Bytes{+n, buf} = b 135 (D.Bytes{n, buf}, n) 136 137 def capacity.fin(+n: U32, r: Array & U32) -> D.Bytes & U32: 138 (buf, +w) = r 139 (D.Bytes{n, buf}, (w << 2n : U32)) 140 141 # How many bytes fit (4 per word). 142 def capacity(b: D.Bytes) -> D.Bytes & U32: 143 D.Bytes{+n, buf} = b 144 capacity.fin(n, Array.size(U32, buf)) 145 146 # Only the first n bytes kept (for n <= len). 147 def truncate(b: D.Bytes, +n: U32) -> D.Bytes: 148 D.Bytes{len, buf} = b 149 D.Bytes{n, buf} 150 151 # Bytes j + k onwards moved to j; r holds byte j + k. 152 def shift.go(n: Nat, r: D.Bytes & U32, +j: U32, +k: U32) -> D.Bytes: 153 match n: 154 case 0n: 155 (b, x) = r 156 b 157 case 1n+m: 158 (b, +x) = r 159 shift.go(m, at(set(b, j, x), ((j + 1 : U32) + k : U32)), (j + 1 : U32), k) 160 161 # The first k bytes dropped, the rest moved to the start (for k <= len). 162 def shift(b: D.Bytes, +k: U32) -> D.Bytes: 163 D.Bytes{+n, buf} = b 164 truncate(shift.go(Nat.sub(U32.to_nat(n), U32.to_nat(k)), at(D.Bytes{n, buf}, k), 0, k), (n - k : U32)) 165 166 def of_list.go(xs: List<&2, U32>, b: D.Bytes) -> D.Bytes: 167 match xs: 168 case Nil{}: 169 b 170 case Con{x, t}: 171 of_list.go(t, push(b, x)) 172 173 # A Bytes in a block of 2^d words holding the bytes of xs (Base's file 174 # reads give such lists). 175 def of_list(+d: Nat, xs: List<&2, U32>) -> D.Bytes: 176 of_list.go(xs, empty(d)) 177 178 def to_list.cons(+x: U32, r: D.Bytes & List<&2, U32>) -> D.Bytes & List<&2, U32>: 179 (b, t) = r 180 (b, Con{x, t}) 181 182 # r holds byte s. 183 def to_list.go(n: Nat, r: D.Bytes & U32, +s: U32) -> D.Bytes & List<&2, U32>: 184 match n: 185 case 0n: 186 (b, x) = r 187 (b, Nil{}) 188 case 1n+m: 189 (b, +x) = r 190 to_list.cons(x, to_list.go(m, at(b, (s + 1 : U32)), (s + 1 : U32))) 191 192 # Bytes s .. s+n-1 as a list (Base's file writes take such lists). 193 def to_list(b: D.Bytes, +s: U32, +n: U32) -> D.Bytes & List<&2, U32>: 194 to_list.go(U32.to_nat(n), at(b, s), s) 195 196 def at2.fin2(+x: U32, r: D.Bytes & U32) -> D.Bytes & (U32 & U32): 197 (b, +y) = r 198 (b, (x, y)) 199 200 def at2.fin(+j: U32, r: D.Bytes & U32) -> D.Bytes & (U32 & U32): 201 (b, +x) = r 202 at2.fin2(x, at(b, j)) 203 204 # Bytes i and j. 205 def at2(b: D.Bytes, +i: U32, +j: U32) -> D.Bytes & (U32 & U32): 206 at2.fin(j, at(b, i)) 207 208 # r holds bytes i and j; acc says all bytes so far matched. 209 def same1.go(n: Nat, r: D.Bytes & (U32 & U32), +i: U32, +j: U32, acc: Bool) -> D.Bytes & Bool: 210 match n: 211 case 0n: 212 (b, q) = r 213 (b, acc) 214 case 1n+m: 215 (b, q) = r 216 (x, y) = q 217 same1.go(m, at2(b, (i + 1 : U32), (j + 1 : U32)), (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(x, y)) 218 219 # Bytes i .. i+n-1 equal bytes j .. j+n-1 of the same buffer. 220 def same1(b: D.Bytes, +i: U32, +j: U32, +n: U32) -> D.Bytes & Bool: 221 same1.go(U32.to_nat(n), at2(b, i, j), i, j, True{})