spec/crypto/blake/blake2s.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as Blake2s
2 imports
import Base import ../../../src/crypto/blake/blake2s/types.bend as T
Definitions
def iv source · line 16 · raw
List<&2, U32>
IV[0..7] = 0x6A09E667 0xBB67AE85 0x3C6EF372 0xA54FF53A 0x510E527F 0x9B05688C 0x1F83D9AB 0x5BE0CD19
def sigma source · line 20 · raw
@r:Nat -> List<&2, Nat>
SIGMA[i mod 10].
def get source · line 36 · raw
@xs:List<&2, U32> -> @i:Nat -> U32
def index source · line 42 · raw
@xs:List<&2, Nat> -> @i:Nat -> Nat
def put source · line 48 · raw
@xs:List<&2, U32> -> @i:Nat -> @y:U32 -> List<&2, U32>
def rotr source · line 57 · raw
@+x:U32 -> @+n:Nat -> U32
x >>> n: rotation of a 32-bit word right by n bits (0 < n < 32).
def mix source · line 61 · raw
@+v:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @x:U32 -> @y:U32 -> List<&2, U32>
G(v[0..15], a, b, c, d, x, y) with BLAKE2s rotations R1..R4 = 16, 12, 8, 7.
def round source · line 75 · raw
@v:List<&2, U32> -> @+s:List<&2, Nat> -> @+m:List<&2, U32> -> List<&2, U32>
One round with schedule s: four column steps, then four diagonal steps.
def rounds source · line 86 · raw
@n:Nat -> @+i:Nat -> @v:List<&2, U32> -> @+m:List<&2, U32> -> List<&2, U32>
Rounds i, i+1, ..., i+n-1.
def invert source · line 91 · raw
@last:Bool -> @+v:List<&2, U32> -> List<&2, U32>
def compress source · line 98 · raw
@+r:Nat -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+m:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @last:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State
F(h, m, t, f) with r rounds (r = 10 for BLAKE2s): t = t0 + 2^32 * t1 is the byte counter, f the final-block flag.
def byte source · line 118 · raw
@+w:U32 -> @k:Nat -> U32
Byte k (0 = least significant) of a word: the packed input holds four message bytes per word in little-endian order.
def octets source · line 121 · raw
@+w:U32 -> List<&2, U32>
def serialize source · line 124 · raw
@ws:List<&2, U32> -> List<&2, U32>
def keep_if source · line 130 · raw
@inside:Bool -> @b:U32 -> U32
Zero padding: the byte at message offset i survives only when i < length.
def pad source · line 135 · raw
@bytes:List<&2, U32> -> @+i:Nat -> @+length:Nat -> List<&2, U32>
def word source · line 141 · raw
@b0:U32 -> @b1:U32 -> @b2:U32 -> @b3:U32 -> U32
A block word from four bytes, least significant first.
def words source · line 144 · raw
@bytes:List<&2, U32> -> List<&2, U32>
def carry source · line 152 · raw
@c:Bool -> @hi:U32 -> U32
The byte counter t as two 32-bit halves: t + n, with the carry into t1.
def count_hi source · line 157 · raw
@+lo:U32 -> @hi:U32 -> @+n:U32 -> U32
def gather source · line 161 · raw
@n:Nat -> @+base:U32 -> @+next:U32 -> @acc:List<&2, U32> -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, List<&2, U32>)
Read the sixteen words of the block at word offset base, in order.
def read_block source · line 166 · raw
@a:Array<U32> -> @+base:U32 -> Pair(Array<U32>, List<&2, U32>)
def full_block source · line 170 · raw
@+r:Nat -> @pair:Pair(Array<U32>, List<&2, U32>) -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)
A block before the last: all 64 bytes are message bytes.
def last_block source · line 175 · raw
@+r:Nat -> @pair:Pair(Array<U32>, List<&2, U32>) -> @+remain:Nat -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State
The last block: the remaining bytes, zero-padded to 64.
def absorb source · line 179 · raw
@+r:Nat -> @a:Array<U32> -> @+base:U32 -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> @+t0:U32 -> @+t1:U32 -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State)
def finish source · line 182 · raw
@+r:Nat -> @a:Array<U32> -> @+base:U32 -> @+t0:U32 -> @t1:U32 -> @+remain:Nat -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State
def blocks source · line 187 · raw
@+r:Nat -> @n:Nat -> @+base:U32 -> @+t0:U32 -> @t1:U32 -> @+remain:Nat -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State
n full blocks, then the last one; t counts the bytes compressed so far.
def initial source · line 196 · raw
0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State
h[0..7] := IV[0..7]; h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0, nn = 32.
def block_count source · line 200 · raw
@+ll:Nat -> Nat
dd = ceil(ll / 64) blocks, and dd = 1 for the empty message.
def hash source · line 205 · raw
@+r:Nat -> @a:Array<U32> -> @+ll:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State
def digest source · line 210 · raw
@h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.State -> Array<U32>
The 32-byte digest as eight little-endian words, in a fresh 8-slot array.
def checked source · line 215 · raw
@+r:Nat -> @valid:Bool -> @a:Array<U32> -> @ll:Nat -> Maybe<&1, Array<U32>>
def sized source · line 220 · raw
@+r:Nat -> @+ll:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&1, Array<U32>>
def blake2s_rounds source · line 226 · raw
@+r:Nat -> @a:Array<U32> -> @ll:Nat -> Maybe<&1, Array<U32>>
The hash with r rounds per compression, of the first ll bytes of the packed array a; None when ll exceeds the 4 * capacity bytes the array holds.
def blake2s source · line 230 · raw
@a:Array<U32> -> @ll:Nat -> Maybe<&1, Array<U32>>
BLAKE2s-256: r = 10.