LAWS.bend
bend-osdev-array@0.1.0.0 · 289 lines · 0 definitions
1# Laws about Base's Array (Array.size, Array.get, Array.set, Array.new), as
2# Base 2.0.37 defines them, for every input:
3#
4# * for every array, of any shape: a read hands back the same array; a read
5# after a write at the same index answers the value written; a write keeps
6# the size; every slot of Array.new holds its value;
7# * perfect trees (`Arrays.is_perfect`): Array.new builds one, Array.set keeps
8# one, and the size of one of depth d is 2^d;
9# * for a perfect tree of depth d < 32, against the list model
10# (`Arrays.leaves`, the slots in index order): a read answers the model's
11# element at the masked index (`Arrays.index`), a write sets it, the model
12# has 2^d elements, and a write leaves every read at a different masked
13# index unchanged;
14# * the masked index is below 2^d, and is k itself for a k below 2^d (for
15# 2^d + k as well, which wraps to k; and for a U32 below 2^d, its value);
16# * arrays built from a Data list (`Arrays.of_list`): every perfect array is
17# one (`reflect`), and get, set and new answer one, so that a proof can
18# follow a sequence of reads and writes on Data alone.
19#
20# Arrays are single-owner values (Type), but a law's statement is checked
21# dead, so it may mention one array several times; the proofs consume each
22# array once (they reflect it into a Data tree).
23import Base
24import bend-osdev-array@0.1.0.0/array.bend as A
25
26# For every array
27
28law get_same_array:
29 for -T: Data
30 for a: Array<T>
31 for i: U32
32 {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}
33
34law get_set_same:
35 for -T: Data
36 for a: Array<T>
37 for i: U32
38 for v: T
39 {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}
40
41law set_keeps_size:
42 for -T: Data
43 for a: Array<T>
44 for i: U32
45 for v: T
46 {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, a, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, a)) : U32}
47
48law get_new:
49 for -T: Data
50 for d: Nat
51 for v: T
52 for i: U32
53 {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}
54
55# Perfect trees
56
57law new_perfect:
58 for -T: Data
59 for d: Nat
60 for v: T
61 {A.Arrays.is_perfect(T, d, Array.new(T, d, v)) == True{} : Bool}
62
63law set_perfect:
64 for -T: Data
65 for d: Nat
66 for a: Array<T>
67 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
68 for i: U32
69 for v: T
70 {A.Arrays.is_perfect(T, d, Array.set(T, a, i, v)) == True{} : Bool}
71
72law size_perfect:
73 for -T: Data
74 for d: Nat
75 for a: Array<T>
76 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
77 {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}
78
79law new_leaves:
80 for -T: Data
81 for d: Nat
82 for v: T
83 {A.Arrays.leaves(T, Array.new(T, d, v)) == List.replicate(T, A.Arrays.slots(d), v) : List<&2, T>}
84
85# The list model, for perfect trees
86
87law model_length:
88 for -T: Data
89 for d: Nat
90 for a: Array<T>
91 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
92 {List.length(&2, T, A.Arrays.leaves(T, a)) == A.Arrays.slots(d) : Nat}
93
94law model_get:
95 for -T: Data
96 for d: Nat
97 for a: Array<T>
98 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
99 for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
100 for i: U32
101 {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}
102
103law model_set:
104 for -T: Data
105 for d: Nat
106 for a: Array<T>
107 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
108 for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
109 for i: U32
110 for v: T
111 {A.Arrays.leaves(T, Array.set(T, a, i, v)) == List.set(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i), v) : List<&2, T>}
112
113law get_set_other:
114 for -T: Data
115 for d: Nat
116 for a: Array<T>
117 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
118 for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
119 for i: U32
120 for j: U32
121 for v: T
122 for hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}
123 {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}
124
125# Indices
126
127law index_below:
128 for d: Nat
129 for i: U32
130 {Nat.is_lt(A.Arrays.index(d, i), A.Arrays.slots(d)) == True{} : Bool}
131
132law index_of_nat:
133 for d: Nat
134 for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
135 for k: Nat
136 for hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}
137 {A.Arrays.index(d, U32.from_nat(k)) == k : Nat}
138
139law index_wrap:
140 for d: Nat
141 for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
142 for k: Nat
143 for hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}
144 {A.Arrays.index(d, U32.from_nat(Nat.add(A.Arrays.slots(d), k))) == k : Nat}
145
146law index_of_u32:
147 for d: Nat
148 for i: U32
149 for hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}
150 {A.Arrays.index(d, i) == U32.to_nat(i) : Nat}
151
152# Arrays built from a Data list: a proof may name such an array as often as
153# it needs, since it is rebuilt from Data each time. `reflect` turns a
154# perfect array into one (using the array once), and get, set and new keep
155# the form, so a proof about a sequence of reads and writes consumes each
156# array once, as the program does.
157
158law of_list_perfect:
159 for -T: Data
160 for +d: Nat
161 for +xs: List<&2, T>
162 for +f: T
163 {A.Arrays.is_perfect(T, d, A.Arrays.of_list(T, d, xs, f)) == True{} : Bool}
164
165law of_list_leaves:
166 for -T: Data
167 for +d: Nat
168 for +xs: List<&2, T>
169 for +f: T
170 for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
171 {A.Arrays.leaves(T, A.Arrays.of_list(T, d, xs, f)) == xs : List<&2, T>}
172
173law of_list_size:
174 for -T: Data
175 for +d: Nat
176 for +xs: List<&2, T>
177 for +f: T
178 {Array.size(T, A.Arrays.of_list(T, d, xs, f)) == (A.Arrays.of_list(T, d, xs, f), U32.shln(1, d)) : Array<T> & U32}
179
180law of_list_get:
181 for -T: Data
182 for +d: Nat
183 for +xs: List<&2, T>
184 for +f: T
185 for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
186 for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
187 for +i: U32
188 {Array.get(T, A.Arrays.of_list(T, d, xs, f), i) == (A.Arrays.of_list(T, d, xs, f), A.Arrays.nth(T, xs, A.Arrays.index(d, i), f)) : Array<T> & T}
189
190law of_list_set:
191 for -T: Data
192 for +d: Nat
193 for +xs: List<&2, T>
194 for +f: T
195 for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
196 for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
197 for +i: U32
198 for +v: T
199 {Array.set(T, A.Arrays.of_list(T, d, xs, f), i, v) == A.Arrays.of_list(T, d, List.set(&2, T, xs, A.Arrays.index(d, i), v), f) : Array<T>}
200
201law of_list_new:
202 for -T: Data
203 for +d: Nat
204 for +v: T
205 {Array.new(T, d, v) == A.Arrays.of_list(T, d, List.replicate(T, A.Arrays.slots(d), v), v) : Array<T>}
206
207law reflect:
208 for -T: Data
209 for +d: Nat
210 for a: Array<T>
211 for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
212 for +f: T
213 exs xs: List<&2, T>
214 {A.Arrays.of_list(T, d, xs, f) == a : Array<T>} & {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
215
216# The list model's own facts, for every list
217
218law set_length:
219 for -T: Data
220 for xs: List<&2, T>
221 for k: Nat
222 for v: T
223 {List.length(&2, T, List.set(&2, T, xs, k, v)) == List.length(&2, T, xs) : Nat}
224
225law nth_set_same:
226 for -T: Data
227 for xs: List<&2, T>
228 for k: Nat
229 for v: T
230 for f: T
231 for h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}
232 {A.Arrays.nth(T, List.set(&2, T, xs, k, v), k, f) == v : T}
233
234law nth_set_other:
235 for -T: Data
236 for xs: List<&2, T>
237 for k: Nat
238 for m: Nat
239 for v: T
240 for f: T
241 for h: {Nat.is_eq(k, m) == False{} : Bool}
242 {A.Arrays.nth(T, List.set(&2, T, xs, k, v), m, f) == A.Arrays.nth(T, xs, m, f) : T}
243
244law nth_replicate:
245 for -T: Data
246 for n: Nat
247 for v: T
248 for k: Nat
249 for f: T
250 for h: {Nat.is_lt(k, n) == True{} : Bool}
251 {A.Arrays.nth(T, List.replicate(T, n, v), k, f) == v : T}
252
253# Witnesses: the hypotheses above hold together (depth 2, an array from
254# Array.new, the indices 1 and 2, the slot 3)
255
256law witness_perfect:
257 {Bool.and(A.Arrays.is_perfect(U32, 2n, Array.new(U32, 2n, 0)), Nat.is_lt(2n, 32n)) == True{} : Bool}
258
259law witness_other:
260 {U32.is_eq(U32.and(1, U32.sub(U32.shln(1, 2n), 1)), U32.and(2, U32.sub(U32.shln(1, 2n), 1))) == False{} : Bool}
261
262law witness_index:
263 {Nat.is_lt(3n, A.Arrays.slots(2n)) == True{} : Bool}
264
265law witness_index_wrap:
266 {Bool.and(Nat.is_lt(U32.to_nat(5), A.Arrays.slots(3n)), Nat.is_lt(3n, A.Arrays.slots(2n))) == True{} : Bool}
267
268law witness_list:
269 {Bool.and(Nat.is_eq(List.length(&2, U32, [5, 6, 7, 8]), A.Arrays.slots(2n)), Bool.and(Nat.is_lt(1n, 4n), Nat.is_ne(1n, 2n))) == True{} : Bool}
270
271# Vectors
272
273law vector_wrap:
274 {Pair.snd(Array<U32>, U32, Array.get(U32, Array.set(U32, Array.new(U32, 2n, 0), 6, 9), 2)) == 9 : U32}
275
276law vector_leaves:
277 {A.Arrays.leaves(U32, Array.set(U32, Array.new(U32, 2n, 0), 1, 7)) == [0, 7, 0, 0] : List<&2, U32>}
278
279law vector_index:
280 {A.Arrays.index(3n, 13) == 5n : Nat}
281
282law vector_of_list:
283 {Pair.snd(Array<U32>, U32, Array.get(U32, Array.set(U32, A.Arrays.of_list(U32, 2n, [5, 6, 7, 8], 0), 1, 9), 5)) == 9 : U32}
284
285law vector_index_wrap:
286 {A.Arrays.index(2n, U32.from_nat(Nat.add(A.Arrays.slots(2n), 3n))) == 3n : Nat}
287
288law vector_not_perfect:
289 {A.Arrays.is_perfect(U32, 2n, ANode{ALeaf{1}, ANode{ALeaf{2}, ALeaf{3}}}) == False{} : Bool}