src/crypto/sha/sha256.bend checks
raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/sha256.bend as Sha256
2 imports
import Base import ./core.bend as Core
Definitions
def constants source · line 6 · 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 24 · raw
@bytes:List<&2, U32> -> List<&2, U32>
def ascii source · line 27 · raw
@s:String -> List<&2, U32>
def hex source · line 30 · raw
@ws:List<&2, U32> -> String
def digest_bytes source · line 34 · raw
@ws:List<&2, U32> -> List<&2, U32>
Big-endian octets, represented as U32 values in 0..255.
def sha256_bytes source · line 44 · raw
@bytes:List<&2, U32> -> List<&2, U32>