1	import Base
2	import ./model.bend as Model
3	import ./size.bend as Size
4	import ./refinement.bend as Refinement
5	import ./main.bend as Storage
6	import ./arith.bend as Arith
7	
8	def 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	
95	def 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	
178	def 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	
265	def 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	
269	def 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	
272	def 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	
281	def 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	
289	def 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	
294	def 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	
300	def 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	
307	def 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	
314	def 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	
334	def 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	
343	def 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	
349	def 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	
359	def 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))