src/crypto/argon2/argon2.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/argon2.bend as Argon2

8 imports

import Base
import ../../math/w64.bend as X
import ../blake/blake2b/types.bend as T
import ../blake/blake2b/sized.bend as H
import ./types.bend as A
import ./blamka.bend as G
import ./sub.bend as SB
import ./memory.bend as M

Definitions

def cat source · line 15 · raw

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

def len source · line 18 · raw

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

def le32 source · line 22 · raw

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

LE32(n) for n < 2^32.

def hp_go source · line 31 · raw

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

H' for T > 64 (RFC 9106 section 3.3): W1 || .. || Wr || V_{r+1}, where Wi is the first 32 bytes of Vi, V_{i+1} = H^64(Vi) and V_{r+1} = H^{T-32r}(Vr). (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 40 · raw

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

def hprime source · line 49 · raw

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

H'^T(a): the variable-length hash, over LE32(T) || a.

def h0 source · line 53 · 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 (RFC 9106 section 3.2, step 1), version 0x13 and type 2 (Argon2id).

def block_of source · line 59 · raw

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

A block from its 1024 little-endian bytes.

def state_bytes source · line 62 · raw

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

def block_bytes source · line 68 · raw

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

The 1024 little-endian bytes of a block.

def row_at source · line 73 · raw

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

def at source · line 92 · raw

@v:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/blake/blake2b/types.State -> @+j:Nat -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/blake/blake2b/types.Lane

def lane source · line 130 · raw

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

Lane n (0 <= n < 128) of a block.

def hi source · line 135 · raw

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

def small source · line 140 · raw

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

def input_of source · line 144 · raw

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

Z = (r, l, s, m', t, y, i), zero-padded to a block.

def input_block source · line 149 · raw

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

(r is inspected first, so the proofs keep an input block with a symbolic pass folded instead of compressing it symbolically.)

def addresses source · line 157 · raw

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

The address block of counter ctr: G(0, G(0, Z)).

def regen source · line 162 · raw

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

The address block for position idx: a new one at the segment's first position and at every multiple of 128 (data-independent segments only).

def area_base source · line 170 · raw

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

|W|, the number of blocks the reference may be drawn from.

def area_other source · line 177 · raw

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

def area source · line 184 · raw

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

def rel source · line 192 · raw

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

|W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32

def start_last source · line 196 · raw

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

def start source · line 205 · raw

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

The first block of the reference area: 0 in the first pass, else the start of the next segment (wrapping).

def ref_lane source · line 212 · raw

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

def prev_index source · line 219 · raw

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

def pick source · line 226 · raw

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

def store_xor source · line 235 · raw

@+cur:Nat -> @+prev:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @+refb:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block) -> Array<U32>

def store source · line 240 · raw

@r0:Bool -> @+cur:Nat -> @+prev:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @+refb:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @a:Array<U32> -> Array<U32>

B[l][j] = G(B[l][j-1], B[l'][z']), XORed into the old block after the first pass.

def with_ref source · line 247 · raw

@r0:Bool -> @+cur:Nat -> @+prev:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block) -> Array<U32>

def step source · line 252 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+cur:Nat -> @+indep:Bool -> @+addr:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block) -> Array<U32>

One block: pair holds the memory and the previous block.

def seg_go source · line 262 · raw

@n:Nat -> @+idx:Nat -> @first:Bool -> @addr:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @a:Array<U32> -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+indep:Bool -> Array<U32>

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

def start_index source · line 272 · raw

@first:Bool -> Nat

def segment source · line 281 · raw

@+r:Nat -> @+s:Nat -> @+l:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @a:Array<U32> -> Array<U32>

Segment s of lane l in pass r; data-independent addressing in the first two slices of the first pass. The first two blocks of each lane are already set.

def lanes_go source · line 286 · raw

@n:Nat -> @+l:Nat -> @+r:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @a:Array<U32> -> Array<U32>

def slices_go source · line 293 · raw

@n:Nat -> @+s:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @a:Array<U32> -> Array<U32>

def passes_go source · line 300 · raw

@n:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @a:Array<U32> -> Array<U32>

def init_go source · line 308 · raw

@n:Nat -> @+l:Nat -> @+q:Nat -> @+hh:List<&2, U32> -> @a:Array<U32> -> Array<U32>

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 319 · raw

@n:Nat -> @+l:Nat -> @+q:Nat -> @c:0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block -> @pair:Pair(Array<U32>, 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block) -> 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/types.Block

C = B[0][q-1] XOR .. XOR B[p-1][q-1]: pair holds the memory and B[l][q-1], n more lanes follow.

def valid source · line 331 · 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 ranges: 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 blocks source · line 337 · raw

@+m:Nat -> @+p:Nat -> Nat

m' = 4p floor(m / 4p), the number of blocks.

def fits source · line 342 · raw

@+m:Nat -> @+p:Nat -> Bool

This implementation's limit: the memory of m' blocks is an array of at most 2^31 words, so m' <= 2^23 (8 GiB), the RFC allowing up to 2^32 - 1 KiB.

def run source · line 346 · 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 for valid parameters.

def checked source · line 355 · 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 365 · 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, p lanes, T tag bytes): the T-byte tag, or None when a parameter is out of the RFC 9106 ranges or the memory does not fit (fits).