src/storage/route.bend
bendtorch-core@0.1.0.0 · 361 lines · 16 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/size.bend as Size
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
6import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
7
8def cap_unit(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {U32{Arith.unit(32n, d)} == Size.capacity(d) : U32}:
9 match d:
10 case 0n:
11 {==}
12 case 1n+d1:
13 match d1:
14 case 0n:
15 {==}
16 case 1n+d2:
17 match d2:
18 case 0n:
19 {==}
20 case 1n+d3:
21 match d3:
22 case 0n:
23 {==}
24 case 1n+d4:
25 match d4:
26 case 0n:
27 {==}
28 case 1n+d5:
29 match d5:
30 case 0n:
31 {==}
32 case 1n+d6:
33 match d6:
34 case 0n:
35 {==}
36 case 1n+d7:
37 match d7:
38 case 0n:
39 {==}
40 case 1n+d8:
41 match d8:
42 case 0n:
43 {==}
44 case 1n+d9:
45 match d9:
46 case 0n:
47 {==}
48 case 1n+d10:
49 match d10:
50 case 0n:
51 {==}
52 case 1n+d11:
53 match d11:
54 case 0n:
55 {==}
56 case 1n+d12:
57 match d12:
58 case 0n:
59 {==}
60 case 1n+d13:
61 match d13:
62 case 0n:
63 {==}
64 case 1n+d14:
65 match d14:
66 case 0n:
67 {==}
68 case 1n+d15:
69 match d15:
70 case 0n:
71 {==}
72 case 1n+d16:
73 match d16:
74 case 0n:
75 {==}
76 case 1n+d17:
77 match d17:
78 case 0n:
79 {==}
80 case 1n+d18:
81 match d18:
82 case 0n:
83 {==}
84 case 1n+d19:
85 match d19:
86 case 0n:
87 {==}
88 case 1n+d20:
89 match d20:
90 case 0n:
91 {==}
92 case 1n+d21:
93 Empty.absurd({U32{Arith.unit(32n, 21n+d21)} == Size.capacity(21n+d21) : U32}, Arith.clash(h))
94
95def shr_cap(+d: Nat, +h: {Nat.is_le(1n+d, 20n) == True{} : Bool}) -> {Size.capacity(d) == U32.shr(Size.capacity(1n+d)) : U32}:
96 match d:
97 case 0n:
98 {==}
99 case 1n+d1:
100 match d1:
101 case 0n:
102 {==}
103 case 1n+d2:
104 match d2:
105 case 0n:
106 {==}
107 case 1n+d3:
108 match d3:
109 case 0n:
110 {==}
111 case 1n+d4:
112 match d4:
113 case 0n:
114 {==}
115 case 1n+d5:
116 match d5:
117 case 0n:
118 {==}
119 case 1n+d6:
120 match d6:
121 case 0n:
122 {==}
123 case 1n+d7:
124 match d7:
125 case 0n:
126 {==}
127 case 1n+d8:
128 match d8:
129 case 0n:
130 {==}
131 case 1n+d9:
132 match d9:
133 case 0n:
134 {==}
135 case 1n+d10:
136 match d10:
137 case 0n:
138 {==}
139 case 1n+d11:
140 match d11:
141 case 0n:
142 {==}
143 case 1n+d12:
144 match d12:
145 case 0n:
146 {==}
147 case 1n+d13:
148 match d13:
149 case 0n:
150 {==}
151 case 1n+d14:
152 match d14:
153 case 0n:
154 {==}
155 case 1n+d15:
156 match d15:
157 case 0n:
158 {==}
159 case 1n+d16:
160 match d16:
161 case 0n:
162 {==}
163 case 1n+d17:
164 match d17:
165 case 0n:
166 {==}
167 case 1n+d18:
168 match d18:
169 case 0n:
170 {==}
171 case 1n+d19:
172 match d19:
173 case 0n:
174 {==}
175 case 1n+d20:
176 Empty.absurd({Size.capacity(20n+d20) == U32.shr(Size.capacity(1n+20n+d20)) : U32}, Arith.clash(h))
177
178def mask_cap(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {U32{Arith.low(32n, d)} == U32.sub(Size.capacity(d), 1) : U32}:
179 match d:
180 case 0n:
181 {==}
182 case 1n+d1:
183 match d1:
184 case 0n:
185 {==}
186 case 1n+d2:
187 match d2:
188 case 0n:
189 {==}
190 case 1n+d3:
191 match d3:
192 case 0n:
193 {==}
194 case 1n+d4:
195 match d4:
196 case 0n:
197 {==}
198 case 1n+d5:
199 match d5:
200 case 0n:
201 {==}
202 case 1n+d6:
203 match d6:
204 case 0n:
205 {==}
206 case 1n+d7:
207 match d7:
208 case 0n:
209 {==}
210 case 1n+d8:
211 match d8:
212 case 0n:
213 {==}
214 case 1n+d9:
215 match d9:
216 case 0n:
217 {==}
218 case 1n+d10:
219 match d10:
220 case 0n:
221 {==}
222 case 1n+d11:
223 match d11:
224 case 0n:
225 {==}
226 case 1n+d12:
227 match d12:
228 case 0n:
229 {==}
230 case 1n+d13:
231 match d13:
232 case 0n:
233 {==}
234 case 1n+d14:
235 match d14:
236 case 0n:
237 {==}
238 case 1n+d15:
239 match d15:
240 case 0n:
241 {==}
242 case 1n+d16:
243 match d16:
244 case 0n:
245 {==}
246 case 1n+d17:
247 match d17:
248 case 0n:
249 {==}
250 case 1n+d18:
251 match d18:
252 case 0n:
253 {==}
254 case 1n+d19:
255 match d19:
256 case 0n:
257 {==}
258 case 1n+d20:
259 match d20:
260 case 0n:
261 {==}
262 case 1n+d21:
263 Empty.absurd({U32{Arith.low(32n, 21n+d21)} == U32.sub(Size.capacity(21n+d21), 1) : U32}, Arith.clash(h))
264
265def cap_nat(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {Model.capacity(d) == U32.to_nat(Size.capacity(d)) : Nat}:
266 %cap_unit(d, h) : {Model.capacity(d) == U32.to_nat(_) : Nat}
267 Arith.unit_nat(32n, d, Arith.lt_le_trans(d, 21n, 32n, Arith.lt_succ(d, 20n, h), {==}))
268
269def cap_word(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {U32.to_nat(Size.capacity(d)) == Model.capacity(d) : Nat}:
270 Equal.sym(Nat, Model.capacity(d), U32.to_nat(Size.capacity(d)), cap_nat(d, h))
271
272def low_inside(+p: Nat, +i: U32, +h: {Nat.is_le(1n+p, 20n) == True{} : Bool},
273 +dz: {True{} == U32.is_lt(i, U32.shr(Size.capacity(1n+p))) : Bool}) ->
274 {Nat.is_lt(U32.to_nat(i), Model.capacity(p)) == True{} : Bool}:
275 +hp = Arith.le_succ(p, 19n, h)
276 %cap_word(p, hp) : {Nat.is_lt(U32.to_nat(i), _) == True{} : Bool}
277 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), U32.to_nat(Size.capacity(p))), U32.is_lt(i, Size.capacity(p)), Arith.u32_lt(i, Size.capacity(p))) : {_ == True{} : Bool}
278 %Equal.sym(U32, Size.capacity(p), U32.shr(Size.capacity(1n+p)), shr_cap(p, h)) : {U32.is_lt(i, _) == True{} : Bool}
279 Equal.sym(Bool, True{}, U32.is_lt(i, U32.shr(Size.capacity(1n+p))), dz)
280
281def high_not_lt(+p: Nat, +i: U32, +h: {Nat.is_le(1n+p, 20n) == True{} : Bool},
282 +dz: {False{} == U32.is_lt(i, U32.shr(Size.capacity(1n+p))) : Bool}) ->
283 {Nat.is_lt(U32.to_nat(i), U32.to_nat(Size.capacity(p))) == False{} : Bool}:
284 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), U32.to_nat(Size.capacity(p))), U32.is_lt(i, Size.capacity(p)), Arith.u32_lt(i, Size.capacity(p))) : {_ == False{} : Bool}
285 %Equal.sym(U32, Size.capacity(p), U32.shr(Size.capacity(1n+p)), shr_cap(p, h)) : {U32.is_lt(i, _) == False{} : Bool}
286 Equal.sym(Bool, False{}, U32.is_lt(i, U32.shr(Size.capacity(1n+p))), dz)
287
288
289def high_le(+p: Nat, +i: U32, +h: {Nat.is_le(1n+p, 20n) == True{} : Bool},
290 +dz: {False{} == U32.is_lt(i, U32.shr(Size.capacity(1n+p))) : Bool}) ->
291 {Nat.is_le(U32.to_nat(Size.capacity(p)), U32.to_nat(i)) == True{} : Bool}:
292 Arith.not_lt_le(U32.to_nat(i), U32.to_nat(Size.capacity(p)), high_not_lt(p, i, h, dz))
293
294def high_split(+p: Nat, +i: U32, +hp: {Nat.is_le(p, 20n) == True{} : Bool},
295 +le: {Nat.is_le(U32.to_nat(Size.capacity(p)), U32.to_nat(i)) == True{} : Bool}) ->
296 {U32.to_nat(i) == Nat.add(Model.capacity(p), U32.to_nat(U32.sub(i, Size.capacity(p)))) : Nat}:
297 %cap_word(p, hp) : {U32.to_nat(i) == Nat.add(_, U32.to_nat(U32.sub(i, Size.capacity(p)))) : Nat}
298 Arith.sub_u32(i, Size.capacity(p), le)
299
300def high_sum(+p: Nat, +i: U32, +hp: {Nat.is_le(p, 20n) == True{} : Bool},
301 +le: {Nat.is_le(U32.to_nat(Size.capacity(p)), U32.to_nat(i)) == True{} : Bool},
302 +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(1n+p)) == True{} : Bool}) ->
303 {Nat.is_lt(Nat.add(Model.capacity(p), U32.to_nat(U32.sub(i, Size.capacity(p)))), Nat.add(Model.capacity(p), Model.capacity(p))) == True{} : Bool}:
304 %high_split(p, i, hp, le) : {Nat.is_lt(_, Nat.add(Model.capacity(p), Model.capacity(p))) == True{} : Bool}
305 inside
306
307def high_inside(+p: Nat, +i: U32, +hp: {Nat.is_le(p, 20n) == True{} : Bool},
308 +le: {Nat.is_le(U32.to_nat(Size.capacity(p)), U32.to_nat(i)) == True{} : Bool},
309 +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(1n+p)) == True{} : Bool}) ->
310 {Nat.is_lt(U32.to_nat(U32.sub(i, Size.capacity(p))), Model.capacity(p)) == True{} : Bool}:
311 Arith.lt_add_cancel(Model.capacity(p), U32.to_nat(U32.sub(i, Size.capacity(p))), Model.capacity(p),
312 high_sum(p, i, hp, le, inside))
313
314def trace_offset(+d: Nat, +i: U32, z: Bool, +dz: {z == U32.is_lt(i, U32.shr(Size.capacity(d))) : Bool},
315 +h: {Nat.is_le(d, 20n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}) ->
316 {U32.to_nat(i) == Model.offset(d, Refinement.trace(d, Size.capacity(d), i, z)) : Nat}:
317 match d:
318 case 0n:
319 Equal.sym(Nat, 0n, U32.to_nat(i), Arith.lt_one(U32.to_nat(i), inside))
320 case 1n+p:
321 match z:
322 case True{}:
323 +hp = Arith.le_succ(p, 19n, h)
324 %shr_cap(p, h) : {U32.to_nat(i) == Model.offset(p, Refinement.trace(p, _, i, U32.is_lt(i, U32.shr(_)))) : Nat}
325 trace_offset(p, i, U32.is_lt(i, U32.shr(Size.capacity(p))), {==}, hp, low_inside(p, i, h, dz))
326 case False{}:
327 +hp = Arith.le_succ(p, 19n, h)
328 +le = high_le(p, i, h, dz)
329 %shr_cap(p, h) : {U32.to_nat(i) == Nat.add(Model.capacity(p), Model.offset(p, Refinement.trace(p, _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_))))) : Nat}
330 +j = U32.sub(i, Size.capacity(p))
331 %trace_offset(p, j, U32.is_lt(j, U32.shr(Size.capacity(p))), {==}, hp, high_inside(p, i, hp, le, inside)) : {U32.to_nat(i) == Nat.add(Model.capacity(p), _) : Nat}
332 high_split(p, i, hp, le)
333
334def mask_u32(+d: Nat, +i: U32, +h: {Nat.is_le(d, 20n) == True{} : Bool},
335 +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}) ->
336 {i == U32.and(i, U32.sub(Size.capacity(d), 1)) : U32}:
337 match i:
338 case U32{+x}:
339 %mask_cap(d, h) : {U32{x} == U32.and(U32{x}, _) : U32}
340 %Arith.mask_word(32n, d, x, inside) : {U32{x} == U32{_} : U32}
341 {==}
342
343def route_offset(+d: Nat, +i: U32, +h: {Nat.is_le(d, 20n) == True{} : Bool},
344 +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}) ->
345 {U32.to_nat(i) == Model.offset(d, Refinement.route(d, i)) : Nat}:
346 %mask_u32(d, i, h, inside) : {U32.to_nat(i) == Model.offset(d, Refinement.trace(d, Size.capacity(d), _, U32.is_lt(_, U32.shr(Size.capacity(d))))) : Nat}
347 trace_offset(d, i, U32.is_lt(i, U32.shr(Size.capacity(d))), {==}, h, inside)
348
349def index_complete(+d: Nat, +n: Nat, +i: U32, +fits: {Storage.bounds(d, n) == True{} : Bool},
350 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> {True{} == Storage.index_matches(d, n, i) : Bool}:
351 +depth = Arith.and_left(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), fits)
352 +rest = Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), fits)
353 +full = Arith.and_right(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)), rest)
354 +slot = Arith.lt_le_trans(U32.to_nat(i), n, Model.capacity(d), inside, full)
355 %route_offset(d, i, depth, slot) : {True{} == Bool.and(Nat.is_eq(_, U32.to_nat(i)), Nat.is_lt(_, n)) : Bool}
356 %Equal.sym(Bool, Nat.is_eq(U32.to_nat(i), U32.to_nat(i)), True{}, Arith.eq_refl(U32.to_nat(i))) : {True{} == Bool.and(_, Nat.is_lt(U32.to_nat(i), n)) : Bool}
357 Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), True{}, inside)
358
359def index_matched(+d: Nat, +n: Nat, +i: U32, +fits: {Storage.bounds(d, n) == True{} : Bool},
360 +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) -> {Storage.index_matches(d, n, i) == True{} : Bool}:
361 Equal.sym(Bool, True{}, Storage.index_matches(d, n, i), index_complete(d, n, i, fits, inside))