~/bend-docscommunity

proofs/crypto/sha/conformance.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/conformance.bend as Conformance

6 imports
import Base
import ../../../src/crypto/sha/state.bend as S
import ../../../src/crypto/sha/core.bend as C
import ../../../spec/crypto/sha.bend as F
import ./list_proofs.bend as L
import ./padding.bend as Padding

Laws

law octets_correct provedsource · line 8 · raw

@+width:Nat -> @+n:Nat -> @+acc:List<&2, U32> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.length_octets(width, n, acc) == List.append(&2, U32, 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.octets(width, n), acc) : List<&2, U32>}

law length_correct provedsource · line 24 · raw

@+n:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.bit_length(n) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.length_field(n) : List<&2, U32>}

law nth_correct provedsource · line 31 · raw

@xs:List<&2, U32> -> @n:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.get(xs, n) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.nth(xs, n) : U32}

law next_correct provedsource · line 45 · raw

@+hs:List<&2, U32> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.next_word(hs) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.recurrence(hs) : U32}

law extension_correct provedsource · line 86 · raw

@+n:Nat -> @+hs:List<&2, U32> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.expand(n, hs) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.extension(n, hs) : List<&2, U32>}

law schedule_correct provedsource · line 101 · raw

@+extra:Nat -> @+block:List<&2, U32> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.schedule(extra, block) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.schedule(extra, block) : List<&2, U32>}

law step_correct provedsource · line 111 · raw

@s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @k:U32 -> @w:U32 -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.step(s, k, w) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.step(s, k, w) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law rounds_correct provedsource · line 122 · raw

