~/bend-docscommunity

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

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

Generated by tools/generators/blake2s_gen.py; do not edit. The unrolled compression function refines the list-based RFC 7693 F.

The implementation runs ten explicit rounds. A proof-side model runs the same round function r times, selecting the permuted words by round index; for an abstract r both the model and the specification stay symbolic, so every comparison below is between one round at most. The theorem is then instantiated at r = 10, where the model coincides with the implementation.

4 imports
import Base
import ../../../../src/crypto/blake/blake2s/types.bend as T
import ../../../../src/crypto/blake/blake2s/compress.bend as C
import ../../../../spec/crypto/blake/blake2s.bend as R

Laws

law round0_correct provedsource · line 106 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(0n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(0n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round1_correct provedsource · line 130 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(1n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(1n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round2_correct provedsource · line 154 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(2n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(2n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round3_correct provedsource · line 178 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(3n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(3n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round4_correct provedsource · line 202 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(4n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(4n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round5_correct provedsource · line 226 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(5n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(5n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round6_correct provedsource · line 250 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(6n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(6n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round7_correct provedsource · line 274 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(7n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(7n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round8_correct provedsource · line 298 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(8n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(8n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round9_correct provedsource · line 322 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(9n, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(9n), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law round_correct provedsource · line 346 · raw

@+i:Nat -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(round_at(i, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.round(vec(v), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.sigma(i), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law rounds_correct provedsource · line 381 · raw

@+n:Nat -> @+i:Nat -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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 -> {vec(rounds(n, i, v, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.rounds(n, i, vec(v), [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15]) : List<&2, U32>}

law finish_correct provedsource · line 417 · raw

@+h0:U32 -> @+h1:U32 -> @+h2:U32 -> @+h3:U32 -> @+h4:U32 -> @+h5:U32 -> @+h6:U32 -> @+h7:U32 -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.finish(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.H{h0, h1, h2, h3, h4, h5, h6, h7}, v) == fin(h0, h1, h2, h3, h4, h5, h6, h7, vec(v)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law init_correct provedsource · line 433 · raw

@+h0:U32 -> @+h1:U32 -> @+h2:U32 -> @+h3:U32 -> @+h4:U32 -> @+h5:U32 -> @+h6:U32 -> @+h7:U32 -> @+t0:U32 -> @+t1:U32 -> @+last:Bool -> {vec(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.init(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.H{h0, h1, h2, h3, h4, h5, h6, h7}, t0, t1, last)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.invert(last, [h0, h1, h2, h3, h4, h5, h6, h7, 1779033703, 3144134277, 1013904242, 2773480762, U32.xor(1359893119, t0), U32.xor(2600822924, t1), 528734635, 1541459225]) : List<&2, U32>}

law model_correct provedsource · line 452 · raw

@+r:Nat -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+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 -> @+t0:U32 -> @+t1:U32 -> @+last:Bool -> {model(r, h, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15, t0, t1, last) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.compress(r, h, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], t0, t1, last) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

law compress_correct provedsource · line 492 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+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 -> @+t0:U32 -> @+t1:U32 -> @+last:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.compress(h, m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15, t0, t1, last) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.compress(10n, h, [m0, m1, m2, m3, m4, m5, m6, m7, m8, m9, m10, m11, m12, m13, m14, m15], t0, t1, last) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State}

F as implemented (ten unrolled rounds) is F of the specification with r = 10.

Definitions

def p0 source · line 16 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

The work vector as the RFC list v[0..15], one projection per entry, so that the list has its shape even when the vector is abstract.

def p1 source · line 20 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p2 source · line 24 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p3 source · line 28 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p4 source · line 32 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p5 source · line 36 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p6 source · line 40 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p7 source · line 44 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p8 source · line 48 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p9 source · line 52 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p10 source · line 56 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p11 source · line 60 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p12 source · line 64 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p13 source · line 68 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p14 source · line 72 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def p15 source · line 76 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> U32

def vec source · line 80 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> List<&2, U32>

def round_at source · line 84 · raw

@i:Nat -> @v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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/src/crypto/blake/blake2s/types.Vector

Model: round i of the implementation reads the words in SIGMA[i mod 10] order.

def rounds source · line 98 · raw

@n:Nat -> @+i:Nat -> @v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.Vector -> @+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/src/crypto/blake/blake2s/types.Vector

def model source · line 103 · raw

@+r:Nat -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+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 -> @t0:U32 -> @t1:U32 -> @last:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State

def fin source · line 414 · raw

@h0:U32 -> @h1:U32 -> @h2:U32 -> @h3:U32 -> @h4:U32 -> @h5:U32 -> @h6:U32 -> @h7:U32 -> @+l:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State