Index.addresses_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend as Index
Lines 199-205 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend&start_line=199&end_line=205

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/src/crypto/argon2/argon2.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as BL

def addresses_eq(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> {I.addresses(r, l, s, mm, t, ctr) == SA.addresses(r, l, s, mm, t, ctr) : A.Block}:
  +z = SA.input_block(r, l, s, mm, t, ctr)
  Equal.trans(A.Block, G.compress(G.zero(), G.compress(G.zero(), I.input_block(r, l, s, mm, t, ctr))), G.compress(G.zero(), G.compress(G.zero(), z)), SG.G(SG.zero(), SG.G(SG.zero(), z)),
    Equal.cong(A.Block, A.Block, x => G.compress(G.zero(), G.compress(G.zero(), x)), I.input_block(r, l, s, mm, t, ctr), z, input_eq(r, l, s, mm, t, ctr)),
    Equal.trans(A.Block, G.compress(G.zero(), G.compress(G.zero(), z)), G.compress(G.zero(), SG.G(SG.zero(), z)), SG.G(SG.zero(), SG.G(SG.zero(), z)),
      Equal.cong(A.Block, A.Block, x => G.compress(G.zero(), x), G.compress(G.zero(), z), SG.G(SG.zero(), z), BL.compress_correct(G.zero(), z)),
      BL.compress_correct(G.zero(), SG.G(SG.zero(), z))))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=compress_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend&name=input_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=addresses
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=input_block
  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=zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=addresses
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=input_block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=compress
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block