PROOF.ap.arkl: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 2079-2098 of bend-osdev-aes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&start_line=2079&end_line=2098

import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-collections@1.0.0.0/src/crypto/aes/aes.bend as A
import bend-collections@1.0.0.0/src/crypto/aes/types.bend as TT

def ap.arkl(+m: TT.State, +k: TT.State) -> {A.add_round_key(X.aes.mask(m), X.aes.mask(k)) == X.aes.mask(A.add_round_key(X.aes.mask(m), X.aes.mask(k))) : TT.State}:
  match m k:
    case TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}} TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}:
      %Equal.sym(U32, U32.xor(U32.and(255, z0), U32.and(255, k0)), U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), ap.xorb(z0, k0)) : {TT.S{TT.W{_, U32.xor(U32.and(255, z1), U32.and(255, k1)), U32.xor(U32.and(255, z2), U32.and(255, k2)), U32.xor(U32.and(255, z3), U32.and(255, k3))}, TT.W{U32.xor(U32.and(255, z4), U32.and(255, k4)), U32.xor(U32.and(255, z5), U32.and(255, k5)), U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z1), U32.and(255, k1)), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), ap.xorb(z1, k1)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), _, U32.xor(U32.and(255, z2), U32.and(255, k2)), U32.xor(U32.and(255, z3), U32.and(255, k3))}, TT.W{U32.xor(U32.and(255, z4), U32.and(255, k4)), U32.xor(U32.and(255, z5), U32.and(255, k5)), U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z2), U32.and(255, k2)), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), ap.xorb(z2, k2)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), _, U32.xor(U32.and(255, z3), U32.and(255, k3))}, TT.W{U32.xor(U32.and(255, z4), U32.and(255, k4)), U32.xor(U32.and(255, z5), U32.and(255, k5)), U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z3), U32.and(255, k3)), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3))), ap.xorb(z3, k3)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), _}, TT.W{U32.xor(U32.and(255, z4), U32.and(255, k4)), U32.xor(U32.and(255, z5), U32.and(255, k5)), U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z4), U32.and(255, k4)), U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), ap.xorb(z4, k4)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{_, U32.xor(U32.and(255, z5), U32.and(255, k5)), U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z5), U32.and(255, k5)), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), ap.xorb(z5, k5)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), _, U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z6), U32.and(255, k6)), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), ap.xorb(z6, k6)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), _, U32.xor(U32.and(255, z7), U32.and(255, k7))}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z7), U32.and(255, k7)), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7))), ap.xorb(z7, k7)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), _}, TT.W{U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z8), U32.and(255, k8)), U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), ap.xorb(z8, k8)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{_, U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z9), U32.and(255, k9)), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), ap.xorb(z9, k9)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), _, U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z10), U32.and(255, k10)), U32.and(255, U32.xor(U32.and(255, z10), U32.and(255, k10))), ap.xorb(z10, k10)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), _, U32.xor(U32.and(255, z11), U32.and(255, k11))}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z11), U32.and(255, k11)), U32.and(255, U32.xor(U32.and(255, z11), U32.and(255, k11))), ap.xorb(z11, k11)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), U32.and(255, U32.xor(U32.and(255, z10), U32.and(255, k10))), _}, TT.W{U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z12), U32.and(255, k12)), U32.and(255, U32.xor(U32.and(255, z12), U32.and(255, k12))), ap.xorb(z12, k12)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), U32.and(255, U32.xor(U32.and(255, z10), U32.and(255, k10))), U32.and(255, U32.xor(U32.and(255, z11), U32.and(255, k11)))}, TT.W{_, U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z13), U32.and(255, k13)), U32.and(255, U32.xor(U32.and(255, z13), U32.and(255, k13))), ap.xorb(z13, k13)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), U32.and(255, U32.xor(U32.and(255, z10), U32.and(255, k10))), U32.and(255, U32.xor(U32.and(255, z11), U32.and(255, k11)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z12), U32.and(255, k12))), _, U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z14), U32.and(255, k14)), U32.and(255, U32.xor(U32.and(255, z14), U32.and(255, k14))), ap.xorb(z14, k14)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), U32.and(255, U32.xor(U32.and(255, z10), U32.and(255, k10))), U32.and(255, U32.xor(U32.and(255, z11), U32.and(255, k11)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z12), U32.and(255, k12))), U32.and(255, U32.xor(U32.and(255, z13), U32.and(255, k13))), _, U32.xor(U32.and(255, z15), U32.and(255, k15))}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      %Equal.sym(U32, U32.xor(U32.and(255, z15), U32.and(255, k15)), U32.and(255, U32.xor(U32.and(255, z15), U32.and(255, k15))), ap.xorb(z15, k15)) : {TT.S{TT.W{U32.and(255, U32.xor(U32.and(255, z0), U32.and(255, k0))), U32.and(255, U32.xor(U32.and(255, z1), U32.and(255, k1))), U32.and(255, U32.xor(U32.and(255, z2), U32.and(255, k2))), U32.and(255, U32.xor(U32.and(255, z3), U32.and(255, k3)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z4), U32.and(255, k4))), U32.and(255, U32.xor(U32.and(255, z5), U32.and(255, k5))), U32.and(255, U32.xor(U32.and(255, z6), U32.and(255, k6))), U32.and(255, U32.xor(U32.and(255, z7), U32.and(255, k7)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z8), U32.and(255, k8))), U32.and(255, U32.xor(U32.and(255, z9), U32.and(255, k9))), U32.and(255, U32.xor(U32.and(255, z10), U32.and(255, k10))), U32.and(255, U32.xor(U32.and(255, z11), U32.and(255, k11)))}, TT.W{U32.and(255, U32.xor(U32.and(255, z12), U32.and(255, k12))), U32.and(255, U32.xor(U32.and(255, z13), U32.and(255, k13))), U32.and(255, U32.xor(U32.and(255, z14), U32.and(255, k14))), _}} == X.aes.mask(A.add_round_key(X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}), X.aes.mask(TT.S{TT.W{k0, k1, k2, k3}, TT.W{k4, k5, k6, k7}, TT.W{k8, k9, k10, k11}, TT.W{k12, k13, k14, k15}}))) : TT.State}
      {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=add_round_key
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=Quad
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xorb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask