fix circom variable order

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 }

app/Contracts/Groth16Verifier.purs

@@ -9,11 +9,11 @@ import Network.Ethereum.Web3 (Vector, Web3, call)
 import Network.Ethereum.Web3.Solidity (Tuple1, Tuple4, UIntN, fromRecord, unTuple1)
 import Network.Ethereum.Web3.Types (CallError, ChainCursor, NoPay, TransactionOptions)
 
-type FnVerifyProofInput = Tagged "verifyProof(uint256[2],uint256[2][2],uint256[2],uint256[3])"
+type FnVerifyProofInput = Tagged "verifyProof(uint256[2],uint256[2][2],uint256[2],uint256[2])"
   ( Tuple4 (Tagged "_pA" (Identity (Vector 2 (UIntN 256))))
       (Tagged "_pB" (Identity (Vector 2 (Vector 2 (UIntN 256)))))
       (Tagged "_pC" (Identity (Vector 2 (UIntN 256))))
-      (Tagged "_pubSignals" (Identity (Vector 3 (UIntN 256))))
+      (Tagged "_pubSignals" (Identity (Vector 2 (UIntN 256))))
   )
 
 type FnVerifyProofOutput = Tuple1 Boolean
@@ -24,7 +24,7 @@ verifyProof
   -> { _pA :: Vector 2 (UIntN 256)
      , _pB :: Vector 2 (Vector 2 (UIntN 256))
      , _pC :: Vector 2 (UIntN 256)
-     , _pubSignals :: Vector 3 (UIntN 256)
+     , _pubSignals :: Vector 2 (UIntN 256)
      }
   -> Web3 (Either CallError Boolean)
 verifyProof txOpts chainCursor x = map unTuple1 <$> call txOpts chainCursor

cabal.project

@@ -25,7 +25,7 @@ source-repository-package
 source-repository-package
   type: git
   location: https://github.com/l-adic/arithmetic-circuits.git
-  tag: 1e16a0ce6683aba33e4ace30bbdefd06e1553160
+  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

@@ -35,5 +35,5 @@ source-repository-package
 source-repository-package
   type: git
   location: https://github.com/l-adic/arithmetic-circuits.git
-  tag: 1e16a0ce6683aba33e4ace30bbdefd06e1553160
+  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,7 @@ common deps
   build-depends:
       protolude
     , arithmetic-circuits
+    , arithmetic-circuits:circom-compat
     , arithmetic-circuits:language
     , base
     , containers
@@ -37,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

@@ -10,6 +10,7 @@ where
 
 import Circuit
 import Circuit.Language
+import R1CS.Circom (circomReindexMap)
 import Data.Field.Galois (GaloisField, Prime)
 import Protolude
 
@@ -19,7 +20,7 @@ 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 Public "b"
+  b <- var_ <$> fieldInput Private "b"
   boolOutput "out" $ eq_ n (a * b)
 
 data Factors f = Factors
@@ -30,7 +31,8 @@ data Factors f = Factors
 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

@@ -8,20 +8,23 @@ import Test.QuickCheck
 import ZK.Factors (Factors (..), Fr, factors)
 
 main :: IO ()
-main = hspec $ do
+main = do
   let circuit = factorsCircuit $ factors @Fr
       vars = factorsVars $ factors @Fr
-  describe "Factors" $ do
-    it "should accept valid factors" $ do
-      property $
-        \x y ->
-          let inputs = assignInputs vars $ Map.fromList [("n", x * y), ("a", x), ("b", y)]
-              w = solve vars circuit inputs
-          in lookupVar vars "out" w === Just 1
-    it "shouldn't accept invalid factors" $ do
-      property $
-        \x y z ->
-          (x * y /= z) ==>
-            let inputs = assignInputs vars $ Map.fromList [("n", z), ("a", x), ("b", y)]
+  print circuit
+  print vars
+  hspec $ do
+    describe "Factors" $ do
+      it "should accept valid factors" $ do
+        property $
+          \x y ->
+            let inputs = assignInputs vars $ Map.fromList [("n", x * y), ("a", x), ("b", y)]
                 w = solve vars circuit inputs
-            in lookupVar vars "out" w == Just 0
+            in lookupVar vars "out" w === Just 1
+      it "shouldn't accept invalid factors" $ do
+        property $
+          \x y z ->
+            (x * y /= z) ==>
+              let inputs = assignInputs vars $ Map.fromList [("n", z), ("a", x), ("b", y)]
+                  w = solve vars circuit inputs
+              in lookupVar vars "out" w == Just 0