~/bend-docscommunity

spec/crypto/argon2/argon2.bend checks

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

6 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
import ./blamka.bend as G

Definitions

def cat source · line 23 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> List<&2, U32>

def len source · line 26 · raw

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

def le32 source · line 32 · raw

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

LE32(n): the four little-endian bytes of n < 2^32.

def word source · line 36 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> U32

The little-endian word of four bytes.

def words source · line 40 · raw

@bs:List<&2, U32> -> List<&2, U32>

Bytes as little-endian words, the last one zero-padded.

def le source · line 53 · raw

@+w:U32 -> List<&2, U32>

def lane_bytes source · line 56 · raw

@l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> List<&2, U32>

def fill source · line 63 · raw

@ws:List<&2, U32> -> @+i:U32 -> @a:Array<U32> -> Array<U32>

def pw source · line 70 · raw

@k:Nat -> Nat

def depth_go source · line 77 · raw

@fuel:Nat -> @+n:Nat -> @+d:Nat -> @done:Bool -> Nat

def pack source · line 87 · raw

@bs:List<&2, U32> -> Array<U32>

The bytes packed in the BLAKE2b specification's input array.

def initial source · line 93 · raw

@+nn:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain

RFC 7693 section 2.5: h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0.

def chain_bytes source · line 96 · raw

@h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> List<&2, U32>

def hash source · line 103 · raw

@+nn:Nat -> @+bs:List<&2, U32> -> List<&2, U32>

H^nn(bs): BLAKE2b with an nn-byte digest, 1 <= nn <= 64: the first nn bytes of h after the dd = max(1, ceil(ll / 128)) blocks.

def hp_go source · line 115 · raw

@n:Nat -> @v:List<&2, U32> -> @+last:Nat -> List<&2, U32>

r = ceil(T / 32) - 2; V1 = H^64(LE32(T) || A), V_{i+1} = H^64(V_i), V_{r+1} = H^{T - 32r}(V_r); the output is W1 || .. || Wr || V_{r+1}, Wi the first 32 bytes of Vi. (V_i is a 64-byte digest, never empty; it is inspected first so that proofs keep the chain of hashes folded.)

def hp_pick source · line 124 · raw

@+tl:Nat -> @+x:List<&2, U32> -> @short:Bool -> List<&2, U32>

def hprime source · line 133 · raw

@+tl:Nat -> @a:List<&2, U32> -> List<&2, U32>

H'^T(a) = H^T(LE32(T) || a) if T <= 64, else as hp_go.

def h0 source · line 139 · raw

@+p:Nat -> @+tl:Nat -> @+m:Nat -> @+t:Nat -> @+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> List<&2, U32>

H0 = H^64(LE32(p) || LE32(T) || LE32(m) || LE32(t) || LE32(v) || LE32(y) || LE32(|P|) || P || LE32(|S|) || S || LE32(|K|) || K || LE32(|X|) || X), with v = 0x13 and y = 2 (Argon2id).

def row_of source · line 145 · raw

@ws:List<&2, U32> -> Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>)

32 words (a row) as sixteen lanes, and the words left.

def rows_of7 source · line 152 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of6 source · line 156 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of5 source · line 160 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of4 source · line 164 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of3 source · line 168 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of2 source · line 172 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of1 source · line 176 · raw

@r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def rows_of0 source · line 180 · raw

@p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

def block_of source · line 185 · raw

@bs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

The block of 1024 bytes: lane n is the little-endian 64-bit word of bytes 8n .. 8n + 7.

def state_bytes source · line 188 · raw

@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> List<&2, U32>

def block_bytes source · line 194 · raw

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

The 1024 bytes of a block.

def get source · line 202 · raw

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

B[i][j] of the memory is element i * q + j; a block out of range reads as zero.

def set source · line 205 · raw

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

def small source · line 210 · raw

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

def input_of source · line 214 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+ctr:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

