Skip to content

Commit

Permalink
use circom program types
Browse files Browse the repository at this point in the history
  • Loading branch information
martyall committed May 21, 2024
1 parent 1b6ed5c commit 05c89ca
Show file tree
Hide file tree
Showing 6 changed files with 28 additions and 35 deletions.
4 changes: 2 additions & 2 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -19,13 +19,13 @@ source-repository-package
source-repository-package
type: git
location: https://github.com/l-adic/galois-fields.git
tag: b0867ffdebda5043c80315a51b15e82ed25acba6
tag: 525521de7b985364f7e0c32222fc3b21fea8e530
--sha256: pYe2FTNHPTzZeTnOMe6S9eh3EOY6Hi6PjdfsNjPSOZQ=

source-repository-package
type: git
location: https://github.com/l-adic/arithmetic-circuits.git
tag: d243f4cd91fb0adae11c18c726ef884cf7ea7d0d
tag: b0fc0e4d9e1fdcf7591298487284206688bcb8e1
--sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q=

index-state: 2023-10-15T12:29:38Z
Expand Down
7 changes: 3 additions & 4 deletions factors-solver/app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ import Circuit.Solver.Circom qualified as Circom
import Data.IORef (IORef, newIORef)
import Protolude
import System.IO.Unsafe (unsafePerformIO)
import ZK.Factors
import ZK.Factors (factors, Fr)

main :: IO ()
main = mempty
Expand All @@ -16,13 +16,12 @@ stateRef = unsafePerformIO $ do
{-# NOINLINE stateRef #-}

env :: Circom.ProgramEnv Fr
env =
Circom.mkProgramEnv (factorsVars @Fr factors) (factorsCircuit factors)
env = Circom.mkProgramEnv factors

foreign export ccall init :: Int -> IO ()

init :: Int -> IO ()
init = Circom._init
init = Circom._init env stateRef

foreign export ccall getNVars :: Int

Expand Down
4 changes: 2 additions & 2 deletions factors-solver/cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -29,11 +29,11 @@ source-repository-package
source-repository-package
type: git
location: https://github.com/l-adic/galois-fields.git
tag: b0867ffdebda5043c80315a51b15e82ed25acba6
tag: 525521de7b985364f7e0c32222fc3b21fea8e530
--sha256: pYe2FTNHPTzZeTnOMe6S9eh3EOY6Hi6PjdfsNjPSOZQ=

source-repository-package
type: git
location: https://github.com/l-adic/arithmetic-circuits.git
tag: d243f4cd91fb0adae11c18c726ef884cf7ea7d0d
tag: b0fc0e4d9e1fdcf7591298487284206688bcb8e1
--sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q=
6 changes: 3 additions & 3 deletions factors/app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ import Data.Binary (encodeFile)
import Protolude
import R1CS (toR1CS)
import R1CS.Circom (r1csToCircomR1CS)
import Circuit.Solver.Circom (CircomProgram(..))
import ZK.Factors

main :: IO ()
main = do
let Factors {..} = factors @Fr
r1cs = toR1CS factorsVars factorsCircuit
encodeFile "trusted-setup/circuit.r1cs" $ r1csToCircomR1CS r1cs
let r1cs = r1csToCircomR1CS $ toR1CS (cpVars factors) (cpCircuit factors)
encodeFile "trusted-setup/circuit.r1cs" r1cs
22 changes: 6 additions & 16 deletions factors/src/ZK/Factors.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,37 +2,27 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}

module ZK.Factors
( Factors (..),
factors,
( factors,
Fr,
)
where

import Circuit
import Circuit.Language
import R1CS.Circom (circomReindexMap)
import Circuit.Solver.Circom (CircomProgram, mkCircomProgram)
import Data.Field.Galois (GaloisField, Prime)
import Protolude

type Fr = Prime 21888242871839275222246405745257275088548364400416034343698204186575808495617

factorsE :: (GaloisField f, Hashable f) => ExprM f (Var Wire f Bool)
factorsE :: (GaloisField f, Hashable f) => ExprM f (Var Wire f 'TBool)
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, Hashable f) => Factors f
factors :: CircomProgram Fr
factors =
let BuilderState {..} = snd $ runCircuitBuilder (factorsE @f)
f = circomReindexMap bsVars
in Factors
{ factorsCircuit = reindex f bsCircuit,
factorsVars = reindex f bsVars
}
let BuilderState {..} = snd $ runCircuitBuilder factorsE
in mkCircomProgram bsVars bsCircuit
20 changes: 12 additions & 8 deletions factors/test/Main.hs
Original file line number Diff line number Diff line change
@@ -1,27 +1,31 @@
module Main (main) where

import Circuit (solve, lookupVar, assignInputs)
import Circuit (lookupVar)
import R1CS (Witness(..))
import R1CS.Circom (witnessFromCircomWitness)
import Circuit.Solver.Circom (CircomProgram(..), nativeGenWitness)
import qualified Data.Map as Map
import Protolude
import Test.Hspec
import Test.QuickCheck
import ZK.Factors (Factors (..), Fr, factors)
import ZK.Factors (factors)

main :: IO ()
main = hspec $ do
let circuit = factorsCircuit $ factors @Fr
vars = factorsVars $ factors @Fr
let vars = cpVars factors
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
let inputs = Map.fromList [("n", x * y), ("a", x), ("b", y)]
Witness w = witnessFromCircomWitness $
nativeGenWitness factors 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)]
w = solve vars circuit inputs
let inputs = Map.fromList [("n", z), ("a", x), ("b", y)]
Witness w = witnessFromCircomWitness $
nativeGenWitness factors inputs
in lookupVar vars "out" w == Just 0

0 comments on commit 05c89ca

Please sign in to comment.