AlphaGitHub
Source/Packages

Data.SHA256Digest

packages/foundation/standard/src/Data/SHA256Digest.alpha

1,631 lines150 declarations64.2 KiBSHA-256 c46a79f2ab9a
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1610–1625

sha256RawDigestOrEmpty

Full file
Bytes -> Bytes raw digest: the 32 digest bytes of the input, or empty bytes on the failure path. Downstream 32-length gates keep empty fail-closed (the raw counterpart of sha256Digest below).
1610def sha256RawDigestOrEmpty =
1611  (lambda unrestricted material : Bytes .
1612    (eliminate
1613      SHA256Result
1614      (lambda unrestricted current : (family SHA256Result) . Bytes)
1615      (sha256Bytes material)
1616      (branch
1617        SHA256Succeeded
1618        digest
1619        .
1620        (eliminate
1621          SHA256Digest
1622          (lambda unrestricted current : (family SHA256Digest) . Bytes)
1623          digest
1624          (branch SHA256DigestValue raw proof . raw)))
1625      (branch SHA256Failed error . b"")))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.