src/hub_sha/sha256.bend checks
raw source on the hub · import mylsm-lsm-store@0.3.1.0/src/hub_sha/sha256.bend as Sha256
Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f (src/crypto/sha/sha256.bend), byte-identical. See core.bend header.
2 imports
import Base import ./core.bend as Core
Definitions
def constants source · line 8 · raw
List<&2, U32>
The core refinement theorem quantifies over every constant table. Instantiate the verified core with the FIPS 180-4 constants.
def sha256 source · line 26 · raw
@bytes:List<&2, U32> -> List<&2, U32>
def ascii source · line 29 · raw
@s:String -> List<&2, U32>
def hex source · line 32 · raw
@ws:List<&2, U32> -> String
def digest_bytes source · line 36 · raw
@ws:List<&2, U32> -> List<&2, U32>
Big-endian octets, represented as U32 values in 0..255.
def sha256_bytes source · line 46 · raw
@bytes:List<&2, U32> -> List<&2, U32>