sha512

Pure Haskell SHA-512, HMAC-SHA512 (docs.ppad.tech/sha512).
git clone git://git.ppad.tech/sha512.git
Log | Files | Refs | README | LICENSE

SHA512.hs (22853B)


      1 {-# OPTIONS_GHC -funbox-small-strict-fields #-}
      2 {-# LANGUAGE BangPatterns #-}
      3 {-# LANGUAGE RecordWildCards #-}
      4 {-# LANGUAGE ViewPatterns #-}
      5 
      6 -- |
      7 -- Module: Crypto.Hash.SHA512
      8 -- Copyright: (c) 2024 Jared Tobin
      9 -- License: MIT
     10 -- Maintainer: Jared Tobin <jared@ppad.tech>
     11 --
     12 -- Pure SHA-512 and HMAC-SHA512 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.SHA512 (
     18   -- * SHA-512 message digest functions
     19     hash
     20   , hash_lazy
     21 
     22   -- * SHA512-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 (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 Word64 (verbatim from
     47 -- Data.Binary)
     48 --
     49 -- invariant:
     50 --   the input bytestring is at least 64 bits in length
     51 unsafe_word64be :: BS.ByteString -> Word64
     52 unsafe_word64be s =
     53   (fi (s `BU.unsafeIndex` 0) `B.unsafeShiftL` 56) .|.
     54   (fi (s `BU.unsafeIndex` 1) `B.unsafeShiftL` 48) .|.
     55   (fi (s `BU.unsafeIndex` 2) `B.unsafeShiftL` 40) .|.
     56   (fi (s `BU.unsafeIndex` 3) `B.unsafeShiftL` 32) .|.
     57   (fi (s `BU.unsafeIndex` 4) `B.unsafeShiftL` 24) .|.
     58   (fi (s `BU.unsafeIndex` 5) `B.unsafeShiftL` 16) .|.
     59   (fi (s `BU.unsafeIndex` 6) `B.unsafeShiftL`  8) .|.
     60   (fi (s `BU.unsafeIndex` 7) )
     61 {-# INLINE unsafe_word64be #-}
     62 
     63 -- utility types for more efficient ByteString management
     64 
     65 data SSPair = SSPair
     66   {-# UNPACK #-} !BS.ByteString
     67   {-# UNPACK #-} !BS.ByteString
     68 
     69 data SLPair = SLPair {-# UNPACK #-} !BS.ByteString !BL.ByteString
     70 
     71 data WSPair = WSPair {-# UNPACK #-} !Word64 {-# UNPACK #-} !BS.ByteString
     72 
     73 -- unsafe version of splitAt that does no bounds checking
     74 --
     75 -- invariant:
     76 --   0 <= n <= l
     77 unsafe_splitAt :: Int -> BS.ByteString -> SSPair
     78 unsafe_splitAt n (BI.BS x l) =
     79   SSPair (BI.BS x n) (BI.BS (plusForeignPtr x n) (l - n))
     80 
     81 -- variant of Data.ByteString.Lazy.splitAt that returns the initial
     82 -- component as a strict, unboxed ByteString
     83 splitAt128 :: BL.ByteString -> SLPair
     84 splitAt128 = splitAt' (128 :: Int) where
     85   splitAt' _ BLI.Empty        = SLPair mempty BLI.Empty
     86   splitAt' n (BLI.Chunk c@(BI.PS _ _ l) cs) =
     87     if    n < l
     88     then
     89       -- n < BS.length c, so unsafe_splitAt is safe
     90       let !(SSPair c0 c1) = unsafe_splitAt n c
     91       in  SLPair c0 (BLI.Chunk c1 cs)
     92     else
     93       let SLPair cs' cs'' = splitAt' (n - l) cs
     94       in  SLPair (c <> cs') cs''
     95 
     96 -- variant of Data.ByteString.splitAt that behaves like an incremental
     97 -- Word64 parser
     98 --
     99 -- invariant:
    100 --   the input bytestring is at least 64 bits in length
    101 unsafe_parseWsPair :: BS.ByteString -> WSPair
    102 unsafe_parseWsPair (BI.BS x l) =
    103   WSPair (unsafe_word64be (BI.BS x 8)) (BI.BS (plusForeignPtr x 8) (l - 8))
    104 {-# INLINE unsafe_parseWsPair #-}
    105 
    106 -- builder realization strategies
    107 
    108 to_strict :: BSB.Builder -> BS.ByteString
    109 to_strict = BL.toStrict . BSB.toLazyByteString
    110 
    111 to_strict_small :: BSB.Builder -> BS.ByteString
    112 to_strict_small = BL.toStrict . BE.toLazyByteStringWith
    113   (BE.safeStrategy 128 BE.smallChunkSize) mempty
    114 
    115 -- message padding and parsing ------------------------------------------------
    116 -- https://datatracker.ietf.org/doc/html/rfc6234#section-4.1
    117 
    118 -- k such that (l + 1 + k) mod 128 = 112
    119 sol :: Word64 -> Word64
    120 sol l =
    121   let r = 112 - fi l `rem` 128 - 1 :: Integer -- fi prevents underflow
    122   in  fi (if r < 0 then r + 128 else r)
    123 
    124 -- RFC 6234 4.1 (strict)
    125 pad :: BS.ByteString -> BS.ByteString
    126 pad m@(BI.PS _ _ (fi -> l))
    127     | l < 128   = to_strict_small padded
    128     | otherwise = to_strict padded
    129   where
    130     padded = BSB.byteString m
    131           <> fill (sol l) (BSB.word8 0x80)
    132           <> BSB.word64BE 0x00
    133           <> BSB.word64BE (l * 8)
    134 
    135     fill j !acc
    136       | j `rem` 8 == 0 =
    137              loop64 j acc
    138       | (j - 7) `rem` 8 == 0 =
    139              loop64 (j - 7) acc
    140           <> BSB.word32BE 0x00
    141           <> BSB.word16BE 0x00
    142           <> BSB.word8 0x00
    143       | (j - 6) `rem` 8 == 0 =
    144              loop64 (j - 6) acc
    145           <> BSB.word32BE 0x00
    146           <> BSB.word16BE 0x00
    147       | (j - 5) `rem` 8 == 0 =
    148              loop64 (j - 5) acc
    149           <> BSB.word32BE 0x00
    150           <> BSB.word8 0x00
    151       | (j - 4) `rem` 8 == 0 =
    152              loop64 (j - 4) acc
    153           <> BSB.word32BE 0x00
    154       | (j - 3) `rem` 8 == 0 =
    155              loop64 (j - 3) acc
    156           <> BSB.word16BE 0x00
    157           <> BSB.word8 0x00
    158       | (j - 2) `rem` 8 == 0 =
    159              loop64 (j - 2) acc
    160           <> BSB.word16BE 0x00
    161       | (j - 1) `rem` 8 == 0 =
    162              loop64 (j - 1) acc
    163           <> BSB.word8 0x00
    164 
    165       | j `rem` 4 == 0 =
    166              loop32 j acc
    167       | (j - 3) `rem` 4 == 0 =
    168              loop32 (j - 3) acc
    169           <> BSB.word16BE 0x00
    170           <> BSB.word8 0x00
    171       | (j - 2) `rem` 4 == 0 =
    172              loop32 (j - 2) acc
    173           <> BSB.word16BE 0x00
    174       | (j - 1) `rem` 4 == 0 =
    175              loop32 (j - 1) acc
    176           <> BSB.word8 0x00
    177 
    178       | j `rem` 2 == 0 =
    179              loop16 j acc
    180       | (j - 1) `rem` 2 == 0 =
    181              loop16 (j - 1) acc
    182           <> BSB.word8 0x00
    183 
    184       | otherwise =
    185             loop8 j acc
    186 
    187     loop64 j !acc
    188       | j == 0 = acc
    189       | otherwise = loop64 (j - 8) (acc <> BSB.word64BE 0x00)
    190 
    191     loop32 j !acc
    192       | j == 0 = acc
    193       | otherwise = loop32 (j - 4) (acc <> BSB.word32BE 0x00)
    194 
    195     loop16 j !acc
    196       | j == 0 = acc
    197       | otherwise = loop16 (j - 2) (acc <> BSB.word16BE 0x00)
    198 
    199     loop8 j !acc
    200       | j == 0 = acc
    201       | otherwise = loop8 (pred j) (acc <> BSB.word8 0x00)
    202 
    203 -- RFC 6234 4.1 (lazy)
    204 pad_lazy :: BL.ByteString -> BL.ByteString
    205 pad_lazy (BL.toChunks -> m) = BL.fromChunks (walk 0 m) where
    206   walk !l bs = case bs of
    207     (c:cs) -> c : walk (l + fi (BS.length c)) cs
    208     [] -> padding l (sol l) (BSB.word8 0x80)
    209 
    210   padding l k bs
    211     | k == 0 =
    212           pure
    213         . to_strict
    214         $ bs <> BSB.word64BE 0x00 <> BSB.word64BE (l * 8)
    215     | otherwise =
    216         let nacc = bs <> BSB.word8 0x00
    217         in  padding l (pred k) nacc
    218 
    219 -- functions and constants used -----------------------------------------------
    220 -- https://datatracker.ietf.org/doc/html/rfc6234#section-5.1
    221 
    222 ch :: Word64 -> Word64 -> Word64 -> Word64
    223 ch x y z = (x .&. y) `B.xor` (B.complement x .&. z)
    224 {-# INLINE ch #-}
    225 
    226 -- credit to SHA authors for the following optimisation. their text:
    227 --
    228 -- > note:
    229 -- >   the original functions is (x & y) ^ (x & z) ^ (y & z)
    230 -- >   if you fire off truth tables, this is equivalent to
    231 -- >     (x & y) | (x & z) | (y & z)
    232 -- >   which you can the use distribution on:
    233 -- >     (x & (y | z)) | (y & z)
    234 -- >   which saves us one operation.
    235 maj :: Word64 -> Word64 -> Word64 -> Word64
    236 maj x y z = (x .&. (y .|. z)) .|. (y .&. z)
    237 {-# INLINE maj #-}
    238 
    239 bsig0 :: Word64 -> Word64
    240 bsig0 x = B.rotateR x 28 `B.xor` B.rotateR x 34 `B.xor` B.rotateR x 39
    241 {-# INLINE bsig0 #-}
    242 
    243 bsig1 :: Word64 -> Word64
    244 bsig1 x = B.rotateR x 14 `B.xor` B.rotateR x 18 `B.xor` B.rotateR x 41
    245 {-# INLINE bsig1 #-}
    246 
    247 ssig0 :: Word64 -> Word64
    248 ssig0 x = B.rotateR x 1 `B.xor` B.rotateR x 8 `B.xor` B.unsafeShiftR x 7
    249 {-# INLINE ssig0 #-}
    250 
    251 ssig1 :: Word64 -> Word64
    252 ssig1 x = B.rotateR x 19 `B.xor` B.rotateR x 61 `B.xor` B.unsafeShiftR x 6
    253 {-# INLINE ssig1 #-}
    254 
    255 data Schedule = Schedule {
    256     w00 :: !Word64, w01 :: !Word64, w02 :: !Word64, w03 :: !Word64
    257   , w04 :: !Word64, w05 :: !Word64, w06 :: !Word64, w07 :: !Word64
    258   , w08 :: !Word64, w09 :: !Word64, w10 :: !Word64, w11 :: !Word64
    259   , w12 :: !Word64, w13 :: !Word64, w14 :: !Word64, w15 :: !Word64
    260   , w16 :: !Word64, w17 :: !Word64, w18 :: !Word64, w19 :: !Word64
    261   , w20 :: !Word64, w21 :: !Word64, w22 :: !Word64, w23 :: !Word64
    262   , w24 :: !Word64, w25 :: !Word64, w26 :: !Word64, w27 :: !Word64
    263   , w28 :: !Word64, w29 :: !Word64, w30 :: !Word64, w31 :: !Word64
    264   , w32 :: !Word64, w33 :: !Word64, w34 :: !Word64, w35 :: !Word64
    265   , w36 :: !Word64, w37 :: !Word64, w38 :: !Word64, w39 :: !Word64
    266   , w40 :: !Word64, w41 :: !Word64, w42 :: !Word64, w43 :: !Word64
    267   , w44 :: !Word64, w45 :: !Word64, w46 :: !Word64, w47 :: !Word64
    268   , w48 :: !Word64, w49 :: !Word64, w50 :: !Word64, w51 :: !Word64
    269   , w52 :: !Word64, w53 :: !Word64, w54 :: !Word64, w55 :: !Word64
    270   , w56 :: !Word64, w57 :: !Word64, w58 :: !Word64, w59 :: !Word64
    271   , w60 :: !Word64, w61 :: !Word64, w62 :: !Word64, w63 :: !Word64
    272   , w64 :: !Word64, w65 :: !Word64, w66 :: !Word64, w67 :: !Word64
    273   , w68 :: !Word64, w69 :: !Word64, w70 :: !Word64, w71 :: !Word64
    274   , w72 :: !Word64, w73 :: !Word64, w74 :: !Word64, w75 :: !Word64
    275   , w76 :: !Word64, w77 :: !Word64, w78 :: !Word64, w79 :: !Word64
    276   }
    277 
    278 -- initialization -------------------------------------------------------------
    279 -- https://datatracker.ietf.org/doc/html/rfc6234#section-6.1
    280 
    281 data Registers = Registers {
    282     h0 :: !Word64, h1 :: !Word64, h2 :: !Word64, h3 :: !Word64
    283   , h4 :: !Word64, h5 :: !Word64, h6 :: !Word64, h7 :: !Word64
    284   }
    285 
    286 -- first 64 bits of the fractional parts of the square roots of the
    287 -- first eight primes
    288 iv :: Registers
    289 iv = Registers
    290   0x6a09e667f3bcc908 0xbb67ae8584caa73b 0x3c6ef372fe94f82b 0xa54ff53a5f1d36f1
    291   0x510e527fade682d1 0x9b05688c2b3e6c1f 0x1f83d9abfb41bd6b 0x5be0cd19137e2179
    292 
    293 -- processing -----------------------------------------------------------------
    294 -- https://datatracker.ietf.org/doc/html/rfc6234#section-6.2
    295 
    296 data Block = Block {
    297     m00 :: !Word64, m01 :: !Word64, m02 :: !Word64, m03 :: !Word64
    298   , m04 :: !Word64, m05 :: !Word64, m06 :: !Word64, m07 :: !Word64
    299   , m08 :: !Word64, m09 :: !Word64, m10 :: !Word64, m11 :: !Word64
    300   , m12 :: !Word64, m13 :: !Word64, m14 :: !Word64, m15 :: !Word64
    301   }
    302 
    303 -- parse strict bytestring to block
    304 --
    305 -- invariant:
    306 --   the input bytestring is exactly 1024 bits long
    307 unsafe_parse :: BS.ByteString -> Block
    308 unsafe_parse bs =
    309   let !(WSPair m00 t00) = unsafe_parseWsPair bs
    310       !(WSPair m01 t01) = unsafe_parseWsPair t00
    311       !(WSPair m02 t02) = unsafe_parseWsPair t01
    312       !(WSPair m03 t03) = unsafe_parseWsPair t02
    313       !(WSPair m04 t04) = unsafe_parseWsPair t03
    314       !(WSPair m05 t05) = unsafe_parseWsPair t04
    315       !(WSPair m06 t06) = unsafe_parseWsPair t05
    316       !(WSPair m07 t07) = unsafe_parseWsPair t06
    317       !(WSPair m08 t08) = unsafe_parseWsPair t07
    318       !(WSPair m09 t09) = unsafe_parseWsPair t08
    319       !(WSPair m10 t10) = unsafe_parseWsPair t09
    320       !(WSPair m11 t11) = unsafe_parseWsPair t10
    321       !(WSPair m12 t12) = unsafe_parseWsPair t11
    322       !(WSPair m13 t13) = unsafe_parseWsPair t12
    323       !(WSPair m14 t14) = unsafe_parseWsPair t13
    324       !(WSPair m15 t15) = unsafe_parseWsPair t14
    325   in  if   BS.null t15
    326       then Block {..}
    327       else error "ppad-sha512: internal error (bytes remaining)"
    328 
    329 -- RFC 6234 6.2 step 1
    330 prepare_schedule :: Block -> Schedule
    331 prepare_schedule Block {..} = Schedule {..} where
    332   w00 = m00; w01 = m01; w02 = m02; w03 = m03
    333   w04 = m04; w05 = m05; w06 = m06; w07 = m07
    334   w08 = m08; w09 = m09; w10 = m10; w11 = m11
    335   w12 = m12; w13 = m13; w14 = m14; w15 = m15
    336   w16 = ssig1 w14 + w09 + ssig0 w01 + w00
    337   w17 = ssig1 w15 + w10 + ssig0 w02 + w01
    338   w18 = ssig1 w16 + w11 + ssig0 w03 + w02
    339   w19 = ssig1 w17 + w12 + ssig0 w04 + w03
    340   w20 = ssig1 w18 + w13 + ssig0 w05 + w04
    341   w21 = ssig1 w19 + w14 + ssig0 w06 + w05
    342   w22 = ssig1 w20 + w15 + ssig0 w07 + w06
    343   w23 = ssig1 w21 + w16 + ssig0 w08 + w07
    344   w24 = ssig1 w22 + w17 + ssig0 w09 + w08
    345   w25 = ssig1 w23 + w18 + ssig0 w10 + w09
    346   w26 = ssig1 w24 + w19 + ssig0 w11 + w10
    347   w27 = ssig1 w25 + w20 + ssig0 w12 + w11
    348   w28 = ssig1 w26 + w21 + ssig0 w13 + w12
    349   w29 = ssig1 w27 + w22 + ssig0 w14 + w13
    350   w30 = ssig1 w28 + w23 + ssig0 w15 + w14
    351   w31 = ssig1 w29 + w24 + ssig0 w16 + w15
    352   w32 = ssig1 w30 + w25 + ssig0 w17 + w16
    353   w33 = ssig1 w31 + w26 + ssig0 w18 + w17
    354   w34 = ssig1 w32 + w27 + ssig0 w19 + w18
    355   w35 = ssig1 w33 + w28 + ssig0 w20 + w19
    356   w36 = ssig1 w34 + w29 + ssig0 w21 + w20
    357   w37 = ssig1 w35 + w30 + ssig0 w22 + w21
    358   w38 = ssig1 w36 + w31 + ssig0 w23 + w22
    359   w39 = ssig1 w37 + w32 + ssig0 w24 + w23
    360   w40 = ssig1 w38 + w33 + ssig0 w25 + w24
    361   w41 = ssig1 w39 + w34 + ssig0 w26 + w25
    362   w42 = ssig1 w40 + w35 + ssig0 w27 + w26
    363   w43 = ssig1 w41 + w36 + ssig0 w28 + w27
    364   w44 = ssig1 w42 + w37 + ssig0 w29 + w28
    365   w45 = ssig1 w43 + w38 + ssig0 w30 + w29
    366   w46 = ssig1 w44 + w39 + ssig0 w31 + w30
    367   w47 = ssig1 w45 + w40 + ssig0 w32 + w31
    368   w48 = ssig1 w46 + w41 + ssig0 w33 + w32
    369   w49 = ssig1 w47 + w42 + ssig0 w34 + w33
    370   w50 = ssig1 w48 + w43 + ssig0 w35 + w34
    371   w51 = ssig1 w49 + w44 + ssig0 w36 + w35
    372   w52 = ssig1 w50 + w45 + ssig0 w37 + w36
    373   w53 = ssig1 w51 + w46 + ssig0 w38 + w37
    374   w54 = ssig1 w52 + w47 + ssig0 w39 + w38
    375   w55 = ssig1 w53 + w48 + ssig0 w40 + w39
    376   w56 = ssig1 w54 + w49 + ssig0 w41 + w40
    377   w57 = ssig1 w55 + w50 + ssig0 w42 + w41
    378   w58 = ssig1 w56 + w51 + ssig0 w43 + w42
    379   w59 = ssig1 w57 + w52 + ssig0 w44 + w43
    380   w60 = ssig1 w58 + w53 + ssig0 w45 + w44
    381   w61 = ssig1 w59 + w54 + ssig0 w46 + w45
    382   w62 = ssig1 w60 + w55 + ssig0 w47 + w46
    383   w63 = ssig1 w61 + w56 + ssig0 w48 + w47
    384   w64 = ssig1 w62 + w57 + ssig0 w49 + w48
    385   w65 = ssig1 w63 + w58 + ssig0 w50 + w49
    386   w66 = ssig1 w64 + w59 + ssig0 w51 + w50
    387   w67 = ssig1 w65 + w60 + ssig0 w52 + w51
    388   w68 = ssig1 w66 + w61 + ssig0 w53 + w52
    389   w69 = ssig1 w67 + w62 + ssig0 w54 + w53
    390   w70 = ssig1 w68 + w63 + ssig0 w55 + w54
    391   w71 = ssig1 w69 + w64 + ssig0 w56 + w55
    392   w72 = ssig1 w70 + w65 + ssig0 w57 + w56
    393   w73 = ssig1 w71 + w66 + ssig0 w58 + w57
    394   w74 = ssig1 w72 + w67 + ssig0 w59 + w58
    395   w75 = ssig1 w73 + w68 + ssig0 w60 + w59
    396   w76 = ssig1 w74 + w69 + ssig0 w61 + w60
    397   w77 = ssig1 w75 + w70 + ssig0 w62 + w61
    398   w78 = ssig1 w76 + w71 + ssig0 w63 + w62
    399   w79 = ssig1 w77 + w72 + ssig0 w64 + w63
    400 
    401 -- RFC 6234 6.2 steps 2, 3, 4
    402 block_hash :: Registers -> Schedule -> Registers
    403 block_hash r00@Registers {..} Schedule {..} =
    404   -- constants are the first 64 bits of the fractional parts of the
    405   -- cube roots of the first eighty prime numbers
    406   let r01 = step r00 0x428a2f98d728ae22 w00
    407       r02 = step r01 0x7137449123ef65cd w01
    408       r03 = step r02 0xb5c0fbcfec4d3b2f w02
    409       r04 = step r03 0xe9b5dba58189dbbc w03
    410       r05 = step r04 0x3956c25bf348b538 w04
    411       r06 = step r05 0x59f111f1b605d019 w05
    412       r07 = step r06 0x923f82a4af194f9b w06
    413       r08 = step r07 0xab1c5ed5da6d8118 w07
    414       r09 = step r08 0xd807aa98a3030242 w08
    415       r10 = step r09 0x12835b0145706fbe w09
    416       r11 = step r10 0x243185be4ee4b28c w10
    417       r12 = step r11 0x550c7dc3d5ffb4e2 w11
    418       r13 = step r12 0x72be5d74f27b896f w12
    419       r14 = step r13 0x80deb1fe3b1696b1 w13
    420       r15 = step r14 0x9bdc06a725c71235 w14
    421       r16 = step r15 0xc19bf174cf692694 w15
    422       r17 = step r16 0xe49b69c19ef14ad2 w16
    423       r18 = step r17 0xefbe4786384f25e3 w17
    424       r19 = step r18 0x0fc19dc68b8cd5b5 w18
    425       r20 = step r19 0x240ca1cc77ac9c65 w19
    426       r21 = step r20 0x2de92c6f592b0275 w20
    427       r22 = step r21 0x4a7484aa6ea6e483 w21
    428       r23 = step r22 0x5cb0a9dcbd41fbd4 w22
    429       r24 = step r23 0x76f988da831153b5 w23
    430       r25 = step r24 0x983e5152ee66dfab w24
    431       r26 = step r25 0xa831c66d2db43210 w25
    432       r27 = step r26 0xb00327c898fb213f w26
    433       r28 = step r27 0xbf597fc7beef0ee4 w27
    434       r29 = step r28 0xc6e00bf33da88fc2 w28
    435       r30 = step r29 0xd5a79147930aa725 w29
    436       r31 = step r30 0x06ca6351e003826f w30
    437       r32 = step r31 0x142929670a0e6e70 w31
    438       r33 = step r32 0x27b70a8546d22ffc w32
    439       r34 = step r33 0x2e1b21385c26c926 w33
    440       r35 = step r34 0x4d2c6dfc5ac42aed w34
    441       r36 = step r35 0x53380d139d95b3df w35
    442       r37 = step r36 0x650a73548baf63de w36
    443       r38 = step r37 0x766a0abb3c77b2a8 w37
    444       r39 = step r38 0x81c2c92e47edaee6 w38
    445       r40 = step r39 0x92722c851482353b w39
    446       r41 = step r40 0xa2bfe8a14cf10364 w40
    447       r42 = step r41 0xa81a664bbc423001 w41
    448       r43 = step r42 0xc24b8b70d0f89791 w42
    449       r44 = step r43 0xc76c51a30654be30 w43
    450       r45 = step r44 0xd192e819d6ef5218 w44
    451       r46 = step r45 0xd69906245565a910 w45
    452       r47 = step r46 0xf40e35855771202a w46
    453       r48 = step r47 0x106aa07032bbd1b8 w47
    454       r49 = step r48 0x19a4c116b8d2d0c8 w48
    455       r50 = step r49 0x1e376c085141ab53 w49
    456       r51 = step r50 0x2748774cdf8eeb99 w50
    457       r52 = step r51 0x34b0bcb5e19b48a8 w51
    458       r53 = step r52 0x391c0cb3c5c95a63 w52
    459       r54 = step r53 0x4ed8aa4ae3418acb w53
    460       r55 = step r54 0x5b9cca4f7763e373 w54
    461       r56 = step r55 0x682e6ff3d6b2b8a3 w55
    462       r57 = step r56 0x748f82ee5defb2fc w56
    463       r58 = step r57 0x78a5636f43172f60 w57
    464       r59 = step r58 0x84c87814a1f0ab72 w58
    465       r60 = step r59 0x8cc702081a6439ec w59
    466       r61 = step r60 0x90befffa23631e28 w60
    467       r62 = step r61 0xa4506cebde82bde9 w61
    468       r63 = step r62 0xbef9a3f7b2c67915 w62
    469       r64 = step r63 0xc67178f2e372532b w63
    470       r65 = step r64 0xca273eceea26619c w64
    471       r66 = step r65 0xd186b8c721c0c207 w65
    472       r67 = step r66 0xeada7dd6cde0eb1e w66
    473       r68 = step r67 0xf57d4f7fee6ed178 w67
    474       r69 = step r68 0x06f067aa72176fba w68
    475       r70 = step r69 0x0a637dc5a2c898a6 w69
    476       r71 = step r70 0x113f9804bef90dae w70
    477       r72 = step r71 0x1b710b35131c471b w71
    478       r73 = step r72 0x28db77f523047d84 w72
    479       r74 = step r73 0x32caab7b40c72493 w73
    480       r75 = step r74 0x3c9ebe0a15c9bebc w74
    481       r76 = step r75 0x431d67c49c100d4c w75
    482       r77 = step r76 0x4cc5d4becb3e42b6 w76
    483       r78 = step r77 0x597f299cfc657e2a w77
    484       r79 = step r78 0x5fcb6fab3ad6faec w78
    485       r80 = step r79 0x6c44198c4a475817 w79
    486       !(Registers a b c d e f g h) = r80
    487   in  Registers
    488         (a + h0) (b + h1) (c + h2) (d + h3)
    489         (e + h4) (f + h5) (g + h6) (h + h7)
    490 
    491 step :: Registers -> Word64 -> Word64 -> Registers
    492 step (Registers a b c d e f g h) k w =
    493   let t1 = h + bsig1 e + ch e f g + k + w
    494       t2 = bsig0 a + maj a b c
    495   in  Registers (t1 + t2) a b c (d + t1) e f g
    496 {-# INLINE step #-}
    497 
    498 -- RFC 6234 6.2 block pipeline
    499 --
    500 -- invariant:
    501 --   the input bytestring is exactly 1024 bits in length
    502 unsafe_hash_alg :: Registers -> BS.ByteString -> Registers
    503 unsafe_hash_alg rs bs = block_hash rs (prepare_schedule (unsafe_parse bs))
    504 
    505 -- register concatenation
    506 cat :: Registers -> BS.ByteString
    507 cat Registers {..} = to_strict_small $
    508      BSB.word64BE h0 <> BSB.word64BE h1 <> BSB.word64BE h2 <> BSB.word64BE h3
    509   <> BSB.word64BE h4 <> BSB.word64BE h5 <> BSB.word64BE h6 <> BSB.word64BE h7
    510 
    511 -- | Compute a condensed representation of a strict bytestring via
    512 --   SHA-512.
    513 --
    514 --   The 512-bit output digest is returned as a strict bytestring.
    515 --
    516 --   >>> hash "strict bytestring input"
    517 --   "<strict 512-bit message digest>"
    518 hash :: BS.ByteString -> BS.ByteString
    519 hash bs = cat (go iv (pad bs)) where
    520   -- proof that 'go' always terminates safely:
    521   --
    522   -- let b = pad bs
    523   -- then length(b) = n * 1024 bits for some n >= 0                 (1)
    524   go :: Registers -> BS.ByteString -> Registers
    525   go !acc b
    526     -- if n == 0, then 'go' terminates safely                       (2)
    527     | BS.null b = acc
    528     -- if n > 0, then
    529     --
    530     -- let (c, r) = unsafe_splitAt 128 b
    531     -- then length(c) == 1024 bits                                  by (1)
    532     --      length(r) == m * 1024 bits for some m >= 0              by (1)
    533     --
    534     -- note 'unsafe_hash_alg' terminates safely for bytestring      (3)
    535     -- input of exactly 1024 bits in length
    536     --
    537     -- length(c) == 1024
    538     --   => 'unsafe_hash_alg' terminates safely                     by (3)
    539     --   => 'go' terminates safely                                  (4)
    540     -- length(r) == m * 1024 bits for m >= 0
    541     --   => next invocation of 'go' terminates safely               by (2), (4)
    542     --
    543     -- then by induction, 'go' always terminates safely (QED)
    544     | otherwise = case unsafe_splitAt 128 b of
    545         SSPair c r -> go (unsafe_hash_alg acc c) r
    546 
    547 -- | Compute a condensed representation of a lazy bytestring via
    548 --   SHA-512.
    549 --
    550 --   The 512-bit output digest is returned as a strict bytestring.
    551 --
    552 --   >>> hash_lazy "lazy bytestring input"
    553 --   "<strict 512-bit message digest>"
    554 hash_lazy :: BL.ByteString -> BS.ByteString
    555 hash_lazy bl = cat (go iv (pad_lazy bl)) where
    556   -- proof of safety proceeds analogously
    557   go :: Registers -> BL.ByteString -> Registers
    558   go !acc bs
    559     | BL.null bs = acc
    560     | otherwise = case splitAt128 bs of
    561         SLPair c r -> go (unsafe_hash_alg acc c) r
    562 
    563 -- HMAC -----------------------------------------------------------------------
    564 -- https://datatracker.ietf.org/doc/html/rfc2104#section-2
    565 
    566 data KeyAndLen = KeyAndLen
    567   {-# UNPACK #-} !BS.ByteString
    568   {-# UNPACK #-} !Int
    569 
    570 -- | Produce a message authentication code for a strict bytestring,
    571 --   based on the provided (strict, bytestring) key, via SHA-512.
    572 --
    573 --   The 512-bit MAC is returned as a strict bytestring.
    574 --
    575 --   Per RFC 2104, the key /should/ be a minimum of 64 bytes long. Keys
    576 --   exceeding 1024 bytes in length will first be hashed (via SHA-512).
    577 --
    578 --   >>> hmac "strict bytestring key" "strict bytestring input"
    579 --   "<strict 512-bit MAC>"
    580 hmac
    581   :: BS.ByteString -- ^ key
    582   -> BS.ByteString -- ^ text
    583   -> BS.ByteString
    584 hmac mk@(BI.PS _ _ l) text =
    585     let step1 = k <> BS.replicate (128 - lk) 0x00
    586         step2 = BS.map (B.xor 0x36) step1
    587         step3 = step2 <> text
    588         step4 = hash step3
    589         step5 = BS.map (B.xor 0x5C) step1
    590         step6 = step5 <> step4
    591     in  hash step6
    592   where
    593     !(KeyAndLen k lk)
    594       | l > 128   = KeyAndLen (hash mk) 64
    595       | otherwise = KeyAndLen mk l
    596 
    597 -- | Produce a message authentication code for a lazy bytestring, based
    598 --   on the provided (strict, bytestring) key, via SHA-512.
    599 --
    600 --   The 512-bit MAC is returned as a strict bytestring.
    601 --
    602 --   Per RFC 2104, the key /should/ be a minimum of 64 bytes long. Keys
    603 --   exceeding 1024 bytes in length will first be hashed (via SHA-512).
    604 --
    605 --   >>> hmac_lazy "strict bytestring key" "lazy bytestring input"
    606 --   "<strict 512-bit MAC>"
    607 hmac_lazy
    608   :: BS.ByteString -- ^ key
    609   -> BL.ByteString -- ^ text
    610   -> BS.ByteString
    611 hmac_lazy mk@(BI.PS _ _ l) text =
    612     let step1 = k <> BS.replicate (128 - lk) 0x00
    613         step2 = BS.map (B.xor 0x36) step1
    614         step3 = BL.fromStrict step2 <> text
    615         step4 = hash_lazy step3
    616         step5 = BS.map (B.xor 0x5C) step1
    617         step6 = step5 <> step4
    618     in  hash step6
    619   where
    620     !(KeyAndLen k lk)
    621       | l > 128   = KeyAndLen (hash mk) 64
    622       | otherwise = KeyAndLen mk l
    623