spec/crypto/blake/blake2b.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as Blake2b
2 imports
import Base import ../../../src/crypto/blake/blake2b/types.bend as T
Definitions
def add source · line 21 · raw
@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
(a + b) mod 2^64: the low halves add modulo 2^32; the high halves add the carry out of the low half, which is 1 exactly when the low sum wrapped.
def xor source · line 27 · raw
@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
def rotr_small source · line 33 · raw
@+lo:U32 -> @+hi:U32 -> @+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
x >>> n for 0 < n < 32: each half takes its own bits shifted right and the other half's low bits shifted in from the top.
def rotr_split source · line 37 · raw
@lo:U32 -> @hi:U32 -> @+n:Nat -> @small:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
n > 32 rotates the swapped halves by n - 32.
def rotr source · line 43 · raw
@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+n:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
Right rotation of a 64-bit word by n (0 <= n < 64).
def iv source · line 52 · raw
@i:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
RFC 7693 section 2.6: IV[i], the SHA-512 initial hash values.
def sigma source · line 65 · raw
@r:Nat -> List<&2, Nat>
RFC 7693 section 2.7: the message word schedule SIGMA[r].
def nth source · line 79 · raw
@-A:Data -> @xs:List<&2, A> -> @n:Nat -> @+zero:A -> A
def at source · line 87 · raw
@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @i:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
def put source · line 107 · raw
@s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @i:Nat -> @x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State
def mix source · line 134 · raw
@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State
RFC 7693 section 3.1, the mixing function G with R1..R4 = 32, 24, 16, 63: v[a] := (v[a] + v[b] + x) mod 2^64; v[d] := (v[d] ^ v[a]) >>> R1 v[c] := (v[c] + v[d]) mod 2^64; v[b] := (v[b] ^ v[c]) >>> R2 v[a] := (v[a] + v[b] + y) mod 2^64; v[d] := (v[d] ^ v[a]) >>> R3 v[c] := (v[c] + v[d]) mod 2^64; v[b] := (v[b] ^ v[c]) >>> R4
def G source · line 146 · raw
@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State
G reads the vector's sixteen words and mixes the four at a, b, c, d.
def word source · line 152 · raw
@+m:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane> -> @+s:List<&2, Nat> -> @+j:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
m[s[j]]: the j-th message word of the round's schedule s.
def round source · line 156 · raw
@v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane> -> @+s:List<&2, Nat> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State
RFC 7693 section 3.2, one round of F with schedule s = SIGMA[i mod 10].
def rounds source · line 167 · raw
@n:Nat -> @+i:Nat -> @v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+m:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane> -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State
Rounds i, i+1, .., i+n-1.
def invert_if source · line 172 · raw
@last:Bool -> @x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane
def start source · line 179 · raw
@h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @last:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State
v[0..7] := h[0..7]; v[8..15] := IV[0..7]; v[12] ^= t mod 2^64; v[13] ^= t >> 64; if last block, v[14] := ~v[14].
def finish source · line 185 · raw
@h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain
h[i] := h[i] ^ v[i] ^ v[i + 8].
def compress source · line 191 · raw
@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @+m:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane> -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @last:Bool -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain
RFC 7693 section 3.2: F(h, m, t, f) with twelve rounds.
def advance source · line 197 · raw
@c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @+x:U32 -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter
t := t + x on the 128-bit counter, carrying from limb to limb.
def keep source · line 208 · raw
@w:U32 -> @n:Nat -> U32
The low n bytes of a little-endian word (all four when n >= 4).
def mask source · line 218 · raw
@w:U32 -> @+pos:Nat -> @+remain:Nat -> U32
The word holding block bytes pos..pos+3 when only remain bytes are message:
the bytes at or past remain are zero padding.
def trim source · line 221 · raw
@ws:List<&2, U32> -> @+pos:Nat -> @+remain:Nat -> List<&2, U32>
def prepare source · line 226 · raw
@last:Bool -> @ws:List<&2, U32> -> @remain:Nat -> List<&2, U32>
def lanes source · line 232 · raw
@ws:List<&2, U32> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane>
m[i] = the little-endian 64-bit word of block bytes 8i..8i+7.
def gather source · line 238 · raw
@n:Nat -> @+base:U32 -> @+next:U32 -> @+last:Bool -> @+remain:Nat -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> @acc:List<&2, U32> -> @pair:Pair(Array<U32>, U32) -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)
Reads the block's 32 words base+0 .. base+31 from the array, then compresses.
def absorb source · line 246 · raw
@a:Array<U32> -> @+index:U32 -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain)
A block that is not the last: t already counts its 128 bytes.
def final source · line 250 · raw
@a:Array<U32> -> @+index:U32 -> @+remain:Nat -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain
The last block: remain message bytes (1..128; 0 for the empty message), t := t + remain.
def blocks source · line 254 · raw
@n:Nat -> @+index:U32 -> @+remain:Nat -> @t:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Counter -> @pair:Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain) -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain
n blocks that are not the last, then the last one.
def initial source · line 262 · raw
0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain
h[0..7] := IV[0..7]; h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0, nn = 64.
def unchecked source · line 267 · raw
@a:Array<U32> -> @+length:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain
dd = max(1, ceil(ll / 128)) blocks: dd - 1 = (ll - 1) div 128 full blocks (0 when ll = 0), then the last block with the remaining ll - 128 (dd - 1) bytes.
def digest source · line 272 · raw
@h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> Array<U32>
The 64-byte digest h[0..7] as sixteen little-endian words.
def checked source · line 277 · raw
@valid:Bool -> @a:Array<U32> -> @length:Nat -> Maybe<&1, Array<U32>>
def sized source · line 282 · raw
@+length:Nat -> @pair:Pair(Array<U32>, U32) -> Maybe<&1, Array<U32>>
def blake2b source · line 288 · raw
@words:Array<U32> -> @byte_length:Nat -> Maybe<&1, Array<U32>>
BLAKE2b-512 of the first byte_length bytes of the packed words; None when byte_length exceeds the array's 4 * capacity bytes.