spec/crypto/blake/blake3.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as Blake3

3 imports

import Base
import ../../../src/crypto/blake/blake3/types.bend as T
import ../../lib/common.bend as SC

Definitions

def iv source · line 24 · raw

List<&2, U32>

def msg_permutation source · line 27 · raw

List<&2, Nat>

def chunk_start source · line 30 · raw

U32

def chunk_end source · line 33 · raw

U32

def parent_flag source · line 36 · raw

U32

def root_flag source · line 39 · raw

U32

def at source · line 44 · raw

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

def put source · line 50 · raw

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

def cv_words source · line 56 · raw

@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> List<&2, U32>

def cv_of source · line 63 · raw

@+ws:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV

(Each list consumer below starts by matching its list, so that it stays an unevaluated call on a symbolic list; the Nil cases agree with the general formula, since at(Nil, i) = 0 and put(Nil, i, x) = Nil.)

def block_of source · line 70 · raw

@+ws:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block

def rotr source · line 80 · raw

@+x:U32 -> @+n:Nat -> U32

Right rotation by n bits, 0 < n < 32.

def g source · line 84 · raw

@+v:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+mx:U32 -> @+my:U32 -> List<&2, U32>

The quarter-round G on state positions a, b, c, d with message words mx, my.

def columns source · line 96 · raw

@+v:List<&2, U32> -> @+m:List<&2, U32> -> List<&2, U32>

A round mixes the columns, then the diagonals, of the 4x4 state.

def diagonals source · line 102 · raw

@+v:List<&2, U32> -> @+m:List<&2, U32> -> List<&2, U32>

def round source · line 108 · raw

@v:List<&2, U32> -> @+m:List<&2, U32> -> List<&2, U32>

def permute_go source · line 115 · raw

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

The message words are permuted between rounds: word i of the next round is word msg_permutation[i] of this one.

def permute source · line 120 · raw

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

def rounds source · line 123 · raw

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

def init source · line 131 · raw

@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @+t:U32 -> @+len:U32 -> @+flags:U32 -> List<&2, U32>

The initial state of compress(h, m, t, len, flags): h[0..7], IV[0..3], the counter t (low word, then the high word, always 0 here: an input has fewer than 2^32 chunks), the block length and the flags.

def output source · line 136 · raw

@+v:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV

The new chaining value: word i xor word i+8 of the final state (the 64-byte extended output is not needed for a 32-byte digest).

def compress source · line 140 · raw

@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @+t:U32 -> @+len:U32 -> @+flags:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV

Seven rounds over the block's words.

def gather source · line 148 · raw

@n:Nat -> @+base:U32 -> @+next:U32 -> @acc:List<&2, U32> -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, List<&2, U32>)

The sixteen words of the block at word index, in order.

def as_block source · line 153 · raw

@pair:Pair(Array<U32>, List<&2, U32>) -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)

def read_block source · line 157 · raw

@a:Array<U32> -> @+index:U32 -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block)

def low_bytes source · line 162 · raw

@w:U32 -> @k:Nat -> U32

A block holding len bytes (len <= 64) is zero past them: the word at byte offset pos keeps its min(4, len - pos) low bytes.

def keep source · line 170 · raw

@w:U32 -> @+pos:Nat -> @+len:Nat -> U32

def zero_tail source · line 173 · raw

@b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block -> @+len:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block

def chunk_blocks source · line 185 · raw

@n:Nat -> @+t:U32 -> @+index:U32 -> @+flags:U32 -> @+len:Nat -> @cv:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Block) -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)

The blocks of a chunk are compressed in order starting from the key (IV in hash mode), all with the chunk counter t; the first block carries CHUNK_START and the last CHUNK_END. The last block is not compressed here: it is the chunk's output node (2.5, 2.6 decide its flags and use). n blocks follow the current block (in pair); the last block has len bytes.

def chunk source · line 193 · raw

@a:Array<U32> -> @+t:U32 -> @+index:U32 -> @+len:Nat -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)

A chunk of len bytes (1..1024; 0 only for the empty message) at word index has max(1, ceil(len/64)) blocks: n = (len - 1) div 64 full blocks, then a last block of len - 64n bytes.

def chunk_at source · line 198 · raw

@more:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @a:Array<U32> -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out)

Every chunk but the last holds 1024 bytes; chunk t starts at word 256t.

def chunks source · line 205 · raw

@+n:Nat -> @+t:U32 -> @+index:U32 -> @+len:Nat -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out) -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out>

The outputs of the chunks, in order; pair holds the current chunk, n chunks follow it, the last one of len bytes.

def message_chunks source · line 212 · raw

@a:Array<U32> -> @+length:Nat -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out>

A message of length bytes has max(1, ceil(length/1024)) chunks: n = (length - 1) div 1024 full ones, then the last of length - 1024n bytes.

def cv source · line 220 · raw

@o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV

A node's chaining value: its compression with its own flags.

def parent source · line 226 · raw

@l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> @r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

A parent node: key IV, block = left child CV ++ right child CV, counter 0, length 64, flag PARENT.

def is_nil source · line 229 · raw

@xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> Bool

def first source · line 234 · raw

@xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

def join source · line 239 · raw

@l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> @alone:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

def tree source · line 250 · raw

@+h:Nat -> @+xs:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out

The tree over the chunk outputs xs, 1 <= |xs| <= 2^h. The chunks are its leaves in order; a left subtree is always complete with a power of two of chunks, the largest one that leaves at least one chunk to its right: with h = g+1 and |xs| > 2^g the left subtree takes the first 2^g chunks and the right one the rest, while |xs| <= 2^g (nothing left for the right) means the tree already fits in height g.

def root source · line 264 · raw

@o:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.Out -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV

The root node is compressed with ROOT added to its flags; the 32-byte digest is the resulting chaining value, words in little-endian order. A single chunk is itself the root.

def hash source · line 268 · raw

@a:Array<U32> -> @+length:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV

def digest source · line 272 · raw

@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.CV -> Array<U32>

def checked source · line 277 · raw

@valid:Bool -> @a:Array<U32> -> @+length:Nat -> Maybe<&1, Array<U32>>

def sized source · line 283 · raw

@+length:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&1, Array<U32>>

None when byte_length exceeds the 4 * capacity bytes the array can hold.

def blake3 source · line 287 · raw

@words:Array<U32> -> @byte_length:Nat -> Maybe<&1, Array<U32>>