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 };
70
71
72 exec(ctx, ast);
73
74 if (!ctx.components["main"]) {
75 throw new Error("A main component must be defined");
76 }
77
78 classifySignals(ctx);
79
80 reduceConstants(ctx);
81 if (options.reduceConstraints) {
82
83 // Repeat while reductions are performed
84 let oldNConstrains = -1;
85 while (ctx.constraints.length != oldNConstrains) {
86 oldNConstrains = ctx.constraints.length;
87 reduceConstrains(ctx);
88 }
89 }
90
91 generateWitnessNames(ctx);
92
93 if (ctx.error) {
94 throw(ctx.error);
95 }
96
97 ctx.scopes = [{}];
98
99 const mainCode = gen(ctx,ast);
100 if (ctx.error) throw(ctx.error);
101
102 const def = buildCircuitDef(ctx, mainCode);
103
104 return def;
105}
106
107
108function classifySignals(ctx) {
109
110 function priorize(t1, t2) {
111 if ((t1 == "error") || (t2=="error")) return "error";
112 if (t1 == "internal") {
113 return t2;
114 } else if (t2=="internal") {
115 return t1;
116 }
117 if ((t1 == "one") || (t2 == "one")) return "one";
118 if ((t1 == "constant") || (t2 == "constant")) return "constant";
119 if (t1!=t2) return "error";
120 return t1;
121 }
122
123 // First classify the signals
124 for (let s in ctx.signals) {
125 const signal = ctx.signals[s];
126 let tAll = "internal";
127 let lSignal = signal;
128 let end = false;
129 while (!end) {
130 let t = lSignal.category || "internal";
131 if (s == "one") {
132 t = "one";
133 } else if (lSignal.value) {
134 t = "constant";
135 } else if (lSignal.component=="main") {
136 if (lSignal.direction == "IN") {
137 if (lSignal.private) {
138 t = "prvInput";
139 } else {
140 t = "pubInput";
141 }
142 } else if (lSignal.direction == "OUT") {
143 t = "output";
144 }
145 }
146 tAll = priorize(t,tAll);
147 if (lSignal.equivalence) {
148 lSignal = ctx.signals[lSignal.equivalence];
149 } else {
150 end=true;
151 }
152 }
153 if (tAll == "error") {
154 throw new Error("Incompatible types in signal: " + s);
155 }
156 lSignal.category = tAll;
157 }
158}
159
160
161function generateWitnessNames(ctx) {
162
163 const totals = {
164 "output": 0,
165 "pubInput": 0,
166 "one": 0,
167 "prvInput": 0,
168 "internal": 0,
169 "constant": 0,
170 };
171 const ids = {};
172
173 const counted = {};
174
175 // First classify the signals
176 for (let s in ctx.signals) {
177 const signal = ctx.signals[s];
178 let lSignal = signal;
179 while (lSignal.equivalence) lSignal = ctx.signals[lSignal.equivalence];
180
181 if (!counted[lSignal.fullName]) {
182 counted[lSignal.fullName] = true;
183 totals[lSignal.category] ++;
184 }
185 }
186
187 ids["one"] = 0;
188 ids["output"] = 1;
189 ids["pubInput"] = ids["output"] + totals["output"];
190 ids["prvInput"] = ids["pubInput"] + totals["pubInput"];
191 ids["internal"] = ids["prvInput"] + totals["prvInput"];
192 ids["constant"] = ids["internal"] + totals["internal"];
193 const nSignals = ids["constant"] + totals["constant"];
194
195 ctx.signalNames = new Array(nSignals);
196 for (let i=0; i< nSignals; i++) ctx.signalNames[i] = [];
197 ctx.signalName2Idx = {};
198
199 for (let s in ctx.signals) {
200 const signal = ctx.signals[s];
201 let lSignal = signal;
202 while (lSignal.equivalence) {
203 lSignal = ctx.signals[lSignal.equivalence];
204 }
205 if ( typeof(lSignal.id) === "undefined" ) {
206 lSignal.id = ids[lSignal.category] ++;
207 }
208
209 signal.id = lSignal.id;
210 ctx.signalNames[signal.id].push(signal.fullName);
211 ctx.signalName2Idx[signal.fullName] = signal.id;
212 }
213
214 ctx.totals = totals;
215}
216
217function reduceConstants(ctx) {
218 const newConstraints = [];
219 for (let i=0; i<ctx.constraints.length; i++) {
220 const c = lc.canonize(ctx, ctx.constraints[i]);
221 if (!lc.isZero(c)) {
222 newConstraints.push(c);
223 }
224 }
225 ctx.constraints = newConstraints;
226}
227
228function reduceConstrains(ctx) {
229 indexVariables();
230 let possibleConstraints = Object.keys(ctx.constraints);
231 while (possibleConstraints.length>0) {
232 let nextPossibleConstraints = {};
233 for (let i in possibleConstraints) {
234 if (!ctx.constraints[i]) continue;
235 const c = ctx.constraints[i];
236
237 // Swap a and b if b has more variables.
238 if (Object.keys(c.b).length > Object.keys(c.a).length) {
239 const aux = c.a;
240 c.a=c.b;
241 c.b=aux;
242 }
243
244 // Mov to C if possible.
245 if (isConstant(c.a)) {
246 const ct = {type: "NUMBER", value: c.a.values["one"]};
247 c.c = lc.add(lc.mul(c.b, ct), c.c);
248 c.a = { type: "LINEARCOMBINATION", values: {} };
249 c.b = { type: "LINEARCOMBINATION", values: {} };
250 }
251 if (isConstant(c.b)) {
252 const ct = {type: "NUMBER", value: c.b.values["one"]};
253 c.c = lc.add(lc.mul(c.a, ct), c.c);
254 c.a = { type: "LINEARCOMBINATION", values: {} };
255 c.b = { type: "LINEARCOMBINATION", values: {} };
256 }
257
258 if (lc.isZero(c.a) || lc.isZero(c.b)) {
259 const isolatedSignal = getFirstInternalSignal(ctx, c.c);
260 if (isolatedSignal) {
261
262 let lSignal = ctx.signals[isolatedSignal];
263 while (lSignal.equivalence) {
264 lSignal = ctx.signals[lSignal.equivalence];
265 }
266
267
268 const isolatedSignalEquivalence = {
269 type: "LINEARCOMBINATION",
270 values: {}
271 };
272 const invCoef = c.c.values[isolatedSignal].modInv(__P__);
273 for (const s in c.c.values) {
274 if (s != isolatedSignal) {
275 const v = __P__.minus(c.c.values[s]).times(invCoef).mod(__P__);
276 if (!v.isZero()) {
277 isolatedSignalEquivalence.values[s] = v;
278 }
279 }
280 }
281
282 for (let j in lSignal.inConstraints) {
283 if ((j!=i)&&(ctx.constraints[j])) {
284 ctx.constraints[j] = lc.substitute(ctx.constraints[j], isolatedSignal, isolatedSignalEquivalence);
285 linkSignalsConstraint(j);
286 if (j<i) {
287 nextPossibleConstraints[j] = true;
288 }
289 }
290 }
291
292 ctx.constraints[i] = null;
293
294 lSignal.category = "constant";
295 } else {
296 if (lc.isZero(c.c)) ctx.constraints[i] = null;
297 }
298 }
299 }
300 possibleConstraints = Object.keys(nextPossibleConstraints);
301 }
302 unindexVariables();
303
304 // Pack the constraints
305 let o = 0;
306 for (let i=0; i<ctx.constraints.length; i++) {
307 if (ctx.constraints[i]) {
308 if (o != i) {
309 ctx.constraints[o] = ctx.constraints[i];
310 }
311 o++;
312 }
313 }
314 ctx.constraints.length = o;
315
316 function indexVariables() {
317 for (let i=0; i<ctx.constraints.length; i++) linkSignalsConstraint(i);
318 }
319
320 function linkSignalsConstraint(cidx) {
321 const ct = ctx.constraints[cidx];
322 for (let k in ct.a.values) linkSignal(k, cidx);
323 for (let k in ct.b.values) linkSignal(k, cidx);
324 for (let k in ct.c.values) linkSignal(k, cidx);
325 }
326
327 function unindexVariables() {
328 for (let s in ctx.signals) {
329 let lSignal = ctx.signals[s];
330 while (lSignal.equivalence) {
331 lSignal = ctx.signals[lSignal.equivalence];
332 }
333 if (lSignal.inConstraints) delete lSignal.inConstraints;
334 }
335 }
336
337/*
338 function unlinkSignal(signalName, cidx) {
339 let lSignal = ctx.signals[signalName];
340 while (lSignal.equivalence) {
341 lSignal = ctx.signals[lSignal.equivalence];
342 }
343 if ((lSignal.inConstraints)&&(lSignal.inConstraints[cidx])) {
344 delete lSignal.inConstraints[cidx];
345 }
346 }
347*/
348
349 function linkSignal(signalName, cidx) {
350 let lSignal = ctx.signals[signalName];
351 while (lSignal.equivalence) {
352 lSignal = ctx.signals[lSignal.equivalence];
353 }
354 if (!lSignal.inConstraints) lSignal.inConstraints = {};
355 lSignal.inConstraints[cidx] = true;
356 }
357
358 function getFirstInternalSignal(ctx, l) {
359 for (let k in l.values) {
360 const signal = ctx.signals[k];
361 if (signal.category == "internal") return k;
362 }
363 return null;
364 }
365
366 function isConstant(l) {
367 for (let k in l.values) {
368 if ((k != "one") && (!l.values[k].isZero())) return false;
369 }
370 if (!l.values["one"] || l.values["one"].isZero()) return false;
371 return true;
372 }
373
374}
375
376
377function buildCircuitDef(ctx, mainCode) {
378 const res = {
379 mainCode: mainCode
380 };
381 res.signalName2Idx = ctx.signalName2Idx;
382
383 res.components = [];
384 res.componentName2Idx = {};
385 for (let c in ctx.components) {
386 const idCoponent = res.components.length;
387 res.components.push({
388 name: c,
389 params: ctx.components[c].params,
390 template: ctx.components[c].template,
391 inputSignals: 0
392 });
393 res.componentName2Idx[c] = idCoponent;
394 }
395
396 res.signals = new Array(ctx.signalNames.length);
397 for (let i=0; i<ctx.signalNames.length; i++) {
398 res.signals[i] = {
399 names: ctx.signalNames[i],
400 triggerComponents: []
401 };
402 ctx.signalNames[i].map( (fullName) => {
403 const idComponet = res.componentName2Idx[ctx.signals[fullName].component];
404 if (ctx.signals[fullName].direction == "IN") {
405 res.signals[i].triggerComponents.push(idComponet);
406 res.components[idComponet].inputSignals++;
407 }
408 });
409 }
410
411 res.constraints = buildConstraints(ctx);
412
413 res.templates = ctx.templates;
414
415 res.functions = {};
416 for (let f in ctx.functions) {
417 res.functions[f] = {
418 params: ctx.functionParams[f],
419 func: ctx.functions[f]
420 };
421 }
422
423 res.nPrvInputs = ctx.totals.prvInput;
424 res.nPubInputs = ctx.totals.pubInput;
425 res.nInputs = res.nPrvInputs + res.nPubInputs;
426 res.nOutputs = ctx.totals.output;
427 res.nVars = res.nInputs + res.nOutputs + ctx.totals.one + ctx.totals.internal;
428 res.nConstants = ctx.totals.constant;
429 res.nSignals = res.nVars + res.nConstants;
430
431 return res;
432}
433
434/*
435 Build constraints
436
437A constraint like this
438
439 [s1 + 2*s2 + 3*s3] * [ s2 + 5*s4] - [s0 ] = 0
440 [ 5*s2 + 6*s3] * [ s2 + ] - [s0 + 2* s2] = 0
441 [s1 + s3] * [ s2 + 5*s3] - [s4 ] = 0
442
443is converted to
444
445[
446 [{"1":"1","2":"2","3":"3"} , {"2":"1","4":"5"} , {"0":"1" }],
447 [{ "2":"5","3":"6"} , {"2":"1" } , {"0":"1", "2":"2"}],
448 [{"1":"1", "3":"1"} , {"2":"1","3":"5"} , {"4":"1" }]
449]
450 ^ ^ ^
451 | | |
452 A B C
453
454*/
455
456function buildConstraints(ctx) {
457 const res = [];
458
459 function fillLC(dst, src) {
460 if (src.type != "LINEARCOMBINATION") throw new Error("Constraint is not a LINEARCOMBINATION");
461 for (let s in src.values) {
462 const v = src.values[s].toString();
463 const id = ctx.signalName2Idx[s];
464 dst[id] = v;
465 }
466 }
467
468 for (let i=0; i<ctx.constraints.length; i++) {
469 const A = {};
470 const B = {};
471 const C = {};
472
473 fillLC(A, ctx.constraints[i].a);
474 fillLC(B, ctx.constraints[i].b);
475 fillLC(C, lc.negate(ctx.constraints[i].c));
476
477 res.push([A,B,C]);
478 }
479
480 return res;
481}
482
483
484