law sha512_length

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha512/laws.bend:16

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/sha512.bend as SHA

16# Every digest is 64 bytes.
17law sha512_length:
18  for +bytes: List<&2, U32>
19  {List.length(&2, U32, SHA.sha512(bytes)) == 64n : Nat}