proofs/crypto/blake/blake2s/reads.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/reads.bend as Reads

Generated by tools/generators/blake2s_gen.py; do not edit. Block reads, the last block, the block loop and the public API. The implementation keeps its own copy of the counter carry; each lemma carries the spec-side high counter half u1 with a proof e : t1 == u1.

8 imports

import Base
import ../../../../src/crypto/blake/blake2s/types.bend as T
import ../../../../src/crypto/blake/blake2s/compress.bend as C
import ../../../../src/crypto/blake/blake2s/blake2s.bend as K
import ../../../../spec/crypto/blake/blake2s.bend as R
import ./compress.bend as P
import ./bytes.bend as B
import ./array.bend as A

Laws

law carry_correct provedsource · line 14 · raw

@+c:Bool -> @+hi:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.carry(c, hi) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.carry(c, hi) : U32}

law count_correct provedsource · line 24 · raw

@+lo:U32 -> @+hi:U32 -> @+n:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.count_hi(lo, hi, n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.count_hi(lo, hi, n) : U32}

law block_correct provedsource · line 33 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/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 -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.compress(h, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, t0, t1, False{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.compress(10n, h, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.serialize([w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15])), t0, u1, False{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law last_correct provedsource · line 63 · raw

@+remain:Nat -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/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 -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.compress(h, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w0, 0n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w1, 4n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w2, 8n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w3, 12n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w4, 16n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w5, 20n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w6, 24n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w7, 28n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w8, 32n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w9, 36n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w10, 40n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w11, 44n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w12, 48n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w13, 52n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w14, 56n, remain), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad_word(w15, 60n, remain), t0, t1, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.compress(10n, h, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.pad(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.serialize([w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15]), 0n, remain)), t0, u1, True{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law read15_correct provedsource · line 94 · raw

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

law read14_correct provedsource · line 123 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read14(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(1n, index, 15, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read13_correct provedsource · line 151 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read13(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(2n, index, 14, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read12_correct provedsource · line 178 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read12(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(3n, index, 13, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read11_correct provedsource · line 204 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read11(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(4n, index, 12, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read10_correct provedsource · line 229 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read10(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(5n, index, 11, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read9_correct provedsource · line 253 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read9(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(6n, index, 10, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read8_correct provedsource · line 276 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.read8(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(7n, index, 9, [w7, w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read7_correct provedsource · line 298 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read7(index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(8n, index, 8, [w6, w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read6_correct provedsource · line 319 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read6(index, h, t0, t1, w0, w1, w2, w3, w4, w5, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(9n, index, 7, [w5, w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read5_correct provedsource · line 339 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read5(index, h, t0, t1, w0, w1, w2, w3, w4, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(10n, index, 6, [w4, w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read4_correct provedsource · line 358 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read4(index, h, t0, t1, w0, w1, w2, w3, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(11n, index, 5, [w3, w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read3_correct provedsource · line 376 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read3(index, h, t0, t1, w0, w1, w2, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(12n, index, 4, [w2, w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read2_correct provedsource · line 393 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read2(index, h, t0, t1, w0, w1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(13n, index, 3, [w1, w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read1_correct provedsource · line 409 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read1(index, h, t0, t1, w0, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(14n, index, 2, [w0], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law read0_correct provedsource · line 424 · raw

@+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.read0(index, h, t0, t1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.full_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(15n, index, 1, [], pair), h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law pad15_correct provedsource · line 438 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad15(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(0n, index, 16, [w14, w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad14_correct provedsource · line 468 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad14(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(1n, index, 15, [w13, w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad13_correct provedsource · line 497 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad13(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(2n, index, 14, [w12, w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad12_correct provedsource · line 525 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad12(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(3n, index, 13, [w11, w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad11_correct provedsource · line 552 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad11(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(4n, index, 12, [w10, w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad10_correct provedsource · line 578 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad10(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(5n, index, 11, [w9, w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad9_correct provedsource · line 603 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad9(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, w8, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(6n, index, 10, [w8, w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad8_correct provedsource · line 627 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+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/blake2s/blake2s.pad8(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, w7, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(7n, index, 9, [w7, w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad7_correct provedsource · line 650 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @+w6:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad7(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, w6, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(8n, index, 8, [w6, w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad6_correct provedsource · line 672 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @+w5:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad6(remain, index, h, t0, t1, w0, w1, w2, w3, w4, w5, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(9n, index, 7, [w5, w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad5_correct provedsource · line 693 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @+w4:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad5(remain, index, h, t0, t1, w0, w1, w2, w3, w4, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(10n, index, 6, [w4, w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad4_correct provedsource · line 713 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @+w3:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad4(remain, index, h, t0, t1, w0, w1, w2, w3, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(11n, index, 5, [w3, w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad3_correct provedsource · line 732 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @+w2:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad3(remain, index, h, t0, t1, w0, w1, w2, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(12n, index, 4, [w2, w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad2_correct provedsource · line 750 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @+w1:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad2(remain, index, h, t0, t1, w0, w1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(13n, index, 3, [w1, w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad1_correct provedsource · line 767 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+w0:U32 -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad1(remain, index, h, t0, t1, w0, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(14n, index, 2, [w0], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law pad0_correct provedsource · line 783 · raw

@+remain:Nat -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @pair:Pair(Array<U32>, U32) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.pad0(remain, index, h, t0, t1, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.last_block(10n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.gather(15n, index, 1, [], pair), remain, h, t0, u1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law absorb_correct provedsource · line 798 · raw

@a:Array<U32> -> @+index:U32 -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.absorb(a, index, h, t0, t1) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.absorb(10n, a, index, h, t0, u1) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)}

law finish_correct provedsource · line 811 · raw

@a:Array<U32> -> @+index:U32 -> @+t0:U32 -> @+t1:U32 -> @+remain:Nat -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.finish(a, index, t0, t1, remain, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.finish(10n, a, index, t0, t1, remain, h) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law blocks_step provedsource · line 823 · raw

@+n:Nat -> @+index:U32 -> @+t0:U32 -> @+t1:U32 -> @+remain:Nat -> @-a:Array<U32> -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @view:Sigma<&2, &1, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/array.Tree, t => {a == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/array.thaw(t) : Array<U32>}> -> @recurse:(@pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.blocks(n, U32.add(index, 16), U32.add(t0, 64), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.count_hi(t0, t1, 64), remain, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.blocks(10n, n, U32.add(index, 16), U32.add(t0, 64), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.count_hi(t0, t1, 64), remain, pair) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.blocks(1n+n, index, t0, t1, remain, (a, h)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.blocks(10n, 1n+n, index, t0, t1, remain, (a, h)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law blocks_correct provedsource · line 846 · raw

@+n:Nat -> @+index:U32 -> @+t0:U32 -> @+t1:U32 -> @+u1:U32 -> @e:{t1 == u1 : U32} -> @+remain:Nat -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.blocks(n, index, t0, t1, remain, pair) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.blocks(10n, n, index, t0, u1, remain, pair) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law leading_correct provedsource · line 866 · raw

@+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.leading(length) == Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.block_count(length), 1n) : Nat}

law hash_tail provedsource · line 875 · raw

@-a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.blocks(10n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.leading(length), 0, 0, 0, Nat.sub(length, Nat.mul(64n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.leading(length))), (a, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.initial)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.hash(10n, a, length) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law unchecked_correct provedsource · line 884 · raw

@a:Array<U32> -> @+length:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.unchecked(a, length) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.hash(10n, a, length) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law digest_correct provedsource · line 894 · raw

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

law checked_true provedsource · line 902 · raw

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

law checked_correct provedsource · line 919 · raw

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

law sized_correct provedsource · line 930 · raw

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

law blake2s_correct provedsource · line 939 · raw

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