Gb.gb2_correct: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend as Gb
Lines 103-110 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&start_line=103&end_line=110

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/lane.bend as L
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/blake/blake2b.bend as B
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as S

def gb2_correct(+a1: T.Lane, +b: T.Lane, +c1: T.Lane, +d1: T.Lane) -> {I.gb2(a1, b, c1, d1) == m2(a1, b, c1, d1) : T.Quad}:
  +bi = L.rot24(L.xor(b, c1))
  +bs = B.rotr(B.xor(b, c1), 24n)
  Equal.trans(T.Quad, I.gb3(I.bla(a1, bi), bi, c1, d1), I.gb3(I.bla(a1, bs), bs, c1, d1), m3(S.fBlaMka(a1, bs), bs, c1, d1),
    Equal.cong(T.Lane, T.Quad, +z => I.gb3(I.bla(a1, z), z, c1, d1), bi, bs, rx24(b, c1)),
    Equal.trans(T.Quad, I.gb3(I.bla(a1, bs), bs, c1, d1), I.gb3(S.fBlaMka(a1, bs), bs, c1, d1), m3(S.fBlaMka(a1, bs), bs, c1, d1),
      Equal.cong(T.Lane, T.Quad, z => I.gb3(z, bs, c1, d1), I.bla(a1, bs), S.fBlaMka(a1, bs), bla_correct(a1, bs)),
      gb3_correct(S.fBlaMka(a1, bs), bs, c1, d1)))

Uses (17):
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&name=bla_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&name=gb3_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&name=m2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&name=m3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&name=rx24
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=fBlaMka
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend&name=rotr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend&name=xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=bla
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=gb2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=gb3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/lane.bend&name=rot24
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/lane.bend&name=xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Lane
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Quad