1 import Base 2 import ../../../src/crypto/blake/blake2s/types.bend as T 3 4 # Executable specification of unkeyed BLAKE2s-256, written from RFC 7693. 5 # Only the neutral chaining-value record T.State is shared with the 6 # implementation; no implementation function is called. The work vector, 7 # the message block and SIGMA are lists indexed as in the RFC, and the message 8 # is handled byte by byte: the packed input is read as little-endian bytes, 9 # the final block is zero-padded byte-wise, and block words are reassembled 10 # from bytes (RFC 7693 section 2.4, "little-endian byte order"). 11 12 # ---------------------------------------------------------------- 2.6 constants 13 14 # IV[0..7] = 0x6A09E667 0xBB67AE85 0x3C6EF372 0xA54FF53A 15 # 0x510E527F 0x9B05688C 0x1F83D9AB 0x5BE0CD19 16 def iv() -> List<&2,U32>: 17 [1779033703, 3144134277, 1013904242, 2773480762, 1359893119, 2600822924, 528734635, 1541459225] 18 19 # SIGMA[i mod 10]. 20 def sigma(r: Nat) -> List<&2,Nat>: 21 match r: 22 case 0n: [0n, 1n, 2n, 3n, 4n, 5n, 6n, 7n, 8n, 9n, 10n, 11n, 12n, 13n, 14n, 15n] 23 case 1n: [14n, 10n, 4n, 8n, 9n, 15n, 13n, 6n, 1n, 12n, 0n, 2n, 11n, 7n, 5n, 3n] 24 case 2n: [11n, 8n, 12n, 0n, 5n, 2n, 15n, 13n, 10n, 14n, 3n, 6n, 7n, 1n, 9n, 4n] 25 case 3n: [7n, 9n, 3n, 1n, 13n, 12n, 11n, 14n, 2n, 6n, 5n, 10n, 4n, 0n, 15n, 8n] 26 case 4n: [9n, 0n, 5n, 7n, 2n, 4n, 10n, 15n, 14n, 1n, 11n, 12n, 6n, 8n, 3n, 13n] 27 case 5n: [2n, 12n, 6n, 10n, 0n, 11n, 8n, 3n, 4n, 13n, 7n, 5n, 15n, 14n, 1n, 9n] 28 case 6n: [12n, 5n, 1n, 15n, 14n, 13n, 4n, 10n, 0n, 7n, 6n, 3n, 9n, 2n, 8n, 11n] 29 case 7n: [13n, 11n, 7n, 14n, 12n, 1n, 3n, 9n, 5n, 0n, 15n, 4n, 8n, 6n, 2n, 10n] 30 case 8n: [6n, 15n, 14n, 9n, 11n, 3n, 0n, 8n, 12n, 2n, 13n, 7n, 1n, 4n, 10n, 5n] 31 case 9n: [10n, 2n, 8n, 4n, 7n, 6n, 1n, 5n, 15n, 11n, 9n, 14n, 3n, 12n, 13n, 0n] 32 case 10n+p: sigma(p) 33 34 # ---------------------------------------------------------------- list indexing 35 36 def get(xs: List<&2,U32>, i: Nat) -> U32: 37 match xs i: 38 case Nil{} _: 0 39 case x <> rest 0n: x 40 case x <> rest 1n+p: get(rest, p) 41 42 def index(xs: List<&2,Nat>, i: Nat) -> Nat: 43 match xs i: 44 case Nil{} _: 0n 45 case x <> rest 0n: x 46 case x <> rest 1n+p: index(rest, p) 47 48 def put(xs: List<&2,U32>, i: Nat, y: U32) -> List<&2,U32>: 49 match xs i: 50 case Nil{} _: Nil{} 51 case x <> rest 0n: y <> rest 52 case x <> rest 1n+p: x <> put(rest, p, y) 53 54 # ---------------------------------------------------------------- 3.1 G 55 56 # x >>> n: rotation of a 32-bit word right by n bits (0 < n < 32). 57 def rotr(+x: U32, +n: Nat) -> U32: 58 U32.or(U32.shrn(x, n), U32.shln(x, Nat.sub(32n, n))) 59 60 # G(v[0..15], a, b, c, d, x, y) with BLAKE2s rotations R1..R4 = 16, 12, 8, 7. 61 def mix(+v: List<&2,U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, x: U32, y: U32) -> List<&2,U32>: 62 +va = U32.add(U32.add(get(v, a), get(v, b)), x) 63 +vd = rotr(U32.xor(get(v, d), va), 16n) 64 +vc = U32.add(get(v, c), vd) 65 +vb = rotr(U32.xor(get(v, b), vc), 12n) 66 +va2 = U32.add(U32.add(va, vb), y) 67 +vd2 = rotr(U32.xor(vd, va2), 8n) 68 +vc2 = U32.add(vc, vd2) 69 +vb2 = rotr(U32.xor(vb, vc2), 7n) 70 put(put(put(put(v, a, va2), b, vb2), c, vc2), d, vd2) 71 72 # ---------------------------------------------------------------- 3.2 F 73 74 # One round with schedule s: four column steps, then four diagonal steps. 75 def round(v: List<&2,U32>, +s: List<&2,Nat>, +m: List<&2,U32>) -> List<&2,U32>: 76 v1 = mix(v, 0n, 4n, 8n, 12n, get(m, index(s, 0n)), get(m, index(s, 1n))) 77 v2 = mix(v1, 1n, 5n, 9n, 13n, get(m, index(s, 2n)), get(m, index(s, 3n))) 78 v3 = mix(v2, 2n, 6n, 10n, 14n, get(m, index(s, 4n)), get(m, index(s, 5n))) 79 v4 = mix(v3, 3n, 7n, 11n, 15n, get(m, index(s, 6n)), get(m, index(s, 7n))) 80 v5 = mix(v4, 0n, 5n, 10n, 15n, get(m, index(s, 8n)), get(m, index(s, 9n))) 81 v6 = mix(v5, 1n, 6n, 11n, 12n, get(m, index(s, 10n)), get(m, index(s, 11n))) 82 v7 = mix(v6, 2n, 7n, 8n, 13n, get(m, index(s, 12n)), get(m, index(s, 13n))) 83 mix(v7, 3n, 4n, 9n, 14n, get(m, index(s, 14n)), get(m, index(s, 15n))) 84 85 # Rounds i, i+1, ..., i+n-1. 86 def rounds(n: Nat, +i: Nat, v: List<&2,U32>, +m: List<&2,U32>) -> List<&2,U32>: 87 match n: 88 case 0n: v 89 case 1n+p: rounds(p, 1n+i, round(v, sigma(i), m), m) 90 91 def invert(last: Bool, +v: List<&2,U32>) -> List<&2,U32>: 92 match last: 93 case True{}: put(v, 14n, U32.xor(get(v, 14n), 4294967295)) 94 case False{}: v 95 96 # F(h, m, t, f) with r rounds (r = 10 for BLAKE2s): t = t0 + 2^32 * t1 is the 97 # byte counter, f the final-block flag. 98 def compress(+r: Nat, h: T.State, +m: List<&2,U32>, +t0: U32, +t1: U32, last: Bool) -> T.State: 99 match h: 100 case T.H{+h0, +h1, +h2, +h3, +h4, +h5, +h6, +h7}: 101 +v0 = List.append(&2, U32, [h0, h1, h2, h3, h4, h5, h6, h7], iv()) 102 +v1 = put(v0, 12n, U32.xor(get(v0, 12n), t0)) 103 +v2 = put(v1, 13n, U32.xor(get(v1, 13n), t1)) 104 +v = rounds(r, 0n, invert(last, v2), m) 105 T.H{U32.xor(U32.xor(h0, get(v, 0n)), get(v, 8n)), 106 U32.xor(U32.xor(h1, get(v, 1n)), get(v, 9n)), 107 U32.xor(U32.xor(h2, get(v, 2n)), get(v, 10n)), 108 U32.xor(U32.xor(h3, get(v, 3n)), get(v, 11n)), 109 U32.xor(U32.xor(h4, get(v, 4n)), get(v, 12n)), 110 U32.xor(U32.xor(h5, get(v, 5n)), get(v, 13n)), 111 U32.xor(U32.xor(h6, get(v, 6n)), get(v, 14n)), 112 U32.xor(U32.xor(h7, get(v, 7n)), get(v, 15n))} 113 114 # ---------------------------------------------------------------- 2.4 bytes 115 116 # Byte k (0 = least significant) of a word: the packed input holds four 117 # message bytes per word in little-endian order. 118 def byte(+w: U32, k: Nat) -> U32: 119 U32.and(255, U32.shrn(w, Nat.mul(8n, k))) 120 121 def octets(+w: U32) -> List<&2,U32>: 122 [byte(w, 0n), byte(w, 1n), byte(w, 2n), byte(w, 3n)] 123 124 def serialize(ws: List<&2,U32>) -> List<&2,U32>: 125 match ws: 126 case Nil{}: Nil{} 127 case w <> rest: List.append(&2, U32, octets(w), serialize(rest)) 128 129 # Zero padding: the byte at message offset i survives only when i < length. 130 def keep_if(inside: Bool, b: U32) -> U32: 131 match inside: 132 case True{}: b 133 case False{}: 0 134 135 def pad(bytes: List<&2,U32>, +i: Nat, +length: Nat) -> List<&2,U32>: 136 match bytes: 137 case Nil{}: Nil{} 138 case b <> rest: keep_if(Nat.is_lt(i, length), b) <> pad(rest, 1n+i, length) 139 140 # A block word from four bytes, least significant first. 141 def word(b0: U32, b1: U32, b2: U32, b3: U32) -> U32: 142 U32.or(U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.shln(b2, 16n)), U32.shln(b3, 24n)) 143 144 def words(bytes: List<&2,U32>) -> List<&2,U32>: 145 match bytes: 146 case b0 <> b1 <> b2 <> b3 <> rest: word(b0, b1, b2, b3) <> words(rest) 147 case _: Nil{} 148 149 # ---------------------------------------------------------------- 3.3 BLAKE2s 150 151 # The byte counter t as two 32-bit halves: t + n, with the carry into t1. 152 def carry(c: Bool, hi: U32) -> U32: 153 match c: 154 case True{}: U32.add(hi, 1) 155 case False{}: hi 156 157 def count_hi(+lo: U32, hi: U32, +n: U32) -> U32: 158 carry(U32.is_lt(U32.add(lo, n), n), hi) 159 160 # Read the sixteen words of the block at word offset base, in order. 161 def gather(n: Nat, +base: U32, +next: U32, acc: List<&2,U32>, pair: Array & U32) -> Array & List<&2,U32>: 162 match n pair: 163 case 0n Tuple{a, w}: (a, List.reverse(&2, U32, w <> acc)) 164 case 1n+p Tuple{a, w}: gather(p, base, U32.inc(next), w <> acc, Array.get(U32, a, U32.add(base, next))) 165 166 def read_block(a: Array, +base: U32) -> Array & List<&2,U32>: 167 gather(15n, base, 1, [], Array.get(U32, a, base)) 168 169 # A block before the last: all 64 bytes are message bytes. 170 def full_block(+r: Nat, pair: Array & List<&2,U32>, h: T.State, +t0: U32, +t1: U32) -> Array & T.State: 171 (a, ws) = pair 172 (a, compress(r, h, words(serialize(ws)), t0, t1, False{})) 173 174 # The last block: the remaining bytes, zero-padded to 64. 175 def last_block(+r: Nat, pair: Array & List<&2,U32>, +remain: Nat, h: T.State, +t0: U32, +t1: U32) -> T.State: 176 (a, ws) = pair 177 compress(r, h, words(pad(serialize(ws), 0n, remain)), t0, t1, True{}) 178 179 def absorb(+r: Nat, a: Array, +base: U32, h: T.State, +t0: U32, +t1: U32) -> Array & T.State: 180 full_block(r, read_block(a, base), h, t0, t1) 181 182 def finish(+r: Nat, a: Array, +base: U32, +t0: U32, t1: U32, +remain: Nat, h: T.State) -> T.State: 183 +n = U32.from_nat(remain) 184 last_block(r, read_block(a, base), remain, h, U32.add(t0, n), count_hi(t0, t1, n)) 185 186 # n full blocks, then the last one; t counts the bytes compressed so far. 187 def blocks(+r: Nat, n: Nat, +base: U32, +t0: U32, t1: U32, +remain: Nat, pair: Array & T.State) -> T.State: 188 match n pair: 189 case 0n Tuple{a, h}: finish(r, a, base, t0, t1, remain, h) 190 case 1n+p Tuple{a, h}: 191 +c0 = U32.add(t0, 64) 192 +c1 = count_hi(t0, t1, 64) 193 blocks(r, p, U32.add(base, 16), c0, c1, remain, absorb(r, a, base, h, c0, c1)) 194 195 # h[0..7] := IV[0..7]; h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0, nn = 32. 196 def initial() -> T.State: 197 T.H{U32.xor(1779033703, U32.xor(16842752, 32)), 3144134277, 1013904242, 2773480762, 1359893119, 2600822924, 528734635, 1541459225} 198 199 # dd = ceil(ll / 64) blocks, and dd = 1 for the empty message. 200 def block_count(+ll: Nat) -> Nat: 201 match ll: 202 case 0n: 1n 203 case 1n+p: Nat.div(Nat.add(ll, 63n), 64n) 204 205 def hash(+r: Nat, a: Array, +ll: Nat) -> T.State: 206 +n = Nat.sub(block_count(ll), 1n) 207 blocks(r, n, 0, 0, 0, Nat.sub(ll, Nat.mul(64n, n)), (a, initial())) 208 209 # The 32-byte digest as eight little-endian words, in a fresh 8-slot array. 210 def digest(h: T.State) -> Array: 211 match h: 212 case T.H{h0, h1, h2, h3, h4, h5, h6, h7}: 213 ANode{ANode{ANode{ALeaf{h0}, ALeaf{h1}}, ANode{ALeaf{h2}, ALeaf{h3}}}, ANode{ANode{ALeaf{h4}, ALeaf{h5}}, ANode{ALeaf{h6}, ALeaf{h7}}}} 214 215 def checked(+r: Nat, valid: Bool, a: Array, ll: Nat) -> Maybe<&1,Array>: 216 match valid: 217 case False{}: None{} 218 case True{}: Some{digest(hash(r, a, ll))} 219 220 def sized(+r: Nat, +ll: Nat, pair: Array & U32) -> Maybe<&1,Array>: 221 (a, capacity) = pair 222 checked(r, Nat.is_le(ll, Nat.mul(4n, U32.to_nat(capacity))), a, ll) 223 224 # The hash with r rounds per compression, of the first ll bytes of the packed 225 # array a; None when ll exceeds the 4 * capacity bytes the array holds. 226 def blake2s_rounds(+r: Nat, a: Array, ll: Nat) -> Maybe<&1,Array>: 227 sized(r, ll, Array.size(U32, a)) 228 229 # BLAKE2s-256: r = 10. 230 def blake2s(a: Array, ll: Nat) -> Maybe<&1,Array>: 231 blake2s_rounds(10n, a, ll)