law ripemd160_digest_length

bend-osdev-hashes@0.1.0.0 · LAWS.bend:218

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-hashes@0.1.0.0/ripemd160.bend as RM

218# RIPEMD-160: the digest of every message has 20 bytes
219law ripemd160_digest_length:
220  for +m: B.Octets
221  {B.Octets.len(RM.HsRipemd160.digest(m)) == 20n : Nat}