def hq

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

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

61# q = 4 sl
62def hq(+m: Nat, +p: Nat, +hp: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, Nat.div(Nat.div(I.blocks(m, p), p), 4n)) : Nat}:
63  %Equal.sym(Nat, Nat.div(Nat.div(I.blocks(m, p), p), 4n), X(m, p), sl_eq(m, p, hp)) : {Nat.div(I.blocks(m, p), p) == Nat.mul(4n, _) : Nat}
64  q_eq(m, p, hp)