LAWS.bend

bend-osdev-array@0.1.0.1 · 289 lines · 38 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.1/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}