You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

416 lines
12 KiB

6 years ago
5 years ago
5 years ago
6 years ago
6 years ago
6 years ago
6 years ago
6 years ago
6 years ago
6 years ago
6 years ago
6 years ago
  1. /*
  2. Copyright 2018 0KIMS association.
  3. This file is part of circom (Zero Knowledge Circuit Compiler).
  4. circom is a free software: you can redistribute it and/or modify it
  5. under the terms of the GNU General Public License as published by
  6. the Free Software Foundation, either version 3 of the License, or
  7. (at your option) any later version.
  8. circom is distributed in the hope that it will be useful, but WITHOUT
  9. ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
  10. or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
  11. License for more details.
  12. You should have received a copy of the GNU General Public License
  13. along with circom. If not, see <https://www.gnu.org/licenses/>.
  14. */
  15. const fs = require("fs");
  16. const path = require("path");
  17. const bigInt = require("big-integer");
  18. const __P__ = new bigInt("21888242871839275222246405745257275088548364400416034343698204186575808495617");
  19. const __MASK__ = new bigInt(2).pow(253).minus(1);
  20. const assert = require("assert");
  21. const gen = require("./gencode");
  22. const exec = require("./exec");
  23. const lc = require("./lcalgebra");
  24. module.exports = compile;
  25. const parser = require("../parser/jaz.js").parser;
  26. const timeout = ms => new Promise(res => setTimeout(res, ms));
  27. async function compile(srcFile, options) {
  28. if (!options) {
  29. options = {};
  30. }
  31. if (typeof options.reduceConstraints === "undefined") {
  32. options.reduceConstraints = true;
  33. }
  34. const fullFileName = srcFile;
  35. const fullFilePath = path.dirname(fullFileName);
  36. const src = fs.readFileSync(fullFileName, "utf8");
  37. const ast = parser.parse(src);
  38. assert(ast.type == "BLOCK");
  39. const ctx = {
  40. scopes: [{}],
  41. signals: {
  42. one: {
  43. fullName: "one",
  44. value: bigInt(1),
  45. equivalence: "",
  46. direction: ""
  47. }
  48. },
  49. currentComponent: "",
  50. constraints: [],
  51. components: {},
  52. templates: {},
  53. functions: {},
  54. functionParams: {},
  55. filePath: fullFilePath,
  56. fileName: fullFileName
  57. };
  58. exec(ctx, ast);
  59. if (!ctx.components["main"]) {
  60. throw new Error("A main component must be defined");
  61. }
  62. classifySignals(ctx);
  63. if (options.reduceConstraints) {
  64. reduceConstants(ctx);
  65. // Repeat while reductions are performed
  66. let oldNConstrains = -1;
  67. while (ctx.constraints.length != oldNConstrains) {
  68. oldNConstrains = ctx.constraints.length;
  69. reduceConstrains(ctx);
  70. }
  71. }
  72. generateWitnessNames(ctx);
  73. if (ctx.error) {
  74. throw(ctx.error);
  75. }
  76. ctx.scopes = [{}];
  77. const mainCode = gen(ctx,ast);
  78. if (ctx.error) throw(ctx.error);
  79. const def = buildCircuitDef(ctx, mainCode);
  80. return def;
  81. }
  82. function classifySignals(ctx) {
  83. function priorize(t1, t2) {
  84. if ((t1 == "error") || (t2=="error")) return "error";
  85. if (t1 == "internal") {
  86. return t2;
  87. } else if (t2=="internal") {
  88. return t1;
  89. }
  90. if ((t1 == "one") || (t2 == "one")) return "one";
  91. if ((t1 == "constant") || (t2 == "constant")) return "constant";
  92. if (t1!=t2) return "error";
  93. return t1;
  94. }
  95. // First classify the signals
  96. for (let s in ctx.signals) {
  97. const signal = ctx.signals[s];
  98. let tAll = "internal";
  99. let lSignal = signal;
  100. let end = false;
  101. while (!end) {
  102. let t = lSignal.category || "internal";
  103. if (s == "one") {
  104. t = "one";
  105. } else if (lSignal.value) {
  106. t = "constant";
  107. } else if (lSignal.component=="main") {
  108. if (lSignal.direction == "IN") {
  109. if (lSignal.private) {
  110. t = "prvInput";
  111. } else {
  112. t = "pubInput";
  113. }
  114. } else if (lSignal.direction == "OUT") {
  115. t = "output";
  116. }
  117. }
  118. tAll = priorize(t,tAll);
  119. if (lSignal.equivalence) {
  120. lSignal = ctx.signals[lSignal.equivalence];
  121. } else {
  122. end=true;
  123. }
  124. }
  125. if (tAll == "error") {
  126. throw new Error("Incompatible types in signal: " + s);
  127. }
  128. lSignal.category = tAll;
  129. }
  130. }
  131. function generateWitnessNames(ctx) {
  132. const totals = {
  133. "output": 0,
  134. "pubInput": 0,
  135. "one": 0,
  136. "prvInput": 0,
  137. "internal": 0,
  138. "constant": 0,
  139. };
  140. const ids = {};
  141. const counted = {};
  142. // First classify the signals
  143. for (let s in ctx.signals) {
  144. const signal = ctx.signals[s];
  145. let lSignal = signal;
  146. while (lSignal.equivalence) lSignal = ctx.signals[lSignal.equivalence];
  147. if (!counted[lSignal.fullName]) {
  148. counted[lSignal.fullName] = true;
  149. totals[lSignal.category] ++;
  150. }
  151. }
  152. ids["one"] = 0;
  153. ids["output"] = 1;
  154. ids["pubInput"] = ids["output"] + totals["output"];
  155. ids["prvInput"] = ids["pubInput"] + totals["pubInput"];
  156. ids["internal"] = ids["prvInput"] + totals["prvInput"];
  157. ids["constant"] = ids["internal"] + totals["internal"];
  158. const nSignals = ids["constant"] + totals["constant"];
  159. ctx.signalNames = new Array(nSignals);
  160. for (let i=0; i< nSignals; i++) ctx.signalNames[i] = [];
  161. ctx.signalName2Idx = {};
  162. for (let s in ctx.signals) {
  163. const signal = ctx.signals[s];
  164. let lSignal = signal;
  165. while (lSignal.equivalence) {
  166. lSignal = ctx.signals[lSignal.equivalence];
  167. }
  168. if ( typeof(lSignal.id) === "undefined" ) {
  169. lSignal.id = ids[lSignal.category] ++;
  170. }
  171. signal.id = lSignal.id;
  172. ctx.signalNames[signal.id].push(signal.fullName);
  173. ctx.signalName2Idx[signal.fullName] = signal.id;
  174. }
  175. ctx.totals = totals;
  176. }
  177. function reduceConstants(ctx) {
  178. const newConstraints = [];
  179. for (let i=0; i<ctx.constraints.length; i++) {
  180. const c = lc.canonize(ctx, ctx.constraints[i]);
  181. if (!lc.isZero(c)) {
  182. newConstraints.push(c);
  183. }
  184. }
  185. ctx.constraints = newConstraints;
  186. }
  187. function reduceConstrains(ctx) {
  188. const newConstraints = [];
  189. for (let i=0; i<ctx.constraints.length; i++) {
  190. const c = ctx.constraints[i];
  191. // Swap a and b if b has more variables.
  192. if (Object.keys(c.b).length > Object.keys(c.a).length) {
  193. const aux = c.a;
  194. c.a=c.b;
  195. c.b=aux;
  196. }
  197. // Mov to C if possible.
  198. if (isConstant(c.a)) {
  199. const ct = {type: "NUMBER", value: c.a.values["one"]};
  200. c.c = lc.add(lc.mul(c.b, ct), c.c);
  201. c.a = { type: "LINEARCOMBINATION", values: {} };
  202. c.b = { type: "LINEARCOMBINATION", values: {} };
  203. }
  204. if (isConstant(c.b)) {
  205. const ct = {type: "NUMBER", value: c.b.values["one"]};
  206. c.c = lc.add(lc.mul(c.a, ct), c.c);
  207. c.a = { type: "LINEARCOMBINATION", values: {} };
  208. c.b = { type: "LINEARCOMBINATION", values: {} };
  209. }
  210. if (lc.isZero(c.a) || lc.isZero(c.b)) {
  211. const isolatedSignal = getFirstInternalSignal(ctx, c.c);
  212. if (isolatedSignal) {
  213. const isolatedSignalEquivalence = {
  214. type: "LINEARCOMBINATION",
  215. values: {}
  216. };
  217. const invCoef = c.c.values[isolatedSignal].modInv(__P__);
  218. for (const s in c.c.values) {
  219. if (s != isolatedSignal) {
  220. const v = __P__.minus(c.c.values[s]).times(invCoef).mod(__P__);
  221. if (!v.isZero()) {
  222. isolatedSignalEquivalence.values[s] = v;
  223. }
  224. }
  225. }
  226. for (let j=0; j<newConstraints.length; j++) {
  227. newConstraints[j] = lc.substitute(newConstraints[j], isolatedSignal, isolatedSignalEquivalence);
  228. }
  229. for (let j=i+1; j<ctx.constraints.length; j++ ) {
  230. ctx.constraints[j] = lc.substitute(ctx.constraints[j], isolatedSignal, isolatedSignalEquivalence);
  231. }
  232. c.a={ type: "LINEARCOMBINATION", values: {} };
  233. c.b={ type: "LINEARCOMBINATION", values: {} };
  234. c.c={ type: "LINEARCOMBINATION", values: {} };
  235. isolatedSignal.category = "constant";
  236. }
  237. }
  238. if (!lc.isZero(c)) {
  239. newConstraints.push(c);
  240. }
  241. }
  242. ctx.constraints = newConstraints;
  243. function getFirstInternalSignal(ctx, l) {
  244. for (let k in l.values) {
  245. const signal = ctx.signals[k];
  246. if (signal.category == "internal") return k;
  247. }
  248. return null;
  249. }
  250. function isConstant(l) {
  251. for (let k in l.values) {
  252. if ((k != "one") && (!l.values[k].isZero())) return false;
  253. }
  254. if (!l.values["one"] || l.values["one"].isZero()) return false;
  255. return true;
  256. }
  257. }
  258. function buildCircuitDef(ctx, mainCode) {
  259. const res = {
  260. mainCode: mainCode
  261. };
  262. res.signalName2Idx = ctx.signalName2Idx;
  263. res.components = [];
  264. res.componentName2Idx = {};
  265. for (let c in ctx.components) {
  266. const idCoponent = res.components.length;
  267. res.components.push({
  268. name: c,
  269. params: ctx.components[c].params,
  270. template: ctx.components[c].template,
  271. inputSignals: 0
  272. });
  273. res.componentName2Idx[c] = idCoponent;
  274. }
  275. res.signals = new Array(ctx.signalNames.length);
  276. for (let i=0; i<ctx.signalNames.length; i++) {
  277. res.signals[i] = {
  278. names: ctx.signalNames[i],
  279. triggerComponents: []
  280. };
  281. ctx.signalNames[i].map( (fullName) => {
  282. const idComponet = res.componentName2Idx[ctx.signals[fullName].component];
  283. if (ctx.signals[fullName].direction == "IN") {
  284. res.signals[i].triggerComponents.push(idComponet);
  285. res.components[idComponet].inputSignals++;
  286. }
  287. });
  288. }
  289. res.constraints = buildConstraints(ctx);
  290. res.templates = ctx.templates;
  291. res.functions = {};
  292. for (let f in ctx.functions) {
  293. res.functions[f] = {
  294. params: ctx.functionParams[f],
  295. func: ctx.functions[f]
  296. };
  297. }
  298. res.nPrvInputs = ctx.totals.prvInput;
  299. res.nPubInputs = ctx.totals.pubInput;
  300. res.nInputs = res.nPrvInputs + res.nPubInputs;
  301. res.nOutputs = ctx.totals.output;
  302. res.nVars = res.nInputs + res.nOutputs + ctx.totals.one + ctx.totals.internal;
  303. res.nConstants = ctx.totals.constant;
  304. res.nSignals = res.nVars + res.nConstants;
  305. return res;
  306. }
  307. /*
  308. Build constraints
  309. A constraint like this
  310. [s1 + 2*s2 + 3*s3] * [ s2 + 5*s4] - [s0 ] = 0
  311. [ 5*s2 + 6*s3] * [ s2 + ] - [s0 + 2* s2] = 0
  312. [s1 + s3] * [ s2 + 5*s3] - [s4 ] = 0
  313. is converted to
  314. [
  315. [{"1":"1","2":"2","3":"3"} , {"2":"1","4":"5"} , {"0":"1" }],
  316. [{ "2":"5","3":"6"} , {"2":"1" } , {"0":"1", "2":"2"}],
  317. [{"1":"1", "3":"1"} , {"2":"1","3":"5"} , {"4":"1" }]
  318. ]
  319. ^ ^ ^
  320. | | |
  321. A B C
  322. */
  323. function buildConstraints(ctx) {
  324. const res = [];
  325. function fillLC(dst, src) {
  326. if (src.type != "LINEARCOMBINATION") throw new Error("Constraint is not a LINEARCOMBINATION");
  327. for (let s in src.values) {
  328. const v = src.values[s].toString();
  329. const id = ctx.signalName2Idx[s];
  330. dst[id] = v;
  331. }
  332. }
  333. for (let i=0; i<ctx.constraints.length; i++) {
  334. const A = {};
  335. const B = {};
  336. const C = {};
  337. fillLC(A, ctx.constraints[i].a);
  338. fillLC(B, ctx.constraints[i].b);
  339. fillLC(C, lc.negate(ctx.constraints[i].c));
  340. res.push([A,B,C]);
  341. }
  342. return res;
  343. }