bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

def fin5
def fin6
def fin7
def fin8
def fin9
def fin10
def fin11
def fin12
def fin13
def fin14
def fin15
def fin16
def fin17
def fin18
def fin19
def fin20
def fin21
def fin22
def fin23
def fin24
def fin25
def fin26
def fin27
def fin28
def fin29
def fin30
def fin31
def fin32
def fin33
def fin34
def fin35
def fin36
def fin37
def fin38
def fin39
def fin40
def fin41
def fin42
def fin43
def fin44
def fin45
def fin46
def fin47
def fin48
def fin49
def fin50
def fin51
def fin52
def fin53
def fin54
def fin55
def fin56
def fin57
def fin58
def fin59
def fin60
def fin61
def fin62
def fin63
def fips_blocksTail-recursive block loop over an already padded byte list.
def zeros_onto
def paddingThe padding suffix built only with tail-recursive loops.
def byte_count
def finish_nFinal block(s) of an n-byte message whose tail has fewer than 64 bytes.
def finishcount is the number of bytes already hashed, always a multiple of 64.
def streamCompress complete 64-byte blocks straight from the input list, so the message is never copied, counted or reversed.
def asciiASCII convenience only; binary inputs use sha256 directly.
def hex_digit_if
def hex_digit
def hex_word_go
def hex_word
def hex
def sha256

law constants_correctThese claims mention the actual public API and the complete independent spec.
law sha256_correct
law digest_bytes_correct
law sha256_bytes_correct
law sha256_bytes_length
law sha256_packed_correctA separate packed-format contract; the original list-to-FIPS theorem is unchanged.
law sha256_array_correctActual production array API; historical list laws above concern only its model.

type TreeA duplicable proof-only description of an array.
def thaw
law reifyConsume any linear array once, retaining a proof of its exact representation.
law reify_node