~/bend-docscommunity

conformance.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/conformance.bend as Conformance

7 imports
import Base
import ./core.bend as Runtime
import ./state.bend as S
import ./core_model.bend as C
import ./fips.bend as F
import ./list_proofs.bend as L
import ./padding_proof.bend as Padding

Laws

law octets_correct provedsource · line 9 · raw

@+width:Nat -> @+n:Nat -> @+acc:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.length_octets(width, n, acc) == List.append(&2, U32, 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.octets(width, n), acc) : List<&2, U32>}

law length_correct provedsource · line 25 · raw

@+n:Nat -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.bit_length(n) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.length_field(n) : List<&2, U32>}

law nth_correct provedsource · line 32 · raw

@xs:List<&2, U32> -> @n:Nat -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.get(xs, n) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.nth(xs, n) : U32}

law next_correct provedsource · line 46 · raw

@+hs:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.next_word(hs) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.recurrence(hs) : U32}

law extension_correct provedsource · line 87 · raw

@+n:Nat -> @+hs:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.expand(n, hs) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.extension(n, hs) : List<&2, U32>}

law schedule_correct provedsource · line 102 · raw

@+extra:Nat -> @+block:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.schedule(extra, block) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.schedule(extra, block) : List<&2, U32>}

law step_correct provedsource · line 112 · raw

@s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> @k:U32 -> @w:U32 -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.step(s, k, w) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.step(s, k, w) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law rounds_correct provedsource · line 123 · raw

@+ks:List<&2, U32> -> @+ws:List<&2, U32> -> @+s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.rounds(ks, ws, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.rounds(ks, ws, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law feedforward_correct provedsource · line 140 · raw

@x:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> @y:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.feedforward(x, y) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.feedforward(x, y) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law compression_correct provedsource · line 150 · raw

@+ws:List<&2, U32> -> @+ks:List<&2, U32> -> @+s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.compress(ws, ks, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.compress(ws, ks, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law expanded_rounds_correct provedsource · line 161 · raw

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

law schedule_rounds_correct provedsource · line 180 · raw

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

law fused_compress_correct provedsource · line 198 · raw

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

law fused_compress_slow_correct provedsource · line 205 · raw

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

law window_rounds_correct provedsource · line 219 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.expanded_rounds(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, ks, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law window_schedule_rounds_correct provedsource · line 257 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_schedule_rounds(ws, extra, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.schedule_rounds(ws, extra, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, ks, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law window_compress16_correct provedsource · line 360 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, extra, ks, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law digest_correct provedsource · line 420 · raw

@s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.digest(s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.digest(s) : List<&2, U32>}

law block_bytes_correct provedsource · line 429 · raw

@+bytes:List<&2, U32> -> @+extra:Nat -> @+ks:List<&2, U32> -> @+s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.block_bytes(bytes, extra, ks, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.blocks(0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.schedules(0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.words(bytes), extra), ks, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law suffix_correct provedsource · line 594 · raw

@+n:Nat -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.suffix(n) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.padding_suffix(n) : List<&2, U32>}

law mod_quotient provedsource · line 615 · 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 633 · 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 640 · raw

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

law kr64_correct provedsource · line 663 · raw

@+q:Nat -> @+win:0x3bdc0c9f5265bb49f7fc76b61f529f24/core.RoundWindow -> @+s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr64(q, win, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, win, [], s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/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 676 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr63(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3329325298], s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr62_correct provedsource · line 706 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr62(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3204031479, 3329325298], s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr61_correct provedsource · line 736 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr61(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2756734187, 3204031479, 3329325298], s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr60_correct provedsource · line 766 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr60(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2428436474, 2756734187, 3204031479, 3329325298], s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr59_correct provedsource · line 796 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr59(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr58_correct provedsource · line 826 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr58(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr57_correct provedsource · line 856 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr57(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr56_correct provedsource · line 886 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr56(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr55_correct provedsource · line 916 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr55(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr54_correct provedsource · line 946 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr54(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr53_correct provedsource · line 976 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr53(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr52_correct provedsource · line 1006 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr52(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr51_correct provedsource · line 1036 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr51(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr50_correct provedsource · line 1066 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr50(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr49_correct provedsource · line 1096 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr49(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr48_correct provedsource · line 1126 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr48(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr47_correct provedsource · line 1156 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr47(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr46_correct provedsource · line 1186 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr46(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr45_correct provedsource · line 1216 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr45(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr44_correct provedsource · line 1246 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr44(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr43_correct provedsource · line 1276 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr43(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr42_correct provedsource · line 1306 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr42(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr41_correct provedsource · line 1336 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr41(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr40_correct provedsource · line 1366 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr40(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr39_correct provedsource · line 1396 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr39(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr38_correct provedsource · line 1426 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr38(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr37_correct provedsource · line 1456 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr37(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr36_correct provedsource · line 1486 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr36(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr35_correct provedsource · line 1516 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr35(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr34_correct provedsource · line 1546 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr34(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr33_correct provedsource · line 1576 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr33(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr32_correct provedsource · line 1606 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr32(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr31_correct provedsource · line 1636 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr31(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr30_correct provedsource · line 1666 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr30(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr29_correct provedsource · line 1696 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr29(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr28_correct provedsource · line 1726 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr28(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr27_correct provedsource · line 1756 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr27(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr26_correct provedsource · line 1786 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr26(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr25_correct provedsource · line 1816 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr25(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr24_correct provedsource · line 1846 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr24(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr23_correct provedsource · line 1876 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr23(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr22_correct provedsource · line 1906 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr22(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr21_correct provedsource · line 1936 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr21(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr20_correct provedsource · line 1966 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr20(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr19_correct provedsource · line 1996 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr19(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr18_correct provedsource · line 2026 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr18(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr17_correct provedsource · line 2056 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr17(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law kr16_correct provedsource · line 2086 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.kr16(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_rounds(q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/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) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law fips16_correct provedsource · line 2116 · 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:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.window_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.round_constants, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State}

law stream_correct provedsource · line 2150 · raw

@+bytes:List<&2, U32> -> @+k:Nat -> @+extra:Nat -> @+s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.stream(bytes, mul64(k), extra, s) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.block_bytes(List.append(&2, U32, bytes, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.suffix(Nat.add(List.length(&2, U32, bytes), mul64(k)))), extra, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.round_constants, s) : 0x3bdc0c9f5265bb49f7fc76b61f529f24/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 2740 · raw

@+bytes:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.sha256(bytes) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.hash(bytes, 48n, 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.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 607 · raw

@k:Nat -> Nat

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