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 bigInt = require("big-integer");
21const __P__ = new bigInt("21888242871839275222246405745257275088548364400416034343698204186575808495617");
22const sONE = 0;
23const buildC = require("./c_build");
24const constructionPhase = require("./construction_phase");
25const Ctx = require("./ctx");
26const ZqField = require("fflib").ZqField;
27const utils = require("./utils");
28const buildR1cs = require("./r1csfile").buildR1cs;
29const BigArray = require("./bigarray");
30
31module.exports = compile;
32
33async function compile(srcFile, options) {
34 options.p = options.p || __P__;
35 if (!options) {
36 options = {};
37 }
38 if (typeof options.reduceConstraints === "undefined") {
39 options.reduceConstraints = true;
40 }
41 const ctx = new Ctx();
42 ctx.field = new ZqField(options.p);
43 ctx.verbose= options.verbose || false;
44 ctx.mainComponent = options.mainComponent || "main";
45 ctx.newThreadTemplates = options.newThreadTemplates;
46
47 constructionPhase(ctx, srcFile);
48
49 console.log("NConstraints Before: "+ctx.constraints.length);
50
51 if (ctx.error) {
52 throw(ctx.error);
53 }
54
55 if (ctx.getComponentIdx(ctx.mainComponent)<0) {
56 throw new Error("A main component must be defined");
57 }
58
59 if (ctx.verbose) console.log("Classify Signals");
60 classifySignals(ctx);
61
62 if (ctx.verbose) console.log("Reduce Constants");
63 reduceConstants(ctx);
64 if (options.reduceConstraints) {
65
66 if (ctx.verbose) console.log("Reduce Constraints");
67 // Repeat while reductions are performed
68 let oldNConstrains = -1;
69 while (ctx.constraints.length != oldNConstrains) {
70 console.log("Reducing constraints: "+ctx.constraints.length);
71 oldNConstrains = ctx.constraints.length;
72 reduceConstrains(ctx);
73 }
74 }
75
76 console.log("NConstraints After: "+ctx.constraints.length);
77
78 generateWitnessNames(ctx);
79
80 if (ctx.error) {
81 throw(ctx.error);
82 }
83
84
85 if (options.cSourceWriteStream) {
86 const cSrc = buildC(ctx);
87 cSrc.pipe(options.cSourceWriteStream);
88 await new Promise(fulfill => options.cSourceWriteStream.on("finish", fulfill));
89 }
90
91 // const mainCode = gen(ctx,ast);
92 if (ctx.error) throw(ctx.error);
93
94 if (options.r1csFileName) {
95 await buildR1cs(ctx, options.r1csFileName);
96 }
97
98 if (options.symWriteStream) {
99 buildSyms(ctx, options.symWriteStream);
100 }
101
102// const def = buildCircuitDef(ctx, mainCode);
103
104}
105
106
107
108function classifySignals(ctx) {
109
110 const ERROR = 0xFFFF;
111
112 function priorize(t1, t2) {
113 if ((t1 == ERROR) || (t2==ERROR)) return ERROR;
114 if (t1 == ctx.stINTERNAL) {
115 return t2;
116 } else if (t2==ctx.stINTERNAL) {
117 return t1;
118 }
119 if ((t1 == ctx.stONE) || (t2 == ctx.stONE)) return ctx.stONE;
120 if ((t1 == ctx.stOUTPUT) || (t2 == ctx.stOUTPUT)) return ctx.stOUTPUT;
121 if ((t1 == ctx.stCONSTANT) || (t2 == ctx.stCONSTANT)) return ctx.stCONSTANT;
122 if ((t1 == ctx.stDISCARDED) || (t2 == ctx.stDISCARDED)) return ctx.stDISCARDED;
123 if (t1!=t2) return ERROR;
124 return t1;
125 }
126
127 // First classify the signals
128 for (let s=0; s<ctx.signals.length; s++) {
129 const signal = ctx.signals[s];
130 let tAll = ctx.stINTERNAL;
131 let lSignal = signal;
132 let end = false;
133 while (!end) {
134 let t = lSignal.c || ctx.stINTERNAL;
135 if (s == 0) {
136 t = ctx.stONE;
137 } else if (lSignal.o & ctx.MAIN) {
138 if (lSignal.o & ctx.IN) {
139 if (lSignal.o & ctx.PRV) {
140 t = ctx.stPRVINPUT;
141 } else {
142 t = ctx.stPUBINPUT;
143 }
144 } else if (lSignal.o & ctx.OUT) {
145 t = ctx.stOUTPUT;
146 }
147 } else if (utils.isDefined(lSignal.v)) {
148 t = ctx.stCONSTANT;
149 }
150 tAll = priorize(t,tAll);
151 if (lSignal.e>=0) {
152 lSignal = ctx.signals[lSignal.e];
153 } else {
154 end=true;
155 }
156 }
157 if (tAll == ERROR) {
158 throw new Error("Incompatible types in signal: " + s);
159 }
160 lSignal.c = tAll;
161 }
162}
163
164
165function generateWitnessNames(ctx) {
166 const totals = {};
167 totals[ctx.stONE] = 0;
168 totals[ctx.stOUTPUT] = 0;
169 totals[ctx.stPUBINPUT] = 0;
170 totals[ctx.stPRVINPUT] = 0;
171 totals[ctx.stINTERNAL] = 0;
172 totals[ctx.stDISCARDED] = 0;
173 totals[ctx.stCONSTANT] = 0;
174 const ids = {};
175
176 // First classify the signals
177 for (let s=0; s<ctx.signals.length; s++) {
178
179 if ((ctx.verbose)&&(s%10000 == 0)) console.log("generate witness (counting): ", s);
180
181 const signal = ctx.signals[s];
182 let lSignal = signal;
183 while (lSignal.e>=0) lSignal = ctx.signals[lSignal.e];
184
185 if (!( lSignal.o & ctx.COUNTED) ) {
186 lSignal.o |= ctx.COUNTED;
187 totals[lSignal.c] ++;
188 }
189 }
190
191 ids[ctx.stONE] = 0;
192 ids[ctx.stOUTPUT] = 1;
193 ids[ctx.stPUBINPUT] = ids[ctx.stOUTPUT] + totals[ctx.stOUTPUT];
194 ids[ctx.stPRVINPUT] = ids[ctx.stPUBINPUT] + totals[ctx.stPUBINPUT];
195 ids[ctx.stINTERNAL] = ids[ctx.stPRVINPUT] + totals[ctx.stPRVINPUT];
196 ids[ctx.stDISCARDED] = ids[ctx.stINTERNAL] + totals[ctx.stINTERNAL];
197 ids[ctx.stCONSTANT] = ids[ctx.stDISCARDED] + totals[ctx.stDISCARDED];
198 const nSignals = ids[ctx.stCONSTANT] + totals[ctx.stCONSTANT];
199
200 for (let s=0; s<ctx.signals.length; s++) {
201
202 if ((ctx.verbose)&&(s%10000 == 0)) console.log("seting id: ", s);
203
204 const signal = ctx.signals[s];
205 let lSignal = signal;
206 while (lSignal.e>=0) {
207 lSignal = ctx.signals[lSignal.e];
208 }
209 if ( typeof(lSignal.id) === "undefined" ) {
210 lSignal.id = ids[lSignal.c] ++;
211 }
212
213 signal.id = lSignal.id;
214 }
215
216 ctx.totals = totals;
217}
218
219function reduceConstants(ctx) {
220 const newConstraints = new BigArray();
221 for (let i=0; i<ctx.constraints.length; i++) {
222 if ((ctx.verbose)&&(i%10000 == 0)) console.log("reducing constants: ", i);
223 const c = ctx.lc.canonize(ctx, ctx.constraints[i]);
224 if (!ctx.lc.isZero(c)) {
225 newConstraints.push(c);
226 }
227 delete ctx.constraints[i];
228 }
229 ctx.constraints = newConstraints;
230}
231
232function reduceConstrains(ctx) {
233 indexVariables();
234 let possibleConstraints = ctx.constraints;
235 let ii=0;
236 while (possibleConstraints.length>0) {
237 let nextPossibleConstraints = new BigArray();
238 for (let i=0; i<possibleConstraints.length; i++) {
239 ii++;
240 if ((ctx.verbose)&&(ii%10000 == 0)) console.log("reducing constraints: ", i);
241 if (!ctx.constraints[i]) continue;
242 const c = ctx.constraints[i];
243
244 // Swap a and b if b has more variables.
245 if (Object.keys(c.b).length > Object.keys(c.a).length) {
246 const aux = c.a;
247 c.a=c.b;
248 c.b=aux;
249 }
250
251 // Mov to C if possible.
252 if (isConstant(c.a)) {
253 const ct = {t: "N", v: c.a.coefs[sONE]};
254 c.c = ctx.lc.add(ctx.lc.mul(c.b, ct), c.c);
255 c.a = { t: "LC", coefs: {} };
256 c.b = { t: "LC", coefs: {} };
257 }
258 if (isConstant(c.b)) {
259 const ct = {t: "N", v: c.b.coefs[sONE]};
260 c.c = ctx.lc.add(ctx.lc.mul(c.a, ct), c.c);
261 c.a = { t: "LC", coefs: {} };
262 c.b = { t: "LC", coefs: {} };
263 }
264
265 if (ctx.lc.isZero(c.a) || ctx.lc.isZero(c.b)) {
266 const isolatedSignal = getFirstInternalSignal(ctx, c.c);
267 if (isolatedSignal) {
268
269 let lSignal = ctx.signals[isolatedSignal];
270 while (lSignal.e>=0) {
271 lSignal = ctx.signals[lSignal.e];
272 }
273
274
275 const isolatedSignalEquivalence = {
276 t: "LC",
277 coefs: {}
278 };
279 const invCoef = c.c.coefs[isolatedSignal].modInv(__P__);
280 for (const s in c.c.coefs) {
281 if (s != isolatedSignal) {
282 const v = __P__.minus(c.c.coefs[s]).times(invCoef).mod(__P__);
283 if (!v.isZero()) {
284 isolatedSignalEquivalence.coefs[s] = v;
285 }
286 }
287 }
288
289 for (let j in lSignal.inConstraints) {
290 if ((j!=i)&&(ctx.constraints[j])) {
291 ctx.constraints[j] = ctx.lc.substitute(ctx.constraints[j], isolatedSignal, isolatedSignalEquivalence);
292 linkSignalsConstraint(j);
293 if (j<i) {
294 nextPossibleConstraints.push(j);
295 }
296 }
297 }
298
299 ctx.constraints[i] = null;
300
301 lSignal.c = ctx.stDISCARDED;
302 } else {
303 if (ctx.lc.isZero(c.c)) ctx.constraints[i] = null;
304 }
305 }
306 }
307 possibleConstraints = nextPossibleConstraints;
308 }
309 unindexVariables();
310
311 // Pack the constraints
312 let o = 0;
313 for (let i=0; i<ctx.constraints.length; i++) {
314 if (ctx.constraints[i]) {
315 if (o != i) {
316 ctx.constraints[o] = ctx.constraints[i];
317 }
318 o++;
319 }
320 }
321 ctx.constraints.length = o;
322
323 function indexVariables() {
324 for (let i=0; i<ctx.constraints.length; i++) linkSignalsConstraint(i);
325 }
326
327 function linkSignalsConstraint(cidx) {
328 const ct = ctx.constraints[cidx];
329 for (let k in ct.a.coefs) linkSignal(k, cidx);
330 for (let k in ct.b.coefs) linkSignal(k, cidx);
331 for (let k in ct.c.coefs) linkSignal(k, cidx);
332 }
333
334 function unindexVariables() {
335 for (let s=0; s<ctx.signals.length; s++) {
336 let lSignal = ctx.signals[s];
337 while (lSignal.e>=0) {
338 lSignal = ctx.signals[lSignal.e];
339 }
340 if (lSignal.inConstraints) delete lSignal.inConstraints;
341 }
342 }
343
344/*
345 function unlinkSignal(signalName, cidx) {
346 let lSignal = ctx.signals[signalName];
347 while (lSignal.e>=0) {
348 lSignal = ctx.signals[lSignal.e];
349 }
350 if ((lSignal.inConstraints)&&(lSignal.inConstraints[cidx])) {
351 delete lSignal.inConstraints[cidx];
352 }
353 }
354*/
355
356 function linkSignal(signalName, cidx) {
357 let lSignal = ctx.signals[signalName];
358 while (lSignal.e>=0) {
359 lSignal = ctx.signals[lSignal.e];
360 }
361 if (!lSignal.inConstraints) lSignal.inConstraints = {};
362 lSignal.inConstraints[cidx] = true;
363 }
364
365 function getFirstInternalSignal(ctx, l) {
366 for (let k in l.coefs) {
367 const signal = ctx.signals[k];
368 if (signal.c == ctx.stINTERNAL) return k;
369 }
370 return null;
371 }
372
373 function isConstant(l) {
374 for (let k in l.coefs) {
375 if ((k != sONE) && (!l.coefs[k].isZero())) return false;
376 }
377 if (!l.coefs[sONE] || l.coefs[sONE].isZero()) return false;
378 return true;
379 }
380
381}
382
383/*
384
385function buildCircuitDef(ctx, mainCode) {
386 const res = {
387 mainCode: mainCode
388 };
389 res.signalName2Idx = ctx.signalName2Idx;
390
391 res.components = [];
392 res.componentName2Idx = {};
393 for (let c in ctx.components) {
394 const idCoponent = res.components.length;
395 res.components.push({
396 name: c,
397 params: ctx.components[c].params,
398 template: ctx.components[c].template,
399 inputSignals: 0
400 });
401 res.componentName2Idx[c] = idCoponent;
402 }
403
404 res.signals = new Array(ctx.signalNames.length);
405 for (let i=0; i<ctx.signalNames.length; i++) {
406 res.signals[i] = {
407 names: ctx.signalNames[i],
408 triggerComponents: []
409 };
410 ctx.signalNames[i].map( (fullName) => {
411 const idComponet = res.componentName2Idx[ctx.signals[fullName].component];
412 if (ctx.signals[fullName].direction == "IN") {
413 res.signals[i].triggerComponents.push(idComponet);
414 res.components[idComponet].inputSignals++;
415 }
416 });
417 }
418
419 res.constraints = buildConstraints(ctx);
420
421 res.templates = ctx.templates;
422
423 res.functions = {};
424 for (let f in ctx.functions) {
425 res.functions[f] = {
426 params: ctx.functionParams[f],
427 func: ctx.functions[f]
428 };
429 }
430
431 res.nPrvInputs = ctx.totals.prvInput;
432 res.nPubInputs = ctx.totals.pubInput;
433 res.nInputs = res.nPrvInputs + res.nPubInputs;
434 res.nOutputs = ctx.totals.output;
435 res.nVars = res.nInputs + res.nOutputs + ctx.totals.one + ctx.totals.internal;
436 res.nConstants = ctx.totals.constant;
437 res.nSignals = res.nVars + res.nConstants;
438
439 return res;
440}
441
442*/
443
444
445/*
446 Build constraints
447
448A constraint like this
449
450 [s1 + 2*s2 + 3*s3] * [ s2 + 5*s4] - [s0 ] = 0
451 [ 5*s2 + 6*s3] * [ s2 + ] - [s0 + 2* s2] = 0
452 [s1 + s3] * [ s2 + 5*s3] - [s4 ] = 0
453
454is converted to
455
456[
457 [{"1":"1","2":"2","3":"3"} , {"2":"1","4":"5"} , {"0":"1" }],
458 [{ "2":"5","3":"6"} , {"2":"1" } , {"0":"1", "2":"2"}],
459 [{"1":"1", "3":"1"} , {"2":"1","3":"5"} , {"4":"1" }]
460]
461 ^ ^ ^
462 | | |
463 A B C
464
465*/
466/*
467function buildConstraints(ctx) {
468 const res = [];
469
470 function fillLC(dst, src) {
471 if (src.t != "LC") throw new Error("Constraint is not a LINEARCOMBINATION");
472 for (let s in src.coefs) {
473 const v = src.coefs[s].toString();
474 const id = ctx.signalName2Idx[s];
475 dst[id] = v;
476 }
477 }
478
479 for (let i=0; i<ctx.constraints.length; i++) {
480 const A = {};
481 const B = {};
482 const C = {};
483
484 fillLC(A, ctx.constraints[i].a);
485 fillLC(B, ctx.constraints[i].b);
486 fillLC(C, ctx.lc.negate(ctx.constraints[i].c));
487
488 res.push([A,B,C]);
489 }
490
491 return res;
492}
493*/
494function buildSyms(ctx, strm) {
495
496 let nSyms;
497
498 addSymbolsComponent(ctx.mainComponent + ".", ctx.getComponentIdx(ctx.mainComponent));
499
500
501 function addSymbolsComponent(prefix, idComponet) {
502 for (let n in ctx.components[idComponet].names.o) {
503 const entrie = ctx.components[idComponet].names.o[n];
504 addSymbolArray(prefix+n, entrie.type, entrie.sizes, entrie.offset);
505 }
506 }
507
508 function addSymbolArray(prefix, type, sizes, offset) {
509 if (sizes.length==0) {
510 if (type == "S") {
511 let s=offset;
512 while (ctx.signals[s].e >= 0) s = ctx.signals[s].e;
513 let wId = ctx.signals[s].id;
514 if (typeof(wId) == "undefined") wId=-1;
515 strm.write(`${offset},${wId},${prefix}\n`);
516 nSyms ++;
517 if ((ctx.verbose)&&(nSyms%10000 == 0)) console.log("Symbols saved: "+nSyms);
518 } else {
519 addSymbolsComponent(prefix+".", offset);
520 }
521 return 1;
522 } else {
523 let acc = 0;
524 for (let i=0; i<sizes[0]; i++) {
525 acc += addSymbolArray(`${prefix}[${i}]`, type, sizes.slice(1), offset + acc );
526 }
527 return acc;
528 }
529 }
530
531}
532
533
534