1 import Base 2 import ../../../src/crypto/blake/blake3/types.bend as T 3 import ../../lib/common.bend as SC 4 5 # BLAKE3 in hash mode with a 32-byte output, written from the BLAKE3 6 # specification document (O'Connor, Aumasson, Neves, Wilcox-O'Hearn, 2020): 7 # section 2.2 (the compression function), 2.3 (modes: hash mode keys with IV), 8 # 2.4 (chunks), 2.5 (the tree) and 2.6 (the root and its output). 9 # 10 # This file is independent of the implementation in src/crypto/blake/blake3/: 11 # it shares only the plain record types CV, Block and Out and never calls the 12 # implementation. It favours the document's structure over speed: the state 13 # and the message are lists indexed by position, the message schedule comes 14 # from repeatedly applying the permutation table, and the tree is defined 15 # recursively by its shape rather than by the implementation's stack. 16 # 17 # Input convention: the message is an array of U32 words holding its bytes 18 # little-endian, four per word (byte 4i+j is bits 8j..8j+7 of word i); 19 # byte_length is the logical length. A 64-byte block is therefore sixteen 20 # consecutive words, and a block of len < 64 bytes is zero past its len bytes. 21 22 # ---- constants (2.2, 2.3) ---- 23 24 def iv() -> List<&2,U32>: 25 [1779033703,3144134277,1013904242,2773480762,1359893119,2600822924,528734635,1541459225] 26 27 def msg_permutation() -> List<&2,Nat>: 28 [2n,6n,3n,10n,7n,0n,4n,13n,1n,11n,12n,5n,9n,14n,15n,8n] 29 30 def chunk_start() -> U32: 31 1 32 33 def chunk_end() -> U32: 34 2 35 36 def parent_flag() -> U32: 37 4 38 39 def root_flag() -> U32: 40 8 41 42 # ---- word lists ---- 43 44 def at(xs: List<&2,U32>, i: Nat) -> U32: 45 match xs i: 46 case Nil{} _: 0 47 case Con{x,r} 0n: x 48 case Con{x,r} 1n+j: at(r,j) 49 50 def put(xs: List<&2,U32>, i: Nat, +v: U32) -> List<&2,U32>: 51 match xs i: 52 case Nil{} _: Nil{} 53 case Con{x,r} 0n: Con{v,r} 54 case Con{x,r} 1n+j: Con{x,put(r,j,v)} 55 56 def cv_words(c: T.CV) -> List<&2,U32>: 57 match c: 58 case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: [h0,h1,h2,h3,h4,h5,h6,h7] 59 60 # (Each list consumer below starts by matching its list, so that it stays an 61 # unevaluated call on a symbolic list; the Nil cases agree with the general 62 # formula, since at(Nil, i) = 0 and put(Nil, i, x) = Nil.) 63 def cv_of(+ws: List<&2,U32>) -> T.CV: 64 match ws: 65 case Nil{}: T.CV{0,0,0,0,0,0,0,0} 66 case Con{+x,+r}: 67 +l = {Con{x,r} : List<&2,U32>} 68 T.CV{at(l,0n),at(l,1n),at(l,2n),at(l,3n),at(l,4n),at(l,5n),at(l,6n),at(l,7n)} 69 70 def block_of(+ws: List<&2,U32>) -> T.Block: 71 match ws: 72 case Nil{}: T.B{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0} 73 case Con{+x,+r}: 74 +l = {Con{x,r} : List<&2,U32>} 75 T.B{at(l,0n),at(l,1n),at(l,2n),at(l,3n),at(l,4n),at(l,5n),at(l,6n),at(l,7n),at(l,8n),at(l,9n),at(l,10n),at(l,11n),at(l,12n),at(l,13n),at(l,14n),at(l,15n)} 76 77 # ---- the compression function (2.2) ---- 78 79 # Right rotation by n bits, 0 < n < 32. 80 def rotr(+x: U32, +n: Nat) -> U32: 81 U32.or(U32.shrn(x,n),U32.shln(x,Nat.sub(32n,n))) 82 83 # The quarter-round G on state positions a, b, c, d with message words mx, my. 84 def g(+v: List<&2,U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +mx: U32, +my: U32) -> List<&2,U32>: 85 +va = U32.add(U32.add(at(v,a),at(v,b)),mx) 86 +vd = rotr(U32.xor(at(v,d),va),16n) 87 +vc = U32.add(at(v,c),vd) 88 +vb = rotr(U32.xor(at(v,b),vc),12n) 89 +va2 = U32.add(U32.add(va,vb),my) 90 +vd2 = rotr(U32.xor(vd,va2),8n) 91 +vc2 = U32.add(vc,vd2) 92 +vb2 = rotr(U32.xor(vb,vc2),7n) 93 put(put(put(put(v,a,va2),b,vb2),c,vc2),d,vd2) 94 95 # A round mixes the columns, then the diagonals, of the 4x4 state. 96 def columns(+v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>: 97 +v1 = g(v,0n,4n,8n,12n,at(m,0n),at(m,1n)) 98 +v2 = g(v1,1n,5n,9n,13n,at(m,2n),at(m,3n)) 99 +v3 = g(v2,2n,6n,10n,14n,at(m,4n),at(m,5n)) 100 g(v3,3n,7n,11n,15n,at(m,6n),at(m,7n)) 101 102 def diagonals(+v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>: 103 +v1 = g(v,0n,5n,10n,15n,at(m,8n),at(m,9n)) 104 +v2 = g(v1,1n,6n,11n,12n,at(m,10n),at(m,11n)) 105 +v3 = g(v2,2n,7n,8n,13n,at(m,12n),at(m,13n)) 106 g(v3,3n,4n,9n,14n,at(m,14n),at(m,15n)) 107 108 def round(v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>: 109 match v: 110 case Nil{}: Nil{} 111 case Con{+x,+r}: diagonals(columns(Con{x,r},m),m) 112 113 # The message words are permuted between rounds: word i of the next round is 114 # word msg_permutation[i] of this one. 115 def permute_go(ps: List<&2,Nat>, +m: List<&2,U32>) -> List<&2,U32>: 116 match ps: 117 case Nil{}: Nil{} 118 case Con{p,r}: Con{at(m,p),permute_go(r,m)} 119 120 def permute(+m: List<&2,U32>) -> List<&2,U32>: 121 permute_go(msg_permutation(),m) 122 123 def rounds(n: Nat, +v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>: 124 match n: 125 case 0n: v 126 case 1n+k: rounds(k,round(v,m),permute(m)) 127 128 # The initial state of compress(h, m, t, len, flags): h[0..7], IV[0..3], the 129 # counter t (low word, then the high word, always 0 here: an input has fewer 130 # than 2^32 chunks), the block length and the flags. 131 def init(c: T.CV, +t: U32, +len: U32, +flags: U32) -> List<&2,U32>: 132 SC.append(U32,cv_words(c),[at(iv(),0n),at(iv(),1n),at(iv(),2n),at(iv(),3n),t,0,len,flags]) 133 134 # The new chaining value: word i xor word i+8 of the final state (the 64-byte 135 # extended output is not needed for a 32-byte digest). 136 def output(+v: List<&2,U32>) -> T.CV: 137 T.CV{U32.xor(at(v,0n),at(v,8n)),U32.xor(at(v,1n),at(v,9n)),U32.xor(at(v,2n),at(v,10n)),U32.xor(at(v,3n),at(v,11n)),U32.xor(at(v,4n),at(v,12n)),U32.xor(at(v,5n),at(v,13n)),U32.xor(at(v,6n),at(v,14n)),U32.xor(at(v,7n),at(v,15n))} 138 139 # Seven rounds over the block's words. 140 def compress(c: T.CV, b: T.Block, +t: U32, +len: U32, +flags: U32) -> T.CV: 141 match b: 142 case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}: 143 output(rounds(7n,init(c,t,len,flags),[m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15])) 144 145 # ---- reading blocks ---- 146 147 # The sixteen words of the block at word `index`, in order. 148 def gather(n: Nat, +base: U32, +next: U32, acc: List<&2,U32>, pair: Array & U32) -> Array & List<&2,U32>: 149 match n pair: 150 case 0n Tuple{a,w}: (a,List.reverse(&2,U32,Con{w,acc})) 151 case 1n+p Tuple{a,w}: gather(p,base,U32.inc(next),Con{w,acc},Array.get(U32,a,U32.add(base,next))) 152 153 def as_block(pair: Array & List<&2,U32>) -> Array & T.Block: 154 (a,ws) = pair 155 (a,block_of(ws)) 156 157 def read_block(a: Array, +index: U32) -> Array & T.Block: 158 as_block(gather(15n,index,1,Nil{},Array.get(U32,a,index))) 159 160 # A block holding len bytes (len <= 64) is zero past them: the word at byte 161 # offset pos keeps its min(4, len - pos) low bytes. 162 def low_bytes(w: U32, k: Nat) -> U32: 163 match k: 164 case 0n: 0 165 case 1n: U32.and(w,255) 166 case 2n: U32.and(w,65535) 167 case 3n: U32.and(w,16777215) 168 case 4n+q: w 169 170 def keep(w: U32, +pos: Nat, +len: Nat) -> U32: 171 low_bytes(w,Nat.min(4n,Nat.sub(len,pos))) 172 173 def zero_tail(b: T.Block, +len: Nat) -> T.Block: 174 match b: 175 case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}: 176 T.B{keep(m0,0n,len),keep(m1,4n,len),keep(m2,8n,len),keep(m3,12n,len),keep(m4,16n,len),keep(m5,20n,len),keep(m6,24n,len),keep(m7,28n,len),keep(m8,32n,len),keep(m9,36n,len),keep(m10,40n,len),keep(m11,44n,len),keep(m12,48n,len),keep(m13,52n,len),keep(m14,56n,len),keep(m15,60n,len)} 177 178 # ---- chunks (2.4) ---- 179 180 # The blocks of a chunk are compressed in order starting from the key (IV in 181 # hash mode), all with the chunk counter t; the first block carries 182 # CHUNK_START and the last CHUNK_END. The last block is not compressed here: 183 # it is the chunk's output node (2.5, 2.6 decide its flags and use). 184 # n blocks follow the current block (in pair); the last block has len bytes. 185 def chunk_blocks(n: Nat, +t: U32, +index: U32, +flags: U32, +len: Nat, cv: T.CV, pair: Array & T.Block) -> Array & T.Out: 186 match n pair: 187 case 0n Tuple{a,b}: (a,T.Out{cv,zero_tail(b,len),t,U32.from_nat(len),U32.or(flags,chunk_end())}) 188 case 1n+p Tuple{a,b}: chunk_blocks(p,t,U32.add(index,16),0,len,compress(cv,zero_tail(b,64n),t,64,flags),read_block(a,U32.add(index,16))) 189 190 # A chunk of len bytes (1..1024; 0 only for the empty message) at word index 191 # has max(1, ceil(len/64)) blocks: n = (len - 1) div 64 full blocks, then a 192 # last block of len - 64n bytes. 193 def chunk(a: Array, +t: U32, +index: U32, +len: Nat) -> Array & T.Out: 194 +n = Nat.div(Nat.sub(len,1n),64n) 195 chunk_blocks(n,t,index,chunk_start(),Nat.sub(len,Nat.mul(n,64n)),cv_of(iv()),read_block(a,index)) 196 197 # Every chunk but the last holds 1024 bytes; chunk t starts at word 256t. 198 def chunk_at(more: Nat, +t: U32, +index: U32, +len: Nat, a: Array) -> Array & T.Out: 199 match more: 200 case 0n: chunk(a,t,index,len) 201 case 1n+q: chunk(a,t,index,1024n) 202 203 # The outputs of the chunks, in order; `pair` holds the current chunk, n 204 # chunks follow it, the last one of len bytes. 205 def chunks(+n: Nat, +t: U32, +index: U32, +len: Nat, pair: Array & T.Out) -> List<&2,T.Out>: 206 match n pair: 207 case 0n Tuple{a,o}: Con{o,Nil{}} 208 case 1n+p Tuple{a,o}: Con{o,chunks(p,U32.inc(t),U32.add(index,256),len,chunk_at(p,U32.inc(t),U32.add(index,256),len,a))} 209 210 # A message of `length` bytes has max(1, ceil(length/1024)) chunks: n = 211 # (length - 1) div 1024 full ones, then the last of length - 1024n bytes. 212 def message_chunks(a: Array, +length: Nat) -> List<&2,T.Out>: 213 +n = Nat.div(Nat.sub(length,1n),1024n) 214 +last = Nat.sub(length,Nat.mul(n,1024n)) 215 chunks(n,0,0,last,chunk_at(n,0,0,last,a)) 216 217 # ---- the tree (2.5) ---- 218 219 # A node's chaining value: its compression with its own flags. 220 def cv(o: T.Out) -> T.CV: 221 match o: 222 case T.Out{c,b,t,len,flags}: compress(c,b,t,len,flags) 223 224 # A parent node: key IV, block = left child CV ++ right child CV, counter 0, 225 # length 64, flag PARENT. 226 def parent(l: T.CV, r: T.CV) -> T.Out: 227 T.Out{cv_of(iv()),block_of(SC.append(U32,cv_words(l),cv_words(r))),0,64,parent_flag()} 228 229 def is_nil(xs: List<&2,T.Out>) -> Bool: 230 match xs: 231 case Nil{}: True{} 232 case Con{x,r}: False{} 233 234 def first(xs: List<&2,T.Out>) -> T.Out: 235 match xs: 236 case Nil{}: T.Out{cv_of(iv()),block_of(Nil{}),0,0,0} 237 case Con{x,r}: x 238 239 def join(l: T.Out, r: T.Out, alone: Bool) -> T.Out: 240 match alone: 241 case True{}: l 242 case False{}: parent(cv(l),cv(r)) 243 244 # The tree over the chunk outputs xs, 1 <= |xs| <= 2^h. The chunks are its 245 # leaves in order; a left subtree is always complete with a power of two of 246 # chunks, the largest one that leaves at least one chunk to its right: with 247 # h = g+1 and |xs| > 2^g the left subtree takes the first 2^g chunks and the 248 # right one the rest, while |xs| <= 2^g (nothing left for the right) means the 249 # tree already fits in height g. 250 def tree(+h: Nat, +xs: List<&2,T.Out>) -> T.Out: 251 match h xs: 252 case 0n Nil{}: first(Nil{}) 253 case 0n Con{+x,+r}: first(Con{x,r}) 254 case 1n+g Nil{}: first(Nil{}) 255 case 1n+g Con{+x,+r}: 256 +k = SC.pow2(g) 257 join(tree(g,SC.take(T.Out,Con{x,r},k)),tree(g,SC.drop(T.Out,Con{x,r},k)),is_nil(SC.drop(T.Out,Con{x,r},k))) 258 259 # ---- the root and the digest (2.6) ---- 260 261 # The root node is compressed with ROOT added to its flags; the 32-byte digest 262 # is the resulting chaining value, words in little-endian order. A single 263 # chunk is itself the root. 264 def root(o: T.Out) -> T.CV: 265 match o: 266 case T.Out{c,b,t,len,flags}: compress(c,b,t,len,U32.or(flags,root_flag())) 267 268 def hash(a: Array, +length: Nat) -> T.CV: 269 +cs = message_chunks(a,length) 270 root(tree(SC.length(T.Out,cs),cs)) 271 272 def digest(c: T.CV) -> Array: 273 match c: 274 case T.CV{h0,h1,h2,h3,h4,h5,h6,h7}: 275 ANode{ANode{ANode{ALeaf{h0},ALeaf{h1}},ANode{ALeaf{h2},ALeaf{h3}}},ANode{ANode{ALeaf{h4},ALeaf{h5}},ANode{ALeaf{h6},ALeaf{h7}}}} 276 277 def checked(valid: Bool, a: Array, +length: Nat) -> Maybe<&1,Array>: 278 match valid: 279 case False{}: None{} 280 case True{}: Some{digest(hash(a,length))} 281 282 # None when byte_length exceeds the 4 * capacity bytes the array can hold. 283 def sized(+length: Nat, pair: Array & U32) -> Maybe<&1,Array>: 284 (a,capacity) = pair 285 checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length) 286 287 def blake3(words: Array, byte_length: Nat) -> Maybe<&1,Array>: 288 sized(byte_length,Array.size(U32,words))