~/bend-docscommunity

spec/crypto/argon2/blamka.bend checks

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

5 imports
import Base
import ../../lib/common.bend as C
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/argon2/types.bend as A
import ../blake/blake2b.bend as B

Definitions

def lane_of source · line 18 · raw

@+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane

The lane of n mod 2^64 (U32.from_nat keeps the low 32 bits).

def fBlaMka source · line 23 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane

fBlaMka(x, y) = x + y + 2 * trunc(x) * trunc(y), modulo 2^64, where trunc(x) * trunc(y) is the 64-bit product of the low 32 bits of x and y.

def GB source · line 30 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

GB(a, b, c, d) (RFC 9106 section 3.6).

def apply source · line 43 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def GBw source · line 49 · raw

@+w:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

(v_a, v_b, v_c, v_d) <- GB(v_a, v_b, v_c, v_d)

def GBi source · line 52 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def P source · line 60 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

The permutation P on sixteen lanes v0..v15: GB on the columns (0, 4, 8, 12), (1, 5, 9, 13), (2, 6, 10, 14), (3, 7, 11, 15), then on the diagonals (0, 5, 10, 15), (1, 6, 11, 12), (2, 7, 8, 13), (3, 4, 9, 14).

def row source · line 72 · raw

@b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @i:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def put_row source · line 91 · raw

@b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @i:Nat -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def lane source · line 111 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane

Lane n of a block, and the block with lane n replaced.

def put_lane source · line 114 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+n:Nat -> @x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def ix source · line 118 · raw

@xs:List<&2, Nat> -> @n:Nat -> Nat

def gather source · line 122 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+idx:List<&2, Nat> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

The sixteen lanes at the given lane numbers, as a state.

def put_lanes source · line 125 · raw

@idx:List<&2, Nat> -> @xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane> -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def scatter source · line 133 · raw

@b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @idx:List<&2, Nat> -> @s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

The block with the state's sixteen lanes stored at the given lane numbers.

def seq source · line 139 · raw

@n:Nat -> @+first:Nat -> @+step:Nat -> List<&2, Nat>

first, first + step, .., n terms.

def row_idx source · line 147 · raw

@+i:Nat -> List<&2, Nat>

Row i: lanes 16i, 16i + 1, .., 16i + 15.

def col_pairs source · line 152 · raw

@n:Nat -> @+first:Nat -> List<&2, Nat>

Column i: the 16-byte registers i, i + 8, .., i + 56, that is lanes 2i, 2i + 1, 2i + 16, 2i + 17, .., 2i + 112, 2i + 113.

def col_idx source · line 159 · raw

@+i:Nat -> List<&2, Nat>

def perms source · line 163 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @idxs:List<&2, List<&2, Nat>> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State>

P applied, independently, to the lanes of each index list of b.

def scatter_all source · line 170 · raw

@idxs:List<&2, List<&2, Nat>> -> @ss:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State> -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def permute source · line 177 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+idxs:List<&2, List<&2, Nat>> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_all source · line 180 · raw

List<&2, List<&2, Nat>>

def cols_all source · line 183 · raw

List<&2, List<&2, Nat>>

def rows source · line 188 · raw

@b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

(Q0, .., Q7) <- P(R0, .., R7), .., (Q56, .., Q63) <- P(R56, .., R63): P on each row of eight 16-byte registers.

def cols source · line 195 · raw

@b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

(Z0, Z8, .., Z56) <- P(Q0, Q8, .., Q56), .., (Z7, .., Z63) <- P(Q7, .., Q63): P on each column.

def xor_state source · line 200 · raw

@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def xor source · line 206 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

X XOR Y, lane by lane.

def G source · line 213 · raw

@x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

G(X, Y) = Z XOR R, where R = X XOR Y, Q = P on the rows of R and Z = P on the columns of Q (RFC 9106 section 3.5).

def zero_state source · line 217 · raw

0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def zero source · line 221 · raw

0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

The all-zero block.