+ /* Here's the pattern of key, constant, nonce, and counter pieces in the
+ * matrix, before and after our permutation.
+ *
+ * [ C0 K0 K1 K2 ] [ C0 C1 C2 C3 ]
+ * [ K3 C1 N0 N1 ] --> [ K3 T1 K7 K2 ]
+ * [ T0 T1 C2 K4 ] [ T0 K6 K1 N1 ]
+ * [ K5 K6 K7 C3 ] [ K5 K0 N0 K4 ]
+ */
+
+ a[13] = LOAD32_L(k + 0);
+ a[10] = LOAD32_L(k + 4);