Merge pull request #4 from l-adic/update-arith-circuits

Update arith circuits

app/App/Component.purs

@@ -3,15 +3,20 @@ module App.Component where
 import Prelude
 
 import App.Form as Form
+import Data.Array ((!!))
 import Data.Either (Either(..))
-import Data.Maybe (Maybe(..), fromMaybe)
+import Data.Maybe (Maybe(..), fromJust, fromMaybe)
 import Effect.Aff (Aff, attempt)
+import Effect.Class.Console as Console
 import Halogen (liftAff)
 import Halogen as H
 import Halogen.HTML as HH
 import JS.BigInt (BigInt)
+import JS.BigInt as BigInt
 import Network.Ethereum.Web3 (Provider, runWeb3)
+import Partial.Unsafe (unsafePartial)
 import Prover.Prove (fullProve)
+import Prover.Types (Fp(..), Inputs(..))
 import Prover.Verify (verifierAddress, verify)
 import Type.Proxy (Proxy(..))
 
@@ -62,8 +67,9 @@ component =
       eProof <- liftAff $ attempt $
         fullProve { a: ci.factorA, b: ci.factorB, n: ci.product }
       case eProof of
-        Left _ -> do
-          let msg = "Prover Error, are you sure the statement is true?"
+        Left e -> do
+          Console.log $ "Prover Error: " <> show e
+          let msg = "Prover Error, check console logs for details."
           H.modify_ _ { message = Just msg }
         Right { inputs, proof } -> do
           { provider } <- H.get
@@ -74,5 +80,13 @@ component =
               Right res ->
                 case res of
                   Left callError -> "Call Error " <> show callError
-                  Right b -> "Proof validated by conract: " <> show b
+                  -- this contract reverts if it doesn't terminate with true
+                  Right _ -> 
+                    let ins = unsafePartial $ fromJust do
+                          let Inputs is = inputs  
+                          out <- is !! 0
+                          n <- is !! 1
+                          -- the output is a field encoded boolean value
+                          pure {out: out == Fp (BigInt.fromInt 1), n}
+                    in "Proof validated by conract with public inputs " <> show ins
           H.modify_ _ { message = Just msg }

cabal.project

@@ -19,13 +19,13 @@ source-repository-package
 source-repository-package
   type: git
   location: https://github.com/l-adic/galois-fields.git
-  tag: fc82039e811ba68c10527cf871796b7ac8514926
+  tag: b0867ffdebda5043c80315a51b15e82ed25acba6
   --sha256: pYe2FTNHPTzZeTnOMe6S9eh3EOY6Hi6PjdfsNjPSOZQ=
 
 source-repository-package
   type: git
   location: https://github.com/l-adic/arithmetic-circuits.git
-  tag: 3212f88b9ff6e4c074fc7908ec72e15cbfc8015e
+  tag: d243f4cd91fb0adae11c18c726ef884cf7ea7d0d
   --sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q=
 
 index-state: 2023-10-15T12:29:38Z

factors-solver/app/Main.hs

