erhant · numtel · Dec 4, 2024 · Dec 4, 2024 · Dec 4, 2024 · Dec 4, 2024
diff --git a/README.md b/README.md
@@ -71,6 +71,12 @@ npx circomkit vkey <circuit> [pkey-path]
 
 # Automatically download PTAU (for BN128)
 npx circomkit ptau <circuit>
+
+# Display circuit info (e.g. constraint count)
+npx circomkit info <circuit>
+
+# Display human-readable constraint formulas
+npx circomkit constraints <circuit>
 ```
 
 > [!NOTE]
@@ -207,6 +213,17 @@ it('should have correct number of constraints', async () => {
 });
 ```
 
+> <picture>
+>   <source media="(prefers-color-scheme: light)" srcset="https://raw.githubusercontent.com/Mqxx/GitHub-Markdown/main/blockquotes/badge/light-theme/tip.svg">
+>   <img alt="Warning" src="https://raw.githubusercontent.com/Mqxx/GitHub-Markdown/main/blockquotes/badge/dark-theme/tip.svg">
+> </picture><br>
+>
+> You can also generate an array of human-readable formulas for each constraint using `parseConstraints`:
+>
+> ```ts
+> console.log((await circuit.parseConstraints()).join('\n'));
+> ```
+
 If you want more control over the output signals, you can use the `compute` function. It takes in an input, and an array of output signal names used in the `main` component so that they can be extracted from the witness.
 
 ```ts

diff --git a/src/cli.ts b/src/cli.ts
@@ -47,6 +47,15 @@ function cli(args: string[]) {
       console.log(`Number of Labels: ${info.labels}`);
     });
 
+  ///////////////////////////////////////////////////////////////////////////////
+  const constraints = new Command('constraints')
+    .description('print constraint formulas')
+    .argument('<circuit>', 'Circuit name')
+    .action(async circuit => {
+      const formulas = await circomkit.constraints(circuit);
+      console.log(formulas.join('\n'));
+    });
+
   ///////////////////////////////////////////////////////////////////////////////
   const clear = new Command('clear')
     .description('clear circuit build artifacts')
@@ -232,6 +241,7 @@ function cli(args: string[]) {
     .addCommand(circuit)
     .addCommand(instantiate)
     .addCommand(info)
+    .addCommand(constraints)
     .addCommand(clear)
     .addCommand(contract)
     .addCommand(vkey)

diff --git a/src/core/index.ts b/src/core/index.ts
@@ -15,7 +15,15 @@ import type {CircuitConfig, CircuitSignals, CircomTester} from '../types';
 import {WitnessTester, ProofTester} from '../testers';
 import {prettyStringify} from '../utils';
 import {CircomkitConfig, DEFAULT, PRIMES, PROTOCOLS} from '../configs';
-import {compileCircuit, instantiateCircuit, readR1CSInfo, getCalldata} from '../functions';
+import {
+  compileCircuit,
+  instantiateCircuit,
+  readR1CSInfo,
+  getCalldata,
+  parseConstraints,
+  readSymbols,
+  stringifyBigIntsWithField,
+} from '../functions';
 import {CircomkitPath} from './pathing';
 
 /**
@@ -132,6 +140,18 @@ export class Circomkit {
     return await readR1CSInfo(this.path.ofCircuit(circuit, 'r1cs'));
   }
 
+  /** Returns human-readable constraint formula array. */
+  async constraints(circuit: string) {
+    const r1csPath = this.path.ofCircuit(circuit, 'r1cs');
+    const symPath = this.path.ofCircuit(circuit, 'sym');
+    // @ts-ignore
+    const r1csFile = await import('r1csfile');
+    const r1cs = await r1csFile.readR1cs(r1csPath, true, true, true);
+    const sym = await readSymbols(symPath);
+    const constraints = stringifyBigIntsWithField(r1cs.curve.Fr, r1cs.constraints);
+    return parseConstraints(constraints, sym, r1cs.prime);
+  }
+
   /** Downloads the phase-1 setup PTAU file for a circuit based on it's number of constraints.
    *
    * The downloaded PTAU files can be seen at [SnarkJS docs](https://github.com/iden3/snarkjs#7-prepare-phase-2).

diff --git a/src/functions/r1cs.ts b/src/functions/r1cs.ts
@@ -1,4 +1,7 @@
 import {ReadPosition, openSync, readSync} from 'fs';
+// @ts-ignore
+import * as fastFile from "fastfile";
+import type {SymbolsType} from '../types/';
 import {primeToName} from '../utils';
 
 /**
@@ -100,6 +103,98 @@ export async function readR1CSInfo(r1csPath: string): Promise<R1CSInfoType> {
   return r1csInfoType;
 }
 
+export async function readSymbols(symFileName: string): Promise<SymbolsType> {
+  const fd = await fastFile.readExisting(symFileName);
+  const buff = await fd.read(fd.totalSize);
+  await fd.close();
+  const symsStr = new TextDecoder("utf-8").decode(buff);
+  const lines = symsStr.split("\n");
+  const out = {};
+  for (let i=0; i<lines.length; i++) {
+    const arr = lines[i].split(",");
+    if (arr.length!=4) continue;
+    // @ts-ignore
+    out[arr[3]] = {
+      labelIdx: Number(arr[0]),
+      varIdx: Number(arr[1]),
+      componentIdx: Number(arr[2]),
+    };
+  }
+  return out;
+}
+
+// @ts-ignore
+export function parseConstraints(constraints, symbols, fieldSize): Promise<string[]> {
+  // @ts-ignore
+  const varsById = Object.entries(symbols).reduce((out, cur) => {
+    // @ts-ignore
+    const id = cur[1].varIdx;
+    if(id !== -1) {
+      // @ts-ignore
+      out[id] = cur[0].slice(5); // Remove main.
+    }
+    return out;
+  }, {});
+
+  // @ts-ignore
+  const parsedConstraints = constraints.map(constraint => {
+    // Every constraint is 3 groups: <1> * <2> - <3> = 0
+    // @ts-ignore
+    const groups = constraint.map(item => {
+      // Each group can contain many signals (with coefficients) summed
+      const vars = Object.keys(item).reduce((out, cur) => {
+        // @ts-ignore
+        const coeffRaw = BigInt(item[cur]);
+        // Display the coefficient as a signed value, helps a lot with -1
+        let coeff = coeffRaw > fieldSize / BigInt(2) ? coeffRaw - fieldSize : coeffRaw;
+        // Reduce numbers that are factors of the field size for better readability
+        // @ts-ignore
+        const modP = BigInt(fieldSize) % BigInt(coeff);
+        // XXX: Why within 10000?
+        if(modP !== BigInt(0) && modP <= BigInt(10000)) {
+          // @ts-ignore
+          coeff = `(p-${fieldSize % coeff})/${fieldSize/coeff}`;
+        }
+        // @ts-ignore
+        const varName = varsById[cur];
+        out.push(
+          // @ts-ignore
+          coeff === BigInt(-1) && varName ? '-' + varName :
+          coeff === BigInt(1) && varName ? varName :
+          !varName ? `${coeff}` :
+          `(${coeff} * ${varName})`,
+        );
+        return out;
+      }, []);
+
+      // Combine all the signals into one statement
+      return vars.reduce((out, cur, index) =>
        // @ts-ignore
+        out + (index > 0 ? cur.startsWith('-') ? ` - ${cur.slice(1)}` : ` + ${cur}` : cur),
+        '');
+    })
+      // @ts-ignore
+      .map(curVar => curVar.indexOf(' ') === -1 ? curVar : `(${curVar})`);
+
+    return (
+      groups[0] +
+      (groups[1] ? ' * ' + groups[1] : '') +
+      (groups[2] ?
+        groups[2].startsWith('-') ?
+          ` + ${groups[2].slice(1)}`
+          : groups[0] || groups[1] ?
+            ' - ' + groups[2]
+            : groups[2].startsWith('(') ?
+              groups[2].slice(1, -1)
+              : groups[2]
+        : '') +
+      ' = 0'
+    );
+  });
+  // @ts-ignore
+  return parsedConstraints;
+}
+
 /** Reads a specified number of bytes from a file and converts them to a `BigInt`.
  *
  * @param offset The position in `buffer` to write the data to.
@@ -113,3 +208,25 @@ export function readBytesFromFile(fd: number, offset: number, length: number, po
 
   return BigInt(`0x${buffer.reverse().toString('hex')}`);
 }
+
+// From Snarkjs
+// @ts-ignore
+export function stringifyBigIntsWithField(Fr, o) {
+    if (o instanceof Uint8Array)  {
+        return Fr.toString(o);
+    } else if (Array.isArray(o)) {
+        return o.map(stringifyBigIntsWithField.bind(null, Fr));
+    } else if (typeof o == "object") {
+        const res = {};
+        const keys = Object.keys(o);
+        keys.forEach( (k) => {
+            // @ts-ignore
+            res[k] = stringifyBigIntsWithField(Fr, o[k]);
+        });
+        return res;
+    } else if ((typeof(o) == "bigint") || o.eq !== undefined)  {
+        return o.toString(10);
+    } else {
+        return o;
+    }
+}
diff --git a/src/testers/witnessTester.ts b/src/testers/witnessTester.ts
@@ -1,5 +1,6 @@
 import {AssertionError} from 'node:assert';
 import type {CircomTester, WitnessType, CircuitSignals, SymbolsType, SignalValueType} from '../types/';
+import {parseConstraints} from '../functions/';
 
 // @todo detect optimized symbols https://github.com/erhant/circomkit/issues/80
 
@@ -138,6 +139,17 @@ export class WitnessTester<IN extends readonly string[] = [], OUT extends readon
     return await this.readWitnessSignals(witness, signals);
   }
 
+  /**
+   * Parse R1CS constraints into human-readable formulas.
+   */
+  async parseConstraints(): Promise<string[]> {
+    await this.loadConstraints();
+    await this.loadSymbols();
+    // @ts-ignore
+    const fieldSize = this.circomTester.witnessCalculator.prime;
+    return parseConstraints(this.constraints, this.symbols, fieldSize);
+  }
+
   /**
    * Override witness value to try and fake a proof. If the circuit has soundness problems (i.e.
    * some signals are not constrained correctly), then you may be able to create a fake witness by
@@ -223,7 +235,7 @@ export class WitnessTester<IN extends readonly string[] = [], OUT extends readon
       const signalDotCount = dotCount(signal) + 1; // +1 for the dot in `main.`
       const signalLength = signal.length + 5; // +5 for prefix `main.`
       const symbolNames = Object.keys(this.symbols!).filter(
-        s => s.startsWith(`main.${signal}`) && signalDotCount === dotCount(s)
+        s => s.match(new RegExp(`^main\\.${signal}(\\[|$|\\.)`)) && signalDotCount === dotCount(s)
       );
 
       // get the symbol values from symbol names, ignoring `main.` prefix

diff --git a/tests/common/circuits.ts b/tests/common/circuits.ts
@@ -7,6 +7,8 @@ type PreparedTestCircuit<S extends Record<string, CircuitSignals>> = {
   signals: S;
   /** Name for the input path to an existing input JSON file under `inputs` folder. */
   inputName: string;
+  /** To compare against generated value. */
+  parsedConstraints: string[];
   /** Circuit information. */
   circuit: {
     /** Circuit name. */
@@ -45,6 +47,17 @@ export function prepareMultiplier(N: number, order: bigint = primes['bn128']) {
   // TOTAL: 3*N - 1
   const size = 3 * N - 1;
 
+  let parsedConstraints;
+  if(N >= 3) {
+    parsedConstraints = [
+      '-in[0] * in[1] + inner[0] = 0',
+      ...Array(N-3).fill(0).map((_, i) => `-inner[${i}] * in[${i+2}] + inner[${i+1}] = 0`),
+      `-inner[${N-3}] * in[${N-1}] + out = 0`,
+      ...Array(N).fill(0).map((_, i) => `isZero[${i}].in * isZero[${i}].inv - 1 = 0`),
+      ...Array(N).fill(0).map((_, i) => `-1 + in[${i}] - isZero[${i}].in = 0`),
+    ];
+  }
+
   const numbers: bigint[] = Array.from({length: N}, () => BigInt(2) + BigInt('0x' + randomBytes(8).toString('hex')));
   const product: bigint = numbers.reduce((prev, acc) => acc * prev) % order;
   const malicious: bigint[] = Array.from({length: N}, () => BigInt(1));
@@ -64,5 +77,6 @@ export function prepareMultiplier(N: number, order: bigint = primes['bn128']) {
     signals,
     circuit: {name, config, size, exact: true},
     inputName: 'input.test',
+    parsedConstraints,
   } as PreparedTestCircuit<typeof signals>;
 }
diff --git a/tests/witnessTester.test.ts b/tests/witnessTester.test.ts
@@ -9,6 +9,7 @@ describe('witness tester', () => {
   const {
     circuit: {name, config, size, exact},
     signals,
+    parsedConstraints,
   } = prepareMultiplier(4);
 
   beforeAll(async () => {
@@ -31,6 +32,10 @@ describe('witness tester', () => {
     // should also work for non-exact too, where we expect at least some amount
     await circuit.expectConstraintCount(size!);
     await circuit.expectConstraintCount(size! - 1);
+
+    const myParsedConstraints = await circuit.parseConstraints();
+    expect(myParsedConstraints).toStrictEqual(parsedConstraints);
+
   });
 
   it('should assert correctly', async () => {