added CircomProgram type

Author: martyall

Diff for: arithmetic-circuits.cabal

@@ -44,6 +44,7 @@ common deps
   build-depends:
       aeson           >=1.4
     , base            >=4.10  && <5
+    , binary          >=0.8.9 && <0.9
     , containers      >=0.6.0
     , filepath        >=1.4.2
     , finite-typelits >=0.1.0
@@ -111,6 +112,7 @@ library circom-compat
   hs-source-dirs:     circom-compat/src
   build-depends:
       arithmetic-circuits
+    , arithmetic-circuits:language
     , binary
     , bytestring
     , vector

Diff for: cabal.project

@@ -13,7 +13,7 @@ source-repository-package
 source-repository-package
   type: git
   location: https://github.com/l-adic/galois-fields.git
-  tag: b0867ffdebda5043c80315a51b15e82ed25acba6
+  tag: 33ee3d68dc9c118e88e8842d9f423a9f4f9851cf
   --sha256: j/zGFd2aeowzJfgCCBmJYmG8mDsfF0irqj/cPOw9ulE=
 
 source-repository-package

Diff for: circom-compat/app/Main.hs

@@ -2,24 +2,26 @@ module Main where
 
 import Circuit
 import Circuit.Language
-import Data.Binary (encodeFile)
+import Circuit.Solver.Circom (CircomProgram (..), mkCircomProgram, nativeGenWitness)
+import Data.Binary (encodeFile, decodeFile)
 import Data.Field.Galois (Prime)
-import Data.IntMap qualified as IntMap
-import Data.IntSet qualified as IntSet
+import Data.Map qualified as Map
 import Protolude
-import R1CS (Inputs (..), calculateWitness, isValidWitness)
-import R1CS.Circom (r1csToCircomR1CS, witnessToCircomWitness)
+import R1CS (toR1CS)
+import R1CS.Circom (r1csToCircomR1CS)
 
 main :: IO ()
 main = do
   let BuilderState {..} = snd $ runCircuitBuilder program
-      publicInputs = IntMap.fromList $ zip (IntSet.toAscList $ cvPublicInputs bsVars) [6]
-      privateInputs = IntMap.fromList $ zip (IntSet.toAscList $ cvPrivateInputs bsVars) [2, 3]
-      inputs = publicInputs <> privateInputs
-      (r1cs, wtns) = calculateWitness bsVars bsCircuit (Inputs inputs)
-  unless (isValidWitness wtns r1cs) $ panic "Invalid witness"
-  encodeFile "circom-compat/examples/factors/circuit.r1cs" $ r1csToCircomR1CS r1cs
-  encodeFile "circom-compat/examples/factors/witness.wtns" $ witnessToCircomWitness wtns
+      prog = mkCircomProgram bsVars bsCircuit
+      r1cs = r1csToCircomR1CS $ toR1CS (cpVars prog) (cpCircuit prog)
+      inputs = Map.fromList [("n", 6), ("a", 2), ("b", 3)]
+      wtns = nativeGenWitness prog inputs
+  encodeFile "circom-compat/examples/factors/circuit.r1cs" r1cs
+  encodeFile "circom-compat/examples/factors/circuit.bin" prog
+  encodeFile "circom-compat/examples/factors/witness.wtns" wtns
+  prog' <- decodeFile "circom-compat/examples/factors/circuit.bin"
+  print $ nativeGenWitness prog' inputs == wtns
 
 type Fr = Prime 21888242871839275222246405745257275088548364400416034343698204186575808495617
 

Diff for: circom-compat/examples/factors/circuit.bin

@@ -1,5 +1,9 @@
 module Circuit.Solver.Circom
