def q_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:47

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I

47# q = m' / p = 4 X.
48def q_eq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, X(m, p)) : Nat}:
49  %Equal.sym(Nat, Nat.mul(Nat.mul(4n, p), X(m, p)), Nat.mul(Nat.mul(4n, X(m, p)), p), mm_swap(p, X(m, p))) : {Nat.div(_, p) == Nat.mul(4n, X(m, p)) : Nat}
50  div_exact(Nat.mul(4n, X(m, p)), p, hp)