Aes.transform: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as Aes
Lines 212-231 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&start_line=212&end_line=231

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T

# The transformation of temp = w[i-1] in Figure 11, by k = i mod Nk,
# big = (Nk > 6) and q = i / Nk.
def transform(k: Nat, big: Bool, +q: Nat, temp: T.Quad) -> T.Quad:
  match k:
    case 0n:
      xor_word(sub_word(rot_word(temp)), rcon(q))
    case 1n:
      temp
    case 2n:
      temp
    case 3n:
      temp
    case 4n:
      match big:
        case True{}:
          sub_word(temp)
        case False{}:
          temp
    case 5n+p:
      temp

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=rcon
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=rot_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=sub_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=xor_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend&name=Quad