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

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.mixl(+s: TT.State) -> {A.mix_columns(X.aes.mask(s)) == X.aes.mask(A.mix_columns(X.aes.mask(s))) : TT.State}:
  match s:
    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}}:
      %Equal.sym(TT.Quad, A.mix_column(TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)})), ap.mixcb(z0, z1, z2, z3)) : {TT.S{_, A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}), A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}), A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)})} == X.aes.mask(A.mix_columns(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}}))) : TT.State}
      %Equal.sym(TT.Quad, A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)})), ap.mixcb(z4, z5, z6, z7)) : {TT.S{X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)})), _, A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}), A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)})} == X.aes.mask(A.mix_columns(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}}))) : TT.State}
      %Equal.sym(TT.Quad, A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)})), ap.mixcb(z8, z9, z10, z11)) : {TT.S{X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)})), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)})), _, A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)})} == X.aes.mask(A.mix_columns(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}}))) : TT.State}
      %Equal.sym(TT.Quad, A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)}), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)})), ap.mixcb(z12, z13, z14, z15)) : {TT.S{X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)})), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)})), X.aes.mask_w(A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)})), _} == X.aes.mask(A.mix_columns(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}}))) : 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.and
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=mix_column
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=mix_columns
  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.mixcb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask_w