def shift_rows
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as Aesimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
20# Row r moves r columns to the left.
21def shift_rows(s: T.State) -> T.State:
22 match s:
23 case T.S{T.W{a0, a1, a2, a3}, T.W{b0, b1, b2, b3}, T.W{c0, c1, c2, c3}, T.W{d0, d1, d2, d3}}:
24 T.S{T.W{a0, b1, c2, d3}, T.W{b0, c1, d2, a3}, T.W{c0, d1, a2, b3}, T.W{d0, a1, b2, c3}}
Uses (2)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes:round
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher:shift_rows_ok
- bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes:last_round
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher:last_round_ok
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher:round_ok