bend-collections
Releases (1)
-
1.0.0.0 indexed
Definitions (4,483)
proofs/crypto/sha/packed/conformance.bend
- 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/packed/core_model.bend
- def rotr
- def get
- def next_word_slowReverse history: at round t, index j contains Runtime.W[t-1-j].
- def next_wordSchedule histories always contain at least 16 words.
- def expand
- def schedule
- def rounds
- def compressCompression consumes an already expanded 64-word schedule.
- def expanded_roundsGenerate each derived schedule word immediately before its round.
- def schedule_roundsConsume the original block words, then continue directly with its expansion.
- def window_roundsA fixed rolling window drops schedule words as soon as they are older than 16 rounds.
- def window_schedule_rounds
- def fused_compress_slow
- def fused_compress
- def window_compress16Fast path for the 16-word blocks produced by block_bytes.
- def be32
- def length_octets
- def bit_length
- def digest
- def block_bytesGeneric block decoder over a padded byte list and any constant table.
- def round_constantsFIPS 180-4 round constants, the table the specialized rounds below inline.
- def suffixSHA-256 round t (16 <= t < 64) with its constant as a literal.
- def fin0Big-endian words of the 64-bit message bit length 8n, computed from n with exactly the digit expressions bit_length produces, but without building and matching an eight-element list.
- def fin1
- def fin2
- def fin3
- def fin4