def ap.ark2

bend-osdev-aes@0.1.0.0 · PROOF.bend:1967
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
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

1967def ap.ark2(+m: TT.State, +k: TT.State) -> {A.add_round_key(A.add_round_key(m, k), k) == m : TT.State}:
1968  match m k:
1969    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}}:
1970      %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}
1971      %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}
1972      %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}
1973      %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}
1974      %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}
1975      %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}
1976      %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}
1977      %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}
1978      %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}
1979      %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}
1980      %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}
1981      %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}
1982      %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}
1983      %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}
1984      %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}
1985      %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}
1986      {==}
def ap.ark2

Uses (7)

Used by (3)
