def ap.mixcb

bend-osdev-aes@0.1.0.0 · PROOF.bend:1958

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
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB

1958def ap.mixcb(+a: U32, +b: U32, +c: U32, +d: U32) -> {A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)}) == X.aes.mask_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) : TT.Quad}:
1959  %Equal.sym(U32, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d)), U32.and(255, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))), ap.isb(U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d)), U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d)), ap.rowb0(a, b, c, d))) : {TT.W{_, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d)), U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))), U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))} == X.aes.mask_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) : TT.Quad}
1960  %Equal.sym(U32, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d)), U32.and(255, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d))), ap.isb(U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d)), U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d)), ap.rowb1(a, b, c, d))) : {TT.W{U32.and(255, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))), _, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))), U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))} == X.aes.mask_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) : TT.Quad}
1961  %Equal.sym(U32, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))), U32.and(255, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d)))), ap.isb(U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))), U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d)))), ap.rowb2(a, b, c, d))) : {TT.W{U32.and(255, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))), U32.and(255, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d))), _, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))} == X.aes.mask_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) : TT.Quad}
1962  %Equal.sym(U32, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d))), U32.and(255, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), ap.isb(U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d))), U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.mul3(U32.and(255, a))), U32.and(255, b))), U32.and(255, c))), U32.and(255, SB.xtime(U32.and(255, d)))), ap.rowb3(a, b, c, d))) : {TT.W{U32.and(255, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))), U32.and(255, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d))), U32.and(255, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d)))), _} == X.aes.mask_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) : TT.Quad}
1963  {==}