Merge pull request #14 from l-adic/require-inputs-only-solve

Add Verify command

.gitignore

@@ -11,3 +11,5 @@ TAGS
 dist-newstyle
 inputs.json
 circuit-output
+factors.*
+factors-inputs-template.json

arithmetic-circuits.cabal

@@ -114,7 +114,7 @@ library circom-compat
       arithmetic-circuits
     , arithmetic-circuits:language
     , bytestring
-    , directory
+    , errors
     , optparse-applicative
     , vector
 

bench/Circuit/Bench.hs

@@ -6,7 +6,6 @@ import Criterion
 import Data.Field.Galois (Prime)
 import Data.IntMap qualified as IntMap
 import Data.Map qualified as Map
-import Data.Vector (generateM)
 import Protolude
 
 type Fr = Prime 21888242871839275222246405745257275088548364400416034343698204186575808495617
@@ -15,30 +14,25 @@ benchmarks :: Benchmark
 benchmarks =
   bgroup
     "largeMult"
-    [ bench "1_000" $ whnf largeMult 1000,
-      bench "10_000" $ whnf largeMult 10000,
-      bench "100_000" $ whnf largeMult 100_000,
-      bench "1_000_000" $ whnf largeMult 1_000_000
+    [ bench "1_000" $ whnf largeMult (Proxy @1000),
+      bench "10_000" $ whnf largeMult (Proxy @10000),
+      bench "100_000" $ whnf largeMult (Proxy @100_000),
+      bench "1_000_000" $ whnf largeMult (Proxy @1_000_000)
     ]
 
-largeMult :: Int -> Fr
+largeMult :: (KnownNat n) => Proxy n -> IO Fr
 largeMult n =
   let BuilderState {bsVars, bsCircuit} = snd $ runCircuitBuilder (program n)
       inputs =
-        assignInputs bsVars $
-          Map.fromList $
-            map (\i -> (nameInput i, fromIntegral i + 1)) [0 .. n - 1]
+        assignInputs bsVars $ Map.singleton "x" (Array $ map fromIntegral [1 .. natVal n])
       w = altSolve bsCircuit inputs
-   in fromMaybe (panic "output not found") $ lookupVar bsVars "out" w
+      res = fromMaybe (panic "output not found") $ lookupVar bsVars "out" w
+   in pure res
 
-nameInput :: (Integral a) => a -> Text
-nameInput i = "x" <> show (toInteger i)
-
-program :: Int -> ExprM Fr (Var Wire Fr 'TField)
-program p = do
-  xs <- generateM p $ \i ->
-    var_ <$> fieldInput Public (nameInput i)
-  fieldOutput "out" $ product xs
+program :: forall n. (KnownNat n) => Proxy n -> ExprM Fr (Var Wire Fr 'TField)
+program _ = do
+  xs <- fieldInputs @n Public "x"
+  fieldOutput "out" $ product $ map var_ xs
 
 altSolve :: ArithCircuit Fr -> IntMap Fr -> IntMap Fr
 altSolve p inputs =

circom-compat/app/Main.hs

@@ -16,9 +16,11 @@ program = do
   a <- var_ <$> fieldInput Private "a"
   b <- var_ <$> fieldInput Private "b"
   n <- var_ <$> fieldInput Public "n"
-  let cs =
+  zs <- map var_ <$> fieldInputs @5 Public "zs"
+  let s = unAdd_ $ foldMap Add_ zs
+      cs =
         [ neq_ n a,
           neq_ n b,
-          eq_ n (a * b)
+          eq_ n (a * b + s)
         ]
   boolOutput "out" $ unAnd_ $ foldMap And_ cs