def sha_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/bytes.bend:108
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytes
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as SHA
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend as S512
108def sha_eq(+bytes: List<&2, U32>) -> {H.sha512(bytes) == SHA.sha512_bytes(bytes) : List<&2, U32>}:
109 S512.sha512_correct(bytes)