|
| 1 | +module Circom.CLI (defaultMain) where |
| 2 | + |
| 3 | +import Circom.R1CS (r1csToCircomR1CS) |
| 4 | +import Circom.Solver (CircomProgram (..), mkCircomProgram, nativeGenWitness) |
| 5 | +import Circuit.Arithmetic (CircuitVars (cvInputsLabels, cvOutputs), InputBindings (labelToVar), restrictVars) |
| 6 | +import Circuit.Dataflow qualified as DataFlow |
| 7 | +import Circuit.Dot (arithCircuitToDot) |
| 8 | +import Circuit.Language.Compile (BuilderState (..), ExprM, runCircuitBuilder) |
| 9 | +import Data.Aeson (decodeFileStrict) |
| 10 | +import Data.Aeson qualified as A |
| 11 | +import Data.Binary (decodeFile, encodeFile) |
| 12 | +import Data.Field.Galois (PrimeField (fromP)) |
| 13 | +import Data.IntSet qualified as IntSet |
| 14 | +import Data.Text qualified as Text |
| 15 | +import Options.Applicative (CommandFields, Mod, Parser, ParserInfo, command, execParser, fullDesc, header, help, helper, hsubparser, info, long, progDesc, showDefault, strOption, switch, value) |
| 16 | +import Protolude |
| 17 | +import R1CS (toR1CS) |
| 18 | +import System.Directory (createDirectoryIfMissing) |
| 19 | + |
| 20 | +data GlobalOpts = GlobalOpts |
| 21 | + { outputDir :: FilePath, |
| 22 | + cmd :: Command |
| 23 | + } |
| 24 | + |
| 25 | +optsParser :: Text -> ParserInfo GlobalOpts |
| 26 | +optsParser progName = |
| 27 | + info |
| 28 | + (helper <*> globalOptsParser) |
| 29 | + ( fullDesc |
| 30 | + <> progDesc ("Compiling " <> Text.unpack progName <> " to a zk-SNARK") |
| 31 | + <> header ("Compile " <> Text.unpack progName <> " to a system of constraints and solve for a witness") |
| 32 | + ) |
| 33 | + where |
| 34 | + globalOptsParser :: Parser GlobalOpts |
| 35 | + globalOptsParser = |
| 36 | + GlobalOpts |
| 37 | + <$> strOption |
| 38 | + ( long "output-dir" |
| 39 | + <> help "output directory" |
| 40 | + <> showDefault |
| 41 | + <> value "circuit-output" |
| 42 | + ) |
| 43 | + <*> hsubparser (compileCommand <> solveCommand) |
| 44 | + |
| 45 | + compileCommand :: Mod CommandFields Command |
| 46 | + compileCommand = |
| 47 | + command "compile" (info (Compile <$> compileOptsParser) (progDesc "Compile the program to an r1cs and constraint system")) |
| 48 | + |
| 49 | + solveCommand :: Mod CommandFields Command |
| 50 | + solveCommand = |
| 51 | + command "solve" (info (Solve <$> solveOptsParser) (progDesc "Generate a witness")) |
| 52 | + |
| 53 | +data Command |
| 54 | + = Compile CompileOpts |
| 55 | + | Solve SolveOpts |
| 56 | + |
| 57 | +data CompileOpts = CompileOpts |
| 58 | + { coOptimizeOpts :: OptimizeOpts, |
| 59 | + coGenInputsTemplate :: Bool, |
| 60 | + coGenDotFile :: Bool, |
| 61 | + coIncludeJson :: Bool |
| 62 | + } |
| 63 | + |
| 64 | +compileOptsParser :: Parser CompileOpts |
| 65 | +compileOptsParser = |
| 66 | + CompileOpts |
| 67 | + <$> optimizeOptsParser |
| 68 | + <*> switch |
| 69 | + ( long "inputs-template" |
| 70 | + <> help "generate a template json file for the inputs" |
| 71 | + ) |
| 72 | + <*> switch |
| 73 | + ( long "dot" |
| 74 | + <> help "generate a dot file for the circuit" |
| 75 | + ) |
| 76 | + <*> switch |
| 77 | + ( long "json" |
| 78 | + <> help "also write json versions of artifacts" |
| 79 | + ) |
| 80 | + |
| 81 | +data OptimizeOpts = OptimizeOpts |
| 82 | + { removeUnreachable :: Bool |
| 83 | + } |
| 84 | + |
| 85 | +optimizeOptsParser :: Parser OptimizeOpts |
| 86 | +optimizeOptsParser = |
| 87 | + OptimizeOpts |
| 88 | + <$> switch |
| 89 | + ( long "remove-unreachable" |
| 90 | + <> help "detect and remove variables not contributing to the output" |
| 91 | + ) |
| 92 | + |
| 93 | +data SolveOpts = SolveOpts |
| 94 | + { soInputsFile :: FilePath, |
| 95 | + soIncludeJson :: Bool |
| 96 | + } |
| 97 | + |
| 98 | +solveOptsParser :: Parser SolveOpts |
| 99 | +solveOptsParser = |
| 100 | + SolveOpts |
| 101 | + <$> strOption |
| 102 | + ( long "inputs" |
| 103 | + <> help "inputs json file" |
| 104 | + <> showDefault |
| 105 | + <> value "inputs.json" |
| 106 | + ) |
| 107 | + <*> switch |
| 108 | + ( long "json" |
| 109 | + <> help "also write json versions of artifacts" |
| 110 | + ) |
| 111 | + |
| 112 | +defaultMain :: |
| 113 | + forall f a. |
| 114 | + (PrimeField f) => |
| 115 | + Text -> |
| 116 | + ExprM f a -> |
| 117 | + IO () |
| 118 | +defaultMain progName program = do |
| 119 | + opts <- execParser (optsParser progName) |
| 120 | + let outDir = outputDir opts |
| 121 | + case cmd opts of |
| 122 | + Compile compilerOpts -> do |
| 123 | + let BuilderState {..} = snd $ runCircuitBuilder program |
| 124 | + prog = optimize (coOptimizeOpts compilerOpts) $ mkCircomProgram bsVars bsCircuit |
| 125 | + r1cs = r1csToCircomR1CS $ toR1CS (cpVars prog) (cpCircuit prog) |
| 126 | + createDirectoryIfMissing True outDir |
| 127 | + encodeFile (r1csFilePath outDir) r1cs |
| 128 | + encodeFile (binFilePath outDir) prog |
| 129 | + when (coGenInputsTemplate compilerOpts) $ do |
| 130 | + let inputsTemplate = map (const A.Null) $ labelToVar $ cvInputsLabels $ cpVars prog |
| 131 | + A.encodeFile (inputsTemplateFilePath outDir) inputsTemplate |
| 132 | + when (coIncludeJson compilerOpts) $ do |
| 133 | + A.encodeFile (r1csFilePath outDir <> ".json") (map fromP r1cs) |
| 134 | + A.encodeFile (binFilePath outDir <> ".json") (map fromP prog) |
| 135 | + when (coGenDotFile compilerOpts) $ do |
| 136 | + writeFile (dotFilePath outDir) $ arithCircuitToDot (cpCircuit prog) |
| 137 | + Solve solveOpts -> do |
| 138 | + inputs <- do |
| 139 | + mInputs <- decodeFileStrict (soInputsFile solveOpts) |
| 140 | + maybe (panic "Failed to decode inputs") (pure . map (fromInteger @f)) mInputs |
| 141 | + circuit <- decodeFile (binFilePath outDir) |
| 142 | + let wtns = nativeGenWitness circuit inputs |
| 143 | + encodeFile (witnessFilePath outDir) wtns |
| 144 | + when (soIncludeJson solveOpts) $ do |
| 145 | + A.encodeFile (witnessFilePath outDir <> ".json") (map fromP wtns) |
| 146 | + where |
| 147 | + baseFilePath :: FilePath -> FilePath |
| 148 | + baseFilePath dir = dir <> "/" <> Text.unpack progName |
| 149 | + inputsTemplateFilePath dir = dir <> "/" <> "inputs-template.json" |
| 150 | + binFilePath dir = baseFilePath dir <> ".bin" |
| 151 | + r1csFilePath dir = baseFilePath dir <> ".r1cs" |
| 152 | + witnessFilePath dir = baseFilePath dir <> ".wtns" |
| 153 | + dotFilePath dir = baseFilePath dir <> ".dot" |
| 154 | + |
| 155 | +optimize :: |
| 156 | + forall f. |
| 157 | + (Ord f) => |
| 158 | + OptimizeOpts -> |
| 159 | + CircomProgram f -> |
| 160 | + CircomProgram f |
| 161 | +optimize opts = |
| 162 | + appEndo . mconcat $ |
| 163 | + [ performRemoveUnreachable |
| 164 | + ] |
| 165 | + where |
| 166 | + performRemoveUnreachable :: Endo (CircomProgram f) |
| 167 | + performRemoveUnreachable = |
| 168 | + if (removeUnreachable opts) |
| 169 | + then Endo $ \prog -> |
| 170 | + let outVars :: [Int] |
| 171 | + outVars = IntSet.toList $ cvOutputs $ cpVars prog |
| 172 | + (newCircuit, usedVars) = DataFlow.removeUnreachable outVars (cpCircuit prog) |
| 173 | + newVars = restrictVars (cpVars prog) usedVars |
| 174 | + in mkCircomProgram newVars newCircuit |
| 175 | + else mempty |
0 commit comments