PROOF.ap.ark2: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 1967-1986 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=1967&end_line=1986

import Base
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.ark2(+m: TT.State, +k: TT.State) -> {A.add_round_key(A.add_round_key(m, k), k) == m : 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.xor(z0, k0), k0), z0, bx.ru32(z0, k0)) : {TT.S{TT.W{_, U32.xor(U32.xor(z1, k1), k1), U32.xor(U32.xor(z2, k2), k2), U32.xor(U32.xor(z3, k3), k3)}, TT.W{U32.xor(U32.xor(z4, k4), k4), U32.xor(U32.xor(z5, k5), k5), U32.xor(U32.xor(z6, k6), k6), U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z1, k1), k1), z1, bx.ru32(z1, k1)) : {TT.S{TT.W{z0, _, U32.xor(U32.xor(z2, k2), k2), U32.xor(U32.xor(z3, k3), k3)}, TT.W{U32.xor(U32.xor(z4, k4), k4), U32.xor(U32.xor(z5, k5), k5), U32.xor(U32.xor(z6, k6), k6), U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z2, k2), k2), z2, bx.ru32(z2, k2)) : {TT.S{TT.W{z0, z1, _, U32.xor(U32.xor(z3, k3), k3)}, TT.W{U32.xor(U32.xor(z4, k4), k4), U32.xor(U32.xor(z5, k5), k5), U32.xor(U32.xor(z6, k6), k6), U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z3, k3), k3), z3, bx.ru32(z3, k3)) : {TT.S{TT.W{z0, z1, z2, _}, TT.W{U32.xor(U32.xor(z4, k4), k4), U32.xor(U32.xor(z5, k5), k5), U32.xor(U32.xor(z6, k6), k6), U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z4, k4), k4), z4, bx.ru32(z4, k4)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{_, U32.xor(U32.xor(z5, k5), k5), U32.xor(U32.xor(z6, k6), k6), U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z5, k5), k5), z5, bx.ru32(z5, k5)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, _, U32.xor(U32.xor(z6, k6), k6), U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z6, k6), k6), z6, bx.ru32(z6, k6)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, _, U32.xor(U32.xor(z7, k7), k7)}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z7, k7), k7), z7, bx.ru32(z7, k7)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, _}, TT.W{U32.xor(U32.xor(z8, k8), k8), U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z8, k8), k8), z8, bx.ru32(z8, k8)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{_, U32.xor(U32.xor(z9, k9), k9), U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z9, k9), k9), z9, bx.ru32(z9, k9)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, _, U32.xor(U32.xor(z10, k10), k10), U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z10, k10), k10), z10, bx.ru32(z10, k10)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, _, U32.xor(U32.xor(z11, k11), k11)}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z11, k11), k11), z11, bx.ru32(z11, k11)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, _}, TT.W{U32.xor(U32.xor(z12, k12), k12), U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z12, k12), k12), z12, bx.ru32(z12, k12)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{_, U32.xor(U32.xor(z13, k13), k13), U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z13, k13), k13), z13, bx.ru32(z13, k13)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, _, U32.xor(U32.xor(z14, k14), k14), U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z14, k14), k14), z14, bx.ru32(z14, k14)) : {TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, _, U32.xor(U32.xor(z15, k15), k15)}} == 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.State}
      %Equal.sym(U32, U32.xor(U32.xor(z15, k15), k15), z15, bx.ru32(z15, k15)) : {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, _}} == 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.State}
      {==}

Uses (7):
  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.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=bx.ru32