@ -0,0 +1,71 @@ |
|||||
|
/* |
||||
|
Copyright 2018 0KIMS association. |
||||
|
|
||||
|
This file is part of circom (Zero Knowledge Circuit Compiler). |
||||
|
|
||||
|
circom is a free software: you can redistribute it and/or modify it |
||||
|
under the terms of the GNU General Public License as published by |
||||
|
the Free Software Foundation, either version 3 of the License, or |
||||
|
(at your option) any later version. |
||||
|
|
||||
|
circom is distributed in the hope that it will be useful, but WITHOUT |
||||
|
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY |
||||
|
or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public |
||||
|
License for more details. |
||||
|
|
||||
|
You should have received a copy of the GNU General Public License |
||||
|
along with circom. If not, see <https://www.gnu.org/licenses/>. |
||||
|
*/ |
||||
|
|
||||
|
/* |
||||
|
This component creates a binary substraction. |
||||
|
|
||||
|
|
||||
|
Main Constraint: |
||||
|
(in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1)) + |
||||
|
+ 2^n |
||||
|
- (in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1)) |
||||
|
=== |
||||
|
out[0] * 2^0 + out[1] * 2^1 + + out[n-1] *2^(n-1) + aux |
||||
|
|
||||
|
|
||||
|
out[0] * (out[0] - 1) === 0 |
||||
|
out[1] * (out[0] - 1) === 0 |
||||
|
. |
||||
|
. |
||||
|
. |
||||
|
out[n-1] * (out[n-1] - 1) === 0 |
||||
|
aux * (aux-1) == 0 |
||||
|
|
||||
|
*/ |
||||
|
|
||||
|
template BinSub(n) { |
||||
|
signal input in[2][n]; |
||||
|
signal output out[n]; |
||||
|
|
||||
|
signal aux; |
||||
|
|
||||
|
var lin = 2**n; |
||||
|
var lout = 0; |
||||
|
|
||||
|
for (var i=0; i<n; i++) { |
||||
|
lin = lin + in[0][i]*(2**i); |
||||
|
lin = lin - in[1][i]*(2**i); |
||||
|
} |
||||
|
|
||||
|
for (var i=0; i<n; i++) { |
||||
|
out[i] <-- (lin >> i) & 1; |
||||
|
|
||||
|
// Ensure out is binary |
||||
|
out[i] * (out[i] - 1) === 0; |
||||
|
|
||||
|
lout = lout + out[i]*(2**i); |
||||
|
} |
||||
|
|
||||
|
aux <-- (lin >> n) & 1; |
||||
|
aux*(aux-1) === 0; |
||||
|
lout = lout + aux*(2**n); |
||||
|
|
||||
|
// Ensure the sum; |
||||
|
lin === lout; |
||||
|
} |
@ -0,0 +1,56 @@ |
|||||
|
const chai = require("chai"); |
||||
|
const path = require("path"); |
||||
|
const snarkjs = require("snarkjs"); |
||||
|
const compiler = require("circom"); |
||||
|
|
||||
|
const assert = chai.assert; |
||||
|
|
||||
|
const bigInt = snarkjs.bigInt; |
||||
|
|
||||
|
function print(circuit, w, s) { |
||||
|
console.log(s + ": " + w[circuit.getSignalIdx(s)]); |
||||
|
} |
||||
|
|
||||
|
function checkSub(_a,_b, circuit) { |
||||
|
let a=bigInt(_a); |
||||
|
let b=bigInt(_b); |
||||
|
if (a.lesser(bigInt.zero)) a = a.add(bigInt.one.shl(16)); |
||||
|
if (b.lesser(bigInt.zero)) b = b.add(bigInt.one.shl(16)); |
||||
|
const w = circuit.calculateWitness({a: a, b: b}); |
||||
|
|
||||
|
let res = a.sub(b); |
||||
|
if (res.lesser(bigInt.zero)) res = res.add(bigInt.one.shl(16)); |
||||
|
assert( w[circuit.getSignalIdx("main.out")].equals(bigInt(res)) ); |
||||
|
} |
||||
|
|
||||
|
describe("BinSub test", () => { |
||||
|
let circuit; |
||||
|
before( async() => { |
||||
|
const cirDef = await compiler(path.join(__dirname, "circuits", "binsub_test.circom")); |
||||
|
|
||||
|
circuit = new snarkjs.Circuit(cirDef); |
||||
|
|
||||
|
console.log("NConstrains BinSub: " + circuit.nConstraints); |
||||
|
}); |
||||
|
|
||||
|
it("Should check variuos ege cases", async () => { |
||||
|
checkSub(0,0, circuit); |
||||
|
checkSub(1,0, circuit); |
||||
|
checkSub(-1,0, circuit); |
||||
|
checkSub(2,1, circuit); |
||||
|
checkSub(2,2, circuit); |
||||
|
checkSub(2,3, circuit); |
||||
|
checkSub(2,-1, circuit); |
||||
|
checkSub(2,-2, circuit); |
||||
|
checkSub(2,-3, circuit); |
||||
|
checkSub(-2,-3, circuit); |
||||
|
checkSub(-2,-2, circuit); |
||||
|
checkSub(-2,-1, circuit); |
||||
|
checkSub(-2,0, circuit); |
||||
|
checkSub(-2,1, circuit); |
||||
|
checkSub(-2,2, circuit); |
||||
|
checkSub(-2,3, circuit); |
||||
|
}); |
||||
|
|
||||
|
|
||||
|
}); |
@ -0,0 +1,26 @@ |
|||||
|
include "../../circuits/bitify.circom" |
||||
|
include "../../circuits/binsub.circom" |
||||
|
|
||||
|
template A() { |
||||
|
signal private input a; |
||||
|
signal input b; |
||||
|
signal output out; |
||||
|
|
||||
|
component n2ba = Num2Bits(16); |
||||
|
component n2bb = Num2Bits(16); |
||||
|
component sub = BinSub(16); |
||||
|
component b2n = Bits2Num(16); |
||||
|
|
||||
|
n2ba.in <== a; |
||||
|
n2bb.in <== b; |
||||
|
|
||||
|
for (var i=0; i<16; i++) { |
||||
|
sub.in[0][i] <== n2ba.out[i]; |
||||
|
sub.in[1][i] <== n2bb.out[i]; |
||||
|
b2n.in[i] <== sub.out[i]; |
||||
|
} |
||||
|
|
||||
|
out <== b2n.out; |
||||
|
} |
||||
|
|
||||
|
component main = A(); |