diff --git a/symbolic-base/src/ZkFold/ArithmeticCircuit/Context.hs b/symbolic-base/src/ZkFold/ArithmeticCircuit/Context.hs index 8317491b8..117098171 100644 --- a/symbolic-base/src/ZkFold/ArithmeticCircuit/Context.hs +++ b/symbolic-base/src/ZkFold/ArithmeticCircuit/Context.hs @@ -1,26 +1,26 @@ {-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE NoStarIsType #-} module ZkFold.ArithmeticCircuit.Context where -import Control.Applicative (liftA2, pure) +import Control.Applicative (liftA2, pure, (<*>)) import Control.DeepSeq (NFData, NFData1, liftRnf, rnf, rwhnf) import Control.Monad.State (State, modify, runState, state) import Data.Aeson ((.:), (.=)) import qualified Data.Aeson.Types as Aeson import Data.Binary (Binary) -import Data.Bool (Bool (..), otherwise, (&&)) +import Data.Bool (Bool (..), (&&)) import Data.ByteString (ByteString) import Data.Either (Either (..)) -import Data.Eq ((==)) +import Data.Eq (Eq, (==)) import Data.Foldable (Foldable, fold, foldl', for_, toList) import Data.Function (flip, ($), (.)) import Data.Functor (Functor, fmap, (<$>), (<&>)) import Data.Functor.Classes (Show1, liftShowList, liftShowsPrec) import Data.Functor.Rep -import Data.Kind (Type) import Data.List.Infinite (Infinite) import qualified Data.List.Infinite as I import Data.Map (Map) @@ -38,23 +38,21 @@ import qualified Data.Set as S import Data.Traversable (Traversable, traverse) import Data.Tuple (fst, snd, uncurry) import Data.Type.Equality (type (~)) -import Data.Typeable (Typeable) import GHC.Generics (Generic, Par1 (..), U1 (..), (:*:) (..)) import Optics (over, set, zoom) import Text.Show -import qualified Type.Reflection as R import Prelude (error, seq) import ZkFold.Algebra.Class import ZkFold.Algebra.Number import ZkFold.Algebra.Polynomial.Multivariate (Poly, var) -import ZkFold.ArithmeticCircuit.Lookup (FunctionId (..), LookupType (..)) import ZkFold.ArithmeticCircuit.MerkleHash (MerkleHash (..), merkleHash, runHash) import ZkFold.ArithmeticCircuit.Var import ZkFold.ArithmeticCircuit.Witness (WitnessF (..)) import ZkFold.ArithmeticCircuit.WitnessEstimation (Partial (..), UVar (..)) import ZkFold.Control.HApplicative (HApplicative, hliftA2, hpure) import ZkFold.Data.Binary (fromByteString, toByteString) +import ZkFold.Data.FromList (FromList, fromList) import ZkFold.Data.HFunctor (HFunctor, hmap) import ZkFold.Data.HFunctor.Classes import ZkFold.Data.Package (Package, packWith, unpackWith) @@ -90,10 +88,8 @@ data CircuitFold a instance NFData a => NFData (CircuitFold a) where rnf CircuitFold {..} = rnf foldCount `seq` liftRnf rnf foldSeed -data LookupFunction a - = forall f g. - (Representable f, Traversable g, Typeable f, Typeable g, Binary (Rep f)) => - LookupFunction (forall x. PrimeField x => f x -> g x) +newtype LookupFunction a = LookupFunction + {runLookupFunction :: forall x. (PrimeField x, Algebra a x) => [x] -> [x]} instance NFData (LookupFunction a) where rnf = rwhnf @@ -102,31 +98,34 @@ type FunctionRegistry a = Map ByteString (LookupFunction a) appendFunction :: forall f g a - . (Representable f, Typeable f, Binary (Rep f)) - => (Traversable g, Typeable g, Arithmetic a) - => (forall x. PrimeField x => f x -> g x) + . (Representable f, FromList f, Binary (Rep f)) + => (Foldable g, Arithmetic a, Binary a) + => (forall x. (PrimeField x, Algebra a x) => f x -> g x) -> FunctionRegistry a - -> (FunctionId (f a -> g a), FunctionRegistry a) + -> (ByteString, FunctionRegistry a) appendFunction f r = let functionId = runHash @(Just (Order a)) $ sum (f $ tabulate merkleHash) - in (FunctionId functionId, M.insert functionId (LookupFunction f) r) - -lookupFunction - :: forall f g (a :: Type) - . (Typeable f, Typeable g) - => FunctionRegistry a - -> FunctionId (f a -> g a) - -> (forall x. PrimeField x => f x -> g x) -lookupFunction m (FunctionId i) = case m M.! i of - LookupFunction f -> cast1 . f . cast1 - where - cast1 :: forall h k b. (Typeable h, Typeable k) => h b -> k b - cast1 x - | Just R.HRefl <- th `R.eqTypeRep` tk = x - | otherwise = error "types are not equal" - where - th = R.typeRep :: R.TypeRep h - tk = R.typeRep :: R.TypeRep k + in (functionId, M.insert functionId (LookupFunction (toList . \x -> f $ fromList x)) r) + +data LookupType a + = LTRanges (Set (a, a)) + | LTProduct (LookupType a) (LookupType a) + | LTPlot ByteString (LookupType a) + deriving + ( Aeson.FromJSON + , Aeson.FromJSONKey + , Aeson.ToJSON + , Aeson.ToJSONKey + , Eq + , Generic + , NFData + , Ord + , Show + ) + +asRange :: LookupType a -> Maybe (Set (a, a)) +asRange (LTRanges rs) = Just rs +asRange _ = Nothing -- | Circuit context in the form of a system of polynomial constraints. data CircuitContext a o = CircuitContext @@ -352,10 +351,10 @@ instance zoom #acSystem . modify $ M.insert (witToVar (p at)) (p $ evalVar var) - lookupConstraint vars lt = do + lookupConstraint vars ltable = do vs <- traverse prepare (toList vars) - zoom #acLookup . modify $ - MM.insertWith S.union (LookupType lt) (S.singleton vs) + lt <- lookupType ltable + zoom #acLookup . modify $ MM.insertWith S.union lt (S.singleton vs) pure () where prepare (LinVar k x b) | k == one && b == zero = pure x @@ -367,7 +366,16 @@ instance constraint (($ toVar v) - ($ src)) pure v - registerFunction f = zoom #acLookupFunction $ state (appendFunction f) +-- | Translates a lookup table into a lookup type, +-- storing all lookup functions in a circuit. +lookupType + :: (Arithmetic a, Binary a) + => LookupTable a f -> State (CircuitContext a o) (LookupType a) +lookupType (Ranges rs) = pure (LTRanges rs) +lookupType (Product t u) = LTProduct <$> lookupType t <*> lookupType u +lookupType (Plot f t) = do + funcId <- zoom #acLookupFunction $ state (appendFunction f) + LTPlot funcId <$> lookupType t -- | Generates new variable index given a witness for it. -- diff --git a/symbolic-base/src/ZkFold/ArithmeticCircuit/Desugaring.hs b/symbolic-base/src/ZkFold/ArithmeticCircuit/Desugaring.hs index a9847deac..c81accd59 100644 --- a/symbolic-base/src/ZkFold/ArithmeticCircuit/Desugaring.hs +++ b/symbolic-base/src/ZkFold/ArithmeticCircuit/Desugaring.hs @@ -16,8 +16,7 @@ import Data.Tuple (fst, uncurry) import Prelude (error) import ZkFold.Algebra.Class -import ZkFold.ArithmeticCircuit.Context (CircuitContext, acLookup) -import ZkFold.ArithmeticCircuit.Lookup (asRange) +import ZkFold.ArithmeticCircuit.Context (CircuitContext, acLookup, asRange) import ZkFold.ArithmeticCircuit.Var (toVar) import ZkFold.Prelude (assert, length) import ZkFold.Symbolic.Class (Arithmetic) diff --git a/symbolic-base/src/ZkFold/ArithmeticCircuit/Experimental.hs b/symbolic-base/src/ZkFold/ArithmeticCircuit/Experimental.hs index 1e0257c5b..daf145d26 100644 --- a/symbolic-base/src/ZkFold/ArithmeticCircuit/Experimental.hs +++ b/symbolic-base/src/ZkFold/ArithmeticCircuit/Experimental.hs @@ -10,15 +10,13 @@ module ZkFold.ArithmeticCircuit.Experimental where import Control.Applicative (pure) import Control.DeepSeq (NFData (..), NFData1, liftRnf, rwhnf) import Control.Monad (unless) -import Control.Monad.State (State, gets, modify', runState, state) +import Control.Monad.State (State, gets, modify', runState) import Data.Binary (Binary) -import Data.ByteString (ByteString) import Data.Eq (Eq (..)) import Data.Foldable (Foldable (..), any, for_) import Data.Function (flip, on, ($), (.)) import Data.Functor (Functor, fmap) import Data.Functor.Rep (Rep, Representable) -import Data.Map (Map) import qualified Data.Map as M import qualified Data.Map.Monoidal as MM import Data.Maybe (Maybe (..)) @@ -40,16 +38,14 @@ import ZkFold.ArithmeticCircuit (ArithmeticCircuit, optimize, solder) import ZkFold.ArithmeticCircuit.Children (children) import ZkFold.ArithmeticCircuit.Context ( CircuitContext, - LookupFunction (LookupFunction), acLookup, acSystem, acWitness, - appendFunction, crown, emptyContext, + lookupType, witToVar, ) -import ZkFold.ArithmeticCircuit.Lookup (LookupTable, LookupType (..)) import ZkFold.ArithmeticCircuit.Var (NewVar (..), Var) import ZkFold.ArithmeticCircuit.Witness (WitnessF (..)) import ZkFold.Control.HApplicative (HApplicative (..)) @@ -70,7 +66,7 @@ import ZkFold.Symbolic.Data.Class ( restore, ) import ZkFold.Symbolic.Data.Input (isValid) -import ZkFold.Symbolic.MonadCircuit (MonadCircuit (..), Witness (..)) +import ZkFold.Symbolic.MonadCircuit (LookupTable, MonadCircuit (..), Witness (..)) ---------------------- Efficient "list" concatenation -------------------------- @@ -105,12 +101,8 @@ data LookupEntry a v ------------- Box of constraints supporting efficient concatenation ------------ --- After #573, can be made even more declarative --- by getting rid of 'cbLkpFuns' field. --- Can then be used for new public Symbolic API (see 'constrain' below)! data ConstraintBox a v = MkCBox { cbPolyCon :: AppList (Polynomial a v) - , cbLkpFuns :: Map ByteString (LookupFunction a) , cbLookups :: AppList (LookupEntry a v) } deriving (Generic, NFData) @@ -192,9 +184,6 @@ instance where unconstrained = pure . fromConstant constraint c = modify' \cb -> cb {cbPolyCon = MkPolynomial c `app` cbPolyCon cb} - registerFunction f = state \(!cb) -> - let (i, r') = appendFunction f (cbLkpFuns cb) - in (i, cb {cbLkpFuns = r'}) lookupConstraint c t = modify' \cb -> cb {cbLookups = LEntry c t `app` cbLookups cb} ------------------------- Optimized compilation function ----------------------- @@ -240,14 +229,12 @@ compile = unless isDone' do constraint (\x -> runPolynomial c (x . pure . elHash)) for_ (children asWitness) work - for_ cbLkpFuns \(LookupFunction f) -> do - _ <- registerFunction f - pure () for_ cbLookups \(LEntry l t) -> do + lt <- lookupType t isDone' <- gets ( any (S.member $ toList $ fmap elHash l) - . (MM.!? LookupType t) + . (MM.!? lt) . acLookup ) unless isDone' do diff --git a/symbolic-base/src/ZkFold/ArithmeticCircuit/Lookup.hs b/symbolic-base/src/ZkFold/ArithmeticCircuit/Lookup.hs deleted file mode 100644 index 0f4a30dda..000000000 --- a/symbolic-base/src/ZkFold/ArithmeticCircuit/Lookup.hs +++ /dev/null @@ -1,97 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeOperators #-} - -module ZkFold.ArithmeticCircuit.Lookup where - -import Control.DeepSeq (NFData (..)) -import Data.Aeson -import Data.Aeson.TH (deriveToJSON) -import Data.Bool (otherwise) -import Data.ByteString (ByteString) -import Data.Eq (Eq (..)) -import Data.Foldable (Foldable) -import Data.Functor (Functor) -import Data.Maybe (Maybe (..)) -import Data.Ord (Ord (..)) -import Data.Semigroup (Semigroup (..)) -import Data.Set (Set) -import Data.Typeable (Typeable) -import qualified Data.Typeable as T -import GHC.Generics (Generic, Par1, (:*:)) -import qualified Type.Reflection as R -import Prelude (Show, undefined) - -import ZkFold.Data.Binary () - -newtype FunctionId f = FunctionId {funcHash :: ByteString} - deriving (Eq, Generic, NFData, Ord, Show, ToJSON) - --- | @LookupTable a f@ is a type of compact lookup table descriptions using ideas from relational algebra. --- @a@ is a base field type, @f@ is a functor such that @f a@ is a type whose subset this lookup table describes. -data LookupTable a f where - -- | @Ranges@ describes a set of disjoint segments of the base field. - Ranges :: Set (a, a) -> LookupTable a Par1 - -- | @Product t u@ is a cartesian product of tables @t@ and @u@. - Product :: LookupTable a f -> LookupTable a g -> LookupTable a (f :*: g) - -- | @Plot f x@ is a plot of a function @f@ with @x@ as a domain. - Plot - :: (Functor f, Functor g, Typeable f, Typeable g) - => FunctionId (f a -> g a) -> LookupTable a f -> LookupTable a (f :*: g) - -deriving instance Eq a => Eq (LookupTable a f) - -deriving instance Ord a => Ord (LookupTable a f) - -deriving instance Show a => Show (LookupTable a f) - -$(deriveToJSON defaultOptions ''LookupTable) - -instance NFData a => NFData (LookupTable a f) where - rnf (Ranges rs) = rnf rs - rnf (Product t1 t2) = rnf (t1, t2) - rnf (Plot i t) = rnf (i, t) - -instance (ToJSON a, ToJSONKey a) => ToJSONKey (LookupTable a f) - -data LookupType a - = forall f. (Foldable f, Typeable f) => LookupType {lTable :: LookupTable a f} - -asRange :: LookupType a -> Maybe (Set (a, a)) -asRange (LookupType (Ranges rs)) = Just rs -asRange _ = Nothing - -castT - :: forall f g a - . (Typeable f, Typeable g) - => LookupTable a f -> Maybe (LookupTable a g) -castT x - | Just R.HRefl <- tf `R.eqTypeRep` tg = Just x - | otherwise = Nothing - where - tf = R.typeRep :: R.TypeRep f - tg = R.typeRep :: R.TypeRep g - -deriving instance Show a => Show (LookupType a) - -instance Eq a => Eq (LookupType a) where - LookupType lt1 == LookupType lt2 = Just lt1 == castT lt2 - -instance Ord a => Ord (LookupType a) where - LookupType lt1 `compare` LookupType lt2 = - (T.typeRep lt1 `compare` T.typeRep lt2) - <> (Just lt1 `compare` castT lt2) - -instance ToJSON a => ToJSON (LookupType a) where - toJSON (LookupType lt) = toJSON lt - -instance (ToJSON a, ToJSONKey a) => ToJSONKey (LookupType a) - --- TODO: Finish this instance -instance FromJSON a => FromJSON (LookupType a) where - parseJSON = undefined - -instance (FromJSON a, FromJSONKey a) => FromJSONKey (LookupType a) - -instance NFData a => NFData (LookupType a) where - rnf (LookupType tbl) = rnf tbl diff --git a/symbolic-base/src/ZkFold/ArithmeticCircuit/Optimization.hs b/symbolic-base/src/ZkFold/ArithmeticCircuit/Optimization.hs index 62c0c4e27..b1d310591 100644 --- a/symbolic-base/src/ZkFold/ArithmeticCircuit/Optimization.hs +++ b/symbolic-base/src/ZkFold/ArithmeticCircuit/Optimization.hs @@ -32,9 +32,10 @@ import ZkFold.ArithmeticCircuit.Context ( CircuitContext (..), CircuitFold (..), Constraint, + LookupType, + asRange, witToVar, ) -import ZkFold.ArithmeticCircuit.Lookup (LookupType, asRange) import ZkFold.ArithmeticCircuit.Var (NewVar (..)) import ZkFold.Data.Binary (fromByteString) import ZkFold.Symbolic.Class (Arithmetic) diff --git a/symbolic-base/src/ZkFold/ArithmeticCircuit/Var.hs b/symbolic-base/src/ZkFold/ArithmeticCircuit/Var.hs index 8dbfcc91b..8e9723ea5 100644 --- a/symbolic-base/src/ZkFold/ArithmeticCircuit/Var.hs +++ b/symbolic-base/src/ZkFold/ArithmeticCircuit/Var.hs @@ -4,6 +4,7 @@ module ZkFold.ArithmeticCircuit.Var where +import ByteString.Aeson.Orphans () import Control.Applicative (Applicative, pure, (<*>)) import Control.DeepSeq (NFData) import Control.Monad (Monad, ap, (>>=)) diff --git a/symbolic-base/src/ZkFold/Data/FromList.hs b/symbolic-base/src/ZkFold/Data/FromList.hs new file mode 100644 index 000000000..7157562ea --- /dev/null +++ b/symbolic-base/src/ZkFold/Data/FromList.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Data.FromList where + +import Control.Applicative (liftA2) +import Control.Monad.State (State, runState, state) +import GHC.Err (error) +import GHC.Generics (Par1 (..), (:*:) (..)) + +class FromList f where + parseList :: State [a] (f a) + +instance FromList Par1 where + parseList = state \case + [] -> error "parseList @Par1: empty list" + (x : xs) -> (Par1 x, xs) + +instance (FromList f, FromList g) => FromList (f :*: g) where + parseList = liftA2 (:*:) parseList parseList + +fromList :: FromList f => [a] -> f a +fromList input = case runState parseList input of + (result, []) -> result + _ -> error "fromList: unconsumed elements" diff --git a/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation.hs b/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation.hs index e7d2a3b9d..cde147935 100644 --- a/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation.hs +++ b/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation.hs @@ -4,6 +4,7 @@ module ZkFold.Protocol.Plonkup.Relation where +import Control.Applicative (pure) import Data.Aeson ((.=)) import qualified Data.Aeson as Aeson import Data.Binary (Binary) @@ -15,14 +16,14 @@ import Data.Functor (fmap, (<$>)) import Data.Functor.Rep (Rep, Representable, tabulate) import Data.List (map, (++)) import qualified Data.List as L -import Data.Map (elems) +import Data.Map (elems, (!)) import qualified Data.Map.Monoidal as M import Data.Maybe (Maybe (..), fromJust) import Data.Monoid (Sum (..)) +import Data.Semigroup ((<>)) import qualified Data.Set as S import Data.Vector (Vector) import qualified Data.Vector as V -import GHC.Generics (Par1 (..), (:*:) (..)) import GHC.IsList (fromList) import Test.QuickCheck (Arbitrary (..)) import Text.Show (Show (..)) @@ -34,8 +35,7 @@ import ZkFold.Algebra.Permutation (Permutation, fromCycles, mkIndexPartition) import ZkFold.Algebra.Polynomial.Multivariate (evalMonomial, evalPolynomial, var) import ZkFold.Algebra.Polynomial.Univariate (UnivariateRingPolyVec (..), toPolyVec) import ZkFold.ArithmeticCircuit (ArithmeticCircuit (..), acSizeN, witnessGenerator) -import ZkFold.ArithmeticCircuit.Context (CircuitContext (..), lookupFunction) -import ZkFold.ArithmeticCircuit.Lookup (LookupTable (..), LookupType (LookupType)) +import ZkFold.ArithmeticCircuit.Context (CircuitContext (..), LookupFunction (..), LookupType (..)) import ZkFold.ArithmeticCircuit.Var (Var, evalVar, toVar) import ZkFold.Prelude (length, replicate, uncurry3) import ZkFold.Protocol.Plonkup.Internal (PlonkupPermutationSize) @@ -143,53 +143,52 @@ toPlonkupRelation !ac = toTriple [!x, !y, !z] = (x, y, z) toTriple ws = P.error ("Expected list of length 1-3, got " ++ show (length ws)) - unfold :: LookupTable a f -> (Natural, (Vector a -> Vector a) -> f (Vector a)) - unfold (Ranges !rs) = + unfold :: LookupType a -> (Natural, (Vector a -> Vector a) -> [Vector a]) + unfold (LTRanges !rs) = let !segs = S.toList rs in ( sum [toConstant (hi - lo + one) | (lo, hi) <- segs] - , Par1 . ($ V.concat [V.enumFromTo lo hi | (lo, hi) <- segs]) + , pure . ($ V.concat [V.enumFromTo lo hi | (lo, hi) <- segs]) ) - unfold (Product !t !u) = + unfold (LTProduct !t !u) = let (!m, ts) = unfold t (!k, us) = unfold u in ( m * k , \f -> ts (f . V.concatMap (V.replicate (P.fromIntegral k))) - :*: us (f . V.concat . L.replicate (P.fromIntegral m)) + <> us (f . V.concat . L.replicate (P.fromIntegral m)) ) - unfold (Plot !g !t) = + unfold (LTPlot !g !t) = let (!k, ts) = unfold t - g' = lookupFunction (acLookupFunction (acContext ac)) g + LookupFunction g' = acLookupFunction (acContext ac) ! g in ( k , \f -> let !ts' = ts id - in f <$> (ts' :*: fmap (toVector k) (g' $ fromVector <$> ts')) + in f <$> (ts' <> fmap (toVector k) (g' $ fromVector <$> ts')) ) lkup - :: Foldable f - => LookupTable a f + :: LookupType a -> [[Var a]] -> ([LookupConstraint i a], Sum Natural, (Vector a, Vector a, Vector a)) lkup !lt !vs = let (!k, !ts) = unfold lt in ( L.map (uncurry3 LookupConstraint . toTriple) vs , Sum k - , toTriple $ toList (ts id) + , toTriple (ts id) ) -- Lookup queries. (!xLookup, Sum !nLookup, (!xs, !ys, !zs)) = case M.assocs (acLookup $ acContext ac) of [] -> ([], 0, (V.empty, V.empty, V.empty)) - [(LookupType lt, vs)] -> lkup lt [L.map toVar v | v <- S.toList vs] + [(lt, vs)] -> lkup lt [L.map toVar v | v <- S.toList vs] asscs -> flip foldMap (L.zip [(0 :: Natural) ..] asscs) $ -- \^ Folding concatenates tuples pointwise, so: -- \* lists of constraints get concatenated -- \* vectors of values get concatenated, too -- Just as planned! - \(fromConstant -> i, (LookupType lt, vs)) -> + \(fromConstant -> i, (lt, vs)) -> lkup - (Ranges (S.singleton (i, i)) `Product` lt) + (LTRanges (S.singleton (i, i)) `LTProduct` lt) [fromConstant i : L.map toVar v | v <- S.toList vs] -- NOTE we use constant variables -- to encode № of a lookup table diff --git a/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation/LookupVector.hs b/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation/LookupVector.hs index 710e1f872..dab6536eb 100644 --- a/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation/LookupVector.hs +++ b/symbolic-base/src/ZkFold/Protocol/Plonkup/Relation/LookupVector.hs @@ -39,6 +39,12 @@ deriving via instance FromConstant b a => FromConstant b (LookupVector a) +deriving via + (ApplicativeAlgebra LookupVector a) + instance + {-# INCOHERENT #-} + FromConstant a (LookupVector a) + deriving via (ApplicativeAlgebra LookupVector a) instance diff --git a/symbolic-base/src/ZkFold/Symbolic/Interpreter.hs b/symbolic-base/src/ZkFold/Symbolic/Interpreter.hs index 0e9b2748b..c0e24b628 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Interpreter.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Interpreter.hs @@ -19,7 +19,6 @@ import GHC.Generics (Generic, Par1 (..)) import Text.Show (Show (..)) import ZkFold.Algebra.Class -import ZkFold.ArithmeticCircuit.Lookup (FunctionId (..)) import ZkFold.Control.HApplicative import ZkFold.Data.HFunctor import ZkFold.Data.HFunctor.Classes (HEq (..), HNFData (..), HShow (..)) @@ -88,4 +87,3 @@ instance unconstrained = return . Identity constraint _ = return () lookupConstraint _ _ = return () - registerFunction _ = return (FunctionId "") diff --git a/symbolic-base/src/ZkFold/Symbolic/MonadCircuit.hs b/symbolic-base/src/ZkFold/Symbolic/MonadCircuit.hs index 16c37393a..07824d8c8 100644 --- a/symbolic-base/src/ZkFold/Symbolic/MonadCircuit.hs +++ b/symbolic-base/src/ZkFold/Symbolic/MonadCircuit.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DerivingVia #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ZkFold.Symbolic.MonadCircuit where @@ -10,13 +11,12 @@ import Data.Foldable (Foldable) import Data.Function (($), (.)) import Data.Functor (Functor) import Data.Functor.Rep (Rep, Representable) -import Data.Set (singleton) -import Data.Traversable (Traversable) +import Data.Set (Set, singleton) import Data.Typeable (Typeable) -import GHC.Generics (Par1 (..)) +import GHC.Generics (Par1 (..), (:*:) (..)) import ZkFold.Algebra.Class -import ZkFold.ArithmeticCircuit.Lookup +import ZkFold.Data.FromList (FromList) import ZkFold.Data.Orphans () -- | A type of witness builders. @i@ is a type of variables. @@ -38,17 +38,19 @@ class PrimeField w => Witness i w | i -> w where -- suitable type, you don't have to check it yourself. type ClosedPoly var a = forall x. Algebra a x => (var -> x) -> x --- | A type of constraints for new variables. --- @var@ is a type of variables, @a@ is a base field. --- --- A function is a constraint for a new variable if, given an arbitrary algebra --- @x@ over @a@, a function mapping known variables to their witnesses in that --- algebra and a new variable, it computes the value of a constraint polynomial --- in that algebra. --- --- NOTE: the property above is correct by construction for each function of a --- suitable type, you don't have to check it yourself. -type NewConstraint var a = forall x. Algebra a x => (var -> x) -> var -> x +-- | @LookupTable a f@ is a type of compact lookup table descriptions using ideas from relational algebra. +-- @a@ is a base field type, @f@ is a functor such that @f a@ is a type whose subset this lookup table describes. +data LookupTable a f where + -- | @Ranges@ describes a set of disjoint segments of the base field. + Ranges :: Set (a, a) -> LookupTable a Par1 + -- | @Product t u@ is a cartesian product of tables @t@ and @u@. + Product :: LookupTable a f -> LookupTable a g -> LookupTable a (f :*: g) + -- | @Plot f x@ is a plot of a function @f@ with @x@ as a domain. + Plot + :: (Representable f, FromList f, Binary (Rep f), Foldable g) + => (forall w. (PrimeField w, Algebra a w) => f w -> g w) + -> LookupTable a f + -> LookupTable a (f :*: g) -- | A monadic DSL for constructing arithmetic circuits. -- @var@ is a type of variables, @a@ is a base field, @w@ is a type of witnesses @@ -90,13 +92,6 @@ class -- NOTE: currently, provided constraints are directly fed to zkSNARK in use. constraint :: ClosedPoly var a -> m () - -- | Registers new lookup function in the system to be used in lookup tables - -- (see 'lookupConstraint'). - registerFunction - :: (Representable f, Binary (Rep f), Typeable f, Traversable g, Typeable g) - => (forall x. PrimeField x => f x -> g x) - -> m (FunctionId (f a -> g a)) - -- | Adds new lookup constraint to the system. -- For examples of lookup constraints, see 'rangeConstraint'. -- @@ -140,6 +135,18 @@ newRanged upperBound witness = do rangeConstraint v upperBound return v +-- | A type of constraints for new variables. +-- @var@ is a type of variables, @a@ is a base field. +-- +-- A function is a constraint for a new variable if, given an arbitrary algebra +-- @x@ over @a@, a function mapping known variables to their witnesses in that +-- algebra and a new variable, it computes the value of a constraint polynomial +-- in that algebra. +-- +-- NOTE: the property above is correct by construction for each function of a +-- suitable type, you don't have to check it yourself. +type NewConstraint var a = forall x. Algebra a x => (var -> x) -> var -> x + -- | Creates new variable from witness constrained by a polynomial. -- E.g., @'newConstrained' (\\x i -> x i * (x i - one)) (\\x -> x j - one)@ -- creates new variable whose value is equal to @x j - one@ and which is diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal index 882823e7c..5481eabdd 100644 --- a/symbolic-base/symbolic-base.cabal +++ b/symbolic-base/symbolic-base.cabal @@ -146,7 +146,6 @@ library ZkFold.ArithmeticCircuit.Context ZkFold.ArithmeticCircuit.Desugaring ZkFold.ArithmeticCircuit.Experimental - ZkFold.ArithmeticCircuit.Lookup ZkFold.ArithmeticCircuit.MerkleHash ZkFold.ArithmeticCircuit.Optimization ZkFold.ArithmeticCircuit.Var @@ -158,6 +157,7 @@ library ZkFold.Data.Binary ZkFold.Data.Empty ZkFold.Data.Eq + ZkFold.Data.FromList ZkFold.Data.HFunctor ZkFold.Data.HFunctor.Classes ZkFold.Data.List.Infinite