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


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