diff --git a/app/App/Component.purs b/app/App/Component.purs index db96b11..bbd3a5d 100644 --- a/app/App/Component.purs +++ b/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 } \ No newline at end of file diff --git a/cabal.project b/cabal.project index 7a831c2..fedec56 100644 --- a/cabal.project +++ b/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 diff --git a/factors-solver/app/Main.hs b/factors-solver/app/Main.hs index 8acd106..68af0b0 100644 --- a/factors-solver/app/Main.hs +++ b/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 () diff --git a/factors-solver/cabal.project b/factors-solver/cabal.project index 61ebe1f..4b9e962 100644 --- a/factors-solver/cabal.project +++ b/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= \ No newline at end of file + tag: d243f4cd91fb0adae11c18c726ef884cf7ea7d0d + --sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q= diff --git a/factors-solver/factors-solver.cabal b/factors-solver/factors-solver.cabal index b31ea92..93f3af2 100644 --- a/factors-solver/factors-solver.cabal +++ b/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 diff --git a/factors/factors.cabal b/factors/factors.cabal index 7c3930e..665f163 100644 --- a/factors/factors.cabal +++ b/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 diff --git a/factors/src/ZK/Factors.hs b/factors/src/ZK/Factors.hs index 3189f7f..146f067 100644 --- a/factors/src/ZK/Factors.hs +++ b/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 } diff --git a/factors/test/Main.hs b/factors/test/Main.hs index fb70c3a..7eff9cd 100644 --- a/factors/test/Main.hs +++ b/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