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