Laws.compress_xor_correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/laws.bend as Laws
Lines 37-41 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/laws.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/laws.bend&start_line=37&end_line=41

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 G
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG

law compress_xor_correct:
  for +x: A.Block
  for +y: A.Block
  for +old: A.Block
  {G.compress_xor(x, y, old) == SG.xor(SG.G(x, y), old) : A.Block}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=compress_xor_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=G
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=compress_xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block