Merge pull request #5 from l-adic/circom-program

Circom program

.gitignore

@@ -2,6 +2,7 @@
 dist-newstyle
 www/circuit_final.zkey
 www/circuit.wasm
+www/circuit.bin
 output
 .spago
 .purs-repl

.parcelrc

@@ -7,6 +7,9 @@
     "*.wasm": [
       "@parcel/transformer-raw"
     ],
+    "*.bin": [
+      "@parcel/transformer-raw"
+    ],
     "*.zkey": [
       "@parcel/transformer-raw"
     ]

README.md

@@ -26,19 +26,30 @@ You should have a local ethereum node with an unlocked default account and the w
 ## Contents
 
 ### The factors zk program
-A ZK program written in a Haskell DSL that expresses a factorization of a public input `n` into a product of secret inputs `a` and `b`. You can produce a circom compatible `r1cs` file for this program by running 
+A ZK program written in a Haskell DSL that expresses a factorization of a public input `n` into a product of secret inputs `a` and `b`. The factorization must be non-trivial, i.e. `a /= 1 && b /= 1`.
+
+You can produce a circom compatible `r1cs` file for this program by running 
+
+```
+> cabal run factors-cli -- compile --output-dir trusted-setup 
+```
+
+You should see the artifacts 
 
 ```
-> cabal run factors
+trusted-setup
+├── circuit.bin
+├── circuit.r1cs
+└ ...
 ```
 
-You should see an artifact `trusted-setup/circuit.r1cs`.
+The `circuit.r1cs` file is the R1CS that is expected by snarkjs for proving/verification key generation. The `circuit.bin` is the binary serialization of the constraints represented by the compiled circuit. This file is required in order to evaluate the circuit, i.e. generate a witness.
 
 ### A factors program constraint solver
 A constraint solver applied to the `factors` program. You can produce a circom compatible WASM binary for this solver by running
 
 ```
-> cd factors-solver
+> cd wasm-solver
 > ./build-wasm
 ```
 
@@ -68,10 +79,10 @@ You can comple the contracts, build the purescript ffi, and deploy this smart co
 ```
 
 ### A frontend application
-Assuming you have done the previous steps, copy the proving key to the `www` folder
+Assuming you have done the previous steps, copy the proving key and the compiled circuit to the `www` folder
 
 ```
