def p_correct
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/blamka.bend:55
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as Blamka
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
55
56def p_correct(+v: T.State) -> {I.p(v) == S.P(v) : T.State}:
57 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),
58 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)),
59 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),
60 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))),
61 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),
62 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))),
63 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),
64 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))),
65 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),
66 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))),
67 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),
68 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))),
69 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),
70 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))),
71 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)))))))))