Sha512.sha512: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/crypto/sha512/sha512.bend as Sha512
Lines 5-10 of bend-collections@1.0.0.0/src/crypto/sha512/sha512.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/crypto/sha512/sha512.bend&start_line=5&end_line=10

import Base
import bend-collections@1.0.0.0/src/crypto/sha512/core.bend as Core

# SHA-512 (FIPS 180-4). Bytes are U32 values, each < 256; the digest is the
# 64 bytes of H0..H7, most significant first. Proved equal to the executable
# specification spec/crypto/sha512.bend for every input:
# proofs/crypto/sha512/laws.bend.
def sha512(bytes: List<&2, U32>) -> List<&2, U32>:
  Core.sha512(bytes)

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha512/core.bend&name=sha512