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 assert = require("assert");
26const gen = require("./gencode");
27const exec = require("./exec");
28const lc = require("./lcalgebra");
29
30module.exports = compile;
31
32const parser = require("../parser/jaz.js").parser;
33
34const timeout = ms => new Promise(res => setTimeout(res, ms));
35
36async function compile(srcFile) {
37 const fullFileName = srcFile;
38 const fullFilePath = path.dirname(fullFileName);
39
40 const src = fs.readFileSync(fullFileName, "utf8");
41 const ast = parser.parse(src);
42
43 assert(ast.type == "BLOCK");
44
45 const ctx = {
46 scopes: [{}],
47 signals: {
48 one: {
49 fullName: "one",
50 value: bigInt(1),
51 equivalence: "",
52 direction: ""
53 }
54 },
55 currentComponent: "",
56 constraints: [],
57 components: {},
58 templates: {},
59 functions: {},
60 functionParams: {},
61 filePath: fullFilePath,
62 fileName: fullFileName
63 };
64
65
66 exec(ctx, ast);
67
68 if (!ctx.components["main"]) {
69 throw new Error("A main component must be defined");
70 }
71
72 classifySignals(ctx);
73 reduceConstants(ctx);
74
75 // Repeat while reductions are performed
76 let oldNConstrains = -1;
77 while (ctx.constraints.length != oldNConstrains) {
78 oldNConstrains = ctx.constraints.length;
79 reduceConstrains(ctx);
80 }
81
82 generateWitnessNames(ctx);
83
84 if (ctx.error) {
85 throw(ctx.error);
86 }
87
88 ctx.scopes = [{}];
89
90 const mainCode = gen(ctx,ast);
91 if (ctx.error) throw(ctx.error);
92
93 const def = buildCircuitDef(ctx, mainCode);
94
95 return def;
96}
97
98
99function classifySignals(ctx) {
100
101 function priorize(t1, t2) {
102 if ((t1 == "error") || (t2=="error")) return "error";
103 if (t1 == "internal") {
104 return t2;
105 } else if (t2=="internal") {
106 return t1;
107 }
108 if ((t1 == "one") || (t2 == "one")) return "one";
109 if ((t1 == "constant") || (t2 == "constant")) return "constant";
110 if (t1!=t2) return "error";
111 return t1;
112 }
113
114 // First classify the signals
115 for (let s in ctx.signals) {
116 const signal = ctx.signals[s];
117 let tAll = "internal";
118 let lSignal = signal;
119 let end = false;
120 while (!end) {
121 let t = lSignal.category || "internal";
122 if (s == "one") {
123 t = "one";
124 } else if (lSignal.value) {
125 t = "constant";
126 } else if (lSignal.component=="main") {
127 if (lSignal.direction == "IN") {
128 if (lSignal.private) {
129 t = "prvInput";
130 } else {
131 t = "pubInput";
132 }
133 } else if (lSignal.direction == "OUT") {
134 t = "output";
135 }
136 }
137 tAll = priorize(t,tAll);
138 if (lSignal.equivalence) {
139 lSignal = ctx.signals[lSignal.equivalence];
140 } else {
141 end=true;
142 }
143 }
144 if (tAll == "error") {
145 throw new Error("Incompatible types in signal: " + s);
146 }
147 lSignal.category = tAll;
148 }
149}
150
151
152function generateWitnessNames(ctx) {
153
154 const totals = {
155 "output": 0,
156 "pubInput": 0,
157 "one": 0,
158 "prvInput": 0,
159 "internal": 0,
160 "constant": 0,
161 };
162 const ids = {};
163
164 const counted = {};
165
166 // First classify the signals
167 for (let s in ctx.signals) {
168 const signal = ctx.signals[s];
169 let lSignal = signal;
170 while (lSignal.equivalence) lSignal = ctx.signals[lSignal.equivalence];
171
172 if (!counted[lSignal.fullName]) {
173 counted[lSignal.fullName] = true;
174 totals[lSignal.category] ++;
175 }
176 }
177
178 ids["one"] = 0;
179 ids["output"] = 1;
180 ids["pubInput"] = ids["output"] + totals["output"];
181 ids["prvInput"] = ids["pubInput"] + totals["pubInput"];
182 ids["internal"] = ids["prvInput"] + totals["prvInput"];
183 ids["constant"] = ids["internal"] + totals["internal"];
184 const nSignals = ids["constant"] + totals["constant"];
185
186 ctx.signalNames = new Array(nSignals);
187 for (let i=0; i< nSignals; i++) ctx.signalNames[i] = [];
188 ctx.signalName2Idx = {};
189
190 for (let s in ctx.signals) {
191 const signal = ctx.signals[s];
192 let lSignal = signal;
193 while (lSignal.equivalence) {
194 lSignal = ctx.signals[lSignal.equivalence];
195 }
196 if ( typeof(lSignal.id) === "undefined" ) {
197 lSignal.id = ids[lSignal.category] ++;
198 }
199
200 signal.id = lSignal.id;
201 ctx.signalNames[signal.id].push(signal.fullName);
202 ctx.signalName2Idx[signal.fullName] = signal.id;
203 }
204
205 ctx.totals = totals;
206}
207
208function reduceConstants(ctx) {
209 const newConstraints = [];
210 for (let i=0; i<ctx.constraints.length; i++) {
211 const c = lc.canonize(ctx, ctx.constraints[i]);
212 if (!lc.isZero(c)) {
213 newConstraints.push(c);
214 }
215 }
216 ctx.constraints = newConstraints;
217}
218
219function reduceConstrains(ctx) {
220 const newConstraints = [];
221 for (let i=0; i<ctx.constraints.length; i++) {
222 const c = ctx.constraints[i];
223
224 // Swap a and b if b has more variables.
225 if (Object.keys(c.b).length > Object.keys(c.a).length) {
226 const aux = c.a;
227 c.a=c.b;
228 c.b=aux;
229 }
230
231 // Mov to C if possible.
232 if (isConstant(c.a)) {
233 const ct = {type: "NUMBER", value: c.a.values["one"]};
234 c.c = lc.add(lc.mul(c.b, ct), c.c);
235 c.a = { type: "LINEARCOMBINATION", values: {} };
236 c.b = { type: "LINEARCOMBINATION", values: {} };
237 }
238 if (isConstant(c.b)) {
239 const ct = {type: "NUMBER", value: c.b.values["one"]};
240 c.c = lc.add(lc.mul(c.a, ct), c.c);
241 c.a = { type: "LINEARCOMBINATION", values: {} };
242 c.b = { type: "LINEARCOMBINATION", values: {} };
243 }
244
245 if (lc.isZero(c.a) || lc.isZero(c.b)) {
246 const isolatedSignal = getFirstInternalSignal(ctx, c.c);
247 if (isolatedSignal) {
248 const isolatedSignalEquivalence = {
249 type: "LINEARCOMBINATION",
250 values: {}
251 };
252 const invCoef = c.c.values[isolatedSignal].modInv(__P__);
253 for (const s in c.c.values) {
254 if (s != isolatedSignal) {
255 const v = __P__.minus(c.c.values[s]).times(invCoef).mod(__P__);
256 if (!v.isZero()) {
257 isolatedSignalEquivalence.values[s] = v;
258 }
259 }
260 }
261
262 for (let j=0; j<newConstraints.length; j++) {
263 newConstraints[j] = lc.substitute(newConstraints[j], isolatedSignal, isolatedSignalEquivalence);
264 }
265 for (let j=i+1; j<ctx.constraints.length; j++ ) {
266 ctx.constraints[j] = lc.substitute(ctx.constraints[j], isolatedSignal, isolatedSignalEquivalence);
267 }
268 c.a={ type: "LINEARCOMBINATION", values: {} };
269 c.b={ type: "LINEARCOMBINATION", values: {} };
270 c.c={ type: "LINEARCOMBINATION", values: {} };
271 isolatedSignal.category = "constant";
272 }
273 }
274
275 if (!lc.isZero(c)) {
276 newConstraints.push(c);
277 }
278 }
279 ctx.constraints = newConstraints;
280
281 function getFirstInternalSignal(ctx, l) {
282 for (let k in l.values) {
283 const signal = ctx.signals[k];
284 if (signal.category == "internal") return k;
285 }
286 return null;
287 }
288
289 function isConstant(l) {
290 for (let k in l.values) {
291 if ((k != "one") && (!l.values[k].isZero())) return false;
292 }
293 if (!l.values["one"] || l.values["one"].isZero()) return false;
294 return true;
295 }
296
297}
298
299
300function buildCircuitDef(ctx, mainCode) {
301 const res = {
302 mainCode: mainCode
303 };
304 res.signalName2Idx = ctx.signalName2Idx;
305
306 res.components = [];
307 res.componentName2Idx = {};
308 for (let c in ctx.components) {
309 const idCoponent = res.components.length;
310 res.components.push({
311 name: c,
312 params: ctx.components[c].params,
313 template: ctx.components[c].template,
314 inputSignals: 0
315 });
316 res.componentName2Idx[c] = idCoponent;
317 }
318
319 res.signals = new Array(ctx.signalNames.length);
320 for (let i=0; i<ctx.signalNames.length; i++) {
321 res.signals[i] = {
322 names: ctx.signalNames[i],
323 triggerComponents: []
324 };
325 ctx.signalNames[i].map( (fullName) => {
326 const idComponet = res.componentName2Idx[ctx.signals[fullName].component];
327 if (ctx.signals[fullName].direction == "IN") {
328 res.signals[i].triggerComponents.push(idComponet);
329 res.components[idComponet].inputSignals++;
330 }
331 });
332 }
333
334 res.constraints = buildConstraints(ctx);
335
336 res.templates = ctx.templates;
337
338 res.functions = {};
339 for (let f in ctx.functions) {
340 res.functions[f] = {
341 params: ctx.functionParams[f],
342 func: ctx.functions[f]
343 };
344 }
345
346 res.nPrvInputs = ctx.totals.prvInput;
347 res.nPubInputs = ctx.totals.pubInput;
348 res.nInputs = res.nPrvInputs + res.nPubInputs;
349 res.nOutputs = ctx.totals.output;
350 res.nVars = res.nInputs + res.nOutputs + ctx.totals.one + ctx.totals.internal;
351 res.nConstants = ctx.totals.constant;
352 res.nSignals = res.nVars + res.nConstants;
353
354 return res;
355}
356
357/*
358 Build constraints
359
360A constraint like this
361
362 [s1 + 2*s2 + 3*s3] * [ s2 + 5*s4] - [s0 ] = 0
363 [ 5*s2 + 6*s3] * [ s2 + ] - [s0 + 2* s2] = 0
364 [s1 + s3] * [ s2 + 5*s3] - [s4 ] = 0
365
366is converted to
367
368[
369 [{"1":"1","2":"2","3":"3"} , {"2":"1","4":"5"} , {"0":"1" }],
370 [{ "2":"5","3":"6"} , {"2":"1" } , {"0":"1", "2":"2"}],
371 [{"1":"1", "3":"1"} , {"2":"1","3":"5"} , {"4":"1" }]
372]
373 ^ ^ ^
374 | | |
375 A B C
376
377*/
378
379function buildConstraints(ctx) {
380 const res = [];
381
382 function fillLC(dst, src) {
383 if (src.type != "LINEARCOMBINATION") throw new Error("Constraint is not a LINEARCOMBINATION");
384 for (let s in src.values) {
385 const v = src.values[s].toString();
386 const id = ctx.signalName2Idx[s];
387 dst[id] = v;
388 }
389 }
390
391 for (let i=0; i<ctx.constraints.length; i++) {
392 const A = {};
393 const B = {};
394 const C = {};
395
396 fillLC(A, ctx.constraints[i].a);
397 fillLC(B, ctx.constraints[i].b);
398 fillLC(C, lc.negate(ctx.constraints[i].c));
399
400 res.push([A,B,C]);
401 }
402
403 return res;
404}
405
406
407