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