{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module ZkFold.Symbolic.Algorithms.Hash.SHA2
    ( AlgorithmSetup (..)
    , SHA2
    , sha2
    , sha2Var
    , SHA2N
    , sha2Natural
    , PaddedLength
    ) where

import           Control.DeepSeq                                (NFData, force)
import           Control.Monad                                  (forM_)
import           Control.Monad.ST                               (ST, runST)
import           Data.Bits                                      (shiftL)
import           Data.Constraint
import           Data.Constraint.Nat
import           Data.Constraint.Unsafe
import           Data.Kind                                      (Type)
import qualified Data.STRef                                     as ST
import           Data.Type.Bool                                 (If)
import           Data.Type.Equality                             (type (~))
import qualified Data.Vector                                    as V
import qualified Data.Vector.Mutable                            as VM
import           GHC.Generics                                   (Par1 (..))
import           GHC.TypeLits                                   (Symbol)
import           GHC.TypeNats                                   (type (<=?), withKnownNat)
import           Prelude                                        (Int, id, pure, zip, ($!), ($), (.), (>>=))
import qualified Prelude                                        as P

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.HFunctor                      (hmap)
import           ZkFold.Base.Data.Vector                        (Vector (..), fromVector, reverse, unsafeToVector)
import           ZkFold.Symbolic.Algorithms.Hash.SHA2.Constants (sha224InitialHashes, sha256InitialHashes,
                                                                 sha384InitialHashes, sha512InitialHashes,
                                                                 sha512_224InitialHashes, sha512_256InitialHashes,
                                                                 word32RoundConstants, word64RoundConstants)
import           ZkFold.Symbolic.Class                          (BaseField, Symbolic, fromCircuitF)
import           ZkFold.Symbolic.Data.Bool                      (Bool (..), BoolType (..))
import           ZkFold.Symbolic.Data.ByteString                (ByteString (..), ShiftBits (..), concat, set, toWords,
                                                                 truncate)
import           ZkFold.Symbolic.Data.Combinators               (Iso (..), RegisterSize (..), Resize (..), expansionW,
                                                                 ilog2)
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.FieldElement              (FieldElement (..))
import           ZkFold.Symbolic.Data.Ord
import           ZkFold.Symbolic.Data.UInt                      (UInt)
import qualified ZkFold.Symbolic.Data.VarByteString             as VB
import           ZkFold.Symbolic.Data.VarByteString             (VarByteString (..))
import           ZkFold.Symbolic.MonadCircuit                   (newAssigned)


-- | SHA2 is a family of hashing functions with almost identical implementations but different constants and parameters.
-- This class links these varying parts with the appropriate algorithm.
--
class
    (Symbolic context
    , NFData (context (Vector (WordSize algorithm)))
    , KnownNat (ChunkSize algorithm)
    , KnownNat (WordSize algorithm)
    , Mod (ChunkSize algorithm) (WordSize algorithm) ~ 0
    , Div (ChunkSize algorithm) (WordSize algorithm) * WordSize algorithm ~ ChunkSize algorithm
    , (Div (8 * (WordSize algorithm)) (WordSize algorithm)) * (WordSize algorithm) ~ 8 * (WordSize algorithm)
    ) => AlgorithmSetup (algorithm :: Symbol) (context :: (Type -> Type) -> Type) where
    type WordSize algorithm :: Natural
    -- ^ The length of words the algorithm operates internally, in bits.

    type ChunkSize algorithm :: Natural
    -- ^ Hashing algorithms from SHA2 family require splitting the input message into blocks.
    -- This type describes the size of these blocks, in bits.

    type ResultSize algorithm :: Natural
    -- ^ The length of the resulting hash, in bits.

    initialHashes :: V.Vector (ByteString (WordSize algorithm) context)
    -- ^ Initial hash values which will be mixed with the message bits.

    roundConstants :: V.Vector (ByteString (WordSize algorithm) context)
    -- ^ Constants used in the internal loop, one per each round.

    truncateResult :: ByteString (8 * WordSize algorithm) context -> ByteString (ResultSize algorithm) context
    -- ^ A function to postprocess the hash. For example, SHA224 requires dropping the last 32 bits of a SHA256 hash.

    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
    -- ^ Round rotation values for Sigma in the internal loop.

    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
    -- ^ Round rotation values for Sum in the internal loop.

instance
    (Symbolic c
    , NFData (c (Vector (WordSize "SHA256")))
    ) => AlgorithmSetup "SHA256" c where
    type WordSize "SHA256" = 32
    type ChunkSize "SHA256" = 512
    type ResultSize "SHA256" = 256
    initialHashes :: Vector (ByteString (WordSize "SHA256") c)
initialHashes = Vector (ByteString 32 c)
Vector (ByteString (WordSize "SHA256") c)
forall a. FromConstant Natural a => Vector a
sha256InitialHashes
    roundConstants :: Vector (ByteString (WordSize "SHA256") c)
roundConstants = Vector (ByteString 32 c)
Vector (ByteString (WordSize "SHA256") c)
forall a. FromConstant Natural a => Vector a
word32RoundConstants
    truncateResult :: ByteString (8 * WordSize "SHA256") c
-> ByteString (ResultSize "SHA256") c
truncateResult = ByteString 256 c -> ByteString 256 c
ByteString (8 * WordSize "SHA256") c
-> ByteString (ResultSize "SHA256") c
forall a. a -> a
id
    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts = (Natural
7, Natural
18, Natural
3, Natural
17, Natural
19, Natural
10)
    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts = (Natural
2, Natural
13, Natural
22, Natural
6, Natural
11, Natural
25)


instance
    (Symbolic c
    , NFData (c (Vector (WordSize "SHA224")))
    ) => AlgorithmSetup "SHA224" c where
    type WordSize "SHA224" = 32
    type ChunkSize "SHA224" = 512
    type ResultSize "SHA224" = 224
    initialHashes :: Vector (ByteString (WordSize "SHA224") c)
initialHashes = Vector (ByteString 32 c)
Vector (ByteString (WordSize "SHA224") c)
forall a. FromConstant Natural a => Vector a
sha224InitialHashes
    roundConstants :: Vector (ByteString (WordSize "SHA224") c)
roundConstants = Vector (ByteString 32 c)
Vector (ByteString (WordSize "SHA224") c)
forall a. FromConstant Natural a => Vector a
word32RoundConstants
    truncateResult :: ByteString (8 * WordSize "SHA224") c
-> ByteString (ResultSize "SHA224") c
truncateResult = ByteString 256 c -> ByteString 224 c
ByteString (8 * WordSize "SHA224") c
-> ByteString (ResultSize "SHA224") c
forall (m :: Natural) (n :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat n, n <= m) =>
ByteString m c -> ByteString n c
truncate
    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts = (Natural
7, Natural
18, Natural
3, Natural
17, Natural
19, Natural
10)
    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts = (Natural
2, Natural
13, Natural
22, Natural
6, Natural
11, Natural
25)

instance
    (Symbolic c
    , NFData (c (Vector (WordSize "SHA512")))
    )  => AlgorithmSetup "SHA512" c where
    type WordSize "SHA512" = 64
    type ChunkSize "SHA512" = 1024
    type ResultSize "SHA512" = 512
    initialHashes :: Vector (ByteString (WordSize "SHA512") c)
initialHashes = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA512") c)
forall a. FromConstant Natural a => Vector a
sha512InitialHashes
    roundConstants :: Vector (ByteString (WordSize "SHA512") c)
roundConstants = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA512") c)
forall a. FromConstant Natural a => Vector a
word64RoundConstants
    truncateResult :: ByteString (8 * WordSize "SHA512") c
-> ByteString (ResultSize "SHA512") c
truncateResult = ByteString 512 c -> ByteString 512 c
ByteString (8 * WordSize "SHA512") c
-> ByteString (ResultSize "SHA512") c
forall a. a -> a
id
    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts = (Natural
1, Natural
8, Natural
7, Natural
19, Natural
61, Natural
6)
    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts = (Natural
28, Natural
34, Natural
39, Natural
14, Natural
18, Natural
41)

instance
    (Symbolic c
    , NFData (c (Vector (WordSize "SHA384")))
    ) => AlgorithmSetup "SHA384" c where
    type WordSize "SHA384" = 64
    type ChunkSize "SHA384" = 1024
    type ResultSize "SHA384" = 384
    initialHashes :: Vector (ByteString (WordSize "SHA384") c)
initialHashes = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA384") c)
forall a. FromConstant Natural a => Vector a
sha384InitialHashes
    roundConstants :: Vector (ByteString (WordSize "SHA384") c)
roundConstants = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA384") c)
forall a. FromConstant Natural a => Vector a
word64RoundConstants
    truncateResult :: ByteString (8 * WordSize "SHA384") c
-> ByteString (ResultSize "SHA384") c
truncateResult = ByteString 512 c -> ByteString 384 c
ByteString (8 * WordSize "SHA384") c
-> ByteString (ResultSize "SHA384") c
forall (m :: Natural) (n :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat n, n <= m) =>
ByteString m c -> ByteString n c
truncate
    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts = (Natural
1, Natural
8, Natural
7, Natural
19, Natural
61, Natural
6)
    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts = (Natural
28, Natural
34, Natural
39, Natural
14, Natural
18, Natural
41)

instance
    (Symbolic c
    , NFData (c (Vector (WordSize "SHA512/224")))
    ) => AlgorithmSetup "SHA512/224" c where
    type WordSize "SHA512/224" = 64
    type ChunkSize "SHA512/224" = 1024
    type ResultSize "SHA512/224" = 224
    initialHashes :: Vector (ByteString (WordSize "SHA512/224") c)
initialHashes = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA512/224") c)
forall a. FromConstant Natural a => Vector a
sha512_224InitialHashes
    roundConstants :: Vector (ByteString (WordSize "SHA512/224") c)
roundConstants = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA512/224") c)
forall a. FromConstant Natural a => Vector a
word64RoundConstants
    truncateResult :: ByteString (8 * WordSize "SHA512/224") c
-> ByteString (ResultSize "SHA512/224") c
truncateResult = ByteString 512 c -> ByteString 224 c
ByteString (8 * WordSize "SHA512/224") c
-> ByteString (ResultSize "SHA512/224") c
forall (m :: Natural) (n :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat n, n <= m) =>
ByteString m c -> ByteString n c
truncate
    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts = (Natural
1, Natural
8, Natural
7, Natural
19, Natural
61, Natural
6)
    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts = (Natural
28, Natural
34, Natural
39, Natural
14, Natural
18, Natural
41)

instance
    (Symbolic c
    , NFData (c (Vector (WordSize "SHA512/256" )))
    ) => AlgorithmSetup "SHA512/256" c where
    type WordSize "SHA512/256" = 64
    type ChunkSize "SHA512/256" = 1024
    type ResultSize "SHA512/256" = 256
    initialHashes :: Vector (ByteString (WordSize "SHA512/256") c)
initialHashes = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA512/256") c)
forall a. FromConstant Natural a => Vector a
sha512_256InitialHashes
    roundConstants :: Vector (ByteString (WordSize "SHA512/256") c)
roundConstants = Vector (ByteString 64 c)
Vector (ByteString (WordSize "SHA512/256") c)
forall a. FromConstant Natural a => Vector a
word64RoundConstants
    truncateResult :: ByteString (8 * WordSize "SHA512/256") c
-> ByteString (ResultSize "SHA512/256") c
truncateResult = ByteString 512 c -> ByteString 256 c
ByteString (8 * WordSize "SHA512/256") c
-> ByteString (ResultSize "SHA512/256") c
forall (m :: Natural) (n :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat n, n <= m) =>
ByteString m c -> ByteString n c
truncate
    sigmaShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts = (Natural
1, Natural
8, Natural
7, Natural
19, Natural
61, Natural
6)
    sumShifts :: (Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts = (Natural
28, Natural
34, Natural
39, Natural
14, Natural
18, Natural
41)

-- | On type level, determine the smallest multiple of @divisor@ not less than @n@.
--
type family NextMultiple (n :: Natural) (divisor :: Natural) :: Natural where
    NextMultiple n divisor = divisor * Div (n + divisor - 1) divisor

{- | On type level, determine the length of the message after padding.
    Padding algorithm is described below:

    1. begin with the original message of length L bits
    2. append a single '1' bit
    3. append K '0' bits, where K is the minimum number >= 0 such that (L + 1 + K + 64) is a multiple of 512
    4. append L as a 64-bit big-endian integer, making the total post-processed length a multiple of 512 bits

    such that the bits in the message are: <original message of length L> 1 <K zeros> <L as 64 bit integer>

    For SHA384, SHA512 and SHA512/t, replace 512 with 1024 and 64 with 128.
-}
type family PaddedLength (msg :: Natural) (block :: Natural) (lenBits :: Natural) :: Natural where
    PaddedLength msg block lenBits = If (NextMultiple msg block - msg <=? lenBits) (block + NextMultiple msg block) (NextMultiple msg block)

paddedLen :: Natural -> Natural -> Natural ->  Natural
paddedLen :: Natural -> Natural -> Natural -> Natural
paddedLen Natural
m Natural
b Natural
l = if Natural -> Natural -> Natural
nextMultiple Natural
m Natural
b Natural -> Natural -> Natural
-! Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
P.<= Natural
l
    then Natural
b Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> Natural -> Natural
nextMultiple Natural
m Natural
b
    else Natural -> Natural -> Natural
nextMultiple Natural
m Natural
b
    where
        nextMultiple :: Natural -> Natural -> Natural
        nextMultiple :: Natural -> Natural -> Natural
nextMultiple Natural
n Natural
d = Natural
d Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
div (Natural
n Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
d Natural -> Natural -> Natural
-! Natural
1) Natural
d

withPaddedLength' :: forall m b l. (KnownNat m, KnownNat b, KnownNat l) :- KnownNat (PaddedLength m b l)
withPaddedLength' :: forall (m :: Natural) (b :: Natural) (l :: Natural).
(KnownNat m, KnownNat b, KnownNat l)
:- KnownNat (PaddedLength m b l)
withPaddedLength' = ((KnownNat m, KnownNat b, KnownNat l) =>
 Dict (KnownNat (PaddedLength m b l)))
-> (KnownNat m, KnownNat b, KnownNat l)
   :- KnownNat (PaddedLength m b l)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((KnownNat m, KnownNat b, KnownNat l) =>
  Dict (KnownNat (PaddedLength m b l)))
 -> (KnownNat m, KnownNat b, KnownNat l)
    :- KnownNat (PaddedLength m b l))
