def sp.nonempty
bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:621
import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
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
621
622def sp.nonempty(ys: List<&2, U32>) -> {Nat.is_le(16n, B.len(ys)) == True{} : Bool} -> {Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(ys)))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(ys))))} == M.cm.split.blocks(M.cm.split(B.mask(ys))) : List<&2, M.CmBlock>}:
623 match ys:
624 case Nil{}:
625 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Nil{})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Nil{}))))} == M.cm.split.blocks(M.cm.split(B.mask(Nil{}))) : List<&2, M.CmBlock>}, h)
626 case Con{+y0, +r0}:
627 match r0:
628 case Nil{}:
629 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Nil{}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Nil{}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Nil{}}))) : List<&2, M.CmBlock>}, h)
630 case Con{+y1, +r1}:
631 match r1:
632 case Nil{}:
633 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Nil{}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Nil{}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Nil{}}}))) : List<&2, M.CmBlock>}, h)
634 case Con{+y2, +r2}:
635 match r2:
636 case Nil{}:
637 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Nil{}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Nil{}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Nil{}}}}))) : List<&2, M.CmBlock>}, h)
638 case Con{+y3, +r3}:
639 match r3:
640 case Nil{}:
641 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}}))) : List<&2, M.CmBlock>}, h)
642 case Con{+y4, +r4}:
643 match r4:
644 case Nil{}:
645 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}}))) : List<&2, M.CmBlock>}, h)
646 case Con{+y5, +r5}:
647 match r5:
648 case Nil{}:
649 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}}))) : List<&2, M.CmBlock>}, h)
650 case Con{+y6, +r6}:
651 match r6:
652 case Nil{}:
653 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}}))) : List<&2, M.CmBlock>}, h)
654 case Con{+y7, +r7}:
655 match r7:
656 case Nil{}:
657 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
658 case Con{+y8, +r8}:
659 match r8:
660 case Nil{}:
661 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
662 case Con{+y9, +r9}:
663 match r9:
664 case Nil{}:
665 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
666 case Con{+y10, +r10}:
667 match r10:
668 case Nil{}:
669 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
670 case Con{+y11, +r11}:
671 match r11:
672 case Nil{}:
673 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
674 case Con{+y12, +r12}:
675 match r12:
676 case Nil{}:
677 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
678 case Con{+y13, +r13}:
679 match r13:
680 case Nil{}:
681 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
682 case Con{+y14, +r14}:
683 match r14:
684 case Nil{}:
685 h => bo.absurd({Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}}})))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}}}))))} == M.cm.split.blocks(M.cm.split(B.mask(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, Nil{}}}}}}}}}}}}}}}}))) : List<&2, M.CmBlock>}, h)
686 case Con{+y15, +t}:
687 h => %Equal.sym(List<&2, M.CmBlock>, M.cm.split.blocks(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)))), Con{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.blocks(M.cm.split(B.mask(t)))}, sp.cons_blocks(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)))) : {Con{sp.hd(_), sp.tl(_)} == _ : List<&2, M.CmBlock>}
688 {==}