{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators       #-}
{-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters

module ZkFold.Symbolic.Algorithms.Hash.Blake2b where

import           Data.Bool                                         (bool)
import           Data.Constraint
import           Data.Constraint.Nat
import           Data.Constraint.Unsafe
import           Data.List                                         (foldl')
import           Data.Ratio                                        ((%))
import           Data.Vector                                       ((!), (//))
import qualified Data.Vector                                       as V
import           GHC.IsList                                        (IsList (..))
import qualified GHC.Num                                           as GHC
import           Prelude                                           hiding (Num (..), concat, divMod, length, mod,
                                                                    replicate, splitAt, truncate, (!!), (&&), (^))

import           ZkFold.Base.Algebra.Basic.Class                   (AdditiveGroup (..), AdditiveSemigroup (..),
                                                                    Exponent (..), FromConstant (..),
                                                                    MultiplicativeSemigroup (..), SemiEuclidean (..),
                                                                    divMod, one, zero, (-!))
import           ZkFold.Base.Algebra.Basic.Number
import qualified ZkFold.Base.Data.Vector                           as Vec
import           ZkFold.Prelude                                    (length, replicate, splitAt, (!!))
import           ZkFold.Symbolic.Algorithms.Hash.Blake2b.Constants (blake2b_iv, sigma)
import           ZkFold.Symbolic.Class                             (Symbolic)
import           ZkFold.Symbolic.Data.Bool                         (BoolType (..))
import           ZkFold.Symbolic.Data.ByteString                   (ByteString (..), Resize (..), ShiftBits (..),
                                                                    concat, reverseEndianness, toWords)
import           ZkFold.Symbolic.Data.Combinators                  (Iso (..), RegisterSize (..))
import           ZkFold.Symbolic.Data.UInt                         (UInt (..))


-- TODO: This module is not finished yet. The hash computation is not correct.

-- | BLAKE2b Cryptographic hash. Reference:
-- https://tools.ietf.org/html/rfc7693


pow2 :: forall a . FromConstant Natural a => Natural -> a
pow2 :: forall a. FromConstant Natural a => Natural -> a
pow2 = forall a b. FromConstant a b => a -> b
fromConstant @Natural (Natural -> a) -> (Natural -> Natural) -> Natural -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^)

shiftUIntR :: forall b . Symbolic b => UInt 64 Auto b -> Natural -> UInt 64 Auto b
shiftUIntR :: forall (b :: (Type -> Type) -> Type).
Symbolic b =>
UInt 64 'Auto b -> Natural -> UInt 64 'Auto b
shiftUIntR UInt 64 'Auto b
u Natural
n = forall a b. Iso a b => a -> b
from @_ @(UInt 64 Auto b) (ByteString 64 b -> UInt 64 'Auto b)
-> ByteString 64 b -> UInt 64 'Auto b
forall a b. (a -> b) -> a -> b
$ forall a b. Iso a b => a -> b
from @_ @(ByteString 64 b) UInt 64 'Auto b
u ByteString 64 b -> Natural -> ByteString 64 b
forall a. ShiftBits a => a -> Natural -> a
`shiftBitsR` Natural
n

shiftUIntL :: forall b . Symbolic b => UInt 64 Auto b -> Natural -> UInt 64 Auto b
shiftUIntL :: forall (b :: (Type -> Type) -> Type).
Symbolic b =>
UInt 64 'Auto b -> Natural -> UInt 64 'Auto b
shiftUIntL UInt 64 'Auto b
u Natural
n = UInt 64 'Auto b
u UInt 64 'Auto b -> UInt 64 'Auto b -> UInt 64 'Auto b
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> UInt 64 'Auto b
forall a. FromConstant Natural a => Natural -> a
pow2 Natural
n

xorUInt :: forall c . Symbolic c => UInt 64 Auto c ->  UInt 64 Auto c ->  UInt 64 Auto c
xorUInt :: forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
xorUInt UInt 64 'Auto c
u1 UInt 64 'Auto c
u2 = forall a b. Iso a b => a -> b
from @(ByteString 64 c) @(UInt 64 Auto c) (ByteString 64 c -> UInt 64 'Auto c)
-> ByteString 64 c -> UInt 64 'Auto c
forall a b. (a -> b) -> a -> b
$ UInt 64 'Auto c -> ByteString 64 c
forall a b. Iso a b => a -> b
from UInt 64 'Auto c
u1 ByteString 64 c -> ByteString 64 c -> ByteString 64 c
forall b. BoolType b => b -> b -> b
`xor` UInt 64 'Auto c -> ByteString 64 c
forall a b. Iso a b => a -> b
from UInt 64 'Auto c
u2

-- | state context
data Blake2bCtx c = Blake2bCtx
   { forall (c :: (Type -> Type) -> Type).
Blake2bCtx c -> Vector (UInt 64 'Auto c)
h :: V.Vector (UInt 64 Auto c) -- chained state 8
   , forall (c :: (Type -> Type) -> Type).
Blake2bCtx c -> Vector (UInt 64 'Auto c)
m :: V.Vector (UInt 64 Auto c) -- input buffer 16
   , forall (c :: (Type -> Type) -> Type).
Blake2bCtx c -> (Natural, Natural)
t :: (Natural, Natural)     -- total number of bytes
   }

-- | Cyclic right rotation.
rotr64 :: Symbolic c => (UInt 64 Auto c, Natural) -> UInt 64 Auto c
rotr64 :: forall (c :: (Type -> Type) -> Type).
Symbolic c =>
(UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
rotr64 (UInt 64 'Auto c
x, Natural
y) = (UInt 64 'Auto c
x UInt 64 'Auto c -> Natural -> UInt 64 'Auto c
forall (b :: (Type -> Type) -> Type).
Symbolic b =>
UInt 64 'Auto b -> Natural -> UInt 64 'Auto b
`shiftUIntR` Natural
y) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` (UInt 64 'Auto c
x UInt 64 'Auto c -> Natural -> UInt 64 'Auto c
forall (b :: (Type -> Type) -> Type).
Symbolic b =>
UInt 64 'Auto b -> Natural -> UInt 64 'Auto b
`shiftUIntL` (Natural
64 Natural -> Natural -> Natural
-! Natural
y))

-- | Little-endian byte access.
b2b_g :: forall c . Symbolic c =>
    V.Vector (UInt 64 Auto c) -> (Int, Int, Int, Int, UInt 64 Auto c, UInt 64 Auto c) -> V.Vector (UInt 64 Auto c)
b2b_g :: forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
v (Int
a, Int
b, Int
c, Int
d, UInt 64 'Auto c
x, UInt 64 'Auto c
y) =
    let va1 :: UInt 64 'Auto c
va1 = (Vector (UInt 64 'Auto c)
v Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
a) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveSemigroup a => a -> a -> a
+ (Vector (UInt 64 'Auto c)
v Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
b) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 64 'Auto c
x                 -- v[a] = v[a] + v[b] + x;         \
        vd1 :: UInt 64 'Auto c
vd1 = (UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
(UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
rotr64 ((Vector (UInt 64 'Auto c)
v Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
d) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` UInt 64 'Auto c
va1, Natural
32)    -- v[d] = ROTR64(v[d] ^ v[a], 32); \
        vc1 :: UInt 64 'Auto c
vc1 = (Vector (UInt 64 'Auto c)
v Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
c) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 64 'Auto c
vd1                         -- v[c] = v[c] + v[d];             \
        vb1 :: UInt 64 'Auto c
vb1 = (UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
(UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
rotr64 ((Vector (UInt 64 'Auto c)
v Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
b) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` UInt 64 'Auto c
vc1, Natural
24)    -- v[b] = ROTR64(v[b] ^ v[c], 24); \
        va2 :: UInt 64 'Auto c
va2 = UInt 64 'Auto c
va1 UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 64 'Auto c
vb1 UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 64 'Auto c
y                         -- v[a] = v[a] + v[b] + y;         \
        vd2 :: UInt 64 'Auto c
vd2 = (UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
(UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
rotr64 (UInt 64 'Auto c
vd1 UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` UInt 64 'Auto c
va2, Natural
16)        -- v[d] = ROTR64(v[d] ^ v[a], 16); \
        vc2 :: UInt 64 'Auto c
vc2 = UInt 64 'Auto c
vc1 UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 64 'Auto c
vd2                             -- v[c] = v[c] + v[d];             \
        vb2 :: UInt 64 'Auto c
vb2 = (UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
(UInt 64 'Auto c, Natural) -> UInt 64 'Auto c
rotr64 (UInt 64 'Auto c
vb1 UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` UInt 64 'Auto c
vc2, Natural
63)        -- v[b] = ROTR64(v[b] ^ v[c], 63);
    in Vector (UInt 64 'Auto c)
v Vector (UInt 64 'Auto c)
-> [(Int, UInt 64 'Auto c)] -> Vector (UInt 64 'Auto c)
forall a. Vector a -> [(Int, a)] -> Vector a
// [(Int
a, UInt 64 'Auto c
va2), (Int
b, UInt 64 'Auto c
vb2), (Int
c, UInt 64 'Auto c
vc2), (Int
d, UInt 64 'Auto c
vd2)]

-- | Compression function. "last" flag indicates the last block.
blake2b_compress :: forall c . Symbolic c => Blake2bCtx c -> Bool -> V.Vector (UInt 64 Auto c)
blake2b_compress :: forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
blake2b_compress Blake2bCtx{Vector (UInt 64 'Auto c)
h :: forall (c :: (Type -> Type) -> Type).
Blake2bCtx c -> Vector (UInt 64 'Auto c)
h :: Vector (UInt 64 'Auto c)
h, Vector (UInt 64 'Auto c)
m :: forall (c :: (Type -> Type) -> Type).
Blake2bCtx c -> Vector (UInt 64 'Auto c)
m :: Vector (UInt 64 'Auto c)
m, (Natural, Natural)
t :: forall (c :: (Type -> Type) -> Type).
Blake2bCtx c -> (Natural, Natural)
t :: (Natural, Natural)
t} Bool
lastBlock =
    let v' :: Vector (UInt 64 'Auto c)
v'  = Vector (UInt 64 'Auto c)
h Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> Vector (UInt 64 'Auto c)
forall a. Vector a -> Vector a -> Vector a
V.++ Vector (UInt 64 'Auto c)
forall x (v :: Type -> Type).
(FromConstant Natural x, IsList (v x), Item (v x) ~ x) =>
v x
blake2b_iv -- init work variables
        v'' :: Vector (UInt 64 'Auto c)
v'' = Vector (UInt 64 'Auto c)
v' Vector (UInt 64 'Auto c)
-> [(Int, UInt 64 'Auto c)] -> Vector (UInt 64 'Auto c)
forall a. Vector a -> [(Int, a)] -> Vector a
V.// [ (Int
12, (Vector (UInt 64 'Auto c)
v' Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
12) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` Natural -> UInt 64 'Auto c
forall a b. FromConstant a b => a -> b
fromConstant ((Natural, Natural) -> Natural
forall a b. (a, b) -> a
fst (Natural, Natural)
t))  -- low word of the offset
                      , (Int
13, (Vector (UInt 64 'Auto c)
v' Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
13) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` Natural -> UInt 64 'Auto c
forall a b. FromConstant a b => a -> b
fromConstant ((Natural, Natural) -> Natural
forall a b. (a, b) -> b
snd (Natural, Natural)
t))] -- high word of the offset

        v0 :: Vector (UInt 64 'Auto c)
v0 = if Bool
lastBlock                                               -- last block flag set ?
                then Vector (UInt 64 'Auto c)
v'' Vector (UInt 64 'Auto c)
-> [(Int, UInt 64 'Auto c)] -> Vector (UInt 64 'Auto c)
forall a. Vector a -> [(Int, a)] -> Vector a
// [(Int
14, (Vector (UInt 64 'Auto c)
v'' Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
14) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` UInt 64 'Auto c -> UInt 64 'Auto c
forall a. AdditiveGroup a => a -> a
negate UInt 64 'Auto c
forall a. MultiplicativeMonoid a => a
one)]     -- Invert all bits
                else Vector (UInt 64 'Auto c)
v''

        hashRound :: Vector (UInt 64 'Auto c) -> Int -> Vector (UInt 64 'Auto c)
hashRound Vector (UInt 64 'Auto c)
w0 Int
i = Vector (UInt 64 'Auto c)
w8
            where
                s :: Vector Int
s  = Vector (Vector Int)
forall (v :: Type -> Type).
(IsList (v Int), IsList (v (v Int)), Item (v Int) ~ Int,
 Item (v (v Int)) ~ v Int) =>
v (v Int)
sigma Vector (Vector Int) -> Int -> Vector Int
forall a. Vector a -> Int -> a
! Int
i
                w1 :: Vector (UInt 64 'Auto c)
w1 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w0 (Int
0, Int
4,  Int
8, Int
12, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
0),  Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
1))
                w2 :: Vector (UInt 64 'Auto c)
w2 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w1 (Int
1, Int
5,  Int
9, Int
13, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
2),  Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
3))
                w3 :: Vector (UInt 64 'Auto c)
w3 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w2 (Int
2, Int
6, Int
10, Int
14, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
4),  Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
5))
                w4 :: Vector (UInt 64 'Auto c)
w4 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w3 (Int
3, Int
7, Int
11, Int
15, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
6),  Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
7))
                w5 :: Vector (UInt 64 'Auto c)
w5 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w4 (Int
0, Int
5, Int
10, Int
15, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
8),  Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
9))
                w6 :: Vector (UInt 64 'Auto c)
w6 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w5 (Int
1, Int
6, Int
11, Int
12, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
10), Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
11))
                w7 :: Vector (UInt 64 'Auto c)
w7 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w6 (Int
2, Int
7,  Int
8, Int
13, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
12), Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
13))
                w8 :: Vector (UInt 64 'Auto c)
w8 = Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector (UInt 64 'Auto c)
-> (Int, Int, Int, Int, UInt 64 'Auto c, UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c)
b2b_g Vector (UInt 64 'Auto c)
w7 (Int
3, Int
4,  Int
9, Int
14, Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
14), Vector (UInt 64 'Auto c)
m Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Vector Int
s Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! Int
15))

        v1 :: Vector (UInt 64 'Auto c)
v1 = (Vector (UInt 64 'Auto c) -> Int -> Vector (UInt 64 'Auto c))
-> Vector (UInt 64 'Auto c)
-> Vector Int
-> Vector (UInt 64 'Auto c)
forall a b. (a -> b -> a) -> a -> Vector b -> a
V.foldl Vector (UInt 64 'Auto c) -> Int -> Vector (UInt 64 'Auto c)
hashRound Vector (UInt 64 'Auto c)
v0 (Vector Int -> Vector (UInt 64 'Auto c))
-> Vector Int -> Vector (UInt 64 'Auto c)
forall a b. (a -> b) -> a -> b
$ [Item (Vector Int)] -> Vector Int
forall l. IsList l => [Item l] -> l
fromList [Int
Item (Vector Int)
0..Int
Item (Vector Int)
11] -- twelve rounds
    in ((Int, UInt 64 'Auto c) -> UInt 64 'Auto c)
-> Vector (Int, UInt 64 'Auto c) -> Vector (UInt 64 'Auto c)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
i, UInt 64 'Auto c
hi) -> UInt 64 'Auto c
hi UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` (Vector (UInt 64 'Auto c)
v1 Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
i) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` (Vector (UInt 64 'Auto c)
v1 Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
GHC.+ Int
8))) (Vector Int
-> Vector (UInt 64 'Auto c) -> Vector (Int, UInt 64 'Auto c)
forall a b. Vector a -> Vector b -> Vector (a, b)
V.zip ([Item (Vector Int)] -> Vector Int
forall l. IsList l => [Item l] -> l
fromList [Int
Item (Vector Int)
0..Int
Item (Vector Int)
7]) Vector (UInt 64 'Auto c)
h)

blake2b' :: forall bb' kk' ll' nn' c .
    ( Symbolic c
    , KnownNat bb'
    , KnownNat kk'
    , KnownNat ll'
    , KnownNat nn'
    ) => [V.Vector (UInt 64 Auto c)] -> ByteString (8 * nn') c
blake2b' :: forall (bb' :: Natural) (kk' :: Natural) (ll' :: Natural)
       (nn' :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat bb', KnownNat kk', KnownNat ll',
 KnownNat nn') =>
[Vector (UInt 64 'Auto c)] -> ByteString (8 * nn') c
blake2b' [Vector (UInt 64 'Auto c)]
d =
    let bb :: Natural
bb = forall (n :: Natural). KnownNat n => Natural
value @bb'
        ll :: Natural
ll = forall (n :: Natural). KnownNat n => Natural
value @ll'
        kk :: Natural
kk = forall (n :: Natural). KnownNat n => Natural
value @kk'
        nn :: Natural
nn = forall (n :: Natural). KnownNat n => Natural
value @nn'
        dd :: Natural
dd = Natural -> Natural -> Bool -> Natural
forall a. a -> a -> Bool -> a
bool (Ratio Natural -> Natural
forall b. Integral b => Ratio Natural -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Natural
kk Natural -> Natural -> Ratio Natural
forall a. Integral a => a -> a -> Ratio a
% Natural
bb) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Ratio Natural -> Natural
forall b. Integral b => Ratio Natural -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Natural
ll Natural -> Natural -> Ratio Natural
forall a. Integral a => a -> a -> Ratio a
% Natural
bb)) Natural
1 (Natural
kk Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 Bool -> Bool -> Bool
forall b. BoolType b => b -> b -> b
&& Natural
ll Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0) :: Natural

        toOffset :: forall x . (FromConstant Natural x) => Natural -> (x, x)
        toOffset :: forall x. FromConstant Natural x => Natural -> (x, x)
toOffset Natural
x = let (Natural
hi, Natural
lo) = Natural
x Natural -> Natural -> (Natural, Natural)
forall a. SemiEuclidean a => a -> a -> (a, a)
`divMod` Natural -> Natural
forall a. FromConstant Natural a => Natural -> a
pow2 Natural
64 in (Natural -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
lo, Natural -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
hi)

        h :: Vector (UInt 64 'Auto c)
h = Vector (UInt 64 'Auto c)
forall x (v :: Type -> Type).
(FromConstant Natural x, IsList (v x), Item (v x) ~ x) =>
v x
blake2b_iv :: V.Vector (UInt 64 Auto c)

        -- Parameter block p[0]
        h' :: Vector (UInt 64 'Auto c)
h' = Vector (UInt 64 'Auto c)
h Vector (UInt 64 'Auto c)
-> [(Int, UInt 64 'Auto c)] -> Vector (UInt 64 'Auto c)
forall a. Vector a -> [(Int, a)] -> Vector a
// [(Int
0, (Vector (UInt 64 'Auto c)
h Vector (UInt 64 'Auto c) -> Int -> UInt 64 'Auto c
forall a. Vector a -> Int -> a
! Int
0) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
0x01010000 UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` (Natural -> UInt 64 'Auto c
forall a b. FromConstant a b => a -> b
fromConstant Natural
kk UInt 64 'Auto c -> Natural -> UInt 64 'Auto c
forall (b :: (Type -> Type) -> Type).
Symbolic b =>
UInt 64 'Auto b -> Natural -> UInt 64 'Auto b
`shiftUIntR` Natural
8) UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
UInt 64 'Auto c -> UInt 64 'Auto c -> UInt 64 'Auto c
`xorUInt` Natural -> UInt 64 'Auto c
forall a b. FromConstant a b => a -> b
fromConstant Natural
nn)]

        -- Process padded key and data blocks
        h'' :: Vector (UInt 64 'Auto c)
h'' = if Natural
dd Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
1
            then (Vector (UInt 64 'Auto c) -> Natural -> Vector (UInt 64 'Auto c))
-> Vector (UInt 64 'Auto c)
-> [Natural]
-> Vector (UInt 64 'Auto c)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Vector (UInt 64 'Auto c)
acc Natural
i -> Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
blake2b_compress (Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> (Natural, Natural) -> Blake2bCtx c
forall (c :: (Type -> Type) -> Type).
Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> (Natural, Natural) -> Blake2bCtx c
Blake2bCtx Vector (UInt 64 'Auto c)
acc ([Vector (UInt 64 'Auto c)]
d [Vector (UInt 64 'Auto c)] -> Natural -> Vector (UInt 64 'Auto c)
forall a. [a] -> Natural -> a
!! Natural
i) (forall x. FromConstant Natural x => Natural -> (x, x)
toOffset @Natural (Natural -> (Natural, Natural)) -> Natural -> (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ (Natural
i Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
bb)) Bool
False) Vector (UInt 64 'Auto c)
h' [Natural
0 .. Natural
dd Natural -> Natural -> Natural
-! Natural
2]
            else Vector (UInt 64 'Auto c)
h'

        -- Final round
        h''' :: Vector (UInt 64 'Auto c)
h''' = if Natural
kk Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0
            then Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
blake2b_compress (Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> (Natural, Natural) -> Blake2bCtx c
forall (c :: (Type -> Type) -> Type).
Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> (Natural, Natural) -> Blake2bCtx c
Blake2bCtx Vector (UInt 64 'Auto c)
h'' ([Vector (UInt 64 'Auto c)]
d [Vector (UInt 64 'Auto c)] -> Natural -> Vector (UInt 64 'Auto c)
forall a. [a] -> Natural -> a
!! (Natural
dd Natural -> Natural -> Natural
-! Natural
1)) (forall x. FromConstant Natural x => Natural -> (x, x)
toOffset @Natural (Natural -> (Natural, Natural)) -> Natural -> (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ Natural
ll)) Bool
True
            else Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
Blake2bCtx c -> Bool -> Vector (UInt 64 'Auto c)
blake2b_compress (Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> (Natural, Natural) -> Blake2bCtx c
forall (c :: (Type -> Type) -> Type).
Vector (UInt 64 'Auto c)
-> Vector (UInt 64 'Auto c) -> (Natural, Natural) -> Blake2bCtx c
Blake2bCtx Vector (UInt 64 'Auto c)
h'' ([Vector (UInt 64 'Auto c)]
d [Vector (UInt 64 'Auto c)] -> Natural -> Vector (UInt 64 'Auto c)
forall a. [a] -> Natural -> a
!! (Natural
dd Natural -> Natural -> Natural
-! Natural
1)) (forall x. FromConstant Natural x => Natural -> (x, x)
toOffset @Natural (Natural -> (Natural, Natural)) -> Natural -> (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ Natural
ll Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
bb)) Bool
True

        bs :: ByteString (64 * 8) c
bs = forall (wordSize :: Natural) (k :: Natural)
       (c :: (Type -> Type) -> Type) (m :: Natural) {n :: Natural}.
(Symbolic c, KnownNat wordSize, n ~ (k * wordSize),
 (m * 8) ~ wordSize) =>
ByteString n c -> ByteString n c
reverseEndianness @64 (ByteString (64 * 8) c -> ByteString (64 * 8) c)
-> ByteString (64 * 8) c -> ByteString (64 * 8) c
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 @64 (Vector 8 (ByteString 64 c) -> ByteString (8 * 64) c)
-> Vector 8 (ByteString 64 c) -> ByteString (8 * 64) c
forall a b. (a -> b) -> a -> b
$ forall (size :: Natural) a. [a] -> Vector size a
Vec.unsafeToVector @8 ([ByteString 64 c] -> Vector 8 (ByteString 64 c))
-> [ByteString 64 c] -> Vector 8 (ByteString 64 c)
forall a b. (a -> b) -> a -> b
$ (UInt 64 'Auto c -> ByteString 64 c)
-> [UInt 64 'Auto c] -> [ByteString 64 c]
forall a b. (a -> b) -> [a] -> [b]
map UInt 64 'Auto c -> ByteString 64 c
forall a b. Iso a b => a -> b
from ([UInt 64 'Auto c] -> [ByteString 64 c])
-> [UInt 64 'Auto c] -> [ByteString 64 c]
forall a b. (a -> b) -> a -> b
$ Vector (UInt 64 'Auto c) -> [Item (Vector (UInt 64 'Auto c))]
forall l. IsList l => l -> [Item l]
toList Vector (UInt 64 'Auto c)
h''' :: ByteString (64 * 8) c
    in forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (8 * n) => r) -> r
with8n @nn' (ByteString 512 c -> ByteString (8 * nn') c
forall a b. Resize a b => a -> b
resize ByteString 512 c
ByteString (64 * 8) c
bs)

type ExtensionBits inputLen = 8 * (128 - Mod inputLen 128)
type ExtendedInputByteString inputLen c = ByteString (8 * inputLen + ExtensionBits inputLen) c

withExtensionBits :: forall n {r}. KnownNat n => (KnownNat (ExtensionBits n) => r) -> r
withExtensionBits :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (ExtensionBits n) => r) -> r
withExtensionBits = ((() :: Constraint)
 :- Assert
      (OrdCond (CmpNat (Mod n 128) 128) 'True 'True 'False)
      (TypeError ...))
-> (Assert
      (OrdCond (CmpNat (Mod n 128) 128) 'True 'True 'False)
      (TypeError ...) =>
    (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (m :: Natural) (n :: Natural). (1 <= n) :- (Mod m n <= n)
modBound @n @128) ((Assert
    (OrdCond (CmpNat (Mod n 128) 128) 'True 'True 'False)
    (TypeError ...) =>
  (KnownNat (ExtensionBits n) => r) -> r)
 -> (KnownNat (ExtensionBits n) => r) -> r)
-> (Assert
      (OrdCond (CmpNat (Mod n 128) 128) 'True 'True 'False)
      (TypeError ...) =>
    (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                        ((KnownNat n, KnownNat 128, () :: Constraint)
 :- KnownNat (Mod n 128))
-> (KnownNat (Mod n 128) => (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
modNat @n @128) ((KnownNat (Mod n 128) => (KnownNat (ExtensionBits n) => r) -> r)
 -> (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (Mod n 128) => (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                            ((KnownNat 128, KnownNat (Mod n 128),
  Assert
    (OrdCond (CmpNat (Mod n 128) 128) 'True 'True 'False)
    (TypeError ...))
 :- KnownNat (128 - Mod n 128))
-> (KnownNat (128 - Mod n 128) =>
    (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
minusNat @128 @(Mod n 128)) ((KnownNat (128 - Mod n 128) =>
  (KnownNat (ExtensionBits n) => r) -> r)
 -> (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (128 - Mod n 128) =>
    (KnownNat (ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                                ((KnownNat 8, KnownNat (128 - Mod n 128))
 :- KnownNat (ExtensionBits n))
-> (KnownNat (ExtensionBits n) => r) -> r
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 @8 @(128 - Mod n 128))

withExtendedInputByteString :: forall n {r}. KnownNat n => (KnownNat (8 * n + ExtensionBits n) => r) -> r
withExtendedInputByteString :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((8 * n) + ExtensionBits n) => r) -> r
withExtendedInputByteString = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (ExtensionBits n) => r) -> r
withExtensionBits @n ((KnownNat (ExtensionBits n) =>
  (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
 -> (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
-> (KnownNat (ExtensionBits n) =>
    (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
-> (KnownNat ((8 * n) + ExtensionBits n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                                    ((KnownNat 8, KnownNat n) :- KnownNat (8 * n))
-> (KnownNat (8 * n) =>
    (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
-> (KnownNat ((8 * n) + ExtensionBits n) => r)
-> r
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 @8 @n) ((KnownNat (8 * n) =>
  (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
 -> (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
-> (KnownNat (8 * n) =>
    (KnownNat ((8 * n) + ExtensionBits n) => r) -> r)
-> (KnownNat ((8 * n) + ExtensionBits n) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                                        ((KnownNat (8 * n), KnownNat (ExtensionBits n))
 :- KnownNat ((8 * n) + ExtensionBits n))
-> (KnownNat ((8 * n) + ExtensionBits n) => r) -> r
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)
plusNat @(8 * n) @(ExtensionBits n))

with8nLessExt :: forall n {r}. KnownNat n => (8 * n <= 8 * n + ExtensionBits n => r) -> r
with8nLessExt :: forall (n :: Natural) {r}.
KnownNat n =>
(((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r
with8nLessExt = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((8 * n) + ExtensionBits n) => r) -> r
withExtendedInputByteString @n ((KnownNat ((8 * n) + ExtensionBits n) =>
  (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
 -> (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
-> (KnownNat ((8 * n) + ExtensionBits n) =>
    (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
-> (((8 * n) <= ((8 * n) + ExtensionBits n)) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                    Dict
  (Assert
     (OrdCond (CmpNat 0 (ExtensionBits n)) 'True 'True 'False)
     (TypeError ...))
-> (Assert
      (OrdCond (CmpNat 0 (ExtensionBits n)) 'True 'True 'False)
      (TypeError ...) =>
    (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
-> (((8 * n) <= ((8 * n) + ExtensionBits n)) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Natural). Dict (0 <= a)
zeroLe @(ExtensionBits n)) ((Assert
    (OrdCond (CmpNat 0 (ExtensionBits n)) 'True 'True 'False)
    (TypeError ...) =>
  (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
 -> (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
-> (Assert
      (OrdCond (CmpNat 0 (ExtensionBits n)) 'True 'True 'False)
      (TypeError ...) =>
    (((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r)
-> (((8 * n) <= ((8 * n) + ExtensionBits n)) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                        (Assert
   (OrdCond (CmpNat 0 (ExtensionBits n)) 'True 'True 'False)
   (TypeError ...)
 :- Assert
      (OrdCond
         (CmpNat (8 * n) ((8 * n) + ExtensionBits n)) 'True 'True 'False)
      (TypeError ...))
-> (Assert
      (OrdCond
         (CmpNat (8 * n) ((8 * n) + ExtensionBits n)) 'True 'True 'False)
      (TypeError ...) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Natural) (b :: Natural) (c :: Natural).
(b <= c) :- ((a + b) <= (a + c))
plusMonotone2 @(8 * n) @0 @(ExtensionBits n))

with8n  :: forall n {r}. KnownNat n => (KnownNat (8 * n) => r) -> r
with8n :: forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (8 * n) => r) -> r
with8n = ((KnownNat 8, KnownNat n) :- KnownNat (8 * n))
-> (KnownNat (8 * n) => r) -> r
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 @8 @n)

blake2bDivConstraint :: forall n. Dict (Div (8 * n + ExtensionBits n) 64 * 64 ~ 8 * n + ExtensionBits n)
blake2bDivConstraint :: forall (n :: Natural).
Dict
  ((Div ((8 * n) + ExtensionBits n) 64 * 64)
   ~ ((8 * n) + ExtensionBits n))
blake2bDivConstraint = Dict
  ((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
   ~ ((8 * n) + (8 * (128 - Mod n 128))))
forall (c :: Constraint). Dict c
unsafeAxiom

withBlake2bDivConstraint :: forall n {r}. (Div (8 * n + ExtensionBits n) 64 * 64 ~ 8 * n + ExtensionBits n => r) -> r
withBlake2bDivConstraint :: forall (n :: Natural) {r}.
(((Div ((8 * n) + ExtensionBits n) 64 * 64)
  ~ ((8 * n) + ExtensionBits n)) =>
 r)
-> r
withBlake2bDivConstraint =  Dict
  ((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
   ~ ((8 * n) + (8 * (128 - Mod n 128))))
-> (((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
     ~ ((8 * n) + (8 * (128 - Mod n 128)))) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Dict
   ((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
    ~ ((8 * n) + (8 * (128 - Mod n 128))))
 -> (((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
      ~ ((8 * n) + (8 * (128 - Mod n 128)))) =>
     r)
 -> r)
-> Dict
     ((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
      ~ ((8 * n) + (8 * (128 - Mod n 128))))
-> (((Div ((8 * n) + (8 * (128 - Mod n 128))) 64 * 64)
     ~ ((8 * n) + (8 * (128 - Mod n 128)))) =>
    r)
-> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
Dict
  ((Div ((8 * n) + ExtensionBits n) 64 * 64)
   ~ ((8 * n) + ExtensionBits n))
blake2bDivConstraint @n

withConstraints :: forall n {r}. KnownNat n => (
    ( KnownNat (8 * n)
    , KnownNat (ExtensionBits n)
    , KnownNat (8 * n + ExtensionBits n)
    , 8 * n <= 8 * n + ExtensionBits n
    , Div (8 * n + ExtensionBits n) 64 * 64 ~ 8 * n + ExtensionBits n) => r) -> r
withConstraints :: forall (n :: Natural) {r}.
KnownNat n =>
((KnownNat (8 * n), KnownNat (ExtensionBits n),
  KnownNat ((8 * n) + ExtensionBits n),
  (8 * n) <= ((8 * n) + ExtensionBits n),
  (Div ((8 * n) + ExtensionBits n) 64 * 64)
  ~ ((8 * n) + ExtensionBits n)) =>
 r)
-> r
withConstraints = forall (n :: Natural) {r}.
KnownNat n =>
(((8 * n) <= ((8 * n) + ExtensionBits n)) => r) -> r
with8nLessExt @n ((((8 * n) <= ((8 * n) + ExtensionBits n)) =>
  ((KnownNat (8 * n), KnownNat (ExtensionBits n),
    KnownNat ((8 * n) + ExtensionBits n),
    (8 * n) <= ((8 * n) + ExtensionBits n),
    (Div ((8 * n) + ExtensionBits n) 64 * 64)
    ~ ((8 * n) + ExtensionBits n)) =>
   r)
  -> r)
 -> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
 -> r)
-> (((8 * n) <= ((8 * n) + ExtensionBits n)) =>
    ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
    -> r)
-> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
     KnownNat ((8 * n) + ExtensionBits n),
     (8 * n) <= ((8 * n) + ExtensionBits n),
     (Div ((8 * n) + ExtensionBits n) 64 * 64)
     ~ ((8 * n) + ExtensionBits n)) =>
    r)
-> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((8 * n) + ExtensionBits n) => r) -> r
withExtendedInputByteString @n ((KnownNat ((8 * n) + ExtensionBits n) =>
  ((KnownNat (8 * n), KnownNat (ExtensionBits n),
    KnownNat ((8 * n) + ExtensionBits n),
    (8 * n) <= ((8 * n) + ExtensionBits n),
    (Div ((8 * n) + ExtensionBits n) 64 * 64)
    ~ ((8 * n) + ExtensionBits n)) =>
   r)
  -> r)
 -> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
 -> r)
-> (KnownNat ((8 * n) + ExtensionBits n) =>
    ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
    -> r)
-> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
     KnownNat ((8 * n) + ExtensionBits n),
     (8 * n) <= ((8 * n) + ExtensionBits n),
     (Div ((8 * n) + ExtensionBits n) 64 * 64)
     ~ ((8 * n) + ExtensionBits n)) =>
    r)
-> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (ExtensionBits n) => r) -> r
withExtensionBits @n ((KnownNat (ExtensionBits n) =>
  ((KnownNat (8 * n), KnownNat (ExtensionBits n),
    KnownNat ((8 * n) + ExtensionBits n),
    (8 * n) <= ((8 * n) + ExtensionBits n),
    (Div ((8 * n) + ExtensionBits n) 64 * 64)
    ~ ((8 * n) + ExtensionBits n)) =>
   r)
  -> r)
 -> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
 -> r)
-> (KnownNat (ExtensionBits n) =>
    ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
    -> r)
-> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
     KnownNat ((8 * n) + ExtensionBits n),
     (8 * n) <= ((8 * n) + ExtensionBits n),
     (Div ((8 * n) + ExtensionBits n) 64 * 64)
     ~ ((8 * n) + ExtensionBits n)) =>
    r)
-> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat (8 * n) => r) -> r
with8n @n ((KnownNat (8 * n) =>
  ((KnownNat (8 * n), KnownNat (ExtensionBits n),
    KnownNat ((8 * n) + ExtensionBits n),
    (8 * n) <= ((8 * n) + ExtensionBits n),
    (Div ((8 * n) + ExtensionBits n) 64 * 64)
    ~ ((8 * n) + ExtensionBits n)) =>
   r)
  -> r)
 -> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
 -> r)
-> (KnownNat (8 * n) =>
    ((KnownNat (8 * n), KnownNat (ExtensionBits n),
      KnownNat ((8 * n) + ExtensionBits n),
      (8 * n) <= ((8 * n) + ExtensionBits n),
      (Div ((8 * n) + ExtensionBits n) 64 * 64)
      ~ ((8 * n) + ExtensionBits n)) =>
     r)
    -> r)
-> ((KnownNat (8 * n), KnownNat (ExtensionBits n),
     KnownNat ((8 * n) + ExtensionBits n),
     (8 * n) <= ((8 * n) + ExtensionBits n),
     (Div ((8 * n) + ExtensionBits n) 64 * 64)
     ~ ((8 * n) + ExtensionBits n)) =>
    r)
-> r
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) {r}.
(((Div ((8 * n) + ExtensionBits n) 64 * 64)
  ~ ((8 * n) + ExtensionBits n)) =>
 r)
-> r
withBlake2bDivConstraint @n


blake2b :: forall keyLen inputLen outputLen c n.
    ( Symbolic c
    , KnownNat keyLen
    , KnownNat inputLen
    , KnownNat outputLen
    , n ~ (8 * inputLen + ExtensionBits inputLen)
    ) => Natural -> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c
blake2b :: forall (keyLen :: Natural) (inputLen :: Natural)
       (outputLen :: Natural) (c :: (Type -> Type) -> Type)
       (n :: Natural).
(Symbolic c, KnownNat keyLen, KnownNat inputLen,
 KnownNat outputLen,
 n ~ ((8 * inputLen) + ExtensionBits inputLen)) =>
Natural
-> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c
blake2b Natural
key ByteString (8 * inputLen) c
input =
    let input' :: Vector (Div n 64) (UInt 64 'Auto c)
input' = forall (n :: Natural) {r}.
KnownNat n =>
((KnownNat (8 * n), KnownNat (ExtensionBits n),
  KnownNat ((8 * n) + ExtensionBits n),
  (8 * n) <= ((8 * n) + ExtensionBits n),
  (Div ((8 * n) + ExtensionBits n) 64 * 64)
  ~ ((8 * n) + ExtensionBits n)) =>
 r)
-> r
withConstraints @inputLen (((KnownNat (8 * inputLen), KnownNat (ExtensionBits inputLen),
   KnownNat ((8 * inputLen) + ExtensionBits inputLen),
   (8 * inputLen) <= ((8 * inputLen) + ExtensionBits inputLen),
   (Div ((8 * inputLen) + ExtensionBits inputLen) 64 * 64)
   ~ ((8 * inputLen) + ExtensionBits inputLen)) =>
  Vector (Div n 64) (UInt 64 'Auto c))
 -> Vector (Div n 64) (UInt 64 'Auto c))
-> ((KnownNat (8 * inputLen), KnownNat (ExtensionBits inputLen),
     KnownNat ((8 * inputLen) + ExtensionBits inputLen),
     (8 * inputLen) <= ((8 * inputLen) + ExtensionBits inputLen),
     (Div ((8 * inputLen) + ExtensionBits inputLen) 64 * 64)
     ~ ((8 * inputLen) + ExtensionBits inputLen)) =>
    Vector (Div n 64) (UInt 64 'Auto c))
-> Vector (Div n 64) (UInt 64 'Auto c)
forall a b. (a -> b) -> a -> b
$
                    ByteString 64 c -> UInt 64 'Auto c
forall a b. Iso a b => a -> b
from (ByteString 64 c -> UInt 64 'Auto c)
-> Vector (Div n 64) (ByteString 64 c)
-> Vector (Div n 64) (UInt 64 'Auto c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f 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 n 64) @64 (ByteString (Div n 64 * 64) c
 -> Vector (Div n 64) (ByteString 64 c))
-> ByteString (Div n 64 * 64) c
-> Vector (Div n 64) (ByteString 64 c)
forall a b. (a -> b) -> a -> b
$
                    forall (wordSize :: Natural) (k :: Natural)
       (c :: (Type -> Type) -> Type) (m :: Natural) {n :: Natural}.
(Symbolic c, KnownNat wordSize, n ~ (k * wordSize),
 (m * 8) ~ wordSize) =>
ByteString n c -> ByteString n c
reverseEndianness @64 (ByteString (Div n 64 * 64) c -> ByteString (Div n 64 * 64) c)
-> ByteString (Div n 64 * 64) c -> ByteString (Div n 64 * 64) c
forall a b. (a -> b) -> a -> b
$
                    (ExtendedInputByteString inputLen c
 -> Natural -> ByteString (Div n 64 * 64) c)
-> Natural
-> ExtendedInputByteString inputLen c
-> ByteString (Div n 64 * 64) c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ByteString n c -> Natural -> ByteString n c
ExtendedInputByteString inputLen c
-> Natural -> ByteString (Div n 64 * 64) c
forall a. ShiftBits a => a -> Natural -> a
rotateBitsL (forall (n :: Natural). KnownNat n => Natural
value @(ExtensionBits inputLen)) (ExtendedInputByteString inputLen c
 -> ByteString (Div n 64 * 64) c)
-> ExtendedInputByteString inputLen c
-> ByteString (Div n 64 * 64) c
forall a b. (a -> b) -> a -> b
$
                    forall a b. Resize a b => a -> b
resize @_ @(ExtendedInputByteString inputLen c) ByteString (8 * inputLen) c
input ) :: Vec.Vector (Div n 64) (UInt 64 Auto c)

        key' :: UInt 64 'Auto c
key'    = forall a b. FromConstant a b => a -> b
fromConstant @_ Natural
key :: UInt 64 Auto c
        input'' :: [UInt 64 'Auto c]
input'' = if forall (n :: Natural). KnownNat n => Natural
value @keyLen Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0
            then UInt 64 'Auto c
key' UInt 64 'Auto c -> [UInt 64 'Auto c] -> [UInt 64 'Auto c]
forall a. a -> [a] -> [a]
: Vector (Div n 64) (UInt 64 'Auto c) -> [UInt 64 'Auto c]
forall (size :: Natural) a. Vector size a -> [a]
Vec.fromVector Vector (Div n 64) (UInt 64 'Auto c)
input'
            else Vector (Div n 64) (UInt 64 'Auto c) -> [UInt 64 'Auto c]
forall (size :: Natural) a. Vector size a -> [a]
Vec.fromVector Vector (Div n 64) (UInt 64 'Auto c)
input'

        padding :: Natural
padding = [UInt 64 'Auto c] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [UInt 64 'Auto c]
input'' Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
16
        input''' :: [UInt 64 'Auto c]
input''' = [UInt 64 'Auto c]
input'' [UInt 64 'Auto c] -> [UInt 64 'Auto c] -> [UInt 64 'Auto c]
forall a. [a] -> [a] -> [a]
++ Natural -> UInt 64 'Auto c -> [UInt 64 'Auto c]
forall a. Natural -> a -> [a]
replicate (Natural
16 Natural -> Natural -> Natural
-! Natural
padding) UInt 64 'Auto c
forall a. AdditiveMonoid a => a
zero

        toBlocks :: [w] -> [V.Vector w]
        toBlocks :: forall w. [w] -> [Vector w]
toBlocks [] = []
        toBlocks [w]
xs = let ([w]
a, [w]
b) = Natural -> [w] -> ([w], [w])
forall a. Natural -> [a] -> ([a], [a])
splitAt Natural
16 [w]
xs in [Item (Vector w)] -> Vector w
forall l. IsList l => [Item l] -> l
fromList [w]
[Item (Vector w)]
a Vector w -> [Vector w] -> [Vector w]
forall a. a -> [a] -> [a]
: [w] -> [Vector w]
forall w. [w] -> [Vector w]
toBlocks [w]
b

        d :: [Vector (UInt 64 'Auto c)]
d = [UInt 64 'Auto c] -> [Vector (UInt 64 'Auto c)]
forall w. [w] -> [Vector w]
toBlocks [UInt 64 'Auto c]
input'''
    in forall (bb' :: Natural) (kk' :: Natural) (ll' :: Natural)
       (nn' :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat bb', KnownNat kk', KnownNat ll',
 KnownNat nn') =>
[Vector (UInt 64 'Auto c)] -> ByteString (8 * nn') c
blake2b'
        @128       -- block size bb'
        @keyLen    -- key length kk'
        @inputLen  -- input length ll'
        [Vector (UInt 64 'Auto c)]
d

-- | Hash a `ByteString` using the Blake2b-224 hash function.
blake2b_224 :: forall inputLen c.
    ( Symbolic c
    , KnownNat inputLen
    ) => ByteString (8 * inputLen) c -> ByteString 224 c
blake2b_224 :: forall (inputLen :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat inputLen) =>
ByteString (8 * inputLen) c -> ByteString 224 c
blake2b_224 = forall (keyLen :: Natural) (inputLen :: Natural)
       (outputLen :: Natural) (c :: (Type -> Type) -> Type)
       (n :: Natural).
(Symbolic c, KnownNat keyLen, KnownNat inputLen,
 KnownNat outputLen,
 n ~ ((8 * inputLen) + ExtensionBits inputLen)) =>
Natural
-> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c
blake2b @0 @inputLen @28 (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
0)

-- | Hash a `ByteString` using the Blake2b-256 hash function.
blake2b_256 :: forall inputLen c.
    ( Symbolic c
    , KnownNat inputLen
    ) => ByteString (8 * inputLen) c -> ByteString 256 c
blake2b_256 :: forall (inputLen :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat inputLen) =>
ByteString (8 * inputLen) c -> ByteString 256 c
blake2b_256 = forall (keyLen :: Natural) (inputLen :: Natural)
       (outputLen :: Natural) (c :: (Type -> Type) -> Type)
       (n :: Natural).
(Symbolic c, KnownNat keyLen, KnownNat inputLen,
 KnownNat outputLen,
 n ~ ((8 * inputLen) + ExtensionBits inputLen)) =>
Natural
-> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c
blake2b @0 @inputLen @32 (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
0)

-- | Hash a `ByteString` using the Blake2b-256 hash function.
blake2b_512 :: forall inputLen c.
    ( Symbolic c
    , KnownNat inputLen
    ) => ByteString (8 * inputLen) c -> ByteString 512 c
blake2b_512 :: forall (inputLen :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat inputLen) =>
ByteString (8 * inputLen) c -> ByteString 512 c
blake2b_512 = forall (keyLen :: Natural) (inputLen :: Natural)
       (outputLen :: Natural) (c :: (Type -> Type) -> Type)
       (n :: Natural).
(Symbolic c, KnownNat keyLen, KnownNat inputLen,
 KnownNat outputLen,
 n ~ ((8 * inputLen) + ExtensionBits inputLen)) =>
Natural
-> ByteString (8 * inputLen) c -> ByteString (8 * outputLen) c
blake2b @0 @inputLen @64 Natural
0