1	import Base
2	import lawful-words@0.1.0.0/defs.bend as W
3	import lawful-arrays@0.1.0.0/defs.bend as A
4	
5	# lawful-bytes definitions: the Bytes type and what it means. The operations
6	# are in bytes.bend, the laws in LAWS.bend.
7	
8	# Bytes packed four to a word, little-endian, in a block of 2^d words: byte i
9	# is byte i & 3 of word i >> 2. len is the number of bytes in use; the bytes
10	# past len are unspecified.
11	type Bytes is Type:
12	  Bytes{len: U32, buf: Array<U32>}
13	
14	# The four bytes of each word, in order.
15	def unpack(ws: List<&2, U32>) -> List<&2, U32>:
16	  match ws:
17	    case Nil{}:
18	      Nil{}
19	    case Con{+w, t}:
20	      List.append(&2, U32, [W.byte(w, 0n), W.byte(w, 1n), W.byte(w, 2n), W.byte(w, 3n)], unpack(t))
21	
22	# What a Bytes holds: its first len bytes.
23	def view(b: Bytes) -> List<&2, U32>:
24	  Bytes{len, buf} = b
25	  List.take(&2, U32, unpack(A.view(U32, buf)), U32.to_nat(len))
26	
27	# The number of bytes in use.
28	def size(b: Bytes) -> Nat:
29	  Bytes{len, buf} = b
30	  U32.to_nat(len)
31	
32	# How many bytes fit: four per word.
33	def cap(b: Bytes) -> Nat:
34	  Bytes{len, buf} = b
35	  Nat.mul(4n, List.length(&2, U32, A.view(U32, buf)))
36	
37	# b is well formed with a block of depth d: a perfect block of 2^d words,
38	# d <= 29, and len within the block. A buffer holds at most 2^31 bytes (2 GiB),
39	# so every index and length fits in a U32; the laws' hypotheses keep sums of
40	# lengths in range too. Larger files are read in pieces.
41	def ok(b: Bytes, +d: Nat) -> Bool:
42	  Bytes{len, buf} = b
43	  A.full(U32, buf, d) && (Nat.is_le(d, 29n) && Nat.is_le(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))))
44	
45	# Every element is a byte (below 256).
46	def all_bytes(xs: List<&2, U32>) -> Bool:
47	  match xs:
48	    case Nil{}:
49	      True{}
50	    case Con{x, t}:
51	      U32.is_lt(x, 256) && all_bytes(t)
52	
53	# n elements from index i.
54	def slice(xs: List<&2, U32>, +i: Nat, +n: Nat) -> List<&2, U32>:
55	  List.take(&2, U32, List.drop(&2, U32, xs, i), n)
56	
57	# How many leading elements are not c.
58	def run_len(xs: List<&2, U32>, +c: U32) -> Nat:
59	  match xs:
60	    case Nil{}:
61	      0n
62	    case Con{+x, t}:
63	      Bool.pick(Nat, U32.is_eq(x, c), 0n, Nat.add(1n, run_len(t, c)))
64	
65	# How many leading elements are neither c1 nor c2.
66	def run_len2(xs: List<&2, U32>, +c1: U32, +c2: U32) -> Nat:
67	  match xs:
68	    case Nil{}:
69	      0n
70	    case Con{+x, t}:
71	      Bool.pick(Nat, U32.is_eq(x, c1) || U32.is_eq(x, c2), 0n, Nat.add(1n, run_len2(t, c1, c2)))
72	
73	# The first index j with from <= j < to where xs has c; to if there is none
74	# (for from <= to <= length(xs), as the laws assume).
75	def first(xs: List<&2, U32>, +from: Nat, +to: Nat, +c: U32) -> Nat:
76	  Nat.add(from, run_len(slice(xs, from, Nat.sub(to, from)), c))
77	
78	# The same for either of two values (same assumptions).
79	def first2(xs: List<&2, U32>, +from: Nat, +to: Nat, +c1: U32, +c2: U32) -> Nat:
80	  Nat.add(from, run_len2(slice(xs, from, Nat.sub(to, from)), c1, c2))
81	
82	# Two lists are equal, element by element.
83	def list_eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
84	  match xs ys:
85	    case Nil{} Nil{}:
86	      True{}
87	    case Con{x, xt} Con{y, yt}:
88	      U32.is_eq(x, y) && list_eq(xt, yt)
89	    case Nil{} Con{y, yt}:
90	      False{}
91	    case Con{x, xt} Nil{}:
92	      False{}
93	
94	# xs has c at index k.
95	def is_some(m: Maybe<&2, U32>, +c: U32) -> Bool:
96	  match m:
97	    case Some{x}:
98	      U32.is_eq(x, c)
99	    case None{}:
100	      False{}
101	
102	def has(xs: List<&2, U32>, +k: Nat, +c: U32) -> Bool:
103	  is_some(List.get(&2, U32, xs, k), c)
104	
105	# xs has c1 or c2 at index k.
106	def has2(+xs: List<&2, U32>, +k: Nat, +c1: U32, +c2: U32) -> Bool:
107	  is_some(List.get(&2, U32, xs, k), c1) || is_some(List.get(&2, U32, xs, k), c2)