src/storage/refinement.bend
bendtorch-core@0.1.0.0 · 448 lines · 57 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/array.bend as Core
4import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
5
6def trace(d: Nat, +n: U32, +i: U32, z: Bool) -> Model.Path(d):
7 match d z:
8 case 0n _:
9 Unit{}
10 case 1n+p True{}:
11 Model.Step{False{}, trace(p, U32.shr(n), i,
12 U32.is_lt(i, U32.shr(U32.shr(n))))}
13 case 1n+p False{}:
14 +j = U32.sub(i, U32.shr(n))
15 Model.Step{True{}, trace(p, U32.shr(n), j,
16 U32.is_lt(j, U32.shr(U32.shr(n))))}
17
18def first(-T: Type, pair: Array<T> & T) -> Array<T>:
19 (array, value) = pair
20 array
21
22def second(-T: Type, pair: Array<T> & T) -> T:
23 (array, value) = pair
24 value
25
26type Get<-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32, -z: Bool> is Type:
27 Get{array: Array<T>, value: T,
28 equal: {(array, value) == Array.get.go(T, original, n, i, z) : Array<T> & T},
29 kept: {array == original : Array<T>},
30 observed: {Some{value} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>},
31 balanced: Model.Balanced(T, d, array)}
32
33def get_low(-T: Data, -p: Nat, -original: Array<T>, -n: U32, -i: U32,
34 ys: Array<T>,
35 child: Get<T, p, original, U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n)))>,
36 ey: Model.Balanced(T, p, ys)) -> Get<T, 1n+p, ANode{original, ys}, n, i, True{}>:
37 match child:
38 case Get{xs, value, equal, kept, observed, ex}:
39 Get{ANode{xs, ys}, value,
40 Equal.cong(Array<T> & T, Array<T> & T, r => Array.swap.lo(T, ys, r),
41 (xs, value), Array.get.go(T, original, U32.shr(n), i,
42 U32.is_lt(i, U32.shr(U32.shr(n)))), equal),
43 Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs, original, kept),
44 observed, (ex, ey)}
45
46def get_high(-T: Data, -p: Nat, -original: Array<T>, -n: U32, -i: U32,
47 xs: Array<T>,
48 child: Get<T, p, original, U32.shr(n), U32.sub(i, U32.shr(n)),
49 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))>,
50 ex: Model.Balanced(T, p, xs)) -> Get<T, 1n+p, ANode{xs, original}, n, i, False{}>:
51 match child:
52 case Get{ys, value, equal, kept, observed, ey}:
53 Get{ANode{xs, ys}, value,
54 Equal.cong(Array<T> & T, Array<T> & T, r => Array.swap.hi(T, xs, r),
55 (ys, value), Array.get.go(T, original, U32.shr(n), U32.sub(i, U32.shr(n)),
56 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), equal),
57 Equal.cong(Array<T>, Array<T>, y => ANode{xs, y}, ys, original, kept),
58 observed, (ex, ey)}
59
60def get_go(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, z: Bool,
61 valid: Model.Balanced(T, d, array)) -> Get<T, d, array, n, i, z>:
62 match d array z:
63 case 0n ALeaf{+value} _:
64 Get{ALeaf{value}, value, {==}, {==}, {==}, valid}
65 case 0n ANode{xs, ys} _:
66 match valid:
67 case 1n+p ALeaf{value} _:
68 match valid:
69 case 1n+p ANode{xs, ys} True{}:
70 (ex, ey) = valid
71 get_low(T, p, xs, n, i, ys,
72 get_go(T, p, xs, U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n))), ex), ey)
73 case 1n+p ANode{xs, ys} False{}:
74 (ex, ey) = valid
75 +j = U32.sub(i, U32.shr(n))
76 get_high(T, p, ys, n, i, xs,
77 get_go(T, p, ys, U32.shr(n), j, U32.is_lt(j, U32.shr(U32.shr(n))), ey), ex)
78
79def get_go_retained(-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32, -z: Bool,
80 cert: Get<T, d, original, n, i, z>) ->
81 {first(T, Array.get.go(T, original, n, i, z)) == original : Array<T>}:
82 match cert:
83 case Get{array, value, equal, kept, observed, valid}:
84 %equal : {first(T, _) == original : Array<T>}
85 kept
86
87def get_go_observed(-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32, -z: Bool,
88 cert: Get<T, d, original, n, i, z>) ->
89 {Some{second(T, Array.get.go(T, original, n, i, z))} ==
90 Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}:
91 match cert:
92 case Get{array, value, equal, kept, observed, valid}:
93 %equal : {Some{second(T, _)} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}
94 observed
95
96def get_go_balanced(-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32, -z: Bool,
97 cert: Get<T, d, original, n, i, z>) ->
98 Model.Balanced(T, d, first(T, Array.get.go(T, original, n, i, z))):
99 match cert:
100 case Get{array, value, equal, kept, observed, valid}:
101 %equal : Model.Balanced(T, d, first(T, _))
102 valid
103
104def law_get_go_retains(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, z: Bool,
105 valid: Model.Balanced(T, d, array)) ->
106 {first(T, Array.get.go(T, array, n, i, z)) == array : Array<T>}:
107 get_go_retained(T, d, array, n, i, z, get_go(T, d, array, n, i, z, valid))
108
109def law_get_go_refines(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, z: Bool,
110 valid: Model.Balanced(T, d, array)) ->
111 {Some{second(T, Array.get.go(T, array, n, i, z))} ==
112 Model.observe(T, d, array, trace(d, n, i, z)) : Maybe<&2, T>}:
113 get_go_observed(T, d, array, n, i, z, get_go(T, d, array, n, i, z, valid))
114
115def law_get_go_balanced(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, z: Bool,
116 valid: Model.Balanced(T, d, array)) ->
117 Model.Balanced(T, d, first(T, Array.get.go(T, array, n, i, z))):
118 get_go_balanced(T, d, array, n, i, z, get_go(T, d, array, n, i, z, valid))
119
120type Swap<-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32, -z: Bool, -new: T> is Type:
121 Swap{array: Array<T>, old: T,
122 equal: {(array, old) == Array.swap.go(T, original, n, i, new, z) : Array<T> & T},
123 written: {array == Core.write_path(T, d, original, trace(d, n, i, z), new) : Array<T>},
124 observed: {Some{old} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>},
125 balanced: Model.Balanced(T, d, array)}
126
127def swap_low(-T: Data, -p: Nat, -original: Array<T>, -n: U32, -i: U32, -new: T,
128 ys: Array<T>,
129 child: Swap<T, p, original, U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n))), new>,
130 ey: Model.Balanced(T, p, ys)) -> Swap<T, 1n+p, ANode{original, ys}, n, i, True{}, new>:
131 match child:
132 case Swap{xs, old, equal, written, observed, ex}:
133 Swap{ANode{xs, ys}, old,
134 Equal.cong(Array<T> & T, Array<T> & T, r => Array.swap.lo(T, ys, r),
135 (xs, old), Array.swap.go(T, original, U32.shr(n), i, new,
136 U32.is_lt(i, U32.shr(U32.shr(n)))), equal),
137 Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs,
138 Core.write_path(T, p, original,
139 trace(p, U32.shr(n), i, U32.is_lt(i, U32.shr(U32.shr(n)))), new), written),
140 observed, (ex, ey)}
141
142def swap_high(-T: Data, -p: Nat, -original: Array<T>, -n: U32, -i: U32, -new: T,
143 xs: Array<T>,
144 child: Swap<T, p, original, U32.shr(n), U32.sub(i, U32.shr(n)),
145 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n))), new>,
146 ex: Model.Balanced(T, p, xs)) -> Swap<T, 1n+p, ANode{xs, original}, n, i, False{}, new>:
147 match child:
148 case Swap{ys, old, equal, written, observed, ey}:
149 Swap{ANode{xs, ys}, old,
150 Equal.cong(Array<T> & T, Array<T> & T, r => Array.swap.hi(T, xs, r),
151 (ys, old), Array.swap.go(T, original, U32.shr(n), U32.sub(i, U32.shr(n)), new,
152 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), equal),
153 Equal.cong(Array<T>, Array<T>, y => ANode{xs, y}, ys,
154 Core.write_path(T, p, original,
155 trace(p, U32.shr(n), U32.sub(i, U32.shr(n)),
156 U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), new), written),
157 observed, (ex, ey)}
158
159def swap_go(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, new: T, z: Bool,
160 valid: Model.Balanced(T, d, array)) -> Swap<T, d, array, n, i, z, new>:
161 match d array z:
162 case 0n ALeaf{old} _:
163 Swap{ALeaf{new}, old, {==}, {==}, {==}, valid}
164 case 0n ANode{xs, ys} _:
165 match valid:
166 case 1n+p ALeaf{old} _:
167 match valid:
168 case 1n+p ANode{xs, ys} True{}:
169 (ex, ey) = valid
170 swap_low(T, p, xs, n, i, new, ys,
171 swap_go(T, p, xs, U32.shr(n), i, new,
172 U32.is_lt(i, U32.shr(U32.shr(n))), ex), ey)
173 case 1n+p ANode{xs, ys} False{}:
174 (ex, ey) = valid
175 +j = U32.sub(i, U32.shr(n))
176 swap_high(T, p, ys, n, i, new, xs,
177 swap_go(T, p, ys, U32.shr(n), j, new,
178 U32.is_lt(j, U32.shr(U32.shr(n))), ey), ex)
179
180def swap_go_written(-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32,
181 -z: Bool, -new: T, cert: Swap<T, d, original, n, i, z, new>) ->
182 {first(T, Array.swap.go(T, original, n, i, new, z)) ==
183 Core.write_path(T, d, original, trace(d, n, i, z), new) : Array<T>}:
184 match cert:
185 case Swap{array, old, equal, written, observed, valid}:
186 %equal : {first(T, _) == Core.write_path(T, d, original, trace(d, n, i, z), new) : Array<T>}
187 written
188
189def swap_go_observed(-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32,
190 -z: Bool, -new: T, cert: Swap<T, d, original, n, i, z, new>) ->
191 {Some{second(T, Array.swap.go(T, original, n, i, new, z))} ==
192 Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}:
193 match cert:
194 case Swap{array, old, equal, written, observed, valid}:
195 %equal : {Some{second(T, _)} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>}
196 observed
197
198def swap_go_balanced(-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32,
199 -z: Bool, -new: T, cert: Swap<T, d, original, n, i, z, new>) ->
200 Model.Balanced(T, d, first(T, Array.swap.go(T, original, n, i, new, z))):
201 match cert:
202 case Swap{array, old, equal, written, observed, valid}:
203 %equal : Model.Balanced(T, d, first(T, _))
204 valid
205
206def law_swap_go_refines(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32,
207 new: T, z: Bool, valid: Model.Balanced(T, d, array)) ->
208 {first(T, Array.swap.go(T, array, n, i, new, z)) ==
209 Core.write_path(T, d, array, trace(d, n, i, z), new) : Array<T>}:
210 swap_go_written(T, d, array, n, i, z, new, swap_go(T, d, array, n, i, new, z, valid))
211
212def law_swap_go_balanced(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32,
213 new: T, z: Bool, valid: Model.Balanced(T, d, array)) ->
214 Model.Balanced(T, d, first(T, Array.swap.go(T, array, n, i, new, z))):
215 swap_go_balanced(T, d, array, n, i, z, new, swap_go(T, d, array, n, i, new, z, valid))
216
217def law_swap_go_observed(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32,
218 new: T, z: Bool, valid: Model.Balanced(T, d, array)) ->
219 {Some{second(T, Array.swap.go(T, array, n, i, new, z))} ==
220 Model.observe(T, d, array, trace(d, n, i, z)) : Maybe<&2, T>}:
221 swap_go_observed(T, d, array, n, i, z, new, swap_go(T, d, array, n, i, new, z, valid))
222
223def masked(+n: U32, i: U32) -> U32:
224 U32.and(i, U32.sub(n, 1))
225
226def route_n(d: Nat, +n: U32, i: U32) -> Model.Path(d):
227 +j = masked(n, i)
228 trace(d, n, j, U32.is_lt(j, U32.shr(n)))
229
230def route(+d: Nat, i: U32) -> Model.Path(d):
231 route_n(d, Size.capacity(d), i)
232
233def observed_transport(-T: Data, -d: Nat, -array: Array<T>, -original: Array<T>,
234 -n: U32, -i: U32, -value: T,
235 kept: {array == original : Array<T>}, extent: {n == Size.capacity(d) : U32},
236 observed: {Some{value} == Model.observe(T, d, array, route_n(d, n, i)) : Maybe<&2, T>}) ->
237 {Some{value} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}:
238 %kept : {Some{value} == Model.observe(T, d, _, route(d, i)) : Maybe<&2, T>}
239 %extent : {Some{value} == Model.observe(T, d, array, route_n(d, _, i)) : Maybe<&2, T>}
240 observed
241
242type GetFull<-T: Data, -d: Nat, -original: Array<T>, -i: U32> is Type:
243 GetFull{array: Array<T>, value: T,
244 equal: {(array, value) == Array.get(T, original, i) : Array<T> & T},
245 kept: {array == original : Array<T>},
246 observed: {Some{value} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>},
247 balanced: Model.Balanced(T, d, array)}
248
249def get_final(-T: Data, -d: Nat, -original: Array<T>, -sized_array: Array<T>, -n: U32, -i: U32,
250 measured: {(sized_array, n) == Array.size(T, original) : Array<T> & U32},
251 +retained: {sized_array == original : Array<T>}, extent: {n == Size.capacity(d) : U32},
252 child: Get<T, d, sized_array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n))>) ->
253 GetFull<T, d, original, i>:
254 match child:
255 case Get{array, value, equal, kept, observed, valid}:
256 GetFull{array, value,
257 Equal.trans(Array<T> & T, (array, value), Array.get.at(T, i, (sized_array, n)),
258 Array.get(T, original, i), equal,
259 Equal.cong(Array<T> & U32, Array<T> & T, r => Array.get.at(T, i, r),
260 (sized_array, n), Array.size(T, original), measured)),
261 Equal.trans(Array<T>, array, sized_array, original, kept, retained),
262 observed_transport(T, d, sized_array, original, n, i, value, retained, extent, observed),
263 valid}
264
265def get_sized(-T: Data, +d: Nat, -original: Array<T>, +i: U32,
266 sized: Size.Sized<T, d, original>) -> GetFull<T, d, original, i>:
267 match sized:
268 case Size.Sized{array, +n, retained, measured, extent, valid}:
269 get_final(T, d, original, array, n, i, measured, retained, extent,
270 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid))
271
272def get(-T: Data, +d: Nat, array: Array<T>, +i: U32,
273 valid: Model.Balanced(T, d, array)) -> GetFull<T, d, array, i>:
274 get_sized(T, d, array, i, Size.certify(T, d, array, valid))
275
276def get_retained(-T: Data, -d: Nat, -original: Array<T>, -i: U32,
277 cert: GetFull<T, d, original, i>) -> {first(T, Array.get(T, original, i)) == original : Array<T>}:
278 match cert:
279 case GetFull{array, value, equal, kept, observed, valid}:
280 %equal : {first(T, _) == original : Array<T>}
281 kept
282
283def get_observed(-T: Data, -d: Nat, -original: Array<T>, -i: U32,
284 cert: GetFull<T, d, original, i>) ->
285 {Some{second(T, Array.get(T, original, i))} ==
286 Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}:
287 match cert:
288 case GetFull{array, value, equal, kept, observed, valid}:
289 %equal : {Some{second(T, _)} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}
290 observed
291
292def get_balanced(-T: Data, -d: Nat, -original: Array<T>, -i: U32,
293 cert: GetFull<T, d, original, i>) -> Model.Balanced(T, d, first(T, Array.get(T, original, i))):
294 match cert:
295 case GetFull{array, value, equal, kept, observed, valid}:
296 %equal : Model.Balanced(T, d, first(T, _))
297 valid
298
299def law_get_retains(-T: Data, +d: Nat, array: Array<T>, +i: U32,
300 valid: Model.Balanced(T, d, array)) -> {first(T, Array.get(T, array, i)) == array : Array<T>}:
301 get_retained(T, d, array, i, get(T, d, array, i, valid))
302
303def law_get_refines(-T: Data, +d: Nat, array: Array<T>, +i: U32,
304 valid: Model.Balanced(T, d, array)) ->
305 {Some{second(T, Array.get(T, array, i))} == Model.observe(T, d, array, route(d, i)) : Maybe<&2, T>}:
306 get_observed(T, d, array, i, get(T, d, array, i, valid))
307
308def law_get_balanced(-T: Data, +d: Nat, array: Array<T>, +i: U32,
309 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, first(T, Array.get(T, array, i))):
310 get_balanced(T, d, array, i, get(T, d, array, i, valid))
311
312def written_transport(-T: Data, -d: Nat, -array: Array<T>, -original: Array<T>,
313 -n: U32, -i: U32, -new: T, -result: Array<T>,
314 kept: {array == original : Array<T>}, extent: {n == Size.capacity(d) : U32},
315 written: {result == Core.write_path(T, d, array, route_n(d, n, i), new) : Array<T>}) ->
316 {result == Core.write_path(T, d, original, route(d, i), new) : Array<T>}:
317 %kept : {result == Core.write_path(T, d, _, route(d, i), new) : Array<T>}
318 %extent : {result == Core.write_path(T, d, array, route_n(d, _, i), new) : Array<T>}
319 written
320
321type SwapFull<-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T> is Type:
322 SwapFull{array: Array<T>, old: T,
323 equal: {(array, old) == Array.swap(T, original, i, new) : Array<T> & T},
324 written: {array == Core.write_path(T, d, original, route(d, i), new) : Array<T>},
325 observed: {Some{old} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>},
326 balanced: Model.Balanced(T, d, array)}
327
328def swap_final(-T: Data, -d: Nat, -original: Array<T>, -sized_array: Array<T>, -n: U32,
329 -i: U32, -new: T,
330 measured: {(sized_array, n) == Array.size(T, original) : Array<T> & U32},
331 +retained: {sized_array == original : Array<T>}, +extent: {n == Size.capacity(d) : U32},
332 child: Swap<T, d, sized_array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), new>) ->
333 SwapFull<T, d, original, i, new>:
334 match child:
335 case Swap{array, old, equal, written, observed, valid}:
336 SwapFull{array, old,
337 Equal.trans(Array<T> & T, (array, old), Array.swap.at(T, i, new, (sized_array, n)),
338 Array.swap(T, original, i, new), equal,
339 Equal.cong(Array<T> & U32, Array<T> & T, r => Array.swap.at(T, i, new, r),
340 (sized_array, n), Array.size(T, original), measured)),
341 written_transport(T, d, sized_array, original, n, i, new, array, retained, extent, written),
342 observed_transport(T, d, sized_array, original, n, i, old, retained, extent, observed),
343 valid}
344
345def swap_sized(-T: Data, +d: Nat, -original: Array<T>, +i: U32, new: T,
346 sized: Size.Sized<T, d, original>) -> SwapFull<T, d, original, i, new>:
347 match sized:
348 case Size.Sized{array, +n, retained, measured, extent, valid}:
349 swap_final(T, d, original, array, n, i, new, measured, retained, extent,
350 swap_go(T, d, array, n, masked(n, i), new, U32.is_lt(masked(n, i), U32.shr(n)), valid))
351
352def swap(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
353 valid: Model.Balanced(T, d, array)) -> SwapFull<T, d, array, i, new>:
354 swap_sized(T, d, array, i, new, Size.certify(T, d, array, valid))
355
356def swap_written(-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T,
357 cert: SwapFull<T, d, original, i, new>) ->
358 {first(T, Array.swap(T, original, i, new)) == Core.write_path(T, d, original, route(d, i), new) : Array<T>}:
359 match cert:
360 case SwapFull{array, old, equal, written, observed, valid}:
361 %equal : {first(T, _) == Core.write_path(T, d, original, route(d, i), new) : Array<T>}
362 written
363
364def swap_observed(-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T,
365 cert: SwapFull<T, d, original, i, new>) ->
366 {Some{second(T, Array.swap(T, original, i, new))} ==
367 Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}:
368 match cert:
369 case SwapFull{array, old, equal, written, observed, valid}:
370 %equal : {Some{second(T, _)} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}
371 observed
372
373def swap_balanced(-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T,
374 cert: SwapFull<T, d, original, i, new>) ->
375 Model.Balanced(T, d, first(T, Array.swap(T, original, i, new))):
376 match cert:
377 case SwapFull{array, old, equal, written, observed, valid}:
378 %equal : Model.Balanced(T, d, first(T, _))
379 valid
380
381def set_written(-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T,
382 cert: SwapFull<T, d, original, i, new>) ->
383 {Array.set(T, original, i, new) == Core.write_path(T, d, original, route(d, i), new) : Array<T>}:
384 match cert:
385 case SwapFull{array, old, equal, written, observed, valid}:
386 %equal : {Array.set.fin(T, _) == Core.write_path(T, d, original, route(d, i), new) : Array<T>}
387 written
388
389def set_balanced(-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T,
390 cert: SwapFull<T, d, original, i, new>) -> Model.Balanced(T, d, Array.set(T, original, i, new)):
391 match cert:
392 case SwapFull{array, old, equal, written, observed, valid}:
393 %equal : Model.Balanced(T, d, Array.set.fin(T, _))
394 valid
395
396def law_swap_refines(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
397 valid: Model.Balanced(T, d, array)) ->
398 {first(T, Array.swap(T, array, i, new)) == Core.write_path(T, d, array, route(d, i), new) : Array<T>}:
399 swap_written(T, d, array, i, new, swap(T, d, array, i, new, valid))
400
401def law_swap_observed(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
402 valid: Model.Balanced(T, d, array)) ->
403 {Some{second(T, Array.swap(T, array, i, new))} == Model.observe(T, d, array, route(d, i)) : Maybe<&2, T>}:
404 swap_observed(T, d, array, i, new, swap(T, d, array, i, new, valid))
405
406def law_swap_balanced(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
407 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, first(T, Array.swap(T, array, i, new))):
408 swap_balanced(T, d, array, i, new, swap(T, d, array, i, new, valid))
409
410def law_set_refines(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
411 valid: Model.Balanced(T, d, array)) ->
412 {Array.set(T, array, i, new) == Core.write_path(T, d, array, route(d, i), new) : Array<T>}:
413 set_written(T, d, array, i, new, swap(T, d, array, i, new, valid))
414
415def law_set_balanced(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
416 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, Array.set(T, array, i, new)):
417 set_balanced(T, d, array, i, new, swap(T, d, array, i, new, valid))
418
419def law_get_at_refines(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32,
420 valid: Model.Balanced(T, d, array)) ->
421 {Some{second(T, Array.get.at(T, i, (array, n)))} ==
422 Model.observe(T, d, array, route_n(d, n, i)) : Maybe<&2, T>}:
423 get_go_observed(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)),
424 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid))
425
426def law_get_at_retains(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32,
427 valid: Model.Balanced(T, d, array)) ->
428 {first(T, Array.get.at(T, i, (array, n))) == array : Array<T>}:
429 get_go_retained(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)),
430 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid))
431
432def law_get_at_balanced(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32,
433 valid: Model.Balanced(T, d, array)) -> Model.Balanced(T, d, first(T, Array.get.at(T, i, (array, n)))):
434 get_go_balanced(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)),
435 get_go(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), valid))
436
437def law_swap_at_refines(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, new: T,
438 valid: Model.Balanced(T, d, array)) ->
439 {first(T, Array.swap.at(T, i, new, (array, n))) ==
440 Core.write_path(T, d, array, route_n(d, n, i), new) : Array<T>}:
441 swap_go_written(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), new,
442 swap_go(T, d, array, n, masked(n, i), new, U32.is_lt(masked(n, i), U32.shr(n)), valid))
443
444def law_swap_at_balanced(-T: Data, d: Nat, array: Array<T>, +n: U32, +i: U32, new: T,
445 valid: Model.Balanced(T, d, array)) ->
446 Model.Balanced(T, d, first(T, Array.swap.at(T, i, new, (array, n)))):
447 swap_go_balanced(T, d, array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), new,
448 swap_go(T, d, array, n, masked(n, i), new, U32.is_lt(masked(n, i), U32.shr(n)), valid))