proofs/crypto/keccak/sponge.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/sponge.bend as Sponge

8 imports

import Base
import ../../../src/crypto/keccak/types.bend as T
import ../../../src/crypto/keccak/keccak.bend as K
import ../../../src/crypto/keccak/permutation.bend as P
import ../../../spec/crypto/keccak/permutation.bend as F
import ../../../spec/crypto/keccak/main.bend as R
import ./permutation.bend as Q
import ./array.bend as A

Laws

law mix_correct provedsource · line 10 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @+w32:U32 -> @+w33:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.mix(s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, w33) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.inject(s, [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, w33]) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law compress_correct provedsource · line 52 · raw

@+r:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @+w32:U32 -> @+w33:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/permutation.rounds(r, 0n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.mix(s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, w33)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/permutation.rounds(r, 0n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.inject(s, [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, w33])) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law read33_correct provedsource · line 96 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @+w32:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read33(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 0n, index, 34, False{}, 0n, s, [w32, w31, w30, w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read32_correct provedsource · line 140 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read32(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 1n, index, 33, False{}, 0n, s, [w31, w30, w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read31_correct provedsource · line 183 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read31(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 2n, index, 32, False{}, 0n, s, [w30, w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read30_correct provedsource · line 225 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read30(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 3n, index, 31, False{}, 0n, s, [w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read29_correct provedsource · line 266 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read29(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 4n, index, 30, False{}, 0n, s, [w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read28_correct provedsource · line 306 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read28(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 5n, index, 29, False{}, 0n, s, [w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read27_correct provedsource · line 345 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read27(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 6n, index, 28, False{}, 0n, s, [w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read26_correct provedsource · line 383 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read26(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 7n, index, 27, False{}, 0n, s, [w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read25_correct provedsource · line 420 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read25(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 8n, index, 26, False{}, 0n, s, [w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read24_correct provedsource · line 456 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read24(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 9n, index, 25, False{}, 0n, s, [w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read23_correct provedsource · line 491 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read23(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 10n, index, 24, False{}, 0n, s, [w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read22_correct provedsource · line 525 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read22(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 11n, index, 23, False{}, 0n, s, [w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read21_correct provedsource · line 558 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read21(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 12n, index, 22, False{}, 0n, s, [w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read20_correct provedsource · line 590 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read20(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 13n, index, 21, False{}, 0n, s, [w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read19_correct provedsource · line 621 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read19(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 14n, index, 20, False{}, 0n, s, [w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read18_correct provedsource · line 651 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read18(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 15n, index, 19, False{}, 0n, s, [w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read17_correct provedsource · line 680 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read17(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 16n, index, 18, False{}, 0n, s, [w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read16_correct provedsource · line 708 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read16(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 17n, index, 17, False{}, 0n, s, [w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read15_correct provedsource · line 735 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read15(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 18n, index, 16, False{}, 0n, s, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read14_correct provedsource · line 761 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read14(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 19n, index, 15, False{}, 0n, s, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read13_correct provedsource · line 786 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read13(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 20n, index, 14, False{}, 0n, s, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read12_correct provedsource · line 810 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read12(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 21n, index, 13, False{}, 0n, s, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read11_correct provedsource · line 833 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read11(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 22n, index, 12, False{}, 0n, s, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read10_correct provedsource · line 855 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read10(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 23n, index, 11, False{}, 0n, s, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read9_correct provedsource · line 876 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read9(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 24n, index, 10, False{}, 0n, s, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read8_correct provedsource · line 896 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read8(r, index, s, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 25n, index, 9, False{}, 0n, s, [w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read7_correct provedsource · line 915 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read7(r, index, s, w0, w1, w2, w3, w4, w5, w6, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 26n, index, 8, False{}, 0n, s, [w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read6_correct provedsource · line 933 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read6(r, index, s, w0, w1, w2, w3, w4, w5, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 27n, index, 7, False{}, 0n, s, [w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read5_correct provedsource · line 950 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read5(r, index, s, w0, w1, w2, w3, w4, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 28n, index, 6, False{}, 0n, s, [w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read4_correct provedsource · line 966 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read4(r, index, s, w0, w1, w2, w3, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 29n, index, 5, False{}, 0n, s, [w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read3_correct provedsource · line 981 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read3(r, index, s, w0, w1, w2, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 30n, index, 4, False{}, 0n, s, [w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read2_correct provedsource · line 995 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read2(r, index, s, w0, w1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 31n, index, 3, False{}, 0n, s, [w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read1_correct provedsource · line 1008 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read1(r, index, s, w0, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 32n, index, 2, False{}, 0n, s, [w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law read0_correct provedsource · line 1020 · raw

@+r:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.read0(r, index, s, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 33n, index, 1, False{}, 0n, s, [], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law padding_correct provedsource · line 1031 · raw

@+remain:Nat -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @+w32:U32 -> @+w33:U32 -> {[0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w0, 0n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w1, 4n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w2, 8n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w3, 12n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w4, 16n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w5, 20n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w6, 24n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w7, 28n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w8, 32n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w9, 36n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w10, 40n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w11, 44n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w12, 48n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w13, 52n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w14, 56n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w15, 60n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w16, 64n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w17, 68n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w18, 72n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w19, 76n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w20, 80n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w21, 84n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w22, 88n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w23, 92n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w24, 96n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w25, 100n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w26, 104n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w27, 108n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w28, 112n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w29, 116n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w30, 120n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w31, 124n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w32, 128n, remain), U32.or(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w33, 132n, remain), 2147483648)] == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.prepare(True{}, [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, w33], remain) : List<&2, U32>}

law padded_compress_correct provedsource · line 1209 · raw

@+r:Nat -> @+remain:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @+w32:U32 -> @+w33:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/permutation.rounds(r, 0n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.mix(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w0, 0n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w1, 4n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w2, 8n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w3, 12n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w4, 16n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w5, 20n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w6, 24n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w7, 28n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w8, 32n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w9, 36n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w10, 40n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w11, 44n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w12, 48n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w13, 52n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w14, 56n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w15, 60n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w16, 64n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w17, 68n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w18, 72n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w19, 76n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w20, 80n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w21, 84n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w22, 88n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w23, 92n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w24, 96n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w25, 100n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w26, 104n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w27, 108n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w28, 112n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w29, 116n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w30, 120n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w31, 124n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w32, 128n, remain), U32.or(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad_word(w33, 132n, remain), 2147483648))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/permutation.rounds(r, 0n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.inject(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.prepare(True{}, [w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, w33], remain))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad33_correct provedsource · line 1257 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @+w32:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad33(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, w32, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 0n, index, 34, True{}, remain, s, [w32, w31, w30, w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad32_correct provedsource · line 1302 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @+w31:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad32(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, w31, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 1n, index, 33, True{}, remain, s, [w31, w30, w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad31_correct provedsource · line 1346 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @+w30:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad31(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, w30, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 2n, index, 32, True{}, remain, s, [w30, w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad30_correct provedsource · line 1389 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @+w29:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad30(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, w29, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 3n, index, 31, True{}, remain, s, [w29, w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad29_correct provedsource · line 1431 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @+w28:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad29(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, w28, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 4n, index, 30, True{}, remain, s, [w28, w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad28_correct provedsource · line 1472 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @+w27:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad28(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, w27, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 5n, index, 29, True{}, remain, s, [w27, w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad27_correct provedsource · line 1512 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @+w26:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad27(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, w26, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 6n, index, 28, True{}, remain, s, [w26, w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad26_correct provedsource · line 1551 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @+w25:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad26(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, w25, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 7n, index, 27, True{}, remain, s, [w25, w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad25_correct provedsource · line 1589 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @+w24:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad25(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, w24, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 8n, index, 26, True{}, remain, s, [w24, w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad24_correct provedsource · line 1626 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @+w23:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad24(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, w23, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 9n, index, 25, True{}, remain, s, [w23, w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad23_correct provedsource · line 1662 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @+w22:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad23(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, w22, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 10n, index, 24, True{}, remain, s, [w22, w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad22_correct provedsource · line 1697 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @+w21:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad22(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, w21, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 11n, index, 23, True{}, remain, s, [w21, w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad21_correct provedsource · line 1731 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @+w20:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad21(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, w20, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 12n, index, 22, True{}, remain, s, [w20, w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad20_correct provedsource · line 1764 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @+w19:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad20(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 13n, index, 21, True{}, remain, s, [w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad19_correct provedsource · line 1796 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @+w18:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad19(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 14n, index, 20, True{}, remain, s, [w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad18_correct provedsource · line 1827 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @+w17:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad18(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 15n, index, 19, True{}, remain, s, [w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad17_correct provedsource · line 1857 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @+w16:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad17(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 16n, index, 18, True{}, remain, s, [w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad16_correct provedsource · line 1886 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @+w15:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad16(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 17n, index, 17, True{}, remain, s, [w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad15_correct provedsource · line 1914 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @+w14:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad15(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 18n, index, 16, True{}, remain, s, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad14_correct provedsource · line 1941 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @+w13:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad14(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 19n, index, 15, True{}, remain, s, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad13_correct provedsource · line 1967 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @+w12:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad13(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 20n, index, 14, True{}, remain, s, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad12_correct provedsource · line 1992 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @+w11:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad12(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 21n, index, 13, True{}, remain, s, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad11_correct provedsource · line 2016 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @+w10:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad11(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 22n, index, 12, True{}, remain, s, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad10_correct provedsource · line 2039 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @+w9:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad10(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 23n, index, 11, True{}, remain, s, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad9_correct provedsource · line 2061 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @+w8:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad9(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 24n, index, 10, True{}, remain, s, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad8_correct provedsource · line 2082 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad8(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, w7, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 25n, index, 9, True{}, remain, s, [w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad7_correct provedsource · line 2102 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad7(r, remain, index, s, w0, w1, w2, w3, w4, w5, w6, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 26n, index, 8, True{}, remain, s, [w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad6_correct provedsource · line 2121 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad6(r, remain, index, s, w0, w1, w2, w3, w4, w5, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 27n, index, 7, True{}, remain, s, [w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad5_correct provedsource · line 2139 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad5(r, remain, index, s, w0, w1, w2, w3, w4, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 28n, index, 6, True{}, remain, s, [w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad4_correct provedsource · line 2156 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad4(r, remain, index, s, w0, w1, w2, w3, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 29n, index, 5, True{}, remain, s, [w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad3_correct provedsource · line 2172 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad3(r, remain, index, s, w0, w1, w2, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 30n, index, 4, True{}, remain, s, [w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad2_correct provedsource · line 2187 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad2(r, remain, index, s, w0, w1, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 31n, index, 3, True{}, remain, s, [w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad1_correct provedsource · line 2201 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad1(r, remain, index, s, w0, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 32n, index, 2, True{}, remain, s, [w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law pad0_correct provedsource · line 2214 · raw

@+r:Nat -> @+remain:Nat -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.pad0(r, remain, index, s, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.gather(r, 33n, index, 1, True{}, remain, s, [], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law absorb_correct provedsource · line 2227 · raw

@+r:Nat -> @a:Array<U32> -> @+index:U32 -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.absorb(r, a, index, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.absorb(r, a, index, s) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State)}

law finish_correct provedsource · line 2237 · raw

@+r:Nat -> @a:Array<U32> -> @+index:U32 -> @+remain:Nat -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.finish(r, a, index, remain, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.finish(r, a, index, remain, s) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law blocks_correct provedsource · line 2248 · raw

@+r:Nat -> @+n:Nat -> @+index:U32 -> @+remain:Nat -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.blocks(r, n, index, remain, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.blocks(r, n, index, remain, pair) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law blocks_step provedsource · line 2256 · raw

@+r:Nat -> @+n:Nat -> @+index:U32 -> @+remain:Nat -> @-a:Array<U32> -> @+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/array.Tree, t => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/array.thaw(t) : Array<U32>}> -> @recurse:(@pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.blocks(r, n, U32.add(index, 34), remain, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.blocks(r, n, U32.add(index, 34), remain, pair) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.blocks(r, 1n+n, index, remain, (a, s)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.blocks(r, 1n+n, index, remain, (a, s)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law unchecked_correct provedsource · line 2285 · raw

@+r:Nat -> @a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.unchecked(r, a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.unchecked(r, a, length) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State}

law digest_correct provedsource · line 2294 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.digest(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.digest(s) : Array<U32>}

law checked_true_reified provedsource · line 2302 · raw

@+r:Nat -> @-a:Array<U32> -> @+length:Nat -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/array.Tree, t => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/array.thaw(t) : Array<U32>}> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.checked(r, True{}, a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.checked(r, True{}, a, length) : Maybe<&1, Array<U32>>}

law checked_correct provedsource · line 2320 · raw

@+r:Nat -> @+valid:Bool -> @a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.checked(r, valid, a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.checked(r, valid, a, length) : Maybe<&1, Array<U32>>}

law sized_correct provedsource · line 2332 · raw

@+r:Nat -> @+length:Nat -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.sized(r, length, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.sized(r, length, pair) : Maybe<&1, Array<U32>>}

law hash_correct provedsource · line 2342 · raw

@+r:Nat -> @a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256_rounds(r, a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.keccak256_rounds(r, a, length) : Maybe<&1, Array<U32>>}

law ethereum_round_count provedsource · line 2351 · raw

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256_rounds(24n, a, length) : Maybe<&1, Array<U32>>}

law public_correct provedsource · line 2358 · raw

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.keccak256(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.keccak256_rounds(24n, a, length) : Maybe<&1, Array<U32>>}