SHA256.hs (20098B)
1 {-# OPTIONS_GHC -funbox-small-strict-fields #-} 2 {-# LANGUAGE BangPatterns #-} 3 {-# LANGUAGE RecordWildCards #-} 4 {-# LANGUAGE ViewPatterns #-} 5 6 -- | 7 -- Module: Crypto.Hash.SHA256 8 -- Copyright: (c) 2024 Jared Tobin 9 -- License: MIT 10 -- Maintainer: Jared Tobin <jared@ppad.tech> 11 -- 12 -- Pure SHA-256 and HMAC-SHA256 implementations for 13 -- strict and lazy ByteStrings, as specified by RFC's 14 -- [6234](https://datatracker.ietf.org/doc/html/rfc6234) and 15 -- [2104](https://datatracker.ietf.org/doc/html/rfc2104). 16 17 module Crypto.Hash.SHA256 ( 18 -- * SHA-256 message digest functions 19 hash 20 , hash_lazy 21 22 -- * SHA256-based MAC functions 23 , hmac 24 , hmac_lazy 25 ) where 26 27 import qualified Data.Bits as B 28 import Data.Bits ((.|.), (.&.)) 29 import qualified Data.ByteString as BS 30 import qualified Data.ByteString.Builder as BSB 31 import qualified Data.ByteString.Builder.Extra as BE 32 import qualified Data.ByteString.Internal as BI 33 import qualified Data.ByteString.Lazy as BL 34 import qualified Data.ByteString.Lazy.Internal as BLI 35 import qualified Data.ByteString.Unsafe as BU 36 import Data.Word (Word32, Word64) 37 import Foreign.ForeignPtr (plusForeignPtr) 38 39 -- preliminary utils 40 41 -- keystroke saver 42 fi :: (Integral a, Num b) => a -> b 43 fi = fromIntegral 44 {-# INLINE fi #-} 45 46 -- parse strict ByteString in BE order to Word32 (verbatim from 47 -- Data.Binary) 48 -- 49 -- invariant: 50 -- the input bytestring is at least 32 bits in length 51 unsafe_word32be :: BS.ByteString -> Word32 52 unsafe_word32be s = 53 (fi (s `BU.unsafeIndex` 0) `B.unsafeShiftL` 24) .|. 54 (fi (s `BU.unsafeIndex` 1) `B.unsafeShiftL` 16) .|. 55 (fi (s `BU.unsafeIndex` 2) `B.unsafeShiftL` 8) .|. 56 (fi (s `BU.unsafeIndex` 3)) 57 {-# INLINE unsafe_word32be #-} 58 59 -- utility types for more efficient ByteString management 60 61 data SSPair = SSPair 62 {-# UNPACK #-} !BS.ByteString 63 {-# UNPACK #-} !BS.ByteString 64 65 data SLPair = SLPair {-# UNPACK #-} !BS.ByteString !BL.ByteString 66 67 data WSPair = WSPair {-# UNPACK #-} !Word32 {-# UNPACK #-} !BS.ByteString 68 69 -- unsafe version of splitAt that does no bounds checking 70 -- 71 -- invariant: 72 -- 0 <= n <= l 73 unsafe_splitAt :: Int -> BS.ByteString -> SSPair 74 unsafe_splitAt n (BI.BS x l) = 75 SSPair (BI.BS x n) (BI.BS (plusForeignPtr x n) (l - n)) 76 77 -- variant of Data.ByteString.Lazy.splitAt that returns the initial 78 -- component as a strict, unboxed ByteString 79 splitAt64 :: BL.ByteString -> SLPair 80 splitAt64 = splitAt' (64 :: Int) where 81 splitAt' _ BLI.Empty = SLPair mempty BLI.Empty 82 splitAt' n (BLI.Chunk c@(BI.PS _ _ l) cs) = 83 if n < l 84 then 85 -- n < BS.length c, so unsafe_splitAt is safe 86 let !(SSPair c0 c1) = unsafe_splitAt n c 87 in SLPair c0 (BLI.Chunk c1 cs) 88 else 89 let SLPair cs' cs'' = splitAt' (n - l) cs 90 in SLPair (c <> cs') cs'' 91 92 -- variant of Data.ByteString.splitAt that behaves like an incremental 93 -- Word32 parser 94 -- 95 -- invariant: 96 -- the input bytestring is at least 32 bits in length 97 unsafe_parseWsPair :: BS.ByteString -> WSPair 98 unsafe_parseWsPair (BI.BS x l) = 99 WSPair (unsafe_word32be (BI.BS x 4)) (BI.BS (plusForeignPtr x 4) (l - 4)) 100 {-# INLINE unsafe_parseWsPair #-} 101 102 -- builder realization strategies 103 104 to_strict :: BSB.Builder -> BS.ByteString 105 to_strict = BL.toStrict . BSB.toLazyByteString 106 107 to_strict_small :: BSB.Builder -> BS.ByteString 108 to_strict_small = BL.toStrict . BE.toLazyByteStringWith 109 (BE.safeStrategy 128 BE.smallChunkSize) mempty 110 111 -- message padding and parsing 112 -- https://datatracker.ietf.org/doc/html/rfc6234#section-4.1 113 114 -- k such that (l + 1 + k) mod 64 = 56 115 sol :: Word64 -> Word64 116 sol l = 117 let r = 56 - fi l `rem` 64 - 1 :: Integer -- fi prevents underflow 118 in fi (if r < 0 then r + 64 else r) 119 120 -- RFC 6234 4.1 (strict) 121 pad :: BS.ByteString -> BS.ByteString 122 pad m@(BI.PS _ _ (fi -> l)) 123 | l < 128 = to_strict_small padded 124 | otherwise = to_strict padded 125 where 126 padded = BSB.byteString m 127 <> fill (sol l) (BSB.word8 0x80) 128 <> BSB.word64BE (l * 8) 129 130 fill j !acc 131 | j `rem` 8 == 0 = 132 loop64 j acc 133 | (j - 7) `rem` 8 == 0 = 134 loop64 (j - 7) acc 135 <> BSB.word32BE 0x00 136 <> BSB.word16BE 0x00 137 <> BSB.word8 0x00 138 | (j - 6) `rem` 8 == 0 = 139 loop64 (j - 6) acc 140 <> BSB.word32BE 0x00 141 <> BSB.word16BE 0x00 142 | (j - 5) `rem` 8 == 0 = 143 loop64 (j - 5) acc 144 <> BSB.word32BE 0x00 145 <> BSB.word8 0x00 146 | (j - 4) `rem` 8 == 0 = 147 loop64 (j - 4) acc 148 <> BSB.word32BE 0x00 149 | (j - 3) `rem` 8 == 0 = 150 loop64 (j - 3) acc 151 <> BSB.word16BE 0x00 152 <> BSB.word8 0x00 153 | (j - 2) `rem` 8 == 0 = 154 loop64 (j - 2) acc 155 <> BSB.word16BE 0x00 156 | (j - 1) `rem` 8 == 0 = 157 loop64 (j - 1) acc 158 <> BSB.word8 0x00 159 160 | j `rem` 4 == 0 = 161 loop32 j acc 162 | (j - 3) `rem` 4 == 0 = 163 loop32 (j - 3) acc 164 <> BSB.word16BE 0x00 165 <> BSB.word8 0x00 166 | (j - 2) `rem` 4 == 0 = 167 loop32 (j - 2) acc 168 <> BSB.word16BE 0x00 169 | (j - 1) `rem` 4 == 0 = 170 loop32 (j - 1) acc 171 <> BSB.word8 0x00 172 173 | j `rem` 2 == 0 = 174 loop16 j acc 175 | (j - 1) `rem` 2 == 0 = 176 loop16 (j - 1) acc 177 <> BSB.word8 0x00 178 179 | otherwise = 180 loop8 j acc 181 182 loop64 j !acc 183 | j == 0 = acc 184 | otherwise = loop64 (j - 8) (acc <> BSB.word64BE 0x00) 185 186 loop32 j !acc 187 | j == 0 = acc 188 | otherwise = loop32 (j - 4) (acc <> BSB.word32BE 0x00) 189 190 loop16 j !acc 191 | j == 0 = acc 192 | otherwise = loop16 (j - 2) (acc <> BSB.word16BE 0x00) 193 194 loop8 j !acc 195 | j == 0 = acc 196 | otherwise = loop8 (pred j) (acc <> BSB.word8 0x00) 197 198 -- RFC 6234 4.1 (lazy) 199 pad_lazy :: BL.ByteString -> BL.ByteString 200 pad_lazy (BL.toChunks -> m) = BL.fromChunks (walk 0 m) where 201 walk !l bs = case bs of 202 (c:cs) -> c : walk (l + fi (BS.length c)) cs 203 [] -> padding l (sol l) (BSB.word8 0x80) 204 205 padding l k bs 206 | k == 0 = 207 pure 208 . to_strict 209 -- more efficient for small builder 210 $ bs <> BSB.word64BE (l * 8) 211 | otherwise = 212 let nacc = bs <> BSB.word8 0x00 213 in padding l (pred k) nacc 214 215 -- functions and constants used 216 -- https://datatracker.ietf.org/doc/html/rfc6234#section-5.1 217 218 ch :: Word32 -> Word32 -> Word32 -> Word32 219 ch x y z = (x .&. y) `B.xor` (B.complement x .&. z) 220 {-# INLINE ch #-} 221 222 -- credit to SHA authors for the following optimisation. their text: 223 -- 224 -- > note: 225 -- > the original functions is (x & y) ^ (x & z) ^ (y & z) 226 -- > if you fire off truth tables, this is equivalent to 227 -- > (x & y) | (x & z) | (y & z) 228 -- > which you can the use distribution on: 229 -- > (x & (y | z)) | (y & z) 230 -- > which saves us one operation. 231 maj :: Word32 -> Word32 -> Word32 -> Word32 232 maj x y z = (x .&. (y .|. z)) .|. (y .&. z) 233 {-# INLINE maj #-} 234 235 bsig0 :: Word32 -> Word32 236 bsig0 x = B.rotateR x 2 `B.xor` B.rotateR x 13 `B.xor` B.rotateR x 22 237 {-# INLINE bsig0 #-} 238 239 bsig1 :: Word32 -> Word32 240 bsig1 x = B.rotateR x 6 `B.xor` B.rotateR x 11 `B.xor` B.rotateR x 25 241 {-# INLINE bsig1 #-} 242 243 ssig0 :: Word32 -> Word32 244 ssig0 x = B.rotateR x 7 `B.xor` B.rotateR x 18 `B.xor` B.unsafeShiftR x 3 245 {-# INLINE ssig0 #-} 246 247 ssig1 :: Word32 -> Word32 248 ssig1 x = B.rotateR x 17 `B.xor` B.rotateR x 19 `B.xor` B.unsafeShiftR x 10 249 {-# INLINE ssig1 #-} 250 251 data Schedule = Schedule { 252 w00 :: !Word32, w01 :: !Word32, w02 :: !Word32, w03 :: !Word32 253 , w04 :: !Word32, w05 :: !Word32, w06 :: !Word32, w07 :: !Word32 254 , w08 :: !Word32, w09 :: !Word32, w10 :: !Word32, w11 :: !Word32 255 , w12 :: !Word32, w13 :: !Word32, w14 :: !Word32, w15 :: !Word32 256 , w16 :: !Word32, w17 :: !Word32, w18 :: !Word32, w19 :: !Word32 257 , w20 :: !Word32, w21 :: !Word32, w22 :: !Word32, w23 :: !Word32 258 , w24 :: !Word32, w25 :: !Word32, w26 :: !Word32, w27 :: !Word32 259 , w28 :: !Word32, w29 :: !Word32, w30 :: !Word32, w31 :: !Word32 260 , w32 :: !Word32, w33 :: !Word32, w34 :: !Word32, w35 :: !Word32 261 , w36 :: !Word32, w37 :: !Word32, w38 :: !Word32, w39 :: !Word32 262 , w40 :: !Word32, w41 :: !Word32, w42 :: !Word32, w43 :: !Word32 263 , w44 :: !Word32, w45 :: !Word32, w46 :: !Word32, w47 :: !Word32 264 , w48 :: !Word32, w49 :: !Word32, w50 :: !Word32, w51 :: !Word32 265 , w52 :: !Word32, w53 :: !Word32, w54 :: !Word32, w55 :: !Word32 266 , w56 :: !Word32, w57 :: !Word32, w58 :: !Word32, w59 :: !Word32 267 , w60 :: !Word32, w61 :: !Word32, w62 :: !Word32, w63 :: !Word32 268 } 269 270 -- initialization 271 -- https://datatracker.ietf.org/doc/html/rfc6234#section-6.1 272 273 data Registers = Registers { 274 h0 :: !Word32, h1 :: !Word32, h2 :: !Word32, h3 :: !Word32 275 , h4 :: !Word32, h5 :: !Word32, h6 :: !Word32, h7 :: !Word32 276 } 277 278 -- first 32 bits of the fractional parts of the square roots of the 279 -- first eight primes 280 iv :: Registers 281 iv = Registers 282 0x6a09e667 0xbb67ae85 0x3c6ef372 0xa54ff53a 283 0x510e527f 0x9b05688c 0x1f83d9ab 0x5be0cd19 284 285 -- processing 286 -- https://datatracker.ietf.org/doc/html/rfc6234#section-6.2 287 288 data Block = Block { 289 m00 :: !Word32, m01 :: !Word32, m02 :: !Word32, m03 :: !Word32 290 , m04 :: !Word32, m05 :: !Word32, m06 :: !Word32, m07 :: !Word32 291 , m08 :: !Word32, m09 :: !Word32, m10 :: !Word32, m11 :: !Word32 292 , m12 :: !Word32, m13 :: !Word32, m14 :: !Word32, m15 :: !Word32 293 } 294 295 -- parse strict bytestring to block 296 -- 297 -- invariant: 298 -- the input bytestring is exactly 512 bits long 299 unsafe_parse :: BS.ByteString -> Block 300 unsafe_parse bs = 301 let !(WSPair m00 t00) = unsafe_parseWsPair bs 302 !(WSPair m01 t01) = unsafe_parseWsPair t00 303 !(WSPair m02 t02) = unsafe_parseWsPair t01 304 !(WSPair m03 t03) = unsafe_parseWsPair t02 305 !(WSPair m04 t04) = unsafe_parseWsPair t03 306 !(WSPair m05 t05) = unsafe_parseWsPair t04 307 !(WSPair m06 t06) = unsafe_parseWsPair t05 308 !(WSPair m07 t07) = unsafe_parseWsPair t06 309 !(WSPair m08 t08) = unsafe_parseWsPair t07 310 !(WSPair m09 t09) = unsafe_parseWsPair t08 311 !(WSPair m10 t10) = unsafe_parseWsPair t09 312 !(WSPair m11 t11) = unsafe_parseWsPair t10 313 !(WSPair m12 t12) = unsafe_parseWsPair t11 314 !(WSPair m13 t13) = unsafe_parseWsPair t12 315 !(WSPair m14 t14) = unsafe_parseWsPair t13 316 !(WSPair m15 t15) = unsafe_parseWsPair t14 317 in if BS.null t15 318 then Block {..} 319 else error "ppad-sha256: internal error (bytes remaining)" 320 321 -- RFC 6234 6.2 step 1 322 prepare_schedule :: Block -> Schedule 323 prepare_schedule Block {..} = Schedule {..} where 324 w00 = m00; w01 = m01; w02 = m02; w03 = m03 325 w04 = m04; w05 = m05; w06 = m06; w07 = m07 326 w08 = m08; w09 = m09; w10 = m10; w11 = m11 327 w12 = m12; w13 = m13; w14 = m14; w15 = m15 328 w16 = ssig1 w14 + w09 + ssig0 w01 + w00 329 w17 = ssig1 w15 + w10 + ssig0 w02 + w01 330 w18 = ssig1 w16 + w11 + ssig0 w03 + w02 331 w19 = ssig1 w17 + w12 + ssig0 w04 + w03 332 w20 = ssig1 w18 + w13 + ssig0 w05 + w04 333 w21 = ssig1 w19 + w14 + ssig0 w06 + w05 334 w22 = ssig1 w20 + w15 + ssig0 w07 + w06 335 w23 = ssig1 w21 + w16 + ssig0 w08 + w07 336 w24 = ssig1 w22 + w17 + ssig0 w09 + w08 337 w25 = ssig1 w23 + w18 + ssig0 w10 + w09 338 w26 = ssig1 w24 + w19 + ssig0 w11 + w10 339 w27 = ssig1 w25 + w20 + ssig0 w12 + w11 340 w28 = ssig1 w26 + w21 + ssig0 w13 + w12 341 w29 = ssig1 w27 + w22 + ssig0 w14 + w13 342 w30 = ssig1 w28 + w23 + ssig0 w15 + w14 343 w31 = ssig1 w29 + w24 + ssig0 w16 + w15 344 w32 = ssig1 w30 + w25 + ssig0 w17 + w16 345 w33 = ssig1 w31 + w26 + ssig0 w18 + w17 346 w34 = ssig1 w32 + w27 + ssig0 w19 + w18 347 w35 = ssig1 w33 + w28 + ssig0 w20 + w19 348 w36 = ssig1 w34 + w29 + ssig0 w21 + w20 349 w37 = ssig1 w35 + w30 + ssig0 w22 + w21 350 w38 = ssig1 w36 + w31 + ssig0 w23 + w22 351 w39 = ssig1 w37 + w32 + ssig0 w24 + w23 352 w40 = ssig1 w38 + w33 + ssig0 w25 + w24 353 w41 = ssig1 w39 + w34 + ssig0 w26 + w25 354 w42 = ssig1 w40 + w35 + ssig0 w27 + w26 355 w43 = ssig1 w41 + w36 + ssig0 w28 + w27 356 w44 = ssig1 w42 + w37 + ssig0 w29 + w28 357 w45 = ssig1 w43 + w38 + ssig0 w30 + w29 358 w46 = ssig1 w44 + w39 + ssig0 w31 + w30 359 w47 = ssig1 w45 + w40 + ssig0 w32 + w31 360 w48 = ssig1 w46 + w41 + ssig0 w33 + w32 361 w49 = ssig1 w47 + w42 + ssig0 w34 + w33 362 w50 = ssig1 w48 + w43 + ssig0 w35 + w34 363 w51 = ssig1 w49 + w44 + ssig0 w36 + w35 364 w52 = ssig1 w50 + w45 + ssig0 w37 + w36 365 w53 = ssig1 w51 + w46 + ssig0 w38 + w37 366 w54 = ssig1 w52 + w47 + ssig0 w39 + w38 367 w55 = ssig1 w53 + w48 + ssig0 w40 + w39 368 w56 = ssig1 w54 + w49 + ssig0 w41 + w40 369 w57 = ssig1 w55 + w50 + ssig0 w42 + w41 370 w58 = ssig1 w56 + w51 + ssig0 w43 + w42 371 w59 = ssig1 w57 + w52 + ssig0 w44 + w43 372 w60 = ssig1 w58 + w53 + ssig0 w45 + w44 373 w61 = ssig1 w59 + w54 + ssig0 w46 + w45 374 w62 = ssig1 w60 + w55 + ssig0 w47 + w46 375 w63 = ssig1 w61 + w56 + ssig0 w48 + w47 376 377 -- RFC 6234 6.2 steps 2, 3, 4 378 block_hash :: Registers -> Schedule -> Registers 379 block_hash r00@Registers {..} Schedule {..} = 380 -- constants are the first 32 bits of the fractional parts of the 381 -- cube roots of the first sixty-four prime numbers 382 let r01 = step r00 0x428a2f98 w00; r02 = step r01 0x71374491 w01 383 r03 = step r02 0xb5c0fbcf w02; r04 = step r03 0xe9b5dba5 w03 384 r05 = step r04 0x3956c25b w04; r06 = step r05 0x59f111f1 w05 385 r07 = step r06 0x923f82a4 w06; r08 = step r07 0xab1c5ed5 w07 386 r09 = step r08 0xd807aa98 w08; r10 = step r09 0x12835b01 w09 387 r11 = step r10 0x243185be w10; r12 = step r11 0x550c7dc3 w11 388 r13 = step r12 0x72be5d74 w12; r14 = step r13 0x80deb1fe w13 389 r15 = step r14 0x9bdc06a7 w14; r16 = step r15 0xc19bf174 w15 390 r17 = step r16 0xe49b69c1 w16; r18 = step r17 0xefbe4786 w17 391 r19 = step r18 0x0fc19dc6 w18; r20 = step r19 0x240ca1cc w19 392 r21 = step r20 0x2de92c6f w20; r22 = step r21 0x4a7484aa w21 393 r23 = step r22 0x5cb0a9dc w22; r24 = step r23 0x76f988da w23 394 r25 = step r24 0x983e5152 w24; r26 = step r25 0xa831c66d w25 395 r27 = step r26 0xb00327c8 w26; r28 = step r27 0xbf597fc7 w27 396 r29 = step r28 0xc6e00bf3 w28; r30 = step r29 0xd5a79147 w29 397 r31 = step r30 0x06ca6351 w30; r32 = step r31 0x14292967 w31 398 r33 = step r32 0x27b70a85 w32; r34 = step r33 0x2e1b2138 w33 399 r35 = step r34 0x4d2c6dfc w34; r36 = step r35 0x53380d13 w35 400 r37 = step r36 0x650a7354 w36; r38 = step r37 0x766a0abb w37 401 r39 = step r38 0x81c2c92e w38; r40 = step r39 0x92722c85 w39 402 r41 = step r40 0xa2bfe8a1 w40; r42 = step r41 0xa81a664b w41 403 r43 = step r42 0xc24b8b70 w42; r44 = step r43 0xc76c51a3 w43 404 r45 = step r44 0xd192e819 w44; r46 = step r45 0xd6990624 w45 405 r47 = step r46 0xf40e3585 w46; r48 = step r47 0x106aa070 w47 406 r49 = step r48 0x19a4c116 w48; r50 = step r49 0x1e376c08 w49 407 r51 = step r50 0x2748774c w50; r52 = step r51 0x34b0bcb5 w51 408 r53 = step r52 0x391c0cb3 w52; r54 = step r53 0x4ed8aa4a w53 409 r55 = step r54 0x5b9cca4f w54; r56 = step r55 0x682e6ff3 w55 410 r57 = step r56 0x748f82ee w56; r58 = step r57 0x78a5636f w57 411 r59 = step r58 0x84c87814 w58; r60 = step r59 0x8cc70208 w59 412 r61 = step r60 0x90befffa w60; r62 = step r61 0xa4506ceb w61 413 r63 = step r62 0xbef9a3f7 w62; r64 = step r63 0xc67178f2 w63 414 !(Registers a b c d e f g h) = r64 415 in Registers 416 (a + h0) (b + h1) (c + h2) (d + h3) 417 (e + h4) (f + h5) (g + h6) (h + h7) 418 419 step :: Registers -> Word32 -> Word32 -> Registers 420 step (Registers a b c d e f g h) k w = 421 let t1 = h + bsig1 e + ch e f g + k + w 422 t2 = bsig0 a + maj a b c 423 in Registers (t1 + t2) a b c (d + t1) e f g 424 {-# INLINE step #-} 425 426 -- RFC 6234 6.2 block pipeline 427 -- 428 -- invariant: 429 -- the input bytestring is exactly 512 bits in length 430 unsafe_hash_alg :: Registers -> BS.ByteString -> Registers 431 unsafe_hash_alg rs bs = block_hash rs (prepare_schedule (unsafe_parse bs)) 432 433 -- register concatenation 434 cat :: Registers -> BS.ByteString 435 cat Registers {..} = to_strict_small $ 436 BSB.word64BE w64_0 <> BSB.word64BE w64_1 437 <> BSB.word64BE w64_2 <> BSB.word64BE w64_3 438 where 439 !w64_0 = fi h0 `B.unsafeShiftL` 32 .|. fi h1 440 !w64_1 = fi h2 `B.unsafeShiftL` 32 .|. fi h3 441 !w64_2 = fi h4 `B.unsafeShiftL` 32 .|. fi h5 442 !w64_3 = fi h6 `B.unsafeShiftL` 32 .|. fi h7 443 444 -- | Compute a condensed representation of a strict bytestring via 445 -- SHA-256. 446 -- 447 -- The 256-bit output digest is returned as a strict bytestring. 448 -- 449 -- >>> hash "strict bytestring input" 450 -- "<strict 256-bit message digest>" 451 hash :: BS.ByteString -> BS.ByteString 452 hash bs = cat (go iv (pad bs)) where 453 -- proof that 'go' always terminates safely: 454 -- 455 -- let b = pad bs 456 -- then length(b) = n * 512 bits for some n >= 0 (1) 457 go :: Registers -> BS.ByteString -> Registers 458 go !acc b 459 -- if n == 0, then 'go' terminates safely (2) 460 | BS.null b = acc 461 -- if n > 0, then 462 -- 463 -- let (c, r) = unsafe_splitAt 64 b 464 -- then length(c) == 512 bits by (1) 465 -- length(r) == m * 512 bits for some m >= 0 by (1) 466 -- 467 -- note 'unsafe_hash_alg' terminates safely for bytestring (3) 468 -- input of exactly 512 bits in length 469 -- 470 -- length(c) == 512 471 -- => 'unsafe_hash_alg' terminates safely by (3) 472 -- => 'go' terminates safely (4) 473 -- length(r) == m * 512 bits for m >= 0 474 -- => next invocation of 'go' terminates safely by (2), (4) 475 -- 476 -- then by induction, 'go' always terminates safely (QED) 477 | otherwise = case unsafe_splitAt 64 b of 478 SSPair c r -> go (unsafe_hash_alg acc c) r 479 480 -- | Compute a condensed representation of a lazy bytestring via 481 -- SHA-256. 482 -- 483 -- The 256-bit output digest is returned as a strict bytestring. 484 -- 485 -- >>> hash_lazy "lazy bytestring input" 486 -- "<strict 256-bit message digest>" 487 hash_lazy :: BL.ByteString -> BS.ByteString 488 hash_lazy bl = cat (go iv (pad_lazy bl)) where 489 -- proof of safety proceeds analogously 490 go :: Registers -> BL.ByteString -> Registers 491 go !acc bs 492 | BL.null bs = acc 493 | otherwise = case splitAt64 bs of 494 SLPair c r -> go (unsafe_hash_alg acc c) r 495 496 -- HMAC ----------------------------------------------------------------------- 497 -- https://datatracker.ietf.org/doc/html/rfc2104#section-2 498 499 data KeyAndLen = KeyAndLen 500 {-# UNPACK #-} !BS.ByteString 501 {-# UNPACK #-} !Int 502 503 -- | Produce a message authentication code for a strict bytestring, 504 -- based on the provided (strict, bytestring) key, via SHA-256. 505 -- 506 -- The 256-bit MAC is returned as a strict bytestring. 507 -- 508 -- Per RFC 2104, the key /should/ be a minimum of 32 bytes long. Keys 509 -- exceeding 64 bytes in length will first be hashed (via SHA-256). 510 -- 511 -- >>> hmac "strict bytestring key" "strict bytestring input" 512 -- "<strict 256-bit MAC>" 513 hmac 514 :: BS.ByteString -- ^ key 515 -> BS.ByteString -- ^ text 516 -> BS.ByteString 517 hmac mk@(BI.PS _ _ l) text = 518 let step1 = k <> BS.replicate (64 - lk) 0x00 519 step2 = BS.map (B.xor 0x36) step1 520 step3 = step2 <> text 521 step4 = hash step3 522 step5 = BS.map (B.xor 0x5C) step1 523 step6 = step5 <> step4 524 in hash step6 525 where 526 !(KeyAndLen k lk) 527 | l > 64 = KeyAndLen (hash mk) 32 528 | otherwise = KeyAndLen mk l 529 530 -- | Produce a message authentication code for a lazy bytestring, based 531 -- on the provided (strict, bytestring) key, via SHA-256. 532 -- 533 -- The 256-bit MAC is returned as a strict bytestring. 534 -- 535 -- Per RFC 2104, the key /should/ be a minimum of 32 bytes long. Keys 536 -- exceeding 64 bytes in length will first be hashed (via SHA-256). 537 -- 538 -- >>> hmac_lazy "strict bytestring key" "lazy bytestring input" 539 -- "<strict 256-bit MAC>" 540 hmac_lazy 541 :: BS.ByteString -- ^ key 542 -> BL.ByteString -- ^ text 543 -> BS.ByteString 544 hmac_lazy mk@(BI.PS _ _ l) text = 545 let step1 = k <> BS.replicate (64 - lk) 0x00 546 step2 = BS.map (B.xor 0x36) step1 547 step3 = BL.fromStrict step2 <> text 548 step4 = hash_lazy step3 549 step5 = BS.map (B.xor 0x5C) step1 550 step6 = step5 <> step4 551 in hash step6 552 where 553 !(KeyAndLen k lk) 554 | l > 64 = KeyAndLen (hash mk) 32 555 | otherwise = KeyAndLen mk l 556