package.bend source

package.bend on the hub · documented module

# bend-sha256: pure Bend SHA-256 with packed arrays and checked source proofs.# Source: https://github.com/Giulio2002/bend-sha256# Based on release c77b76cc084ddd5aa1c930ac8215b2f3d148afc0, Bend 2.0.16.## Input: four big-endian bytes per U32 plus the logical byte length.# Output: Some{eight big-endian U32 words}, exactly 32 digest bytes;# None if byte_length exceeds the input array's capacity in bytes.# Unused trailing input bytes/slots are ignored. Input is consumed.# No crypto FFI, hardware intrinsics, or runtime linked-list representation.## Proof scope: universal refinement of the public array API to the independent# packed-input specification, with digest word-order and size laws. Historical# byte-list models are also proved against the independent FIPS specification.# The universal bridge from packed bytes to that original byte-list theorem is# not claimed. The Bend kernel, Base, compiler, C toolchain and CPU are trusted.# Full scope: https://github.com/Giulio2002/bend-sha256/blob/main/CORRECTNESS.md## This entry checks and bundles the proofs. For implementation-only imports,# use sha256.bend from the same content-addressed package.import Baseimport ./sha256.bend as SHAimport ./PROOF.bend as Proofdef sha256(words: Array<U32>, byte_length: Nat) -> Maybe<&1,Array<U32>>:  SHA.sha256(words,byte_length)def hex(digest: Array<U32>) -> String:  SHA.hex(digest)