-> cp trusted-setup/circuit_final.zkey www
+> cp trusted-setup/circuit_final.zkey trusted-setup/circuit.bin www
 ```
 
 You should see the `circuit.wasm` solver binary is already there. Assuming you have deployed the verifying contract, you can start the frontend:

app/Prover/Prove.js

@@ -1,13 +1,33 @@
-import { WASI } from "@bjorn3/browser_wasi_shim/dist";
+import { WASI, PreopenDirectory, File, OpenFile, ConsoleStdout } from "@bjorn3/browser_wasi_shim/dist";
 import { groth16, wtns } from "snarkjs";
 
+async function load_external_file(path) {
+  const response = await fetch(path);
+  const buffer = await response.arrayBuffer();
+  return new File(buffer);
+}
 
 async function _fullProve(input) {
   const wasmFile = "circuit.wasm";
   const zkeyFile = "circuit_final.zkey";
-  const wasi = new WASI([], [], []);
-  let options = { additionalImports: { wasi_snapshot_preview1: wasi.wasiImport }};
-  const w= {
+  let fds = [
+    new OpenFile(new File([])), // stdin
+    ConsoleStdout.lineBuffered(msg => console.log(`[WASI stdout] ${msg}`)),
+    ConsoleStdout.lineBuffered(msg => console.warn(`[WASI stderr] ${msg}`)),
+    new PreopenDirectory("/", [
+      ["circuit.bin", await load_external_file("circuit.bin")]
+    ])
+  ];
+  const wasi = new WASI([], [], fds, { debug: true });
+  let options = {
+    initializeWasiReactorModuleInstance: (instance) => {
+      wasi.initialize(instance);
+    },
+    additionalWASMImports: {
+      wasi_snapshot_preview1: wasi.wasiImport
+    }
+  };
+  const w = {
         type: "mem"
     };
   await wtns.calculate(input, wasmFile, w, options);

cabal.project

@@ -19,15 +19,13 @@ source-repository-package
 source-repository-package
   type: git
   location: https://github.com/l-adic/galois-fields.git
-  tag: b0867ffdebda5043c80315a51b15e82ed25acba6
-  --sha256: pYe2FTNHPTzZeTnOMe6S9eh3EOY6Hi6PjdfsNjPSOZQ=
+  tag: 525521de7b985364f7e0c32222fc3b21fea8e530
+  --sha256: hPbO7PElCJ3X6+WibL0EmdPlZqLq6stjn2r5auhsv08=
 
 source-repository-package
   type: git
   location: https://github.com/l-adic/arithmetic-circuits.git
-  tag: d243f4cd91fb0adae11c18c726ef884cf7ea7d0d
-  --sha256: cmgHbYgMfPCjtZiLqqKMrvL+D8kIPGN9sE07iVqBS5Q=
-
-index-state: 2023-10-15T12:29:38Z
-
+  tag: 77415e01245ff6cc3cc60e9062dcf3e986b9811f
+  --sha256: jI3tAEGwOBqiCr6JqQfAws3X2RIp1eYbI9fXWutTMuE=
 
+index-state: 2024-05-21T06:16:08Z

factors/cli/Main.hs

@@ -0,0 +1,10 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Main where
+
+import Circom.CLI (defaultMain)
+import Protolude
+import ZK.Factors (Fr, factors)
+
+main :: IO ()
+main = defaultMain "circuit" $ factors @Fr

factors/factors.cabal

@@ -13,6 +13,7 @@ common extensions
     DataKinds
     TypeApplications
     NoImplicitPrelude
+    NamedFieldPuns
     RecordWildCards
     OverloadedStrings
 
@@ -34,16 +35,13 @@ library
   hs-source-dirs:   src
   default-language: GHC2021
 
-executable factors
+executable factors-cli
   import:           warnings, extensions, deps
   main-is:          Main.hs
   build-depends:
-      binary
-    , factors
-    , aeson
-    , wl-pprint-text  >=1.2.0
+      factors
 
-  hs-source-dirs:   app
+  hs-source-dirs:   cli
   default-language: GHC2021
 
 test-suite factors-test
@@ -53,6 +51,7 @@ test-suite factors-test
   hs-source-dirs:   test
   main-is:          Main.hs
   build-depends:
+      binary
     , factors
     , hspec
     , QuickCheck

factors/src/ZK/Factors.hs

@@ -2,37 +2,26 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module ZK.Factors
-  ( Factors (..),
-    factors,
+  ( factors,
     Fr,
   )
 where
 
 import Circuit
 import Circuit.Language
-import R1CS.Circom (circomReindexMap)
 import Data.Field.Galois (GaloisField, Prime)
 import Protolude
 
 type Fr = Prime 21888242871839275222246405745257275088548364400416034343698204186575808495617
 
-factorsE :: (GaloisField f, Hashable f) => ExprM f (Var Wire f Bool)
-factorsE = do
-  n <- var_ <$> fieldInput Public "n"
+factors :: (GaloisField f, Hashable f) => ExprM f (Var Wire f 'TBool)
+factors = do
   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 =
-  let BuilderState {..} = snd $ runCircuitBuilder (factorsE @f)
-      f = circomReindexMap bsVars
-   in Factors
-        { factorsCircuit = reindex f bsCircuit,
-          factorsVars = reindex f bsVars
-        }
+  n <- var_ <$> fieldInput Public "n"
+  let cs =
+        [ neq_ n a,
+          neq_ n b,
+          eq_ n (a * b)
+        ]
+  boolOutput "out" $ unAnd_ $ foldMap And_ cs

factors/test/Main.hs

@@ -1,27 +1,49 @@
 module Main (main) where
 
-import Circuit (solve, lookupVar, assignInputs)
+import Circom.R1CS (witnessFromCircomWitness)
+import Circom.Solver (CircomProgram (..), mkCircomProgram, nativeGenWitness)
+import Circuit
+import Circuit.Language
 import qualified Data.Map as Map
 import Protolude
+import R1CS (Witness (..))
 import Test.Hspec
 import Test.QuickCheck
-import ZK.Factors (Factors (..), Fr, factors)
+import ZK.Factors (Fr, factors)
+import Data.Binary (encode, decode)
 
 main :: IO ()
 main = hspec $ do
-  let circuit = factorsCircuit $ factors @Fr
-      vars = factorsVars $ factors @Fr
+  let BuilderState {bsVars, bsCircuit} = snd $ runCircuitBuilder (factors @Fr)
+      program = mkCircomProgram bsVars bsCircuit
+      vars = cpVars program
   describe "Factors" $ do
-    it "should accept valid factors" $ do
+    it "can serialize/deserialize the program" $ do
+      let a = decode (encode program)
+      cpCircuit a `shouldBe` cpCircuit program
+
+    it "should accept valid factorizations" $
       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
+          (x /= 1 && y /= 1) ==>
+            let inputs = Map.fromList [("n", x * y), ("a", x), ("b", y)]
+                Witness w =
+                  witnessFromCircomWitness $
+                    nativeGenWitness program inputs
+             in lookupVar vars "out" w === Just 1
+    it "shouldn't accept trivial factorizations" $
+      property $ \x ->
+        let inputs = Map.fromList [("n", x), ("a", 1), ("b", x)]
+            Witness w =
+              witnessFromCircomWitness $
+                nativeGenWitness program inputs
+         in lookupVar vars "out" w == Just 0
+    it "shouldn't accept invalid factorizations" $
       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
+            let inputs = Map.fromList [("n", z), ("a", x), ("b", y)]
+                Witness w =
+                  witnessFromCircomWitness $
+                    nativeGenWitness program inputs
+             in lookupVar vars "out" w == Just 0

flake.nix

@@ -41,7 +41,7 @@
         );
         defaultGHC = perGHC.${defaultGHCVersion};
 
-        ormoluLive = import factors-solver/default.nix {
+        wasmSolver = import wasm-solver/default.nix {
           inherit pkgs inputs defaultGHC;
         };
       in
@@ -63,8 +63,8 @@
             withHoogle = false;
             exactDeps = false;
           };
-          ormoluLive = ormoluLive.shell;
-          ghcWasm = ormoluLive.ghcWasmShell;
+          wasmSolver = wasmSolver.shell;
+          ghcWasm = wasmSolver.ghcWasmShell;
         };
         legacyPackages = defaultGHC // perGHC;
       });