def hprime
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as Argon2import Base
48# H'^T(a): the variable-length hash, over LE32(T) || a.
49def hprime(+tl: Nat, a: List<&2, U32>) -> List<&2, U32>:
50 hp_pick(tl, cat(le32(tl), a), Nat.is_le(tl, 64n))
Uses (7)
Used by (12)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2:run
- bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2:init_go
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash:hprime_eq
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password:hprime_len
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password:hprime_ok
- …