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

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

4 imports

import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/compress.bend as C
import ../../../../spec/crypto/blake/blake3.bend as S

Laws

law round_correct provedsource · line 19 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.St -> @+m0:U32 -> @+m1:U32 -> @+m2:U32 -> @+m3:U32 -> @+m4:U32 -> @+m5:U32 -> @+m6:U32 -> @+m7:U32 -> @+m8:U32 -> @+m9:U32 -> @+m10:U32 -> @+m11:U32 -> @+m12:U32 -> @+m13:U32 -> @+m14:U32 -> @+m15:U32 -> {st_list(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.round(s, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.round(st_list(s), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

One round, by evaluation on a symbolic state.

law step provedsource · line 45 · raw

@+k:Nat -> @+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.St -> @+m0:U32 -> @+m1:U32 -> @+m2:U32 -> @+m3:U32 -> @+m4:U32 -> @+m5:U32 -> @+m6:U32 -> @+m7:U32 -> @+m8:U32 -> @+m9:U32 -> @+m10:U32 -> @+m11:U32 -> @+m12:U32 -> @+m13:U32 -> @+m14:U32 -> @+m15:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.rounds(1n+k, st_list(x), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.rounds(k, st_list(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.round(x, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)), [m2, m6, m3, m10, m7, m0, m4, m13, m1, m11, m12, m5, m9, m14, m15, m8]) : List<&2, U32>}

One round of the specification's loop, with the permutation applied to the message words.

law rounds7_correct provedsource · line 70 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.St -> @+m0:U32 -> @+m1:U32 -> @+m2:U32 -> @+m3:U32 -> @+m4:U32 -> @+m5:U32 -> @+m6:U32 -> @+m7:U32 -> @+m8:U32 -> @+m9:U32 -> @+m10:U32 -> @+m11:U32 -> @+m12:U32 -> @+m13:U32 -> @+m14:U32 -> @+m15:U32 -> {st_list(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.rounds7(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.B{m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15})) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.rounds(7n, st_list(s), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law fold_correct provedsource · line 101 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.St -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.fold(s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.output(st_list(s)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

law init_correct provedsource · line 109 · raw

@+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+t:U32 -> @+len:U32 -> @+flags:U32 -> {st_list(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.init(c, t, len, flags)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.init(c, t, len, flags) : List<&2, U32>}

law compress_correct provedsource · line 120 · raw

@+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @+t:U32 -> @+len:U32 -> @+flags:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.compress(c, b, t, len, flags) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.compress(c, b, t, len, flags) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV}

Definitions

def st_list source · line 14 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.St -> List<&2, U32>