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

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

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

4 imports

import Base
import ../../../../src/crypto/blake/blake2b/types.bend as T
import ../../../../src/crypto/blake/blake2b/compress.bend as I
import ../../../../spec/crypto/blake/blake2b.bend as S

Laws

law column0_correct provedsource · line 7 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column0(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal0_correct provedsource · line 23 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal0(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round0_correct provedsource · line 39 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round0(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(0n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column1_correct provedsource · line 67 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column1(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal1_correct provedsource · line 83 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal1(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round1_correct provedsource · line 99 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round1(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(1n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column2_correct provedsource · line 127 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column2(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal2_correct provedsource · line 143 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal2(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round2_correct provedsource · line 159 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round2(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(2n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column3_correct provedsource · line 187 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column3(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal3_correct provedsource · line 203 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal3(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round3_correct provedsource · line 219 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round3(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(3n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column4_correct provedsource · line 247 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column4(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal4_correct provedsource · line 263 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal4(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round4_correct provedsource · line 279 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round4(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(4n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column5_correct provedsource · line 307 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column5(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal5_correct provedsource · line 323 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal5(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round5_correct provedsource · line 339 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round5(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(5n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column6_correct provedsource · line 367 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column6(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal6_correct provedsource · line 383 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal6(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round6_correct provedsource · line 399 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round6(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(6n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column7_correct provedsource · line 427 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column7(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal7_correct provedsource · line 443 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal7(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round7_correct provedsource · line 459 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round7(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(7n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column8_correct provedsource · line 487 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column8(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal8_correct provedsource · line 503 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal8(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round8_correct provedsource · line 519 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round8(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(8n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column9_correct provedsource · line 547 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column9(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal9_correct provedsource · line 563 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal9(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round9_correct provedsource · line 579 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round9(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(9n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column10_correct provedsource · line 607 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column10(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal10_correct provedsource · line 623 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal10(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round10_correct provedsource · line 639 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round10(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(0n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law column11_correct provedsource · line 667 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.column11(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 4n, 8n, 12n, x0, x1), 1n, 5n, 9n, 13n, x2, x3), 2n, 6n, 10n, 14n, x4, x5), 3n, 7n, 11n, 15n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law diagonal11_correct provedsource · line 683 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.diagonal11(v, x0, x1, x2, x3, x4, x5, x6, x7) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.G(v, 0n, 5n, 10n, 15n, x0, x1), 1n, 6n, 11n, 12n, x2, x3), 2n, 7n, 8n, 13n, x4, x5), 3n, 4n, 9n, 14n, x6, x7) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law round11_correct provedsource · line 699 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.round11(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.round(v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.sigma(1n)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law rounds_correct provedsource · line 727 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+m15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.rounds(v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.rounds(12n, 0n, v, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law start_correct provedsource · line 772 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.start(h, t) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.start(h, t, False{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law start_last_correct provedsource · line 781 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.start_last(h, t) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.start(h, t, True{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

law finish_correct provedsource · line 790 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.finish(h, v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.finish(h, v) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law compress_correct provedsource · line 799 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+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/compress.compress(h, t, 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) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.compress(h, [0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w0, w1}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w2, w3}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w4, w5}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w6, w7}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w8, w9}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w10, w11}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w12, w13}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w14, w15}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w16, w17}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w18, w19}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w20, w21}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w22, w23}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w24, w25}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w26, w27}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w28, w29}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w30, w31}], t, False{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law compress_last_correct provedsource · line 843 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+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/compress.compress_last(h, t, 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) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.compress(h, [0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w0, w1}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w2, w3}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w4, w5}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w6, w7}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w8, w9}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w10, w11}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w12, w13}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w14, w15}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w16, w17}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w18, w19}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w20, w21}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w22, w23}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w24, w25}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w26, w27}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w28, w29}, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.W{w30, w31}], t, True{}) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

law bump_correct provedsource · line 887 · raw

@+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.bump(c, x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.advance(c, x) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter}