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