LAWS.bend
bend-osdev-bytes@0.1.0.0 · 232 lines · 0 definitions
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.
4import Base
5import bend-osdev-word64@0.1.0.0/word64.bend as W
6import bend-osdev-bytes@0.1.0.0/bytes.bend as B
7
8# Properties, for every input
9
10law le16_round_trip:
11 for v: U32
12 {B.le16_at(B.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
13
14law be16_round_trip:
15 for v: U32
16 {B.be16_at(B.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
17
18law le32_round_trip:
19 for v: U32
20 {B.le32_at(B.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
21
22law be32_round_trip:
23 for v: U32
24 {B.be32_at(B.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
25
26law le64_round_trip:
27 for +v: W.W64
28 {B.le64_at(B.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
29
30law be64_round_trip:
31 for +v: W.W64
32 {B.be64_at(B.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
33
34law byte_below_256:
35 for b: U32
36 {U32.is_lt(B.byte(b), 256) == True{} : Bool}
37
38law 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
45law be32_order:
46 {B.be32(305419896) == [18, 52, 86, 120] : List<&2, U32>}
47
48law le32_order:
49 {B.le32(305419896) == [120, 86, 52, 18] : List<&2, U32>}
50
51law be64_order:
52 {B.be64(W.W64.from_parts(16909060, 84281096)) == [1, 2, 3, 4, 5, 6, 7, 8] : List<&2, U32>}
53
54law le16_at_offset:
55 {B.le16_at([9, 52, 18], 1n) == Some{4660} : Maybe<&2, U32>}
56
57law short_input:
58 {B.le16_at([1, 2, 3], 2n) == None{} : Maybe<&2, U32>}
59
60law at_end:
61 {B.at([7, 8], 2n) == None{} : Maybe<&2, U32>}
62
63law masks_elements:
64 {B.at([7, 264], 1n) == Some{8} : Maybe<&2, U32>}
65
66law 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
71law 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
75law 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
79law octets_le32_round_trip:
80 for v: U32
81 {B.Octets.le32_at(B.Octets.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
82
83law octets_be32_round_trip:
84 for v: U32
85 {B.Octets.be32_at(B.Octets.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
86
87law 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
91law 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
95law 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
101law 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
105law octets_is_eq_refl:
106 for o: B.Octets
107 {B.Octets.is_eq(o, o) == True{} : Bool}
108
109law octets_masks:
110 {B.Octets.hex(B.Octets.of_list([255, 256, 257])) == "ff0001" : String}
111
112law 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
118law 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
124law 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
129law 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
133law octets_zeros_list:
134 for n: Nat
135 {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}
136
137law 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
142law 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
147law 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
152law 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
157law 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
162law octets_split_short:
163 {B.Octets.split_at(4n, B.Octets.of_string("abc")) == None{} : Maybe<&2, B.OctetsSplit>}
164
165law 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
173law len_fast:
174 for xs: List<&2, U32>
175 {B.len(xs) == B.len.fast(xs) : Nat}
176
177law 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
182law 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
187law zeros_fast:
188 for n: Nat
189 {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}
190
191law mask_fast:
192 for xs: List<&2, U32>
193 {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}
194
195law of_string_fast:
196 for s: String
197 {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>}
198
199law to_string_fast:
200 for xs: List<&2, U32>
201 {B.to_string(xs) == B.to_string.fast(xs) : String}
202
203law hex_fast:
204 for xs: List<&2, U32>
205 {B.hex(xs) == B.hex.fast(xs) : String}
206
207law 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
212law 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
218law octets_hex_list:
219 for o: B.Octets
220 {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String}
221
222law 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
226law octets_concat_nil:
227 {B.Octets.concat(Nil{}) == B.Octets.empty() : B.Octets}
228
229law 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}