def sp.bb16
bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:762
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
762
763def sp.bb16(ys: List<&2, U32>) -> {Nat.is_eq(B.len(ys), 16n) == True{} : Bool} -> {M.cm.bytes_of(M.cm.block_of(ys)) == B.mask(ys) : List<&2, U32>}:
764 match ys:
765 case Nil{}:
766 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Nil{})) == B.mask(Nil{}) : List<&2, U32>}, h)
767 case Con{+y0, +r0}:
768 match r0:
769 case Nil{}:
770 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Nil{}})) == B.mask(Con{y0, Nil{}}) : List<&2, U32>}, h)
771 case Con{+y1, +r1}:
772 match r1:
773 case Nil{}:
774 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Nil{}}})) == B.mask(Con{y0, Con{y1, Nil{}}}) : List<&2, U32>}, h)
775 case Con{+y2, +r2}:
776 match r2:
777 case Nil{}:
778 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Nil{}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Nil{}}}}) : List<&2, U32>}, h)
779 case Con{+y3, +r3}:
780 match r3:
781 case Nil{}:
782 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}}) : List<&2, U32>}, h)
783 case Con{+y4, +r4}:
784 match r4:
785 case Nil{}:
786 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}}) : List<&2, U32>}, h)
787 case Con{+y5, +r5}:
788 match r5:
789 case Nil{}:
790 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}}) : List<&2, U32>}, h)
791 case Con{+y6, +r6}:
792 match r6:
793 case Nil{}:
794 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}}) : List<&2, U32>}, h)
795 case Con{+y7, +r7}:
796 match r7:
797 case Nil{}:
798 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}}) : List<&2, U32>}, h)
799 case Con{+y8, +r8}:
800 match r8:
801 case Nil{}:
802 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}})) == B.mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}}) : List<&2, U32>}, h)
803 case Con{+y9, +r9}:
804 match r9:
805 case Nil{}:
806 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}})) == 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, U32>}, h)
807 case Con{+y10, +r10}:
808 match r10:
809 case Nil{}:
810 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}})) == 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, U32>}, h)
811 case Con{+y11, +r11}:
812 match r11:
813 case Nil{}:
814 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(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{}}}}}}}}}}}}})) == 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, U32>}, h)
815 case Con{+y12, +r12}:
816 match r12:
817 case Nil{}:
818 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(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{}}}}}}}}}}}}}})) == 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, U32>}, h)
819 case Con{+y13, +r13}:
820 match r13:
821 case Nil{}:
822 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(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{}}}}}}}}}}}}}}})) == 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, U32>}, h)
823 case Con{+y14, +r14}:
824 match r14:
825 case Nil{}:
826 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(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{}}}}}}}}}}}}}}}})) == 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, U32>}, h)
827 case Con{+y15, +t}:
828 match t:
829 case Nil{}:
830 h => sp.blk16g(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15, Nil{})
831 case Con{+z, +zs}:
832 h => bo.absurd({M.cm.bytes_of(M.cm.block_of(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}}}}}}}}}}}}}}}}})) == 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, Con{y15, Con{z, zs}}}}}}}}}}}}}}}}}) : List<&2, U32>}, h)