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