1 import Base 2 import ../../../src/crypto/blake/blake2b/types.bend as T 3 4 # BLAKE2b-512 (RFC 7693), unkeyed, as an executable specification. 5 # 6 # Written from the RFC; it never calls the implementation. It shares only the 7 # record types of src/crypto/blake/blake2b/types.bend: a 64-bit word is a pair 8 # of U32 halves T.W{lo, hi} (low half first), the working vector v[0..15] is 9 # T.V{..}, the chaining value h[0..7] is T.H{..} and the 128-bit byte counter t 10 # is four little-endian U32 limbs T.C{..}. The state is indexed with at/put and 11 # the message schedule is read from the SIGMA table, as in the RFC's pseudocode. 12 # 13 # Input convention (shared with the public API): the message bytes are packed 14 # little-endian, four per U32 word, in an Array; byte_length is the number 15 # of message bytes. Bytes of the last block past byte_length are zero. 16 17 # ---------------------------------------------------------------- 64-bit words 18 19 # (a + b) mod 2^64: the low halves add modulo 2^32; the high halves add the 20 # carry out of the low half, which is 1 exactly when the low sum wrapped. 21 def add(a: T.Lane, b: T.Lane) -> T.Lane: 22 match a b: 23 case T.W{+al,ah} T.W{bl,bh}: 24 +lo = U32.add(al,bl) 25 T.W{lo,U32.add(U32.add(ah,bh),Bool.to_u32(U32.is_lt(lo,al)))} 26 27 def xor(a: T.Lane, b: T.Lane) -> T.Lane: 28 match a b: 29 case T.W{al,ah} T.W{bl,bh}: T.W{U32.xor(al,bl),U32.xor(ah,bh)} 30 31 # x >>> n for 0 < n < 32: each half takes its own bits shifted right and the 32 # other half's low bits shifted in from the top. 33 def rotr_small(+lo: U32, +hi: U32, +n: Nat) -> T.Lane: 34 T.W{U32.or(U32.shrn(lo,n),U32.shln(hi,Nat.sub(32n,n))),U32.or(U32.shrn(hi,n),U32.shln(lo,Nat.sub(32n,n)))} 35 36 # n > 32 rotates the swapped halves by n - 32. 37 def rotr_split(lo: U32, hi: U32, +n: Nat, small: Bool) -> T.Lane: 38 match small: 39 case True{}: rotr_small(lo,hi,n) 40 case False{}: rotr_small(hi,lo,Nat.sub(n,32n)) 41 42 # Right rotation of a 64-bit word by n (0 <= n < 64). 43 def rotr(a: T.Lane, +n: Nat) -> T.Lane: 44 match a n: 45 case T.W{lo,hi} 0n: T.W{lo,hi} 46 case T.W{lo,hi} 32n: T.W{hi,lo} 47 case T.W{lo,hi} n: rotr_split(lo,hi,n,Nat.is_lt(n,32n)) 48 49 # ---------------------------------------------------------------- constants 50 51 # RFC 7693 section 2.6: IV[i], the SHA-512 initial hash values. 52 def iv(i: Nat) -> T.Lane: 53 match i: 54 case 0n: T.W{4089235720,1779033703} 55 case 1n: T.W{2227873595,3144134277} 56 case 2n: T.W{4271175723,1013904242} 57 case 3n: T.W{1595750129,2773480762} 58 case 4n: T.W{2917565137,1359893119} 59 case 5n: T.W{725511199,2600822924} 60 case 6n: T.W{4215389547,528734635} 61 case 7n: T.W{327033209,1541459225} 62 case _: T.W{0,0} 63 64 # RFC 7693 section 2.7: the message word schedule SIGMA[r]. 65 def sigma(r: Nat) -> List<&2,Nat>: 66 match r: 67 case 0n: [0n,1n,2n,3n,4n,5n,6n,7n,8n,9n,10n,11n,12n,13n,14n,15n] 68 case 1n: [14n,10n,4n,8n,9n,15n,13n,6n,1n,12n,0n,2n,11n,7n,5n,3n] 69 case 2n: [11n,8n,12n,0n,5n,2n,15n,13n,10n,14n,3n,6n,7n,1n,9n,4n] 70 case 3n: [7n,9n,3n,1n,13n,12n,11n,14n,2n,6n,5n,10n,4n,0n,15n,8n] 71 case 4n: [9n,0n,5n,7n,2n,4n,10n,15n,14n,1n,11n,12n,6n,8n,3n,13n] 72 case 5n: [2n,12n,6n,10n,0n,11n,8n,3n,4n,13n,7n,5n,15n,14n,1n,9n] 73 case 6n: [12n,5n,1n,15n,14n,13n,4n,10n,0n,7n,6n,3n,9n,2n,8n,11n] 74 case 7n: [13n,11n,7n,14n,12n,1n,3n,9n,5n,0n,15n,4n,8n,6n,2n,10n] 75 case 8n: [6n,15n,14n,9n,11n,3n,0n,8n,12n,2n,13n,7n,1n,4n,10n,5n] 76 case 9n: [10n,2n,8n,4n,7n,6n,1n,5n,15n,11n,9n,14n,3n,12n,13n,0n] 77 case _: [] 78 79 def nth(-A: Data, xs: List<&2,A>, n: Nat, +zero: A) -> A: 80 match xs n: 81 case Nil{} _: zero 82 case x <> rest 0n: x 83 case x <> rest 1n+p: nth(A,rest,p,zero) 84 85 # ---------------------------------------------------------------- the working vector 86 87 def at(s: T.State, i: Nat) -> T.Lane: 88 match s i: 89 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 0n: v0 90 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 1n: v1 91 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 2n: v2 92 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 3n: v3 93 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 4n: v4 94 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 5n: v5 95 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 6n: v6 96 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 7n: v7 97 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 8n: v8 98 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 9n: v9 99 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 10n: v10 100 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 11n: v11 101 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 12n: v12 102 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 13n: v13 103 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 14n: v14 104 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 15n: v15 105 case _ _: T.W{0,0} 106 107 def put(s: T.State, i: Nat, x: T.Lane) -> T.State: 108 match s i: 109 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 0n: T.V{x,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 110 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 1n: T.V{v0,x,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 111 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 2n: T.V{v0,v1,x,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 112 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 3n: T.V{v0,v1,v2,x,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 113 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 4n: T.V{v0,v1,v2,v3,x,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 114 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 5n: T.V{v0,v1,v2,v3,v4,x,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 115 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 6n: T.V{v0,v1,v2,v3,v4,v5,x,v7,v8,v9,v10,v11,v12,v13,v14,v15} 116 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 7n: T.V{v0,v1,v2,v3,v4,v5,v6,x,v8,v9,v10,v11,v12,v13,v14,v15} 117 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 8n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,x,v9,v10,v11,v12,v13,v14,v15} 118 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 9n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,x,v10,v11,v12,v13,v14,v15} 119 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 10n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,x,v11,v12,v13,v14,v15} 120 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 11n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,x,v12,v13,v14,v15} 121 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 12n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,x,v13,v14,v15} 122 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 13n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,x,v14,v15} 123 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 14n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,x,v15} 124 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15} 15n: T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,x} 125 case s _: s 126 127 # ---------------------------------------------------------------- G, the round, F 128 129 # RFC 7693 section 3.1, the mixing function G with R1..R4 = 32, 24, 16, 63: 130 # v[a] := (v[a] + v[b] + x) mod 2^64; v[d] := (v[d] ^ v[a]) >>> R1 131 # v[c] := (v[c] + v[d]) mod 2^64; v[b] := (v[b] ^ v[c]) >>> R2 132 # v[a] := (v[a] + v[b] + y) mod 2^64; v[d] := (v[d] ^ v[a]) >>> R3 133 # v[c] := (v[c] + v[d]) mod 2^64; v[b] := (v[b] ^ v[c]) >>> R4 134 def mix(+s: T.State, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: T.Lane, y: T.Lane) -> T.State: 135 +a1 = add(add(at(s,a),at(s,b)),x) 136 +d1 = rotr(xor(at(s,d),a1),32n) 137 +c1 = add(at(s,c),d1) 138 +b1 = rotr(xor(at(s,b),c1),24n) 139 +a2 = add(add(a1,b1),y) 140 +d2 = rotr(xor(d1,a2),16n) 141 +c2 = add(c1,d2) 142 +b2 = rotr(xor(b1,c2),63n) 143 put(put(put(put(s,a,a2),b,b2),c,c2),d,d2) 144 145 # G reads the vector's sixteen words and mixes the four at a, b, c, d. 146 def G(v: T.State, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: T.Lane, y: T.Lane) -> T.State: 147 match v: 148 case T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}: 149 mix(T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15},a,b,c,d,x,y) 150 151 # m[s[j]]: the j-th message word of the round's schedule s. 152 def word(+m: List<&2,T.Lane>, +s: List<&2,Nat>, +j: Nat) -> T.Lane: 153 nth(T.Lane,m,nth(Nat,s,j,0n),T.W{0,0}) 154 155 # RFC 7693 section 3.2, one round of F with schedule s = SIGMA[i mod 10]. 156 def round(v: T.State, +m: List<&2,T.Lane>, +s: List<&2,Nat>) -> T.State: 157 v = G(v,0n,4n,8n,12n,word(m,s,0n),word(m,s,1n)) 158 v = G(v,1n,5n,9n,13n,word(m,s,2n),word(m,s,3n)) 159 v = G(v,2n,6n,10n,14n,word(m,s,4n),word(m,s,5n)) 160 v = G(v,3n,7n,11n,15n,word(m,s,6n),word(m,s,7n)) 161 v = G(v,0n,5n,10n,15n,word(m,s,8n),word(m,s,9n)) 162 v = G(v,1n,6n,11n,12n,word(m,s,10n),word(m,s,11n)) 163 v = G(v,2n,7n,8n,13n,word(m,s,12n),word(m,s,13n)) 164 G(v,3n,4n,9n,14n,word(m,s,14n),word(m,s,15n)) 165 166 # Rounds i, i+1, .., i+n-1. 167 def rounds(n: Nat, +i: Nat, v: T.State, +m: List<&2,T.Lane>) -> T.State: 168 match n: 169 case 0n: v 170 case 1n+p: rounds(p,1n+i,round(v,m,sigma(Nat.mod(i,10n))),m) 171 172 def invert_if(last: Bool, x: T.Lane) -> T.Lane: 173 match last: 174 case True{}: xor(x,T.W{4294967295,4294967295}) 175 case False{}: x 176 177 # v[0..7] := h[0..7]; v[8..15] := IV[0..7]; v[12] ^= t mod 2^64; 178 # v[13] ^= t >> 64; if last block, v[14] := ~v[14]. 179 def start(h: T.Chain, t: T.Counter, last: Bool) -> T.State: 180 match h t: 181 case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.C{t0,t1,t2,t3}: 182 T.V{h0,h1,h2,h3,h4,h5,h6,h7,iv(0n),iv(1n),iv(2n),iv(3n),xor(iv(4n),T.W{t0,t1}),xor(iv(5n),T.W{t2,t3}),invert_if(last,iv(6n)),iv(7n)} 183 184 # h[i] := h[i] ^ v[i] ^ v[i + 8]. 185 def finish(h: T.Chain, v: T.State) -> T.Chain: 186 match h v: 187 case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}: 188 T.H{xor(xor(h0,v0),v8),xor(xor(h1,v1),v9),xor(xor(h2,v2),v10),xor(xor(h3,v3),v11),xor(xor(h4,v4),v12),xor(xor(h5,v5),v13),xor(xor(h6,v6),v14),xor(xor(h7,v7),v15)} 189 190 # RFC 7693 section 3.2: F(h, m, t, f) with twelve rounds. 191 def compress(+h: T.Chain, +m: List<&2,T.Lane>, t: T.Counter, last: Bool) -> T.Chain: 192 finish(h,rounds(12n,0n,start(h,t,last),m)) 193 194 # ---------------------------------------------------------------- message blocks 195 196 # t := t + x on the 128-bit counter, carrying from limb to limb. 197 def advance(c: T.Counter, +x: U32) -> T.Counter: 198 match c: 199 case T.C{c0,c1,c2,c3}: 200 +s0 = U32.add(c0,x) 201 +k0 = Bool.to_u32(U32.is_lt(s0,x)) 202 +s1 = U32.add(c1,k0) 203 +k1 = Bool.to_u32(U32.is_lt(s1,k0)) 204 +s2 = U32.add(c2,k1) 205 T.C{s0,s1,s2,U32.add(c3,Bool.to_u32(U32.is_lt(s2,k1)))} 206 207 # The low n bytes of a little-endian word (all four when n >= 4). 208 def keep(w: U32, n: Nat) -> U32: 209 match n: 210 case 0n: 0 211 case 1n: U32.and(w,255) 212 case 2n: U32.and(w,65535) 213 case 3n: U32.and(w,16777215) 214 case _: w 215 216 # The word holding block bytes pos..pos+3 when only `remain` bytes are message: 217 # the bytes at or past `remain` are zero padding. 218 def mask(w: U32, +pos: Nat, +remain: Nat) -> U32: 219 keep(w,Nat.sub(remain,pos)) 220 221 def trim(ws: List<&2,U32>, +pos: Nat, +remain: Nat) -> List<&2,U32>: 222 match ws: 223 case Nil{}: Nil{} 224 case w <> rest: mask(w,pos,remain) <> trim(rest,Nat.add(pos,4n),remain) 225 226 def prepare(last: Bool, ws: List<&2,U32>, remain: Nat) -> List<&2,U32>: 227 match last: 228 case False{}: ws 229 case True{}: trim(ws,0n,remain) 230 231 # m[i] = the little-endian 64-bit word of block bytes 8i..8i+7. 232 def lanes(ws: List<&2,U32>) -> List<&2,T.Lane>: 233 match ws: 234 case lo <> hi <> rest: T.W{lo,hi} <> lanes(rest) 235 case _: Nil{} 236 237 # Reads the block's 32 words base+0 .. base+31 from the array, then compresses. 238 def gather(n: Nat, +base: U32, +next: U32, +last: Bool, +remain: Nat, t: T.Counter, h: T.Chain, acc: List<&2,U32>, pair: Array & U32) -> Array & T.Chain: 239 match n pair: 240 case 0n Tuple{a,w}: 241 (a,compress(h,lanes(prepare(last,List.reverse(&2,U32,w <> acc),remain)),t,last)) 242 case 1n+p Tuple{a,w}: 243 gather(p,base,U32.inc(next),last,remain,t,h,w <> acc,Array.get(U32,a,U32.add(base,next))) 244 245 # A block that is not the last: t already counts its 128 bytes. 246 def absorb(a: Array, +index: U32, t: T.Counter, h: T.Chain) -> Array & T.Chain: 247 gather(31n,index,1,False{},0n,t,h,Nil{},Array.get(U32,a,index)) 248 249 # The last block: remain message bytes (1..128; 0 for the empty message), t := t + remain. 250 def final(a: Array, +index: U32, +remain: Nat, t: T.Counter, h: T.Chain) -> T.Chain: 251 Pair.snd(Array,T.Chain,gather(31n,index,1,True{},remain,advance(t,U32.from_nat(remain)),h,Nil{},Array.get(U32,a,index))) 252 253 # n blocks that are not the last, then the last one. 254 def blocks(n: Nat, +index: U32, +remain: Nat, t: T.Counter, pair: Array & T.Chain) -> T.Chain: 255 match n pair: 256 case 0n Tuple{a,h}: final(a,index,remain,t,h) 257 case 1n+p Tuple{a,h}: 258 +t2 = advance(t,128) 259 blocks(p,U32.add(index,32),remain,t2,absorb(a,index,t2,h)) 260 261 # h[0..7] := IV[0..7]; h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0, nn = 64. 262 def initial() -> T.Chain: 263 T.H{xor(iv(0n),T.W{16842816,0}),iv(1n),iv(2n),iv(3n),iv(4n),iv(5n),iv(6n),iv(7n)} 264 265 # dd = max(1, ceil(ll / 128)) blocks: dd - 1 = (ll - 1) div 128 full blocks 266 # (0 when ll = 0), then the last block with the remaining ll - 128 (dd - 1) bytes. 267 def unchecked(a: Array, +length: Nat) -> T.Chain: 268 +n = Nat.div(Nat.sub(length,1n),128n) 269 blocks(n,0,Nat.sub(length,Nat.mul(n,128n)),T.C{0,0,0,0},(a,initial())) 270 271 # The 64-byte digest h[0..7] as sixteen little-endian words. 272 def digest(h: T.Chain) -> Array: 273 match h: 274 case T.H{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7}}: 275 ANode{ANode{ANode{ANode{ALeaf{l0},ALeaf{u0}},ANode{ALeaf{l1},ALeaf{u1}}},ANode{ANode{ALeaf{l2},ALeaf{u2}},ANode{ALeaf{l3},ALeaf{u3}}}},ANode{ANode{ANode{ALeaf{l4},ALeaf{u4}},ANode{ALeaf{l5},ALeaf{u5}}},ANode{ANode{ALeaf{l6},ALeaf{u6}},ANode{ALeaf{l7},ALeaf{u7}}}}} 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(unchecked(a,length))} 281 282 def sized(+length: Nat, pair: Array & U32) -> Maybe<&1,Array>: 283 (a,capacity) = pair 284 checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length) 285 286 # BLAKE2b-512 of the first byte_length bytes of the packed words; None when 287 # byte_length exceeds the array's 4 * capacity bytes. 288 def blake2b(words: Array, byte_length: Nat) -> Maybe<&1,Array>: 289 sized(byte_length,Array.size(U32,words))