def sp.short_split

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:421

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

421# fewer than 16 bytes are all tail
422def sp.short_split(ys: List<&2, U32>) -> {Nat.is_lt(B.len(ys), 16n) == True{} : Bool} -> {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}:
423  match ys:
424    case Nil{}:
425      h => {==}
426    case Con{+y0, +r0}:
427      match r0:
428        case Nil{}:
429          h => {==}
430        case Con{+y1, +r1}:
431          match r1:
432            case Nil{}:
433              h => {==}
434            case Con{+y2, +r2}:
435              match r2:
436                case Nil{}:
437                  h => {==}
438                case Con{+y3, +r3}:
439                  match r3:
440                    case Nil{}:
441                      h => {==}
442                    case Con{+y4, +r4}:
443                      match r4:
444                        case Nil{}:
445                          h => {==}
446                        case Con{+y5, +r5}:
447                          match r5:
448                            case Nil{}:
449                              h => {==}
450                            case Con{+y6, +r6}:
451                              match r6:
452                                case Nil{}:
453                                  h => {==}
454                                case Con{+y7, +r7}:
455                                  match r7:
456                                    case Nil{}:
457                                      h => {==}
458                                    case Con{+y8, +r8}:
459                                      match r8:
460                                        case Nil{}:
461                                          h => {==}
462                                        case Con{+y9, +r9}:
463                                          match r9:
464                                            case Nil{}:
465                                              h => {==}
466                                            case Con{+y10, +r10}:
467                                              match r10:
468                                                case Nil{}:
469                                                  h => {==}
470                                                case Con{+y11, +r11}:
471                                                  match r11:
472                                                    case Nil{}:
473                                                      h => {==}
474                                                    case Con{+y12, +r12}:
475                                                      match r12:
476                                                        case Nil{}:
477                                                          h => {==}
478                                                        case Con{+y13, +r13}:
479                                                          match r13:
480                                                            case Nil{}:
481                                                              h => {==}
482                                                            case Con{+y14, +r14}:
483                                                              match r14:
484                                                                case Nil{}:
485                                                                  h => {==}
486                                                                case Con{+y15, +t}:
487                                                                  match t:
488                                                                    case Nil{}:
489                                                                      h => bo.absurd({M.cm.split(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Nil{}}}}}}}}}}}}}}}}}) == M.CmSplit{Nil{}, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Nil{}}}}}}}}}}}}}}}}}} : M.CmSplit}, h)
490                                                                    case Con{+z, +zs}:
491                                                                      h => bo.absurd({M.cm.split(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Con{z, zs}}}}}}}}}}}}}}}}}) == M.CmSplit{Nil{}, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Con{z, zs}}}}}}}}}}}}}}}}}} : M.CmSplit}, h)