def compress_xor_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/blamka.bend:143

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as S

143# Version 0x13 passes after the first: G(X, Y) XOR the old block.
144def compress_xor_correct(+x: A.Block, +y: A.Block, +old: A.Block) -> {I.compress_xor(x, y, old) == S.xor(S.G(x, y), old) : A.Block}:
145  Equal.trans(A.Block, I.xor(I.compress(x, y), old), I.xor(S.G(x, y), old), S.xor(S.G(x, y), old),
146    Equal.cong(A.Block, A.Block, z => I.xor(z, old), I.compress(x, y), S.G(x, y), compress_correct(x, y)),
147    xor_correct(S.G(x, y), old))