CurrentRoundKey[3:0] : bits(128) -> bits(128) function aes_subbytes_inv(x) = { foreach (i from 0 to 7) output[i] = x[7-i]); output /* Return value */ } /* 8-bit to 32-bit partial AES Mix Column - inverse*/ val aes_mixcolumn_byte_inv