-  ( ProgramEnv (..),
+  ( CircomProgram,
+    cpVars,
+    cpCircuit,
+    mkCircomProgram,
+    ProgramEnv (..),
     mkProgramEnv,
     ProgramState (..),
     mkProgramState,
@@ -15,11 +19,12 @@ module Circuit.Solver.Circom
     _setInputSignal,
     _getWitnessSize,
     _getWitness,
-    standardSolver,
+    nativeGenWitness,
   )
 where
 
 import Circuit
+import Data.Binary (Binary)
 import Data.Field.Galois (GaloisField, PrimeField (fromP), char)
 import Data.IORef (IORef, readIORef, writeIORef)
 import Data.IntMap qualified as IntMap
@@ -31,9 +36,28 @@ import Data.Vector.Mutable qualified as MV
 import FNV (FNVHash (..), hashText, mkFNV)
 import Protolude
 import R1CS (Inputs (..), Witness (..), oneVar)
-import R1CS.Circom (CircomWitness, FieldSize (..), integerFromLittleEndian, integerToLittleEndian, n32, witnessToCircomWitness)
+import R1CS.Circom (CircomWitness, FieldSize (..), circomReindexMap, integerFromLittleEndian, integerToLittleEndian, n32, witnessToCircomWitness)
 import Text.PrettyPrint.Leijen.Text (Pretty (pretty), (<+>))
 
+data CircomProgram f = CircomProgram
+  { cpVars :: CircuitVars Text,
+    cpCircuit :: ArithCircuit f
+  }
+  deriving (Generic)
+
+instance (Binary f) => Binary (CircomProgram f)
+
+mkCircomProgram ::
+  CircuitVars Text ->
+  ArithCircuit f ->
+  CircomProgram f
+mkCircomProgram vars circ =
+  let f = circomReindexMap vars
+   in CircomProgram
+        { cpVars = reindex f vars,
+          cpCircuit = reindex f circ
+        }
+
 -- WASM Solver
 
 data ProgramEnv f = ProgramEnv
@@ -49,10 +73,9 @@ data ProgramEnv f = ProgramEnv
 mkProgramEnv ::
   forall f.
   (GaloisField f) =>
-  CircuitVars Text ->
-  ArithCircuit f ->
+  CircomProgram f ->
   ProgramEnv f
-mkProgramEnv vars circ =
+mkProgramEnv CircomProgram {cpVars = vars, cpCircuit = circ} =
   ProgramEnv
     { peFieldSize = FieldSize 32,
       peRawPrime = toInteger $ char (1 :: f),
@@ -163,22 +186,21 @@ _getWitness env stRef i = do
 --------------------------------------------------------------------------------
 -- Standard Solver (to be used as native executable)
 
-standardSolver ::
+nativeGenWitness ::
   forall f.
   (PrimeField f) =>
-  CircuitVars Text ->
-  ArithCircuit f ->
+  CircomProgram f ->
   Map Text f ->
   CircomWitness f
-standardSolver vars circ inputs =
+nativeGenWitness CircomProgram {cpVars = vars, cpCircuit = circ} inputs =
   let initAssignments = assignInputs vars inputs
       wtns =
         evalArithCircuit
           (\w a -> IntMap.lookup (wireName w) a)
           (\w a -> safeAssign (wireName w) a)
           circ
           initAssignments
-   in witnessToCircomWitness $ Witness $ IntMap.insert oneVar 1 wtns
+   in witnessToCircomWitness $ Witness wtns
 
 --------------------------------------------------------------------------------
 

Diff for: circom-compat/examples/factors/circuit.r1cs

@@ -28,7 +28,7 @@ import Data.IntSet qualified as IntSet
 import Data.Vector (Vector)
 import Data.Vector qualified as V
 import Protolude
-import R1CS (LinearPoly (..), R1C (..), R1CS (..), Witness (..))
+import R1CS (LinearPoly (..), R1C (..), R1CS (..), Witness (..), oneVar)
 import Prelude (fail)
 
 --------------------------------------------------------------------------------
@@ -343,22 +343,23 @@ data CircomWitness f = CircomWitness
   deriving (Show, Eq)
 
 witnessToCircomWitness :: forall f. (PrimeField f) => Witness f -> CircomWitness f
-witnessToCircomWitness (Witness m) =
-  CircomWitness
-    { wtnsPreamble =
-        Preamble
-          { magic = 0x736e7477,
-            version = 1,
-            nSections = 2
-          },
-      wtnsHeader =
-        WitnessHeader
-          { whFieldSize = FieldSize 32,
-            whPrime = fromIntegral $ char (1 :: f),
-            whWitnessSize = fromIntegral $ IntMap.size m
-          },
-      wtnsValues = snd <$> IntMap.toAscList m
-    }
+witnessToCircomWitness (Witness _m) =
+  let m = IntMap.insert oneVar 1 _m
+   in CircomWitness
+        { wtnsPreamble =
+            Preamble
+              { magic = 0x736e7477,
+                version = 1,
+                nSections = 2
+              },
+          wtnsHeader =
+            WitnessHeader
+              { whFieldSize = FieldSize 32,
+                whPrime = fromIntegral $ char (1 :: f),
+                whWitnessSize = fromIntegral $ IntMap.size m
+              },
+          wtnsValues = snd <$> IntMap.toAscList m
+        }
 
 witnessFromCircomWitness :: CircomWitness f -> Witness f
 witnessFromCircomWitness (CircomWitness {wtnsValues}) =

Diff for: circom-compat/examples/factors/witness.wtns

@@ -11,6 +11,7 @@ module Circuit.Affine
 where
 
 import Data.Aeson (FromJSON, ToJSON)
+import Data.Binary (Binary)
 import Data.Map qualified as Map
 import Protolude
 import Text.PrettyPrint.Leijen.Text
@@ -30,6 +31,8 @@ data AffineCircuit f i
   | Var i
   deriving (Read, Eq, Ord, Show, Generic, NFData)
 
+instance (Binary i, Binary f) => Binary (AffineCircuit f i)
+
 instance (FromJSON i, FromJSON f) => FromJSON (AffineCircuit f i)
 
 instance (ToJSON i, ToJSON f) => ToJSON (AffineCircuit f i)

Diff for: circom-compat/src/Circuit/Solver/Circom.hs

@@ -31,6 +31,7 @@ import Circuit.Affine
     evalAffineCircuit,
   )
 import Data.Aeson (FromJSON, ToJSON)
+import Data.Binary (Binary)
 import Data.Field.Galois (PrimeField, fromP)
 import Data.IntMap qualified as IntMap
 import Data.IntSet qualified as IntSet
@@ -54,6 +55,8 @@ instance FromJSON InputType
 
 instance ToJSON InputType
 
+instance Binary InputType
+
 -- | Wires are can be labeled in the ways given in this data type
 data Wire
   = InputWire Text InputType Int
@@ -68,6 +71,8 @@ instance ToJSON Wire
 instance Hashable Wire where
   hashWithSalt s w = s `hashWithSalt` (0 :: Int) `hashWithSalt` (wireName w)
 
+instance Binary Wire
+
 instance Pretty Wire where
   pretty (InputWire label t v) =
     let a = case t of
@@ -109,6 +114,8 @@ deriving instance Foldable (Gate f)
 
 deriving instance Traversable (Gate f)
 
+instance (Binary i, Binary f) => Binary (Gate f i)
+
 instance Bifunctor Gate where
   bimap f g = \case
     Mul l r o -> Mul (bimap f g l) (bimap f g r) (g o)
@@ -211,6 +218,8 @@ instance (FromJSON f) => FromJSON (ArithCircuit f)
 
 instance (ToJSON f) => ToJSON (ArithCircuit f)
 
+instance (Binary f) => Binary (ArithCircuit f)
+
 instance Functor ArithCircuit where
   fmap f (ArithCircuit gates) = ArithCircuit $ map (first f) gates
 
@@ -287,7 +296,9 @@ data CircuitVars label = CircuitVars
     cvOutputs :: IntSet,
     cvInputsLabels :: InputBidings label
   }
-  deriving (Show)
+  deriving (Show, Generic, NFData)
+
+instance (Binary label) => Binary (CircuitVars label)
 
 instance (Pretty label) => Pretty (CircuitVars label) where
   pretty CircuitVars {cvVars, cvPrivateInputs, cvPublicInputs, cvOutputs, cvInputsLabels} =
@@ -392,7 +403,9 @@ data InputBidings label = InputBidings
   { labelToVar :: Map label Int,
     varToLabel :: IntMap label
   }
-  deriving (Show)
+  deriving (Show, Generic, NFData)
+
+instance (Binary label) => Binary (InputBidings label)
 
 mapLabels :: (Ord l2) => (l1 -> l2) -> InputBidings l1 -> InputBidings l2
 mapLabels f InputBidings {labelToVar, varToLabel} =