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).
23	import Base
24	import ./array.bend as A
25	
26	# For every array
27	
28	law 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	
34	law 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	
41	law 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	
48	law 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	
57	law 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	
63	law 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	
72	law 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	
79	law 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	
87	law 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	
94	law 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	
103	law 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	
113	law 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	
127	law 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	
132	law 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	
139	law 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	
146	law 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	
158	law 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	
165	law 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	
173	law 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	
180	law 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	
190	law 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	
201	law 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	
207	law 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	
218	law 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	
225	law 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	
234	law 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	
244	law 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	
256	law witness_perfect:
257	  {Bool.and(A.Arrays.is_perfect(U32, 2n, Array.new(U32, 2n, 0)), Nat.is_lt(2n, 32n)) == True{} : Bool}
258	
259	law 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	
262	law witness_index:
263	  {Nat.is_lt(3n, A.Arrays.slots(2n)) == True{} : Bool}
264	
265	law 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	
268	law 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	
273	law 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	
276	law 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	
279	law vector_index:
280	  {A.Arrays.index(3n, 13) == 5n : Nat}
281	
282	law 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	
285	law vector_index_wrap:
286	  {A.Arrays.index(2n, U32.from_nat(Nat.add(A.Arrays.slots(2n), 3n))) == 3n : Nat}
287	
288	law vector_not_perfect:
289	  {A.Arrays.is_perfect(U32, 2n, ANode{ALeaf{1}, ANode{ALeaf{2}, ALeaf{3}}}) == False{} : Bool}