circom/src/compiler.js
src/compiler.jsRaw
1/*
2 Copyright 2018 0KIMS association.
3
4 This file is part of circom (Zero Knowledge Circuit Compiler).
5
6 circom is a free software: you can redistribute it and/or modify it
7 under the terms of the GNU General Public License as published by
8 the Free Software Foundation, either version 3 of the License, or
9 (at your option) any later version.
10
11 circom is distributed in the hope that it will be useful, but WITHOUT
12 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 License for more details.
15
16 You should have received a copy of the GNU General Public License
17 along with circom. If not, see <https://www.gnu.org/licenses/>.
18*/
19
20const fs = require("fs");
21const path = require("path");
22const bigInt = require("big-integer");
23const __P__ = new bigInt("21888242871839275222246405745257275088548364400416034343698204186575808495617");
24const __MASK__ = new bigInt(2).pow(253).minus(1);
25const assert = require("assert");
26const gen = require("./gencode");
27const exec = require("./exec");
28const lc = require("./lcalgebra");
29
30module.exports = compile;
31
32const parser = require("../parser/jaz.js").parser;
33
34const timeout = ms => new Promise(res => setTimeout(res, ms));
35
36async function compile(srcFile, options) {
37 if (!options) {
38 options = {};
39 }
40 if (typeof options.reduceConstraints === "undefined") {
41 options.reduceConstraints = true;
42 }
43 const fullFileName = srcFile;
44 const fullFilePath = path.dirname(fullFileName);
45
46 const src = fs.readFileSync(fullFileName, "utf8");
47 const ast = parser.parse(src);
48
49 assert(ast.type == "BLOCK");
50
51 const ctx = {
52 scopes: [{}],
53 signals: {
54 one: {
55 fullName: "one",
56 value: bigInt(1),
57 equivalence: "",
58 direction: ""
59 }
60 },
61 currentComponent: "",
62 constraints: [],
63 components: {},
64 templates: {},
65 functions: {},
66 functionParams: {},
67 filePath: fullFilePath,
68 fileName: fullFileName,
69 verbose: options.verbose || false
70 };
71
72
73 exec(ctx, ast);
74
75 if (!ctx.components["main"]) {
76 throw new Error("A main component must be defined");
77 }
78
79 if (ctx.verbose) console.log("Classify Signals");
80 classifySignals(ctx);
81
82 if (ctx.verbose) console.log("Reduce Constraints");
83 reduceConstants(ctx);
84 if (options.reduceConstraints) {
85
86 // Repeat while reductions are performed
87 let oldNConstrains = -1;
88 while (ctx.constraints.length != oldNConstrains) {
89 oldNConstrains = ctx.constraints.length;
90 reduceConstrains(ctx);
91 }
92 }
93
94 generateWitnessNames(ctx);
95
96 if (ctx.error) {
97 throw(ctx.error);
98 }
99
100 ctx.scopes = [{}];
101
102 const mainCode = gen(ctx,ast);
103 if (ctx.error) throw(ctx.error);
104
105 const def = buildCircuitDef(ctx, mainCode);
106
107 return def;
108}
109
110
111function classifySignals(ctx) {
112
113 function priorize(t1, t2) {
114 if ((t1 == "error") || (t2=="error")) return "error";
115 if (t1 == "internal") {
116 return t2;
117 } else if (t2=="internal") {
118 return t1;
119 }
120 if ((t1 == "one") || (t2 == "one")) return "one";
121 if ((t1 == "constant") || (t2 == "constant")) return "constant";
122 if (t1!=t2) return "error";
123 return t1;
124 }
125
126 // First classify the signals
127 for (let s in ctx.signals) {
128 const signal = ctx.signals[s];
129 let tAll = "internal";
130 let lSignal = signal;
131 let end = false;
132 while (!end) {
133 let t = lSignal.category || "internal";
134 if (s == "one") {
135 t = "one";
136 } else if (lSignal.value) {
137 t = "constant";
138 } else if (lSignal.component=="main") {
139 if (lSignal.direction == "IN") {
140 if (lSignal.private) {
141 t = "prvInput";
142 } else {
143 t = "pubInput";
144 }
145 } else if (lSignal.direction == "OUT") {
146 t = "output";
147 }
148 }
149 tAll = priorize(t,tAll);
150 if (lSignal.equivalence) {
151 lSignal = ctx.signals[lSignal.equivalence];
152 } else {
153 end=true;
154 }
155 }
156 if (tAll == "error") {
157 throw new Error("Incompatible types in signal: " + s);
158 }
159 lSignal.category = tAll;
160 }
161}
162
163
164function generateWitnessNames(ctx) {
165
166 const totals = {
167 "output": 0,
168 "pubInput": 0,
169 "one": 0,
170 "prvInput": 0,
171 "internal": 0,
172 "constant": 0,
173 };
174 const ids = {};
175
176 const counted = {};
177
178 // First classify the signals
179 for (let s in ctx.signals) {
180 const signal = ctx.signals[s];
181 let lSignal = signal;
182 while (lSignal.equivalence) lSignal = ctx.signals[lSignal.equivalence];
183
184 if (!counted[lSignal.fullName]) {
185 counted[lSignal.fullName] = true;
186 totals[lSignal.category] ++;
187 }
188 }
189
190 ids["one"] = 0;
191 ids["output"] = 1;
192 ids["pubInput"] = ids["output"] + totals["output"];
193 ids["prvInput"] = ids["pubInput"] + totals["pubInput"];
194 ids["internal"] = ids["prvInput"] + totals["prvInput"];
195 ids["constant"] = ids["internal"] + totals["internal"];
196 const nSignals = ids["constant"] + totals["constant"];
197
198 ctx.signalNames = new Array(nSignals);
199 for (let i=0; i< nSignals; i++) ctx.signalNames[i] = [];
200 ctx.signalName2Idx = {};
201
202 for (let s in ctx.signals) {
203 const signal = ctx.signals[s];
204 let lSignal = signal;
205 while (lSignal.equivalence) {
206 lSignal = ctx.signals[lSignal.equivalence];
207 }
208 if ( typeof(lSignal.id) === "undefined" ) {
209 lSignal.id = ids[lSignal.category] ++;
210 }
211
212 signal.id = lSignal.id;
213 ctx.signalNames[signal.id].push(signal.fullName);
214 ctx.signalName2Idx[signal.fullName] = signal.id;
215 }
216
217 ctx.totals = totals;
218}
219
220function reduceConstants(ctx) {
221 const newConstraints = [];
222 for (let i=0; i<ctx.constraints.length; i++) {
223 if ((ctx.verbose)&&(i%10000 == 0)) console.log("reducing constants: ", i);
224 const c = lc.canonize(ctx, ctx.constraints[i]);
225 if (!lc.isZero(c)) {
226 newConstraints.push(c);
227 }
228 }
229 ctx.constraints = newConstraints;
230}
231
232function reduceConstrains(ctx) {
233 indexVariables();
234 let possibleConstraints = Object.keys(ctx.constraints);
235 while (possibleConstraints.length>0) {
236 let nextPossibleConstraints = {};
237 for (let i in possibleConstraints) {
238 if ((ctx.verbose)&&(i%10000 == 0)) console.log("reducing constraints: ", i);
239 if (!ctx.constraints[i]) continue;
240 const c = ctx.constraints[i];
241
242 // Swap a and b if b has more variables.
243 if (Object.keys(c.b).length > Object.keys(c.a).length) {
244 const aux = c.a;
245 c.a=c.b;
246 c.b=aux;
247 }
248
249 // Mov to C if possible.
250 if (isConstant(c.a)) {
251 const ct = {type: "NUMBER", value: c.a.values["one"]};
252 c.c = lc.add(lc.mul(c.b, ct), c.c);
253 c.a = { type: "LINEARCOMBINATION", values: {} };
254 c.b = { type: "LINEARCOMBINATION", values: {} };
255 }
256 if (isConstant(c.b)) {
257 const ct = {type: "NUMBER", value: c.b.values["one"]};
258 c.c = lc.add(lc.mul(c.a, ct), c.c);
259 c.a = { type: "LINEARCOMBINATION", values: {} };
260 c.b = { type: "LINEARCOMBINATION", values: {} };
261 }
262
263 if (lc.isZero(c.a) || lc.isZero(c.b)) {
264 const isolatedSignal = getFirstInternalSignal(ctx, c.c);
265 if (isolatedSignal) {
266
267 let lSignal = ctx.signals[isolatedSignal];
268 while (lSignal.equivalence) {
269 lSignal = ctx.signals[lSignal.equivalence];
270 }
271
272
273 const isolatedSignalEquivalence = {
274 type: "LINEARCOMBINATION",
275 values: {}
276 };
277 const invCoef = c.c.values[isolatedSignal].modInv(__P__);
278 for (const s in c.c.values) {
279 if (s != isolatedSignal) {
280 const v = __P__.minus(c.c.values[s]).times(invCoef).mod(__P__);
281 if (!v.isZero()) {
282 isolatedSignalEquivalence.values[s] = v;
283 }
284 }
285 }
286
287 for (let j in lSignal.inConstraints) {
288 if ((j!=i)&&(ctx.constraints[j])) {
289 ctx.constraints[j] = lc.substitute(ctx.constraints[j], isolatedSignal, isolatedSignalEquivalence);
290 linkSignalsConstraint(j);
291 if (j<i) {
292 nextPossibleConstraints[j] = true;
293 }
294 }
295 }
296
297 ctx.constraints[i] = null;
298
299 lSignal.category = "constant";
300 } else {
301 if (lc.isZero(c.c)) ctx.constraints[i] = null;
302 }
303 }
304 }
305 possibleConstraints = Object.keys(nextPossibleConstraints);
306 }
307 unindexVariables();
308
309 // Pack the constraints
310 let o = 0;
311 for (let i=0; i<ctx.constraints.length; i++) {
312 if (ctx.constraints[i]) {
313 if (o != i) {
314 ctx.constraints[o] = ctx.constraints[i];
315 }
316 o++;
317 }
318 }
319 ctx.constraints.length = o;
320
321 function indexVariables() {
322 for (let i=0; i<ctx.constraints.length; i++) linkSignalsConstraint(i);
323 }
324
325 function linkSignalsConstraint(cidx) {
326 const ct = ctx.constraints[cidx];
327 for (let k in ct.a.values) linkSignal(k, cidx);
328 for (let k in ct.b.values) linkSignal(k, cidx);
329 for (let k in ct.c.values) linkSignal(k, cidx);
330 }
331
332 function unindexVariables() {
333 for (let s in ctx.signals) {
334 let lSignal = ctx.signals[s];
335 while (lSignal.equivalence) {
336 lSignal = ctx.signals[lSignal.equivalence];
337 }
338 if (lSignal.inConstraints) delete lSignal.inConstraints;
339 }
340 }
341
342/*
343 function unlinkSignal(signalName, cidx) {
344 let lSignal = ctx.signals[signalName];
345 while (lSignal.equivalence) {
346 lSignal = ctx.signals[lSignal.equivalence];
347 }
348 if ((lSignal.inConstraints)&&(lSignal.inConstraints[cidx])) {
349 delete lSignal.inConstraints[cidx];
350 }
351 }
352*/
353
354 function linkSignal(signalName, cidx) {
355 let lSignal = ctx.signals[signalName];
356 while (lSignal.equivalence) {
357 lSignal = ctx.signals[lSignal.equivalence];
358 }
359 if (!lSignal.inConstraints) lSignal.inConstraints = {};
360 lSignal.inConstraints[cidx] = true;
361 }
362
363 function getFirstInternalSignal(ctx, l) {
364 for (let k in l.values) {
365 const signal = ctx.signals[k];
366 if (signal.category == "internal") return k;
367 }
368 return null;
369 }
370
371 function isConstant(l) {
372 for (let k in l.values) {
373 if ((k != "one") && (!l.values[k].isZero())) return false;
374 }
375 if (!l.values["one"] || l.values["one"].isZero()) return false;
376 return true;
377 }
378
379}
380
381
382function buildCircuitDef(ctx, mainCode) {
383 const res = {
384 mainCode: mainCode
385 };
386 res.signalName2Idx = ctx.signalName2Idx;
387
388 res.components = [];
389 res.componentName2Idx = {};
390 for (let c in ctx.components) {
391 const idCoponent = res.components.length;
392 res.components.push({
393 name: c,
394 params: ctx.components[c].params,
395 template: ctx.components[c].template,
396 inputSignals: 0
397 });
398 res.componentName2Idx[c] = idCoponent;
399 }
400
401 res.signals = new Array(ctx.signalNames.length);
402 for (let i=0; i<ctx.signalNames.length; i++) {
403 res.signals[i] = {
404 names: ctx.signalNames[i],
405 triggerComponents: []
406 };
407 ctx.signalNames[i].map( (fullName) => {
408 const idComponet = res.componentName2Idx[ctx.signals[fullName].component];
409 if (ctx.signals[fullName].direction == "IN") {
410 res.signals[i].triggerComponents.push(idComponet);
411 res.components[idComponet].inputSignals++;
412 }
413 });
414 }
415
416 res.constraints = buildConstraints(ctx);
417
418 res.templates = ctx.templates;
419
420 res.functions = {};
421 for (let f in ctx.functions) {
422 res.functions[f] = {
423 params: ctx.functionParams[f],
424 func: ctx.functions[f]
425 };
426 }
427
428 res.nPrvInputs = ctx.totals.prvInput;
429 res.nPubInputs = ctx.totals.pubInput;
430 res.nInputs = res.nPrvInputs + res.nPubInputs;
431 res.nOutputs = ctx.totals.output;
432 res.nVars = res.nInputs + res.nOutputs + ctx.totals.one + ctx.totals.internal;
433 res.nConstants = ctx.totals.constant;
434 res.nSignals = res.nVars + res.nConstants;
435
436 return res;
437}
438
439/*
440 Build constraints
441
442A constraint like this
443
444 [s1 + 2*s2 + 3*s3] * [ s2 + 5*s4] - [s0 ] = 0
445 [ 5*s2 + 6*s3] * [ s2 + ] - [s0 + 2* s2] = 0
446 [s1 + s3] * [ s2 + 5*s3] - [s4 ] = 0
447
448is converted to
449
450[
451 [{"1":"1","2":"2","3":"3"} , {"2":"1","4":"5"} , {"0":"1" }],
452 [{ "2":"5","3":"6"} , {"2":"1" } , {"0":"1", "2":"2"}],
453 [{"1":"1", "3":"1"} , {"2":"1","3":"5"} , {"4":"1" }]
454]
455 ^ ^ ^
456 | | |
457 A B C
458
459*/
460
461function buildConstraints(ctx) {
462 const res = [];
463
464 function fillLC(dst, src) {
465 if (src.type != "LINEARCOMBINATION") throw new Error("Constraint is not a LINEARCOMBINATION");
466 for (let s in src.values) {
467 const v = src.values[s].toString();
468 const id = ctx.signalName2Idx[s];
469 dst[id] = v;
470 }
471 }
472
473 for (let i=0; i<ctx.constraints.length; i++) {
474 const A = {};
475 const B = {};
476 const C = {};
477
478 fillLC(A, ctx.constraints[i].a);
479 fillLC(B, ctx.constraints[i].b);
480 fillLC(C, lc.negate(ctx.constraints[i].c));
481
482 res.push([A,B,C]);
483 }
484
485 return res;
486}
487
488
489