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 (21110B)


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