todo sudoku

circuits/sudoku.circom

@@ -0,0 +1,79 @@
+pragma circom 2.0.0;
+
+// Assert that two elements are not equal.
+// Done via the check if in0 - in1 is non-zero.
+template NonEqual() {
+  signal input in0;
+  signal input in1;
+  signal inv;
+
+  inv <-- 1/ (in0 - in1);
+  inv*(in0 - in1) === 1;
+}
+
+// Assert that all given values are unique
+template Distinct(n) {
+  signal input in[n];
+  component nonEqual[n][n];
+  for(var i = 0; i < n; i++){
+    for(var j = 0; j < i; j++){
+      nonEqual[i][j] = NonEqual();
+      nonEqual[i][j].in0 <== in[i];
+      nonEqual[i][j].in1 <== in[j];
+    }
+  }
+}
+
+// Enforce that 0 <= in < 16
+template Bits4() {
+  signal input in;
+  signal bits[4];
+  var bitsum = 0;
+  for (var i = 0; i < 4; i++) {
+    bits[i] <-- (in >> i) & 1;
+    bits[i] * (bits[i] - 1) === 0;
+    bitsum = bitsum + 2 ** i * bits[i];
+  }
+  bitsum === in;
+}
+
+// Check if a given signal is in range [1, 9]
+template OneToNine() {
+  signal input in;
+  component lowerBound = Bits4();
+  component upperBound = Bits4();
+  lowerBound.in <== in - 1;
+  upperBound.in <== in + 6;
+}
+
+template Sudoku(n) {
+  // solution is a 2D array: indices are (row_i, col_i)
+  signal input solution[n][n];
+  // puzzle is the same, but a zero indicates a blank
+  signal input puzzle[n][n];
+
+  // make sure the solution agrees with the puzzle
+	// meaning that non-empty cells of the puzzle should equal to the corresponding solution value
+  // other values of the puzzle must be 0 (empty cell)
+  for (var row_i = 0; row_i < n; row_i++) {
+    for (var col_i = 0; col_i < n; col_i++) {
+      puzzle[row_i][col_i] * (puzzle[row_i][col_i] - solution[row_i][col_i]) === 0;
+    } 
+  }
+
+  // ensure all values in the solution are distinct and in range
+  component inRange[n][n];
+  component distinct[n];
+  for (var row_i = 0; row_i < n; row_i++) {
+    for (var col_i = 0; col_i < n; col_i++) {
+      if (row_i == 0) {
+        distinct[col_i] = Distinct(n);
+      }
+      inRange[row_i][col_i] = OneToNine();
+      inRange[row_i][col_i].in <== solution[row_i][col_i];
+      distinct[col_i].in[row_i] <== solution[row_i][col_i];
+    }
+  }
+}
+
+component main {public[puzzle]} = Sudoku(9);

inputs/sudoku/default.json

@@ -0,0 +1,24 @@
+{
+  "solution": [
+    ["1", "9", "4", "8", "6", "5", "2", "3", "7"],
+    ["7", "3", "5", "4", "1", "2", "9", "6", "8"],
+    ["8", "6", "2", "3", "9", "7", "1", "4", "5"],
+    ["9", "2", "1", "7", "4", "8", "3", "5", "6"],
+    ["6", "7", "8", "5", "3", "1", "4", "2", "9"],
+    ["4", "5", "3", "9", "2", "6", "8", "7", "1"],
+    ["3", "8", "9", "6", "5", "4", "7", "1", "2"],
+    ["2", "4", "6", "1", "7", "9", "5", "8", "3"],
+    ["5", "1", "7", "2", "8", "3", "6", "9", "4"]
+  ],
+  "puzzle": [
+    ["0", "0", "0", "8", "6", "0", "2", "3", "0"],
+    ["7", "0", "5", "0", "0", "0", "9", "0", "8"],
+    ["0", "6", "0", "3", "0", "7", "0", "4", "0"],
+    ["0", "2", "0", "7", "0", "8", "0", "5", "0"],
+    ["0", "7", "8", "5", "0", "0", "0", "0", "0"],
+    ["4", "0", "0", "9", "0", "6", "0", "7", "0"],
+    ["3", "0", "9", "0", "5", "0", "7", "0", "2"],
+    ["0", "4", "0", "1", "0", "9", "0", "8", "0"],
+    ["5", "0", "7", "0", "8", "0", "0", "9", "4"]
+  ]
+}

tests/sudoku.test.ts

@@ -0,0 +1,74 @@
+import {compileCircuit} from '../utils';
+import {Circuit} from '../utils/circuit';
+import type {FullProof} from '../types/circuit';
+import type {WasmTester} from '../types/wasmTester';
+import {assert, expect} from 'chai';
+
+const CIRCUIT_NAME = 'sudoku';
+describe(CIRCUIT_NAME, () => {
+  const INPUT = {
+    solution: [
+      ['1', '9', '4', '8', '6', '5', '2', '3', '7'],
+      ['7', '3', '5', '4', '1', '2', '9', '6', '8'],
+      ['8', '6', '2', '3', '9', '7', '1', '4', '5'],
+      ['9', '2', '1', '7', '4', '8', '3', '5', '6'],
+      ['6', '7', '8', '5', '3', '1', '4', '2', '9'],
+      ['4', '5', '3', '9', '2', '6', '8', '7', '1'],
+      ['3', '8', '9', '6', '5', '4', '7', '1', '2'],
+      ['2', '4', '6', '1', '7', '9', '5', '8', '3'],
+      ['5', '1', '7', '2', '8', '3', '6', '9', '4'],
+    ],
+    puzzle: [
+      ['0', '0', '0', '8', '6', '0', '2', '3', '0'],
+      ['7', '0', '5', '0', '0', '0', '9', '0', '8'],
+      ['0', '6', '0', '3', '0', '7', '0', '4', '0'],
+      ['0', '2', '0', '7', '0', '8', '0', '5', '0'],
+      ['0', '7', '8', '5', '0', '0', '0', '0', '0'],
+      ['4', '0', '0', '9', '0', '6', '0', '7', '0'],
+      ['3', '0', '9', '0', '5', '0', '7', '0', '2'],
+      ['0', '4', '0', '1', '0', '9', '0', '8', '0'],
+      ['5', '0', '7', '0', '8', '0', '0', '9', '4'],
+    ],
+  };
+
+  describe('functionality', () => {
+    let circuit: WasmTester;
+
+    before(async () => {
+      circuit = await compileCircuit(CIRCUIT_NAME);
+    });
+
+    it('should compute correctly', async () => {
+      // compute witness
+      const witness = await circuit.calculateWitness(INPUT, true);
+
+      // witness should have valid constraints
+      await circuit.checkConstraints(witness);
+
+      // witness should have correct output
+      // await circuit.assertOut(witness, {
+      //   main: INPUT.puzzle,
+      // });
+    });
+  });
+
+  describe('validation', () => {
+    let fullProof: FullProof;
+
+    const circuit = new Circuit(CIRCUIT_NAME);
+
+    before(async () => {
+      fullProof = await circuit.prove(INPUT);
+    });
+
+    it('should verify', async () => {
+      expect(await circuit.verify(fullProof.proof, fullProof.publicSignals)).to.be.true;
+    });
+
+    it('should NOT verify a wrong puzzle', async () => {
+      // just give a prime number, assuming there are no factors of 1
+      // TODO; provide wrong answer
+      expect(await circuit.verify(fullProof.proof, ['13'])).to.be.false;
+    });
+  });
+});