def step2_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/blamka.bend:25

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

25def step2_correct(+v: T.State) -> {I.step2(v) == S.GBi(v, 2n, 6n, 10n, 14n) : T.State}:
26  match v:
27    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
28      Equal.cong(T.Quad, T.State, q => I.put2(q, x0,x1,x3,x4,x5,x7,x8,x9,x11,x12,x13,x15), I.gb(x2, x6, x10, x14), S.GB(x2, x6, x10, x14), GB.gb_correct(x2, x6, x10, x14))