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