@@ -16,7 +16,8 @@ stateRef = unsafePerformIO $ do
 {-# NOINLINE stateRef #-}
 
 env :: Circom.ProgramEnv Fr
-env = Circom.mkProgramEnv (factorsVars @Fr factors) (factorsCircuit factors)
+env = 
+  Circom.mkProgramEnv (factorsVars @Fr factors) (factorsCircuit factors)
 
 foreign export ccall init :: Int -> IO ()
 

factors-solver/cabal.project

@@ -29,11 +29,11 @@ source-repository-package
 source-repository-package
   type: git
   location: https://github.com/l-adic/galois-fields.git
-  tag: fc82039e811ba68c10527cf871796b7ac8514926
+  tag: b0867ffdebda5043c80315a51b15e82ed25acba6
   --sha256: pYe2FTNHPTzZeTnOMe6S9eh3EOY6Hi6PjdfsNjPSOZQ=
 
 source-repository-package
   type: git
   location: https://github.com/l-adic/arithmetic-circuits.git
-  tag: 3212f88b9ff6e4c074fc7908ec72e15cbfc8015e
-  --sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q=
+  tag: d243f4cd91fb0adae11c18c726ef884cf7ea7d0d
+  --sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q=

factors-solver/factors-solver.cabal

@@ -17,7 +17,7 @@ executable factors-solver
     "-optl-Wl,--export=init,--export=getNVars,--export=getVersion,--export=getRawPrime,--export=writeSharedRWMemory,--export=readSharedRWMemory,--export=getFieldNumLen32,--export=setInputSignal,--export=getInputSignalSize,--export=getWitnessSize,--export=getWitness,--export=getInputSize"
 
   build-depends:
-    , arithmetic-circuits:circom-compat
+      arithmetic-circuits:circom-compat
     , base            >=4.10  && <5
     , factors
     , protolude

factors/factors.cabal

@@ -20,6 +20,8 @@ common deps
   build-depends:
       protolude
     , arithmetic-circuits
+    , arithmetic-circuits:circom-compat
+    , arithmetic-circuits:language
     , base
     , containers
     , galois-field
@@ -36,8 +38,7 @@ executable factors
   import:           warnings, extensions, deps
   main-is:          Main.hs
   build-depends:
-    , arithmetic-circuits:circom-compat
-    , binary
+      binary
     , factors
     , aeson
     , wl-pprint-text  >=1.2.0

factors/src/ZK/Factors.hs

@@ -9,29 +9,30 @@ module ZK.Factors
 where
 
 import Circuit
+import Circuit.Language
+import R1CS.Circom (circomReindexMap)
 import Data.Field.Galois (GaloisField, Prime)
 import Protolude
 
-factorsE :: (GaloisField f) => ExprM f Wire
-factorsE = do
-  n <- deref <$> freshPublicInput "n"
-  a <- deref <$> freshPrivateInput "a"
-  b <- deref <$> freshPrivateInput "b"
-  let isFactorization = eq n (a `mul` b)
-  compileWithWire (freshPublicInput "out") $ 
-    cond isFactorization (c 1) (c 0)
-
 type Fr = Prime 21888242871839275222246405745257275088548364400416034343698204186575808495617
 
+factorsE :: (GaloisField f, Hashable f) => ExprM f (Var Wire f Bool)
+factorsE = do
+  n <- var_ <$> fieldInput Public "n"
+  a <- var_ <$> fieldInput Private "a"
+  b <- var_ <$> fieldInput Private "b"
+  boolOutput "out" $ eq_ n (a * b)
+
 data Factors f = Factors
   { factorsCircuit :: ArithCircuit f,
     factorsVars :: CircuitVars Text
   }
 
-factors :: forall f. (GaloisField f) => Factors f
+factors :: forall f. (GaloisField f, Hashable f) => Factors f
 factors =
   let BuilderState {..} = snd $ runCircuitBuilder (factorsE @f)
+      f = circomReindexMap bsVars
    in Factors
-        { factorsCircuit = bsCircuit,
-          factorsVars = bsVars
+        { factorsCircuit = reindex f bsCircuit,
+          factorsVars = reindex f bsVars
         }

factors/test/Main.hs

@@ -1,6 +1,6 @@
 module Main (main) where
 
-import Circuit (CircuitVars (..), solve)
+import Circuit (solve, lookupVar, assignInputs)
 import qualified Data.Map as Map
 import Protolude
 import Test.Hspec
@@ -11,23 +11,17 @@ main :: IO ()
 main = hspec $ do
   let circuit = factorsCircuit $ factors @Fr
       vars = factorsVars $ factors @Fr
-      (n, a, b, out) = fromMaybe (panic "Inputs not found") $ do
-        _n <- Map.lookup "n" $ cvInputsLabels vars
-        _a <- Map.lookup "a" $ cvInputsLabels vars
-        _b <- Map.lookup "b" $ cvInputsLabels vars
-        _out <- Map.lookup "out" $ cvInputsLabels vars
-        pure (_n, _a, _b, _out)
   describe "Factors" $ do
     it "should accept valid factors" $ do
       property $
         \x y ->
-          let inputs = Map.fromList [(n, x * y), (a, x), (b, y), (out,1)]
+          let inputs = assignInputs vars $ Map.fromList [("n", x * y), ("a", x), ("b", y)]
               w = solve vars circuit inputs
-           in Map.lookup out w == Just 1
+          in lookupVar vars "out" w === Just 1
     it "shouldn't accept invalid factors" $ do
       property $
         \x y z ->
           (x * y /= z) ==>
-            let inputs = Map.fromList [(n, z), (a, x), (b, y)]
+            let inputs = assignInputs vars $ Map.fromList [("n", z), ("a", x), ("b", y)]
                 w = solve vars circuit inputs
-             in Map.lookup out w == Just 0
+            in lookupVar vars "out" w == Just 0