@+ks:List<&2, U32> -> @+ws:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.rounds(ks, ws, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.rounds(ks, ws, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law feedforward_correct provedsource · line 139 · raw

@x:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> @y:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.feedforward(x, y) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.feedforward(x, y) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law compression_correct provedsource · line 149 · raw

@+ws:List<&2, U32> -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.compress(ws, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.compress(ws, ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law expanded_rounds_correct provedsource · line 160 · raw

@+n:Nat -> @+history:List<&2, U32> -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.expanded_rounds(n, history, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.rounds(ks, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.expand(n, history), s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law schedule_rounds_correct provedsource · line 179 · raw

@+ws:List<&2, U32> -> @+extra:Nat -> @+history:List<&2, U32> -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.schedule_rounds(ws, extra, history, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.rounds(ks, List.append(&2, U32, ws, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.expand(extra, history)), s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law fused_compress_correct provedsource · line 197 · raw

@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.fused_compress(block, extra, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.compress(0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.schedule(extra, block), ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law fused_compress_slow_correct provedsource · line 204 · raw

@+block:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.fused_compress_slow(block, extra, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.compress(0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.schedule(extra, block), ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law window_rounds_correct provedsource · line 218 · raw

@+q:Nat -> @+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+rest:List<&2, U32> -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.expanded_rounds(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law window_schedule_rounds_correct provedsource · line 256 · raw

@+ws:List<&2, U32> -> @+extra:Nat -> @+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+rest:List<&2, U32> -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_schedule_rounds(ws, extra, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.schedule_rounds(ws, extra, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law window_compress16_correct provedsource · line 359 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, extra, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law digest_correct provedsource · line 419 · raw

@s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.digest(s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.digest(s) : List<&2, U32>}

law block_bytes_correct provedsource · line 428 · raw

@+bytes:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.block_bytes(bytes, extra, ks, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.blocks(0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.schedules(0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.words(bytes), extra), ks, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law suffix_correct provedsource · line 593 · raw

@+n:Nat -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.suffix(n) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.padding_suffix(n) : List<&2, U32>}

law mod_quotient provedsource · line 614 · raw

@+x:Nat -> @+m:Nat -> @+d:Nat -> @+e:Nat -> @+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}

The quotient accumulator never affects the remainder computed by divmod.

law mod_shift provedsource · line 632 · raw

@+x:Nat -> {Nat.mod(Nat.add(64n, x), 64n) == Nat.mod(x, 64n) : Nat}

Sixty-four divmod steps return to the initial counter state with a larger quotient.

law mod_tail provedsource · line 639 · raw

@+x:Nat -> @+k:Nat -> {Nat.mod(Nat.add(x, mul64(k)), 64n) == Nat.mod(x, 64n) : Nat}

law kr64_correct provedsource · line 662 · raw

@+q:Nat -> @+win:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.ShaWindow -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr64(q, win, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, win, [], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

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 kr63_correct provedsource · line 675 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr63(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr62_correct provedsource · line 705 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr62(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr61_correct provedsource · line 735 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr61(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr60_correct provedsource · line 765 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr60(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr59_correct provedsource · line 795 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr59(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr58_correct provedsource · line 825 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr58(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr57_correct provedsource · line 855 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr57(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr56_correct provedsource · line 885 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr56(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr55_correct provedsource · line 915 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr55(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr54_correct provedsource · line 945 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr54(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr53_correct provedsource · line 975 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr53(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr52_correct provedsource · line 1005 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr52(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr51_correct provedsource · line 1035 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr51(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr50_correct provedsource · line 1065 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr50(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr49_correct provedsource · line 1095 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr49(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr48_correct provedsource · line 1125 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr48(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr47_correct provedsource · line 1155 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr47(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr46_correct provedsource · line 1185 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr46(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr45_correct provedsource · line 1215 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr45(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr44_correct provedsource · line 1245 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr44(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr43_correct provedsource · line 1275 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr43(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr42_correct provedsource · line 1305 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr42(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr41_correct provedsource · line 1335 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr41(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr40_correct provedsource · line 1365 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr40(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr39_correct provedsource · line 1395 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr39(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr38_correct provedsource · line 1425 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr38(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr37_correct provedsource · line 1455 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr37(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr36_correct provedsource · line 1485 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr36(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr35_correct provedsource · line 1515 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr35(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr34_correct provedsource · line 1545 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr34(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr33_correct provedsource · line 1575 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr33(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr32_correct provedsource · line 1605 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr32(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr31_correct provedsource · line 1635 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr31(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr30_correct provedsource · line 1665 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr30(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr29_correct provedsource · line 1695 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr29(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr28_correct provedsource · line 1725 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr28(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr27_correct provedsource · line 1755 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr27(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr26_correct provedsource · line 1785 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr26(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr25_correct provedsource · line 1815 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr25(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr24_correct provedsource · line 1845 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr24(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr23_correct provedsource · line 1875 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr23(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr22_correct provedsource · line 1905 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr22(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr21_correct provedsource · line 1935 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr21(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr20_correct provedsource · line 1965 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr20(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr19_correct provedsource · line 1995 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr19(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [604807628, 770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr18_correct provedsource · line 2025 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr18(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [264347078, 604807628, 770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr17_correct provedsource · line 2055 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr17(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [4022224774, 264347078, 604807628, 770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law kr16_correct provedsource · line 2085 · raw

@+q:Nat -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.kr16(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_rounds(q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3835390401, 4022224774, 264347078, 604807628, 770255983, 1249150122, 1555081692, 1996064986, 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law fips16_correct provedsource · line 2115 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> @+e:U32 -> @+f:U32 -> @+g:U32 -> @+h:U32 -> @+i:U32 -> @+j:U32 -> @+k:U32 -> @+l:U32 -> @+m:U32 -> @+n:U32 -> @+o:U32 -> @+p:U32 -> @+q:Nat -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.round_constants, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

law stream_correct provedsource · line 2149 · raw

@+bytes:List<&2, U32> -> @+k:Nat -> @+extra:Nat -> @+s:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.stream(bytes, mul64(k), extra, s) == 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.block_bytes(List.append(&2, U32, bytes, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.suffix(Nat.add(List.length(&2, U32, bytes), mul64(k)))), extra, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.round_constants, s) : 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/state.State}

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 sha256_correct provedsource · line 2739 · raw

@+bytes:List<&2, U32> -> {0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.sha256(bytes) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.hash(bytes, 48n, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/sha/core.round_constants) : List<&2, U32>}

Unlike the old theorem, there is NO arbitrary preprocessing parameter. This proves the actual implementation pipeline against the independent one.

Definitions

def mul64 source · line 606 · raw

@k:Nat -> Nat

Byte counts of whole blocks: 64 * k, built the way stream accumulates them.