From 1d7d953c3aff80961b880bcd63991ff7d22fca98 Mon Sep 17 00:00:00 2001 From: Erhan Tezcan Date: Mon, 20 Feb 2023 20:56:09 +0300 Subject: [PATCH] todo sudoku --- circuits/sudoku.circom | 79 ++++++++++++++++++++++++++++++++++++++ inputs/sudoku/default.json | 24 ++++++++++++ tests/sudoku.test.ts | 74 +++++++++++++++++++++++++++++++++++ 3 files changed, 177 insertions(+) create mode 100644 circuits/sudoku.circom create mode 100644 inputs/sudoku/default.json create mode 100644 tests/sudoku.test.ts diff --git a/circuits/sudoku.circom b/circuits/sudoku.circom new file mode 100644 index 0000000..d1555fd --- /dev/null +++ b/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); diff --git a/inputs/sudoku/default.json b/inputs/sudoku/default.json new file mode 100644 index 0000000..428ee62 --- /dev/null +++ b/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"] + ] +} diff --git a/tests/sudoku.test.ts b/tests/sudoku.test.ts new file mode 100644 index 0000000..0122739 --- /dev/null +++ b/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; + }); + }); +});