Blamka.p_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 55-71 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=55&end_line=71

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

# P, one GB at a time.
def p_correct(+v: T.State) -> {I.p(v) == S.P(v) : T.State}:
  Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(I.step0(v)))))))), I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(S.GBi(v, 0n, 4n, 8n, 12n)))))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(z))))))), I.step0(v), S.GBi(v, 0n, 4n, 8n, 12n), step0_correct(v)),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(S.GBi(v, 0n, 4n, 8n, 12n)))))))), I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n))))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(z)))))), I.step1(S.GBi(v, 0n, 4n, 8n, 12n)), S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), step1_correct(S.GBi(v, 0n, 4n, 8n, 12n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n))))))), I.step7(I.step6(I.step5(I.step4(I.step3(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n)))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(I.step3(z))))), I.step2(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n)), S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), step2_correct(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n)))))), I.step7(I.step6(I.step5(I.step4(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(z)))), I.step3(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n)), S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), step3_correct(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n))))), I.step7(I.step6(I.step5(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n)))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(z))), I.step4(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), step4_correct(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n)))), I.step7(I.step6(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(z)), I.step5(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), step5_correct(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n))),
    Equal.trans(T.State, I.step7(I.step6(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n))), I.step7(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(z), I.step6(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), step6_correct(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n))),
    step7_correct(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n)))))))))

Uses (22):
  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/blamka.bend&name=step0_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step1_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step2_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step3_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step4_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step5_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step6_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=step7_correct
  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/spec/crypto/argon2/blamka.bend&name=P
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=p
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step3
  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/argon2/blamka.bend&name=step5
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step6
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=step7
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=State