1 # Generated by tools/generators/blake2s_gen.py; do not edit. 2 import Base 3 import ./types.bend as T 4 import ./compress.bend as C 5 6 # The 64-bit byte counter t is kept as two U32 halves (t0 low, t1 high). 7 def carry(c: Bool, hi: U32) -> U32: 8 match c: 9 case True{}: U32.add(hi,1) 10 case False{}: hi 11 12 def count_hi(+lo: U32, hi: U32, +n: U32) -> U32: 13 carry(U32.is_lt(U32.add(lo,n),n),hi) 14 15 def read15(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32,w14: U32, pair: Array & U32) -> Array & T.State: 16 (a,w15) = pair 17 (a,C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{})) 18 19 def read14(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32, pair: Array & U32) -> Array & T.State: 20 (a,w14) = pair 21 read15(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15))) 22 23 def read13(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32, pair: Array & U32) -> Array & T.State: 24 (a,w13) = pair 25 read14(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14))) 26 27 def read12(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32, pair: Array & U32) -> Array & T.State: 28 (a,w12) = pair 29 read13(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13))) 30 31 def read11(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32, pair: Array & U32) -> Array & T.State: 32 (a,w11) = pair 33 read12(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12))) 34 35 def read10(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32, pair: Array & U32) -> Array & T.State: 36 (a,w10) = pair 37 read11(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11))) 38 39 def read9(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32, pair: Array & U32) -> Array & T.State: 40 (a,w9) = pair 41 read10(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10))) 42 43 def read8(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32, pair: Array & U32) -> Array & T.State: 44 (a,w8) = pair 45 read9(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9))) 46 47 def read7(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32, pair: Array & U32) -> Array & T.State: 48 (a,w7) = pair 49 read8(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8))) 50 51 def read6(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32, pair: Array & U32) -> Array & T.State: 52 (a,w6) = pair 53 read7(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7))) 54 55 def read5(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32, pair: Array & U32) -> Array & T.State: 56 (a,w5) = pair 57 read6(index,h,t0,t1,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6))) 58 59 def read4(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32, pair: Array & U32) -> Array & T.State: 60 (a,w4) = pair 61 read5(index,h,t0,t1,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5))) 62 63 def read3(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32, pair: Array & U32) -> Array & T.State: 64 (a,w3) = pair 65 read4(index,h,t0,t1,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4))) 66 67 def read2(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32, pair: Array & U32) -> Array & T.State: 68 (a,w2) = pair 69 read3(index,h,t0,t1,w0,w1,w2,Array.get(U32,a,U32.add(index,3))) 70 71 def read1(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32, pair: Array & U32) -> Array & T.State: 72 (a,w1) = pair 73 read2(index,h,t0,t1,w0,w1,Array.get(U32,a,U32.add(index,2))) 74 75 def read0(+index: U32, h: T.State, t0: U32, t1: U32, pair: Array & U32) -> Array & T.State: 76 (a,w0) = pair 77 read1(index,h,t0,t1,w0,Array.get(U32,a,U32.add(index,1))) 78 79 def absorb(a: Array, +index: U32, h: T.State, t0: U32, t1: U32) -> Array & T.State: 80 read0(index,h,t0,t1,Array.get(U32,a,index)) 81 82 # The final block keeps the bytes before the logical length and zeroes the rest. 83 # keep(n, w) keeps the low n bytes of w. 84 def keep(n: Nat, +w: U32) -> U32: 85 match n: 86 case 0n: 0 87 case 1n: U32.and(255,w) 88 case 2n: U32.and(65535,w) 89 case 3n: U32.and(16777215,w) 90 case 4n+p: w 91 92 def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32: 93 keep(Nat.sub(remain,pos),w) 94 95 def pad15(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32,w14: U32, pair: Array & U32) -> T.State: 96 (a,w15) = pair 97 C.compress(h,pad_word(w0,0n,remain),pad_word(w1,4n,remain),pad_word(w2,8n,remain),pad_word(w3,12n,remain),pad_word(w4,16n,remain),pad_word(w5,20n,remain),pad_word(w6,24n,remain),pad_word(w7,28n,remain),pad_word(w8,32n,remain),pad_word(w9,36n,remain),pad_word(w10,40n,remain),pad_word(w11,44n,remain),pad_word(w12,48n,remain),pad_word(w13,52n,remain),pad_word(w14,56n,remain),pad_word(w15,60n,remain),t0,t1,True{}) 98 99 def pad14(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32, pair: Array & U32) -> T.State: 100 (a,w14) = pair 101 pad15(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15))) 102 103 def pad13(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32, pair: Array & U32) -> T.State: 104 (a,w13) = pair 105 pad14(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14))) 106 107 def pad12(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32, pair: Array & U32) -> T.State: 108 (a,w12) = pair 109 pad13(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13))) 110 111 def pad11(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32, pair: Array & U32) -> T.State: 112 (a,w11) = pair 113 pad12(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12))) 114 115 def pad10(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32, pair: Array & U32) -> T.State: 116 (a,w10) = pair 117 pad11(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11))) 118 119 def pad9(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32, pair: Array & U32) -> T.State: 120 (a,w9) = pair 121 pad10(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10))) 122 123 def pad8(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32, pair: Array & U32) -> T.State: 124 (a,w8) = pair 125 pad9(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9))) 126 127 def pad7(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32, pair: Array & U32) -> T.State: 128 (a,w7) = pair 129 pad8(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8))) 130 131 def pad6(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32, pair: Array & U32) -> T.State: 132 (a,w6) = pair 133 pad7(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7))) 134 135 def pad5(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32, pair: Array & U32) -> T.State: 136 (a,w5) = pair 137 pad6(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6))) 138 139 def pad4(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32, pair: Array & U32) -> T.State: 140 (a,w4) = pair 141 pad5(remain,index,h,t0,t1,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5))) 142 143 def pad3(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32, pair: Array & U32) -> T.State: 144 (a,w3) = pair 145 pad4(remain,index,h,t0,t1,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4))) 146 147 def pad2(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32, pair: Array & U32) -> T.State: 148 (a,w2) = pair 149 pad3(remain,index,h,t0,t1,w0,w1,w2,Array.get(U32,a,U32.add(index,3))) 150 151 def pad1(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32, pair: Array & U32) -> T.State: 152 (a,w1) = pair 153 pad2(remain,index,h,t0,t1,w0,w1,Array.get(U32,a,U32.add(index,2))) 154 155 def pad0(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, pair: Array & U32) -> T.State: 156 (a,w0) = pair 157 pad1(remain,index,h,t0,t1,w0,Array.get(U32,a,U32.add(index,1))) 158 159 def finish(a: Array, +index: U32, +t0: U32, t1: U32, +remain: Nat, h: T.State) -> T.State: 160 +n = U32.from_nat(remain) 161 pad0(remain,index,h,U32.add(t0,n),count_hi(t0,t1,n),Array.get(U32,a,index)) 162 163 def blocks(n: Nat, +index: U32, +t0: U32, t1: U32, +remain: Nat, pair: Array & T.State) -> T.State: 164 match n pair: 165 case 0n Tuple{a,h}: finish(a,index,t0,t1,remain,h) 166 case 1n+p Tuple{a,h}: 167 +c0 = U32.add(t0,64) 168 +c1 = count_hi(t0,t1,64) 169 blocks(p,U32.add(index,16),c0,c1,remain,absorb(a,index,h,c0,c1)) 170 171 # Parameter block for an unkeyed 32-byte digest: h0 = IV0 ^ 0x01010020. 172 def initial() -> T.State: 173 T.H{1795745351,3144134277,1013904242,2773480762,1359893119,2600822924,528734635,1541459225} 174 175 # Blocks before the last one: max(1, ceil(length/64)) - 1. 176 def leading(length: Nat) -> Nat: 177 Nat.sub(Nat.div(Nat.add(length,63n),64n),1n) 178 179 def unchecked(a: Array, +length: Nat) -> T.State: 180 +n = leading(length) 181 blocks(n,0,0,0,Nat.sub(length,Nat.mul(64n,n)),(a,initial())) 182 183 def digest(h: T.State) -> Array: 184 match h: 185 case T.H{h0,h1,h2,h3,h4,h5,h6,h7}: 186 a = Array.new(U32,3n,0) 187 a = Array.set(U32,a,0,h0) 188 a = Array.set(U32,a,1,h1) 189 a = Array.set(U32,a,2,h2) 190 a = Array.set(U32,a,3,h3) 191 a = Array.set(U32,a,4,h4) 192 a = Array.set(U32,a,5,h5) 193 a = Array.set(U32,a,6,h6) 194 a = Array.set(U32,a,7,h7) 195 a 196 197 def checked(valid: Bool, a: Array, length: Nat) -> Maybe<&1,Array>: 198 match valid: 199 case False{}: None{} 200 case True{}: Some{digest(unchecked(a,length))} 201 202 def sized(+length: Nat, pair: Array & U32) -> Maybe<&1,Array>: 203 (a,capacity) = pair 204 checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length) 205 206 # BLAKE2s-256 of the first `length` bytes of `a` (four little-endian bytes per 207 # word): the eight little-endian digest words, or None when length exceeds 208 # 4 * the array capacity. 209 def blake2s(a: Array, length: Nat) -> Maybe<&1,Array>: 210 sized(length,Array.size(U32,a))