Blamka.step4_correct: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as Blamka
Lines 35-38 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&start_line=35&end_line=38

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/argon2/blamka.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend as GB

def step4_correct(+v: T.State) -> {I.step4(v) == S.GBi(v, 0n, 5n, 10n, 15n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put4(q, x1,x2,x3,x4,x6,x7,x8,x9,x11,x12,x13,x14), I.gb(x0, x5, x10, x15), S.GB(x0, x5, x10, x15), GB.gb_correct(x0, x5, x10, x15))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend&name=gb_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=GB
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=GBi
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=gb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=put4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Quad
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=State