bend-collections Releases (1): 1.0.0.0 0xd9a2fae439ac7ff9e21e0853948f94fe indexed https://jend.leeeet.dev/files.txt?path=bend-collections@1.0.0.0 Definitions (4483, 1 to 100 shown): Conformance.octets_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=octets_correct) law octets_correct: for +width: Nat for +n: Nat for +acc: List<&2, U32> {C.length_octets(width, n, acc) == List.append(&2, U32, F.octets(width, n), acc) : List<&2, U32>} Conformance.length_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=length_correct) law length_correct: for +n: Nat {C.bit_length(n) == F.length_field(n) : List<&2, U32>} Conformance.nth_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=nth_correct) law nth_correct: for xs: List<&2, U32> for n: Nat {C.get(xs, n) == F.nth(xs, n) : U32} Conformance.next_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=next_correct) law next_correct: for +hs: List<&2, U32> {C.next_word(hs) == F.recurrence(hs) : U32} Conformance.extension_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=extension_correct) law extension_correct: for +n: Nat for +hs: List<&2, U32> {C.expand(n, hs) == F.extension(n, hs) : List<&2, U32>} Conformance.schedule_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=schedule_correct) law schedule_correct: for +extra: Nat for +block: List<&2, U32> {C.schedule(extra, block) == F.schedule(extra, block) : List<&2, U32>} Conformance.step_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=step_correct) law step_correct: for s: S.State for k: U32 for w: U32 {C.step(s, k, w) == F.step(s, k, w) : S.State} Conformance.rounds_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=rounds_correct) law rounds_correct: for +ks: List<&2, U32> for +ws: List<&2, U32> for +s: S.State {C.rounds(ks, ws, s) == F.rounds(ks, ws)(s) : S.State} Conformance.feedforward_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=feedforward_correct) law feedforward_correct: for x: S.State for y: S.State {C.feedforward(x, y) == F.feedforward(x, y) : S.State} Conformance.compression_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=compression_correct) law compression_correct: for +ws: List<&2, U32> for +ks: List<&2, U32> for +s: S.State {C.compress(ws, ks, s) == F.compress(ws, ks, s) : S.State} Conformance.expanded_rounds_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=expanded_rounds_correct) law expanded_rounds_correct: for +n: Nat for +history: List<&2, U32> for +ks: List<&2, U32> for +s: S.State {C.expanded_rounds(n, history, ks, s) == C.rounds(ks, C.expand(n, history), s) : S.State} Conformance.schedule_rounds_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=schedule_rounds_correct) law schedule_rounds_correct: for +ws: List<&2, U32> for +extra: Nat for +history: List<&2, U32> for +ks: List<&2, U32> for +s: S.State {C.schedule_rounds(ws, extra, history, ks, s) == C.rounds(ks, List.append(&2, U32, ws, C.expand(extra, history)), s) : S.State} Conformance.fused_compress_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=fused_compress_correct) law fused_compress_correct: for +block: List<&2, U32> for +extra: Nat for +ks: List<&2, U32> for +s: S.State {C.fused_compress(block, extra, ks, s) == C.compress(C.schedule(extra, block), ks, s) : S.State} Conformance.fused_compress_slow_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=fused_compress_slow_correct) law fused_compress_slow_correct: for +block: List<&2, U32> for +extra: Nat for +ks: List<&2, U32> for +s: S.State {C.fused_compress_slow(block, extra, ks, s) == C.compress(C.schedule(extra, block), ks, s) : S.State} Conformance.window_rounds_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=window_rounds_correct) law window_rounds_correct: for +q: Nat for +a: U32 for +b: U32 for +c: U32 for +d: U32 for +e: U32 for +f: U32 for +g: U32 for +h: U32 for +i: U32 … Conformance.window_schedule_rounds_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=window_schedule_rounds_correct) law window_schedule_rounds_correct: for +ws: List<&2, U32> for +extra: Nat for +a: U32 for +b: U32 for +c: U32 for +d: U32 for +e: U32 for +f: U32 for +g: U32 for +h: U32 … Conformance.window_compress16_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=window_compress16_correct) law window_compress16_correct: for +a: U32 for +b: U32 for +c: U32 for +d: U32 for +e: U32 for +f: U32 for +g: U32 for +h: U32 for +i: U32 for +j: U32 … Conformance.digest_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=digest_correct) law digest_correct: for s: S.State {C.digest(s) == F.digest(s) : List<&2, U32>} Conformance.block_bytes_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=block_bytes_correct) law block_bytes_correct: for +bytes: List<&2, U32> for +extra: Nat for +ks: List<&2, U32> for +s: S.State {C.block_bytes(bytes, extra, ks, s) == F.blocks(F.schedules(F.words(bytes), extra), ks)(s) : S.State} Conformance.suffix_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=suffix_correct) law suffix_correct: for +n: Nat {C.suffix(n) == F.padding_suffix(n) : List<&2, U32>} Conformance.mul64 (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=mul64) # Byte counts of whole blocks: 64 * k, built the way stream accumulates them. def mul64(k: Nat) -> Nat: Conformance.mod_quotient (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=mod_quotient) # The quotient accumulator never affects the remainder computed by divmod. law mod_quotient: for +x: Nat for +m: Nat for +d: Nat for +e: Nat for +r: Nat {Pair.snd(Nat, Nat, Nat.divmod.go(x, m, d, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(x, m, e, r)) : Nat} Conformance.mod_shift (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=mod_shift) # Sixty-four divmod steps return to the initial counter state with a larger quotient. law mod_shift: for +x: Nat {Nat.mod(Nat.add(64n, x), 64n) == Nat.mod(x, 64n) : Nat} Conformance.mod_tail (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=mod_tail) law mod_tail: for +x: Nat for +k: Nat {Nat.mod(Nat.add(x, mul64(k)), 64n) == Nat.mod(x, 64n) : Nat} Conformance.kr64_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr64_correct) # Each 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 kr64_correct: for +q: Nat for +win: C.ShaWindow for +s: S.State {C.kr64(q, win, s) == C.window_rounds(q, win, Nil{}, s) : S.State} Conformance.kr63_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr63_correct) law kr63_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr62_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr62_correct) law kr62_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr61_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr61_correct) law kr61_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr60_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr60_correct) law kr60_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr59_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr59_correct) law kr59_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr58_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr58_correct) law kr58_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr57_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr57_correct) law kr57_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr56_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr56_correct) law kr56_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr55_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr55_correct) law kr55_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr54_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr54_correct) law kr54_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr53_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr53_correct) law kr53_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr52_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr52_correct) law kr52_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr51_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr51_correct) law kr51_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr50_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr50_correct) law kr50_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr49_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr49_correct) law kr49_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr48_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr48_correct) law kr48_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr47_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr47_correct) law kr47_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr46_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr46_correct) law kr46_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr45_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr45_correct) law kr45_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr44_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr44_correct) law kr44_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr43_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr43_correct) law kr43_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr42_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr42_correct) law kr42_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr41_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr41_correct) law kr41_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr40_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr40_correct) law kr40_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr39_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr39_correct) law kr39_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr38_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr38_correct) law kr38_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr37_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr37_correct) law kr37_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr36_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr36_correct) law kr36_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr35_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr35_correct) law kr35_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr34_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr34_correct) law kr34_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr33_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr33_correct) law kr33_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr32_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr32_correct) law kr32_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr31_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr31_correct) law kr31_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr30_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr30_correct) law kr30_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr29_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr29_correct) law kr29_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr28_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr28_correct) law kr28_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr27_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr27_correct) law kr27_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr26_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr26_correct) law kr26_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr25_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr25_correct) law kr25_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr24_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr24_correct) law kr24_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr23_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr23_correct) law kr23_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr22_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr22_correct) law kr22_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr21_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr21_correct) law kr21_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr20_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr20_correct) law kr20_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr19_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr19_correct) law kr19_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr18_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr18_correct) law kr18_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr17_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr17_correct) law kr17_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.kr16_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=kr16_correct) law kr16_correct: for +q: Nat for +x0: U32 for +x1: U32 for +x2: U32 for +x3: U32 for +x4: U32 for +x5: U32 for +x6: U32 for +x7: U32 for +x8: U32 … Conformance.fips16_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=fips16_correct) law fips16_correct: for +a: U32 for +b: U32 for +c: U32 for +d: U32 for +e: U32 for +f: U32 for +g: U32 for +h: U32 for +i: U32 for +j: U32 … Conformance.stream_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=stream_correct) # Streaming refines the generic block decoder, instantiated with the FIPS # table, applied to the padded message. After a complete block the count grows # by 64 exactly as the remaining length shrinks. For a short tail, count = 64k # fixes n mod 64 to the tail length, so the modular zero count is concrete and # finish_go packs the same 64 or 128 bytes that block_bytes decodes. law stream_correct: for +bytes: List<&2, U32> for +k: Nat for +extra: Nat for +s: S.State {C.stream(bytes, mul64(k), extra, s) == C.block_bytes(List.append(&2, U32, bytes, C.suffix(Nat.add(List.length(&2, U32, bytes), mul64(k)))), extra, C.round_constants(), s) : S.State} Conformance.sha256_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/conformance.bend&name=sha256_correct) # Unlike the old theorem, there is NO arbitrary preprocessing parameter. # This proves the actual implementation pipeline against the independent one. law sha256_correct: for +bytes: List<&2, U32> {C.sha256(bytes) == F.hash(bytes, 48n, C.round_constants()) : List<&2, U32>} Correctness.digest_octets_length (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/correctness.bend&name=digest_octets_length) law digest_octets_length: for s: State.State {List.length(&2, U32, FIPS.digest_octets(FIPS.digest(s))) == 32n : Nat} Laws.constants_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/laws.bend&name=constants_correct) # These claims mention the actual public API and the complete independent spec. # There are no arbitrary preprocessing functions, tables, or correctness premises. law constants_correct: {SHA.constants() == FIPS.constants() : List<&2, U32>} Laws.sha256_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/laws.bend&name=sha256_correct) law sha256_correct: for +bytes: List<&2, U32> {SHA.sha256(bytes) == FIPS.sha256(bytes) : List<&2, U32>} Laws.digest_bytes_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/laws.bend&name=digest_bytes_correct) law digest_bytes_correct: for +ws: List<&2, U32> {SHA.digest_bytes(ws) == FIPS.digest_octets(ws) : List<&2, U32>} Laws.sha256_bytes_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/laws.bend&name=sha256_bytes_correct) law sha256_bytes_correct: for +bytes: List<&2, U32> {SHA.sha256_bytes(bytes) == FIPS.sha256_bytes(bytes) : List<&2, U32>} Laws.sha256_bytes_length (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/laws.bend&name=sha256_bytes_length) law sha256_bytes_length: for +bytes: List<&2, U32> {List.length(&2, U32, SHA.sha256_bytes(bytes)) == 32n : Nat} ListProofs.append_assoc (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=append_assoc) law append_assoc: for -A: Data for xs: List<&2, A> for ys: List<&2, A> for zs: List<&2, A> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>} ListProofs.reverse_twice (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=reverse_twice) law reverse_twice: for -A: Data for xs: List<&2, A> for acc: List<&2, A> for ys: List<&2, A> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), ys) == List.reverse.go(&2, A, acc, List.append(&2, A, xs, ys)) : List<&2, A>} ListProofs.reverse_append (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=reverse_append) law reverse_append: for -A: Data for xs: List<&2, A> for ys: List<&2, A> {List.reverse.go(&2, A, List.reverse(&2, A, xs), ys) == List.append(&2, A, xs, ys) : List<&2, A>} ListProofs.add_succ (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=add_succ) law add_succ: for n: Nat for m: Nat {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat} ListProofs.add_zero (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=add_zero) law add_zero: for n: Nat {Nat.add(n, 0n) == n : Nat} ListProofs.append_assoc_reverse (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=append_assoc_reverse) law append_assoc_reverse: for -A: Data for +xs: List<&2, A> for +ys: List<&2, A> for +zs: List<&2, A> {List.append(&2, A, xs, List.append(&2, A, ys, zs)) == List.append(&2, A, List.append(&2, A, xs, ys), zs) : List<&2, A>} ListProofs.add_swap (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/list_proofs.bend&name=add_swap) law add_swap: for +n: Nat for +k: Nat for +m: Nat {Nat.add(n, Nat.add(k, m)) == Nat.add(k, Nat.add(n, m)) : Nat} BufferProof.correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=correct) law correct: for a: Array for +length: Nat {SHA.sha256(a,length) == B.result(R.hash(a,length)) : Maybe<&1,Array>} BufferProof.digest_size (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=digest_size) law digest_size: for s: S.State {Pair.snd(Array,U32,Array.size(U32,B.digest(s))) == 8 : U32} BufferProof.words (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=words) # Proof-only observation; never called by the buffer hashing API. def words(a: Array) -> List<&2,U32>: BufferProof.digest_words (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=digest_words) law digest_words: for +s: S.State {words(B.digest(s)) == F.digest(s) : List<&2,U32>} BufferProof.observe (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=observe) # Full public-result observation against the independent packed specification. def observe(r: Maybe<&1,Array>) -> Maybe<&2,List<&2,U32>>: BufferProof.observe_digest (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=observe_digest) law observe_digest: for +r: Maybe<&2,S.State> {observe(B.result(r)) == R.digest_result(r) : Maybe<&2,List<&2,U32>>} BufferProof.full_reified (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=full_reified) law full_reified: for -a: Array for +length: Nat for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array}> {observe(SHA.sha256(a,length)) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>} BufferProof.full_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend&name=full_correct) law full_correct: for a: Array for +length: Nat {observe(SHA.sha256(a,length)) == R.sha256(a,length) : Maybe<&2,List<&2,U32>>} Conformance.octets_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=octets_correct) law octets_correct: for +width: Nat for +n: Nat for +acc: List<&2, U32> {C.length_octets(width, n, acc) == List.append(&2, U32, F.octets(width, n), acc) : List<&2, U32>} Conformance.length_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=length_correct) law length_correct: for +n: Nat {C.bit_length(n) == F.length_field(n) : List<&2, U32>} Conformance.nth_correct (https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=nth_correct) law nth_correct: for xs: List<&2, U32> for n: Nat {C.get(xs, n) == F.nth(xs, n) : U32} More: https://jend.leeeet.dev/packages/bend-collections.txt?definitions_offset=100