Z = (r, l, s, m', t, y, i) as the first seven 64-bit lanes of a zero block.

def input_block source · line 219 · raw

@r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+ctr:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

(r is inspected first, so that proofs keep an input block with a symbolic pass number folded instead of evaluating G on it.)

def addresses source · line 227 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+ctr:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

The address block with counter ctr: G(ZERO, G(ZERO, Z)).

def regen source · line 233 · raw

@need:Bool -> @addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+idx:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

In a data-independent segment a new address block is computed for the segment's first position and at every multiple of 128, with counter idx / 128 + 1 (the i-th address block has counter i).

def area_base source · line 246 · raw

@r0:Bool -> @+s:Nat -> @+sl:Nat -> @+q:Nat -> Nat

|W|: in the first pass, the blocks of finished segments of the lane (all previous blocks of the segment too, when the reference lane is the current one); in later passes the last three segments of the lane, plus the current segment's previous blocks for the same lane; never the block just before the current one ("minus one" when the current index is the first of its segment and the lane is another one).

def area_other source · line 253 · raw

@+base:Nat -> @zero:Bool -> Nat

def area source · line 260 · raw

@+base:Nat -> @+idx:Nat -> @same:Bool -> Nat

def rel source · line 268 · raw

@+w:Nat -> @+j1:U32 -> Nat

x = J1^2 / 2^32; y = (|W| * x) / 2^32; zz = |W| - 1 - y.

def start_last source · line 272 · raw

@+s:Nat -> @+sl:Nat -> @last:Bool -> Nat

def start source · line 280 · raw

@r0:Bool -> @+s:Nat -> @+sl:Nat -> Nat

The reference area starts at 0 in the first pass, else at the next segment.

def ref_lane source · line 288 · raw

@forced:Bool -> @+l:Nat -> @+j2:U32 -> @+p:Nat -> Nat

l = J2 mod p, except in the first slice of the first pass (the current lane).

def prev_index source · line 296 · raw

@+l:Nat -> @+q:Nat -> @+j:Nat -> @first:Bool -> Nat

The previous block: B[l][j - 1], or B[l][q - 1] for j = 0.

def pick source · line 305 · raw

@indep:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+idx:Nat -> @+prev:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane

J1 || J2: the address block's lane idx mod 128 (data-independent), or the first lane of the previous block (data-dependent).

def lo source · line 312 · raw

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

def hi source · line 317 · raw

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

def store source · line 326 · raw

@r0:Bool -> @+cur:Nat -> @+prev:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+refb:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

B[l][j] = G(B[l][j-1], B[l'][z']) in the first pass; XORed into the old B[l][j] in later passes (version 0x13).

def step source · line 333 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+cur:Nat -> @+indep:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+prev:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

def seg_go source · line 342 · raw

@n:Nat -> @+idx:Nat -> @first:Bool -> @addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+indep:Bool -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

Positions idx .. idx + n - 1 of segment (r, s) of lane l.

def start_index source · line 353 · raw

@first:Bool -> Nat

def segment source · line 362 · raw

@+r:Nat -> @+s:Nat -> @+l:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

Segment s of lane l in pass r; data-independent addressing (Argon2i) in the first two slices of the first pass, data-dependent (Argon2d) otherwise.

def lanes_go source · line 367 · raw

@n:Nat -> @+l:Nat -> @+r:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

def slices_go source · line 374 · raw

@n:Nat -> @+s:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

def passes_go source · line 381 · raw

@n:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

def init_go source · line 389 · raw

@n:Nat -> @+l:Nat -> @+q:Nat -> @+hh:List<&2, U32> -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block>

B[l][0] = H'^1024(H0 || LE32(0) || LE32(l)), B[l][1] = H'^1024(H0 || LE32(1) || LE32(l)).

def final_go source · line 400 · raw

@n:Nat -> @+l:Nat -> @+q:Nat -> @c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block

C = B[0][q-1] XOR B[1][q-1] XOR .. XOR B[p-1][q-1]: b is B[l][q-1], n more lanes follow.

def valid source · line 412 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> Bool

RFC 9106 section 3.1: 1 <= p <= 2^24 - 1, 4 <= T <= 2^32 - 1, 8p <= m <= 2^32 - 1, 1 <= t <= 2^32 - 1, 8 <= |S| <= 2^32 - 1 and |P|, |K|, |X| <= 2^32 - 1.

def run source · line 418 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> List<&2, U32>

The tag: m' = 4p floor(m / 4p) blocks, q = m' / p columns, segments of q / 4.

def checked source · line 426 · raw

@ok:Bool -> @+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> Maybe<&2, List<&2, U32>>

def argon2id source · line 435 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> Maybe<&2, List<&2, U32>>

Argon2id(P, S, K, X; t passes, m KiB of memory, p lanes, T tag bytes), or None when a parameter is out of range.