~/bend-docscommunity

proofs/crypto/argon2/blamka.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as Blamka

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

6 imports
import Base
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/argon2/types.bend as A
import ../../../src/crypto/argon2/blamka.bend as I
import ../../../spec/crypto/argon2/blamka.bend as S
import ./gb.bend as GB

Definitions

def step0_correct source · line 15 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step0(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 0n, 4n, 8n, 12n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step1_correct source · line 20 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step1(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 1n, 5n, 9n, 13n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step2_correct source · line 25 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step2(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 2n, 6n, 10n, 14n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step3_correct source · line 30 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step3(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 3n, 7n, 11n, 15n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step4_correct source · line 35 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step4(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 0n, 5n, 10n, 15n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step5_correct source · line 40 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step5(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 1n, 6n, 11n, 12n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step6_correct source · line 45 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step6(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 2n, 7n, 8n, 13n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def step7_correct source · line 50 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.step7(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GBi(v, 3n, 4n, 9n, 14n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def p_correct source · line 56 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.p(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.P(v) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

P, one GB at a time.

def rows_correct source · line 74 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.rows(b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.rows(b) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

P on the rows: the rows are the specification's gathered lanes.

def cols_correct source · line 94 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.cols(b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.cols(b) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

P on the columns: column i of the specification is lanes 2i, 2i+1, 2i+16, ...

def xs_correct source · line 114 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.xs(s, t) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.xor_state(s, t) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

Two rows XORed, lane by lane.

def xor_correct source · line 120 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.xor(x, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.xor(x, y) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

X XOR Y, row by row.

def compress_correct source · line 134 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.compress(x, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.G(x, y) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

G(X, Y): the compression function.

def compress_xor_correct source · line 144 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+old:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.compress_xor(x, y, old) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.xor(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.G(x, y), old) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

Version 0x13 passes after the first: G(X, Y) XOR the old block.

def zero_correct source · line 150 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.zero == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.zero : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

The all-zero block.