Redundant constraints

examples/Snarkl/Example/Basic.hs

@@ -73,4 +73,4 @@ test1 :: (GaloisField k) => State (Env k) (TExp 'TBool k)
 test1 = do
   b <- fresh_input
   z <- if return b then comp1 else comp2
-  case_sum return (const $ return false) z
+  case_sum return (const $ return false) z

examples/Snarkl/Example/Games.hs

@@ -6,9 +6,9 @@
 
 module Snarkl.Example.Games where
 
-import Data.Field.Galois (GaloisField, Prime)
+import Data.Field.Galois (GaloisField)
+import Data.Kind (Type)
 import Data.Typeable
-import GHC.TypeLits (KnownNat, Nat)
 import Snarkl.Errors
 import Snarkl.Field (F_BN128)
 import Snarkl.Language.Syntax
@@ -38,7 +38,7 @@ data ISO (t :: Ty) (s :: Ty) k = Iso
     from :: TExp s k -> Comp t k
   }
 
-data Game :: Ty -> * -> * where
+data Game :: Ty -> Type -> Type where
   Single ::
     forall (s :: Ty) (t :: Ty) k.
     ( Typeable s,
@@ -108,8 +108,7 @@ sum_game ::
     Zippable t1 k,
     Zippable t2 k,
     Derive t1 k,
-    Derive t2 k,
-    GaloisField k
+    Derive t2 k
   ) =>
   Game t1 k ->
   Game t2 k ->
@@ -133,9 +132,7 @@ t2 :: F_BN128
 t2 = comp_interp basic_test [1, 23, 88] -- 88
 
 (+>) ::
-  ( Typeable t,
-    Typeable s,
-    Zippable t k,
+  ( Typeable s,
     Zippable s k
   ) =>
   Game t k ->
@@ -151,8 +148,7 @@ prodI ::
   ( Typeable a,
     Typeable b,
     Typeable c,
-    Typeable d,
-    GaloisField k
+    Typeable d
   ) =>
   ISO a b k ->
   ISO c d k ->
@@ -174,13 +170,12 @@ prodI (Iso f g) (Iso f' g') =
         pair y1 y2
     )
 
