def mask_cap

bendtorch-core@0.1.0.0 · src/storage/route.bend:178

import Base
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

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))