def cancel12

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:173
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as Aead
import Base

173def cancel12(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +x11: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, +k8: U32, +k9: U32, +k10: U32, +k11: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}:
174  %xor_inv(x0, k0) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [_, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
175  %xor_inv(x1, k1) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), _, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
176  %xor_inv(x2, k2) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), _, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
177  %xor_inv(x3, k3) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), _, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
178  %xor_inv(x4, k4) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), _, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
179  %xor_inv(x5, k5) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), _, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
180  %xor_inv(x6, k6) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), _, x7, x8, x9, x10, x11] : List<&2, U32>}
181  %xor_inv(x7, k7) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), _, x8, x9, x10, x11] : List<&2, U32>}
182  %xor_inv(x8, k8) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), _, x9, x10, x11] : List<&2, U32>}
183  %xor_inv(x9, k9) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), _, x10, x11] : List<&2, U32>}
184  %xor_inv(x10, k10) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), _, x11] : List<&2, U32>}
185  %xor_inv(x11, k11) : {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), _] : List<&2, U32>}
186  {==}
Uses (4)

Used by (1)

bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead:gctr_inv