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