def sp.tail_short

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

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

483# the tail of a split has fewer than 16 bytes
484def sp.tail_short(ys: List<&2, U32>) -> {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}:
485  match ys:
486    case Nil{}:
487      {==}
488    case Con{+y0, +r0}:
489      match r0:
490        case Nil{}:
491          {==}
492        case Con{+y1, +r1}:
493          match r1:
494            case Nil{}:
495              {==}
496            case Con{+y2, +r2}:
497              match r2:
498                case Nil{}:
499                  {==}
500                case Con{+y3, +r3}:
501                  match r3:
502                    case Nil{}:
503                      {==}
504                    case Con{+y4, +r4}:
505                      match r4:
506                        case Nil{}:
507                          {==}
508                        case Con{+y5, +r5}:
509                          match r5:
510                            case Nil{}:
511                              {==}
512                            case Con{+y6, +r6}:
513                              match r6:
514                                case Nil{}:
515                                  {==}
516                                case Con{+y7, +r7}:
517                                  match r7:
518                                    case Nil{}:
519                                      {==}
520                                    case Con{+y8, +r8}:
521                                      match r8:
522                                        case Nil{}:
523                                          {==}
524                                        case Con{+y9, +r9}:
525                                          match r9:
526                                            case Nil{}:
527                                              {==}
528                                            case Con{+y10, +r10}:
529                                              match r10:
530                                                case Nil{}:
531                                                  {==}
532                                                case Con{+y11, +r11}:
533                                                  match r11:
534                                                    case Nil{}:
535                                                      {==}
536                                                    case Con{+y12, +r12}:
537                                                      match r12:
538                                                        case Nil{}:
539                                                          {==}
540                                                        case Con{+y13, +r13}:
541                                                          match r13:
542                                                            case Nil{}:
543                                                              {==}
544                                                            case Con{+y14, +r14}:
545                                                              match r14:
546                                                                case Nil{}:
547                                                                  {==}
548                                                                case Con{+y15, +t}:
549                                                                  %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {Nat.is_lt(B.len(_), 16n) == True{} : Bool}
550                                                                  sp.tail_short(t)