-> ((KnownNat m, KnownNat b, KnownNat l) =>
    Dict (KnownNat (PaddedLength m b l)))
-> (KnownNat m, KnownNat b, KnownNat l)
   :- KnownNat (PaddedLength m b l)
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
withKnownNat @(PaddedLength m b l) (Natural
-> SNat
     (If
        (OrdCond
           (CmpNat ((b * Div ((m + b) - 1) b) - m) l) 'True 'True 'False)
        (b + (b * Div ((m + b) - 1) b))
        (b * Div ((m + b) - 1) b))
forall (n :: Natural). Natural -> SNat n
unsafeSNat (Natural -> Natural -> Natural -> Natural
paddedLen (forall (n :: Natural). KnownNat n => Natural
value @m) (forall (n :: Natural). KnownNat n => Natural
value @b) (forall (n :: Natural). KnownNat n => Natural
value @l))) Dict
  (KnownNat
     (If
        (OrdCond
           (CmpNat ((b * Div ((m + b) - 1) b) - m) l) 'True 'True 'False)
        (b + (b * Div ((m + b) - 1) b))
        (b * Div ((m + b) - 1) b)))
KnownNat (PaddedLength m b l) =>
Dict
  (KnownNat
     (If
        (OrdCond
           (CmpNat ((b * Div ((m + b) - 1) b) - m) l) 'True 'True 'False)
        (b + (b * Div ((m + b) - 1) b))
        (b * Div ((m + b) - 1) b)))
forall (a :: Constraint). a => Dict a
Dict

withPaddedLength :: forall n d l {r}. ( KnownNat d, KnownNat n, KnownNat l) => (KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength :: forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength = ((KnownNat n, KnownNat d, KnownNat l)
 :- KnownNat
      (If
         (OrdCond
            (CmpNat ((d * Div ((n + d) - 1) d) - n) l) 'True 'True 'False)
         (d + (d * Div ((n + d) - 1) d))
         (d * Div ((n + d) - 1) d)))
-> (KnownNat
      (If
         (OrdCond
            (CmpNat ((d * Div ((n + d) - 1) d) - n) l) 'True 'True 'False)
         (d + (d * Div ((n + d) - 1) d))
         (d * Div ((n + d) - 1) d)) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (m :: Natural) (b :: Natural) (l :: Natural).
(KnownNat m, KnownNat b, KnownNat l)
:- KnownNat (PaddedLength m b l)
withPaddedLength' @n @d @l)

modPaddedLength :: forall k algorithm. Dict (Mod (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) (ChunkSize algorithm) ~ 0)
modPaddedLength :: forall (k :: Natural) (algorithm :: Symbol).
Dict
  (Mod
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)
   ~ 0)
modPaddedLength = Dict
  (Mod
     (If
        (OrdCond
           (CmpNat
              ((ChunkSize algorithm
                * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))
               - k)
              (2 * WordSize algorithm))
           'True
           'True
           'False)
        (ChunkSize algorithm
         + (ChunkSize algorithm
            * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
        (ChunkSize algorithm
         * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
     (ChunkSize algorithm)
   ~ 0)
Dict
  (Mod
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)
   ~ 0)
forall (c :: Constraint). Dict c
unsafeAxiom

withModPaddedLength :: forall k algorithm {r}. (Mod (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) (ChunkSize algorithm) ~ 0 => r) -> r
withModPaddedLength :: forall (k :: Natural) (algorithm :: Symbol) {r}.
((Mod
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    (ChunkSize algorithm)
  ~ 0) =>
 r)
-> r
withModPaddedLength = Dict
  (Mod
     (If
        (OrdCond
           (CmpNat
              ((ChunkSize algorithm
                * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))
               - k)
              (2 * WordSize algorithm))
           'True
           'True
           'False)
        (ChunkSize algorithm
         + (ChunkSize algorithm
            * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
        (ChunkSize algorithm
         * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
     (ChunkSize algorithm)
   ~ 0)
-> ((Mod
       (If
          (OrdCond
             (CmpNat
                ((ChunkSize algorithm
                  * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))
                 - k)
                (2 * WordSize algorithm))
             'True
             'True
             'False)
          (ChunkSize algorithm
           + (ChunkSize algorithm
              * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
          (ChunkSize algorithm
           * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
       (ChunkSize algorithm)
     ~ 0) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (k :: Natural) (algorithm :: Symbol).
Dict
  (Mod
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)
   ~ 0)
modPaddedLength @k @algorithm)

kLessPaddedLength :: forall k algorithm. Dict (k <= PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
kLessPaddedLength :: forall (k :: Natural) (algorithm :: Symbol).
Dict
  (k
   <= PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
kLessPaddedLength = Dict
  (Assert
     (OrdCond
        (CmpNat
           k
           (If
              (OrdCond
                 (CmpNat
                    ((ChunkSize algorithm
                      * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))
                     - k)
                    (2 * WordSize algorithm))
                 'True
                 'True
                 'False)
              (ChunkSize algorithm
               + (ChunkSize algorithm
                  * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
              (ChunkSize algorithm
               * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))))
        'True
        'True
        'False)
     (TypeError ...))
Dict
  (Assert
     (OrdCond
        (Compare
           k (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)))
        'True
        'True
        'False)
     (TypeError ...))
forall (c :: Constraint). Dict c
unsafeAxiom

withKLessPaddedLength :: forall k algorithm {r}. (k <= PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm) => r) -> r
withKLessPaddedLength :: forall (k :: Natural) (algorithm :: Symbol) {r}.
((k
  <= PaddedLength
       k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
 r)
-> r
withKLessPaddedLength = Dict
  (Assert
     (OrdCond
        (CmpNat
           k
           (If
              (OrdCond
                 (CmpNat
                    ((ChunkSize algorithm
                      * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))
                     - k)
                    (2 * WordSize algorithm))
                 'True
                 'True
                 'False)
              (ChunkSize algorithm
               + (ChunkSize algorithm
                  * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
              (ChunkSize algorithm
               * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))))
        'True
        'True
        'False)
     (TypeError ...))
-> (Assert
      (OrdCond
         (CmpNat
            k
            (If
               (OrdCond
                  (CmpNat
                     ((ChunkSize algorithm
                       * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))
                      - k)
                     (2 * WordSize algorithm))
                  'True
                  'True
                  'False)
               (ChunkSize algorithm
                + (ChunkSize algorithm
                   * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm)))
               (ChunkSize algorithm
                * Div ((k + ChunkSize algorithm) - 1) (ChunkSize algorithm))))
         'True
         'True
         'False)
      (TypeError ...) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (k :: Natural) (algorithm :: Symbol).
Dict
  (k
   <= PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
kLessPaddedLength @k @algorithm)

divisibleDiv :: forall a b. (Mod a b ~ 0) :- (Div a b * b ~ a)
divisibleDiv :: forall (a :: Natural) (b :: Natural).
(Mod a b ~ 0) :- ((Div a b * b) ~ a)
divisibleDiv = ((Mod a b ~ 0) => Dict ((Div a b * b) ~ a))
-> (Mod a b ~ 0) :- ((Div a b * b) ~ a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict ((Div a b * b) ~ a)
(Mod a b ~ 0) => Dict ((Div a b * b) ~ a)
forall (c :: Constraint). Dict c
unsafeAxiom

withDivisibleDiv :: forall a b {r}. Mod a b ~ 0 => ((Div a b * b ~ a) => r) -> r
withDivisibleDiv :: forall (a :: Natural) (b :: Natural) {r}.
(Mod a b ~ 0) =>
(((Div a b * b) ~ a) => r) -> r
withDivisibleDiv = ((0 ~ 0) :- ((Div a b * b) ~ a)) -> (((Div a b * b) ~ a) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Natural) (b :: Natural).
(Mod a b ~ 0) :- ((Div a b * b) ~ a)
divisibleDiv @a @b)

-- | Constraints required for a type-safe SHA2
--
type SHA2 algorithm context k = (AlgorithmSetup algorithm context, KnownNat k)

-- | A generalised version of SHA2. It is agnostic of the ByteString base field.
-- Sample usage:
--
-- >>> bs = fromConstant (42 :: Natural) :: ByteString 8 (Zp BLS12_381_Scalar)
-- >>> hash = sha2 @"SHA256" bs
--

sha2
    :: forall (algorithm :: Symbol) context k {d}
    .  SHA2 algorithm context k
    => d ~ Div (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) (ChunkSize algorithm)
    => ByteString k context -> ByteString (ResultSize algorithm) context
sha2 :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type)
       (k :: Natural) {d :: Natural}.
(SHA2 algorithm context k,
 d
 ~ Div
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)) =>
ByteString k context -> ByteString (ResultSize algorithm) context
sha2 ByteString k context
messageBits = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
[ByteString (ChunkSize algorithm) context]
-> ByteString (ResultSize algorithm) context
sha2Blocks @algorithm @context (Vector d (ByteString (ChunkSize algorithm) context)
-> [ByteString (ChunkSize algorithm) context]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector d (ByteString (ChunkSize algorithm) context)
chunks)
    where
        paddedMessage :: ByteString (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) context
        paddedMessage :: ByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
paddedMessage = ((KnownNat 2, KnownNat (WordSize algorithm))
 :- KnownNat (2 * WordSize algorithm))
-> (KnownNat (2 * WordSize algorithm) =>
    ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> ByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat @2 @(WordSize algorithm)) ((KnownNat (2 * WordSize algorithm) =>
  ByteString
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    context)
 -> ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> (KnownNat (2 * WordSize algorithm) =>
    ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> ByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @(ChunkSize algorithm) @(2 * WordSize algorithm) ((KnownNat
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
  ByteString
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    context)
 -> ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> (KnownNat
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
    ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> ByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall a b. (a -> b) -> a -> b
$
                            forall (k :: Natural) (algorithm :: Symbol) {r}.
((k
  <= PaddedLength
       k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
 r)
-> r
withKLessPaddedLength @k @algorithm (((k
   <= PaddedLength
        k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
  ByteString
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    context)
 -> ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> ((k
     <= PaddedLength
          k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
    ByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> ByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall a b. (a -> b) -> a -> b
$
                                forall (padTo :: Natural) (lenBits :: Natural)
       (context :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic context, KnownNat k, KnownNat padTo, KnownNat lenBits) =>
ByteString k context
-> ByteString (PaddedLength k padTo lenBits) context
sha2Pad @(ChunkSize algorithm) @(2 * WordSize algorithm) ByteString k context
messageBits

        chunks :: Vector d (ByteString (ChunkSize algorithm) context)
        chunks :: Vector d (ByteString (ChunkSize algorithm) context)
chunks = forall (k :: Natural) (algorithm :: Symbol) {r}.
((Mod
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    (ChunkSize algorithm)
  ~ 0) =>
 r)
-> r
withModPaddedLength @k @algorithm (((Mod
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)
   ~ 0) =>
  Vector d (ByteString (ChunkSize algorithm) context))
 -> Vector d (ByteString (ChunkSize algorithm) context))
-> ((Mod
       (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
       (ChunkSize algorithm)
     ~ 0) =>
    Vector d (ByteString (ChunkSize algorithm) context))
-> Vector d (ByteString (ChunkSize algorithm) context)
forall a b. (a -> b) -> a -> b
$
                    forall (a :: Natural) (b :: Natural) {r}.
(Mod a b ~ 0) =>
(((Div a b * b) ~ a) => r) -> r
withDivisibleDiv @(PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) @(ChunkSize algorithm) ((((Div
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      (ChunkSize algorithm)
    * ChunkSize algorithm)
   ~ PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
  Vector d (ByteString (ChunkSize algorithm) context))
 -> Vector d (ByteString (ChunkSize algorithm) context))
-> (((Div
        (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
        (ChunkSize algorithm)
      * ChunkSize algorithm)
     ~ PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
    Vector d (ByteString (ChunkSize algorithm) context))
-> Vector d (ByteString (ChunkSize algorithm) context)
forall a b. (a -> b) -> a -> b
$
                        forall (m :: Natural) (wordSize :: Natural)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat wordSize) =>
ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
toWords @d @(ChunkSize algorithm) ByteString (d * ChunkSize algorithm) context
ByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
paddedMessage

sha2Var
    :: forall (algorithm :: Symbol) context k {d}
    .  SHA2 algorithm context k
    => KnownNat (Log2 (ChunkSize algorithm))
    => d ~ Div (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) (ChunkSize algorithm)
    => VarByteString k context -> ByteString (ResultSize algorithm) context
sha2Var :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type)
       (k :: Natural) {d :: Natural}.
(SHA2 algorithm context k, KnownNat (Log2 (ChunkSize algorithm)),
 d
 ~ Div
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)) =>
VarByteString k context
-> ByteString (ResultSize algorithm) context
sha2Var VarByteString k context
messageBits = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
FieldElement context
-> [ByteString (ChunkSize algorithm) context]
-> ByteString (ResultSize algorithm) context
sha2BlocksVar @algorithm @context FieldElement context
bsLength (Vector d (ByteString (ChunkSize algorithm) context)
-> [ByteString (ChunkSize algorithm) context]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector d (ByteString (ChunkSize algorithm) context)
chunks)
    where
        paddedMessage :: VarByteString (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) context
        paddedMessage :: VarByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
paddedMessage = ((KnownNat 2, KnownNat (WordSize algorithm))
 :- KnownNat (2 * WordSize algorithm))
-> (KnownNat (2 * WordSize algorithm) =>
    VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> VarByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat @2 @(WordSize algorithm)) ((KnownNat (2 * WordSize algorithm) =>
  VarByteString
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    context)
 -> VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> (KnownNat (2 * WordSize algorithm) =>
    VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> VarByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @(ChunkSize algorithm) @(2 * WordSize algorithm) ((KnownNat
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
  VarByteString
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    context)
 -> VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> (KnownNat
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
    VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> VarByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall a b. (a -> b) -> a -> b
$
                            forall (k :: Natural) (algorithm :: Symbol) {r}.
((k
  <= PaddedLength
       k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
 r)
-> r
withKLessPaddedLength @k @algorithm (((k
   <= PaddedLength
        k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
  VarByteString
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    context)
 -> VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> ((k
     <= PaddedLength
          k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
    VarByteString
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      context)
-> VarByteString
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     context
forall a b. (a -> b) -> a -> b
$
                                forall (padTo :: Natural) (lenBits :: Natural)
       (context :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic context, KnownNat k, KnownNat padTo,
 KnownNat (Log2 padTo), KnownNat lenBits) =>
VarByteString k context
-> VarByteString (PaddedLength k padTo lenBits) context
sha2PadVar @(ChunkSize algorithm) @(2 * WordSize algorithm) VarByteString k context
messageBits

        VarByteString{FieldElement context
ByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
bsLength :: FieldElement context
bsBuffer :: ByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
bsLength :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsBuffer :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
..} = VarByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
paddedMessage

        chunks :: Vector d (ByteString (ChunkSize algorithm) context)
        chunks :: Vector d (ByteString (ChunkSize algorithm) context)
chunks = forall (k :: Natural) (algorithm :: Symbol) {r}.
((Mod
    (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
    (ChunkSize algorithm)
  ~ 0) =>
 r)
-> r
withModPaddedLength @k @algorithm (((Mod
     (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
     (ChunkSize algorithm)
   ~ 0) =>
  Vector d (ByteString (ChunkSize algorithm) context))
 -> Vector d (ByteString (ChunkSize algorithm) context))
-> ((Mod
       (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
       (ChunkSize algorithm)
     ~ 0) =>
    Vector d (ByteString (ChunkSize algorithm) context))
-> Vector d (ByteString (ChunkSize algorithm) context)
forall a b. (a -> b) -> a -> b
$
                    forall (a :: Natural) (b :: Natural) {r}.
(Mod a b ~ 0) =>
(((Div a b * b) ~ a) => r) -> r
withDivisibleDiv @(PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) @(ChunkSize algorithm) ((((Div
      (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
      (ChunkSize algorithm)
    * ChunkSize algorithm)
   ~ PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
  Vector d (ByteString (ChunkSize algorithm) context))
 -> Vector d (ByteString (ChunkSize algorithm) context))
-> (((Div
        (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
        (ChunkSize algorithm)
      * ChunkSize algorithm)
     ~ PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm)) =>
    Vector d (ByteString (ChunkSize algorithm) context))
-> Vector d (ByteString (ChunkSize algorithm) context)
forall a b. (a -> b) -> a -> b
$
                        forall (m :: Natural) (wordSize :: Natural)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat wordSize) =>
ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
toWords @d @(ChunkSize algorithm) ByteString (d * ChunkSize algorithm) context
ByteString
  (PaddedLength k (ChunkSize algorithm) (2 * WordSize algorithm))
  context
bsBuffer


-- | Pad the input bytestring according to the rules described in @PaddedLength@
--
sha2Pad
    :: forall (padTo :: Natural) (lenBits :: Natural) context (k :: Natural)
    .  Symbolic context
    => KnownNat k
    => KnownNat padTo
    => KnownNat lenBits
    => ByteString k context
    -> ByteString (PaddedLength k padTo lenBits) context
sha2Pad :: forall (padTo :: Natural) (lenBits :: Natural)
       (context :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic context, KnownNat k, KnownNat padTo, KnownNat lenBits) =>
ByteString k context
-> ByteString (PaddedLength k padTo lenBits) context
sha2Pad ByteString k context
bs = forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) =>
  ByteString (PaddedLength k padTo lenBits) context)
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (KnownNat (PaddedLength k padTo lenBits) =>
    ByteString (PaddedLength k padTo lenBits) context)
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
ByteString (PaddedLength k padTo lenBits) context
grown ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall b. BoolType b => b -> b -> b
|| Natural
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a b. FromConstant a b => a -> b
fromConstant Natural
padValue
    where
        l :: Natural
        l :: Natural
l = forall (n :: Natural). KnownNat n => Natural
value @k

        diff :: Natural
        diff :: Natural
diff = forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) => Natural) -> Natural)
-> (KnownNat (PaddedLength k padTo lenBits) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(PaddedLength k padTo lenBits) Natural -> Natural -> Natural
-! forall (n :: Natural). KnownNat n => Natural
value @k

        padValue :: Natural
        padValue :: Natural
padValue = Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
P.^ (Natural
diff Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.+ Natural
l

        grown :: ByteString (PaddedLength k padTo lenBits) context
        grown :: ByteString (PaddedLength k padTo lenBits) context
grown = forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) =>
  ByteString (PaddedLength k padTo lenBits) context)
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (KnownNat (PaddedLength k padTo lenBits) =>
    ByteString (PaddedLength k padTo lenBits) context)
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ ByteString k context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a b. Resize a b => a -> b
resize ByteString k context
bs ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
-> Natural
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a. ShiftBits a => a -> Natural -> a
`shiftBitsL` Natural
diff


-- | Same as @sha2Pad@ but for variable-length ByteStrings
--
sha2PadVar
    :: forall (padTo :: Natural) (lenBits :: Natural) context (k :: Natural)
    .  Symbolic context
    => KnownNat k
    => KnownNat padTo
    => KnownNat (Log2 padTo)
    => KnownNat lenBits
    => VarByteString k context
    -> VarByteString (PaddedLength k padTo lenBits) context
sha2PadVar :: forall (padTo :: Natural) (lenBits :: Natural)
       (context :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic context, KnownNat k, KnownNat padTo,
 KnownNat (Log2 padTo), KnownNat lenBits) =>
VarByteString k context
-> VarByteString (PaddedLength k padTo lenBits) context
sha2PadVar VarByteString{FieldElement context
ByteString k context
bsLength :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsBuffer :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
bsLength :: FieldElement context
bsBuffer :: ByteString k context
..} = FieldElement context
-> ByteString (PaddedLength k padTo lenBits) context
-> VarByteString (PaddedLength k padTo lenBits) context
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString FieldElement context
paddedLengthFe (ByteString (PaddedLength k padTo lenBits) context
 -> VarByteString (PaddedLength k padTo lenBits) context)
-> ByteString (PaddedLength k padTo lenBits) context
-> VarByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) =>
  ByteString (PaddedLength k padTo lenBits) context)
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (KnownNat (PaddedLength k padTo lenBits) =>
    ByteString (PaddedLength k padTo lenBits) context)
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
ByteString (PaddedLength k padTo lenBits) context
grown ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall b. BoolType b => b -> b -> b
|| ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
ByteString (PaddedLength k padTo lenBits) context
lenBits
    where
        chunkBits :: Natural
        chunkBits :: Natural
chunkBits = Natural -> Natural
ilog2 (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @padTo

        numWords :: Natural
        numWords :: Natural
numWords = (forall (n :: Natural). KnownNat n => Natural
value @(NumberOfBits (BaseField context)) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
chunkBits Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
chunkBits

        getNextChunk :: FieldElement context -> FieldElement context
        getNextChunk :: FieldElement context -> FieldElement context
getNextChunk (FieldElement context Par1
fe) = context Par1 -> FieldElement context
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (context Par1 -> FieldElement context)
-> context Par1 -> FieldElement context
forall a b. (a -> b) -> a -> b
$ context Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i,
     MonadCircuit i (BaseField context) (WitnessField context) m) =>
    FunBody '[Par1] Par1 i m)
-> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun '[f] g context -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF context Par1
fe ((forall {i} {m :: Type -> Type}.
  (NFData i,
   MonadCircuit i (BaseField context) (WitnessField context) m) =>
  FunBody '[Par1] Par1 i m)
 -> context Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i,
     MonadCircuit i (BaseField context) (WitnessField context) m) =>
    FunBody '[Par1] Par1 i m)
-> context Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
e) -> do
            [i]
feWords <- forall (r :: Natural) i a w (m :: Type -> Type).
(KnownNat r, MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansionW @(Log2 padTo) Natural
numWords i
e
            i
d <- ClosedPoly i (BaseField context) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField context) -> m i)
-> ClosedPoly i (BaseField context) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> (Natural -> x
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> x) -> Natural -> x
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @padTo) x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p ([i] -> i
forall a. HasCallStack => [a] -> a
P.head [i]
feWords)
            [i]
dWords <- forall (r :: Natural) i a w (m :: Type -> Type).
(KnownNat r, MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansionW @(Log2 padTo) Natural
2 i
d -- unset the most significant bit if feWords was divisible by @padTo@
            i
res <- ClosedPoly i (BaseField context) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField context) -> m i)
-> ClosedPoly i (BaseField context) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
e x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p ([i] -> i
forall a. HasCallStack => [a] -> a
P.head [i]
dWords)
            Par1 i -> m (Par1 i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Par1 i -> m (Par1 i)) -> Par1 i -> m (Par1 i)
forall a b. (a -> b) -> a -> b
$ i -> Par1 i
forall p. p -> Par1 p
Par1 i
res

        nextChunk :: FieldElement context
        nextChunk :: FieldElement context
nextChunk = FieldElement context -> FieldElement context
getNextChunk FieldElement context
bsLength

        paddedLengthFe :: FieldElement context
        paddedLengthFe :: FieldElement context
paddedLengthFe = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool context) FieldElement context
nextChunk (FieldElement context
nextChunk FieldElement context
-> FieldElement context -> FieldElement context
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> FieldElement context
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @padTo)) (FieldElement context
nextChunk FieldElement context
-> FieldElement context -> BooleanOf (FieldElement context)
forall a. Ord a => a -> a -> BooleanOf a
<= FieldElement context
bsLength FieldElement context
-> FieldElement context -> FieldElement context
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> FieldElement context
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @lenBits))

        diff :: FieldElement context
        diff :: FieldElement context
diff = FieldElement context
paddedLengthFe FieldElement context
-> FieldElement context -> FieldElement context
forall a. AdditiveGroup a => a -> a -> a
- FieldElement context
bsLength

        lenBits :: ByteString (PaddedLength k padTo lenBits) context
        lenBits :: ByteString (PaddedLength k padTo lenBits) context
lenBits = forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) =>
  ByteString (PaddedLength k padTo lenBits) context)
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (KnownNat (PaddedLength k padTo lenBits) =>
    ByteString (PaddedLength k padTo lenBits) context)
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ ByteString (Log2 (Order (BaseField context) - 1) + 1) context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
ByteString (Log2 (Order (BaseField context) - 1) + 1) context
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. Resize a b => a -> b
resize (ByteString (Log2 (Order (BaseField context) - 1) + 1) context
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (context (Vector (Log2 (Order (BaseField context) - 1) + 1))
    -> ByteString (Log2 (Order (BaseField context) - 1) + 1) context)
-> context (Vector (Log2 (Order (BaseField context) - 1) + 1))
-> ByteString (PaddedLength k padTo lenBits) context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. context (Vector (Log2 (Order (BaseField context) - 1) + 1))
-> ByteString (Log2 (Order (BaseField context) - 1) + 1) context
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (context (Vector (Log2 (Order (BaseField context) - 1) + 1))
 -> ByteString (Log2 (Order (BaseField context) - 1) + 1) context)
-> (context (Vector (Log2 (Order (BaseField context) - 1) + 1))
    -> context (Vector (Log2 (Order (BaseField context) - 1) + 1)))
-> context (Vector (Log2 (Order (BaseField context) - 1) + 1))
-> ByteString (Log2 (Order (BaseField context) - 1) + 1) context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a.
 Vector (Log2 (Order (BaseField context) - 1) + 1) a
 -> Vector (Log2 (Order (BaseField context) - 1) + 1) a)
-> context (Vector (Log2 (Order (BaseField context) - 1) + 1))
-> context (Vector (Log2 (Order (BaseField context) - 1) + 1))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> context f -> context g
hmap Vector (Log2 (Order (BaseField context) - 1) + 1) a
-> Vector (Log2 (Order (BaseField context) - 1) + 1) a
forall (size :: Natural) a. Vector size a -> Vector size a
forall a.
Vector (Log2 (Order (BaseField context) - 1) + 1) a
-> Vector (Log2 (Order (BaseField context) - 1) + 1) a
reverse (context (Vector (Log2 (Order (BaseField context) - 1) + 1))
 -> ByteString (PaddedLength k padTo lenBits) context)
-> context (Vector (Log2 (Order (BaseField context) - 1) + 1))
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ FieldElement context -> Bits (FieldElement context)
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion FieldElement context
bsLength

        paddedL :: Natural
        paddedL :: Natural
paddedL = forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) => Natural) -> Natural)
-> (KnownNat (PaddedLength k padTo lenBits) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(PaddedLength k padTo lenBits)

        grown :: ByteString (PaddedLength k padTo lenBits) context
        grown :: ByteString (PaddedLength k padTo lenBits) context
grown = let resized :: ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
resized = forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) =>
  ByteString
    (If
       (OrdCond
          (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
          'True
          'True
          'False)
       (padTo + (padTo * Div ((k + padTo) - 1) padTo))
       (padTo * Div ((k + padTo) - 1) padTo))
    context)
 -> ByteString
      (If
         (OrdCond
            (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
            'True
            'True
            'False)
         (padTo + (padTo * Div ((k + padTo) - 1) padTo))
         (padTo * Div ((k + padTo) - 1) padTo))
      context)
-> (KnownNat (PaddedLength k padTo lenBits) =>
    ByteString
      (If
         (OrdCond
            (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
            'True
            'True
            'False)
         (padTo + (padTo * Div ((k + padTo) - 1) padTo))
         (padTo * Div ((k + padTo) - 1) padTo))
      context)
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a b. (a -> b) -> a -> b
$ ByteString k context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a b. Resize a b => a -> b
resize ByteString k context
bsBuffer
                 in forall (n :: Natural) (d :: Natural) (l :: Natural) {r}.
(KnownNat d, KnownNat n, KnownNat l) =>
(KnownNat (PaddedLength n d l) => r) -> r
withPaddedLength @k @padTo @lenBits ((KnownNat (PaddedLength k padTo lenBits) =>
  ByteString (PaddedLength k padTo lenBits) context)
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (KnownNat (PaddedLength k padTo lenBits) =>
    ByteString (PaddedLength k padTo lenBits) context)
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ (ByteString (PaddedLength k padTo lenBits) context
-> FieldElement context
-> ByteString (PaddedLength k padTo lenBits) context
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
`VB.shiftL` (FieldElement context
diff FieldElement context
-> FieldElement context -> FieldElement context
forall a. AdditiveGroup a => a -> a -> a
- FieldElement context
forall a. MultiplicativeMonoid a => a
one)) (ByteString
   (If
      (OrdCond
         (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
         'True
         'True
         'False)
      (padTo + (padTo * Div ((k + padTo) - 1) padTo))
      (padTo * Div ((k + padTo) - 1) padTo))
   context
 -> ByteString (PaddedLength k padTo lenBits) context)
-> (ByteString
      (If
         (OrdCond
            (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
            'True
            'True
            'False)
         (padTo + (padTo * Div ((k + padTo) - 1) padTo))
         (padTo * Div ((k + padTo) - 1) padTo))
      context
    -> ByteString
         (If
            (OrdCond
               (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
               'True
               'True
               'False)
            (padTo + (padTo * Div ((k + padTo) - 1) padTo))
            (padTo * Div ((k + padTo) - 1) padTo))
         context)
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
-> ByteString (PaddedLength k padTo lenBits) context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString
   (If
      (OrdCond
         (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
         'True
         'True
         'False)
      (padTo + (padTo * Div ((k + padTo) - 1) padTo))
      (padTo * Div ((k + padTo) - 1) padTo))
   context
 -> Natural
 -> ByteString
      (If
         (OrdCond
            (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
            'True
            'True
            'False)
         (padTo + (padTo * Div ((k + padTo) - 1) padTo))
         (padTo * Div ((k + padTo) - 1) padTo))
      context)
-> Natural
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
-> Natural
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall (c :: (Type -> Type) -> Type) (n :: Natural).
(Symbolic c, KnownNat n) =>
ByteString n c -> Natural -> ByteString n c
set (Natural
paddedL Natural -> Natural -> Natural
-! Natural
1) (ByteString
   (If
      (OrdCond
         (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
         'True
         'True
         'False)
      (padTo + (padTo * Div ((k + padTo) - 1) padTo))
      (padTo * Div ((k + padTo) - 1) padTo))
   context
 -> ByteString
      (If
         (OrdCond
            (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
            'True
            'True
            'False)
         (padTo + (padTo * Div ((k + padTo) - 1) padTo))
         (padTo * Div ((k + padTo) - 1) padTo))
      context)
-> (ByteString
      (If
         (OrdCond
            (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
            'True
            'True
            'False)
         (padTo + (padTo * Div ((k + padTo) - 1) padTo))
         (padTo * Div ((k + padTo) - 1) padTo))
      context
    -> ByteString
         (If
            (OrdCond
               (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
               'True
               'True
               'False)
            (padTo + (padTo * Div ((k + padTo) - 1) padTo))
            (padTo * Div ((k + padTo) - 1) padTo))
         context)
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
-> Natural
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
forall a. ShiftBits a => a -> Natural -> a
`shiftBitsL` Natural
1) (ByteString
   (If
      (OrdCond
         (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
         'True
         'True
         'False)
      (padTo + (padTo * Div ((k + padTo) - 1) padTo))
      (padTo * Div ((k + padTo) - 1) padTo))
   context
 -> ByteString (PaddedLength k padTo lenBits) context)
-> ByteString
     (If
        (OrdCond
           (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
           'True
           'True
           'False)
        (padTo + (padTo * Div ((k + padTo) - 1) padTo))
        (padTo * Div ((k + padTo) - 1) padTo))
     context
-> ByteString (PaddedLength k padTo lenBits) context
forall a b. (a -> b) -> a -> b
$ ByteString
  (If
     (OrdCond
        (CmpNat ((padTo * Div ((k + padTo) - 1) padTo) - k) lenBits)
        'True
        'True
        'False)
     (padTo + (padTo * Div ((k + padTo) - 1) padTo))
     (padTo * Div ((k + padTo) - 1) padTo))
  context
resized

-- | This allows us to calculate hash of a bytestring represented by a Natural number.
-- This is only useful for testing when the length of the test string is unknown at compile time.
-- This should not be exposed to users (and they probably won't find it useful anyway).
--
toWordsNat :: forall n c. (KnownNat n, FromConstant Natural (ByteString n c)) => Natural -> [ByteString n c]
toWordsNat :: forall (n :: Natural) (c :: (Type -> Type) -> Type).
(KnownNat n, FromConstant Natural (ByteString n c)) =>
Natural -> [ByteString n c]
toWordsNat = [ByteString n c] -> [ByteString n c]
forall a. [a] -> [a]
P.reverse ([ByteString n c] -> [ByteString n c])
-> (Natural -> [ByteString n c]) -> Natural -> [ByteString n c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> [ByteString n c]
toWords'
    where
        toWords' :: Natural -> [ByteString n c]
        toWords' :: Natural -> [ByteString n c]
toWords' Natural
0 = []
        toWords' Natural
n = Natural -> ByteString n c
forall a b. FromConstant a b => a -> b
fromConstant (Natural
n Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
base) ByteString n c -> [ByteString n c] -> [ByteString n c]
forall a. a -> [a] -> [a]
: Natural -> [ByteString n c]
toWords' (Natural
n Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
base)

        base :: Natural
        base :: Natural
base = Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
P.^ (forall (n :: Natural). KnownNat n => Natural
value @n)


-- | Constraints required for a SHA2 of a Natural number.
--
type SHA2N algorithm context = AlgorithmSetup algorithm context


-- | Same as @sha2@ but accepts a Natural number and length of message in bits instead of a ByteString.
-- Only used for testing.
--
sha2Natural
    :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type)
    .  SHA2N algorithm context
    => Natural -> Natural -> ByteString (ResultSize algorithm) context
sha2Natural :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
SHA2N algorithm context =>
Natural -> Natural -> ByteString (ResultSize algorithm) context
sha2Natural Natural
numBits Natural
messageBits = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
[ByteString (ChunkSize algorithm) context]
-> ByteString (ResultSize algorithm) context
sha2Blocks @algorithm @context [ByteString (ChunkSize algorithm) context]
chunks
    where
        paddedMessage :: Natural
        paddedMessage :: Natural
paddedMessage = (Natural
messageBits Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` Int
diff) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.+ (Natural
1 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shiftL` (Int
diff Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1)) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.+ Natural
numBits

        chunkSize :: Natural
        chunkSize :: Natural
chunkSize = forall (n :: Natural). KnownNat n => Natural
value @(ChunkSize algorithm)

        wordSize :: Natural
        wordSize :: Natural
wordSize = forall (n :: Natural). KnownNat n => Natural
value @(WordSize algorithm)

        closestDivisor :: Natural
        closestDivisor :: Natural
closestDivisor = ((Natural
numBits Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.+ Natural
chunkSize Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
chunkSize) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.* Natural
chunkSize

        paddedLength :: Natural
        paddedLength :: Natural
paddedLength
          | Natural
closestDivisor Natural -> Natural -> Natural
-! Natural
numBits Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
P.<= (Natural
2 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
wordSize) = Natural
closestDivisor Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.+ Natural
chunkSize
          | Bool
P.otherwise = Natural
closestDivisor

        diff :: P.Int
        diff :: Int
diff = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Natural
paddedLength Natural -> Natural -> Natural
-! Natural
numBits

        chunks :: [ByteString (ChunkSize algorithm) context]
        chunks :: [ByteString (ChunkSize algorithm) context]
chunks = Natural -> [ByteString (ChunkSize algorithm) context]
forall (n :: Natural) (c :: (Type -> Type) -> Type).
(KnownNat n, FromConstant Natural (ByteString n c)) =>
Natural -> [ByteString n c]
toWordsNat Natural
paddedMessage

-- | Internal loop of the SHA2 family algorithms.
--
-- A note on @force@: it is really necessary, otherwise the algorithm keeps piling up thunks.
-- Even 16 GB of RAM is not enough.
--
sha2Blocks
    :: forall algorithm (context :: (Type -> Type) -> Type)
    .  AlgorithmSetup algorithm context
    => [ByteString (ChunkSize algorithm) context] -> ByteString (ResultSize algorithm) context
sha2Blocks :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
[ByteString (ChunkSize algorithm) context]
-> ByteString (ResultSize algorithm) context
sha2Blocks [ByteString (ChunkSize algorithm) context]
chunks = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
ByteString (8 * WordSize algorithm) context
-> ByteString (ResultSize algorithm) context
truncateResult @algorithm @context (ByteString (8 * WordSize algorithm) context
 -> ByteString (ResultSize algorithm) context)
-> ByteString (8 * WordSize algorithm) context
-> ByteString (ResultSize algorithm) context
forall a b. (a -> b) -> a -> b
$ forall (k :: Natural) (m :: Natural) (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector k (ByteString m c) -> ByteString (k * m) c
concat @8 @(WordSize algorithm) (Vector 8 (ByteString (WordSize algorithm) context)
 -> ByteString (8 * WordSize algorithm) context)
-> Vector 8 (ByteString (WordSize algorithm) context)
-> ByteString (8 * WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector @8 ([ByteString (WordSize algorithm) context]
 -> Vector 8 (ByteString (WordSize algorithm) context))
-> [ByteString (WordSize algorithm) context]
-> Vector 8 (ByteString (WordSize algorithm) context)
forall a b. (a -> b) -> a -> b
$ Vector (ByteString (WordSize algorithm) context)
-> [ByteString (WordSize algorithm) context]
forall a. Vector a -> [a]
V.toList Vector (ByteString (WordSize algorithm) context)
hashParts
    where
        hashParts :: V.Vector (ByteString (WordSize algorithm) context)
        hashParts :: Vector (ByteString (WordSize algorithm) context)
hashParts = (forall s.
 ST s (MVector s (ByteString (WordSize algorithm) context)))
-> Vector (ByteString (WordSize algorithm) context)
forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create ((forall s.
  ST s (MVector s (ByteString (WordSize algorithm) context)))
 -> Vector (ByteString (WordSize algorithm) context))
-> (forall s.
    ST s (MVector s (ByteString (WordSize algorithm) context)))
-> Vector (ByteString (WordSize algorithm) context)
forall a b. (a -> b) -> a -> b
$ do
            !MVector s (ByteString (WordSize algorithm) context)
hn <- Vector (ByteString (WordSize algorithm) context)
-> ST
     s
     (MVector
        (PrimState (ST s)) (ByteString (WordSize algorithm) context))
forall (m :: Type -> Type) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw (Vector (ByteString (WordSize algorithm) context)
 -> ST
      s
      (MVector
         (PrimState (ST s)) (ByteString (WordSize algorithm) context)))
-> Vector (ByteString (WordSize algorithm) context)
-> ST
     s
     (MVector
        (PrimState (ST s)) (ByteString (WordSize algorithm) context))
forall a b. (a -> b) -> a -> b
$ forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
Vector (ByteString (WordSize algorithm) context)
initialHashes @algorithm @context

            [ByteString (ChunkSize algorithm) context]
-> (ByteString (ChunkSize algorithm) context
    -> ST s (MVector s (ByteString (WordSize algorithm) context)))
-> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ByteString (ChunkSize algorithm) context]
chunks ((ByteString (ChunkSize algorithm) context
  -> ST s (MVector s (ByteString (WordSize algorithm) context)))
 -> ST s ())
-> (ByteString (ChunkSize algorithm) context
    -> ST s (MVector s (ByteString (WordSize algorithm) context)))
-> ST s ()
forall a b. (a -> b) -> a -> b
$ forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type) s.
AlgorithmSetup algorithm context =>
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> ByteString (ChunkSize algorithm) context
-> ST
     s
     (MVector
        (PrimState (ST s)) (ByteString (WordSize algorithm) context))
processChunk @algorithm @context MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn

            MVector s (ByteString (WordSize algorithm) context)
-> ST s (MVector s (ByteString (WordSize algorithm) context))
forall a. a -> ST s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure MVector s (ByteString (WordSize algorithm) context)
hn


-- | Same as @sha2Blocks@ but ignores unassigned blocks of a VarByteString
-- The current length of the VarByteString being processed is stored in the FieldElement
--
sha2BlocksVar
    :: forall algorithm (context :: (Type -> Type) -> Type)
    .  AlgorithmSetup algorithm context
    => FieldElement context -> [ByteString (ChunkSize algorithm) context] -> ByteString (ResultSize algorithm) context
sha2BlocksVar :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
FieldElement context
-> [ByteString (ChunkSize algorithm) context]
-> ByteString (ResultSize algorithm) context
sha2BlocksVar FieldElement context
len [ByteString (ChunkSize algorithm) context]
chunks = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
ByteString (8 * WordSize algorithm) context
-> ByteString (ResultSize algorithm) context
truncateResult @algorithm @context (ByteString (8 * WordSize algorithm) context
 -> ByteString (ResultSize algorithm) context)
-> ByteString (8 * WordSize algorithm) context
-> ByteString (ResultSize algorithm) context
forall a b. (a -> b) -> a -> b
$ forall (k :: Natural) (m :: Natural) (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector k (ByteString m c) -> ByteString (k * m) c
concat @8 @(WordSize algorithm) (Vector 8 (ByteString (WordSize algorithm) context)
 -> ByteString (8 * WordSize algorithm) context)
-> Vector 8 (ByteString (WordSize algorithm) context)
-> ByteString (8 * WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ forall (size :: Natural) a. Vector a -> Vector size a
Vector @8 Vector (ByteString (WordSize algorithm) context)
hashParts
    where
        chunkSize :: Natural
        chunkSize :: Natural
chunkSize = forall (n :: Natural). KnownNat n => Natural
value @(ChunkSize algorithm)

        initHn :: V.Vector (ByteString (WordSize algorithm) context)
        initHn :: Vector (ByteString (WordSize algorithm) context)
initHn = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
Vector (ByteString (WordSize algorithm) context)
initialHashes @algorithm @context

        hashParts :: V.Vector (ByteString (WordSize algorithm) context)
        hashParts :: Vector (ByteString (WordSize algorithm) context)
hashParts = (Vector (ByteString (WordSize algorithm) context)
 -> (Natural, ByteString (ChunkSize algorithm) context)
 -> Vector (ByteString (WordSize algorithm) context))
-> Vector (ByteString (WordSize algorithm) context)
-> [(Natural, ByteString (ChunkSize algorithm) context)]
-> Vector (ByteString (WordSize algorithm) context)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl Vector (ByteString (WordSize algorithm) context)
-> (Natural, ByteString (ChunkSize algorithm) context)
-> Vector (ByteString (WordSize algorithm) context)
varStep Vector (ByteString (WordSize algorithm) context)
initHn ([(Natural, ByteString (ChunkSize algorithm) context)]
-> [(Natural, ByteString (ChunkSize algorithm) context)]
forall a. [a] -> [a]
P.reverse ([(Natural, ByteString (ChunkSize algorithm) context)]
 -> [(Natural, ByteString (ChunkSize algorithm) context)])
-> [(Natural, ByteString (ChunkSize algorithm) context)]
-> [(Natural, ByteString (ChunkSize algorithm) context)]
forall a b. (a -> b) -> a -> b
$ [Natural]
-> [ByteString (ChunkSize algorithm) context]
-> [(Natural, ByteString (ChunkSize algorithm) context)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [Natural
0..] ([ByteString (ChunkSize algorithm) context]
 -> [(Natural, ByteString (ChunkSize algorithm) context)])
-> [ByteString (ChunkSize algorithm) context]
-> [(Natural, ByteString (ChunkSize algorithm) context)]
forall a b. (a -> b) -> a -> b
$ [ByteString (ChunkSize algorithm) context]
-> [ByteString (ChunkSize algorithm) context]
forall a. [a] -> [a]
P.reverse [ByteString (ChunkSize algorithm) context]
chunks)

        varStep
            :: V.Vector (ByteString (WordSize algorithm) context)
            -> (Natural, ByteString (ChunkSize algorithm) context)
            -> V.Vector (ByteString (WordSize algorithm) context)
        varStep :: Vector (ByteString (WordSize algorithm) context)
-> (Natural, ByteString (ChunkSize algorithm) context)
-> Vector (ByteString (WordSize algorithm) context)
varStep Vector (ByteString (WordSize algorithm) context)
hn (Natural
ix, ByteString (ChunkSize algorithm) context
chunk) =
            Vector 8 (ByteString (WordSize algorithm) context)
-> Vector (ByteString (WordSize algorithm) context)
forall (size :: Natural) a. Vector size a -> Vector a
toV (Vector 8 (ByteString (WordSize algorithm) context)
 -> Vector (ByteString (WordSize algorithm) context))
-> Vector 8 (ByteString (WordSize algorithm) context)
-> Vector (ByteString (WordSize algorithm) context)
forall a b. (a -> b) -> a -> b
$ forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool context)
                    (forall (size :: Natural) a. Vector a -> Vector size a
Vector @8 Vector (ByteString (WordSize algorithm) context)
hn)
                    (forall (size :: Natural) a. Vector a -> Vector size a
Vector @8 (Vector (ByteString (WordSize algorithm) context)
 -> Vector 8 (ByteString (WordSize algorithm) context))
-> Vector (ByteString (WordSize algorithm) context)
-> Vector 8 (ByteString (WordSize algorithm) context)
forall a b. (a -> b) -> a -> b
$ forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
Vector (ByteString (WordSize algorithm) context)
-> ByteString (ChunkSize algorithm) context
-> Vector (ByteString (WordSize algorithm) context)
processChunkPure @algorithm @context Vector (ByteString (WordSize algorithm) context)
hn ByteString (ChunkSize algorithm) context
chunk)
                    (FieldElement context
len FieldElement context
-> FieldElement context -> BooleanOf (FieldElement context)
forall a. Ord a => a -> a -> BooleanOf a
> (Natural -> FieldElement context
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> FieldElement context)
-> Natural -> FieldElement context
forall a b. (a -> b) -> a -> b
$ Natural
ix Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
chunkSize))

processChunkPure
    :: forall algorithm context
    .  AlgorithmSetup algorithm context
    => V.Vector (ByteString (WordSize algorithm) context)
    -> ByteString (ChunkSize algorithm) context
    -> V.Vector (ByteString (WordSize algorithm) context)
processChunkPure :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
Vector (ByteString (WordSize algorithm) context)
-> ByteString (ChunkSize algorithm) context
-> Vector (ByteString (WordSize algorithm) context)
processChunkPure Vector (ByteString (WordSize algorithm) context)
hn ByteString (ChunkSize algorithm) context
chunk = (forall s. ST s (Vector (ByteString (WordSize algorithm) context)))
-> Vector (ByteString (WordSize algorithm) context)
forall a. (forall s. ST s a) -> a
runST ((forall s.
  ST s (Vector (ByteString (WordSize algorithm) context)))
 -> Vector (ByteString (WordSize algorithm) context))
-> (forall s.
    ST s (Vector (ByteString (WordSize algorithm) context)))
-> Vector (ByteString (WordSize algorithm) context)
forall a b. (a -> b) -> a -> b
$ do
    MVector s (ByteString (WordSize algorithm) context)
mutHn <- Vector (ByteString (WordSize algorithm) context)
-> ST
     s
     (MVector
        (PrimState (ST s)) (ByteString (WordSize algorithm) context))
forall (m :: Type -> Type) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector (ByteString (WordSize algorithm) context)
hn
    MVector s (ByteString (WordSize algorithm) context)
res <- forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type) s.
AlgorithmSetup algorithm context =>
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> ByteString (ChunkSize algorithm) context
-> ST
     s
     (MVector
        (PrimState (ST s)) (ByteString (WordSize algorithm) context))
processChunk @algorithm @context MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
mutHn ByteString (ChunkSize algorithm) context
chunk
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> ST s (Vector (ByteString (WordSize algorithm) context))
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> m (Vector a)
V.freeze MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
res

processChunk
    :: forall algorithm context s
    .  AlgorithmSetup algorithm context
    => V.MVector (VM.PrimState (ST s)) (ByteString (WordSize algorithm) context)
    -> ByteString (ChunkSize algorithm) context
    -> ST s (V.MVector (VM.PrimState (ST s)) (ByteString (WordSize algorithm) context))
processChunk :: forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type) s.
AlgorithmSetup algorithm context =>
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> ByteString (ChunkSize algorithm) context
-> ST
     s
     (MVector
        (PrimState (ST s)) (ByteString (WordSize algorithm) context))
processChunk MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn ByteString (ChunkSize algorithm) context
chunk = do
    let words :: [ByteString (WordSize algorithm) context]
words =
            Vector
  (Div (ChunkSize algorithm) (WordSize algorithm))
  (ByteString (WordSize algorithm) context)
-> [ByteString (WordSize algorithm) context]
forall (size :: Natural) a. Vector size a -> [a]
fromVector (Vector
   (Div (ChunkSize algorithm) (WordSize algorithm))
   (ByteString (WordSize algorithm) context)
 -> [ByteString (WordSize algorithm) context])
-> Vector
     (Div (ChunkSize algorithm) (WordSize algorithm))
     (ByteString (WordSize algorithm) context)
-> [ByteString (WordSize algorithm) context]
forall a b. (a -> b) -> a -> b
$
                forall (a :: Natural) (b :: Natural) {r}.
(Mod a b ~ 0) =>
(((Div a b * b) ~ a) => r) -> r
withDivisibleDiv @(ChunkSize algorithm) @(WordSize algorithm) ((((Div (ChunkSize algorithm) (WordSize algorithm)
    * WordSize algorithm)
   ~ ChunkSize algorithm) =>
  Vector
    (Div (ChunkSize algorithm) (WordSize algorithm))
    (ByteString (WordSize algorithm) context))
 -> Vector
      (Div (ChunkSize algorithm) (WordSize algorithm))
      (ByteString (WordSize algorithm) context))
-> (((Div (ChunkSize algorithm) (WordSize algorithm)
      * WordSize algorithm)
     ~ ChunkSize algorithm) =>
    Vector
      (Div (ChunkSize algorithm) (WordSize algorithm))
      (ByteString (WordSize algorithm) context))
-> Vector
     (Div (ChunkSize algorithm) (WordSize algorithm))
     (ByteString (WordSize algorithm) context)
forall a b. (a -> b) -> a -> b
$
                    forall (m :: Natural) (wordSize :: Natural)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat wordSize) =>
ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
toWords @(Div (ChunkSize algorithm) (WordSize algorithm)) @(WordSize algorithm) ByteString
  (Div (ChunkSize algorithm) (WordSize algorithm)
   * WordSize algorithm)
  context
ByteString (ChunkSize algorithm) context
chunk

    MVector s (ByteString (WordSize algorithm) context)
messageSchedule <- forall (m :: Type -> Type) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
VM.unsafeNew @_ @(ByteString (WordSize algorithm) context) Int
rounds
    [(Int, ByteString (WordSize algorithm) context)]
-> ((Int, ByteString (WordSize algorithm) context) -> ST s ())
-> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Int]
-> [ByteString (WordSize algorithm) context]
-> [(Int, ByteString (WordSize algorithm) context)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [ByteString (WordSize algorithm) context]
words) (((Int, ByteString (WordSize algorithm) context) -> ST s ())
 -> ST s ())
-> ((Int, ByteString (WordSize algorithm) context) -> ST s ())
-> ST s ()
forall a b. (a -> b) -> a -> b
$ (Int -> ByteString (WordSize algorithm) context -> ST s ())
-> (Int, ByteString (WordSize algorithm) context) -> ST s ()
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry (MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ByteString (WordSize algorithm) context -> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
VM.write MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule)

    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
16 .. Int
rounds Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
ix -> do
        !ByteString (WordSize algorithm) context
w16 <- MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
16)
        !ByteString (WordSize algorithm) context
w15 <- MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
15)
        !ByteString (WordSize algorithm) context
w7  <- MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
7)
        !ByteString (WordSize algorithm) context
w2  <- MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
2)
        let (Natural
sh0, Natural
sh1, Natural
sh2, Natural
sh3, Natural
sh4, Natural
sh5) = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
(Natural, Natural, Natural, Natural, Natural, Natural)
sigmaShifts @algorithm @context
            s0 :: ByteString (WordSize algorithm) context
s0  = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ (ByteString (WordSize algorithm) context
w15 ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh0) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
w15 ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh1) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
w15 ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`shiftBitsR` Natural
sh2)
            s1 :: ByteString (WordSize algorithm) context
s1  = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ (ByteString (WordSize algorithm) context
w2 ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh3) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
w2 ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh4) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
w2 ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`shiftBitsR` Natural
sh5)
        MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ByteString (WordSize algorithm) context -> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
VM.write MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule Int
ix (ByteString (WordSize algorithm) context -> ST s ())
-> ByteString (WordSize algorithm) context -> ST s ()
forall a b. (a -> b) -> a -> b
$! UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w16 UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
s0 UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w7 UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
s1 :: UInt (WordSize algorithm) Auto context)

    !STRef s (ByteString (WordSize algorithm) context)
aRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
0 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
bRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
1 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
cRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
2 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
dRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
3 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
eRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
4 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
fRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
5 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
gRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
6 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef
    !STRef s (ByteString (WordSize algorithm) context)
hRef <- MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
7 ST s (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ST s (STRef s (ByteString (WordSize algorithm) context)))
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString (WordSize algorithm) context
-> ST s (STRef s (ByteString (WordSize algorithm) context))
forall a s. a -> ST s (STRef s a)
ST.newSTRef

    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0 .. Int
rounds Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
ix -> do
        !ByteString (WordSize algorithm) context
a <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
aRef
        !ByteString (WordSize algorithm) context
b <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
bRef
        !ByteString (WordSize algorithm) context
c <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
cRef
        !ByteString (WordSize algorithm) context
d <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
dRef
        !ByteString (WordSize algorithm) context
e <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
eRef
        !ByteString (WordSize algorithm) context
f <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
fRef
        !ByteString (WordSize algorithm) context
g <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
gRef
        !ByteString (WordSize algorithm) context
h <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
hRef

        let ki :: ByteString (WordSize algorithm) context
ki = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
Vector (ByteString (WordSize algorithm) context)
roundConstants @algorithm @context Vector (ByteString (WordSize algorithm) context)
-> Int -> ByteString (WordSize algorithm) context
forall a. Vector a -> Int -> a
V.! Int
ix
        ByteString (WordSize algorithm) context
wi <- MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
messageSchedule MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> Int -> ST s (ByteString (WordSize algorithm) context)
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
`VM.read` Int
ix

        let (Natural
sh0, Natural
sh1, Natural
sh2, Natural
sh3, Natural
sh4, Natural
sh5) = forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
(Natural, Natural, Natural, Natural, Natural, Natural)
sumShifts @algorithm @context
            s1 :: ByteString (WordSize algorithm) context
s1    = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ (ByteString (WordSize algorithm) context
e ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh3) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
e ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh4) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
e ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh5)
            ch :: ByteString (WordSize algorithm) context
ch    = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ (ByteString (WordSize algorithm) context
e ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
&& ByteString (WordSize algorithm) context
f) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b
not ByteString (WordSize algorithm) context
e ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
&& ByteString (WordSize algorithm) context
g)
            temp1 :: ByteString (WordSize algorithm) context
temp1 = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
h UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
s1 UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
ch UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
ki UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
wi :: UInt (WordSize algorithm) Auto context) :: ByteString (WordSize algorithm) context
            s0 :: ByteString (WordSize algorithm) context
s0    = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ (ByteString (WordSize algorithm) context
a ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh0) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
a ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh1) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
a ByteString (WordSize algorithm) context
-> Natural -> ByteString (WordSize algorithm) context
forall a. ShiftBits a => a -> Natural -> a
`rotateBitsR` Natural
sh2)
            maj :: ByteString (WordSize algorithm) context
maj   = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ (ByteString (WordSize algorithm) context
a ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
&& ByteString (WordSize algorithm) context
b) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
a ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
&& ByteString (WordSize algorithm) context
c) ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
`xor` (ByteString (WordSize algorithm) context
b ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall b. BoolType b => b -> b -> b
&& ByteString (WordSize algorithm) context
c)
            temp2 :: ByteString (WordSize algorithm) context
temp2 = ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a. NFData a => a -> a
force (ByteString (WordSize algorithm) context
 -> ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context
-> ByteString (WordSize algorithm) context
forall a b. (a -> b) -> a -> b
$ UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
s0 UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
maj :: UInt (WordSize algorithm) Auto context) :: ByteString (WordSize algorithm) context

        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
hRef ByteString (WordSize algorithm) context
g
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
gRef ByteString (WordSize algorithm) context
f
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
fRef ByteString (WordSize algorithm) context
e
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
eRef (ByteString (WordSize algorithm) context -> ST s ())
-> ByteString (WordSize algorithm) context -> ST s ()
forall a b. (a -> b) -> a -> b
$ UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
d UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
temp1 :: UInt (WordSize algorithm) Auto context)
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
dRef ByteString (WordSize algorithm) context
c
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
cRef ByteString (WordSize algorithm) context
b
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
bRef ByteString (WordSize algorithm) context
a
        STRef s (ByteString (WordSize algorithm) context)
-> ByteString (WordSize algorithm) context -> ST s ()
forall s a. STRef s a -> a -> ST s ()
ST.writeSTRef STRef s (ByteString (WordSize algorithm) context)
aRef (ByteString (WordSize algorithm) context -> ST s ())
-> ByteString (WordSize algorithm) context -> ST s ()
forall a b. (a -> b) -> a -> b
$ UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
temp1 UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
temp2 :: UInt (WordSize algorithm) Auto context)

    !ByteString (WordSize algorithm) context
a <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
aRef
    !ByteString (WordSize algorithm) context
b <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
bRef
    !ByteString (WordSize algorithm) context
c <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
cRef
    !ByteString (WordSize algorithm) context
d <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
dRef
    !ByteString (WordSize algorithm) context
e <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
eRef
    !ByteString (WordSize algorithm) context
f <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
fRef
    !ByteString (WordSize algorithm) context
g <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
gRef
    !ByteString (WordSize algorithm) context
h <- STRef s (ByteString (WordSize algorithm) context)
-> ST s (ByteString (WordSize algorithm) context)
forall s a. STRef s a -> ST s a
ST.readSTRef STRef s (ByteString (WordSize algorithm) context)
hRef

    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
a :: UInt (WordSize algorithm) Auto context)) Int
0
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
b :: UInt (WordSize algorithm) Auto context)) Int
1
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
c :: UInt (WordSize algorithm) Auto context)) Int
2
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
d :: UInt (WordSize algorithm) Auto context)) Int
3
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
e :: UInt (WordSize algorithm) Auto context)) Int
4
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
f :: UInt (WordSize algorithm) Auto context)) Int
5
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
g :: UInt (WordSize algorithm) Auto context)) Int
6
    MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
-> (ByteString (WordSize algorithm) context
    -> ByteString (WordSize algorithm) context)
-> Int
-> ST s ()
forall (m :: Type -> Type) a.
PrimMonad m =>
MVector (PrimState m) a -> (a -> a) -> Int -> m ()
VM.modify MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn (\ByteString (WordSize algorithm) context
w -> UInt (WordSize algorithm) 'Auto context
-> ByteString (WordSize algorithm) context
forall a b. Iso a b => a -> b
from (ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
w UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
-> UInt (WordSize algorithm) 'Auto context
forall a. AdditiveSemigroup a => a -> a -> a
+ ByteString (WordSize algorithm) context
-> UInt (WordSize algorithm) 'Auto context
forall a b. Iso a b => a -> b
from ByteString (WordSize algorithm) context
h :: UInt (WordSize algorithm) Auto context)) Int
7

    MVector s (ByteString (WordSize algorithm) context)
-> ST s (MVector s (ByteString (WordSize algorithm) context))
forall a. a -> ST s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure MVector s (ByteString (WordSize algorithm) context)
MVector
  (PrimState (ST s)) (ByteString (WordSize algorithm) context)
hn

    where
        rounds :: Int
        rounds :: Int
rounds = Vector (ByteString (WordSize algorithm) context) -> Int
forall a. Vector a -> Int
V.length (Vector (ByteString (WordSize algorithm) context) -> Int)
-> Vector (ByteString (WordSize algorithm) context) -> Int
forall a b. (a -> b) -> a -> b
$ forall (algorithm :: Symbol) (context :: (Type -> Type) -> Type).
AlgorithmSetup algorithm context =>
Vector (ByteString (WordSize algorithm) context)
roundConstants @algorithm @context