-seqI :: (Typeable b) => ISO a b p -> ISO b c p -> ISO a c p
+seqI :: ISO a b p -> ISO b c p -> ISO a c p
 seqI (Iso f g) (Iso f' g') = Iso (\a -> f a >>= f') (\c -> g' c >>= g)
 
 prodLInputI ::
   ( Typeable a,
-    Typeable b,
-    GaloisField k
+    Typeable b
   ) =>
   ISO ('TProd a b) b k
 prodLInputI =
@@ -200,8 +195,7 @@ prodLSumI ::
     Zippable c k,
     Derive a k,
     Derive b k,
-    Derive c k,
-    GaloisField k
+    Derive c k
   ) =>
   ISO ('TProd ('TSum b c) a) ('TSum ('TProd b a) ('TProd c a)) k
 prodLSumI =
@@ -301,8 +295,7 @@ instance (GaloisField k) => Gameable 'TUnit k where
   mkGame = unit_game
 
 instance
-  ( Typeable a,
-    Typeable b,
+  ( Typeable b,
     Zippable a k,
     Zippable b k,
     Derive a k,
@@ -323,8 +316,7 @@ instance
     Derive a k,
     Derive b k,
     Gameable a k,
-    Gameable b k,
-    GaloisField k
+    Gameable b k
   ) =>
   Gameable ('TSum a b) k
   where

examples/Snarkl/Example/Queue.hs

@@ -2,10 +2,8 @@
 
 module Snarkl.Example.Queue where
 
-import Data.Field.Galois (GaloisField, Prime)
+import Data.Field.Galois (GaloisField)
 import Data.Typeable
-import GHC.TypeLits (KnownNat)
-import Snarkl.Compile
 import Snarkl.Example.List
 import Snarkl.Example.Stack
 import Snarkl.Language.Syntax
@@ -36,7 +34,7 @@ empty_queue = do
   pair l r
 
 enqueue ::
-  (Zippable a k, Derive a k, Typeable a, GaloisField k) =>
+  (Typeable a, GaloisField k) =>
   TExp a k ->
   Queue a k ->
   Comp (TQueue a) k

snarkl.cabal

@@ -141,6 +141,8 @@ test-suite spec
     , process        >=1.2
     , QuickCheck
     , snarkl         >=0.1.0.0
+  ghc-options:
+    -Wredundant-constraints
 
 benchmark criterion
   type:               exitcode-stdio-1.0

src/Snarkl/Common.hs

@@ -67,4 +67,4 @@ isAssoc op = case op of
   Or -> True
   XOr -> True
   Eq -> True
-  BEq -> True
+  BEq -> True

src/Snarkl/Compile.hs

@@ -249,19 +249,19 @@ encode_binop op (x, y, z) = go op
       add_constraint $
         CMult (1, y) (1, z) (1, Just x)
 
-encode_linear :: (GaloisField a) => Var -> [Either (Var, a) a] -> State (CEnv a) ()
+encode_linear :: (GaloisField k) => Var -> [Either (Var, k) k] -> State (CEnv k) ()
 encode_linear out xs =
   let c = foldl (flip (+)) 0 $ map (fromRight 0) xs
    in add_constraint $
         cadd c $
           (out, -1) : remove_consts xs
   where
-    remove_consts :: [Either (Var, a) a] -> [(Var, a)]
+    remove_consts :: [Either (Var, k) k] -> [(Var, k)]
     remove_consts [] = []
     remove_consts (Left p : l) = p : remove_consts l
     remove_consts (Right _ : l) = remove_consts l
 
-cs_of_exp :: (GaloisField a) => Var -> Core.Exp a -> State (CEnv a) ()
+cs_of_exp :: (GaloisField k) => Var -> Core.Exp k -> State (CEnv k) ()
 cs_of_exp out e = case e of
   Core.EVar x ->
     ensure_equal (out, view _Var x)
@@ -287,7 +287,7 @@ cs_of_exp out e = case e of
     -- We special-case linear combinations in this way to avoid having
     -- to introduce new multiplication gates for multiplication by
     -- constant scalars.
-    let go_linear :: (GaloisField a) => [Core.Exp a] -> State (CEnv a) [Either (Var, a) a]
+    let go_linear :: (GaloisField k) => [Core.Exp k] -> State (CEnv k) [Either (Var, k) k]
         go_linear [] = return []
         go_linear (Core.EBinop Mult [Core.EVar x, Core.EVal coeff] : es') =
           do
@@ -338,7 +338,7 @@ cs_of_exp out e = case e of
         rev_pol (Left (x, c) : ls) = Left (x, -c) : rev_pol ls
         rev_pol (Right c : ls) = Right (-c) : rev_pol ls
 
-        go_other :: (GaloisField a) => [Core.Exp a] -> State (CEnv a) [Var]
+        go_other :: (GaloisField k) => [Core.Exp k] -> State (CEnv k) [Var]
         go_other [] = return []
         go_other (Core.EVar x : es') =
           do
@@ -457,10 +457,10 @@ data TExpPkg ty k = TExpPkg
   }
   deriving (Show)
 
-instance (Typeable ty) => Pretty (TExpPkg ty k) where
+instance Pretty (TExpPkg ty k) where
   pretty (TExpPkg _ _ e) = pretty e
 
-deriving instance (Eq (TExp ty k)) => Eq (TExpPkg ty k)
+deriving instance Eq (TExpPkg ty k)
 
 -- | Desugar a 'Comp'utation to a pair of:
 --   the total number of vars,

src/Snarkl/Field.hs

@@ -6,4 +6,4 @@ import Data.Field.Galois (Prime)
 
 type P_BN128 = 21888242871839275222246405745257275088548364400416034343698204186575808495617
 
-type F_BN128 = Prime P_BN128
+type F_BN128 = Prime P_BN128

src/Snarkl/Interp.hs

@@ -4,7 +4,6 @@ module Snarkl.Interp
 where
 
 import Control.Monad (ap, foldM)
-import Data.Data (Typeable)
 import Data.Field.Galois (GaloisField)
 import Data.Foldable (traverse_)
 import Data.Map (Map)
@@ -77,20 +76,19 @@ boolOfField v =
     )
 
 interpTExp ::
-  ( GaloisField a,
-    Typeable ty
+  ( GaloisField k
   ) =>
-  TExp ty a ->
-  InterpM a (Maybe a)
+  TExp ty k ->
+  InterpM k (Maybe k)
 interpTExp e = do
   let _exp = compileTExpToProgram e
   interpProg _exp
 
 interp ::
-  (GaloisField a, Typeable ty) =>
-  Map Variable a ->
-  TExp ty a ->
-  Either ErrMsg (Env a, Maybe a)
+  (GaloisField k) =>
+  Map Variable k ->
+  TExp ty k ->
+  Either ErrMsg (Env k, Maybe k)
 interp rho e = runInterpM (interpTExp e) $ Map.map Just rho
 
 interpProg ::

src/Snarkl/Language.hs

@@ -85,7 +85,6 @@ module Snarkl.Language
   )
 where
 
-import Data.Data (Typeable)
 import Data.Field.Galois (GaloisField)
 import Snarkl.Language.Core
   ( Assignment (..),
@@ -166,7 +165,7 @@ import Snarkl.Language.TExpr (TExp, booleanVarsOfTexp, tExpToLambdaExp)
 import Snarkl.Language.Type
 import Prelude (Either (..), error, ($), (.), (<>))
 
-compileTExpToProgram :: (GaloisField a, Typeable ty) => TExp ty a -> Program a
+compileTExpToProgram :: (GaloisField k) => TExp ty k -> Program k
 compileTExpToProgram te =
   let eprog = mkProgram . expOfLambdaExp . tExpToLambdaExp $ te
    in case eprog of

src/Snarkl/Language/Core.hs

@@ -13,9 +13,13 @@ data Exp :: Type -> Type where
   EVal :: (GaloisField k) => k -> Exp k
   EUnop :: UnOp -> Exp k -> Exp k
   EBinop :: Op -> [Exp k] -> Exp k
-  EIf :: Exp k -> Exp a -> Exp k -> Exp k
+  EIf :: Exp k -> Exp k -> Exp k -> Exp k
   EUnit :: Exp k
 
+deriving instance Eq (Exp k)
+
+deriving instance Show (Exp k)
+
 data Assignment a = Assignment Variable (Exp a)
 
 data Program :: Type -> Type where

src/Snarkl/Language/Expr.hs

@@ -152,7 +152,7 @@ mkProgram _exp = do
       let (eexpr, assignments) = runState (runExceptT $ go es) mempty
       Core.Program assignments <$> eexpr
       where
-        go :: (Show k) => Seq (Exp k) -> ExceptT String (State (Seq (Core.Assignment k))) (Core.Exp k)
+        go :: Seq (Exp k) -> ExceptT String (State (Seq (Core.Assignment k))) (Core.Exp k)
         go = \case
           Empty -> throwError "mkProgram: empty sequence"
           e :<| Empty -> hoistEither $ mkExpression e

src/Snarkl/Language/LambdaExpr.hs

@@ -38,7 +38,7 @@ deriving instance Show (Exp k)
 
 deriving instance Eq (Exp k)
 
-betaNormalize :: Exp a -> Exp a
+betaNormalize :: Exp k -> Exp k
 betaNormalize = \case
   EVar x -> EVar x
   EVal v -> EVal v
@@ -55,7 +55,7 @@ betaNormalize = \case
   EUnit -> EUnit
   where
     -- substitute x e1 e2 = e2 [x := e1 ]
-    substitute :: (Variable, Exp a) -> Exp a -> Exp a
+    substitute :: (Variable, Exp k) -> Exp k -> Exp k
     substitute (var, e1) = \case
       e@(EVar var') -> if var == var' then e1 else e
       e@(EVal _) -> e

src/Snarkl/Language/Syntax.hs

@@ -768,4 +768,4 @@ uncurry f p = do
   return $ TEApp g y
 
 apply :: (Typeable a, Typeable b) => TExp ('TFun a b) k -> TExp a k -> Comp b k
-apply f x = return $ TEApp f x
+apply f x = return $ TEApp f x

src/Snarkl/Language/TExpr.hs

@@ -217,4 +217,4 @@ lastSeq ::
   TExp ty a
 lastSeq te = case te of
   TESeq _ te2 -> lastSeq te2
-  _ -> te
+  _ -> te

src/Snarkl/Toplevel.hs

@@ -41,7 +41,8 @@ import Prelude
 -- | Using the executable semantics for the 'TExp' language, execute
 -- the computation on the provided inputs, returning the 'k' result.
 comp_interp ::
-  (Typeable ty, GaloisField k) =>
+  forall ty k.
+  (GaloisField k) =>
   Comp ty k ->
   [k] ->
   k
@@ -64,7 +65,7 @@ data Result k = Result
   }
   deriving (Show)
 
-instance Pretty (Result k) where
+instance (Pretty k) => Pretty (Result k) where
   pretty (Result sat vars constraints result _ _) =
     mconcat $
       intercalate

tests/Test/ArkworksBridge.hs

@@ -4,8 +4,16 @@ import qualified Data.ByteString.Lazy as LBS
 import Data.Field.Galois (GaloisField, PrimeField)
 import Data.Typeable (Typeable)
 import Snarkl.Backend.R1CS
+  ( mkInputsFilePath,
+    mkR1CSFilePath,
+    mkWitnessFilePath,
+    serializeInputsAsJson,
+    serializeR1CSAsJson,
+    serializeWitnessAsJson,
+    wit_of_r1cs,
+  )
 import Snarkl.Compile (SimplParam, compileCompToR1CS)
-import Snarkl.Language (Comp)
+import Snarkl.Language.SyntaxMonad (Comp)
 import qualified System.Exit as GHC
 import System.Process (createProcess, shell, waitForProcess)
 

tests/Test/Snarkl/DataflowSpec.hs

@@ -2,9 +2,7 @@
 
 module Test.Snarkl.DataflowSpec where
 
-import Data.Field.Galois (GaloisField, Prime, PrimeField, toP)
-import qualified Data.IntMap as IntMap
-import qualified Data.Map as Map
+import Data.Field.Galois (Prime, toP)
 import qualified Data.Set as Set
 import GHC.TypeLits (KnownNat)
 import Snarkl.Common (Var (Var))
@@ -30,8 +28,8 @@ constraint2 :: (KnownNat p) => Constraint (Prime p)
 constraint2 = CMult (toP 2, Var 1) (toP 3, Var 2) (toP 4, Just $ Var 3)
 
 -- NOTE: notice 4 doesn't count as a variable here, WHY?
-constraint3 :: (GaloisField k) => Constraint k
-constraint3 = CMagic (Var 4) [Var 2, Var 3] $ \vars -> return True
+constraint3 :: Constraint k
+constraint3 = CMagic (Var 4) [Var 2, Var 3] $ \_ -> return True
 
 -- 4 is independent from 1,2,3
 constraint4 :: (KnownNat p) => Constraint (Prime p)