bend-collections
Releases (1)
-
1.0.0.0 indexed
Definitions (4,483)
proofs/crypto/sha/conformance.bend
- law octets_correct
- law length_correct
- law nth_correct
- law next_correct
- law extension_correct
- law schedule_correct
- law step_correct
- law rounds_correct
- law feedforward_correct
- law compression_correct
- law expanded_rounds_correct
- law schedule_rounds_correct
- law fused_compress_correct
- law fused_compress_slow_correct
- law window_rounds_correct
- law window_schedule_rounds_correct
- law window_compress16_correct
- law digest_correct
- law block_bytes_correct
- law suffix_correct
- def mul64Byte counts of whole blocks: 64 * k, built the way stream accumulates them.
- law mod_quotientThe quotient accumulator never affects the remainder computed by divmod.
- law mod_shiftSixty-four divmod steps return to the initial counter state with a larger quotient.
- law mod_tail
- law kr64_correctEach literal-constant round refines one step of window_rounds over the remaining FIPS constants; the window variables stay abstract, so every proof is one unfolding followed by the next round's lemma.
- law kr63_correct
- law kr62_correct
- law kr61_correct
- law kr60_correct
- law kr59_correct
- law kr58_correct
- law kr57_correct
- law kr56_correct
- law kr55_correct
- law kr54_correct
- law kr53_correct
- law kr52_correct
- law kr51_correct
- law kr50_correct
- law kr49_correct
- law kr48_correct
- law kr47_correct
- law kr46_correct
- law kr45_correct
- law kr44_correct
- law kr43_correct
- law kr42_correct
- law kr41_correct
- law kr40_correct
- law kr39_correct
- law kr38_correct
- law kr37_correct
- law kr36_correct
- law kr35_correct
- law kr34_correct
- law kr33_correct
- law kr32_correct
- law kr31_correct
- law kr30_correct
- law kr29_correct
- law kr28_correct
- law kr27_correct
- law kr26_correct
- law kr25_correct
- law kr24_correct
- law kr23_correct
- law kr22_correct
- law kr21_correct
- law kr20_correct
- law kr19_correct
- law kr18_correct
- law kr17_correct
- law kr16_correct
- law fips16_correct
- law stream_correctStreaming refines the generic block decoder, instantiated with the FIPS table, applied to the padded message.
- law sha256_correctUnlike the old theorem, there is NO arbitrary preprocessing parameter.
proofs/crypto/sha/correctness.bend
proofs/crypto/sha/laws.bend
- 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
proofs/crypto/sha/list_proofs.bend
- law append_assoc
- law reverse_twice
- law reverse_append
- law add_succ
- law add_zero
- law append_assoc_reverse
- law add_swap
proofs/crypto/sha/packed/buffer_proof.bend
- law correct
- law digest_size
- def wordsProof-only observation; never called by the buffer hashing API.
- law digest_words
- def observeFull public-result observation against the independent packed specification.
- law observe_digest
- law full_reified
- law full_correct
proofs/crypto/sha/packed/conformance.bend
- law octets_correct
- law length_correct
- law nth_correct