~/bend-docscommunity

proofs/crypto/blake/blake2b/blocks.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/blocks.bend as Blocks

Generated by tools/generators/blake2b_gen.py; do not edit by hand.

7 imports
import Base
import ../../../../src/crypto/blake/blake2b/types.bend as T
import ../../../../src/crypto/blake/blake2b/compress.bend as F
import ../../../../src/crypto/blake/blake2b/blake2b.bend as I
import ../../../../spec/crypto/blake/blake2b.bend as S
import ./compress.bend as C
import ./array.bend as A

Laws

law read31_correct provedsource · line 10 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read31(index, t, h, 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/blake/blake2b.gather(0n, index, 32, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read30_correct provedsource · line 52 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read30(index, t, h, 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/blake/blake2b.gather(1n, index, 31, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read29_correct provedsource · line 93 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read29(index, t, h, 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/blake/blake2b.gather(2n, index, 30, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read28_correct provedsource · line 133 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read28(index, t, h, 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/blake/blake2b.gather(3n, index, 29, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read27_correct provedsource · line 172 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read27(index, t, h, 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/blake/blake2b.gather(4n, index, 28, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read26_correct provedsource · line 210 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read26(index, t, h, 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/blake/blake2b.gather(5n, index, 27, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read25_correct provedsource · line 247 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read25(index, t, h, 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/blake/blake2b.gather(6n, index, 26, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read24_correct provedsource · line 283 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read24(index, t, h, 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/blake/blake2b.gather(7n, index, 25, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read23_correct provedsource · line 318 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read23(index, t, h, 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/blake/blake2b.gather(8n, index, 24, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read22_correct provedsource · line 352 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read22(index, t, h, 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/blake/blake2b.gather(9n, index, 23, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read21_correct provedsource · line 385 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read21(index, t, h, 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/blake/blake2b.gather(10n, index, 22, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read20_correct provedsource · line 417 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read20(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, w19, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(11n, index, 21, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read19_correct provedsource · line 448 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read19(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, w18, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(12n, index, 20, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read18_correct provedsource · line 478 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read18(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, w17, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(13n, index, 19, False{}, 0n, t, h, [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/blake/blake2b/types.Chain)}

law read17_correct provedsource · line 507 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read17(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(14n, index, 18, False{}, 0n, t, h, [w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read16_correct provedsource · line 535 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read16(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(15n, index, 17, False{}, 0n, t, h, [w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read15_correct provedsource · line 562 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read15(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(16n, index, 16, False{}, 0n, t, h, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read14_correct provedsource · line 588 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read14(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(17n, index, 15, False{}, 0n, t, h, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read13_correct provedsource · line 613 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read13(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(18n, index, 14, False{}, 0n, t, h, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read12_correct provedsource · line 637 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read12(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(19n, index, 13, False{}, 0n, t, h, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read11_correct provedsource · line 660 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read11(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(20n, index, 12, False{}, 0n, t, h, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read10_correct provedsource · line 682 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read10(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(21n, index, 11, False{}, 0n, t, h, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read9_correct provedsource · line 703 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.read9(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(22n, index, 10, False{}, 0n, t, h, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read8_correct provedsource · line 723 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read8(index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(23n, index, 9, False{}, 0n, t, h, [w7, w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read7_correct provedsource · line 742 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read7(index, t, h, w0, w1, w2, w3, w4, w5, w6, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(24n, index, 8, False{}, 0n, t, h, [w6, w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read6_correct provedsource · line 760 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read6(index, t, h, w0, w1, w2, w3, w4, w5, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(25n, index, 7, False{}, 0n, t, h, [w5, w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read5_correct provedsource · line 777 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read5(index, t, h, w0, w1, w2, w3, w4, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(26n, index, 6, False{}, 0n, t, h, [w4, w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read4_correct provedsource · line 793 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read4(index, t, h, w0, w1, w2, w3, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(27n, index, 5, False{}, 0n, t, h, [w3, w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read3_correct provedsource · line 808 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read3(index, t, h, w0, w1, w2, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(28n, index, 4, False{}, 0n, t, h, [w2, w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read2_correct provedsource · line 822 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read2(index, t, h, w0, w1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(29n, index, 3, False{}, 0n, t, h, [w1, w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read1_correct provedsource · line 835 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read1(index, t, h, w0, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(30n, index, 2, False{}, 0n, t, h, [w0], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law read0_correct provedsource · line 847 · raw

@+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.read0(index, t, h, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(31n, index, 1, False{}, 0n, t, h, [], pair) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law absorb_correct provedsource · line 858 · raw

@a:Array<U32> -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.absorb(a, index, t, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.absorb(a, index, t, h) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)}

law keep_correct provedsource · line 868 · raw

@+w:U32 -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.keep(w, n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.keep(w, n) : U32}

law masks_correct provedsource · line 881 · 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 -> {[0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w0, 0n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w1, 4n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w2, 8n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w3, 12n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w4, 16n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w5, 20n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w6, 24n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w7, 28n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w8, 32n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w9, 36n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w10, 40n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w11, 44n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w12, 48n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w13, 52n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w14, 56n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w15, 60n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w16, 64n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w17, 68n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w18, 72n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w19, 76n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w20, 80n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w21, 84n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w22, 88n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w23, 92n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w24, 96n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w25, 100n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w26, 104n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w27, 108n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w28, 112n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w29, 116n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w30, 120n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.mask(w31, 124n, remain)] == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.trim([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], 0n, remain) : List<&2, U32>}

law last31_correct provedsource · line 952 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last31(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(0n, index, 32, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last30_correct provedsource · line 997 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last30(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(1n, index, 31, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last29_correct provedsource · line 1039 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last29(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(2n, index, 30, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last28_correct provedsource · line 1080 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last28(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(3n, index, 29, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last27_correct provedsource · line 1120 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last27(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(4n, index, 28, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last26_correct provedsource · line 1159 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last26(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(5n, index, 27, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last25_correct provedsource · line 1197 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last25(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(6n, index, 26, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last24_correct provedsource · line 1234 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last24(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(7n, index, 25, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last23_correct provedsource · line 1270 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last23(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(8n, index, 24, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last22_correct provedsource · line 1305 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last22(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(9n, index, 23, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last21_correct provedsource · line 1339 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last21(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(10n, index, 22, True{}, remain, t, h, [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/blake/blake2b/types.Chain}

law last20_correct provedsource · line 1372 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last20(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(11n, index, 21, True{}, remain, t, h, [w19, w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last19_correct provedsource · line 1404 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last19(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(12n, index, 20, True{}, remain, t, h, [w18, w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last18_correct provedsource · line 1435 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last18(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(13n, index, 19, True{}, remain, t, h, [w17, w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last17_correct provedsource · line 1465 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last17(remain, index, t, h, 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/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(14n, index, 18, True{}, remain, t, h, [w16, w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last16_correct provedsource · line 1494 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last16(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(15n, index, 17, True{}, remain, t, h, [w15, w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last15_correct provedsource · line 1522 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last15(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(16n, index, 16, True{}, remain, t, h, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last14_correct provedsource · line 1549 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last14(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(17n, index, 15, True{}, remain, t, h, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last13_correct provedsource · line 1575 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last13(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(18n, index, 14, True{}, remain, t, h, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last12_correct provedsource · line 1600 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last12(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(19n, index, 13, True{}, remain, t, h, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last11_correct provedsource · line 1624 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last11(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(20n, index, 12, True{}, remain, t, h, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last10_correct provedsource · line 1647 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last10(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(21n, index, 11, True{}, remain, t, h, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last9_correct provedsource · line 1669 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+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/blake/blake2b/blake2b.last9(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(22n, index, 10, True{}, remain, t, h, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last8_correct provedsource · line 1690 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @+w7:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last8(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, w7, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(23n, index, 9, True{}, remain, t, h, [w7, w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last7_correct provedsource · line 1710 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last7(remain, index, t, h, w0, w1, w2, w3, w4, w5, w6, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(24n, index, 8, True{}, remain, t, h, [w6, w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last6_correct provedsource · line 1729 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last6(remain, index, t, h, w0, w1, w2, w3, w4, w5, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(25n, index, 7, True{}, remain, t, h, [w5, w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last5_correct provedsource · line 1747 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last5(remain, index, t, h, w0, w1, w2, w3, w4, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(26n, index, 6, True{}, remain, t, h, [w4, w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last4_correct provedsource · line 1764 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last4(remain, index, t, h, w0, w1, w2, w3, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(27n, index, 5, True{}, remain, t, h, [w3, w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last3_correct provedsource · line 1780 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last3(remain, index, t, h, w0, w1, w2, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(28n, index, 4, True{}, remain, t, h, [w2, w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last2_correct provedsource · line 1795 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last2(remain, index, t, h, w0, w1, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(29n, index, 3, True{}, remain, t, h, [w1, w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last1_correct provedsource · line 1809 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last1(remain, index, t, h, w0, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(30n, index, 2, True{}, remain, t, h, [w0], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law last0_correct provedsource · line 1822 · raw

@+remain:Nat -> @+index:U32 -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.last0(remain, index, t, h, pair) == Pair.snd(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.gather(31n, index, 1, True{}, remain, t, h, [], pair)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law final_correct provedsource · line 1834 · raw

@a:Array<U32> -> @+index:U32 -> @+remain:Nat -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.final(a, index, remain, t, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.final(a, index, remain, t, h) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law blocks_step provedsource · line 1846 · raw

@+n:Nat -> @+index:U32 -> @+remain:Nat -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @-a:Array<U32> -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/array.Tree, z => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/array.thaw(z) : Array<U32>}> -> @recurse:(@pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.blocks(n, U32.add(index, 32), remain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.advance(t, 128), pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.blocks(n, U32.add(index, 32), remain, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.advance(t, 128), pair) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.blocks(1n+n, index, remain, t, (a, h)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.blocks(1n+n, index, remain, t, (a, h)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law blocks_correct provedsource · line 1870 · raw

@+n:Nat -> @+index:U32 -> @+remain:Nat -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.blocks(n, index, remain, t, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.blocks(n, index, remain, t, pair) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law unchecked_correct provedsource · line 1884 · raw

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.unchecked(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.unchecked(a, length) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law digest_correct provedsource · line 1892 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.digest(h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.digest(h) : Array<U32>}

law checked_true_reified provedsource · line 1900 · raw

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

law checked_correct provedsource · line 1917 · raw

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

law sized_correct provedsource · line 1928 · raw

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

law blake2b_correct provedsource · line 1937 · raw

@words:Array<U32> -> @+byte_length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.blake2b(words, byte_length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.blake2b(words, byte_length) : Maybe<&1, Array<U32>>}