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