{-# 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)
class Hashable h a where
hasher :: a -> h
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)
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)
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)