~/bend-docscommunity

src/hub_sha/sha256.bend checks

raw source on the hub · import mylsm-lsm-store@0.4.0.0/src/hub_sha/sha256.bend as Sha256

Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f (src/crypto/sha/sha256.bend), byte-identical. See core.bend header.

4 imports
import Base
import ./core.bend as Core
import ./state.bend as S
import bend-kit-bytes@0.3.2.0/bytes.bend as Packed

Definitions

def constants source · line 10 · 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 29 · raw

@bytes:List<&2, U32> -> List<&2, U32>

SHA-256 for the reference octet-list input.

def ascii source · line 33 · raw

@text:String -> List<&2, U32>

Convert ASCII text to the reference octet-list input.

def hex source · line 37 · raw

@ws:List<&2, U32> -> String

Format eight digest words as lowercase hexadecimal.

def digest_bytes source · line 41 · raw

@ws:List<&2, U32> -> List<&2, U32>

Big-endian octets, represented as U32 values in 0..255.

def sha256_bytes source · line 52 · raw

@bytes:List<&2, U32> -> List<&2, U32>

Return the reference digest as eight big-endian octets per word.

def packed.compress source · line 57 · raw

@words:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

Compress one packed block using sixteen transient big-endian words. The file buffer stays packed; no per-byte List is constructed for complete blocks.

def packed.blocks source · line 65 · raw

@remaining:Nat -> @in_block:Nat -> @pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, Maybe<&2, U32>) -> @acc:List<&2, U32> -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State)

Read complete 64-byte blocks directly through a bounded package cursor.

def packed.tail source · line 115 · raw

@remaining:Nat -> @pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, Maybe<&2, U32>) -> @acc:List<&2, U32> -> Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, List<&2, U32>)

Read the remaining fewer than 64 bytes for the existing constant-space tail padding routines. This list is bounded by 63 octets, regardless of file size.

def packed.finish.tail source · line 138 · raw

@total:U32 -> @pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, List<&2, U32>) -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

def packed.final.tail source · line 143 · raw

@total:U32 -> @tail_len:Nat -> @cursor:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State

def packed.final source · line 150 · raw

@total:U32 -> @tail_len:Nat -> @cursor:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @state:0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State -> List<&2, U32>

def packed.after_blocks source · line 153 · raw

@total:U32 -> @tail_len:Nat -> @pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.State) -> List<&2, U32>

def packed.start.blocks source · line 158 · raw

@+total:U32 -> @cursor:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> @blocks:Nat -> @+tail_len:Nat -> List<&2, U32>

def packed.start source · line 166 · raw

@+total:U32 -> @cursor:0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor -> List<&2, U32>

def sha256_packed source · line 172 · raw

@bytes:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> List<&2, U32>

SHA-256 directly over packed bytes. Full blocks are read as sixteen u32be words; only the final 0..63 octets use the existing tail padding interface.

def packed.digest.finish.bytes source · line 177 · raw

@pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes, U32) -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes

def packed.digest.finish source · line 182 · raw

@pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, Bool) -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes

def packed.digest.words source · line 187 · raw

@words:List<&2, U32> -> @pair:Pair(0x185ae03c75e3e75be1171471f68b43cb/bytes.Cursor, Bool) -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes

def sha256_packed_bytes source · line 197 · raw

@bytes:0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes -> 0x185ae03c75e3e75be1171471f68b43cb/bytes.Bytes

Return the SHA-256 digest as packed bytes in canonical big-endian order.