def sp.short_split

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:690

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

690# fewer than 16 bytes are all tail
691def 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}:
692  match ys:
693    case Nil{}:
694      h => {==}
695    case Con{+y0, +r0}:
696      match r0:
697        case Nil{}:
698          h => {==}
699        case Con{+y1, +r1}:
700          match r1:
701            case Nil{}:
702              h => {==}
703            case Con{+y2, +r2}:
704              match r2:
705                case Nil{}:
706                  h => {==}
707                case Con{+y3, +r3}:
708                  match r3:
709                    case Nil{}:
710                      h => {==}
711                    case Con{+y4, +r4}:
712                      match r4:
713                        case Nil{}:
714                          h => {==}
715                        case Con{+y5, +r5}:
716                          match r5:
717                            case Nil{}:
718                              h => {==}
719                            case Con{+y6, +r6}:
720                              match r6:
721                                case Nil{}:
722                                  h => {==}
723                                case Con{+y7, +r7}:
724                                  match r7:
725                                    case Nil{}:
726                                      h => {==}
727                                    case Con{+y8, +r8}:
728                                      match r8:
729                                        case Nil{}:
730                                          h => {==}
731                                        case Con{+y9, +r9}:
732                                          match r9:
733                                            case Nil{}:
734                                              h => {==}
735                                            case Con{+y10, +r10}:
736                                              match r10:
737                                                case Nil{}:
738                                                  h => {==}
739                                                case Con{+y11, +r11}:
740                                                  match r11:
741                                                    case Nil{}:
742                                                      h => {==}
743                                                    case Con{+y12, +r12}:
744                                                      match r12:
745                                                        case Nil{}:
746                                                          h => {==}
747                                                        case Con{+y13, +r13}:
748                                                          match r13:
749                                                            case Nil{}:
750                                                              h => {==}
751                                                            case Con{+y14, +r14}:
752                                                              match r14:
753                                                                case Nil{}:
754                                                                  h => {==}
755                                                                case Con{+y15, +t}:
756                                                                  match t:
757                                                                    case Nil{}:
758                                                                      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)
759                                                                    case Con{+z, +zs}:
760                                                                      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)