def bla_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/gb.bend:46

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/argon2/blamka.bend as S

46# fBlaMka
47def bla_correct(+x: T.Lane, +y: T.Lane) -> {I.bla(x, y) == S.fBlaMka(x, y) : T.Lane}:
48  match x y:
49    case T.W{+xl, +xh} T.W{+yl, +yh}:
50      Equal.cong(T.Lane, T.Lane, +z => L.add(L.add(T.W{xl, xh}, T.W{yl, yh}), L.add(z, z)), I.prod(xl, yl), S.lane_of(Nat.mul(U32.to_nat(xl), U32.to_nat(yl))), prod_correct(xl, yl))