{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Algorithms.Hash.MiMC where

import           Data.Foldable                                  (toList)
import           Data.List.NonEmpty                             (NonEmpty ((:|)), nonEmpty)
import           Data.Proxy                                     (Proxy (..))
import           Numeric.Natural                                (Natural)
import           Prelude                                        hiding (Eq (..), Num (..), any, length, not, (!!), (/),
                                                                 (^), (||))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Data.HFunctor                      (hmap)
import           ZkFold.Base.Data.Package                       (unpacked)
import           ZkFold.Symbolic.Algorithms.Hash.MiMC.Constants (mimcConstants)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.FieldElement

-- | MiMC-2n/n (Feistel) hash function.
-- See https://eprint.iacr.org/2016/492.pdf, page 5
mimcHash2 :: (FromConstant a x, Ring x) => [a] -> a -> x -> x -> x
mimcHash2 :: forall a x. (FromConstant a x, Ring x) => [a] -> a -> x -> x -> x
mimcHash2 ((a -> x) -> [a] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map a -> x
forall a b. FromConstant a b => a -> b
fromConstant -> [x]
xs) (a -> x
forall a b. FromConstant a b => a -> b
fromConstant -> x
k) = case [x] -> Maybe (NonEmpty x)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([x] -> [x]
forall a. [a] -> [a]
reverse [x]
xs) of
    Just NonEmpty x
cs -> NonEmpty x -> x -> x -> x
go NonEmpty x
cs
    Maybe (NonEmpty x)
Nothing -> [Char] -> x -> x -> x
forall a. HasCallStack => [Char] -> a
error [Char]
"mimcHash: empty list"
    where
        go :: NonEmpty x -> x -> x -> x
go (x
c :| [x]
cs) x
xL x
xR =
          let t5 :: x
t5 = (x
xL x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
k x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
c) x -> Natural -> x
forall a b. Exponent a b => a -> b -> a
^ (Natural
5 :: Natural)
           in case [x] -> Maybe (NonEmpty x)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [x]
cs of
              Just NonEmpty x
cs' -> NonEmpty x -> x -> x -> x
go NonEmpty x
cs' (x
xR x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
t5) x
xL
              Maybe (NonEmpty x)
Nothing  -> x
xR x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
t5

mimcHashN :: (FromConstant a x, Ring x) => [a] -> a -> [x] -> x
mimcHashN :: forall a x. (FromConstant a x, Ring x) => [a] -> a -> [x] -> x
mimcHashN [a]
xs a
k = [x] -> x
go
  where
    go :: [x] -> x
go [x]
zs = case [x]
zs of
      []          -> [a] -> a -> x -> x -> x
forall a x. (FromConstant a x, Ring x) => [a] -> a -> x -> x -> x
mimcHash2 [a]
xs a
k x
forall a. AdditiveMonoid a => a
zero x
forall a. AdditiveMonoid a => a
zero
      [x
z]         -> [a] -> a -> x -> x -> x
forall a x. (FromConstant a x, Ring x) => [a] -> a -> x -> x -> x
mimcHash2 [a]
xs a
k x
forall a. AdditiveMonoid a => a
zero x
z
      [x
zL, x
zR]    -> [a] -> a -> x -> x -> x
forall a x. (FromConstant a x, Ring x) => [a] -> a -> x -> x -> x
mimcHash2 [a]
xs a
k x
zL x
zR
      (x
zL:x
zR:[x]
zs') -> [x] -> x
go ([a] -> a -> x -> x -> x
forall a x. (FromConstant a x, Ring x) => [a] -> a -> x -> x -> x
mimcHash2 [a]
xs a
k x
zL x
zR x -> [x] -> [x]
forall a. a -> [a] -> [a]
: [x]
zs')

hash :: forall context x a .
    ( SymbolicOutput x
    , BaseField context ~ a
    , Context x ~ context
    ) => x -> FieldElement context
hash :: forall (context :: (Type -> Type) -> Type) x a.
(SymbolicOutput x, BaseField context ~ a, Context x ~ context) =>
x -> FieldElement context
hash = [a] -> a -> [FieldElement context] -> FieldElement context
forall a x. (FromConstant a x, Ring x) => [a] -> a -> [x] -> x
mimcHashN [a]
forall a. FromConstant Integer a => [a]
mimcConstants (a
forall a. AdditiveMonoid a => a
zero :: a) ([FieldElement context] -> FieldElement context)
-> (x -> [FieldElement context]) -> x -> FieldElement context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (context Par1 -> FieldElement context)
-> [context Par1] -> [FieldElement context]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap context Par1 -> FieldElement context
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement ([context Par1] -> [FieldElement context])
-> (x -> [context Par1]) -> x -> [FieldElement context]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. context [] -> [context Par1]
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Package c, Functor f) =>
c f -> f (c Par1)
unpacked (context [] -> [context Par1])
-> (x -> context []) -> x -> [context Par1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Layout x a -> [a]) -> context (Layout x) -> context []
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 Layout x a -> [a]
forall a. Layout x a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (context (Layout x) -> context [])
-> (x -> context (Layout x)) -> x -> context []
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> Proxy context -> context (Layout x))
-> Proxy context -> x -> context (Layout x)
forall a b c. (a -> b -> c) -> b -> a -> c
flip x -> Proxy context -> context (Layout x)
x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize Proxy context
forall {k} (t :: k). Proxy t
Proxy