From 90b32847a788afd75f1f9a70b026f0c41ea39620 Mon Sep 17 00:00:00 2001 From: martyall Date: Sat, 13 Jan 2024 19:01:36 -0800 Subject: [PATCH 01/13] wip --- app/Main.hs | 32 ++-- examples/Snarkl/Example/Basic.hs | 2 +- snarkl.cabal | 8 + src/Snarkl/CLI.hs | 60 +++++++ src/Snarkl/CLI/Compile.hs | 39 ++++ src/Snarkl/CLI/GenWitness.hs | 11 ++ src/Snarkl/CLI/RunAll.hs | 9 + src/Snarkl/Compile.hs | 27 ++- src/Snarkl/Toplevel.hs | 6 +- tests/Test/ArkworksBridge.hs | 6 +- tests/Test/Snarkl/UnitSpec.hs | 298 +++++++++++++++---------------- 11 files changed, 311 insertions(+), 187 deletions(-) create mode 100644 src/Snarkl/CLI.hs create mode 100644 src/Snarkl/CLI/Compile.hs create mode 100644 src/Snarkl/CLI/GenWitness.hs create mode 100644 src/Snarkl/CLI/RunAll.hs diff --git a/app/Main.hs b/app/Main.hs index 5d2adc0..8b57cee 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -4,6 +4,7 @@ import Control.Monad (unless) import qualified Data.ByteString.Lazy as LBS import Data.Field.Galois (PrimeField) import Data.Typeable (Typeable) +import Snarkl.CLI (compiler) import Snarkl.Compile (SimplParam (NoSimplify)) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Field @@ -11,19 +12,20 @@ import Snarkl.Toplevel import qualified Test.Snarkl.Unit.Programs as Programs main :: IO () -main = do - executeAndWriteArtifacts "./snarkl-output" "prog2" NoSimplify (Programs.prog2 10) [1 :: F_BN128] +main = compiler "prog2" (Programs.prog2 10 :: Comp 'TField 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 +-- 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 diff --git a/examples/Snarkl/Example/Basic.hs b/examples/Snarkl/Example/Basic.hs index 7a86fd1..dec403d 100644 --- a/examples/Snarkl/Example/Basic.hs +++ b/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 = compileCompToR1CS [Simplify] p1 comp1 :: (GaloisField k, Typeable a) => Comp ('TSum 'TBool a) k comp1 = inl false diff --git a/snarkl.cabal b/snarkl.cabal index 0492d85..81a51e6 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -55,6 +55,12 @@ library Snarkl.Language.SyntaxMonad Snarkl.Language.TExpr Snarkl.Toplevel + Snarkl.CLI + + other-modules: + Snarkl.CLI.Compile + Snarkl.CLI.GenWitness + Snarkl.CLI.RunAll default-extensions: BangPatterns @@ -87,8 +93,10 @@ library , jsonl >=0.1.4 , lens , mtl >=2.2 && <2.3 + , optparse-applicative , parallel >=3.2 && <3.3 , process >=1.2 + , streamly , wl-pprint-text hs-source-dirs: src diff --git a/src/Snarkl/CLI.hs b/src/Snarkl/CLI.hs new file mode 100644 index 0000000..8e46894 --- /dev/null +++ b/src/Snarkl/CLI.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE RecordWildCards #-} + +module Snarkl.CLI (compiler) where + +import qualified Data.ByteString.Lazy as LBS +import Data.Field.Galois (PrimeField) +import Data.Maybe (catMaybes) +import Data.Typeable (Typeable) +import Options.Applicative (execParser, fullDesc, header, helper, info, (<**>)) +import Snarkl.Backend.R1CS +import Snarkl.CLI.Compile (CompileOpts (..), OptimiseOpts (..), compileOptsParser) +import Snarkl.CLI.GenWitness (GenWitnessOpts (..)) +import Snarkl.Compile +import Snarkl.Constraint () +import Snarkl.Language + +data CMD + = Compile CompileOpts + | GenWitness GenWitnessOpts + +compiler :: + forall ty k. + (Typeable ty) => + (PrimeField k) => + String -> + Comp ty k -> + IO () +compiler name comp = do + compileOpts <- execParser opts + runCMD (Compile compileOpts) name comp + where + opts = + info + (compileOptsParser <**> helper) + ( fullDesc + <> header ("Compiling the program " <> name <> " to a ZK-SNARK") + ) + +runCMD :: + forall ty k. + (Typeable ty) => + (PrimeField k) => + CMD -> + String -> + Comp ty k -> + IO () +runCMD cmd name comp = case cmd of + Compile (CompileOpts {..}) -> do + let simpl = + catMaybes + [ if simplify optimiseOpts then Just Simplify else Nothing, + if removeUnreachable optimiseOpts then Just RemoveUnreachable else Nothing + ] + TExpPkg nv in_vars e = compileCompToTexp comp + r1cs = compileTExpToR1CS simpl (TExpPkg nv in_vars e) + r1csFP = mkR1CSFilePath name r1csOutput + LBS.writeFile r1csFP (serializeR1CSAsJson r1cs) + putStrLn $ "Wrote R1CS to file " <> r1csOutput + GenWitness (GenWitnessOpts {..}) -> do + \ No newline at end of file diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs new file mode 100644 index 0000000..1f7bf0f --- /dev/null +++ b/src/Snarkl/CLI/Compile.hs @@ -0,0 +1,39 @@ +module Snarkl.CLI.Compile + ( OptimiseOpts (..), + CompileOpts (..), + compileOptsParser, + ) +where + +import Options.Applicative + +data OptimiseOpts = OptimiseOpts + { simplify :: Bool, + removeUnreachable :: Bool + } + +optimizeOptsParser :: Parser OptimiseOpts +optimizeOptsParser = + OptimiseOpts + <$> switch + ( long "simplify" + <> help "run the constraint simplifier" + ) + <*> switch + ( long "remove-unreachable" + <> help "detect and remove variables not contributing to the output" + ) + +data CompileOpts = CompileOpts + { optimiseOpts :: OptimiseOpts, + r1csOutput :: FilePath + } + +compileOptsParser :: Parser CompileOpts +compileOptsParser = + CompileOpts + <$> optimizeOptsParser + <*> strOption + ( long "r1cs-output-dir" + <> help "the directory to write the r1cs artifact" + ) diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs new file mode 100644 index 0000000..e37c707 --- /dev/null +++ b/src/Snarkl/CLI/GenWitness.hs @@ -0,0 +1,11 @@ +module Snarkl.CLI.GenWitness where + +data InputOpts + = Explicit [Integer] + | FromFile FilePath + +data GenWitnessOpts = GenWitnessOpts + { r1csInput :: FilePath, + inputs :: InputOpts, + witnessOutput :: FilePath + } \ No newline at end of file diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs new file mode 100644 index 0000000..3b2cc7b --- /dev/null +++ b/src/Snarkl/CLI/RunAll.hs @@ -0,0 +1,9 @@ +module Snarkl.CLI.RunAll where + +import Snarkl.CLI.GenWitness (InputOpts) + +data RunAllOpts = RunAllOpts + { r1csOutput :: FilePath, + inputs :: InputOpts, + witnessOutput :: FilePath + } \ No newline at end of file diff --git a/src/Snarkl/Compile.hs b/src/Snarkl/Compile.hs index 3fb5ac1..dba6e3f 100644 --- a/src/Snarkl/Compile.hs +++ b/src/Snarkl/Compile.hs @@ -414,23 +414,24 @@ cs_of_exp out e = case e of data SimplParam = NoSimplify | Simplify - | SimplifyDataflow + | RemoveUnreachable + deriving (Eq) -- | Snarkl.Compile a list of arithmetic constraints to a rank-1 constraint -- system. Takes as input the constraints, the input variables, and -- the output variables, and return the corresponding R1CS. compileConstraintsToR1CS :: (GaloisField a) => - SimplParam -> + [SimplParam] -> ConstraintSystem a -> R1CS a -compileConstraintsToR1CS simpl cs = +compileConstraintsToR1CS simpls cs = let -- Simplify resulting constraints. cs_simpl = - if must_simplify simpl + if must_simplify then snd $ do_simplify False Map.empty cs else cs - cs_dataflow = if must_dataflow simpl then removeUnreachable cs_simpl else cs_simpl + cs_dataflow = if must_dataflow then removeUnreachable cs_simpl else cs_simpl -- Renumber constraint variables sequentially, from 0 to -- 'max_var'. 'renumber_f' is a function mapping variables to -- their renumbered counterparts. @@ -444,15 +445,11 @@ compileConstraintsToR1CS simpl cs = f = solve cs' in r1cs_of_cs cs' f where - must_simplify :: SimplParam -> Bool - must_simplify NoSimplify = False - must_simplify Simplify = True - must_simplify SimplifyDataflow = True + must_simplify :: Bool + must_simplify = Simplify `elem` simpls - must_dataflow :: SimplParam -> Bool - must_dataflow NoSimplify = False - must_dataflow Simplify = False - must_dataflow SimplifyDataflow = True + must_dataflow :: Bool + must_dataflow = RemoveUnreachable `elem` simpls ------------------------------------------------------ -- @@ -551,7 +548,7 @@ compileCompToConstraints = compileTexpToConstraints . compileCompToTexp -- | Snarkl.Compile 'TExp's to 'R1CS'. compileTExpToR1CS :: (Typeable ty, GaloisField k) => - SimplParam -> + [SimplParam] -> TExpPkg ty k -> R1CS k compileTExpToR1CS simpl = compileConstraintsToR1CS simpl . compileTexpToConstraints @@ -559,7 +556,7 @@ compileTExpToR1CS simpl = compileConstraintsToR1CS simpl . compileTexpToConstrai -- | Snarkl.Compile Snarkl computations to 'R1CS'. compileCompToR1CS :: (Typeable ty, GaloisField k) => - SimplParam -> + [SimplParam] -> Comp ty k -> R1CS k compileCompToR1CS simpl = compileConstraintsToR1CS simpl . compileCompToConstraints diff --git a/src/Snarkl/Toplevel.hs b/src/Snarkl/Toplevel.hs index 5f7e3a1..7b55c99 100644 --- a/src/Snarkl/Toplevel.hs +++ b/src/Snarkl/Toplevel.hs @@ -12,7 +12,6 @@ module Snarkl.Toplevel -- * Re-exported modules module Snarkl.Language, - module Snarkl.Constraint, module Snarkl.Backend.R1CS, module Snarkl.Compile, ) @@ -25,12 +24,11 @@ import Data.Typeable (Typeable) import Snarkl.Backend.R1CS import Snarkl.Common (Assgn) import Snarkl.Compile -import Snarkl.Constraint +import Snarkl.Constraint () import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Interp (interp) import Snarkl.Language import Text.PrettyPrint.Leijen.Text (Pretty (..), line, (<+>)) -import Prelude ---------------------------------------------------- -- @@ -86,7 +84,7 @@ instance (Pretty k) => Pretty (Result k) where -- (3) Check whether 'w' satisfies the constraint system produced in (1). -- (4) Check whether the R1CS result matches the interpreter result. -- (5) Return the 'Result'. -execute :: (Typeable ty, PrimeField k) => SimplParam -> Comp ty k -> [k] -> Result k +execute :: (Typeable ty, PrimeField k) => [SimplParam] -> Comp ty k -> [k] -> Result k execute simpl mf inputs = let TExpPkg nv in_vars e = compileCompToTexp mf r1cs = compileTExpToR1CS simpl (TExpPkg nv in_vars e) diff --git a/tests/Test/ArkworksBridge.hs b/tests/Test/ArkworksBridge.hs index e1e4703..b0a678f 100644 --- a/tests/Test/ArkworksBridge.hs +++ b/tests/Test/ArkworksBridge.hs @@ -10,9 +10,9 @@ import qualified System.Exit as GHC import System.Process (createProcess, shell, waitForProcess) data CMD k where - CreateTrustedSetup :: (Typeable ty, GaloisField k) => FilePath -> String -> SimplParam -> Comp ty k -> CMD k - CreateProof :: (Typeable ty, GaloisField k) => FilePath -> String -> SimplParam -> Comp ty k -> [k] -> CMD k - RunR1CS :: (Typeable ty, GaloisField k) => FilePath -> String -> SimplParam -> Comp ty k -> [k] -> CMD k + CreateTrustedSetup :: (Typeable ty, GaloisField k) => FilePath -> String -> [SimplParam] -> Comp ty k -> CMD k + CreateProof :: (Typeable ty, GaloisField k) => FilePath -> String -> [SimplParam] -> Comp ty k -> [k] -> CMD k + RunR1CS :: (Typeable ty, GaloisField k) => FilePath -> String -> [SimplParam] -> Comp ty k -> [k] -> CMD k runCMD :: (PrimeField k) => CMD k -> IO GHC.ExitCode runCMD (CreateTrustedSetup rootDir name simpl c) = do diff --git a/tests/Test/Snarkl/UnitSpec.hs b/tests/Test/Snarkl/UnitSpec.hs index 0a3701a..344ae24 100644 --- a/tests/Test/Snarkl/UnitSpec.hs +++ b/tests/Test/Snarkl/UnitSpec.hs @@ -21,7 +21,7 @@ import Test.Hspec (Spec, describe, it, shouldBe, shouldReturn) import Test.Snarkl.Unit.Programs import Prelude -test_comp :: (Typeable ty, PrimeField k) => SimplParam -> Comp ty k -> [k] -> IO (Either ExitCode k) +test_comp :: (Typeable ty, PrimeField k) => [SimplParam] -> Comp ty k -> [k] -> IO (Either ExitCode k) test_comp simpl mf args = do exit_code <- runCMD $ RunR1CS "./scripts" "hspec" simpl mf args @@ -35,266 +35,266 @@ spec :: Spec spec = do describe "Field Tests" $ do describe "if-then-else" $ do - it "1-1" $ test_comp Simplify prog1 [1, 2, 1] `shouldReturn` Right (negate 240) + it "1-1" $ test_comp [Simplify] prog1 [1, 2, 1] `shouldReturn` Right (negate 240) describe "bigsum" $ do - it "2-1" $ test_comp @_ @F_BN128 Simplify (prog2 4) [0] `shouldReturn` Right 10 - it "2-2" $ test_comp @_ @F_BN128 Simplify (prog2 4) [1] `shouldReturn` Right 15 - it "2-3" $ test_comp @_ @F_BN128 Simplify (prog2 4) [2] `shouldReturn` Right 20 - it "2-4" $ test_comp @_ @F_BN128 Simplify (prog2 10) [10] `shouldReturn` Right 165 + it "2-1" $ test_comp @_ @F_BN128 [Simplify] (prog2 4) [0] `shouldReturn` Right 10 + it "2-2" $ test_comp @_ @F_BN128 [Simplify] (prog2 4) [1] `shouldReturn` Right 15 + it "2-3" $ test_comp @_ @F_BN128 [Simplify] (prog2 4) [2] `shouldReturn` Right 20 + it "2-4" $ test_comp @_ @F_BN128 [Simplify] (prog2 10) [10] `shouldReturn` Right 165 describe "arrays" $ do - it "3-1" $ test_comp @_ @F_BN128 Simplify prog3 [8] `shouldReturn` Right 512 - it "3-2" $ test_comp @_ @F_BN128 Simplify prog3 [16] `shouldReturn` Right 4096 - it "3-3" $ test_comp @_ @F_BN128 Simplify prog3 [0] `shouldReturn` Right 0 - it "3-4" $ test_comp @_ @F_BN128 Simplify prog3 [-1] `shouldReturn` Right (-1) - - it "4-1" $ test_comp @_ @F_BN128 Simplify prog4 [8] `shouldReturn` Right 512 - it "4-2" $ test_comp @_ @F_BN128 Simplify prog4 [16] `shouldReturn` Right 4096 - it "4-3" $ test_comp @_ @F_BN128 Simplify prog4 [0] `shouldReturn` Right 0 - it "4-4" $ test_comp @_ @F_BN128 Simplify prog4 [-1] `shouldReturn` Right (-1) - - it "5-1" $ test_comp @_ @F_BN128 Simplify prog5 [4] `shouldReturn` Right (4 ^ (101 :: Integer)) - it "5-2" $ test_comp @_ @F_BN128 Simplify prog5 [5] `shouldReturn` Right (5 ^ (101 :: Integer)) + it "3-1" $ test_comp @_ @F_BN128 [Simplify] prog3 [8] `shouldReturn` Right 512 + it "3-2" $ test_comp @_ @F_BN128 [Simplify] prog3 [16] `shouldReturn` Right 4096 + it "3-3" $ test_comp @_ @F_BN128 [Simplify] prog3 [0] `shouldReturn` Right 0 + it "3-4" $ test_comp @_ @F_BN128 [Simplify] prog3 [-1] `shouldReturn` Right (-1) + + it "4-1" $ test_comp @_ @F_BN128 [Simplify] prog4 [8] `shouldReturn` Right 512 + it "4-2" $ test_comp @_ @F_BN128 [Simplify] prog4 [16] `shouldReturn` Right 4096 + it "4-3" $ test_comp @_ @F_BN128 [Simplify] prog4 [0] `shouldReturn` Right 0 + it "4-4" $ test_comp @_ @F_BN128 [Simplify] prog4 [-1] `shouldReturn` Right (-1) + + it "5-1" $ test_comp @_ @F_BN128 [Simplify] prog5 [4] `shouldReturn` Right (4 ^ (101 :: Integer)) + it "5-2" $ test_comp @_ @F_BN128 [Simplify] prog5 [5] `shouldReturn` Right (5 ^ (101 :: Integer)) -- TODO: INVESTIGATE: FAILS with "EXCEEDS FIELD SIZE" - it "5-2" $ test_comp @_ @F_BN128 Simplify prog5 [5] `shouldReturn` Right (5 ^ (101 :: Integer)) - it "5-3" $ test_comp @_ @F_BN128 Simplify prog5 [0] `shouldReturn` Right 0 - it "5-4" $ test_comp @_ @F_BN128 Simplify prog5 [-1] `shouldReturn` Right (-1) + it "5-2" $ test_comp @_ @F_BN128 [Simplify] prog5 [5] `shouldReturn` Right (5 ^ (101 :: Integer)) + it "5-3" $ test_comp @_ @F_BN128 [Simplify] prog5 [0] `shouldReturn` Right 0 + it "5-4" $ test_comp @_ @F_BN128 [Simplify] prog5 [-1] `shouldReturn` Right (-1) describe "times" $ do - it "6-1" $ test_comp @_ @F_BN128 Simplify prog6 [8] `shouldReturn` Right 8 + it "6-1" $ test_comp @_ @F_BN128 [Simplify] prog6 [8] `shouldReturn` Right 8 describe "forall" $ do - it "7-1" $ test_comp @_ @F_BN128 Simplify prog7 [] `shouldReturn` Right 100 + it "7-1" $ test_comp @_ @F_BN128 [Simplify] prog7 [] `shouldReturn` Right 100 describe "forall2" $ do - it "8-1" $ test_comp @_ @F_BN128 Simplify prog8 [] `shouldReturn` Right 29 + it "8-1" $ test_comp @_ @F_BN128 [Simplify] prog8 [] `shouldReturn` Right 29 describe "unused inputs" $ do - it "11-1" $ test_comp @_ @F_BN128 Simplify prog11 [1, 1] `shouldReturn` Right 1 + it "11-1" $ test_comp @_ @F_BN128 [Simplify] prog11 [1, 1] `shouldReturn` Right 1 describe "multiplicative identity" $ do - it "13-1" $ test_comp @_ @F_BN128 Simplify prog13 [1] `shouldReturn` Right 1 + it "13-1" $ test_comp @_ @F_BN128 [Simplify] prog13 [1] `shouldReturn` Right 1 describe "opt: 0x * 3y = out ~~> out=0" $ do - it "14-1" $ test_comp @_ @F_BN128 Simplify prog14 [3, 4] `shouldReturn` Right 0 + it "14-1" $ test_comp @_ @F_BN128 [Simplify] prog14 [3, 4] `shouldReturn` Right 0 describe "exp_binop smart constructor: 3 - (2 - 1) = 2" $ do - it "15-1" $ test_comp @_ @F_BN128 Simplify prog15 [] `shouldReturn` Right 2 + it "15-1" $ test_comp @_ @F_BN128 [Simplify] prog15 [] `shouldReturn` Right 2 describe "lists" $ do - it "26-1" $ test_comp @_ @F_BN128 Simplify prog26 [] `shouldReturn` Right 33 - it "27-1" $ test_comp @_ @F_BN128 Simplify prog27 [] `shouldReturn` Right 34 - it "28-1" $ test_comp @_ @F_BN128 Simplify prog28 [] `shouldReturn` Right 24 - it "29-1" $ test_comp @_ @F_BN128 Simplify prog29 [1] `shouldReturn` Right 24 - it "30-1" $ test_comp @_ @F_BN128 Simplify prog30 [] `shouldReturn` Right 24 - it "37-1" $ test_comp @_ @F_BN128 Simplify prog37 (30 : take 100 [0 ..]) `shouldReturn` Right 30 + it "26-1" $ test_comp @_ @F_BN128 [Simplify] prog26 [] `shouldReturn` Right 33 + it "27-1" $ test_comp @_ @F_BN128 [Simplify] prog27 [] `shouldReturn` Right 34 + it "28-1" $ test_comp @_ @F_BN128 [Simplify] prog28 [] `shouldReturn` Right 24 + it "29-1" $ test_comp @_ @F_BN128 [Simplify] prog29 [1] `shouldReturn` Right 24 + it "30-1" $ test_comp @_ @F_BN128 [Simplify] prog30 [] `shouldReturn` Right 24 + it "37-1" $ test_comp @_ @F_BN128 [Simplify] prog37 (30 : take 100 [0 ..]) `shouldReturn` Right 30 describe "div" $ do - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [4, 2] `shouldReturn` Right 2 - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [4, 1] `shouldReturn` Right 4 - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [4, 4] `shouldReturn` Right 1 - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [21, 7] `shouldReturn` Right 3 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [4, 2] `shouldReturn` Right 2 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [4, 1] `shouldReturn` Right 4 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [4, 4] `shouldReturn` Right 1 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [21, 7] `shouldReturn` Right 3 describe "beta" $ do - it "34-1" $ test_comp @_ @F_BN128 Simplify prog34 [] `shouldReturn` Right 0 + it "34-1" $ test_comp @_ @F_BN128 [Simplify] prog34 [] `shouldReturn` Right 0 describe "trees" $ do - it "35-1" $ test_comp @_ @F_BN128 Simplify prog35 [1] `shouldReturn` Right 77 + it "35-1" $ test_comp @_ @F_BN128 [Simplify] prog35 [1] `shouldReturn` Right 77 describe "Boolean Tests" $ do describe "and" $ do - it "9-1" $ test_comp @_ @F_BN128 Simplify bool_prog9 [0, 0] `shouldReturn` Right 0 - it "9-2" $ test_comp @_ @F_BN128 Simplify bool_prog9 [0, 1] `shouldReturn` Right 0 - it "9-3" $ test_comp @_ @F_BN128 Simplify bool_prog9 [1, 0] `shouldReturn` Right 0 - it "9-4" $ test_comp @_ @F_BN128 Simplify bool_prog9 [1, 1] `shouldReturn` Right 1 + it "9-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [0, 0] `shouldReturn` Right 0 + it "9-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [0, 1] `shouldReturn` Right 0 + it "9-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [1, 0] `shouldReturn` Right 0 + it "9-4" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [1, 1] `shouldReturn` Right 1 describe "if-then-else" $ do - it "1-1" $ test_comp @_ @F_BN128 Simplify prog1 [1, 2, 1] `shouldReturn` Right (negate 240) + it "1-1" $ test_comp @_ @F_BN128 [Simplify] prog1 [1, 2, 1] `shouldReturn` Right (negate 240) describe "bigsum" $ do - it "2-1" $ test_comp @_ @F_BN128 Simplify (prog2 4) [0] `shouldReturn` Right 10 - it "2-2" $ test_comp @_ @F_BN128 Simplify (prog2 4) [1] `shouldReturn` Right 15 - it "2-3" $ test_comp @_ @F_BN128 Simplify (prog2 4) [2] `shouldReturn` Right 20 - it "2-4" $ test_comp @_ @F_BN128 Simplify (prog2 10) [10] `shouldReturn` Right 165 + it "2-1" $ test_comp @_ @F_BN128 [Simplify] (prog2 4) [0] `shouldReturn` Right 10 + it "2-2" $ test_comp @_ @F_BN128 [Simplify] (prog2 4) [1] `shouldReturn` Right 15 + it "2-3" $ test_comp @_ @F_BN128 [Simplify] (prog2 4) [2] `shouldReturn` Right 20 + it "2-4" $ test_comp @_ @F_BN128 [Simplify] (prog2 10) [10] `shouldReturn` Right 165 describe "arrays" $ do - it "3-1" $ test_comp @_ @F_BN128 Simplify prog3 [8] `shouldReturn` Right 512 - it "3-2" $ test_comp @_ @F_BN128 Simplify prog3 [16] `shouldReturn` Right 4096 - it "3-3" $ test_comp @_ @F_BN128 Simplify prog3 [0] `shouldReturn` Right 0 - it "3-4" $ test_comp @_ @F_BN128 Simplify prog3 [-1] `shouldReturn` Right (-1) - - it "4-1" $ test_comp @_ @F_BN128 Simplify prog4 [8] `shouldReturn` Right 512 - it "4-2" $ test_comp @_ @F_BN128 Simplify prog4 [16] `shouldReturn` Right 4096 - it "4-3" $ test_comp @_ @F_BN128 Simplify prog4 [0] `shouldReturn` Right 0 - it "4-4" $ test_comp @_ @F_BN128 Simplify prog4 [-1] `shouldReturn` Right (-1) - - it "5-1" $ test_comp @_ @F_BN128 Simplify prog5 [4] `shouldReturn` Right (4 ^ (101 :: Integer)) - it "5-2" $ test_comp @_ @F_BN128 Simplify prog5 [5] `shouldReturn` Right (5 ^ (101 :: Integer)) + it "3-1" $ test_comp @_ @F_BN128 [Simplify] prog3 [8] `shouldReturn` Right 512 + it "3-2" $ test_comp @_ @F_BN128 [Simplify] prog3 [16] `shouldReturn` Right 4096 + it "3-3" $ test_comp @_ @F_BN128 [Simplify] prog3 [0] `shouldReturn` Right 0 + it "3-4" $ test_comp @_ @F_BN128 [Simplify] prog3 [-1] `shouldReturn` Right (-1) + + it "4-1" $ test_comp @_ @F_BN128 [Simplify] prog4 [8] `shouldReturn` Right 512 + it "4-2" $ test_comp @_ @F_BN128 [Simplify] prog4 [16] `shouldReturn` Right 4096 + it "4-3" $ test_comp @_ @F_BN128 [Simplify] prog4 [0] `shouldReturn` Right 0 + it "4-4" $ test_comp @_ @F_BN128 [Simplify] prog4 [-1] `shouldReturn` Right (-1) + + it "5-1" $ test_comp @_ @F_BN128 [Simplify] prog5 [4] `shouldReturn` Right (4 ^ (101 :: Integer)) + it "5-2" $ test_comp @_ @F_BN128 [Simplify] prog5 [5] `shouldReturn` Right (5 ^ (101 :: Integer)) -- TODO: INVESTIGATE: FAILS with "EXCEEDS FIELD SIZE" - -- it "5-2" $ test_comp @_ @P_BN128 Simplify prog5 [5] `shouldReturn` Right (5^(101::Integer)) - it "5-3" $ test_comp @_ @F_BN128 Simplify prog5 [0] `shouldReturn` Right 0 - it "5-4" $ test_comp @_ @F_BN128 Simplify prog5 [-1] `shouldReturn` Right (-1) + -- it "5-2" $ test_comp @_ @P_BN128 [Simplify] prog5 [5] `shouldReturn` Right (5^(101::Integer)) + it "5-3" $ test_comp @_ @F_BN128 [Simplify] prog5 [0] `shouldReturn` Right 0 + it "5-4" $ test_comp @_ @F_BN128 [Simplify] prog5 [-1] `shouldReturn` Right (-1) describe "times" $ do - it "6-1" $ test_comp @_ @F_BN128 Simplify prog6 [8] `shouldReturn` Right 8 + it "6-1" $ test_comp @_ @F_BN128 [Simplify] prog6 [8] `shouldReturn` Right 8 describe "forall" $ do - it "7-1" $ test_comp @_ @F_BN128 Simplify prog7 [] `shouldReturn` Right 100 + it "7-1" $ test_comp @_ @F_BN128 [Simplify] prog7 [] `shouldReturn` Right 100 describe "forall2" $ do - it "8-1" $ test_comp @_ @F_BN128 Simplify prog8 [] `shouldReturn` Right 29 + it "8-1" $ test_comp @_ @F_BN128 [Simplify] prog8 [] `shouldReturn` Right 29 describe "unused inputs" $ do - it "11-1" $ test_comp @_ @F_BN128 Simplify prog11 [1, 1] `shouldReturn` Right 1 + it "11-1" $ test_comp @_ @F_BN128 [Simplify] prog11 [1, 1] `shouldReturn` Right 1 describe "multiplicative identity" $ do - it "13-1" $ test_comp @_ @F_BN128 Simplify prog13 [1] `shouldReturn` Right 1 + it "13-1" $ test_comp @_ @F_BN128 [Simplify] prog13 [1] `shouldReturn` Right 1 describe "opt: 0x * 3y = out ~~> out=0" $ do - it "14-1" $ test_comp @_ @F_BN128 Simplify prog14 [3, 4] `shouldReturn` Right 0 + it "14-1" $ test_comp @_ @F_BN128 [Simplify] prog14 [3, 4] `shouldReturn` Right 0 describe "exp_binop smart constructor: 3 - (2 - 1) = 2" $ do - it "15-1" $ test_comp @_ @F_BN128 Simplify prog15 [] `shouldReturn` Right 2 + it "15-1" $ test_comp @_ @F_BN128 [Simplify] prog15 [] `shouldReturn` Right 2 describe "lists" $ do - it "26-1" $ test_comp @_ @F_BN128 Simplify prog26 [] `shouldReturn` Right 33 - it "27-1" $ test_comp @_ @F_BN128 Simplify prog27 [] `shouldReturn` Right 34 - it "28-1" $ test_comp @_ @F_BN128 Simplify prog28 [] `shouldReturn` Right 24 - it "29-1" $ test_comp @_ @F_BN128 Simplify prog29 [1] `shouldReturn` Right 24 - it "30-1" $ test_comp @_ @F_BN128 Simplify prog30 [] `shouldReturn` Right 24 - it "37-1" $ test_comp @_ @F_BN128 Simplify prog37 (30 : take 100 [0 ..]) `shouldReturn` Right 30 + it "26-1" $ test_comp @_ @F_BN128 [Simplify] prog26 [] `shouldReturn` Right 33 + it "27-1" $ test_comp @_ @F_BN128 [Simplify] prog27 [] `shouldReturn` Right 34 + it "28-1" $ test_comp @_ @F_BN128 [Simplify] prog28 [] `shouldReturn` Right 24 + it "29-1" $ test_comp @_ @F_BN128 [Simplify] prog29 [1] `shouldReturn` Right 24 + it "30-1" $ test_comp @_ @F_BN128 [Simplify] prog30 [] `shouldReturn` Right 24 + it "37-1" $ test_comp @_ @F_BN128 [Simplify] prog37 (30 : take 100 [0 ..]) `shouldReturn` Right 30 describe "div" $ do - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [4, 2] `shouldReturn` Right 2 - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [4, 1] `shouldReturn` Right 4 - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [4, 4] `shouldReturn` Right 1 - it "31-1" $ test_comp @_ @F_BN128 Simplify prog31 [21, 7] `shouldReturn` Right 3 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [4, 2] `shouldReturn` Right 2 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [4, 1] `shouldReturn` Right 4 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [4, 4] `shouldReturn` Right 1 + it "31-1" $ test_comp @_ @F_BN128 [Simplify] prog31 [21, 7] `shouldReturn` Right 3 describe "beta" $ do - it "34-1" $ test_comp @_ @F_BN128 Simplify prog34 [] `shouldReturn` Right 0 + it "34-1" $ test_comp @_ @F_BN128 [Simplify] prog34 [] `shouldReturn` Right 0 describe "trees" $ do - it "35-1" $ test_comp @_ @F_BN128 Simplify prog35 [1] `shouldReturn` Right 77 + it "35-1" $ test_comp @_ @F_BN128 [Simplify] prog35 [1] `shouldReturn` Right 77 describe "Boolean Tests" $ do describe "and" $ do - it "9-1" $ test_comp @_ @F_BN128 Simplify bool_prog9 [0, 0] `shouldReturn` Right 0 - it "9-2" $ test_comp @_ @F_BN128 Simplify bool_prog9 [0, 1] `shouldReturn` Right 0 - it "9-3" $ test_comp @_ @F_BN128 Simplify bool_prog9 [1, 0] `shouldReturn` Right 0 - it "9-4" $ test_comp @_ @F_BN128 Simplify bool_prog9 [1, 1] `shouldReturn` Right 1 + it "9-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [0, 0] `shouldReturn` Right 0 + it "9-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [0, 1] `shouldReturn` Right 0 + it "9-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [1, 0] `shouldReturn` Right 0 + it "9-4" $ test_comp @_ @F_BN128 [Simplify] bool_prog9 [1, 1] `shouldReturn` Right 1 describe "xor" $ do - it "10-1" $ test_comp @_ @F_BN128 Simplify bool_prog10 [0, 0] `shouldReturn` Right 0 - it "10-2" $ test_comp @_ @F_BN128 Simplify bool_prog10 [0, 1] `shouldReturn` Right 1 - it "10-3" $ test_comp @_ @F_BN128 Simplify bool_prog10 [1, 0] `shouldReturn` Right 1 - it "10-4" $ test_comp @_ @F_BN128 Simplify bool_prog10 [1, 1] `shouldReturn` Right 0 + it "10-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [0, 0] `shouldReturn` Right 0 + it "10-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [0, 1] `shouldReturn` Right 1 + it "10-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [1, 0] `shouldReturn` Right 1 + it "10-4" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [1, 1] `shouldReturn` Right 0 describe "boolean eq" $ do - it "12-1" $ test_comp @_ @F_BN128 Simplify bool_prog12 [0, 0] `shouldReturn` Right 1 - it "12-2" $ test_comp @_ @F_BN128 Simplify bool_prog12 [0, 1] `shouldReturn` Right 0 - it "12-3" $ test_comp @_ @F_BN128 Simplify bool_prog12 [1, 0] `shouldReturn` Right 0 - it "12-4" $ test_comp @_ @F_BN128 Simplify bool_prog12 [1, 1] `shouldReturn` Right 1 + it "12-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [0, 0] `shouldReturn` Right 1 + it "12-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [0, 1] `shouldReturn` Right 0 + it "12-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [1, 0] `shouldReturn` Right 0 + it "12-4" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [1, 1] `shouldReturn` Right 1 describe "bool inputs" $ do - it "16-1" $ test_comp @_ @F_BN128 Simplify bool_prog16 (replicate 100 1) `shouldReturn` Right 0 + it "16-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog16 (replicate 100 1) `shouldReturn` Right 0 describe "array" $ do - it "17-1" $ test_comp @_ @F_BN128 Simplify bool_prog17 [] `shouldReturn` Right 1 + it "17-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog17 [] `shouldReturn` Right 1 describe "input array" $ do - it "18-1" $ test_comp @_ @F_BN128 Simplify bool_prog18 [0, 1, 0, 1, 0, 1, 0, 1] `shouldReturn` Right 1 + it "18-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog18 [0, 1, 0, 1, 0, 1, 0, 1] `shouldReturn` Right 1 describe "products" $ do - it "19-1" $ test_comp @_ @F_BN128 Simplify bool_prog19 [1, 1] `shouldReturn` Right 1 - it "20-1" $ test_comp @_ @F_BN128 Simplify bool_prog20 [1, 1] `shouldReturn` Right 1 - it "21-1" $ test_comp @_ @F_BN128 Simplify bool_prog21 [0, 1] `shouldReturn` Right 0 + it "19-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog19 [1, 1] `shouldReturn` Right 1 + it "20-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog20 [1, 1] `shouldReturn` Right 1 + it "21-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog21 [0, 1] `shouldReturn` Right 0 describe "products" $ do - it "22-1" $ test_comp @_ @F_BN128 Simplify bool_prog22 [0, 1] `shouldReturn` Right 1 - it "23-1" $ test_comp @_ @F_BN128 Simplify bool_prog23 [0, 1] `shouldReturn` Right 0 + it "22-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog22 [0, 1] `shouldReturn` Right 1 + it "23-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog23 [0, 1] `shouldReturn` Right 0 describe "peano" $ do - it "24-1" $ test_comp @_ @F_BN128 Simplify bool_prog24 [] `shouldReturn` Right 1 + it "24-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog24 [] `shouldReturn` Right 1 describe "lam" $ do - it "25-1" $ test_comp @_ @F_BN128 Simplify bool_prog25 [] `shouldReturn` Right 1 + it "25-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog25 [] `shouldReturn` Right 1 describe "zeq" $ do - it "32-1" $ test_comp @_ @F_BN128 Simplify bool_prog32 [0] `shouldReturn` Right 1 - it "32-2" $ test_comp @_ @F_BN128 Simplify bool_prog32 [1] `shouldReturn` Right 0 - it "32-3" $ test_comp @_ @F_BN128 Simplify bool_prog32 [2] `shouldReturn` Right 0 + it "32-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog32 [0] `shouldReturn` Right 1 + it "32-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog32 [1] `shouldReturn` Right 0 + it "32-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog32 [2] `shouldReturn` Right 0 describe "eq" $ do - it "33-1" $ test_comp @_ @F_BN128 Simplify bool_prog33 [23, 44] `shouldReturn` Right 0 - it "33-2" $ test_comp @_ @F_BN128 Simplify bool_prog33 [0, 100] `shouldReturn` Right 0 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [0, 0] `shouldReturn` Right 1 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [100, 100] `shouldReturn` Right 1 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [-33, 44] `shouldReturn` Right 0 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [-1, -1] `shouldReturn` Right 1 + it "33-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [23, 44] `shouldReturn` Right 0 + it "33-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [0, 100] `shouldReturn` Right 0 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [0, 0] `shouldReturn` Right 1 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [100, 100] `shouldReturn` Right 1 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [-33, 44] `shouldReturn` Right 0 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [-1, -1] `shouldReturn` Right 1 describe "sum" $ do - it "36-1" $ test_comp @_ @F_BN128 Simplify prog36 [0] `shouldReturn` Right 10 - it "36-2" $ test_comp @_ @F_BN128 Simplify prog36 [1] `shouldReturn` Right 7 + it "36-1" $ test_comp @_ @F_BN128 [Simplify] prog36 [0] `shouldReturn` Right 10 + it "36-2" $ test_comp @_ @F_BN128 [Simplify] prog36 [1] `shouldReturn` Right 7 describe "Keccak Tests" $ do describe "keccak" $ do - it "keccak-2" $ test_comp @_ @F_BN128 Simplify (keccak1 2) (fromIntegral <$> input_vals) `shouldReturn` Right 1 - it "keccak-2" $ test_comp @_ @F_BN128 Simplify (keccak1 5) (fromIntegral <$> input_vals) `shouldReturn` Right 1 + it "keccak-2" $ test_comp @_ @F_BN128 [Simplify] (keccak1 2) (fromIntegral <$> input_vals) `shouldReturn` Right 1 + it "keccak-2" $ test_comp @_ @F_BN128 [Simplify] (keccak1 5) (fromIntegral <$> input_vals) `shouldReturn` Right 1 - it "10-1" $ test_comp @_ @F_BN128 Simplify bool_prog10 [0, 0] `shouldReturn` Right 0 - it "10-2" $ test_comp @_ @F_BN128 Simplify bool_prog10 [0, 1] `shouldReturn` Right 1 - it "10-3" $ test_comp @_ @F_BN128 Simplify bool_prog10 [1, 0] `shouldReturn` Right 1 - it "10-4" $ test_comp @_ @F_BN128 Simplify bool_prog10 [1, 1] `shouldReturn` Right 0 + it "10-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [0, 0] `shouldReturn` Right 0 + it "10-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [0, 1] `shouldReturn` Right 1 + it "10-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [1, 0] `shouldReturn` Right 1 + it "10-4" $ test_comp @_ @F_BN128 [Simplify] bool_prog10 [1, 1] `shouldReturn` Right 0 describe "boolean eq" $ do - it "12-1" $ test_comp @_ @F_BN128 Simplify bool_prog12 [0, 0] `shouldReturn` Right 1 - it "12-2" $ test_comp @_ @F_BN128 Simplify bool_prog12 [0, 1] `shouldReturn` Right 0 - it "12-3" $ test_comp @_ @F_BN128 Simplify bool_prog12 [1, 0] `shouldReturn` Right 0 - it "12-4" $ test_comp @_ @F_BN128 Simplify bool_prog12 [1, 1] `shouldReturn` Right 1 + it "12-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [0, 0] `shouldReturn` Right 1 + it "12-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [0, 1] `shouldReturn` Right 0 + it "12-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [1, 0] `shouldReturn` Right 0 + it "12-4" $ test_comp @_ @F_BN128 [Simplify] bool_prog12 [1, 1] `shouldReturn` Right 1 describe "bool inputs" $ do - it "16-1" $ test_comp @_ @F_BN128 Simplify bool_prog16 (replicate 100 1) `shouldReturn` Right 0 + it "16-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog16 (replicate 100 1) `shouldReturn` Right 0 describe "array" $ do - it "17-1" $ test_comp @_ @F_BN128 Simplify bool_prog17 [] `shouldReturn` Right 1 + it "17-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog17 [] `shouldReturn` Right 1 describe "input array" $ do - it "18-1" $ test_comp @_ @F_BN128 Simplify bool_prog18 [0, 1, 0, 1, 0, 1, 0, 1] `shouldReturn` Right 1 + it "18-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog18 [0, 1, 0, 1, 0, 1, 0, 1] `shouldReturn` Right 1 describe "products" $ do - it "19-1" $ test_comp @_ @F_BN128 Simplify bool_prog19 [1, 1] `shouldReturn` Right 1 - it "20-1" $ test_comp @_ @F_BN128 Simplify bool_prog20 [1, 1] `shouldReturn` Right 1 - it "21-1" $ test_comp @_ @F_BN128 Simplify bool_prog21 [0, 1] `shouldReturn` Right 0 + it "19-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog19 [1, 1] `shouldReturn` Right 1 + it "20-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog20 [1, 1] `shouldReturn` Right 1 + it "21-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog21 [0, 1] `shouldReturn` Right 0 describe "products" $ do - it "22-1" $ test_comp @_ @F_BN128 Simplify bool_prog22 [0, 1] `shouldReturn` Right 1 - it "23-1" $ test_comp @_ @F_BN128 Simplify bool_prog23 [0, 1] `shouldReturn` Right 0 + it "22-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog22 [0, 1] `shouldReturn` Right 1 + it "23-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog23 [0, 1] `shouldReturn` Right 0 describe "peano" $ do - it "24-1" $ test_comp @_ @F_BN128 Simplify bool_prog24 [] `shouldReturn` Right 1 + it "24-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog24 [] `shouldReturn` Right 1 describe "lam" $ do - it "25-1" $ test_comp @_ @F_BN128 Simplify bool_prog25 [] `shouldReturn` Right 1 + it "25-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog25 [] `shouldReturn` Right 1 describe "zeq" $ do - it "32-1" $ test_comp @_ @F_BN128 Simplify bool_prog32 [0] `shouldReturn` Right 1 - it "32-2" $ test_comp @_ @F_BN128 Simplify bool_prog32 [1] `shouldReturn` Right 0 - it "32-3" $ test_comp @_ @F_BN128 Simplify bool_prog32 [2] `shouldReturn` Right 0 + it "32-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog32 [0] `shouldReturn` Right 1 + it "32-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog32 [1] `shouldReturn` Right 0 + it "32-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog32 [2] `shouldReturn` Right 0 describe "eq" $ do - it "33-1" $ test_comp @_ @F_BN128 Simplify bool_prog33 [23, 44] `shouldReturn` Right 0 - it "33-2" $ test_comp @_ @F_BN128 Simplify bool_prog33 [0, 100] `shouldReturn` Right 0 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [0, 0] `shouldReturn` Right 1 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [100, 100] `shouldReturn` Right 1 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [-33, 44] `shouldReturn` Right 0 - it "33-3" $ test_comp @_ @F_BN128 Simplify bool_prog33 [-1, -1] `shouldReturn` Right 1 + it "33-1" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [23, 44] `shouldReturn` Right 0 + it "33-2" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [0, 100] `shouldReturn` Right 0 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [0, 0] `shouldReturn` Right 1 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [100, 100] `shouldReturn` Right 1 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [-33, 44] `shouldReturn` Right 0 + it "33-3" $ test_comp @_ @F_BN128 [Simplify] bool_prog33 [-1, -1] `shouldReturn` Right 1 describe "sum" $ do - it "36-1" $ test_comp @_ @F_BN128 Simplify prog36 [0] `shouldReturn` Right 10 - it "36-2" $ test_comp @_ @F_BN128 Simplify prog36 [1] `shouldReturn` Right 7 + it "36-1" $ test_comp @_ @F_BN128 [Simplify] prog36 [0] `shouldReturn` Right 10 + it "36-2" $ test_comp @_ @F_BN128 [Simplify] prog36 [1] `shouldReturn` Right 7 describe "Keccak Tests" $ do describe "keccak" $ do - it "keccak-2" $ test_comp @_ @F_BN128 Simplify (keccak1 2) (fromIntegral <$> input_vals) `shouldReturn` Right 1 - it "keccak-2" $ test_comp @_ @F_BN128 Simplify (keccak1 5) (fromIntegral <$> input_vals) `shouldReturn` Right 1 + it "keccak-2" $ test_comp @_ @F_BN128 [Simplify] (keccak1 2) (fromIntegral <$> input_vals) `shouldReturn` Right 1 + it "keccak-2" $ test_comp @_ @F_BN128 [Simplify] (keccak1 5) (fromIntegral <$> input_vals) `shouldReturn` Right 1 From 8c2a8b92aff009441f96934e9d73cef9f3ba8c78 Mon Sep 17 00:00:00 2001 From: martyall Date: Mon, 15 Jan 2024 14:27:47 -0800 Subject: [PATCH 02/13] CLI commands for r1cs, witness, and runall --- examples/Snarkl/Example/Basic.hs | 2 +- snarkl.cabal | 4 +- src/Snarkl/Backend/R1CS/Poly.hs | 20 +++-- src/Snarkl/Backend/R1CS/R1CS.hs | 49 ++++------- src/Snarkl/Backend/R1CS/Serialize.hs | 73 ++++++++++++----- src/Snarkl/CLI.hs | 41 ++++------ src/Snarkl/CLI/Compile.hs | 64 +++++++++++++-- src/Snarkl/CLI/GenWitness.hs | 117 ++++++++++++++++++++++++++- src/Snarkl/CLI/RunAll.hs | 93 ++++++++++++++++++++- src/Snarkl/Common.hs | 10 ++- src/Snarkl/Compile.hs | 16 ++-- src/Snarkl/Constraint/Constraints.hs | 115 ++++++++++++++++++++++++-- src/Snarkl/Constraint/SimplMonad.hs | 12 +-- src/Snarkl/Constraint/Simplify.hs | 22 ++--- src/Snarkl/Toplevel.hs | 36 ++++++++- 15 files changed, 527 insertions(+), 147 deletions(-) diff --git a/examples/Snarkl/Example/Basic.hs b/examples/Snarkl/Example/Basic.hs index dec403d..4b81b84 100644 --- a/examples/Snarkl/Example/Basic.hs +++ b/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 diff --git a/snarkl.cabal b/snarkl.cabal index 81a51e6..30f3b6f 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -96,7 +96,7 @@ library , optparse-applicative , parallel >=3.2 && <3.3 , process >=1.2 - , streamly + , string-conversions , wl-pprint-text hs-source-dirs: src @@ -224,7 +224,7 @@ executable print-examples , snarkl >=0.1.0.0 , wl-pprint-text -executable compile +executable snarkl main-is: Main.hs other-modules: Snarkl.Example.Basic diff --git a/src/Snarkl/Backend/R1CS/Poly.hs b/src/Snarkl/Backend/R1CS/Poly.hs index 461aef1..d89694c 100644 --- a/src/Snarkl/Backend/R1CS/Poly.hs +++ b/src/Snarkl/Backend/R1CS/Poly.hs @@ -1,9 +1,11 @@ {-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE TypeApplications #-} module Snarkl.Backend.R1CS.Poly where import qualified Data.Aeson as A import Data.Field.Galois (GaloisField, PrimeField, fromP) +import Data.Foldable (toList) import qualified Data.Map as Map import Snarkl.Common import Text.PrettyPrint.Leijen.Text (Pretty (..)) @@ -16,20 +18,22 @@ 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 + let kvs = map (\(var, coeff) -> (show $ fromP coeff, var)) $ Map.toList m in A.toJSON kvs +instance (PrimeField a) => A.FromJSON (Poly a) where + parseJSON = + A.withArray "Poly" $ \arr -> do + kvs <- mapM (A.parseJSON @(String, Var)) arr + let m = Map.fromList $ map (\(k, v) -> (v, fromInteger $ read k)) (toList kvs) + return $ Poly 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 $ Map.singleton (Var (-1)) c -- | The polynomial equal variable 'x' var_poly :: @@ -39,4 +43,4 @@ var_poly :: -- | Resulting polynomial Poly a var_poly (coeff, x) = - Poly $ Map.insert x coeff Map.empty + Poly $ Map.singleton x coeff diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index beacafc..1ad2e38 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -2,7 +2,6 @@ module Snarkl.Backend.R1CS.R1CS ( R1C (..), R1CS (..), sat_r1cs, - wit_of_r1cs, num_constraints, ) where @@ -13,7 +12,7 @@ import Data.Field.Galois (GaloisField, PrimeField) import qualified Data.Map as Map import Snarkl.Backend.R1CS.Poly import Snarkl.Common -import Snarkl.Errors +-- import Snarkl.Errors import Text.PrettyPrint.Leijen.Text (Pretty (..), (<+>)) ---------------------------------------------------------------- @@ -33,6 +32,14 @@ instance (PrimeField k) => A.ToJSON (R1C k) where "C" A..= c ] +instance (PrimeField k) => A.FromJSON (R1C k) where + parseJSON = + A.withObject "R1C" $ \v -> do + a <- v A..: "A" + b <- v A..: "B" + c <- v A..: "C" + pure $ R1C (a, b, c) + instance (Pretty a) => Pretty (R1C a) where pretty (R1C (aV, bV, cV)) = pretty aV <+> "*" <+> pretty bV <+> "==" <+> pretty cV @@ -40,12 +47,12 @@ data R1CS a = R1CS { r1cs_clauses :: [R1C a], r1cs_num_vars :: Int, r1cs_in_vars :: [Var], - r1cs_out_vars :: [Var], - r1cs_gen_witness :: Assgn a -> Assgn a + r1cs_out_vars :: [Var] + -- r1cs_gen_witness :: Assgn a -> Assgn a } + deriving (Show) -instance (Show a) => Show (R1CS a) where - show (R1CS cs nvs ivs ovs _) = show (cs, nvs, ivs, ovs) +-- instance (Show a) => Show (R1CS a) num_constraints :: R1CS a -> Int num_constraints = length . r1cs_clauses @@ -73,32 +80,4 @@ sat_r1cs w cs = and $ is_sat (r1cs_clauses cs) chunk_sz cs0 = truncate $ (fromIntegral (length cs0) :: Rational) / num_chunks g c = - sat_r1c w c - || failWith - ( ErrMsg - ( "witness\n " - ++ show w - ++ "\nfailed to satisfy constraint\n " - ++ show c - ++ "\nin R1CS\n " - ++ show cs - ) - ) - --- | For a given R1CS and inputs, calculate a satisfying assignment. -wit_of_r1cs :: [k] -> R1CS k -> Assgn k -wit_of_r1cs inputs r1cs = - let in_vars = r1cs_in_vars r1cs - f = r1cs_gen_witness r1cs . Map.fromList - in if length in_vars /= length inputs - then - failWith $ - ErrMsg - ( "expected " - ++ show (length in_vars) - ++ " input(s)" - ++ " but got " - ++ show (length inputs) - ++ " input(s)" - ) - else f (zip in_vars inputs) + sat_r1c w c \ No newline at end of file diff --git a/src/Snarkl/Backend/R1CS/Serialize.hs b/src/Snarkl/Backend/R1CS/Serialize.hs index 95dfab4..51b6df9 100644 --- a/src/Snarkl/Backend/R1CS/Serialize.hs +++ b/src/Snarkl/Backend/R1CS/Serialize.hs @@ -1,16 +1,18 @@ +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE RecordWildCards #-} module Snarkl.Backend.R1CS.Serialize where +import Control.Monad.Except (throwError) import qualified Data.Aeson as A -import Data.ByteString.Builder (toLazyByteString) +import Data.ByteString.Builder (Builder, lazyByteString, toLazyByteString) import qualified Data.ByteString.Lazy as LBS import Data.Field.Galois (GaloisField (char, deg), PrimeField, fromP) import Data.List (sortOn) import qualified Data.Map as Map -import JSONL (jsonLine, jsonlBuilder) +import GHC.Generics (Generic) import Snarkl.Backend.R1CS.R1CS (R1CS (..), num_constraints) -import Snarkl.Common (Assgn, Var, incVar) +import Snarkl.Common (Assgn, Var) import Prelude hiding (writeFile) data R1CSHeader k = R1CSHeader @@ -21,17 +23,11 @@ data R1CSHeader k = R1CSHeader input_variables :: [Var], output_variables :: [Var] } + deriving (Generic) -instance (GaloisField k) => A.ToJSON (R1CSHeader k) where - toJSON (R1CSHeader {..}) = - A.object - [ "field_characteristic" A..= show field_characteristic, - "extension_degree" A..= extension_degree, - "n_constraints" A..= n_constraints, - "n_variables" A..= n_variables, - "input_variables" A..= map incVar input_variables, - "output_variables" A..= map incVar output_variables - ] +instance A.ToJSON (R1CSHeader k) + +instance A.FromJSON (R1CSHeader k) r1csToHeader :: (GaloisField k) => R1CS k -> R1CSHeader k r1csToHeader x@(R1CS {..} :: R1CS k) = @@ -47,21 +43,37 @@ r1csToHeader x@(R1CS {..} :: R1CS k) = serializeR1CSAsJson :: (PrimeField k) => R1CS k -> LBS.ByteString serializeR1CSAsJson x = let b = jsonLine (r1csToHeader x) <> jsonlBuilder (r1cs_clauses x) - in toLazyByteString b + in toLazyByteString (unJSONLine b) + +deserializeR1CS :: (PrimeField k) => LBS.ByteString -> Either String (R1CS k) +deserializeR1CS file = do + let ls = LBS.split 0x0a file + case ls of + [] -> throwError "Empty file" + (h : cs) -> do + header <- A.eitherDecode h + clauses <- mapM A.eitherDecode cs + return $ + R1CS + { r1cs_clauses = clauses, + r1cs_num_vars = n_variables header, + r1cs_in_vars = input_variables header, + r1cs_out_vars = output_variables header + } -serializeWitnessAsJson :: (PrimeField k) => R1CS k -> Assgn k -> LBS.ByteString -serializeWitnessAsJson r1cs assgn = - let inputs_assgn = map (\(v, f) -> (incVar v, show $ fromP f)) $ Map.toAscList assgn - b = jsonLine (r1csToHeader r1cs) <> jsonlBuilder inputs_assgn - in toLazyByteString b +serializeWitnessAsJson :: (PrimeField k) => R1CSHeader k -> Assgn k -> LBS.ByteString +serializeWitnessAsJson header assgn = + let inputs_assgn = map (\(v, f) -> (v, show $ fromP f)) $ Map.toAscList assgn + b = jsonLine header <> jsonlBuilder inputs_assgn + in toLazyByteString $ unJSONLine b serializeInputsAsJson :: (PrimeField k) => R1CS k -> [k] -> LBS.ByteString serializeInputsAsJson r1cs inputs = let inputs_assgn = - map (\(v, f) -> (incVar v, show $ fromP f)) $ + map (\(v, f) -> (v, show $ fromP f)) $ sortOn fst $ zip (r1cs_in_vars r1cs) inputs - in toLazyByteString $ jsonlBuilder inputs_assgn + in toLazyByteString $ unJSONLine $ jsonlBuilder inputs_assgn mkR1CSFilePath :: FilePath -> String -> FilePath mkR1CSFilePath rootDir name = rootDir <> "/" <> name <> "-r1cs.jsonl" @@ -71,3 +83,22 @@ mkWitnessFilePath rootDir name = rootDir <> "/" <> name <> "-witness.jsonl" mkInputsFilePath :: FilePath -> String -> FilePath mkInputsFilePath rootDir name = rootDir <> "/" <> name <> "-inputs.jsonl" + +parseInputs :: (PrimeField k) => LBS.ByteString -> Either String [k] +parseInputs file = + map fromInteger <$> do + let ls = LBS.split 0x0a file + case ls of + [] -> pure ([] :: [Integer]) + inputs -> traverse A.eitherDecode inputs + +newtype JSONLine = JSONLine {unJSONLine :: Builder} + +instance Semigroup JSONLine where + JSONLine a <> JSONLine b = JSONLine (a <> "\n" <> b) + +jsonLine :: (A.ToJSON a) => a -> JSONLine +jsonLine = JSONLine . lazyByteString . A.encode + +jsonlBuilder :: (Foldable t, Functor t, A.ToJSON a) => t a -> JSONLine +jsonlBuilder = foldl1 (<>) . fmap jsonLine \ No newline at end of file diff --git a/src/Snarkl/CLI.hs b/src/Snarkl/CLI.hs index 8e46894..7191bb2 100644 --- a/src/Snarkl/CLI.hs +++ b/src/Snarkl/CLI.hs @@ -1,22 +1,19 @@ -{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} module Snarkl.CLI (compiler) where -import qualified Data.ByteString.Lazy as LBS import Data.Field.Galois (PrimeField) -import Data.Maybe (catMaybes) import Data.Typeable (Typeable) -import Options.Applicative (execParser, fullDesc, header, helper, info, (<**>)) -import Snarkl.Backend.R1CS -import Snarkl.CLI.Compile (CompileOpts (..), OptimiseOpts (..), compileOptsParser) -import Snarkl.CLI.GenWitness (GenWitnessOpts (..)) -import Snarkl.Compile -import Snarkl.Constraint () +import Options.Applicative (command, execParser, fullDesc, header, helper, info, progDesc, subparser, (<**>)) +import Snarkl.CLI.Compile (CompileOpts, compile, compileOptsParser) +import Snarkl.CLI.GenWitness (GenWitnessOpts, genWitness, genWitnessOptsParser) +import Snarkl.CLI.RunAll (RunAllOpts, runAll, runAllOptsParser) import Snarkl.Language data CMD = Compile CompileOpts | GenWitness GenWitnessOpts + | RunAll RunAllOpts compiler :: forall ty k. @@ -26,12 +23,16 @@ compiler :: Comp ty k -> IO () compiler name comp = do - compileOpts <- execParser opts - runCMD (Compile compileOpts) name comp + cmd <- execParser opts + runCMD cmd name comp where + cmds = + command "compile" (info (Compile <$> compileOptsParser <**> helper) (progDesc "Compile to program to an r1cs and constraints file")) + <> command "gen-witness" (info (GenWitness <$> genWitnessOptsParser <**> helper) (progDesc "Generate a witness for the program")) + <> command "run-all" (info (RunAll <$> runAllOptsParser <**> helper) (progDesc "Compile to program to an r1cs and constraints file and generate a witness")) opts = info - (compileOptsParser <**> helper) + (subparser cmds <**> helper) ( fullDesc <> header ("Compiling the program " <> name <> " to a ZK-SNARK") ) @@ -45,16 +46,6 @@ runCMD :: Comp ty k -> IO () runCMD cmd name comp = case cmd of - Compile (CompileOpts {..}) -> do - let simpl = - catMaybes - [ if simplify optimiseOpts then Just Simplify else Nothing, - if removeUnreachable optimiseOpts then Just RemoveUnreachable else Nothing - ] - TExpPkg nv in_vars e = compileCompToTexp comp - r1cs = compileTExpToR1CS simpl (TExpPkg nv in_vars e) - r1csFP = mkR1CSFilePath name r1csOutput - LBS.writeFile r1csFP (serializeR1CSAsJson r1cs) - putStrLn $ "Wrote R1CS to file " <> r1csOutput - GenWitness (GenWitnessOpts {..}) -> do - \ No newline at end of file + Compile opts -> compile opts name comp + GenWitness opts -> genWitness opts name comp + RunAll opts -> runAll opts name comp \ No newline at end of file diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index 1f7bf0f..326c2e9 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -1,20 +1,40 @@ +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} + module Snarkl.CLI.Compile - ( OptimiseOpts (..), - CompileOpts (..), + ( CompileOpts (CompileOpts), + compile, compileOptsParser, + OptimizeOpts (..), + optimizeOptsParser, ) where -import Options.Applicative +import Control.Monad (unless) +import qualified Data.Aeson as A +import qualified Data.ByteString.Lazy as LBS +import Data.Field.Galois (PrimeField (fromP)) +import Data.Foldable (Foldable (toList)) +import qualified Data.Map as Map +import Data.Maybe (catMaybes) +import qualified Data.String.Conversions as CS +import Data.Typeable (Typeable) +import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, strOption, subparser, switch, (<**>)) +import Snarkl.Backend.R1CS +import Snarkl.Compile +import Snarkl.Constraint (ConstraintSystem (cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath, parseConstraintSystem, serializeConstraintSystemAsJson) +import Snarkl.Errors (ErrMsg (ErrMsg), failWith) +import Snarkl.Language +import Snarkl.Toplevel (comp_interp, wit_of_cs) -data OptimiseOpts = OptimiseOpts +data OptimizeOpts = OptimizeOpts { simplify :: Bool, removeUnreachable :: Bool } -optimizeOptsParser :: Parser OptimiseOpts +optimizeOptsParser :: Parser OptimizeOpts optimizeOptsParser = - OptimiseOpts + OptimizeOpts <$> switch ( long "simplify" <> help "run the constraint simplifier" @@ -25,8 +45,9 @@ optimizeOptsParser = ) data CompileOpts = CompileOpts - { optimiseOpts :: OptimiseOpts, - r1csOutput :: FilePath + { optimizeOpts :: OptimizeOpts, + r1csOutput :: FilePath, + constraintsOutput :: FilePath } compileOptsParser :: Parser CompileOpts @@ -37,3 +58,30 @@ compileOptsParser = ( long "r1cs-output-dir" <> help "the directory to write the r1cs artifact" ) + <*> strOption + ( long "constraints-output-dir" + <> help "the directory to write the constraints artifact" + ) + +compile :: + forall ty k. + (Typeable ty) => + (PrimeField k) => + CompileOpts -> + String -> + Comp ty k -> + IO () +compile CompileOpts {..} name comp = do + let simpl = + catMaybes + [ if simplify optimizeOpts then Just Simplify else Nothing, + if removeUnreachable optimizeOpts then Just RemoveUnreachable else Nothing + ] + TExpPkg nv in_vars e = compileCompToTexp comp + (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) + r1csFP = mkR1CSFilePath r1csOutput name + LBS.writeFile r1csFP (serializeR1CSAsJson r1cs) + putStrLn $ "Wrote R1CS to file " <> r1csOutput + let csFP = mkConstraintsFilePath constraintsOutput name + LBS.writeFile csFP (serializeConstraintSystemAsJson cs) + putStrLn $ "Wrote constraints to file " <> constraintsOutput \ No newline at end of file diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index e37c707..6c3f167 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -1,11 +1,122 @@ -module Snarkl.CLI.GenWitness where +{-# LANGUAGE RecordWildCards #-} + +module Snarkl.CLI.GenWitness + ( GenWitnessOpts, + genWitnessOptsParser, + genWitness, + InputOpts (..), + inputOptsParser, + ) +where + +import Control.Applicative ((<|>)) +import Control.Monad (unless) +import qualified Data.Aeson as A +import qualified Data.ByteString.Lazy as LBS +import Data.Field.Galois (PrimeField (fromP)) +import Data.Foldable (Foldable (toList)) +import qualified Data.Map as Map +import qualified Data.String.Conversions as CS +import Data.Typeable (Typeable) +import Options.Applicative (Parser, eitherReader, help, long, option, strOption) +import Snarkl.Backend.R1CS +import Snarkl.Constraint (ConstraintSystem (cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath, parseConstraintSystem) +import Snarkl.Errors (ErrMsg (ErrMsg), failWith) +import Snarkl.Language +import Snarkl.Toplevel (comp_interp, wit_of_cs) +import Text.Read (readEither) data InputOpts = Explicit [Integer] | FromFile FilePath +inputOptsParser :: Parser InputOpts +inputOptsParser = + Explicit + <$> option + (eitherReader readEither) + ( long "inputs" + <> help "an input value" + ) + <|> FromFile + <$> strOption + ( long "inputs-dir" + <> help "The directory where the inputs.jsonl file is located" + ) + data GenWitnessOpts = GenWitnessOpts - { r1csInput :: FilePath, + { constraintsInput :: FilePath, + r1csInput :: FilePath, inputs :: InputOpts, witnessOutput :: FilePath - } \ No newline at end of file + } + +genWitnessOptsParser :: Parser GenWitnessOpts +genWitnessOptsParser = + GenWitnessOpts + <$> strOption + ( long "constraints-input-dir" + <> help "the directory where the constrains.jsonl file is located" + ) + <*> strOption + ( long "r1cs-input-dir" + <> help "the directory where the r1cs.jsonl file is located" + ) + <*> inputOptsParser + <*> strOption + ( long "witness-output-dir" + <> help "the directory to write the witness.jsonl file" + ) + +genWitness :: + forall ty k. + (Typeable ty) => + (PrimeField k) => + GenWitnessOpts -> + String -> + Comp ty k -> + IO () +genWitness GenWitnessOpts {..} name comp = do + -- parse the constraints file + let csFP = mkConstraintsFilePath constraintsInput name + constraintsBS <- LBS.readFile csFP + let constraints = either error id $ parseConstraintSystem constraintsBS + [out_var] = cs_out_vars (unSimplifiedConstraintSystem constraints) + -- parse the inputs, either from cli or from file + is <- case inputs of + Explicit is -> pure $ map fromInteger is + FromFile fp -> do + inputsBS <- LBS.readFile fp + either error pure $ parseInputs inputsBS + let out_interp = comp_interp comp is + witness = wit_of_cs is constraints + out = case Map.lookup out_var witness of + Nothing -> + failWith $ + ErrMsg + ( "output variable " + ++ show out_var + ++ "not mapped, in\n " + ++ show witness + ) + Just out_val -> out_val + unless (out_interp == out) $ + failWith $ + ErrMsg $ + "interpreter result " + ++ show out_interp + ++ " differs from actual result " + ++ show out + let r1csFP = mkR1CSFilePath r1csInput name + r1csBS <- LBS.readFile r1csFP + let r1cs = either error id $ deserializeR1CS r1csBS + unless (sat_r1cs witness r1cs) $ + failWith $ + ErrMsg $ + "witness\n " + ++ CS.cs (A.encode $ toList (fromP <$> witness)) + ++ "\nfailed to satisfy R1CS\n " + ++ CS.cs (A.encode $ r1cs_clauses r1cs) + let witnessFP = mkWitnessFilePath witnessOutput name + LBS.writeFile witnessFP (serializeWitnessAsJson (constraintSystemToHeader constraints) witness) + putStrLn $ "Wrote witness to file " <> witnessOutput \ No newline at end of file diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index 3b2cc7b..a360a5c 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -1,9 +1,98 @@ +{-# LANGUAGE RecordWildCards #-} + module Snarkl.CLI.RunAll where -import Snarkl.CLI.GenWitness (InputOpts) +import Control.Monad (unless) +import qualified Data.Aeson as A +import qualified Data.ByteString.Lazy as LBS +import Data.Field.Galois (PrimeField (fromP)) +import Data.Foldable (Foldable (toList)) +import qualified Data.Map as Map +import Data.Maybe (catMaybes) +import qualified Data.String.Conversions as CS +import Data.Typeable (Typeable) +import Options.Applicative (Parser, help, long, strOption) +import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), mkR1CSFilePath, mkWitnessFilePath, parseInputs, r1csToHeader, sat_r1cs, serializeR1CSAsJson, serializeWitnessAsJson) +import Snarkl.CLI.Compile (OptimizeOpts (removeUnreachable, simplify), optimizeOptsParser) +import Snarkl.CLI.GenWitness (InputOpts (Explicit, FromFile), inputOptsParser) +import Snarkl.Compile (SimplParam (RemoveUnreachable, Simplify), TExpPkg (TExpPkg), compileCompToTexp, compileTExpToR1CS) +import Snarkl.Errors (ErrMsg (ErrMsg), failWith) +import Snarkl.Language (Comp) +import Snarkl.Toplevel (comp_interp, wit_of_cs) data RunAllOpts = RunAllOpts { r1csOutput :: FilePath, + optimizeOpts :: OptimizeOpts, inputs :: InputOpts, witnessOutput :: FilePath - } \ No newline at end of file + } + +runAllOptsParser :: Parser RunAllOpts +runAllOptsParser = + RunAllOpts + <$> strOption + ( long "r1cs-output-dir" + <> help "the directory to write the r1cs artifact" + ) + <*> optimizeOptsParser + <*> inputOptsParser + <*> strOption + ( long "witness-output-dir" + <> help "the directory to write the witness.jsonl file" + ) + +runAll :: + forall ty k. + (Typeable ty) => + (PrimeField k) => + RunAllOpts -> + String -> + Comp ty k -> + IO () +runAll RunAllOpts {..} name comp = do + let simpl = + catMaybes + [ if simplify optimizeOpts then Just Simplify else Nothing, + if removeUnreachable optimizeOpts then Just RemoveUnreachable else Nothing + ] + TExpPkg nv in_vars e = compileCompToTexp comp + (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) + let [out_var] = r1cs_out_vars r1cs + -- parse the inputs, either from cli or from file + is <- case inputs of + Explicit is -> pure $ map fromInteger is + FromFile fp -> do + inputsBS <- LBS.readFile fp + either error pure $ parseInputs inputsBS + let out_interp = comp_interp comp is + witness = wit_of_cs is cs + out = case Map.lookup out_var witness of + Nothing -> + failWith $ + ErrMsg + ( "output variable " + ++ show out_var + ++ "not mapped, in\n " + ++ show witness + ) + Just out_val -> out_val + unless (out_interp == out) $ + failWith $ + ErrMsg $ + "interpreter result " + ++ show out_interp + ++ " differs from actual result " + ++ show out + unless (sat_r1cs witness r1cs) $ + failWith $ + ErrMsg $ + "witness\n " + ++ CS.cs (A.encode $ toList (fromP <$> witness)) + ++ "\nfailed to satisfy R1CS\n " + ++ CS.cs (A.encode $ r1cs_clauses r1cs) + let r1csFP = mkR1CSFilePath r1csOutput name + LBS.writeFile r1csFP (serializeR1CSAsJson r1cs) + putStrLn $ "Wrote R1CS to file " <> r1csOutput + let witnessFP = mkWitnessFilePath witnessOutput name + LBS.writeFile witnessFP (serializeWitnessAsJson (r1csToHeader r1cs) witness) + putStrLn $ "Wrote witness to file " <> witnessOutput diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index 953d841..380709f 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -6,7 +6,15 @@ import qualified Data.Aeson as A import qualified Data.Map as Map import Text.PrettyPrint.Leijen.Text (Pretty (pretty)) -newtype Var = Var Int deriving (Eq, Ord, Show, A.ToJSON) +newtype Var = Var Int deriving (Eq, Ord, Show) + +instance A.ToJSON Var where + toJSON (Var i) = A.toJSON (i + 1) + +instance A.FromJSON Var where + parseJSON v = do + i <- A.parseJSON v + return $ Var (i - 1) instance Pretty Var where pretty (Var i) = "x_" <> pretty i diff --git a/src/Snarkl/Compile.hs b/src/Snarkl/Compile.hs index dba6e3f..64fbdfb 100644 --- a/src/Snarkl/Compile.hs +++ b/src/Snarkl/Compile.hs @@ -13,6 +13,7 @@ module Snarkl.Compile ) where +import Control.Arrow (Arrow (second)) import Control.Lens (Iso', iso, view, (#), (^.)) import Control.Monad.State ( State, @@ -32,6 +33,7 @@ import Snarkl.Common (Op (..), UnOp (..), Var (Var), incVar) import Snarkl.Constraint ( Constraint (CMagic, CMult), ConstraintSystem (ConstraintSystem), + SimplifiedConstraintSystem (..), bind_of_var, bind_var, cadd, @@ -40,7 +42,6 @@ import Snarkl.Constraint r1cs_of_cs, removeUnreachable, renumber_constraints, - solve, ) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language @@ -424,7 +425,7 @@ compileConstraintsToR1CS :: (GaloisField a) => [SimplParam] -> ConstraintSystem a -> - R1CS a + (R1CS a, SimplifiedConstraintSystem a) compileConstraintsToR1CS simpls cs = let -- Simplify resulting constraints. cs_simpl = @@ -435,15 +436,14 @@ compileConstraintsToR1CS simpls cs = -- Renumber constraint variables sequentially, from 0 to -- 'max_var'. 'renumber_f' is a function mapping variables to -- their renumbered counterparts. - (_, cs') = renumber_constraints cs_dataflow - -- 'f' is a function mapping input bindings to witnesses. + (_, cs') = second SimplifiedConstraintSystem $ renumber_constraints cs_dataflow + in -- 'f' is a function mapping input bindings to witnesses. -- NOTE: we assume the initial variable assignment passed to -- 'f' is the one derived by zipping the inputs together with -- the (renamed) input vars. of the R1CS produced by this -- function. Alternatively, we could 'Map.mapKeys renumber_f' -- before applying 'solve cs''. - f = solve cs' - in r1cs_of_cs cs' f + (r1cs_of_cs cs', cs') where must_simplify :: Bool must_simplify = Simplify `elem` simpls @@ -550,7 +550,7 @@ compileTExpToR1CS :: (Typeable ty, GaloisField k) => [SimplParam] -> TExpPkg ty k -> - R1CS k + (R1CS k, SimplifiedConstraintSystem k) compileTExpToR1CS simpl = compileConstraintsToR1CS simpl . compileTexpToConstraints -- | Snarkl.Compile Snarkl computations to 'R1CS'. @@ -558,7 +558,7 @@ compileCompToR1CS :: (Typeable ty, GaloisField k) => [SimplParam] -> Comp ty k -> - R1CS k + (R1CS k, SimplifiedConstraintSystem k) compileCompToR1CS simpl = compileConstraintsToR1CS simpl . compileCompToConstraints -------------------------------------------------------------------------------- diff --git a/src/Snarkl/Constraint/Constraints.hs b/src/Snarkl/Constraint/Constraints.hs index 3d43adb..a43b1bb 100644 --- a/src/Snarkl/Constraint/Constraints.hs +++ b/src/Snarkl/Constraint/Constraints.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use camelCase" #-} @@ -8,19 +9,29 @@ module Snarkl.Constraint.Constraints cadd, ConstraintSet, ConstraintSystem (..), + SimplifiedConstraintSystem (..), r1cs_of_cs, renumber_constraints, constraint_vars, + serializeConstraintSystemAsJson, + mkConstraintsFilePath, + parseConstraintSystem, + constraintSystemToHeader, ) where +import Control.Monad.Except (MonadError (throwError)) import Control.Monad.State (State) -import Data.Bifunctor (Bifunctor (first)) -import Data.Field.Galois (GaloisField, Prime) +import qualified Data.Aeson as A +import Data.Bifunctor (Bifunctor (first, second)) +import Data.ByteString.Builder (toLazyByteString) +import qualified Data.ByteString.Lazy as LBS +import Data.Field.Galois (GaloisField (char, deg), Prime, PrimeField (fromP)) +import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map import qualified Data.Set as Set -import Snarkl.Backend.R1CS (Poly (Poly), R1C (R1C), R1CS (R1CS), const_poly, var_poly) -import Snarkl.Common (Assgn, Var (Var)) +import Snarkl.Backend.R1CS (JSONLine (unJSONLine), Poly (Poly), R1C (R1C), R1CS (R1CS), R1CSHeader (..), const_poly, jsonLine, jsonlBuilder, var_poly) +import Snarkl.Common (Var (Var)) import Snarkl.Constraint.SimplMonad (SEnv) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) @@ -31,6 +42,12 @@ import Snarkl.Errors (ErrMsg (ErrMsg), failWith) newtype CoeffList k v = CoeffList {asList :: [(k, v)]} deriving (Eq) +instance (PrimeField v) => A.ToJSON (CoeffList Var v) where + toJSON (CoeffList l) = A.toJSON $ map (second fromP) l + +instance (PrimeField v) => A.FromJSON (CoeffList Var v) where + parseJSON v = CoeffList . map (second fromInteger) <$> A.parseJSON v + -- COEFFLIST INVARIANT: no key appears more than once. Upon duplicate -- insertion, insert field sum of the values. Terms with 0 coeff. are -- implicitly removed. Smart constructor 'cadd' (below) enforces this @@ -73,6 +90,46 @@ data Constraint a | CMult !(a, Var) !(a, Var) !(a, Maybe Var) | CMagic Var [Var] ([Var] -> State (SEnv a) Bool) +instance (PrimeField a) => A.ToJSON (Constraint a) where + toJSON (CAdd a m) = + A.object + [ "tag" A..= ("CAdd" :: String), + "data" + A..= A.object + [ "a" A..= fromP a, + "m" A..= m + ] + ] + toJSON (CMult (c, x) (d, y) (e, mz)) = + A.object + [ "tag" A..= ("CMult" :: String), + "data" + A..= A.object + [ "cx" A..= (fromP c, x), + "dy" A..= (fromP d, y), + "ez" A..= (fromP e, mz) + ] + ] + toJSON (CMagic {}) = error "ToJSON (Constraint a): CMagic not implemented" + +instance (PrimeField a) => A.FromJSON (Constraint a) where + parseJSON = + A.withObject "Constraint" $ \v -> do + tag <- v A..: "tag" + case tag :: String of + "CAdd" -> do + d <- v A..: "data" + a <- d A..: "a" + m <- d A..: "m" + pure $ CAdd (fromInteger a) m + "CMult" -> do + d <- v A..: "data" + cx <- d A..: "cx" + dy <- d A..: "dy" + ez <- d A..: "ez" + pure $ CMult (first fromInteger cx) (first fromInteger dy) (first fromInteger ez) + _ -> error "FromJSON (Constraint a): unknown tag" + -- | Smart constructor enforcing CoeffList invariant cadd :: (GaloisField a) => a -> [(Var, a)] -> Constraint a cadd !a !l = CAdd a (remove_zeros $ coeff_merge $ CoeffList l) @@ -165,14 +222,18 @@ instance (Show a) => Show (Constraint a) where -- Compilation to R1CS ---------------------------------------------------------------- +-- Contains no magic constraints, hence we can serialize them +newtype SimplifiedConstraintSystem a = SimplifiedConstraintSystem + { unSimplifiedConstraintSystem :: ConstraintSystem a + } + deriving (Show, Eq) + r1cs_of_cs :: (GaloisField a) => -- | Constraints - ConstraintSystem a -> - -- | Witness generator - (Assgn a -> Assgn a) -> + SimplifiedConstraintSystem a -> R1CS a -r1cs_of_cs cs = +r1cs_of_cs (SimplifiedConstraintSystem cs) = R1CS (go $ Set.toList $ cs_constraints cs) (cs_num_vars cs) @@ -250,3 +311,41 @@ renumber_constraints cs = CMult (c, renum_f x) (d, renum_f y) (e, fmap renum_f mz) CMagic nm xs f -> CMagic nm (map renum_f xs) f + +constraintSystemToHeader :: (GaloisField k) => SimplifiedConstraintSystem k -> R1CSHeader k +constraintSystemToHeader (SimplifiedConstraintSystem (ConstraintSystem {..} :: ConstraintSystem k)) = + R1CSHeader + { field_characteristic = toInteger $ char (undefined :: k), + extension_degree = toInteger $ deg (undefined :: k), + n_constraints = Set.size cs_constraints, + -- TODO: should we also add the number of output variables? We do this for + -- the R1CS header, but the examples i checked didn't seem to work + n_variables = cs_num_vars, + input_variables = cs_in_vars, + output_variables = cs_out_vars + } + +serializeConstraintSystemAsJson :: (PrimeField k) => SimplifiedConstraintSystem k -> LBS.ByteString +serializeConstraintSystemAsJson cs = + let b = jsonLine (constraintSystemToHeader cs) <> jsonlBuilder (toList $ cs_constraints $ unSimplifiedConstraintSystem cs) + in toLazyByteString $ unJSONLine b + +parseConstraintSystem :: (PrimeField k) => LBS.ByteString -> Either String (SimplifiedConstraintSystem k) +parseConstraintSystem file = do + let ls = LBS.split 0x0a file + case ls of + [] -> throwError "Empty file" + (h : cs) -> do + header <- A.eitherDecode h + constraints <- traverse A.eitherDecode cs + return $ + SimplifiedConstraintSystem $ + ConstraintSystem + { cs_constraints = Set.fromList constraints, + cs_num_vars = n_variables header, + cs_in_vars = input_variables header, + cs_out_vars = output_variables header + } + +mkConstraintsFilePath :: FilePath -> String -> FilePath +mkConstraintsFilePath rootDir name = rootDir <> "/" <> name <> "-constraints.jsonl" \ No newline at end of file diff --git a/src/Snarkl/Constraint/SimplMonad.hs b/src/Snarkl/Constraint/SimplMonad.hs index da43648..e7591ea 100644 --- a/src/Snarkl/Constraint/SimplMonad.hs +++ b/src/Snarkl/Constraint/SimplMonad.hs @@ -9,7 +9,6 @@ module Snarkl.Constraint.SimplMonad bind_of_var, assgn_of_vars, SolveMode (..), - solve_mode_flag, ) where @@ -85,13 +84,4 @@ assgn_of_vars vars = Left _ -> [] Right c -> [(x, c)] ) - $ zip vars binds - --- | Are we in solve mode? -solve_mode_flag :: State (SEnv a) Bool -solve_mode_flag = - do - env <- get - case solve_mode env of - UseMagic -> return True - JustSimplify -> return False + $ zip vars binds \ No newline at end of file diff --git a/src/Snarkl/Constraint/Simplify.hs b/src/Snarkl/Constraint/Simplify.hs index fb65a83..4c2e376 100644 --- a/src/Snarkl/Constraint/Simplify.hs +++ b/src/Snarkl/Constraint/Simplify.hs @@ -6,7 +6,7 @@ module Snarkl.Constraint.Simplify ) where -import Control.Monad.State (State, evalState, when) +import Control.Monad.State (State, evalState, gets, when) import Data.Field.Galois (GaloisField) import Data.List (foldl') import qualified Data.Set as Set @@ -20,13 +20,12 @@ import Snarkl.Constraint.Constraints constraint_vars, ) import Snarkl.Constraint.SimplMonad - ( SEnv (SEnv), + ( SEnv (SEnv, solve_mode), SolveMode (JustSimplify, UseMagic), assgn_of_vars, bind_of_var, bind_var, root_of_var, - solve_mode_flag, unite_vars, ) import qualified Snarkl.Constraint.UnionFind as UF @@ -46,14 +45,15 @@ subst_constr :: subst_constr !constr = case constr of CMagic !_ !xs !mf -> do - solve <- solve_mode_flag - if solve - then do - b <- mf xs - if b - then return $ cadd 0 [] - else return constr - else return constr + solveMode <- gets solve_mode + case solveMode of + UseMagic -> + do + b <- mf xs + if b + then return $ cadd 0 [] + else return constr + JustSimplify -> return constr CAdd a m -> do -- Variables resolvable to constants diff --git a/src/Snarkl/Toplevel.hs b/src/Snarkl/Toplevel.hs index 7b55c99..be08535 100644 --- a/src/Snarkl/Toplevel.hs +++ b/src/Snarkl/Toplevel.hs @@ -9,6 +9,7 @@ module Snarkl.Toplevel -- * Convenience functions Result (..), execute, + wit_of_cs, -- * Re-exported modules module Snarkl.Language, @@ -24,7 +25,7 @@ import Data.Typeable (Typeable) import Snarkl.Backend.R1CS import Snarkl.Common (Assgn) import Snarkl.Compile -import Snarkl.Constraint () +import Snarkl.Constraint (ConstraintSystem (cs_in_vars), SimplifiedConstraintSystem (..), solve) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Interp (interp) import Snarkl.Language @@ -87,9 +88,9 @@ instance (Pretty k) => Pretty (Result k) where execute :: (Typeable ty, PrimeField k) => [SimplParam] -> Comp ty k -> [k] -> Result k execute simpl mf inputs = let TExpPkg nv in_vars e = compileCompToTexp mf - r1cs = compileTExpToR1CS simpl (TExpPkg nv in_vars e) + (r1cs, constraintSystem) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) [out_var] = r1cs_out_vars r1cs - wit = wit_of_r1cs inputs r1cs + wit = wit_of_cs inputs constraintSystem out = case Map.lookup out_var wit of Nothing -> failWith $ @@ -118,3 +119,32 @@ execute simpl mf inputs = nw = r1cs_num_vars r1cs ng = num_constraints r1cs in Result result nw ng out r1cs wit + +-- +-- data ConstraintSystem a = ConstraintSystem +-- { cs_constraints :: ConstraintSet a, +-- cs_num_vars :: Int, +-- cs_in_vars :: [Var], +-- cs_out_vars :: [Var] +-- } +-- deriving (Show, Eq) + +-- | For a given R1CS and inputs, calculate a satisfying assignment. +wit_of_cs :: (GaloisField k) => [k] -> SimplifiedConstraintSystem k -> Assgn k +wit_of_cs inputs (SimplifiedConstraintSystem cs) = + let in_vars = cs_in_vars cs + f = gen_witness . Map.fromList + in if length in_vars /= length inputs + then + failWith $ + ErrMsg + ( "expected " + ++ show (length in_vars) + ++ " input(s)" + ++ " but got " + ++ show (length inputs) + ++ " input(s)" + ) + else f (zip in_vars inputs) + where + gen_witness = solve cs \ No newline at end of file From 1d59894da4189f817879fac2304017c45da2cb19 Mon Sep 17 00:00:00 2001 From: martyall Date: Mon, 15 Jan 2024 14:28:06 -0800 Subject: [PATCH 03/13] formatting --- snarkl.cabal | 38 ++++++++++++++-------------- src/Snarkl/Backend/R1CS/R1CS.hs | 2 +- src/Snarkl/Backend/R1CS/Serialize.hs | 2 +- src/Snarkl/CLI.hs | 2 +- src/Snarkl/CLI/Compile.hs | 2 +- src/Snarkl/CLI/GenWitness.hs | 2 +- src/Snarkl/Constraint/Constraints.hs | 2 +- src/Snarkl/Constraint/SimplMonad.hs | 2 +- src/Snarkl/Toplevel.hs | 2 +- 9 files changed, 27 insertions(+), 27 deletions(-) diff --git a/snarkl.cabal b/snarkl.cabal index 30f3b6f..3c6fb15 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -36,6 +36,7 @@ library Snarkl.Backend.R1CS.Poly Snarkl.Backend.R1CS.R1CS Snarkl.Backend.R1CS.Serialize + Snarkl.CLI Snarkl.Common Snarkl.Compile Snarkl.Constraint @@ -55,7 +56,6 @@ library Snarkl.Language.SyntaxMonad Snarkl.Language.TExpr Snarkl.Toplevel - Snarkl.CLI other-modules: Snarkl.CLI.Compile @@ -84,18 +84,18 @@ library 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 + , galois-field >=1.0.4 + , hspec >=2.0 + , jsonl >=0.1.4 , lens - , mtl >=2.2 && <2.3 + , mtl >=2.2 && <2.3 , optparse-applicative - , parallel >=3.2 && <3.3 - , process >=1.2 + , parallel >=3.2 && <3.3 + , process >=1.2 , string-conversions , wl-pprint-text @@ -149,7 +149,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 @@ -217,11 +217,11 @@ 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 snarkl @@ -249,9 +249,9 @@ executable snarkl 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 diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index 1ad2e38..d599e3f 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -80,4 +80,4 @@ sat_r1cs w cs = and $ is_sat (r1cs_clauses cs) chunk_sz cs0 = truncate $ (fromIntegral (length cs0) :: Rational) / num_chunks g c = - sat_r1c w c \ No newline at end of file + sat_r1c w c diff --git a/src/Snarkl/Backend/R1CS/Serialize.hs b/src/Snarkl/Backend/R1CS/Serialize.hs index 51b6df9..72c54e0 100644 --- a/src/Snarkl/Backend/R1CS/Serialize.hs +++ b/src/Snarkl/Backend/R1CS/Serialize.hs @@ -101,4 +101,4 @@ jsonLine :: (A.ToJSON a) => a -> JSONLine jsonLine = JSONLine . lazyByteString . A.encode jsonlBuilder :: (Foldable t, Functor t, A.ToJSON a) => t a -> JSONLine -jsonlBuilder = foldl1 (<>) . fmap jsonLine \ No newline at end of file +jsonlBuilder = foldl1 (<>) . fmap jsonLine diff --git a/src/Snarkl/CLI.hs b/src/Snarkl/CLI.hs index 7191bb2..30d316a 100644 --- a/src/Snarkl/CLI.hs +++ b/src/Snarkl/CLI.hs @@ -48,4 +48,4 @@ runCMD :: runCMD cmd name comp = case cmd of Compile opts -> compile opts name comp GenWitness opts -> genWitness opts name comp - RunAll opts -> runAll opts name comp \ No newline at end of file + RunAll opts -> runAll opts name comp diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index 326c2e9..ea16db0 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -84,4 +84,4 @@ compile CompileOpts {..} name comp = do putStrLn $ "Wrote R1CS to file " <> r1csOutput let csFP = mkConstraintsFilePath constraintsOutput name LBS.writeFile csFP (serializeConstraintSystemAsJson cs) - putStrLn $ "Wrote constraints to file " <> constraintsOutput \ No newline at end of file + putStrLn $ "Wrote constraints to file " <> constraintsOutput diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index 6c3f167..89649cd 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -119,4 +119,4 @@ genWitness GenWitnessOpts {..} name comp = do ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name LBS.writeFile witnessFP (serializeWitnessAsJson (constraintSystemToHeader constraints) witness) - putStrLn $ "Wrote witness to file " <> witnessOutput \ No newline at end of file + putStrLn $ "Wrote witness to file " <> witnessOutput diff --git a/src/Snarkl/Constraint/Constraints.hs b/src/Snarkl/Constraint/Constraints.hs index a43b1bb..292cf1f 100644 --- a/src/Snarkl/Constraint/Constraints.hs +++ b/src/Snarkl/Constraint/Constraints.hs @@ -348,4 +348,4 @@ parseConstraintSystem file = do } mkConstraintsFilePath :: FilePath -> String -> FilePath -mkConstraintsFilePath rootDir name = rootDir <> "/" <> name <> "-constraints.jsonl" \ No newline at end of file +mkConstraintsFilePath rootDir name = rootDir <> "/" <> name <> "-constraints.jsonl" diff --git a/src/Snarkl/Constraint/SimplMonad.hs b/src/Snarkl/Constraint/SimplMonad.hs index e7591ea..e7d2bc8 100644 --- a/src/Snarkl/Constraint/SimplMonad.hs +++ b/src/Snarkl/Constraint/SimplMonad.hs @@ -84,4 +84,4 @@ assgn_of_vars vars = Left _ -> [] Right c -> [(x, c)] ) - $ zip vars binds \ No newline at end of file + $ zip vars binds diff --git a/src/Snarkl/Toplevel.hs b/src/Snarkl/Toplevel.hs index be08535..bc6536f 100644 --- a/src/Snarkl/Toplevel.hs +++ b/src/Snarkl/Toplevel.hs @@ -147,4 +147,4 @@ wit_of_cs inputs (SimplifiedConstraintSystem cs) = ) else f (zip in_vars inputs) where - gen_witness = solve cs \ No newline at end of file + gen_witness = solve cs From 3b3fd02080eefc7e85ad2f3503a0c6e750702734 Mon Sep 17 00:00:00 2001 From: martyall Date: Mon, 15 Jan 2024 15:05:49 -0800 Subject: [PATCH 04/13] add default values --- app/Main.hs | 30 ++++----------------------- snarkl.cabal | 3 +++ src/Snarkl/CLI.hs | 33 +++++++++++------------------- src/Snarkl/CLI/Compile.hs | 14 +++++++------ src/Snarkl/CLI/GenWitness.hs | 10 ++++++--- src/Snarkl/CLI/RunAll.hs | 13 +++++++----- src/Snarkl/CLI/Utils.hs | 17 +++++++++++++++ tests/Test/Snarkl/Unit/Programs.hs | 1 + 8 files changed, 60 insertions(+), 61 deletions(-) create mode 100644 src/Snarkl/CLI/Utils.hs diff --git a/app/Main.hs b/app/Main.hs index 8b57cee..3a16d85 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,31 +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.CLI (compiler) -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 = compiler "prog2" (Programs.prog2 10 :: Comp 'TField F_BN128) - --- 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 "prog2" (Programs.prog2 10 :: Comp 'TField F_BN128) diff --git a/snarkl.cabal b/snarkl.cabal index 3c6fb15..7814461 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -61,6 +61,7 @@ library Snarkl.CLI.Compile Snarkl.CLI.GenWitness Snarkl.CLI.RunAll + Snarkl.CLI.Utils default-extensions: BangPatterns @@ -88,6 +89,8 @@ library , bytestring , Cabal >=1.22 , containers >=0.5 && <0.7 + , directory + , filepath , galois-field >=1.0.4 , hspec >=2.0 , jsonl >=0.1.4 diff --git a/src/Snarkl/CLI.hs b/src/Snarkl/CLI.hs index 30d316a..fe6f3a5 100644 --- a/src/Snarkl/CLI.hs +++ b/src/Snarkl/CLI.hs @@ -1,6 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} -module Snarkl.CLI (compiler) where +module Snarkl.CLI (defaultMain) where import Data.Field.Galois (PrimeField) import Data.Typeable (Typeable) @@ -15,37 +15,28 @@ data CMD | GenWitness GenWitnessOpts | RunAll RunAllOpts -compiler :: +defaultMain :: forall ty k. (Typeable ty) => (PrimeField k) => String -> Comp ty k -> IO () -compiler name comp = do - cmd <- execParser opts - runCMD cmd name comp +defaultMain name comp = do + _opts <- execParser opts + runCMD _opts where cmds = - command "compile" (info (Compile <$> compileOptsParser <**> helper) (progDesc "Compile to program to an r1cs and constraints file")) - <> command "gen-witness" (info (GenWitness <$> genWitnessOptsParser <**> helper) (progDesc "Generate a witness for the program")) - <> command "run-all" (info (RunAll <$> runAllOptsParser <**> helper) (progDesc "Compile to program to an r1cs and constraints file and generate a witness")) + command "compile" (info (Compile <$> compileOptsParser <**> helper) (progDesc "Compile the program to an r1cs and constraint system")) + <> command "solve" (info (GenWitness <$> genWitnessOptsParser <**> helper) (progDesc "Generate a witness for the program")) + <> command "run-all" (info (RunAll <$> runAllOptsParser <**> helper) (progDesc "Compile the program to an r1cs and generate a witness (useful for testing)")) opts = info (subparser cmds <**> helper) ( fullDesc <> header ("Compiling the program " <> name <> " to a ZK-SNARK") ) - -runCMD :: - forall ty k. - (Typeable ty) => - (PrimeField k) => - CMD -> - String -> - Comp ty k -> - IO () -runCMD cmd name comp = case cmd of - Compile opts -> compile opts name comp - GenWitness opts -> genWitness opts name comp - RunAll opts -> runAll opts name comp + runCMD cmd = case cmd of + Compile _opts -> compile _opts name comp + GenWitness _opts -> genWitness _opts name comp + RunAll _opts -> runAll _opts name comp diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index ea16db0..d5da24e 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -12,15 +12,15 @@ where import Control.Monad (unless) import qualified Data.Aeson as A -import qualified Data.ByteString.Lazy as LBS import Data.Field.Galois (PrimeField (fromP)) import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) -import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, strOption, subparser, switch, (<**>)) +import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, strOption, subparser, switch, value, (<**>)) import Snarkl.Backend.R1CS +import qualified Snarkl.CLI.Utils as Utils import Snarkl.Compile import Snarkl.Constraint (ConstraintSystem (cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath, parseConstraintSystem, serializeConstraintSystemAsJson) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) @@ -57,10 +57,12 @@ compileOptsParser = <*> strOption ( long "r1cs-output-dir" <> help "the directory to write the r1cs artifact" + <> value "./snarkl-output" ) <*> strOption ( long "constraints-output-dir" <> help "the directory to write the constraints artifact" + <> value "./snarkl-output" ) compile :: @@ -80,8 +82,8 @@ compile CompileOpts {..} name comp = do TExpPkg nv in_vars e = compileCompToTexp comp (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) r1csFP = mkR1CSFilePath r1csOutput name - LBS.writeFile r1csFP (serializeR1CSAsJson r1cs) - putStrLn $ "Wrote R1CS to file " <> r1csOutput + Utils.writeFile r1csFP (serializeR1CSAsJson r1cs) + putStrLn $ "Wrote R1CS to " <> r1csFP let csFP = mkConstraintsFilePath constraintsOutput name - LBS.writeFile csFP (serializeConstraintSystemAsJson cs) - putStrLn $ "Wrote constraints to file " <> constraintsOutput + Utils.writeFile csFP (serializeConstraintSystemAsJson cs) + putStrLn $ "Wrote constraints to " <> csFP diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index 89649cd..94e1d7d 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -18,8 +18,9 @@ import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) -import Options.Applicative (Parser, eitherReader, help, long, option, strOption) +import Options.Applicative (Parser, eitherReader, help, long, option, strOption, value) import Snarkl.Backend.R1CS +import qualified Snarkl.CLI.Utils as Utils import Snarkl.Constraint (ConstraintSystem (cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath, parseConstraintSystem) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language @@ -57,15 +58,18 @@ genWitnessOptsParser = <$> strOption ( long "constraints-input-dir" <> help "the directory where the constrains.jsonl file is located" + <> value "./snarkl-output" ) <*> strOption ( long "r1cs-input-dir" <> help "the directory where the r1cs.jsonl file is located" + <> value "./snarkl-output" ) <*> inputOptsParser <*> strOption ( long "witness-output-dir" <> help "the directory to write the witness.jsonl file" + <> value "./snarkl-output" ) genWitness :: @@ -118,5 +122,5 @@ genWitness GenWitnessOpts {..} name comp = do ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name - LBS.writeFile witnessFP (serializeWitnessAsJson (constraintSystemToHeader constraints) witness) - putStrLn $ "Wrote witness to file " <> witnessOutput + Utils.writeFile witnessFP (serializeWitnessAsJson (constraintSystemToHeader constraints) witness) + putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index a360a5c..c0566ba 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -11,10 +11,11 @@ import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) -import Options.Applicative (Parser, help, long, strOption) +import Options.Applicative (Parser, help, long, strOption, value) import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), mkR1CSFilePath, mkWitnessFilePath, parseInputs, r1csToHeader, sat_r1cs, serializeR1CSAsJson, serializeWitnessAsJson) import Snarkl.CLI.Compile (OptimizeOpts (removeUnreachable, simplify), optimizeOptsParser) import Snarkl.CLI.GenWitness (InputOpts (Explicit, FromFile), inputOptsParser) +import qualified Snarkl.CLI.Utils as Utils import Snarkl.Compile (SimplParam (RemoveUnreachable, Simplify), TExpPkg (TExpPkg), compileCompToTexp, compileTExpToR1CS) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language (Comp) @@ -33,12 +34,14 @@ runAllOptsParser = <$> strOption ( long "r1cs-output-dir" <> help "the directory to write the r1cs artifact" + <> value "./snarkl-output" ) <*> optimizeOptsParser <*> inputOptsParser <*> strOption ( long "witness-output-dir" <> help "the directory to write the witness.jsonl file" + <> value "./snarkl-output" ) runAll :: @@ -91,8 +94,8 @@ runAll RunAllOpts {..} name comp = do ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let r1csFP = mkR1CSFilePath r1csOutput name - LBS.writeFile r1csFP (serializeR1CSAsJson r1cs) - putStrLn $ "Wrote R1CS to file " <> r1csOutput + Utils.writeFile r1csFP (serializeR1CSAsJson r1cs) + putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name - LBS.writeFile witnessFP (serializeWitnessAsJson (r1csToHeader r1cs) witness) - putStrLn $ "Wrote witness to file " <> witnessOutput + Utils.writeFile witnessFP (serializeWitnessAsJson (r1csToHeader r1cs) witness) + putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/Utils.hs b/src/Snarkl/CLI/Utils.hs new file mode 100644 index 0000000..ced7263 --- /dev/null +++ b/src/Snarkl/CLI/Utils.hs @@ -0,0 +1,17 @@ +module Snarkl.CLI.Utils where + +import qualified Data.ByteString.Lazy as LBS +import System.Directory (createDirectoryIfMissing) +import System.FilePath (takeDirectory) + +createDirForFile :: FilePath -> IO () +createDirForFile filePath = + createDirectoryIfMissing True (takeDirectory filePath) + +writeFile :: + FilePath -> + LBS.ByteString -> + IO () +writeFile filePath contents = do + createDirForFile filePath + LBS.writeFile filePath contents diff --git a/tests/Test/Snarkl/Unit/Programs.hs b/tests/Test/Snarkl/Unit/Programs.hs index fa316ef..bf96b05 100644 --- a/tests/Test/Snarkl/Unit/Programs.hs +++ b/tests/Test/Snarkl/Unit/Programs.hs @@ -52,6 +52,7 @@ prog1 = -- For example, the following code calculates the R1CS expression -- (n+e) + (n-1+e) + (n-2+e) + ... + (n-(n-1)+e) -- with e an fresh_input expression. +prog2 :: forall a k. (GaloisField a) => Int -> State (Env k) (TExp 'TField a) prog2 n = do e <- fresh_input From 14120460bb977d6b9550239b3f94399d23d2dc06 Mon Sep 17 00:00:00 2001 From: martyall Date: Tue, 16 Jan 2024 10:05:17 -0800 Subject: [PATCH 05/13] uniform serializtion --- snarkl.cabal | 4 +- src/Snarkl/Backend/R1CS/Poly.hs | 29 ++++------- src/Snarkl/Backend/R1CS/R1CS.hs | 18 +++---- src/Snarkl/Backend/R1CS/Serialize.hs | 74 +++------------------------- src/Snarkl/CLI/Compile.hs | 14 +++--- src/Snarkl/CLI/GenWitness.hs | 59 ++++++++++++++-------- src/Snarkl/CLI/RunAll.hs | 28 ++++++----- src/Snarkl/CLI/Utils.hs | 17 ------- src/Snarkl/Common.hs | 26 +++++++++- src/Snarkl/Compile.hs | 4 +- src/Snarkl/Constraint/Constraints.hs | 56 ++++++--------------- src/Snarkl/Constraint/SimplMonad.hs | 3 +- src/Snarkl/Constraint/Simplify.hs | 4 +- src/Snarkl/Constraint/Solve.hs | 15 +++--- src/Snarkl/Toplevel.hs | 26 +++------- src/Snarkl/Utils.hs | 72 +++++++++++++++++++++++++++ 16 files changed, 224 insertions(+), 225 deletions(-) delete mode 100644 src/Snarkl/CLI/Utils.hs create mode 100644 src/Snarkl/Utils.hs diff --git a/snarkl.cabal b/snarkl.cabal index 7814461..796f049 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -61,7 +61,7 @@ library Snarkl.CLI.Compile Snarkl.CLI.GenWitness Snarkl.CLI.RunAll - Snarkl.CLI.Utils + Snarkl.Utils default-extensions: BangPatterns @@ -79,6 +79,8 @@ library RankNTypes ScopedTypeVariables StandaloneDeriving + TupleSections + TypeApplications TypeFamilies TypeSynonymInstances UndecidableInstances diff --git a/src/Snarkl/Backend/R1CS/Poly.hs b/src/Snarkl/Backend/R1CS/Poly.hs index d89694c..77d196a 100644 --- a/src/Snarkl/Backend/R1CS/Poly.hs +++ b/src/Snarkl/Backend/R1CS/Poly.hs @@ -1,11 +1,7 @@ -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE TypeApplications #-} - module Snarkl.Backend.R1CS.Poly where import qualified Data.Aeson as A -import Data.Field.Galois (GaloisField, PrimeField, fromP) -import Data.Foldable (toList) +import Data.Field.Galois (GaloisField, PrimeField) import qualified Data.Map as Map import Snarkl.Common import Text.PrettyPrint.Leijen.Text (Pretty (..)) @@ -15,25 +11,20 @@ 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 - instance (PrimeField a) => A.ToJSON (Poly a) where - toJSON :: Poly a -> A.Value - toJSON (Poly m) = - let kvs = map (\(var, coeff) -> (show $ fromP coeff, var)) $ Map.toList m - in A.toJSON kvs + toJSON (Poly m) = A.toJSON m instance (PrimeField a) => A.FromJSON (Poly a) where - parseJSON = - A.withArray "Poly" $ \arr -> do - kvs <- mapM (A.parseJSON @(String, Var)) arr - let m = Map.fromList $ map (\(k, v) -> (v, fromInteger $ read k)) (toList kvs) - return $ Poly m + parseJSON v = do + m <- A.parseJSON v + return (Poly m) + +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.singleton (Var (-1)) c +const_poly c = Poly $ Assgn $ Map.singleton (Var (-1)) c -- | The polynomial equal variable 'x' var_poly :: @@ -43,4 +34,4 @@ var_poly :: -- | Resulting polynomial Poly a var_poly (coeff, x) = - Poly $ Map.singleton x coeff + Poly $ Assgn $ Map.singleton x coeff diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index d599e3f..fd5cee9 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -1,6 +1,7 @@ module Snarkl.Backend.R1CS.R1CS ( R1C (..), R1CS (..), + Witness (..), sat_r1cs, num_constraints, ) @@ -48,31 +49,30 @@ data R1CS a = R1CS r1cs_num_vars :: Int, r1cs_in_vars :: [Var], r1cs_out_vars :: [Var] - -- r1cs_gen_witness :: Assgn a -> Assgn a } deriving (Show) --- instance (Show a) => Show (R1CS a) +newtype Witness k = Witness {unWitness :: Assgn k} deriving (Show, Foldable, Functor) num_constraints :: R1CS a -> Int num_constraints = length . r1cs_clauses -- sat_r1c: Does witness 'w' satisfy constraint 'c'? -sat_r1c :: (GaloisField a) => Assgn a -> R1C a -> Bool +sat_r1c :: (GaloisField a) => Witness a -> R1C a -> Bool sat_r1c w c | R1C (aV, bV, cV) <- c = inner aV w * inner bV w == inner cV w where - inner :: (GaloisField a) => Poly a -> Assgn a -> a - inner (Poly v) w' = + inner :: (GaloisField a) => Poly a -> Witness a -> a + inner (Poly (Assgn v)) (Witness (Assgn wit)) = let c0 = Map.findWithDefault 0 (Var (-1)) v - in Map.foldlWithKey (f w') c0 v + in Map.foldlWithKey (f wit) c0 v - f w' acc v_key v_val = - (v_val * Map.findWithDefault 0 v_key w') + acc + f wit acc v_key v_val = + (v_val * Map.findWithDefault 0 v_key wit) + acc -- sat_r1cs: Does witness 'w' satisfy constraint set 'cs'? -sat_r1cs :: (GaloisField a) => Assgn a -> R1CS a -> Bool +sat_r1cs :: (GaloisField a) => Witness a -> R1CS a -> Bool sat_r1cs w cs = and $ is_sat (r1cs_clauses cs) where is_sat cs0 = map g cs0 `using` parListChunk (chunk_sz cs0) rseq diff --git a/src/Snarkl/Backend/R1CS/Serialize.hs b/src/Snarkl/Backend/R1CS/Serialize.hs index 72c54e0..e3b6adc 100644 --- a/src/Snarkl/Backend/R1CS/Serialize.hs +++ b/src/Snarkl/Backend/R1CS/Serialize.hs @@ -3,19 +3,13 @@ module Snarkl.Backend.R1CS.Serialize where -import Control.Monad.Except (throwError) import qualified Data.Aeson as A -import Data.ByteString.Builder (Builder, lazyByteString, toLazyByteString) -import qualified Data.ByteString.Lazy as LBS -import Data.Field.Galois (GaloisField (char, deg), PrimeField, fromP) -import Data.List (sortOn) -import qualified Data.Map as Map +import Data.Field.Galois (GaloisField (char, deg)) import GHC.Generics (Generic) import Snarkl.Backend.R1CS.R1CS (R1CS (..), num_constraints) -import Snarkl.Common (Assgn, Var) -import Prelude hiding (writeFile) +import Snarkl.Common (Var) -data R1CSHeader k = R1CSHeader +data ConstraintHeader k = ConstraintHeader { field_characteristic :: Integer, extension_degree :: Integer, n_constraints :: Int, @@ -25,13 +19,13 @@ data R1CSHeader k = R1CSHeader } deriving (Generic) -instance A.ToJSON (R1CSHeader k) +instance A.ToJSON (ConstraintHeader k) -instance A.FromJSON (R1CSHeader k) +instance A.FromJSON (ConstraintHeader k) -r1csToHeader :: (GaloisField k) => R1CS k -> R1CSHeader k +r1csToHeader :: (GaloisField k) => R1CS k -> ConstraintHeader k r1csToHeader x@(R1CS {..} :: R1CS k) = - R1CSHeader + ConstraintHeader { field_characteristic = toInteger $ char (undefined :: k), extension_degree = toInteger $ deg (undefined :: k), n_constraints = num_constraints x, @@ -40,41 +34,6 @@ r1csToHeader x@(R1CS {..} :: R1CS k) = output_variables = r1cs_out_vars } -serializeR1CSAsJson :: (PrimeField k) => R1CS k -> LBS.ByteString -serializeR1CSAsJson x = - let b = jsonLine (r1csToHeader x) <> jsonlBuilder (r1cs_clauses x) - in toLazyByteString (unJSONLine b) - -deserializeR1CS :: (PrimeField k) => LBS.ByteString -> Either String (R1CS k) -deserializeR1CS file = do - let ls = LBS.split 0x0a file - case ls of - [] -> throwError "Empty file" - (h : cs) -> do - header <- A.eitherDecode h - clauses <- mapM A.eitherDecode cs - return $ - R1CS - { r1cs_clauses = clauses, - r1cs_num_vars = n_variables header, - r1cs_in_vars = input_variables header, - r1cs_out_vars = output_variables header - } - -serializeWitnessAsJson :: (PrimeField k) => R1CSHeader k -> Assgn k -> LBS.ByteString -serializeWitnessAsJson header assgn = - let inputs_assgn = map (\(v, f) -> (v, show $ fromP f)) $ Map.toAscList assgn - b = jsonLine header <> jsonlBuilder inputs_assgn - in toLazyByteString $ unJSONLine b - -serializeInputsAsJson :: (PrimeField k) => R1CS k -> [k] -> LBS.ByteString -serializeInputsAsJson r1cs inputs = - let inputs_assgn = - map (\(v, f) -> (v, show $ fromP f)) $ - sortOn fst $ - zip (r1cs_in_vars r1cs) inputs - in toLazyByteString $ unJSONLine $ jsonlBuilder inputs_assgn - mkR1CSFilePath :: FilePath -> String -> FilePath mkR1CSFilePath rootDir name = rootDir <> "/" <> name <> "-r1cs.jsonl" @@ -83,22 +42,3 @@ mkWitnessFilePath rootDir name = rootDir <> "/" <> name <> "-witness.jsonl" mkInputsFilePath :: FilePath -> String -> FilePath mkInputsFilePath rootDir name = rootDir <> "/" <> name <> "-inputs.jsonl" - -parseInputs :: (PrimeField k) => LBS.ByteString -> Either String [k] -parseInputs file = - map fromInteger <$> do - let ls = LBS.split 0x0a file - case ls of - [] -> pure ([] :: [Integer]) - inputs -> traverse A.eitherDecode inputs - -newtype JSONLine = JSONLine {unJSONLine :: Builder} - -instance Semigroup JSONLine where - JSONLine a <> JSONLine b = JSONLine (a <> "\n" <> b) - -jsonLine :: (A.ToJSON a) => a -> JSONLine -jsonLine = JSONLine . lazyByteString . A.encode - -jsonlBuilder :: (Foldable t, Functor t, A.ToJSON a) => t a -> JSONLine -jsonlBuilder = foldl1 (<>) . fmap jsonLine diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index d5da24e..2d32234 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -12,20 +12,20 @@ where import Control.Monad (unless) import qualified Data.Aeson as A -import Data.Field.Galois (PrimeField (fromP)) +import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) -import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, strOption, subparser, switch, value, (<**>)) +import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, showDefault, strOption, subparser, switch, value, (<**>)) import Snarkl.Backend.R1CS -import qualified Snarkl.CLI.Utils as Utils import Snarkl.Compile -import Snarkl.Constraint (ConstraintSystem (cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath, parseConstraintSystem, serializeConstraintSystemAsJson) +import Snarkl.Constraint (ConstraintSystem (cs_constraints, cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language import Snarkl.Toplevel (comp_interp, wit_of_cs) +import qualified Snarkl.Utils as Utils data OptimizeOpts = OptimizeOpts { simplify :: Bool, @@ -58,11 +58,13 @@ compileOptsParser = ( long "r1cs-output-dir" <> help "the directory to write the r1cs artifact" <> value "./snarkl-output" + <> showDefault ) <*> strOption ( long "constraints-output-dir" <> help "the directory to write the constraints artifact" <> value "./snarkl-output" + <> showDefault ) compile :: @@ -82,8 +84,8 @@ compile CompileOpts {..} name comp = do TExpPkg nv in_vars e = compileCompToTexp comp (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) r1csFP = mkR1CSFilePath r1csOutput name - Utils.writeFile r1csFP (serializeR1CSAsJson r1cs) + Utils.writeJSONLines r1csFP (Just $ r1csToHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let csFP = mkConstraintsFilePath constraintsOutput name - Utils.writeFile csFP (serializeConstraintSystemAsJson cs) + Utils.writeJSONLines csFP (Just $ constraintSystemToHeader cs) (toList $ cs_constraints $ unSimplifiedConstraintSystem cs) putStrLn $ "Wrote constraints to " <> csFP diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index 94e1d7d..871e297 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -12,19 +12,22 @@ where import Control.Applicative ((<|>)) import Control.Monad (unless) import qualified Data.Aeson as A -import qualified Data.ByteString.Lazy as LBS -import Data.Field.Galois (PrimeField (fromP)) +import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map +import qualified Data.Set as Set import qualified Data.String.Conversions as CS -import Data.Typeable (Typeable) -import Options.Applicative (Parser, eitherReader, help, long, option, strOption, value) +import Data.Typeable (Proxy (Proxy), Typeable) +import Data.Void (Void) +import Options.Applicative (Parser, eitherReader, help, long, option, showDefault, strOption, value) import Snarkl.Backend.R1CS -import qualified Snarkl.CLI.Utils as Utils -import Snarkl.Constraint (ConstraintSystem (cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath, parseConstraintSystem) +import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem, unFieldElem)) +import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (SimplifiedConstraintSystem, unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language import Snarkl.Toplevel (comp_interp, wit_of_cs) +import qualified Snarkl.Utils as LBS +import qualified Snarkl.Utils as Utils import Text.Read (readEither) data InputOpts @@ -59,17 +62,20 @@ genWitnessOptsParser = ( long "constraints-input-dir" <> help "the directory where the constrains.jsonl file is located" <> value "./snarkl-output" + <> showDefault ) <*> strOption ( long "r1cs-input-dir" <> help "the directory where the r1cs.jsonl file is located" <> value "./snarkl-output" + <> showDefault ) <*> inputOptsParser <*> strOption ( long "witness-output-dir" <> help "the directory to write the witness.jsonl file" <> value "./snarkl-output" + <> showDefault ) genWitness :: @@ -82,19 +88,25 @@ genWitness :: IO () genWitness GenWitnessOpts {..} name comp = do -- parse the constraints file - let csFP = mkConstraintsFilePath constraintsInput name - constraintsBS <- LBS.readFile csFP - let constraints = either error id $ parseConstraintSystem constraintsBS - [out_var] = cs_out_vars (unSimplifiedConstraintSystem constraints) + constraints <- do + let csFP = mkConstraintsFilePath constraintsInput name + (Just ConstraintHeader {..}, cs) <- LBS.readJSONLines csFP (Just $ Proxy @(ConstraintHeader k)) + pure $ + SimplifiedConstraintSystem $ + ConstraintSystem + { cs_constraints = Set.fromList cs, + cs_num_vars = n_variables, + cs_in_vars = input_variables, + cs_out_vars = output_variables + } + let [out_var] = cs_out_vars (unSimplifiedConstraintSystem constraints) -- parse the inputs, either from cli or from file is <- case inputs of Explicit is -> pure $ map fromInteger is - FromFile fp -> do - inputsBS <- LBS.readFile fp - either error pure $ parseInputs inputsBS + FromFile fp -> map unFieldElem . snd <$> Utils.readJSONLines fp (Nothing :: Maybe (Proxy Void)) let out_interp = comp_interp comp is - witness = wit_of_cs is constraints - out = case Map.lookup out_var witness of + witness@(Witness (Assgn m)) = wit_of_cs is constraints + out = case Map.lookup out_var m of Nothing -> failWith $ ErrMsg @@ -111,16 +123,23 @@ genWitness GenWitnessOpts {..} name comp = do ++ show out_interp ++ " differs from actual result " ++ show out - let r1csFP = mkR1CSFilePath r1csInput name - r1csBS <- LBS.readFile r1csFP - let r1cs = either error id $ deserializeR1CS r1csBS + r1cs <- do + let r1csFP = mkR1CSFilePath r1csInput name + (Just ConstraintHeader {..}, items) <- Utils.readJSONLines r1csFP (Just $ Proxy @(ConstraintHeader k)) + pure $ + R1CS + { r1cs_clauses = items, + r1cs_num_vars = n_variables, + r1cs_in_vars = input_variables, + r1cs_out_vars = output_variables + } unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ "witness\n " - ++ CS.cs (A.encode $ toList (fromP <$> witness)) + ++ CS.cs (A.encode $ toList (FieldElem <$> witness)) ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name - Utils.writeFile witnessFP (serializeWitnessAsJson (constraintSystemToHeader constraints) witness) + Utils.writeJSONLines witnessFP (Just $ constraintSystemToHeader constraints) (FieldElem <$> witness) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index c0566ba..eb9f000 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -4,22 +4,24 @@ module Snarkl.CLI.RunAll where import Control.Monad (unless) import qualified Data.Aeson as A -import qualified Data.ByteString.Lazy as LBS -import Data.Field.Galois (PrimeField (fromP)) +import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map import Data.Maybe (catMaybes) +import Data.Proxy (Proxy) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) -import Options.Applicative (Parser, help, long, strOption, value) -import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), mkR1CSFilePath, mkWitnessFilePath, parseInputs, r1csToHeader, sat_r1cs, serializeR1CSAsJson, serializeWitnessAsJson) +import Data.Void (Void) +import Options.Applicative (Parser, help, long, showDefault, strOption, value) +import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), Witness (Witness), mkR1CSFilePath, mkWitnessFilePath, r1csToHeader, sat_r1cs) import Snarkl.CLI.Compile (OptimizeOpts (removeUnreachable, simplify), optimizeOptsParser) import Snarkl.CLI.GenWitness (InputOpts (Explicit, FromFile), inputOptsParser) -import qualified Snarkl.CLI.Utils as Utils +import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem, unFieldElem)) import Snarkl.Compile (SimplParam (RemoveUnreachable, Simplify), TExpPkg (TExpPkg), compileCompToTexp, compileTExpToR1CS) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language (Comp) import Snarkl.Toplevel (comp_interp, wit_of_cs) +import qualified Snarkl.Utils as Utils data RunAllOpts = RunAllOpts { r1csOutput :: FilePath, @@ -35,6 +37,7 @@ runAllOptsParser = ( long "r1cs-output-dir" <> help "the directory to write the r1cs artifact" <> value "./snarkl-output" + <> showDefault ) <*> optimizeOptsParser <*> inputOptsParser @@ -42,6 +45,7 @@ runAllOptsParser = ( long "witness-output-dir" <> help "the directory to write the witness.jsonl file" <> value "./snarkl-output" + <> showDefault ) runAll :: @@ -64,12 +68,10 @@ runAll RunAllOpts {..} name comp = do -- parse the inputs, either from cli or from file is <- case inputs of Explicit is -> pure $ map fromInteger is - FromFile fp -> do - inputsBS <- LBS.readFile fp - either error pure $ parseInputs inputsBS + FromFile fp -> map unFieldElem . snd <$> Utils.readJSONLines fp (Nothing :: Maybe (Proxy Void)) let out_interp = comp_interp comp is - witness = wit_of_cs is cs - out = case Map.lookup out_var witness of + witness@(Witness (Assgn m)) = wit_of_cs is cs + out = case Map.lookup out_var m of Nothing -> failWith $ ErrMsg @@ -90,12 +92,12 @@ runAll RunAllOpts {..} name comp = do failWith $ ErrMsg $ "witness\n " - ++ CS.cs (A.encode $ toList (fromP <$> witness)) + ++ CS.cs (A.encode $ toList (FieldElem <$> witness)) ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let r1csFP = mkR1CSFilePath r1csOutput name - Utils.writeFile r1csFP (serializeR1CSAsJson r1cs) + Utils.writeJSONLines r1csFP (Just $ r1csToHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name - Utils.writeFile witnessFP (serializeWitnessAsJson (r1csToHeader r1cs) witness) + Utils.writeJSONLines witnessFP (Just $ r1csToHeader r1cs) (fmap FieldElem witness) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/Utils.hs b/src/Snarkl/CLI/Utils.hs deleted file mode 100644 index ced7263..0000000 --- a/src/Snarkl/CLI/Utils.hs +++ /dev/null @@ -1,17 +0,0 @@ -module Snarkl.CLI.Utils where - -import qualified Data.ByteString.Lazy as LBS -import System.Directory (createDirectoryIfMissing) -import System.FilePath (takeDirectory) - -createDirForFile :: FilePath -> IO () -createDirForFile filePath = - createDirectoryIfMissing True (takeDirectory filePath) - -writeFile :: - FilePath -> - LBS.ByteString -> - IO () -writeFile filePath contents = do - createDirForFile filePath - LBS.writeFile filePath contents diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index 380709f..4e41464 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -3,6 +3,8 @@ module Snarkl.Common where import qualified Data.Aeson as A +import Data.Field.Galois (PrimeField (fromP)) +import Data.Foldable (Foldable (toList)) import qualified Data.Map as Map import Text.PrettyPrint.Leijen.Text (Pretty (pretty)) @@ -22,7 +24,29 @@ instance Pretty Var where incVar :: Var -> Var incVar (Var i) = Var (i + 1) -type Assgn a = Map.Map Var a +newtype Assgn a = Assgn (Map.Map Var a) deriving (Show, Eq, Functor, Foldable) + +newtype FieldElem k = FieldElem {unFieldElem :: k} deriving (Show, Eq) + +instance (PrimeField k) => A.ToJSON (FieldElem k) where + toJSON (FieldElem k) = A.toJSON (show $ fromP k) + +instance (PrimeField k) => A.FromJSON (FieldElem k) where + parseJSON v = do + k <- A.parseJSON v + return $ FieldElem (fromInteger $ read k) + +instance (PrimeField a) => A.ToJSON (Assgn a) where + toJSON (Assgn m) = + let kvs = map (\(var, coeff) -> (FieldElem coeff, var)) $ Map.toList m + in A.toJSON kvs + +instance (PrimeField a) => A.FromJSON (Assgn a) where + parseJSON = + A.withArray "Assgn" $ \arr -> do + kvs <- mapM A.parseJSON arr + let m = Map.fromList $ map (\(FieldElem k, v) -> (v, k)) (toList kvs) + return (Assgn m) data UnOp = ZEq deriving (Eq, Show) diff --git a/src/Snarkl/Compile.hs b/src/Snarkl/Compile.hs index 64fbdfb..b30fee1 100644 --- a/src/Snarkl/Compile.hs +++ b/src/Snarkl/Compile.hs @@ -29,7 +29,7 @@ import Data.Sequence (pattern Empty, pattern (:<|)) import qualified Data.Set as Set import Data.Typeable (Typeable) import Snarkl.Backend.R1CS.R1CS (R1CS) -import Snarkl.Common (Op (..), UnOp (..), Var (Var), incVar) +import Snarkl.Common (Assgn (Assgn), Op (..), UnOp (..), Var (Var), incVar) import Snarkl.Constraint ( Constraint (CMagic, CMult), ConstraintSystem (ConstraintSystem), @@ -430,7 +430,7 @@ compileConstraintsToR1CS simpls cs = let -- Simplify resulting constraints. cs_simpl = if must_simplify - then snd $ do_simplify False Map.empty cs + then snd $ do_simplify False (Assgn Map.empty) cs else cs cs_dataflow = if must_dataflow then removeUnreachable cs_simpl else cs_simpl -- Renumber constraint variables sequentially, from 0 to diff --git a/src/Snarkl/Constraint/Constraints.hs b/src/Snarkl/Constraint/Constraints.hs index 292cf1f..5ae0588 100644 --- a/src/Snarkl/Constraint/Constraints.hs +++ b/src/Snarkl/Constraint/Constraints.hs @@ -13,25 +13,19 @@ module Snarkl.Constraint.Constraints r1cs_of_cs, renumber_constraints, constraint_vars, - serializeConstraintSystemAsJson, mkConstraintsFilePath, - parseConstraintSystem, constraintSystemToHeader, ) where -import Control.Monad.Except (MonadError (throwError)) import Control.Monad.State (State) import qualified Data.Aeson as A import Data.Bifunctor (Bifunctor (first, second)) -import Data.ByteString.Builder (toLazyByteString) -import qualified Data.ByteString.Lazy as LBS -import Data.Field.Galois (GaloisField (char, deg), Prime, PrimeField (fromP)) -import Data.Foldable (Foldable (toList)) +import Data.Field.Galois (GaloisField (char, deg), Prime, PrimeField) import qualified Data.Map as Map import qualified Data.Set as Set -import Snarkl.Backend.R1CS (JSONLine (unJSONLine), Poly (Poly), R1C (R1C), R1CS (R1CS), R1CSHeader (..), const_poly, jsonLine, jsonlBuilder, var_poly) -import Snarkl.Common (Var (Var)) +import Snarkl.Backend.R1CS (ConstraintHeader (..), Poly (Poly), R1C (R1C), R1CS (R1CS), const_poly, var_poly) +import Snarkl.Common (Assgn (Assgn), FieldElem (..), Var (Var)) import Snarkl.Constraint.SimplMonad (SEnv) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) @@ -43,10 +37,10 @@ newtype CoeffList k v = CoeffList {asList :: [(k, v)]} deriving (Eq) instance (PrimeField v) => A.ToJSON (CoeffList Var v) where - toJSON (CoeffList l) = A.toJSON $ map (second fromP) l + toJSON (CoeffList l) = A.toJSON $ map (second FieldElem) l instance (PrimeField v) => A.FromJSON (CoeffList Var v) where - parseJSON v = CoeffList . map (second fromInteger) <$> A.parseJSON v + parseJSON v = CoeffList . map (second unFieldElem) <$> A.parseJSON v -- COEFFLIST INVARIANT: no key appears more than once. Upon duplicate -- insertion, insert field sum of the values. Terms with 0 coeff. are @@ -96,7 +90,7 @@ instance (PrimeField a) => A.ToJSON (Constraint a) where [ "tag" A..= ("CAdd" :: String), "data" A..= A.object - [ "a" A..= fromP a, + [ "a" A..= FieldElem a, "m" A..= m ] ] @@ -105,9 +99,9 @@ instance (PrimeField a) => A.ToJSON (Constraint a) where [ "tag" A..= ("CMult" :: String), "data" A..= A.object - [ "cx" A..= (fromP c, x), - "dy" A..= (fromP d, y), - "ez" A..= (fromP e, mz) + [ "cx" A..= (FieldElem c, x), + "dy" A..= (FieldElem d, y), + "ez" A..= (FieldElem e, mz) ] ] toJSON (CMagic {}) = error "ToJSON (Constraint a): CMagic not implemented" @@ -121,13 +115,13 @@ instance (PrimeField a) => A.FromJSON (Constraint a) where d <- v A..: "data" a <- d A..: "a" m <- d A..: "m" - pure $ CAdd (fromInteger a) m + pure $ CAdd (unFieldElem a) m "CMult" -> do d <- v A..: "data" cx <- d A..: "cx" dy <- d A..: "dy" ez <- d A..: "ez" - pure $ CMult (first fromInteger cx) (first fromInteger dy) (first fromInteger ez) + pure $ CMult (first unFieldElem cx) (first unFieldElem dy) (first unFieldElem ez) _ -> error "FromJSON (Constraint a): unknown tag" -- | Smart constructor enforcing CoeffList invariant @@ -244,7 +238,7 @@ r1cs_of_cs (SimplifiedConstraintSystem cs) = go (CAdd a m : cs') = R1C ( const_poly 1, - Poly $ Map.insert (Var (-1)) a $ Map.fromList (asList m), + Poly $ Assgn $ Map.insert (Var (-1)) a $ Map.fromList (asList m), const_poly 0 ) : go cs' @@ -312,9 +306,9 @@ renumber_constraints cs = CMagic nm xs f -> CMagic nm (map renum_f xs) f -constraintSystemToHeader :: (GaloisField k) => SimplifiedConstraintSystem k -> R1CSHeader k +constraintSystemToHeader :: (GaloisField k) => SimplifiedConstraintSystem k -> ConstraintHeader k constraintSystemToHeader (SimplifiedConstraintSystem (ConstraintSystem {..} :: ConstraintSystem k)) = - R1CSHeader + ConstraintHeader { field_characteristic = toInteger $ char (undefined :: k), extension_degree = toInteger $ deg (undefined :: k), n_constraints = Set.size cs_constraints, @@ -325,27 +319,5 @@ constraintSystemToHeader (SimplifiedConstraintSystem (ConstraintSystem {..} :: C output_variables = cs_out_vars } -serializeConstraintSystemAsJson :: (PrimeField k) => SimplifiedConstraintSystem k -> LBS.ByteString -serializeConstraintSystemAsJson cs = - let b = jsonLine (constraintSystemToHeader cs) <> jsonlBuilder (toList $ cs_constraints $ unSimplifiedConstraintSystem cs) - in toLazyByteString $ unJSONLine b - -parseConstraintSystem :: (PrimeField k) => LBS.ByteString -> Either String (SimplifiedConstraintSystem k) -parseConstraintSystem file = do - let ls = LBS.split 0x0a file - case ls of - [] -> throwError "Empty file" - (h : cs) -> do - header <- A.eitherDecode h - constraints <- traverse A.eitherDecode cs - return $ - SimplifiedConstraintSystem $ - ConstraintSystem - { cs_constraints = Set.fromList constraints, - cs_num_vars = n_variables header, - cs_in_vars = input_variables header, - cs_out_vars = output_variables header - } - mkConstraintsFilePath :: FilePath -> String -> FilePath mkConstraintsFilePath rootDir name = rootDir <> "/" <> name <> "-constraints.jsonl" diff --git a/src/Snarkl/Constraint/SimplMonad.hs b/src/Snarkl/Constraint/SimplMonad.hs index e7d2bc8..4f864df 100644 --- a/src/Snarkl/Constraint/SimplMonad.hs +++ b/src/Snarkl/Constraint/SimplMonad.hs @@ -15,7 +15,7 @@ where import Control.Monad.State import Data.Field.Galois (GaloisField) import qualified Data.Map as Map -import Snarkl.Common (Assgn, Var) +import Snarkl.Common (Assgn (Assgn), Var) import qualified Snarkl.Constraint.UnionFind as UF ---------------------------------------------------------------- @@ -78,6 +78,7 @@ assgn_of_vars vars = do binds <- mapM bind_of_var vars return + $ Assgn $ Map.fromList $ concatMap ( \(x, ec) -> case ec of diff --git a/src/Snarkl/Constraint/Simplify.hs b/src/Snarkl/Constraint/Simplify.hs index 4c2e376..b8d26ec 100644 --- a/src/Snarkl/Constraint/Simplify.hs +++ b/src/Snarkl/Constraint/Simplify.hs @@ -10,7 +10,7 @@ import Control.Monad.State (State, evalState, gets, when) import Data.Field.Galois (GaloisField) import Data.List (foldl') import qualified Data.Set as Set -import Snarkl.Common (Assgn, Var) +import Snarkl.Common (Assgn (Assgn), Var) import Snarkl.Constraint.Constraints ( CoeffList (CoeffList, asList), Constraint (..), @@ -185,7 +185,7 @@ do_simplify :: ConstraintSystem a -> -- | Resulting assignment, simplified constraint set (Assgn a, ConstraintSystem a) -do_simplify in_solve_mode env cs = +do_simplify in_solve_mode (Assgn env) cs = -- NOTE: Pinned vars include: -- - input vars -- - output vars diff --git a/src/Snarkl/Constraint/Solve.hs b/src/Snarkl/Constraint/Solve.hs index 56084f7..8c1e028 100644 --- a/src/Snarkl/Constraint/Solve.hs +++ b/src/Snarkl/Constraint/Solve.hs @@ -5,10 +5,8 @@ where import Data.Field.Galois (GaloisField) import qualified Data.Map as Map -import Data.Maybe - ( isJust, - ) -import Snarkl.Common (Assgn, Var (..)) +import Data.Set (member) +import Snarkl.Common (Assgn (Assgn), Var (..)) import Snarkl.Constraint.Constraints ( ConstraintSystem (cs_in_vars, cs_num_vars, cs_out_vars), ) @@ -56,6 +54,9 @@ solve cs env = ++ show cs ) where - all_assigned vars0 assgn = all (is_mapped assgn) vars0 - is_mapped assgn x = isJust (Map.lookup x assgn) - unassigned vars0 assgn = [x | x <- vars0, not $ is_mapped assgn x] + all_assigned vars0 (Assgn assgn) = + let known = Map.keysSet assgn + in all (`member` known) vars0 + unassigned vars0 (Assgn assgn) = + let known = Map.keysSet assgn + in [x | x <- vars0, not $ x `member` known] diff --git a/src/Snarkl/Toplevel.hs b/src/Snarkl/Toplevel.hs index bc6536f..063c768 100644 --- a/src/Snarkl/Toplevel.hs +++ b/src/Snarkl/Toplevel.hs @@ -23,7 +23,7 @@ import Data.List (intercalate) import qualified Data.Map as Map import Data.Typeable (Typeable) import Snarkl.Backend.R1CS -import Snarkl.Common (Assgn) +import Snarkl.Common (Assgn (Assgn)) import Snarkl.Compile import Snarkl.Constraint (ConstraintSystem (cs_in_vars), SimplifiedConstraintSystem (..), solve) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) @@ -59,7 +59,7 @@ data Result k = Result result_constraints :: Int, result_result :: k, result_r1cs :: R1CS k, - result_witness :: Assgn k + result_witness :: Witness k } deriving (Show) @@ -90,8 +90,8 @@ execute simpl mf inputs = let TExpPkg nv in_vars e = compileCompToTexp mf (r1cs, constraintSystem) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) [out_var] = r1cs_out_vars r1cs - wit = wit_of_cs inputs constraintSystem - out = case Map.lookup out_var wit of + wit@(Witness (Assgn m)) = wit_of_cs inputs constraintSystem + out = case Map.lookup out_var m of Nothing -> failWith $ ErrMsg @@ -120,20 +120,10 @@ execute simpl mf inputs = ng = num_constraints r1cs in Result result nw ng out r1cs wit --- --- data ConstraintSystem a = ConstraintSystem --- { cs_constraints :: ConstraintSet a, --- cs_num_vars :: Int, --- cs_in_vars :: [Var], --- cs_out_vars :: [Var] --- } --- deriving (Show, Eq) - -- | For a given R1CS and inputs, calculate a satisfying assignment. -wit_of_cs :: (GaloisField k) => [k] -> SimplifiedConstraintSystem k -> Assgn k +wit_of_cs :: (GaloisField k) => [k] -> SimplifiedConstraintSystem k -> Witness k wit_of_cs inputs (SimplifiedConstraintSystem cs) = let in_vars = cs_in_vars cs - f = gen_witness . Map.fromList in if length in_vars /= length inputs then failWith $ @@ -145,6 +135,6 @@ wit_of_cs inputs (SimplifiedConstraintSystem cs) = ++ show (length inputs) ++ " input(s)" ) - else f (zip in_vars inputs) - where - gen_witness = solve cs + else + let inputAssignments = Assgn . Map.fromList $ zip in_vars inputs + in Witness $ solve cs inputAssignments diff --git a/src/Snarkl/Utils.hs b/src/Snarkl/Utils.hs new file mode 100644 index 0000000..568fc27 --- /dev/null +++ b/src/Snarkl/Utils.hs @@ -0,0 +1,72 @@ +module Snarkl.Utils + ( writeFile, + writeJSONLines, + readJSONLines, + ) +where + +import qualified Data.Aeson as A +import Data.ByteString.Builder (Builder, lazyByteString) +import qualified Data.ByteString.Builder as LBS +import qualified Data.ByteString.Lazy as LBS +import Data.Data (Proxy) +import Snarkl.Errors (ErrMsg (ErrMsg), failWith) +import System.Directory (createDirectoryIfMissing) +import System.FilePath (takeDirectory) +import Prelude hiding (writeFile) + +writeFile :: + FilePath -> + LBS.ByteString -> + IO () +writeFile filePath contents = do + createDirectoryIfMissing True (takeDirectory filePath) + LBS.writeFile filePath contents + +writeJSONLines :: + (Foldable t) => + (Functor t) => + (A.ToJSON hdr) => + (A.ToJSON a) => + FilePath -> + Maybe hdr -> + t a -> + IO () +writeJSONLines filePath hdr items = + let contents = jsonlBuilder items + b = case hdr of + Nothing -> contents + Just h -> jsonLine h <> contents + in writeFile + filePath + (LBS.toLazyByteString $ unJSONLine b) + +readJSONLines :: + (A.FromJSON a, A.FromJSON hdr) => + FilePath -> + Maybe (Proxy hdr) -> + IO (Maybe hdr, [a]) +readJSONLines filePath (mHdrType :: Maybe (Proxy hdr)) = do + file <- LBS.readFile filePath + let ls = LBS.split 0x0a file + case ls of + [] -> failWith $ ErrMsg "Empty file" + (a : as) -> either (failWith . ErrMsg) pure $ case mHdrType of + Nothing -> do + items <- traverse A.eitherDecode (a : as) + pure (Nothing, items) + Just _ -> do + hdr <- Just <$> A.eitherDecode @hdr a + items <- traverse A.eitherDecode as + pure (hdr, items) + +newtype JSONLine = JSONLine {unJSONLine :: Builder} + +instance Semigroup JSONLine where + JSONLine a <> JSONLine b = JSONLine (a <> "\n" <> b) + +jsonLine :: (A.ToJSON a) => a -> JSONLine +jsonLine = JSONLine . lazyByteString . A.encode + +jsonlBuilder :: (Foldable t, Functor t, A.ToJSON a) => t a -> JSONLine +jsonlBuilder = foldl1 (<>) . fmap jsonLine From 1206f625b1c34a3a22f99aa2728b534876eba4df Mon Sep 17 00:00:00 2001 From: martyall Date: Tue, 16 Jan 2024 22:13:34 -0800 Subject: [PATCH 06/13] move json lines stuff to its own module --- snarkl.cabal | 9 +++- src/Data/JSONLines.hs | 64 +++++++++++++++++++++++++ src/Snarkl/Backend/R1CS.hs | 2 - src/Snarkl/Backend/R1CS/R1CS.hs | 60 +++++++++++++++++++++-- src/Snarkl/Backend/R1CS/Serialize.hs | 44 ----------------- src/Snarkl/CLI/Common.hs | 32 +++++++++++++ src/Snarkl/CLI/Compile.hs | 17 +++++-- src/Snarkl/CLI/GenWitness.hs | 33 ++++++++----- src/Snarkl/CLI/RunAll.hs | 24 ++++++---- src/Snarkl/Common.hs | 39 +++++++++++++++ src/Snarkl/Constraint/Constraints.hs | 40 ++++++++-------- src/Snarkl/Toplevel.hs | 11 +++-- src/Snarkl/Utils.hs | 72 ---------------------------- 13 files changed, 272 insertions(+), 175 deletions(-) create mode 100644 src/Data/JSONLines.hs delete mode 100644 src/Snarkl/Backend/R1CS/Serialize.hs create mode 100644 src/Snarkl/CLI/Common.hs delete mode 100644 src/Snarkl/Utils.hs diff --git a/snarkl.cabal b/snarkl.cabal index 796f049..c635151 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -32,10 +32,10 @@ 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.Common Snarkl.Compile @@ -58,25 +58,30 @@ library Snarkl.Toplevel other-modules: + Snarkl.CLI.Common Snarkl.CLI.Compile Snarkl.CLI.GenWitness Snarkl.CLI.RunAll - Snarkl.Utils default-extensions: BangPatterns DataKinds DeriveDataTypeable + DeriveGeneric FlexibleContexts FlexibleInstances + FunctionalDependencies GADTs GeneralizedNewtypeDeriving KindSignatures LambdaCase + MultiParamTypeClasses + NamedFieldPuns OverloadedStrings PatternSynonyms PolyKinds RankNTypes + RecordWildCards ScopedTypeVariables StandaloneDeriving TupleSections diff --git a/src/Data/JSONLines.hs b/src/Data/JSONLines.hs new file mode 100644 index 0000000..e0d0139 --- /dev/null +++ b/src/Data/JSONLines.hs @@ -0,0 +1,64 @@ +module Data.JSONLines + ( ToJSONLines (..), + FromJSONLines (..), + JSONLine (..), + NoHeader (..), + jsonlBuilder, + jsonLine, + ) +where + +import qualified Data.Aeson as A +import Data.ByteString.Builder (Builder, lazyByteString, toLazyByteString) +import qualified Data.ByteString.Lazy as LBS +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 NoHeader = NoHeader + +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 hdr item where + toJSONLines :: (Foldable t) => hdr -> t item -> LBS.ByteString + +instance (A.ToJSON item) => ToJSONLines NoHeader item where + toJSONLines _ = toBS . jsonlBuilder + +instance {-# OVERLAPPABLE #-} (A.ToJSON hdr, A.ToJSON item) => ToJSONLines hdr item where + toJSONLines hdr items = toBS $ jsonLine hdr <> jsonlBuilder items + +class FromJSONLines hdr item where + fromJSONLines :: [LazyByteString] -> Either String (hdr, [item]) + +instance (A.FromJSON item) => FromJSONLines NoHeader item where + fromJSONLines items = (NoHeader,) <$> traverse A.eitherDecode items + +instance {-# OVERLAPPABLE #-} (A.FromJSON hdr, A.FromJSON item) => FromJSONLines hdr item where + fromJSONLines (hdr : items) = do + hdr' <- A.eitherDecode hdr + items' <- traverse A.eitherDecode items + pure (hdr', items') + fromJSONLines [] = Left "Empty file" diff --git a/src/Snarkl/Backend/R1CS.hs b/src/Snarkl/Backend/R1CS.hs index 50f12df..b1e4351 100644 --- a/src/Snarkl/Backend/R1CS.hs +++ b/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 diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index fd5cee9..7c39dda 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -1,7 +1,10 @@ module Snarkl.Backend.R1CS.R1CS ( R1C (..), R1CS (..), + r1csHeader, Witness (..), + witnessHeader, + WitnessHeader (..), sat_r1cs, num_constraints, ) @@ -9,11 +12,10 @@ where import Control.Parallel.Strategies import qualified Data.Aeson as A -import Data.Field.Galois (GaloisField, PrimeField) +import Data.Field.Galois (GaloisField (char, deg), PrimeField) import qualified Data.Map as Map import Snarkl.Backend.R1CS.Poly import Snarkl.Common --- import Snarkl.Errors import Text.PrettyPrint.Leijen.Text (Pretty (..), (<+>)) ---------------------------------------------------------------- @@ -52,7 +54,57 @@ data R1CS a = R1CS } deriving (Show) -newtype Witness k = Witness {unWitness :: Assgn k} deriving (Show, Foldable, Functor) +r1csHeader :: (GaloisField a) => R1CS a -> ConstraintHeader +r1csHeader (cs :: R1CS a) = + ConstraintHeader + { field_characteristic = toInteger $ char (undefined :: a), + extension_degree = toInteger $ deg (undefined :: a), + n_constraints = length (r1cs_clauses cs), + n_variables = r1cs_num_vars cs, + input_variables = r1cs_in_vars cs, + output_variables = r1cs_out_vars cs + } + +data Witness k = Witness + { witness_assgn :: Assgn k, + witness_in_vars :: [Var], + witness_out_vars :: [Var], + witness_num_vars :: Int + } + deriving (Show) + +instance Functor Witness where + fmap f w = w {witness_assgn = fmap f (witness_assgn w)} + +data WitnessHeader = WitnessHeader + { in_vars :: [Var], + out_vars :: [Var], + num_vars :: Int + } + +instance A.ToJSON WitnessHeader where + toJSON (WitnessHeader in_vars out_vars num_vars) = + A.object + [ "in_vars" A..= in_vars, + "out_vars" A..= out_vars, + "num_vars" A..= num_vars + ] + +instance A.FromJSON WitnessHeader where + parseJSON = + A.withObject "WitnessHeader" $ \v -> do + in_vars <- v A..: "in_vars" + out_vars <- v A..: "out_vars" + num_vars <- v A..: "num_vars" + pure $ WitnessHeader in_vars out_vars num_vars + +witnessHeader :: Witness k -> WitnessHeader +witnessHeader (Witness {..}) = + WitnessHeader + { in_vars = witness_in_vars, + out_vars = witness_out_vars, + num_vars = witness_num_vars + } num_constraints :: R1CS a -> Int num_constraints = length . r1cs_clauses @@ -64,7 +116,7 @@ sat_r1c w c inner aV w * inner bV w == inner cV w where inner :: (GaloisField a) => Poly a -> Witness a -> a - inner (Poly (Assgn v)) (Witness (Assgn wit)) = + inner (Poly (Assgn v)) (Witness {witness_assgn = Assgn wit}) = let c0 = Map.findWithDefault 0 (Var (-1)) v in Map.foldlWithKey (f wit) c0 v diff --git a/src/Snarkl/Backend/R1CS/Serialize.hs b/src/Snarkl/Backend/R1CS/Serialize.hs deleted file mode 100644 index e3b6adc..0000000 --- a/src/Snarkl/Backend/R1CS/Serialize.hs +++ /dev/null @@ -1,44 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE RecordWildCards #-} - -module Snarkl.Backend.R1CS.Serialize where - -import qualified Data.Aeson as A -import Data.Field.Galois (GaloisField (char, deg)) -import GHC.Generics (Generic) -import Snarkl.Backend.R1CS.R1CS (R1CS (..), num_constraints) -import Snarkl.Common (Var) - -data ConstraintHeader k = ConstraintHeader - { field_characteristic :: Integer, - extension_degree :: Integer, - n_constraints :: Int, - n_variables :: Int, - input_variables :: [Var], - output_variables :: [Var] - } - deriving (Generic) - -instance A.ToJSON (ConstraintHeader k) - -instance A.FromJSON (ConstraintHeader k) - -r1csToHeader :: (GaloisField k) => R1CS k -> ConstraintHeader k -r1csToHeader x@(R1CS {..} :: R1CS k) = - ConstraintHeader - { field_characteristic = toInteger $ char (undefined :: k), - extension_degree = toInteger $ deg (undefined :: k), - n_constraints = num_constraints x, - n_variables = r1cs_num_vars + length r1cs_out_vars, - input_variables = r1cs_in_vars, - output_variables = r1cs_out_vars - } - -mkR1CSFilePath :: FilePath -> String -> FilePath -mkR1CSFilePath rootDir name = rootDir <> "/" <> name <> "-r1cs.jsonl" - -mkWitnessFilePath :: FilePath -> String -> FilePath -mkWitnessFilePath rootDir name = rootDir <> "/" <> name <> "-witness.jsonl" - -mkInputsFilePath :: FilePath -> String -> FilePath -mkInputsFilePath rootDir name = rootDir <> "/" <> name <> "-inputs.jsonl" diff --git a/src/Snarkl/CLI/Common.hs b/src/Snarkl/CLI/Common.hs new file mode 100644 index 0000000..aa0a497 --- /dev/null +++ b/src/Snarkl/CLI/Common.hs @@ -0,0 +1,32 @@ +module Snarkl.CLI.Common where + +import qualified Data.ByteString.Lazy as LBS +import System.Directory (createDirectoryIfMissing) +import System.FilePath (takeDirectory) + +writeFileWithDir :: + FilePath -> + LBS.ByteString -> + IO () +writeFileWithDir filePath contents = do + createDirectoryIfMissing True (takeDirectory filePath) + LBS.writeFile filePath contents + +readLines :: + FilePath -> + IO [LBS.ByteString] +readLines filePath = do + contents <- LBS.readFile filePath + return $ LBS.split 0xa contents + +mkR1CSFilePath :: FilePath -> String -> FilePath +mkR1CSFilePath rootDir name = rootDir <> "/" <> name <> "-r1cs.jsonl" + +mkWitnessFilePath :: FilePath -> String -> FilePath +mkWitnessFilePath rootDir name = rootDir <> "/" <> name <> "-witness.jsonl" + +mkInputsFilePath :: FilePath -> String -> FilePath +mkInputsFilePath rootDir name = rootDir <> "/" <> name <> "-inputs.jsonl" + +mkConstraintsFilePath :: FilePath -> String -> FilePath +mkConstraintsFilePath rootDir name = rootDir <> "/" <> name <> "-constraints.jsonl" diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index 2d32234..e98b45e 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -14,18 +14,19 @@ import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) +import Data.JSONLines (ToJSONLines (toJSONLines)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, showDefault, strOption, subparser, switch, value, (<**>)) import Snarkl.Backend.R1CS +import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, writeFileWithDir) import Snarkl.Compile -import Snarkl.Constraint (ConstraintSystem (cs_constraints, cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath) +import Snarkl.Constraint (ConstraintSystem (cs_constraints, cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemHeader) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language import Snarkl.Toplevel (comp_interp, wit_of_cs) -import qualified Snarkl.Utils as Utils data OptimizeOpts = OptimizeOpts { simplify :: Bool, @@ -83,9 +84,15 @@ compile CompileOpts {..} name comp = do ] TExpPkg nv in_vars e = compileCompToTexp comp (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) - r1csFP = mkR1CSFilePath r1csOutput name - Utils.writeJSONLines r1csFP (Just $ r1csToHeader r1cs) (r1cs_clauses r1cs) + let r1csFP = mkR1CSFilePath r1csOutput name + writeFileWithDir r1csFP $ + toJSONLines + (r1csHeader r1cs) + (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let csFP = mkConstraintsFilePath constraintsOutput name - Utils.writeJSONLines csFP (Just $ constraintSystemToHeader cs) (toList $ cs_constraints $ unSimplifiedConstraintSystem cs) + writeFileWithDir csFP $ + toJSONLines + (constraintSystemHeader cs) + (cs_constraints $ unSimplifiedConstraintSystem cs) putStrLn $ "Wrote constraints to " <> csFP diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index 871e297..d7aa672 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -14,20 +14,19 @@ import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) +import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (NoHeader), ToJSONLines (toJSONLines)) import qualified Data.Map as Map import qualified Data.Set as Set import qualified Data.String.Conversions as CS -import Data.Typeable (Proxy (Proxy), Typeable) -import Data.Void (Void) +import Data.Typeable (Typeable) import Options.Applicative (Parser, eitherReader, help, long, option, showDefault, strOption, value) import Snarkl.Backend.R1CS -import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem, unFieldElem)) -import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (SimplifiedConstraintSystem, unSimplifiedConstraintSystem), constraintSystemToHeader, mkConstraintsFilePath) +import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, mkWitnessFilePath, readLines, writeFileWithDir) +import Snarkl.Common (Assgn (Assgn), ConstraintHeader (..), FieldElem (..)) +import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (SimplifiedConstraintSystem, unSimplifiedConstraintSystem)) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language import Snarkl.Toplevel (comp_interp, wit_of_cs) -import qualified Snarkl.Utils as LBS -import qualified Snarkl.Utils as Utils import Text.Read (readEither) data InputOpts @@ -90,7 +89,8 @@ genWitness GenWitnessOpts {..} name comp = do -- parse the constraints file constraints <- do let csFP = mkConstraintsFilePath constraintsInput name - (Just ConstraintHeader {..}, cs) <- LBS.readJSONLines csFP (Just $ Proxy @(ConstraintHeader k)) + eConstraints <- fromJSONLines <$> readLines csFP + (ConstraintHeader {..}, cs) <- either (failWith . ErrMsg) pure eConstraints pure $ SimplifiedConstraintSystem $ ConstraintSystem @@ -103,9 +103,12 @@ genWitness GenWitnessOpts {..} name comp = do -- parse the inputs, either from cli or from file is <- case inputs of Explicit is -> pure $ map fromInteger is - FromFile fp -> map unFieldElem . snd <$> Utils.readJSONLines fp (Nothing :: Maybe (Proxy Void)) + FromFile fp -> do + eInput <- fromJSONLines <$> readLines fp + (NoHeader, input) <- either (failWith . ErrMsg) pure eInput + pure $ map unFieldElem input let out_interp = comp_interp comp is - witness@(Witness (Assgn m)) = wit_of_cs is constraints + witness@(Witness {witness_assgn = Assgn m}) = wit_of_cs is constraints out = case Map.lookup out_var m of Nothing -> failWith $ @@ -125,7 +128,9 @@ genWitness GenWitnessOpts {..} name comp = do ++ show out r1cs <- do let r1csFP = mkR1CSFilePath r1csInput name - (Just ConstraintHeader {..}, items) <- Utils.readJSONLines r1csFP (Just $ Proxy @(ConstraintHeader k)) + (Just ConstraintHeader {..}, items) <- do + eConstraints <- fromJSONLines <$> readLines r1csFP + either (failWith . ErrMsg) pure eConstraints pure $ R1CS { r1cs_clauses = items, @@ -133,13 +138,17 @@ genWitness GenWitnessOpts {..} name comp = do r1cs_in_vars = input_variables, r1cs_out_vars = output_variables } + let witnessAssgn = witness_assgn witness unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ "witness\n " - ++ CS.cs (A.encode $ toList (FieldElem <$> witness)) + ++ CS.cs (A.encode $ toList (FieldElem <$> witnessAssgn)) ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name - Utils.writeJSONLines witnessFP (Just $ constraintSystemToHeader constraints) (FieldElem <$> witness) + writeFileWithDir witnessFP $ + toJSONLines + (witnessHeader witness) + (FieldElem <$> witnessAssgn) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index eb9f000..0dafd88 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -5,15 +5,14 @@ module Snarkl.CLI.RunAll where import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.Foldable (Foldable (toList)) +import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (NoHeader), ToJSONLines (toJSONLines)) import qualified Data.Map as Map import Data.Maybe (catMaybes) -import Data.Proxy (Proxy) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) -import Data.Void (Void) import Options.Applicative (Parser, help, long, showDefault, strOption, value) -import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), Witness (Witness), mkR1CSFilePath, mkWitnessFilePath, r1csToHeader, sat_r1cs) +import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), Witness (Witness, witness_assgn), r1csHeader, sat_r1cs) +import Snarkl.CLI.Common (mkR1CSFilePath, mkWitnessFilePath, readLines, writeFileWithDir) import Snarkl.CLI.Compile (OptimizeOpts (removeUnreachable, simplify), optimizeOptsParser) import Snarkl.CLI.GenWitness (InputOpts (Explicit, FromFile), inputOptsParser) import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem, unFieldElem)) @@ -21,7 +20,6 @@ import Snarkl.Compile (SimplParam (RemoveUnreachable, Simplify), TExpPkg (TExpPk import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language (Comp) import Snarkl.Toplevel (comp_interp, wit_of_cs) -import qualified Snarkl.Utils as Utils data RunAllOpts = RunAllOpts { r1csOutput :: FilePath, @@ -68,9 +66,12 @@ runAll RunAllOpts {..} name comp = do -- parse the inputs, either from cli or from file is <- case inputs of Explicit is -> pure $ map fromInteger is - FromFile fp -> map unFieldElem . snd <$> Utils.readJSONLines fp (Nothing :: Maybe (Proxy Void)) + FromFile fp -> do + eInput <- fromJSONLines @NoHeader @(FieldElem k) <$> readLines fp + (NoHeader, input) <- either (failWith . ErrMsg) pure eInput + pure $ map unFieldElem input let out_interp = comp_interp comp is - witness@(Witness (Assgn m)) = wit_of_cs is cs + witness@(Witness {witness_assgn = Assgn m}) = wit_of_cs is cs out = case Map.lookup out_var m of Nothing -> failWith $ @@ -88,16 +89,19 @@ runAll RunAllOpts {..} name comp = do ++ show out_interp ++ " differs from actual result " ++ show out + let witnessAssgn = witness_assgn witness unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ "witness\n " - ++ CS.cs (A.encode $ toList (FieldElem <$> witness)) + ++ CS.cs (A.encode witnessAssgn) ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let r1csFP = mkR1CSFilePath r1csOutput name - Utils.writeJSONLines r1csFP (Just $ r1csToHeader r1cs) (r1cs_clauses r1cs) + writeFileWithDir r1csFP $ + toJSONLines (r1csHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name - Utils.writeJSONLines witnessFP (Just $ r1csToHeader r1cs) (fmap FieldElem witness) + writeFileWithDir witnessFP $ + toJSONLines (r1csHeader r1cs) (fmap FieldElem witnessAssgn) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index 4e41464..d6cda82 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -100,3 +100,42 @@ isAssoc op = case op of XOr -> True Eq -> True BEq -> True + +data ConstraintHeader = ConstraintHeader + { field_characteristic :: Integer, + extension_degree :: Integer, + n_constraints :: Int, + n_variables :: Int, + input_variables :: [Var], + output_variables :: [Var] + } + +instance A.ToJSON ConstraintHeader where + toJSON (ConstraintHeader {..}) = + A.object + [ "field_characteristic" A..= field_characteristic, + "extension_degree" A..= extension_degree, + "n_constraints" A..= n_constraints, + "n_variables" A..= n_variables, + "input_variables" A..= input_variables, + "output_variables" A..= output_variables + ] + +instance A.FromJSON ConstraintHeader where + parseJSON = + A.withObject "ConstraintHeader" $ \v -> do + field_characteristic <- v A..: "field_characteristic" + extension_degree <- v A..: "extension_degree" + n_constraints <- v A..: "n_constraints" + n_variables <- v A..: "n_variables" + input_variables <- v A..: "input_variables" + output_variables <- v A..: "output_variables" + pure $ + ConstraintHeader + { field_characteristic, + extension_degree, + n_constraints, + n_variables, + input_variables, + output_variables + } diff --git a/src/Snarkl/Constraint/Constraints.hs b/src/Snarkl/Constraint/Constraints.hs index 5ae0588..6d40e71 100644 --- a/src/Snarkl/Constraint/Constraints.hs +++ b/src/Snarkl/Constraint/Constraints.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use camelCase" #-} @@ -10,11 +9,10 @@ module Snarkl.Constraint.Constraints ConstraintSet, ConstraintSystem (..), SimplifiedConstraintSystem (..), + constraintSystemHeader, r1cs_of_cs, renumber_constraints, constraint_vars, - mkConstraintsFilePath, - constraintSystemToHeader, ) where @@ -24,8 +22,8 @@ import Data.Bifunctor (Bifunctor (first, second)) import Data.Field.Galois (GaloisField (char, deg), Prime, PrimeField) import qualified Data.Map as Map import qualified Data.Set as Set -import Snarkl.Backend.R1CS (ConstraintHeader (..), Poly (Poly), R1C (R1C), R1CS (R1CS), const_poly, var_poly) -import Snarkl.Common (Assgn (Assgn), FieldElem (..), Var (Var)) +import Snarkl.Backend.R1CS (Poly (Poly), R1C (R1C), R1CS (R1CS), const_poly, var_poly) +import Snarkl.Common (Assgn (Assgn), ConstraintHeader (..), FieldElem (..), Var (Var)) import Snarkl.Constraint.SimplMonad (SEnv) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) @@ -222,6 +220,22 @@ newtype SimplifiedConstraintSystem a = SimplifiedConstraintSystem } deriving (Show, Eq) +constraintSystemHeader :: + (GaloisField a) => + SimplifiedConstraintSystem a -> + ConstraintHeader +constraintSystemHeader (SimplifiedConstraintSystem (ConstraintSystem {..}) :: SimplifiedConstraintSystem a) = + ConstraintHeader + { field_characteristic = toInteger $ char (undefined :: a), + extension_degree = toInteger $ deg (undefined :: a), + n_constraints = Set.size cs_constraints, + -- TODO: should we also add the number of output variables? We do this for + -- the R1CS header, but the examples i checked didn't seem to work + n_variables = cs_num_vars, + input_variables = cs_in_vars, + output_variables = cs_out_vars + } + r1cs_of_cs :: (GaloisField a) => -- | Constraints @@ -305,19 +319,3 @@ renumber_constraints cs = CMult (c, renum_f x) (d, renum_f y) (e, fmap renum_f mz) CMagic nm xs f -> CMagic nm (map renum_f xs) f - -constraintSystemToHeader :: (GaloisField k) => SimplifiedConstraintSystem k -> ConstraintHeader k -constraintSystemToHeader (SimplifiedConstraintSystem (ConstraintSystem {..} :: ConstraintSystem k)) = - ConstraintHeader - { field_characteristic = toInteger $ char (undefined :: k), - extension_degree = toInteger $ deg (undefined :: k), - n_constraints = Set.size cs_constraints, - -- TODO: should we also add the number of output variables? We do this for - -- the R1CS header, but the examples i checked didn't seem to work - n_variables = cs_num_vars, - input_variables = cs_in_vars, - output_variables = cs_out_vars - } - -mkConstraintsFilePath :: FilePath -> String -> FilePath -mkConstraintsFilePath rootDir name = rootDir <> "/" <> name <> "-constraints.jsonl" diff --git a/src/Snarkl/Toplevel.hs b/src/Snarkl/Toplevel.hs index 063c768..da60693 100644 --- a/src/Snarkl/Toplevel.hs +++ b/src/Snarkl/Toplevel.hs @@ -25,7 +25,7 @@ import Data.Typeable (Typeable) import Snarkl.Backend.R1CS import Snarkl.Common (Assgn (Assgn)) import Snarkl.Compile -import Snarkl.Constraint (ConstraintSystem (cs_in_vars), SimplifiedConstraintSystem (..), solve) +import Snarkl.Constraint (ConstraintSystem (cs_in_vars, cs_num_vars, cs_out_vars), SimplifiedConstraintSystem (..), solve) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Interp (interp) import Snarkl.Language @@ -90,7 +90,7 @@ execute simpl mf inputs = let TExpPkg nv in_vars e = compileCompToTexp mf (r1cs, constraintSystem) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) [out_var] = r1cs_out_vars r1cs - wit@(Witness (Assgn m)) = wit_of_cs inputs constraintSystem + wit@(Witness {witness_assgn = Assgn m}) = wit_of_cs inputs constraintSystem out = case Map.lookup out_var m of Nothing -> failWith $ @@ -137,4 +137,9 @@ wit_of_cs inputs (SimplifiedConstraintSystem cs) = ) else let inputAssignments = Assgn . Map.fromList $ zip in_vars inputs - in Witness $ solve cs inputAssignments + in Witness + { witness_assgn = solve cs inputAssignments, + witness_in_vars = in_vars, + witness_out_vars = cs_out_vars cs, + witness_num_vars = cs_num_vars cs + } diff --git a/src/Snarkl/Utils.hs b/src/Snarkl/Utils.hs deleted file mode 100644 index 568fc27..0000000 --- a/src/Snarkl/Utils.hs +++ /dev/null @@ -1,72 +0,0 @@ -module Snarkl.Utils - ( writeFile, - writeJSONLines, - readJSONLines, - ) -where - -import qualified Data.Aeson as A -import Data.ByteString.Builder (Builder, lazyByteString) -import qualified Data.ByteString.Builder as LBS -import qualified Data.ByteString.Lazy as LBS -import Data.Data (Proxy) -import Snarkl.Errors (ErrMsg (ErrMsg), failWith) -import System.Directory (createDirectoryIfMissing) -import System.FilePath (takeDirectory) -import Prelude hiding (writeFile) - -writeFile :: - FilePath -> - LBS.ByteString -> - IO () -writeFile filePath contents = do - createDirectoryIfMissing True (takeDirectory filePath) - LBS.writeFile filePath contents - -writeJSONLines :: - (Foldable t) => - (Functor t) => - (A.ToJSON hdr) => - (A.ToJSON a) => - FilePath -> - Maybe hdr -> - t a -> - IO () -writeJSONLines filePath hdr items = - let contents = jsonlBuilder items - b = case hdr of - Nothing -> contents - Just h -> jsonLine h <> contents - in writeFile - filePath - (LBS.toLazyByteString $ unJSONLine b) - -readJSONLines :: - (A.FromJSON a, A.FromJSON hdr) => - FilePath -> - Maybe (Proxy hdr) -> - IO (Maybe hdr, [a]) -readJSONLines filePath (mHdrType :: Maybe (Proxy hdr)) = do - file <- LBS.readFile filePath - let ls = LBS.split 0x0a file - case ls of - [] -> failWith $ ErrMsg "Empty file" - (a : as) -> either (failWith . ErrMsg) pure $ case mHdrType of - Nothing -> do - items <- traverse A.eitherDecode (a : as) - pure (Nothing, items) - Just _ -> do - hdr <- Just <$> A.eitherDecode @hdr a - items <- traverse A.eitherDecode as - pure (hdr, items) - -newtype JSONLine = JSONLine {unJSONLine :: Builder} - -instance Semigroup JSONLine where - JSONLine a <> JSONLine b = JSONLine (a <> "\n" <> b) - -jsonLine :: (A.ToJSON a) => a -> JSONLine -jsonLine = JSONLine . lazyByteString . A.encode - -jsonlBuilder :: (Foldable t, Functor t, A.ToJSON a) => t a -> JSONLine -jsonlBuilder = foldl1 (<>) . fmap jsonLine From ffda3dec133594acd0c7fc3ea8b5e4e84291c6f5 Mon Sep 17 00:00:00 2001 From: martyall Date: Tue, 16 Jan 2024 22:55:44 -0800 Subject: [PATCH 07/13] fix var number problem --- src/Data/JSONLines.hs | 8 ++++---- src/Snarkl/CLI/GenWitness.hs | 11 +++++------ src/Snarkl/CLI/RunAll.hs | 4 ++-- src/Snarkl/Common.hs | 2 +- src/Snarkl/Constraint/Constraints.hs | 2 -- 5 files changed, 12 insertions(+), 15 deletions(-) diff --git a/src/Data/JSONLines.hs b/src/Data/JSONLines.hs index e0d0139..d159a0a 100644 --- a/src/Data/JSONLines.hs +++ b/src/Data/JSONLines.hs @@ -44,19 +44,19 @@ toBS (JSONLine a) = toLazyByteString a class ToJSONLines hdr item where toJSONLines :: (Foldable t) => hdr -> t item -> LBS.ByteString -instance (A.ToJSON item) => ToJSONLines NoHeader item where +instance {-# OVERLAPPING #-} (A.ToJSON item) => ToJSONLines NoHeader item where toJSONLines _ = toBS . jsonlBuilder -instance {-# OVERLAPPABLE #-} (A.ToJSON hdr, A.ToJSON item) => ToJSONLines hdr item where +instance (A.ToJSON hdr, A.ToJSON item) => ToJSONLines hdr item where toJSONLines hdr items = toBS $ jsonLine hdr <> jsonlBuilder items class FromJSONLines hdr item where fromJSONLines :: [LazyByteString] -> Either String (hdr, [item]) -instance (A.FromJSON item) => FromJSONLines NoHeader item where +instance {-# OVERLAPS #-} (A.FromJSON item) => FromJSONLines NoHeader item where fromJSONLines items = (NoHeader,) <$> traverse A.eitherDecode items -instance {-# OVERLAPPABLE #-} (A.FromJSON hdr, A.FromJSON item) => FromJSONLines hdr item where +instance (A.FromJSON hdr, A.FromJSON item) => FromJSONLines hdr item where fromJSONLines (hdr : items) = do hdr' <- A.eitherDecode hdr items' <- traverse A.eitherDecode items diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index d7aa672..b5ce753 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -13,7 +13,6 @@ import Control.Applicative ((<|>)) import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.Foldable (Foldable (toList)) import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (NoHeader), ToJSONLines (toJSONLines)) import qualified Data.Map as Map import qualified Data.Set as Set @@ -25,7 +24,7 @@ import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, mkWitnessFilePa import Snarkl.Common (Assgn (Assgn), ConstraintHeader (..), FieldElem (..)) import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (SimplifiedConstraintSystem, unSimplifiedConstraintSystem)) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) -import Snarkl.Language +import Snarkl.Language (Comp) import Snarkl.Toplevel (comp_interp, wit_of_cs) import Text.Read (readEither) @@ -104,7 +103,7 @@ genWitness GenWitnessOpts {..} name comp = do is <- case inputs of Explicit is -> pure $ map fromInteger is FromFile fp -> do - eInput <- fromJSONLines <$> readLines fp + eInput <- fromJSONLines @NoHeader @(FieldElem k) <$> readLines fp (NoHeader, input) <- either (failWith . ErrMsg) pure eInput pure $ map unFieldElem input let out_interp = comp_interp comp is @@ -138,17 +137,17 @@ genWitness GenWitnessOpts {..} name comp = do r1cs_in_vars = input_variables, r1cs_out_vars = output_variables } - let witnessAssgn = witness_assgn witness + let witnessAssgn@(Assgn assgn) = witness_assgn witness unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ "witness\n " - ++ CS.cs (A.encode $ toList (FieldElem <$> witnessAssgn)) + ++ CS.cs (A.encode witnessAssgn) ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name writeFileWithDir witnessFP $ toJSONLines (witnessHeader witness) - (FieldElem <$> witnessAssgn) + (Map.toList (FieldElem <$> assgn)) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index 0dafd88..0a6c32b 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -89,7 +89,7 @@ runAll RunAllOpts {..} name comp = do ++ show out_interp ++ " differs from actual result " ++ show out - let witnessAssgn = witness_assgn witness + let witnessAssgn@(Assgn assgn) = witness_assgn witness unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ @@ -103,5 +103,5 @@ runAll RunAllOpts {..} name comp = do putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name writeFileWithDir witnessFP $ - toJSONLines (r1csHeader r1cs) (fmap FieldElem witnessAssgn) + toJSONLines (r1csHeader r1cs) (Map.toList $ fmap FieldElem assgn) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index d6cda82..92bde87 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -24,7 +24,7 @@ instance Pretty Var where incVar :: Var -> Var incVar (Var i) = Var (i + 1) -newtype Assgn a = Assgn (Map.Map Var a) deriving (Show, Eq, Functor, Foldable) +newtype Assgn a = Assgn (Map.Map Var a) deriving (Show, Eq, Functor) newtype FieldElem k = FieldElem {unFieldElem :: k} deriving (Show, Eq) diff --git a/src/Snarkl/Constraint/Constraints.hs b/src/Snarkl/Constraint/Constraints.hs index 6d40e71..779f94b 100644 --- a/src/Snarkl/Constraint/Constraints.hs +++ b/src/Snarkl/Constraint/Constraints.hs @@ -229,8 +229,6 @@ constraintSystemHeader (SimplifiedConstraintSystem (ConstraintSystem {..}) :: Si { field_characteristic = toInteger $ char (undefined :: a), extension_degree = toInteger $ deg (undefined :: a), n_constraints = Set.size cs_constraints, - -- TODO: should we also add the number of output variables? We do this for - -- the R1CS header, but the examples i checked didn't seem to work n_variables = cs_num_vars, input_variables = cs_in_vars, output_variables = cs_out_vars From bb99f06bc820587a0b3f17738b0a0ba89ba6ebf6 Mon Sep 17 00:00:00 2001 From: martyall Date: Tue, 16 Jan 2024 23:50:32 -0800 Subject: [PATCH 08/13] try to fix overlappables --- src/Data/JSONLines.hs | 6 +++--- src/Snarkl/Common.hs | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/JSONLines.hs b/src/Data/JSONLines.hs index d159a0a..0f8d298 100644 --- a/src/Data/JSONLines.hs +++ b/src/Data/JSONLines.hs @@ -47,16 +47,16 @@ class ToJSONLines hdr item where instance {-# OVERLAPPING #-} (A.ToJSON item) => ToJSONLines NoHeader item where toJSONLines _ = toBS . jsonlBuilder -instance (A.ToJSON hdr, A.ToJSON item) => ToJSONLines hdr item where +instance {-# OVERLAPPABLE #-} (A.ToJSON hdr, A.ToJSON item) => ToJSONLines hdr item where toJSONLines hdr items = toBS $ jsonLine hdr <> jsonlBuilder items class FromJSONLines hdr item where fromJSONLines :: [LazyByteString] -> Either String (hdr, [item]) -instance {-# OVERLAPS #-} (A.FromJSON item) => FromJSONLines NoHeader item where +instance {-# OVERLAPPING #-} (A.FromJSON item) => FromJSONLines NoHeader item where fromJSONLines items = (NoHeader,) <$> traverse A.eitherDecode items -instance (A.FromJSON hdr, A.FromJSON item) => FromJSONLines hdr item where +instance {-# OVERLAPPABLE #-} (A.FromJSON hdr, A.FromJSON item) => FromJSONLines hdr item where fromJSONLines (hdr : items) = do hdr' <- A.eitherDecode hdr items' <- traverse A.eitherDecode items diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index 92bde87..0b5ceb8 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -113,7 +113,7 @@ data ConstraintHeader = ConstraintHeader instance A.ToJSON ConstraintHeader where toJSON (ConstraintHeader {..}) = A.object - [ "field_characteristic" A..= field_characteristic, + [ "field_characteristic" A..= show field_characteristic, "extension_degree" A..= extension_degree, "n_constraints" A..= n_constraints, "n_variables" A..= n_variables, @@ -124,7 +124,7 @@ instance A.ToJSON ConstraintHeader where instance A.FromJSON ConstraintHeader where parseJSON = A.withObject "ConstraintHeader" $ \v -> do - field_characteristic <- v A..: "field_characteristic" + field_characteristic <- read <$> v A..: "field_characteristic" extension_degree <- v A..: "extension_degree" n_constraints <- v A..: "n_constraints" n_variables <- v A..: "n_variables" From 9711f0d607597fe24842efa688fa3e584a7bb9fe Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 17 Jan 2024 12:07:48 -0800 Subject: [PATCH 09/13] remove overlapping instances --- src/Data/JSONLines.hs | 39 ++++++++++++++++++--------------- src/Snarkl/Backend/R1CS/Poly.hs | 4 +--- src/Snarkl/Backend/R1CS/R1CS.hs | 8 +++---- src/Snarkl/CLI/Common.hs | 4 ++-- src/Snarkl/CLI/Compile.hs | 15 +++++-------- src/Snarkl/CLI/GenWitness.hs | 24 ++++++++++---------- src/Snarkl/CLI/RunAll.hs | 16 +++++++------- src/Snarkl/Common.hs | 5 +++++ 8 files changed, 57 insertions(+), 58 deletions(-) diff --git a/src/Data/JSONLines.hs b/src/Data/JSONLines.hs index 0f8d298..e20304f 100644 --- a/src/Data/JSONLines.hs +++ b/src/Data/JSONLines.hs @@ -2,12 +2,12 @@ module Data.JSONLines ( ToJSONLines (..), FromJSONLines (..), JSONLine (..), + WithHeader(..), NoHeader (..), - jsonlBuilder, - jsonLine, ) where +import Data.Kind (Type) import qualified Data.Aeson as A import Data.ByteString.Builder (Builder, lazyByteString, toLazyByteString) import qualified Data.ByteString.Lazy as LBS @@ -25,7 +25,10 @@ instance Semigroup JSONLine where instance Monoid JSONLine where mempty = EmptyLine -data NoHeader = NoHeader +data WithHeader :: Type -> Type -> Type where + WithHeader :: hdr -> [item] -> WithHeader hdr item + +data NoHeader item = NoHeader [item] jsonlBuilder :: (Foldable t) => @@ -41,24 +44,24 @@ toBS :: JSONLine -> LBS.ByteString toBS EmptyLine = mempty toBS (JSONLine a) = toLazyByteString a -class ToJSONLines hdr item where - toJSONLines :: (Foldable t) => hdr -> t item -> LBS.ByteString +class ToJSONLines a where + toJSONLines :: a -> LBS.ByteString -instance {-# OVERLAPPING #-} (A.ToJSON item) => ToJSONLines NoHeader item where - toJSONLines _ = toBS . jsonlBuilder +instance (A.ToJSON item) => ToJSONLines (NoHeader item) where + toJSONLines (NoHeader items) = toBS . jsonlBuilder $ items -instance {-# OVERLAPPABLE #-} (A.ToJSON hdr, A.ToJSON item) => ToJSONLines hdr item where - toJSONLines hdr items = toBS $ jsonLine hdr <> 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 hdr item where - fromJSONLines :: [LazyByteString] -> Either String (hdr, [item]) +class FromJSONLines a where + fromJSONLines :: [LazyByteString] -> Either String a -instance {-# OVERLAPPING #-} (A.FromJSON item) => FromJSONLines NoHeader item where - fromJSONLines items = (NoHeader,) <$> traverse A.eitherDecode items +instance (A.FromJSON item) => FromJSONLines (NoHeader item) where + fromJSONLines items = NoHeader <$> traverse A.eitherDecode items -instance {-# OVERLAPPABLE #-} (A.FromJSON hdr, A.FromJSON item) => FromJSONLines hdr item where - fromJSONLines (hdr : items) = do - hdr' <- A.eitherDecode hdr - items' <- traverse A.eitherDecode items - pure (hdr', 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" diff --git a/src/Snarkl/Backend/R1CS/Poly.hs b/src/Snarkl/Backend/R1CS/Poly.hs index 77d196a..a0f8f64 100644 --- a/src/Snarkl/Backend/R1CS/Poly.hs +++ b/src/Snarkl/Backend/R1CS/Poly.hs @@ -15,9 +15,7 @@ instance (PrimeField a) => A.ToJSON (Poly a) where toJSON (Poly m) = A.toJSON m instance (PrimeField a) => A.FromJSON (Poly a) where - parseJSON v = do - m <- A.parseJSON v - return (Poly m) + parseJSON v = Poly <$> A.parseJSON v instance (Pretty a) => Pretty (Poly a) where pretty (Poly (Assgn m)) = pretty $ Map.toList m diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index 7c39dda..ebf6ed7 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -59,7 +59,7 @@ r1csHeader (cs :: R1CS a) = ConstraintHeader { field_characteristic = toInteger $ char (undefined :: a), extension_degree = toInteger $ deg (undefined :: a), - n_constraints = length (r1cs_clauses cs), + n_constraints = num_constraints cs, n_variables = r1cs_num_vars cs, input_variables = r1cs_in_vars cs, output_variables = r1cs_out_vars cs @@ -127,9 +127,7 @@ sat_r1c w c sat_r1cs :: (GaloisField a) => Witness a -> R1CS a -> Bool sat_r1cs w cs = and $ is_sat (r1cs_clauses cs) where - is_sat cs0 = map g cs0 `using` parListChunk (chunk_sz cs0) rseq + is_sat cs0 = map (sat_r1c w ) cs0 `using` parListChunk (chunk_sz cs0) rseq num_chunks = 32 chunk_sz cs0 = - truncate $ (fromIntegral (length cs0) :: Rational) / num_chunks - g c = - sat_r1c w c + truncate $ (fromIntegral (length cs0) :: Rational) / num_chunks \ No newline at end of file diff --git a/src/Snarkl/CLI/Common.hs b/src/Snarkl/CLI/Common.hs index aa0a497..f6d448f 100644 --- a/src/Snarkl/CLI/Common.hs +++ b/src/Snarkl/CLI/Common.hs @@ -12,10 +12,10 @@ writeFileWithDir filePath contents = do createDirectoryIfMissing True (takeDirectory filePath) LBS.writeFile filePath contents -readLines :: +readFileLines :: FilePath -> IO [LBS.ByteString] -readLines filePath = do +readFileLines filePath = do contents <- LBS.readFile filePath return $ LBS.split 0xa contents diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index e98b45e..37b5e43 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -10,11 +10,12 @@ module Snarkl.CLI.Compile ) where +import qualified Data.Set as Set import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) -import Data.JSONLines (ToJSONLines (toJSONLines)) +import Data.JSONLines (ToJSONLines (toJSONLines), WithHeader(..)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS @@ -85,14 +86,10 @@ compile CompileOpts {..} name comp = do TExpPkg nv in_vars e = compileCompToTexp comp (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) let r1csFP = mkR1CSFilePath r1csOutput name - writeFileWithDir r1csFP $ - toJSONLines - (r1csHeader r1cs) - (r1cs_clauses r1cs) + writeFileWithDir r1csFP . toJSONLines $ + WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let csFP = mkConstraintsFilePath constraintsOutput name - writeFileWithDir csFP $ - toJSONLines - (constraintSystemHeader cs) - (cs_constraints $ unSimplifiedConstraintSystem cs) + writeFileWithDir csFP . toJSONLines $ + WithHeader (constraintSystemHeader cs) (Set.toList $ cs_constraints $ unSimplifiedConstraintSystem cs) putStrLn $ "Wrote constraints to " <> csFP diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index b5ce753..9c41046 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -13,14 +13,14 @@ import Control.Applicative ((<|>)) import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (NoHeader), ToJSONLines (toJSONLines)) +import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (..), WithHeader(..), ToJSONLines (toJSONLines)) import qualified Data.Map as Map import qualified Data.Set as Set import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (Parser, eitherReader, help, long, option, showDefault, strOption, value) import Snarkl.Backend.R1CS -import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, mkWitnessFilePath, readLines, writeFileWithDir) +import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, mkWitnessFilePath, readFileLines, writeFileWithDir) import Snarkl.Common (Assgn (Assgn), ConstraintHeader (..), FieldElem (..)) import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (SimplifiedConstraintSystem, unSimplifiedConstraintSystem)) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) @@ -58,7 +58,7 @@ genWitnessOptsParser = GenWitnessOpts <$> strOption ( long "constraints-input-dir" - <> help "the directory where the constrains.jsonl file is located" + <> help "the directory where the constraints.jsonl file is located" <> value "./snarkl-output" <> showDefault ) @@ -88,8 +88,8 @@ genWitness GenWitnessOpts {..} name comp = do -- parse the constraints file constraints <- do let csFP = mkConstraintsFilePath constraintsInput name - eConstraints <- fromJSONLines <$> readLines csFP - (ConstraintHeader {..}, cs) <- either (failWith . ErrMsg) pure eConstraints + eConstraints <- fromJSONLines <$> readFileLines csFP + (WithHeader ConstraintHeader {..} cs) <- either (failWith . ErrMsg) pure eConstraints pure $ SimplifiedConstraintSystem $ ConstraintSystem @@ -103,8 +103,8 @@ genWitness GenWitnessOpts {..} name comp = do is <- case inputs of Explicit is -> pure $ map fromInteger is FromFile fp -> do - eInput <- fromJSONLines @NoHeader @(FieldElem k) <$> readLines fp - (NoHeader, input) <- either (failWith . ErrMsg) pure eInput + eInput <- fromJSONLines <$> readFileLines fp + NoHeader input <- either (failWith . ErrMsg) pure eInput pure $ map unFieldElem input let out_interp = comp_interp comp is witness@(Witness {witness_assgn = Assgn m}) = wit_of_cs is constraints @@ -127,8 +127,8 @@ genWitness GenWitnessOpts {..} name comp = do ++ show out r1cs <- do let r1csFP = mkR1CSFilePath r1csInput name - (Just ConstraintHeader {..}, items) <- do - eConstraints <- fromJSONLines <$> readLines r1csFP + (WithHeader ConstraintHeader {..} items) <- do + eConstraints <- fromJSONLines <$> readFileLines r1csFP either (failWith . ErrMsg) pure eConstraints pure $ R1CS @@ -146,8 +146,6 @@ genWitness GenWitnessOpts {..} name comp = do ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name - writeFileWithDir witnessFP $ - toJSONLines - (witnessHeader witness) - (Map.toList (FieldElem <$> assgn)) + writeFileWithDir witnessFP . toJSONLines $ + WithHeader (witnessHeader witness) (Map.toList (FieldElem <$> assgn)) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index 0a6c32b..3955e3a 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -5,14 +5,14 @@ module Snarkl.CLI.RunAll where import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (NoHeader), ToJSONLines (toJSONLines)) +import Data.JSONLines (FromJSONLines (..), NoHeader (..), WithHeader(..), ToJSONLines (..)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (Parser, help, long, showDefault, strOption, value) import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), Witness (Witness, witness_assgn), r1csHeader, sat_r1cs) -import Snarkl.CLI.Common (mkR1CSFilePath, mkWitnessFilePath, readLines, writeFileWithDir) +import Snarkl.CLI.Common (mkR1CSFilePath, mkWitnessFilePath, readFileLines, writeFileWithDir) import Snarkl.CLI.Compile (OptimizeOpts (removeUnreachable, simplify), optimizeOptsParser) import Snarkl.CLI.GenWitness (InputOpts (Explicit, FromFile), inputOptsParser) import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem, unFieldElem)) @@ -67,8 +67,8 @@ runAll RunAllOpts {..} name comp = do is <- case inputs of Explicit is -> pure $ map fromInteger is FromFile fp -> do - eInput <- fromJSONLines @NoHeader @(FieldElem k) <$> readLines fp - (NoHeader, input) <- either (failWith . ErrMsg) pure eInput + eInput <- fromJSONLines <$> readFileLines fp + NoHeader input <- either (failWith . ErrMsg) pure eInput pure $ map unFieldElem input let out_interp = comp_interp comp is witness@(Witness {witness_assgn = Assgn m}) = wit_of_cs is cs @@ -98,10 +98,10 @@ runAll RunAllOpts {..} name comp = do ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let r1csFP = mkR1CSFilePath r1csOutput name - writeFileWithDir r1csFP $ - toJSONLines (r1csHeader r1cs) (r1cs_clauses r1cs) + writeFileWithDir r1csFP . toJSONLines $ + WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name - writeFileWithDir witnessFP $ - toJSONLines (r1csHeader r1cs) (Map.toList $ fmap FieldElem assgn) + writeFileWithDir witnessFP . toJSONLines $ + WithHeader (r1csHeader r1cs) (Map.toList $ fmap FieldElem assgn) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index 0b5ceb8..378d5fc 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -10,6 +10,9 @@ import Text.PrettyPrint.Leijen.Text (Pretty (pretty)) newtype Var = Var Int deriving (Eq, Ord, Show) +-- Internally variables start at index 0 and the constant "variable" with +-- value 1 is at index -1. This works well internall but poorly for downstream +-- dependencies, so when serializing/deserializing we adjust. instance A.ToJSON Var where toJSON (Var i) = A.toJSON (i + 1) @@ -26,6 +29,8 @@ incVar (Var i) = Var (i + 1) newtype Assgn a = Assgn (Map.Map Var a) deriving (Show, Eq, Functor) +-- We use this wrapper to get a stringified representation of big integers. +-- This plays better with downstream dependencies, e.g. javascript. newtype FieldElem k = FieldElem {unFieldElem :: k} deriving (Show, Eq) instance (PrimeField k) => A.ToJSON (FieldElem k) where From e5121494eaa37867b3983da68d9373765915a628 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 17 Jan 2024 12:18:48 -0800 Subject: [PATCH 10/13] unify cli prompts --- src/Data/JSONLines.hs | 8 ++++---- src/Snarkl/Backend/R1CS/R1CS.hs | 4 ++-- src/Snarkl/CLI/Compile.hs | 12 ++++++------ src/Snarkl/CLI/GenWitness.hs | 8 ++++---- src/Snarkl/CLI/RunAll.hs | 10 +++++----- src/Snarkl/Compile.hs | 4 ++-- 6 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/Data/JSONLines.hs b/src/Data/JSONLines.hs index e20304f..d9628ab 100644 --- a/src/Data/JSONLines.hs +++ b/src/Data/JSONLines.hs @@ -2,15 +2,15 @@ module Data.JSONLines ( ToJSONLines (..), FromJSONLines (..), JSONLine (..), - WithHeader(..), + WithHeader (..), NoHeader (..), ) where -import Data.Kind (Type) 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 @@ -25,8 +25,8 @@ instance Semigroup JSONLine where instance Monoid JSONLine where mempty = EmptyLine -data WithHeader :: Type -> Type -> Type where - WithHeader :: hdr -> [item] -> WithHeader hdr item +data WithHeader :: Type -> Type -> Type where + WithHeader :: hdr -> [item] -> WithHeader hdr item data NoHeader item = NoHeader [item] diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index ebf6ed7..99b046c 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -127,7 +127,7 @@ sat_r1c w c sat_r1cs :: (GaloisField a) => Witness a -> R1CS a -> Bool sat_r1cs w cs = and $ is_sat (r1cs_clauses cs) where - is_sat cs0 = map (sat_r1c w ) cs0 `using` parListChunk (chunk_sz cs0) rseq + is_sat cs0 = map (sat_r1c w) cs0 `using` parListChunk (chunk_sz cs0) rseq num_chunks = 32 chunk_sz cs0 = - truncate $ (fromIntegral (length cs0) :: Rational) / num_chunks \ No newline at end of file + truncate $ (fromIntegral (length cs0) :: Rational) / num_chunks diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index 37b5e43..2081c57 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -10,14 +10,14 @@ module Snarkl.CLI.Compile ) where -import qualified Data.Set as Set import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) import Data.Foldable (Foldable (toList)) -import Data.JSONLines (ToJSONLines (toJSONLines), WithHeader(..)) +import Data.JSONLines (ToJSONLines (toJSONLines), WithHeader (..)) import qualified Data.Map as Map import Data.Maybe (catMaybes) +import qualified Data.Set as Set import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, showDefault, strOption, subparser, switch, value, (<**>)) @@ -58,13 +58,13 @@ compileOptsParser = <$> optimizeOptsParser <*> strOption ( long "r1cs-output-dir" - <> help "the directory to write the r1cs artifact" + <> help "the directory to write the r1cs.jsonl artifact" <> value "./snarkl-output" <> showDefault ) <*> strOption ( long "constraints-output-dir" - <> help "the directory to write the constraints artifact" + <> help "the directory to write the constraints.jsonl artifact" <> value "./snarkl-output" <> showDefault ) @@ -86,10 +86,10 @@ compile CompileOpts {..} name comp = do TExpPkg nv in_vars e = compileCompToTexp comp (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) let r1csFP = mkR1CSFilePath r1csOutput name - writeFileWithDir r1csFP . toJSONLines $ + writeFileWithDir r1csFP . toJSONLines $ WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let csFP = mkConstraintsFilePath constraintsOutput name - writeFileWithDir csFP . toJSONLines $ + writeFileWithDir csFP . toJSONLines $ WithHeader (constraintSystemHeader cs) (Set.toList $ cs_constraints $ unSimplifiedConstraintSystem cs) putStrLn $ "Wrote constraints to " <> csFP diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index 9c41046..2f9f25e 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -13,7 +13,7 @@ import Control.Applicative ((<|>)) import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (..), WithHeader(..), ToJSONLines (toJSONLines)) +import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (..), ToJSONLines (toJSONLines), WithHeader (..)) import qualified Data.Map as Map import qualified Data.Set as Set import qualified Data.String.Conversions as CS @@ -43,7 +43,7 @@ inputOptsParser = <|> FromFile <$> strOption ( long "inputs-dir" - <> help "The directory where the inputs.jsonl file is located" + <> help "The directory where the inputs.jsonl artifact is located" ) data GenWitnessOpts = GenWitnessOpts @@ -58,7 +58,7 @@ genWitnessOptsParser = GenWitnessOpts <$> strOption ( long "constraints-input-dir" - <> help "the directory where the constraints.jsonl file is located" + <> help "the directory where the constraints.jsonl artifact is located" <> value "./snarkl-output" <> showDefault ) @@ -146,6 +146,6 @@ genWitness GenWitnessOpts {..} name comp = do ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name - writeFileWithDir witnessFP . toJSONLines $ + writeFileWithDir witnessFP . toJSONLines $ WithHeader (witnessHeader witness) (Map.toList (FieldElem <$> assgn)) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index 3955e3a..a5ceb6a 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -5,7 +5,7 @@ module Snarkl.CLI.RunAll where import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.JSONLines (FromJSONLines (..), NoHeader (..), WithHeader(..), ToJSONLines (..)) +import Data.JSONLines (FromJSONLines (..), NoHeader (..), ToJSONLines (..), WithHeader (..)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS @@ -33,7 +33,7 @@ runAllOptsParser = RunAllOpts <$> strOption ( long "r1cs-output-dir" - <> help "the directory to write the r1cs artifact" + <> help "the directory to write the r1cs.jsonl artifact" <> value "./snarkl-output" <> showDefault ) @@ -41,7 +41,7 @@ runAllOptsParser = <*> inputOptsParser <*> strOption ( long "witness-output-dir" - <> help "the directory to write the witness.jsonl file" + <> help "the directory to write the witness.jsonl artifact" <> value "./snarkl-output" <> showDefault ) @@ -98,10 +98,10 @@ runAll RunAllOpts {..} name comp = do ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let r1csFP = mkR1CSFilePath r1csOutput name - writeFileWithDir r1csFP . toJSONLines $ + writeFileWithDir r1csFP . toJSONLines $ WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name - writeFileWithDir witnessFP . toJSONLines $ + writeFileWithDir witnessFP . toJSONLines $ WithHeader (r1csHeader r1cs) (Map.toList $ fmap FieldElem assgn) putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/Compile.hs b/src/Snarkl/Compile.hs index b30fee1..9d8a7d7 100644 --- a/src/Snarkl/Compile.hs +++ b/src/Snarkl/Compile.hs @@ -436,14 +436,14 @@ compileConstraintsToR1CS simpls cs = -- Renumber constraint variables sequentially, from 0 to -- 'max_var'. 'renumber_f' is a function mapping variables to -- their renumbered counterparts. - (_, cs') = second SimplifiedConstraintSystem $ renumber_constraints cs_dataflow + (_, simplifiedCS) = second SimplifiedConstraintSystem $ renumber_constraints cs_dataflow in -- 'f' is a function mapping input bindings to witnesses. -- NOTE: we assume the initial variable assignment passed to -- 'f' is the one derived by zipping the inputs together with -- the (renamed) input vars. of the R1CS produced by this -- function. Alternatively, we could 'Map.mapKeys renumber_f' -- before applying 'solve cs''. - (r1cs_of_cs cs', cs') + (r1cs_of_cs simplifiedCS, simplifiedCS) where must_simplify :: Bool must_simplify = Simplify `elem` simpls From b2c6d427d5468cb0656f5bc9e56ca8a941c2218d Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 17 Jan 2024 12:53:03 -0800 Subject: [PATCH 11/13] tests pass --- snarkl.cabal | 2 +- src/Snarkl/Backend/R1CS/R1CS.hs | 17 ++++++++++------ src/Snarkl/Compile.hs | 2 -- tests/Test/ArkworksBridge.hs | 35 ++++++++++++++++++++++----------- 4 files changed, 36 insertions(+), 20 deletions(-) diff --git a/snarkl.cabal b/snarkl.cabal index c635151..e011bb3 100644 --- a/snarkl.cabal +++ b/snarkl.cabal @@ -37,6 +37,7 @@ library Snarkl.Backend.R1CS.Poly Snarkl.Backend.R1CS.R1CS Snarkl.CLI + Snarkl.CLI.Common Snarkl.Common Snarkl.Compile Snarkl.Constraint @@ -58,7 +59,6 @@ library Snarkl.Toplevel other-modules: - Snarkl.CLI.Common Snarkl.CLI.Compile Snarkl.CLI.GenWitness Snarkl.CLI.RunAll diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index 99b046c..a87d0d2 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -4,6 +4,7 @@ module Snarkl.Backend.R1CS.R1CS r1csHeader, Witness (..), witnessHeader, + witnessInputs, WitnessHeader (..), sat_r1cs, num_constraints, @@ -85,17 +86,17 @@ data WitnessHeader = WitnessHeader instance A.ToJSON WitnessHeader where toJSON (WitnessHeader in_vars out_vars num_vars) = A.object - [ "in_vars" A..= in_vars, - "out_vars" A..= out_vars, - "num_vars" A..= num_vars + [ "input_variables" A..= in_vars, + "output_variables" A..= out_vars, + "n_variables" A..= num_vars ] instance A.FromJSON WitnessHeader where parseJSON = A.withObject "WitnessHeader" $ \v -> do - in_vars <- v A..: "in_vars" - out_vars <- v A..: "out_vars" - num_vars <- v A..: "num_vars" + in_vars <- v A..: "input_variables" + out_vars <- v A..: "output_variables" + num_vars <- v A..: "n_variables" pure $ WitnessHeader in_vars out_vars num_vars witnessHeader :: Witness k -> WitnessHeader @@ -106,6 +107,10 @@ witnessHeader (Witness {..}) = num_vars = witness_num_vars } +witnessInputs :: Witness k -> Assgn k +witnessInputs (Witness {witness_in_vars, witness_assgn = Assgn m}) = + Assgn $ Map.filterWithKey (\k _ -> k `elem` witness_in_vars) m + num_constraints :: R1CS a -> Int num_constraints = length . r1cs_clauses diff --git a/src/Snarkl/Compile.hs b/src/Snarkl/Compile.hs index 9d8a7d7..8639bef 100644 --- a/src/Snarkl/Compile.hs +++ b/src/Snarkl/Compile.hs @@ -565,5 +565,3 @@ compileCompToR1CS simpl = compileConstraintsToR1CS simpl . compileCompToConstrai _Var :: Iso' Variable Var _Var = iso (\(Variable v) -> Var v) (\(Var v) -> Variable v) - --------------------------------------------------------------------------------- diff --git a/tests/Test/ArkworksBridge.hs b/tests/Test/ArkworksBridge.hs index b0a678f..ff54d11 100644 --- a/tests/Test/ArkworksBridge.hs +++ b/tests/Test/ArkworksBridge.hs @@ -2,10 +2,16 @@ module Test.ArkworksBridge where import qualified Data.ByteString.Lazy as LBS import Data.Field.Galois (GaloisField, PrimeField) +import Data.JSONLines (NoHeader (NoHeader), ToJSONLines (toJSONLines), WithHeader (WithHeader)) +import qualified Data.Map as Map import Data.Typeable (Typeable) import Snarkl.Backend.R1CS +import Snarkl.Backend.R1CS.R1CS (witnessInputs) +import Snarkl.CLI.Common (mkInputsFilePath, mkR1CSFilePath, mkWitnessFilePath) +import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem)) import Snarkl.Compile (SimplParam, compileCompToR1CS) import Snarkl.Language (Comp) +import Snarkl.Toplevel (wit_of_cs) import qualified System.Exit as GHC import System.Process (createProcess, shell, waitForProcess) @@ -16,9 +22,10 @@ data CMD k where runCMD :: (PrimeField k) => CMD k -> IO GHC.ExitCode runCMD (CreateTrustedSetup rootDir name simpl c) = do - let r1cs = compileCompToR1CS simpl c + let (r1cs, _) = compileCompToR1CS simpl c r1csFilePath = mkR1CSFilePath rootDir name - LBS.writeFile r1csFilePath (serializeR1CSAsJson r1cs) + LBS.writeFile r1csFilePath . toJSONLines $ + WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) let cmd = mkCommand "create-trusted-setup" @@ -30,12 +37,14 @@ runCMD (CreateTrustedSetup rootDir name simpl c) = do (_, _, _, hdl) <- createProcess $ shell cmd waitForProcess hdl runCMD (CreateProof rootDir name simpl c inputs) = do - let r1cs = compileCompToR1CS simpl c - wit = wit_of_r1cs inputs r1cs + let (r1cs, simplifiedCS) = compileCompToR1CS simpl c + wit@(Witness {witness_assgn = Assgn m}) = wit_of_cs inputs simplifiedCS r1csFilePath = mkR1CSFilePath rootDir name witsFilePath = mkWitnessFilePath rootDir name - LBS.writeFile r1csFilePath (serializeR1CSAsJson r1cs) - LBS.writeFile witsFilePath (serializeWitnessAsJson r1cs wit) + LBS.writeFile r1csFilePath . toJSONLines $ + WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) + LBS.writeFile witsFilePath . toJSONLines $ + WithHeader (witnessHeader wit) (Map.toList (FieldElem <$> m)) let cmd = mkCommand "create-proof" @@ -47,14 +56,18 @@ runCMD (CreateProof rootDir name simpl c inputs) = do (_, _, _, hdl) <- createProcess $ shell cmd waitForProcess hdl runCMD (RunR1CS rootDir name simpl c inputs) = do - let r1cs = compileCompToR1CS simpl c - wit = wit_of_r1cs inputs r1cs + let (r1cs, simplifiedCS) = compileCompToR1CS simpl c + wit@(Witness {witness_assgn = Assgn m}) = wit_of_cs inputs simplifiedCS r1csFilePath = mkR1CSFilePath rootDir name witsFilePath = mkWitnessFilePath rootDir name inputsFilePath = mkInputsFilePath rootDir name - LBS.writeFile r1csFilePath (serializeR1CSAsJson r1cs) - LBS.writeFile witsFilePath (serializeWitnessAsJson r1cs wit) - LBS.writeFile inputsFilePath (serializeInputsAsJson r1cs inputs) + LBS.writeFile r1csFilePath . toJSONLines $ + WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) + LBS.writeFile witsFilePath . toJSONLines $ + WithHeader (witnessHeader wit) (Map.toList (FieldElem <$> m)) + let Assgn inputAssignments = witnessInputs wit + LBS.writeFile inputsFilePath . toJSONLines $ + NoHeader (Map.toList $ FieldElem <$> inputAssignments) let cmd = mkCommand "run-r1cs" From 8506960d6ad56b5564667fafdd293631574274e3 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 17 Jan 2024 13:46:47 -0800 Subject: [PATCH 12/13] way easier and more consistent jsonl serialization --- src/Data/JSONLines.hs | 2 +- src/Snarkl/Backend/R1CS/R1CS.hs | 69 ++++++++++++++++++++-------- src/Snarkl/CLI/Compile.hs | 9 ++-- src/Snarkl/CLI/GenWitness.hs | 42 +++++------------ src/Snarkl/CLI/RunAll.hs | 14 ++---- src/Snarkl/Common.hs | 32 ++++++++----- src/Snarkl/Constraint/Constraints.hs | 40 ++++++++++------ tests/Test/ArkworksBridge.hs | 23 ++++------ 8 files changed, 124 insertions(+), 107 deletions(-) diff --git a/src/Data/JSONLines.hs b/src/Data/JSONLines.hs index d9628ab..fc0ef87 100644 --- a/src/Data/JSONLines.hs +++ b/src/Data/JSONLines.hs @@ -28,7 +28,7 @@ instance Monoid JSONLine where data WithHeader :: Type -> Type -> Type where WithHeader :: hdr -> [item] -> WithHeader hdr item -data NoHeader item = NoHeader [item] +newtype NoHeader item = NoHeader [item] jsonlBuilder :: (Foldable t) => diff --git a/src/Snarkl/Backend/R1CS/R1CS.hs b/src/Snarkl/Backend/R1CS/R1CS.hs index a87d0d2..16dd89a 100644 --- a/src/Snarkl/Backend/R1CS/R1CS.hs +++ b/src/Snarkl/Backend/R1CS/R1CS.hs @@ -1,11 +1,8 @@ module Snarkl.Backend.R1CS.R1CS ( R1C (..), R1CS (..), - r1csHeader, Witness (..), - witnessHeader, witnessInputs, - WitnessHeader (..), sat_r1cs, num_constraints, ) @@ -13,7 +10,9 @@ where import Control.Parallel.Strategies import qualified Data.Aeson as A +import Data.Bifunctor (Bifunctor (second)) import Data.Field.Galois (GaloisField (char, deg), PrimeField) +import Data.JSONLines (FromJSONLines (fromJSONLines), ToJSONLines (toJSONLines), WithHeader (..)) import qualified Data.Map as Map import Snarkl.Backend.R1CS.Poly import Snarkl.Common @@ -55,16 +54,29 @@ data R1CS a = R1CS } deriving (Show) -r1csHeader :: (GaloisField a) => R1CS a -> ConstraintHeader -r1csHeader (cs :: R1CS a) = - ConstraintHeader - { field_characteristic = toInteger $ char (undefined :: a), - extension_degree = toInteger $ deg (undefined :: a), - n_constraints = num_constraints cs, - n_variables = r1cs_num_vars cs, - input_variables = r1cs_in_vars cs, - output_variables = r1cs_out_vars cs - } +instance (PrimeField k) => ToJSONLines (R1CS k) where + toJSONLines cs = toJSONLines $ WithHeader (r1csHeader cs) (r1cs_clauses cs) + where + r1csHeader (_ :: R1CS a) = + ConstraintHeader + { field_characteristic = toInteger $ char (undefined :: a), + extension_degree = toInteger $ deg (undefined :: a), + n_constraints = num_constraints cs, + n_variables = r1cs_num_vars cs, + input_variables = r1cs_in_vars cs, + output_variables = r1cs_out_vars cs + } + +instance (PrimeField k) => FromJSONLines (R1CS k) where + fromJSONLines ls = do + WithHeader ConstraintHeader {..} cs <- fromJSONLines ls + pure + R1CS + { r1cs_clauses = cs, + r1cs_num_vars = fromIntegral n_variables, + r1cs_in_vars = input_variables, + r1cs_out_vars = output_variables + } data Witness k = Witness { witness_assgn :: Assgn k, @@ -99,13 +111,30 @@ instance A.FromJSON WitnessHeader where num_vars <- v A..: "n_variables" pure $ WitnessHeader in_vars out_vars num_vars -witnessHeader :: Witness k -> WitnessHeader -witnessHeader (Witness {..}) = - WitnessHeader - { in_vars = witness_in_vars, - out_vars = witness_out_vars, - num_vars = witness_num_vars - } +instance (PrimeField k) => ToJSONLines (Witness k) where + toJSONLines wit@(Witness {witness_assgn = Assgn m}) = + toJSONLines $ + WithHeader + (witnessHeader wit) + (Map.toList (FieldElem <$> m)) + where + witnessHeader (Witness {..}) = + WitnessHeader + { in_vars = witness_in_vars, + out_vars = witness_out_vars, + num_vars = witness_num_vars + } + +instance (PrimeField k) => FromJSONLines (Witness k) where + fromJSONLines ls = do + WithHeader WitnessHeader {..} assgn <- fromJSONLines ls + pure + Witness + { witness_assgn = Assgn $ Map.fromList (second unFieldElem <$> assgn), + witness_in_vars = in_vars, + witness_out_vars = out_vars, + witness_num_vars = num_vars + } witnessInputs :: Witness k -> Assgn k witnessInputs (Witness {witness_in_vars, witness_assgn = Assgn m}) = diff --git a/src/Snarkl/CLI/Compile.hs b/src/Snarkl/CLI/Compile.hs index 2081c57..85b2dd2 100644 --- a/src/Snarkl/CLI/Compile.hs +++ b/src/Snarkl/CLI/Compile.hs @@ -18,13 +18,12 @@ import Data.JSONLines (ToJSONLines (toJSONLines), WithHeader (..)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.Set as Set -import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (CommandFields, Mod, Parser, command, execParser, fullDesc, header, help, helper, info, long, progDesc, showDefault, strOption, subparser, switch, value, (<**>)) import Snarkl.Backend.R1CS import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, writeFileWithDir) import Snarkl.Compile -import Snarkl.Constraint (ConstraintSystem (cs_constraints, cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem), constraintSystemHeader) +import Snarkl.Constraint (ConstraintSystem (cs_constraints, cs_out_vars), SimplifiedConstraintSystem (unSimplifiedConstraintSystem)) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language import Snarkl.Toplevel (comp_interp, wit_of_cs) @@ -86,10 +85,8 @@ compile CompileOpts {..} name comp = do TExpPkg nv in_vars e = compileCompToTexp comp (r1cs, cs) = compileTExpToR1CS simpl (TExpPkg nv in_vars e) let r1csFP = mkR1CSFilePath r1csOutput name - writeFileWithDir r1csFP . toJSONLines $ - WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) + writeFileWithDir r1csFP $ toJSONLines r1cs putStrLn $ "Wrote R1CS to " <> r1csFP let csFP = mkConstraintsFilePath constraintsOutput name - writeFileWithDir csFP . toJSONLines $ - WithHeader (constraintSystemHeader cs) (Set.toList $ cs_constraints $ unSimplifiedConstraintSystem cs) + writeFileWithDir csFP $ toJSONLines cs putStrLn $ "Wrote constraints to " <> csFP diff --git a/src/Snarkl/CLI/GenWitness.hs b/src/Snarkl/CLI/GenWitness.hs index 2f9f25e..bb13ebf 100644 --- a/src/Snarkl/CLI/GenWitness.hs +++ b/src/Snarkl/CLI/GenWitness.hs @@ -13,16 +13,16 @@ import Control.Applicative ((<|>)) import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (..), ToJSONLines (toJSONLines), WithHeader (..)) +import Data.JSONLines (FromJSONLines (fromJSONLines), ToJSONLines (toJSONLines)) +import Data.List (sortOn) import qualified Data.Map as Map -import qualified Data.Set as Set import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (Parser, eitherReader, help, long, option, showDefault, strOption, value) import Snarkl.Backend.R1CS import Snarkl.CLI.Common (mkConstraintsFilePath, mkR1CSFilePath, mkWitnessFilePath, readFileLines, writeFileWithDir) -import Snarkl.Common (Assgn (Assgn), ConstraintHeader (..), FieldElem (..)) -import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (SimplifiedConstraintSystem, unSimplifiedConstraintSystem)) +import Snarkl.Common (Assgn (Assgn)) +import Snarkl.Constraint (ConstraintSystem (..), SimplifiedConstraintSystem (unSimplifiedConstraintSystem)) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language (Comp) import Snarkl.Toplevel (comp_interp, wit_of_cs) @@ -89,23 +89,15 @@ genWitness GenWitnessOpts {..} name comp = do constraints <- do let csFP = mkConstraintsFilePath constraintsInput name eConstraints <- fromJSONLines <$> readFileLines csFP - (WithHeader ConstraintHeader {..} cs) <- either (failWith . ErrMsg) pure eConstraints - pure $ - SimplifiedConstraintSystem $ - ConstraintSystem - { cs_constraints = Set.fromList cs, - cs_num_vars = n_variables, - cs_in_vars = input_variables, - cs_out_vars = output_variables - } + either (failWith . ErrMsg) pure eConstraints let [out_var] = cs_out_vars (unSimplifiedConstraintSystem constraints) -- parse the inputs, either from cli or from file is <- case inputs of Explicit is -> pure $ map fromInteger is FromFile fp -> do eInput <- fromJSONLines <$> readFileLines fp - NoHeader input <- either (failWith . ErrMsg) pure eInput - pure $ map unFieldElem input + let Assgn input = either (failWith . ErrMsg) id eInput + pure . map snd . sortOn fst $ Map.toList input let out_interp = comp_interp comp is witness@(Witness {witness_assgn = Assgn m}) = wit_of_cs is constraints out = case Map.lookup out_var m of @@ -127,25 +119,13 @@ genWitness GenWitnessOpts {..} name comp = do ++ show out r1cs <- do let r1csFP = mkR1CSFilePath r1csInput name - (WithHeader ConstraintHeader {..} items) <- do - eConstraints <- fromJSONLines <$> readFileLines r1csFP - either (failWith . ErrMsg) pure eConstraints - pure $ - R1CS - { r1cs_clauses = items, - r1cs_num_vars = n_variables, - r1cs_in_vars = input_variables, - r1cs_out_vars = output_variables - } - let witnessAssgn@(Assgn assgn) = witness_assgn witness + eConstraints <- fromJSONLines <$> readFileLines r1csFP + either (failWith . ErrMsg) pure eConstraints unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ - "witness\n " - ++ CS.cs (A.encode witnessAssgn) - ++ "\nfailed to satisfy R1CS\n " + "witness failed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let witnessFP = mkWitnessFilePath witnessOutput name - writeFileWithDir witnessFP . toJSONLines $ - WithHeader (witnessHeader witness) (Map.toList (FieldElem <$> assgn)) + writeFileWithDir witnessFP $ toJSONLines witness putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/CLI/RunAll.hs b/src/Snarkl/CLI/RunAll.hs index a5ceb6a..d660c41 100644 --- a/src/Snarkl/CLI/RunAll.hs +++ b/src/Snarkl/CLI/RunAll.hs @@ -5,17 +5,17 @@ module Snarkl.CLI.RunAll where import Control.Monad (unless) import qualified Data.Aeson as A import Data.Field.Galois (PrimeField) -import Data.JSONLines (FromJSONLines (..), NoHeader (..), ToJSONLines (..), WithHeader (..)) +import Data.JSONLines (FromJSONLines (..), NoHeader (..), ToJSONLines (..)) import qualified Data.Map as Map import Data.Maybe (catMaybes) import qualified Data.String.Conversions as CS import Data.Typeable (Typeable) import Options.Applicative (Parser, help, long, showDefault, strOption, value) -import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), Witness (Witness, witness_assgn), r1csHeader, sat_r1cs) +import Snarkl.Backend.R1CS (R1CS (r1cs_clauses, r1cs_out_vars), Witness (Witness, witness_assgn), sat_r1cs) import Snarkl.CLI.Common (mkR1CSFilePath, mkWitnessFilePath, readFileLines, writeFileWithDir) import Snarkl.CLI.Compile (OptimizeOpts (removeUnreachable, simplify), optimizeOptsParser) import Snarkl.CLI.GenWitness (InputOpts (Explicit, FromFile), inputOptsParser) -import Snarkl.Common (Assgn (Assgn), FieldElem (FieldElem, unFieldElem)) +import Snarkl.Common (Assgn (Assgn), unFieldElem) import Snarkl.Compile (SimplParam (RemoveUnreachable, Simplify), TExpPkg (TExpPkg), compileCompToTexp, compileTExpToR1CS) import Snarkl.Errors (ErrMsg (ErrMsg), failWith) import Snarkl.Language (Comp) @@ -89,19 +89,15 @@ runAll RunAllOpts {..} name comp = do ++ show out_interp ++ " differs from actual result " ++ show out - let witnessAssgn@(Assgn assgn) = witness_assgn witness unless (sat_r1cs witness r1cs) $ failWith $ ErrMsg $ "witness\n " - ++ CS.cs (A.encode witnessAssgn) ++ "\nfailed to satisfy R1CS\n " ++ CS.cs (A.encode $ r1cs_clauses r1cs) let r1csFP = mkR1CSFilePath r1csOutput name - writeFileWithDir r1csFP . toJSONLines $ - WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) + writeFileWithDir r1csFP $ toJSONLines r1cs putStrLn $ "Wrote R1CS to " <> r1csFP let witnessFP = mkWitnessFilePath witnessOutput name - writeFileWithDir witnessFP . toJSONLines $ - WithHeader (r1csHeader r1cs) (Map.toList $ fmap FieldElem assgn) + writeFileWithDir witnessFP $ toJSONLines witness putStrLn $ "Wrote witness to " <> witnessFP diff --git a/src/Snarkl/Common.hs b/src/Snarkl/Common.hs index 378d5fc..136d8e5 100644 --- a/src/Snarkl/Common.hs +++ b/src/Snarkl/Common.hs @@ -3,8 +3,10 @@ module Snarkl.Common where import qualified Data.Aeson as A +import Data.Bifunctor (Bifunctor (second)) import Data.Field.Galois (PrimeField (fromP)) -import Data.Foldable (Foldable (toList)) +import Data.Foldable (toList) +import Data.JSONLines (FromJSONLines (fromJSONLines), NoHeader (..), ToJSONLines (toJSONLines)) import qualified Data.Map as Map import Text.PrettyPrint.Leijen.Text (Pretty (pretty)) @@ -29,6 +31,18 @@ incVar (Var i) = Var (i + 1) newtype Assgn a = Assgn (Map.Map Var a) deriving (Show, Eq, Functor) +instance (PrimeField a) => A.ToJSON (Assgn a) where + toJSON (Assgn m) = + let kvs = map (\(var, coeff) -> (FieldElem coeff, var)) $ Map.toList m + in A.toJSON kvs + +instance (PrimeField a) => A.FromJSON (Assgn a) where + parseJSON = + A.withArray "Assgn" $ \arr -> do + kvs <- mapM A.parseJSON arr + let m = Map.fromList $ map (\(FieldElem k, v) -> (v, k)) (toList kvs) + return (Assgn m) + -- We use this wrapper to get a stringified representation of big integers. -- This plays better with downstream dependencies, e.g. javascript. newtype FieldElem k = FieldElem {unFieldElem :: k} deriving (Show, Eq) @@ -41,17 +55,13 @@ instance (PrimeField k) => A.FromJSON (FieldElem k) where k <- A.parseJSON v return $ FieldElem (fromInteger $ read k) -instance (PrimeField a) => A.ToJSON (Assgn a) where - toJSON (Assgn m) = - let kvs = map (\(var, coeff) -> (FieldElem coeff, var)) $ Map.toList m - in A.toJSON kvs +instance (PrimeField k) => ToJSONLines (Assgn k) where + toJSONLines (Assgn m) = toJSONLines $ NoHeader (Map.toList $ FieldElem <$> m) -instance (PrimeField a) => A.FromJSON (Assgn a) where - parseJSON = - A.withArray "Assgn" $ \arr -> do - kvs <- mapM A.parseJSON arr - let m = Map.fromList $ map (\(FieldElem k, v) -> (v, k)) (toList kvs) - return (Assgn m) +instance (PrimeField k) => FromJSONLines (Assgn k) where + fromJSONLines ls = do + NoHeader kvs <- fromJSONLines ls + pure . Assgn . Map.fromList $ map (second unFieldElem) kvs data UnOp = ZEq deriving (Eq, Show) diff --git a/src/Snarkl/Constraint/Constraints.hs b/src/Snarkl/Constraint/Constraints.hs index 779f94b..41da167 100644 --- a/src/Snarkl/Constraint/Constraints.hs +++ b/src/Snarkl/Constraint/Constraints.hs @@ -9,7 +9,6 @@ module Snarkl.Constraint.Constraints ConstraintSet, ConstraintSystem (..), SimplifiedConstraintSystem (..), - constraintSystemHeader, r1cs_of_cs, renumber_constraints, constraint_vars, @@ -20,6 +19,7 @@ import Control.Monad.State (State) import qualified Data.Aeson as A import Data.Bifunctor (Bifunctor (first, second)) import Data.Field.Galois (GaloisField (char, deg), Prime, PrimeField) +import Data.JSONLines (FromJSONLines (fromJSONLines), ToJSONLines (toJSONLines), WithHeader (..)) import qualified Data.Map as Map import qualified Data.Set as Set import Snarkl.Backend.R1CS (Poly (Poly), R1C (R1C), R1CS (R1CS), const_poly, var_poly) @@ -220,19 +220,31 @@ newtype SimplifiedConstraintSystem a = SimplifiedConstraintSystem } deriving (Show, Eq) -constraintSystemHeader :: - (GaloisField a) => - SimplifiedConstraintSystem a -> - ConstraintHeader -constraintSystemHeader (SimplifiedConstraintSystem (ConstraintSystem {..}) :: SimplifiedConstraintSystem a) = - ConstraintHeader - { field_characteristic = toInteger $ char (undefined :: a), - extension_degree = toInteger $ deg (undefined :: a), - n_constraints = Set.size cs_constraints, - n_variables = cs_num_vars, - input_variables = cs_in_vars, - output_variables = cs_out_vars - } +instance (PrimeField k) => ToJSONLines (SimplifiedConstraintSystem k) where + toJSONLines scs@(SimplifiedConstraintSystem (ConstraintSystem {..})) = + toJSONLines $ WithHeader (constraintSystemHeader scs) (Set.toList cs_constraints) + where + constraintSystemHeader (_ :: SimplifiedConstraintSystem a) = + ConstraintHeader + { field_characteristic = toInteger $ char (undefined :: a), + extension_degree = toInteger $ deg (undefined :: a), + n_constraints = Set.size cs_constraints, + n_variables = cs_num_vars, + input_variables = cs_in_vars, + output_variables = cs_out_vars + } + +instance (PrimeField k) => FromJSONLines (SimplifiedConstraintSystem k) where + fromJSONLines ls = do + WithHeader ConstraintHeader {..} cs <- fromJSONLines ls + pure $ + SimplifiedConstraintSystem $ + ConstraintSystem + { cs_constraints = Set.fromList cs, + cs_num_vars = fromIntegral n_variables, + cs_in_vars = input_variables, + cs_out_vars = output_variables + } r1cs_of_cs :: (GaloisField a) => diff --git a/tests/Test/ArkworksBridge.hs b/tests/Test/ArkworksBridge.hs index ff54d11..226bc05 100644 --- a/tests/Test/ArkworksBridge.hs +++ b/tests/Test/ArkworksBridge.hs @@ -2,7 +2,7 @@ module Test.ArkworksBridge where import qualified Data.ByteString.Lazy as LBS import Data.Field.Galois (GaloisField, PrimeField) -import Data.JSONLines (NoHeader (NoHeader), ToJSONLines (toJSONLines), WithHeader (WithHeader)) +import Data.JSONLines (ToJSONLines (toJSONLines)) import qualified Data.Map as Map import Data.Typeable (Typeable) import Snarkl.Backend.R1CS @@ -24,8 +24,7 @@ runCMD :: (PrimeField k) => CMD k -> IO GHC.ExitCode runCMD (CreateTrustedSetup rootDir name simpl c) = do let (r1cs, _) = compileCompToR1CS simpl c r1csFilePath = mkR1CSFilePath rootDir name - LBS.writeFile r1csFilePath . toJSONLines $ - WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) + LBS.writeFile r1csFilePath $ toJSONLines r1cs let cmd = mkCommand "create-trusted-setup" @@ -38,13 +37,11 @@ runCMD (CreateTrustedSetup rootDir name simpl c) = do waitForProcess hdl runCMD (CreateProof rootDir name simpl c inputs) = do let (r1cs, simplifiedCS) = compileCompToR1CS simpl c - wit@(Witness {witness_assgn = Assgn m}) = wit_of_cs inputs simplifiedCS + witness = wit_of_cs inputs simplifiedCS r1csFilePath = mkR1CSFilePath rootDir name witsFilePath = mkWitnessFilePath rootDir name - LBS.writeFile r1csFilePath . toJSONLines $ - WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) - LBS.writeFile witsFilePath . toJSONLines $ - WithHeader (witnessHeader wit) (Map.toList (FieldElem <$> m)) + LBS.writeFile r1csFilePath $ toJSONLines r1cs + LBS.writeFile witsFilePath $ toJSONLines witness let cmd = mkCommand "create-proof" @@ -61,13 +58,9 @@ runCMD (RunR1CS rootDir name simpl c inputs) = do r1csFilePath = mkR1CSFilePath rootDir name witsFilePath = mkWitnessFilePath rootDir name inputsFilePath = mkInputsFilePath rootDir name - LBS.writeFile r1csFilePath . toJSONLines $ - WithHeader (r1csHeader r1cs) (r1cs_clauses r1cs) - LBS.writeFile witsFilePath . toJSONLines $ - WithHeader (witnessHeader wit) (Map.toList (FieldElem <$> m)) - let Assgn inputAssignments = witnessInputs wit - LBS.writeFile inputsFilePath . toJSONLines $ - NoHeader (Map.toList $ FieldElem <$> inputAssignments) + LBS.writeFile r1csFilePath $ toJSONLines r1cs + LBS.writeFile witsFilePath $ toJSONLines wit + LBS.writeFile inputsFilePath $ toJSONLines $ witnessInputs wit let cmd = mkCommand "run-r1cs" From 2d8c7508dca9989efbd8066ee5c64d6717dbd06e Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 17 Jan 2024 18:53:39 -0800 Subject: [PATCH 13/13] update arkworks tag --- .github/workflows/nix-ci.yml | 2 +- app/Main.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml index 0177596..c58bd0c 100644 --- a/.github/workflows/nix-ci.yml +++ b/.github/workflows/nix-ci.yml @@ -18,7 +18,7 @@ jobs: uses: jaxxstorm/action-install-gh-release@v1.10.0 with: repo: torsion-labs/arkworks-bridge - tag: v0.2.0 + tag: v1.0.0-rc1 - uses: cachix/install-nix-action@v24 with: diff --git a/app/Main.hs b/app/Main.hs index 3a16d85..858d119 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -6,4 +6,4 @@ import Snarkl.Toplevel (Comp, Ty (TField)) import qualified Test.Snarkl.Unit.Programs as Programs main :: IO () -main = defaultMain "prog2" (Programs.prog2 10 :: Comp 'TField F_BN128) +main = defaultMain "prog" (Programs.prog2 10 :: Comp 'TField F_BN128)