Bytes.sha_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytes
Lines 108-109 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend&start_line=108&end_line=109

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

def sha_eq(+bytes: List<&2, U32>) -> {H.sha512(bytes) == SHA.sha512_bytes(bytes) : List<&2, U32>}:
  S512.sha512_correct(bytes)

Uses (5):
  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-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend&name=sha512_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=sha512_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend&name=sha512