1	# Every field writer and its reader agree, for every value; a byte is always
2	# below 256; and a byte string split anywhere joins back to itself. The
3	# vectors fix the byte orders, the hex text, and what a short input reads.
4	import Base
5	import bend-osdev-word64@0.1.0.0/word64.bend as W
6	import ./bytes.bend as B
7	
8	# Properties, for every input
9	
10	law le16_round_trip:
11	  for v: U32
12	  {B.le16_at(B.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
13	
14	law be16_round_trip:
15	  for v: U32
16	  {B.be16_at(B.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
17	
18	law le32_round_trip:
19	  for v: U32
20	  {B.le32_at(B.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
21	
22	law be32_round_trip:
23	  for v: U32
24	  {B.be32_at(B.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
25	
26	law le64_round_trip:
27	  for +v: W.W64
28	  {B.le64_at(B.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
29	
30	law be64_round_trip:
31	  for +v: W.W64
32	  {B.be64_at(B.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
33	
34	law byte_below_256:
35	  for b: U32
36	  {U32.is_lt(B.byte(b), 256) == True{} : Bool}
37	
38	law take_drop:
39	  for n: Nat
40	  for xs: List<&2, U32>
41	  {B.append(B.take(n, xs), B.drop(n, xs)) == xs : List<&2, U32>}
42	
43	# Vectors (0x12345678 = 305419896)
44	
45	law be32_order:
46	  {B.be32(305419896) == [18, 52, 86, 120] : List<&2, U32>}
47	
48	law le32_order:
49	  {B.le32(305419896) == [120, 86, 52, 18] : List<&2, U32>}
50	
51	law be64_order:
52	  {B.be64(W.W64.from_parts(16909060, 84281096)) == [1, 2, 3, 4, 5, 6, 7, 8] : List<&2, U32>}
53	
54	law le16_at_offset:
55	  {B.le16_at([9, 52, 18], 1n) == Some{4660} : Maybe<&2, U32>}
56	
57	law short_input:
58	  {B.le16_at([1, 2, 3], 2n) == None{} : Maybe<&2, U32>}
59	
60	law at_end:
61	  {B.at([7, 8], 2n) == None{} : Maybe<&2, U32>}
62	
63	law masks_elements:
64	  {B.at([7, 264], 1n) == Some{8} : Maybe<&2, U32>}
65	
66	law hex_text:
67	  {B.hex(B.of_string("Bend")) == "42656e64" : String}
68	
69	# The Octets interface: the same round trips, and slicing, on Octets
70	
71	law octets_le16_round_trip:
72	  for v: U32
73	  {B.Octets.le16_at(B.Octets.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
74	
75	law octets_be16_round_trip:
76	  for v: U32
77	  {B.Octets.be16_at(B.Octets.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
78	
79	law octets_le32_round_trip:
80	  for v: U32
81	  {B.Octets.le32_at(B.Octets.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
82	
83	law octets_be32_round_trip:
84	  for v: U32
85	  {B.Octets.be32_at(B.Octets.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
86	
87	law octets_le64_round_trip:
88	  for +v: W.W64
89	  {B.Octets.le64_at(B.Octets.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
90	
91	law octets_be64_round_trip:
92	  for +v: W.W64
93	  {B.Octets.be64_at(B.Octets.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
94	
95	law octets_take_drop:
96	  for n: Nat
97	  for o: B.Octets
98	  {B.Octets.append(B.Octets.take(n, o), B.Octets.drop(n, o)) == o : B.Octets}
99	
100	# of_list masks once: converting a byte string to a list and back changes nothing
101	law octets_of_list_idempotent:
102	  for xs: List<&2, U32>
103	  {B.Octets.of_list(B.Octets.to_list(B.Octets.of_list(xs))) == B.Octets.of_list(xs) : B.Octets}
104	
105	law octets_is_eq_refl:
106	  for o: B.Octets
107	  {B.Octets.is_eq(o, o) == True{} : Bool}
108	
109	law octets_masks:
110	  {B.Octets.hex(B.Octets.of_list([255, 256, 257])) == "ff0001" : String}
111	
112	law octets_slice:
113	  {B.Octets.to_string(B.Octets.slice(2n, 3n, B.Octets.of_string("bend-osdev"))) == "nd-" : String}
114	
115	# The interface laws other packages' proofs rely on: how Octets relates to
116	# lists, without depending on how Octets stores its bytes
117	
118	law octets_append_list:
119	  for a: B.Octets
120	  for b: B.Octets
121	  {B.Octets.to_list(B.Octets.append(a, b)) == B.append(B.Octets.to_list(a), B.Octets.to_list(b)) : List<&2, U32>}
122	
123	# every Octets is a valid byte string: to a list and back changes nothing
124	law octets_of_to:
125	  for o: B.Octets
126	  {B.Octets.of_list(B.Octets.to_list(o)) == o : B.Octets}
127	
128	# a list becomes Octets by masking each element to its low 8 bits
129	law octets_to_of:
130	  for xs: List<&2, U32>
131	  {B.Octets.to_list(B.Octets.of_list(xs)) == B.mask(xs) : List<&2, U32>}
132	
133	law octets_zeros_list:
134	  for n: Nat
135	  {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}
136	
137	law octets_cons_list:
138	  for b: U32
139	  for o: B.Octets
140	  {B.Octets.to_list(B.Octets.cons(b, o)) == Con{B.byte(b), B.Octets.to_list(o)} : List<&2, U32>}
141	
142	law octets_len_list:
143	  for o: B.Octets
144	  {B.Octets.len(o) == B.len(B.Octets.to_list(o)) : Nat}
145	
146	# a joined string splits back exactly where it was joined
147	law octets_take_append:
148	  for +a: B.Octets
149	  for b: B.Octets
150	  {B.Octets.take(B.Octets.len(a), B.Octets.append(a, b)) == a : B.Octets}
151	
152	law octets_drop_append:
153	  for a: B.Octets
154	  for +b: B.Octets
155	  {B.Octets.drop(B.Octets.len(a), B.Octets.append(a, b)) == b : B.Octets}
156	
157	law octets_split_at_append:
158	  for +a: B.Octets
159	  for +b: B.Octets
160	  {B.Octets.split_at(B.Octets.len(a), B.Octets.append(a, b)) == Some{B.OctetsSplit{a, b}} : Maybe<&2, B.OctetsSplit>}
161	
162	law octets_split_short:
163	  {B.Octets.split_at(4n, B.Octets.of_string("abc")) == None{} : Maybe<&2, B.OctetsSplit>}
164	
165	law octets_split_text:
166	  {B.Octets.split_at(2n, B.Octets.of_string("abc")) == Some{B.OctetsSplit{B.Octets.of_string("ab"), B.Octets.of_string("c")}} : Maybe<&2, B.OctetsSplit>}
167	
168	# The tail-recursive list layer: each fast form equals its structural form,
169	# for every input (stated structural == fast, the direction rewrites use, so
170	# that `%BL.len_fast(xs) : {... _ ...}` turns a fast form back into the one
171	# the other laws are about)
172	
173	law len_fast:
174	  for xs: List<&2, U32>
175	  {B.len(xs) == B.len.fast(xs) : Nat}
176	
177	law take_fast:
178	  for n: Nat
179	  for xs: List<&2, U32>
180	  {B.take(n, xs) == B.take.fast(n, xs) : List<&2, U32>}
181	
182	law append_fast:
183	  for xs: List<&2, U32>
184	  for ys: List<&2, U32>
185	  {B.append(xs, ys) == B.append.fast(xs, ys) : List<&2, U32>}
186	
187	law zeros_fast:
188	  for n: Nat
189	  {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}
190	
191	law mask_fast:
192	  for xs: List<&2, U32>
193	  {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}
194	
195	law of_string_fast:
196	  for s: String
197	  {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>}
198	
199	law to_string_fast:
200	  for xs: List<&2, U32>
201	  {B.to_string(xs) == B.to_string.fast(xs) : String}
202	
203	law hex_fast:
204	  for xs: List<&2, U32>
205	  {B.hex(xs) == B.hex.fast(xs) : String}
206	
207	law list_eq_fast:
208	  for xs: List<&2, U32>
209	  for ys: List<&2, U32>
210	  {B.list_eq(xs, ys) == B.list_eq.fast(xs, ys) : Bool}
211	
212	law rev_rev:
213	  for xs: List<&2, U32>
214	  {B.rev(B.rev(xs)) == xs : List<&2, U32>}
215	
216	# Octets' text and hex are the list layer's, and concat joins in order
217	
218	law octets_hex_list:
219	  for o: B.Octets
220	  {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String}
221	
222	law octets_to_string_list:
223	  for o: B.Octets
224	  {B.Octets.to_string(o) == B.to_string(B.Octets.to_list(o)) : String}
225	
226	law octets_concat_nil:
227	  {B.Octets.concat(Nil{}) == B.Octets.empty() : B.Octets}
228	
229	law octets_concat_cons:
230	  for h: B.Octets
231	  for t: List<&2, B.Octets>
232	  {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets}