src/crypto/argon2/blamka.bend checks

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

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

5 imports

import Base
import ../../math/w64.bend as X
import ../blake/blake2b/types.bend as T
import ../blake/blake2b/lane.bend as L
import ./types.bend as A

Definitions

def lo source · line 9 · raw

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

The low half of a lane (trunc in RFC 9106).

def prod source · line 14 · raw

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

The full 64-bit product of two U32 (src/math/w64.bend, proved).

def bla source · line 19 · 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) mod 2^64 (RFC 9106 section 3.6).

def gb4 source · line 26 · raw

@+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

GB (RFC 9106 section 3.6), one assignment pair per function.

def gb3 source · line 29 · raw

@+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

def gb2 source · line 33 · raw

@+a1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

def gb1 source · line 37 · raw

@+a1: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

def gb source · line 41 · 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

def put0 source · line 44 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x3: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 -> @x9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step0 source · line 50 · raw

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

GB on positions 0, 4, 8, 12.

def put1 source · line 55 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x0: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 -> @x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step1 source · line 61 · raw

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

GB on positions 1, 5, 9, 13.

def put2 source · line 66 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x1: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 -> @x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step2 source · line 72 · raw

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

GB on positions 2, 6, 10, 14.

def put3 source · line 77 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x2: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 -> @x8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step3 source · line 83 · raw

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

GB on positions 3, 7, 11, 15.

def put4 source · line 88 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @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 -> @x6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step4 source · line 94 · raw

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

GB on positions 0, 5, 10, 15.

def put5 source · line 99 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x0: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 -> @x7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step5 source · line 105 · raw

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

GB on positions 1, 6, 11, 12.

def put6 source · line 110 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x1: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 -> @x9:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x14:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step6 source · line 116 · raw

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

GB on positions 2, 7, 8, 13.

def put7 source · line 121 · raw

@q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad -> @x0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x2: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 -> @x8:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x10:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x11:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x12:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x13:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @x15:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State

def step7 source · line 127 · raw

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

GB on positions 3, 4, 9, 14.

def p source · line 133 · raw

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

The permutation P on sixteen lanes.

def rows source · line 137 · raw

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

P on each row: lanes 16i .. 16i+15.

def untr source · line 143 · raw

@c0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @c7:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

The eight permuted columns back into rows: column i holds lanes 2i, 2i+1 of every row.

def cols source · line 149 · raw

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

P on each column: lanes 2i, 2i+1, 2i+16, 2i+17, .., 2i+112, 2i+113.

def xs source · line 155 · raw

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

Lane-wise XOR of two rows, and of two blocks (row by row).

def xor source · line 160 · raw

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

def fin source · line 167 · raw

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

G(X, Y) = P(R) XOR R with R = X XOR Y, P on the rows then the columns (RFC 9106 section 3.5).

def compress source · line 170 · raw

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

def compress_xor source · line 174 · 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/types.Block

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

def zero source · line 178 · raw

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

The all-zero block.