Add CLI

.github/workflows/nix-ci.yml

@@ -18,7 +18,7 @@ jobs:
       uses: jaxxstorm/[email protected]
       with:
         repo: torsion-labs/arkworks-bridge
-        tag: v0.2.0
+        tag: v1.0.0-rc1
 
     - uses: cachix/install-nix-action@v24
       with:

app/Main.hs

@@ -1,29 +1,9 @@
 module Main where
 
-import Control.Monad (unless)
-import qualified Data.ByteString.Lazy as LBS
-import Data.Field.Galois (PrimeField)
-import Data.Typeable (Typeable)
-import Snarkl.Compile (SimplParam (NoSimplify))
-import Snarkl.Errors (ErrMsg (ErrMsg), failWith)
-import Snarkl.Field
-import Snarkl.Toplevel
+import Snarkl.CLI (defaultMain)
+import Snarkl.Field (F_BN128)
+import Snarkl.Toplevel (Comp, Ty (TField))
 import qualified Test.Snarkl.Unit.Programs as Programs
 
 main :: IO ()
-main = do
-  executeAndWriteArtifacts "./snarkl-output" "prog2" NoSimplify (Programs.prog2 10) [1 :: F_BN128]
-
-executeAndWriteArtifacts :: (Typeable ty, PrimeField k) => FilePath -> String -> SimplParam -> Comp ty k -> [k] -> IO ()
-executeAndWriteArtifacts fp name simpl mf inputs = do
-  let Result {result_sat = isSatisfied, result_r1cs = r1cs, result_witness = wit} = execute simpl mf inputs
-  unless isSatisfied $ failWith $ ErrMsg "R1CS is not satisfied"
-  let r1csFP = mkR1CSFilePath fp name
-  LBS.writeFile r1csFP (serializeR1CSAsJson r1cs)
-  putStrLn $ "Wrote R1CS to file " <> r1csFP
-  let witnessFP = mkWitnessFilePath fp name
-  LBS.writeFile witnessFP (serializeWitnessAsJson r1cs wit)
-  putStrLn $ "Wrote witness to file " <> witnessFP
-  let inputsFP = mkInputsFilePath fp name
-  LBS.writeFile inputsFP (serializeInputsAsJson r1cs inputs)
-  putStrLn $ "Wrote inputs to file " <> inputsFP
+main = defaultMain "prog" (Programs.prog2 10 :: Comp 'TField F_BN128)

examples/Snarkl/Example/Basic.hs

@@ -61,7 +61,7 @@ interp2' :: (GaloisField k) => k
 interp2' = comp_interp p2 [256]
 
 compile1 :: (GaloisField k) => R1CS k
-compile1 = compileCompToR1CS Simplify p1
+compile1 = fst $ compileCompToR1CS [Simplify] p1
 
 comp1 :: (GaloisField k, Typeable a) => Comp ('TSum 'TBool a) k
 comp1 = inl false

snarkl.cabal

@@ -32,10 +32,12 @@ library
   exposed-modules:
     Control.Monad.Supply
     Control.Monad.Supply.Class
+    Data.JSONLines
     Snarkl.Backend.R1CS
     Snarkl.Backend.R1CS.Poly
     Snarkl.Backend.R1CS.R1CS
-    Snarkl.Backend.R1CS.Serialize
+    Snarkl.CLI
+    Snarkl.CLI.Common
     Snarkl.Common
     Snarkl.Compile
     Snarkl.Constraint
@@ -56,39 +58,55 @@ library
     Snarkl.Language.TExpr
     Snarkl.Toplevel
 
+  other-modules:
+    Snarkl.CLI.Compile
+    Snarkl.CLI.GenWitness
+    Snarkl.CLI.RunAll
+
   default-extensions:
     BangPatterns
     DataKinds
     DeriveDataTypeable
+    DeriveGeneric
     FlexibleContexts
     FlexibleInstances
+    FunctionalDependencies
     GADTs
     GeneralizedNewtypeDeriving
     KindSignatures
     LambdaCase
+    MultiParamTypeClasses
+    NamedFieldPuns
     OverloadedStrings
     PatternSynonyms
     PolyKinds
     RankNTypes
+    RecordWildCards
     ScopedTypeVariables
     StandaloneDeriving
+    TupleSections
+    TypeApplications
     TypeFamilies
     TypeSynonymInstances
     UndecidableInstances
 
   build-depends:
       aeson
-    , base           >=4.7
+    , base                  >=4.7
     , bytestring
-    , Cabal          >=1.22
-    , containers     >=0.5   && <0.7
-    , galois-field   >=1.0.4
-    , hspec          >=2.0
-    , jsonl          >=0.1.4
+    , Cabal                 >=1.22
+    , containers            >=0.5   && <0.7
+    , directory
+    , filepath
+    , galois-field          >=1.0.4
+    , hspec                 >=2.0
+    , jsonl                 >=0.1.4
     , lens
-    , mtl            >=2.2   && <2.3
-    , parallel       >=3.2   && <3.3
-    , process        >=1.2
+    , mtl                   >=2.2   && <2.3
+    , optparse-applicative
+    , parallel              >=3.2   && <3.3
+    , process               >=1.2
+    , string-conversions
     , wl-pprint-text
 
   hs-source-dirs:     src
@@ -141,7 +159,7 @@ test-suite spec
 benchmark criterion
   type:               exitcode-stdio-1.0
   main-is:            Main.hs
-  ghc-options: -threaded -O2
+  ghc-options:        -threaded -O2
   other-modules:
     Harness
     Snarkl.Example.Basic
@@ -209,14 +227,14 @@ executable print-examples
   hs-source-dirs:     print-examples examples tests
   default-language:   Haskell2010
   build-depends:
-      base           >=4.7
+      base            >=4.7
     , containers
-    , galois-field   >=1.0.4
-    , hspec          >=2.0
-    , snarkl         >=0.1.0.0
+    , galois-field    >=1.0.4
+    , hspec           >=2.0
+    , snarkl          >=0.1.0.0
     , wl-pprint-text
 
-executable compile
+executable snarkl
   main-is:            Main.hs
   other-modules:
     Snarkl.Example.Basic
@@ -241,9 +259,9 @@ executable compile
   hs-source-dirs:     app examples tests
   default-language:   Haskell2010
   build-depends:
-      base           >=4.7
+      base          >=4.7
     , bytestring
     , containers
-    , galois-field   >=1.0.4
-    , hspec          >=2.0
-    , snarkl         >=0.1.0.0
+    , galois-field  >=1.0.4
+    , hspec         >=2.0
+    , snarkl        >=0.1.0.0

src/Data/JSONLines.hs

@@ -0,0 +1,67 @@
+module Data.JSONLines
+  ( ToJSONLines (..),
+    FromJSONLines (..),
+    JSONLine (..),
+    WithHeader (..),
+    NoHeader (..),
+  )
+where
+
+import qualified Data.Aeson as A
+import Data.ByteString.Builder (Builder, lazyByteString, toLazyByteString)
+import qualified Data.ByteString.Lazy as LBS
+import Data.Kind (Type)
+import Data.String.Conversions (LazyByteString)
+
+data JSONLine
+  = JSONLine Builder
+  | EmptyLine
+
+instance Semigroup JSONLine where
+  EmptyLine <> a = a
+  a <> EmptyLine = a
+  JSONLine a <> JSONLine b = JSONLine (a <> "\n" <> b)
+
+instance Monoid JSONLine where
+  mempty = EmptyLine
+
+data WithHeader :: Type -> Type -> Type where
+  WithHeader :: hdr -> [item] -> WithHeader hdr item
+
+newtype NoHeader item = NoHeader [item]
+
+jsonlBuilder ::
+  (Foldable t) =>
+  (A.ToJSON a) =>
+  t a ->
+  JSONLine
+jsonlBuilder = foldMap jsonLine
+
+jsonLine :: (A.ToJSON a) => a -> JSONLine
+jsonLine = JSONLine . lazyByteString . A.encode
+
+toBS :: JSONLine -> LBS.ByteString
+toBS EmptyLine = mempty
+toBS (JSONLine a) = toLazyByteString a
+
+class ToJSONLines a where
+  toJSONLines :: a -> LBS.ByteString
+
+instance (A.ToJSON item) => ToJSONLines (NoHeader item) where
+  toJSONLines (NoHeader items) = toBS . jsonlBuilder $ items
+
+instance (A.ToJSON hdr, A.ToJSON item) => ToJSONLines (WithHeader hdr item) where
+  toJSONLines (WithHeader hdr items) = toBS $ jsonLine hdr <> jsonlBuilder items
+
+class FromJSONLines a where
+  fromJSONLines :: [LazyByteString] -> Either String a
+
+instance (A.FromJSON item) => FromJSONLines (NoHeader item) where
+  fromJSONLines items = NoHeader <$> traverse A.eitherDecode items
+
+instance (A.FromJSON hdr, A.FromJSON item) => FromJSONLines (WithHeader hdr item) where
+  fromJSONLines (h : is) = do
+    hdr <- A.eitherDecode h
+    items <- traverse A.eitherDecode is
+    pure $ WithHeader hdr items
+  fromJSONLines [] = Left "Empty file"

src/Snarkl/Backend/R1CS.hs

@@ -1,10 +1,8 @@
 module Snarkl.Backend.R1CS
   ( module Snarkl.Backend.R1CS.R1CS,
-    module Snarkl.Backend.R1CS.Serialize,
     module Snarkl.Backend.R1CS.Poly,
   )
 where
 
 import Snarkl.Backend.R1CS.Poly
 import Snarkl.Backend.R1CS.R1CS
-import Snarkl.Backend.R1CS.Serialize

src/Snarkl/Backend/R1CS/Poly.hs

@@ -1,9 +1,7 @@
-{-# LANGUAGE InstanceSigs #-}
-
 module Snarkl.Backend.R1CS.Poly where
 
 import qualified Data.Aeson as A
-import Data.Field.Galois (GaloisField, PrimeField, fromP)
+import Data.Field.Galois (GaloisField, PrimeField)
 import qualified Data.Map as Map
 import Snarkl.Common
 import Text.PrettyPrint.Leijen.Text (Pretty (..))
@@ -13,23 +11,18 @@ data Poly a where
 
 deriving instance (Show a) => Show (Poly a)
 
-instance (Pretty a) => Pretty (Poly a) where
-  pretty (Poly m) = pretty $ Map.toList m
-
--- The reason we use incVar is that we want to use -1 internally as the constant
--- variable (which turns out to be easier to work with internally but
--- harder to work with downstream where e.g. arkworks expects positive indices).
--- The reason we use show is because it's hard to deserialize large integers
--- in certain langauges (e.g. javascript, even rust).
 instance (PrimeField a) => A.ToJSON (Poly a) where
-  toJSON :: Poly a -> A.Value
-  toJSON (Poly m) =
-    let kvs = map (\(var, coeff) -> (show $ fromP coeff, incVar var)) $ Map.toList m
-     in A.toJSON kvs
+  toJSON (Poly m) = A.toJSON m
+
+instance (PrimeField a) => A.FromJSON (Poly a) where
+  parseJSON v = Poly <$> A.parseJSON v
+
+instance (Pretty a) => Pretty (Poly a) where
+  pretty (Poly (Assgn m)) = pretty $ Map.toList m
 
 -- | The constant polynomial equal 'c'
 const_poly :: (GaloisField a) => a -> Poly a
-const_poly c = Poly $ Map.insert (Var (-1)) c Map.empty
+const_poly c = Poly $ Assgn $ Map.singleton (Var (-1)) c
 
 -- | The polynomial equal variable 'x'
 var_poly ::
@@ -39,4 +32,4 @@ var_poly ::
   -- | Resulting polynomial
   Poly a
 var_poly (coeff, x) =
-  Poly $ Map.insert x coeff Map.empty
+  Poly $ Assgn $ Map.singleton x coeff