def cancel13

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

188def cancel13(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +x11: U32, +x12: 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, +k12: 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), U32.xor(U32.xor(x12, k12), k12)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}:
189  %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), U32.xor(U32.xor(x12, k12), k12)] == [_, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
190  %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(x12, k12), k12)] == [U32.xor(U32.xor(x0, k0), k0), _, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
191  %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(x12, k12), k12)] == [U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), _, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
192  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
193  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
194  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
195  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
196  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
197  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
198  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
199  %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(x12, k12), k12)] == [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, x12] : List<&2, U32>}
200  %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(x12, k12), k12)] == [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), _, x12] : List<&2, U32>}
201  %xor_inv(x12, k12) : {[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(x12, k12), k12)] == [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), _] : List<&2, U32>}
202  {==}
Uses (4)

Used by (1)

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