{-# LANGUAGE TypeOperators #-}

module ZkFold.Symbolic.Data.Hash where

import           Control.Monad                    (return)
import           Data.Function                    (const, ($))
import           Data.Proxy                       (Proxy (..))
import           Data.Traversable                 (traverse)
import           Data.Type.Equality               (type (~))
import           GHC.Generics                     (Generic, Par1 (..), (:*:) (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Control.HApplicative (hunit)
import           ZkFold.Symbolic.Class            (Symbolic (fromCircuitF, witnessF), fromCircuit2F)
import           ZkFold.Symbolic.Data.Bool        (Bool (..))
import           ZkFold.Symbolic.Data.Class       (SymbolicData (..), SymbolicOutput)
import           ZkFold.Symbolic.Data.Eq          (Eq, (==))
import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (Payloaded))
import           ZkFold.Symbolic.MonadCircuit     (constraint, unconstrained)

-- | A generic hashing interface for Symbolic DSL.
-- 'h' is the result of the hashing algorithm;
-- 'a' is the datatype being hashed.
--
-- The relationship between datatypes and hashes is many-to-many
-- so there's no functional dependency in either direction.
class Hashable h a where
  -- | Hashing algorithm itself.
  hasher :: a -> h

-- | An invertible hash 'h' of a symbolic datatype 'a'.
data Hash h a = Hash
  { forall h a. Hash h a -> h
hHash  :: h
  , forall h a.
Hash h a -> Payloaded (Layout a :*: Payload a) (Context h)
hValue :: Payloaded (Layout a :*: Payload a) (Context h)
  }
  deriving ((forall x. Hash h a -> Rep (Hash h a) x)
-> (forall x. Rep (Hash h a) x -> Hash h a) -> Generic (Hash h a)
forall x. Rep (Hash h a) x -> Hash h a
forall x. Hash h a -> Rep (Hash h a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall h a x. Rep (Hash h a) x -> Hash h a
forall h a x. Hash h a -> Rep (Hash h a) x
$cfrom :: forall h a x. Hash h a -> Rep (Hash h a) x
from :: forall x. Hash h a -> Rep (Hash h a) x
$cto :: forall h a x. Rep (Hash h a) x -> Hash h a
to :: forall x. Rep (Hash h a) x -> Hash h a
Generic)

instance (SymbolicOutput h, SymbolicOutput a) => SymbolicData (Hash h a)
instance (SymbolicInput h, SymbolicInput a) => SymbolicInput (Hash h a)

-- | Restorably hash the data.
hash :: (Hashable h a, SymbolicOutput a, Context h ~ Context a) => a -> Hash h a
hash :: forall h a.
(Hashable h a, SymbolicOutput a, Context h ~ Context a) =>
a -> Hash h a
hash a
a = h -> Payloaded (Layout a :*: Payload a) (Context h) -> Hash h a
forall h a.
h -> Payloaded (Layout a :*: Payload a) (Context h) -> Hash h a
Hash (a -> h
forall h a. Hashable h a => a -> h
hasher a
a) (Payloaded (Layout a :*: Payload a) (Context h) -> Hash h a)
-> Payloaded (Layout a :*: Payload a) (Context h) -> Hash h a
forall a b. (a -> b) -> a -> b
$
  (:*:) (Layout a) (Payload a) (WitnessField (Context a))
-> Payloaded (Layout a :*: Payload a) (Context a)
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded (Context a (Layout a) -> Layout a (WitnessField (Context a))
forall (f :: Type -> Type).
Functor f =>
Context a f -> f (WitnessField (Context a))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
c f -> f (WitnessField c)
witnessF (a -> Support a -> Context a (Layout a)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize a
a Proxy (Context a)
Support a
forall {k} (t :: k). Proxy t
Proxy) Layout a (WitnessField (Context a))
-> Payload a (WitnessField (Context a))
-> (:*:) (Layout a) (Payload a) (WitnessField (Context a))
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: a -> Support a -> Payload a (WitnessField (Context a))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload a
a Proxy (Context a)
Support a
forall {k} (t :: k). Proxy t
Proxy)

-- | Restore the data which were hashed.
preimage ::
  forall h a c .
  ( Hashable h a, SymbolicOutput a, Context h ~ c, Context a ~ c
  , Eq (Bool c) h) => Hash h a -> a
preimage :: forall h a (c :: (Type -> Type) -> Type).
(Hashable h a, SymbolicOutput a, Context h ~ c, Context a ~ c,
 Eq (Bool c) h) =>
Hash h a -> a
preimage Hash {h
Payloaded (Layout a :*: Payload a) (Context h)
hHash :: forall h a. Hash h a -> h
hValue :: forall h a.
Hash h a -> Payloaded (Layout a :*: Payload a) (Context h)
hHash :: h
hValue :: Payloaded (Layout a :*: Payload a) (Context h)
..} =
  let Payloaded (Layout a (WitnessField (Context h))
l :*: Payload a (WitnessField (Context h))
p) = Payloaded (Layout a :*: Payload a) (Context h)
hValue
      a
raw :: a = (Support a -> (c (Layout a), Payload a (WitnessField c))) -> a
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context a ~ c) =>
(Support a -> (c (Layout a), Payload a (WitnessField c))) -> a
restore ((Support a -> (c (Layout a), Payload a (WitnessField c))) -> a)
-> (Support a -> (c (Layout a), Payload a (WitnessField c))) -> a
forall a b. (a -> b) -> a -> b
$ (c (Layout a), Payload a (WitnessField c))
-> Proxy c -> (c (Layout a), Payload a (WitnessField c))
forall a b. a -> b -> a
const
        ( c U1 -> CircuitFun '[U1] (Layout a) c -> c (Layout a)
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF c U1
forall {k} (c :: (k -> Type) -> Type). HApplicative c => c U1
hunit (CircuitFun '[U1] (Layout a) c -> c (Layout a))
-> CircuitFun '[U1] (Layout a) c -> c (Layout a)
forall a b. (a -> b) -> a -> b
$ m (Layout a i) -> U1 i -> m (Layout a i)
forall a b. a -> b -> a
const ((WitnessField c -> m i)
-> Layout a (WitnessField c) -> m (Layout a i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Layout a a -> f (Layout a b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained Layout a (WitnessField c)
Layout a (WitnessField (Context h))
l)
        , Payload a (WitnessField c)
Payload a (WitnessField (Context h))
p)
      Bool c Par1
b = a -> h
forall h a. Hashable h a => a -> h
hasher a
raw h -> h -> Bool c
forall b a. Eq b a => a -> a -> b
== h
hHash
   in (Support a -> (c (Layout a), Payload a (WitnessField c))) -> a
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context a ~ c) =>
(Support a -> (c (Layout a), Payload a (WitnessField c))) -> a
restore ((Support a -> (c (Layout a), Payload a (WitnessField c))) -> a)
-> (Support a -> (c (Layout a), Payload a (WitnessField c))) -> a
forall a b. (a -> b) -> a -> b
$ \Support a
s ->
      ( c (Layout a)
-> c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Layout a, Par1] (Layout a) i m)
-> c (Layout a)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F (a -> Support a -> Context a (Layout a)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize a
raw Support a
s) c Par1
b ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Layout a, Par1] (Layout a) i m)
 -> c (Layout a))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Layout a, Par1] (Layout a) i m)
-> c (Layout a)
forall a b. (a -> b) -> a -> b
$ \Layout a i
r (Par1 i
i) -> do
          ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)
          Layout a i -> m (Layout a i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Layout a i
r
      , a -> Support a -> Payload a (WitnessField (Context a))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload a
raw Support a
s)