Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
970 changes: 970 additions & 0 deletions circuits/bigInt/bigInt.circom

Large diffs are not rendered by default.

561 changes: 561 additions & 0 deletions circuits/bigInt/bigIntFunc.circom

Large diffs are not rendered by default.

435 changes: 435 additions & 0 deletions circuits/bigInt/bigIntOverflow.circom

Large diffs are not rendered by default.

53 changes: 53 additions & 0 deletions circuits/bigInt/karatsuba.circom
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
pragma circom 2.1.6;

// Calculates 2 numbers with CHUNK_NUMBER multiplication using karatsuba method
// out is overflowed
// use only for 2 ** k CHUNK_NUMBER, othewise u will get error
// here is no check for CHUNK_SIZE <= 126, maybe will be added later
template KaratsubaNoCarry(CHUNK_NUMBER) {
signal input in[2][CHUNK_NUMBER];
signal output out[2 * CHUNK_NUMBER];
signal input dummy;

if (CHUNK_NUMBER == 1) {
out[0] <== in[0][0] * in[1][0];
} else {
component karatsubaA1B1 = KaratsubaNoCarry(CHUNK_NUMBER / 2);
component karatsubaA2B2 = KaratsubaNoCarry(CHUNK_NUMBER / 2);
component karatsubaA1A2B1B2 = KaratsubaNoCarry(CHUNK_NUMBER / 2);
karatsubaA2B2.dummy <== dummy;
karatsubaA1B1.dummy <== dummy;
karatsubaA1A2B1B2.dummy <== dummy;

for (var i = 0; i < CHUNK_NUMBER / 2; i++) {
karatsubaA1B1.in[0][i] <== in[0][i];
karatsubaA1B1.in[1][i] <== in[1][i];
karatsubaA2B2.in[0][i] <== in[0][i + CHUNK_NUMBER / 2];
karatsubaA2B2.in[1][i] <== in[1][i + CHUNK_NUMBER / 2];
karatsubaA1A2B1B2.in[0][i] <== in[0][i] + in[0][i + CHUNK_NUMBER / 2];
karatsubaA1A2B1B2.in[1][i] <== in[1][i] + in[1][i + CHUNK_NUMBER / 2];
}

for (var i = 0; i < 2 * CHUNK_NUMBER; i++) {
if (i < CHUNK_NUMBER) {
if (CHUNK_NUMBER / 2 <= i && i < 3 * (CHUNK_NUMBER / 2)) {
out[i] <== karatsubaA1B1.out[i]
+ karatsubaA1A2B1B2.out[i - CHUNK_NUMBER / 2]
- karatsubaA1B1.out[i - CHUNK_NUMBER / 2]
- karatsubaA2B2.out[i - CHUNK_NUMBER / 2] + dummy * dummy;
} else {
out[i] <== karatsubaA1B1.out[i] + dummy * dummy;
}
} else {
if (CHUNK_NUMBER / 2 <= i && i < 3 * (CHUNK_NUMBER / 2)) {
out[i] <== karatsubaA2B2.out[i - CHUNK_NUMBER]
+ karatsubaA1A2B1B2.out[i - CHUNK_NUMBER / 2]
- karatsubaA1B1.out[i - CHUNK_NUMBER / 2]
- karatsubaA2B2.out[i - CHUNK_NUMBER / 2] + dummy * dummy;
} else {
out[i] <== karatsubaA2B2.out[i - CHUNK_NUMBER] + dummy * dummy;
}
}
}
}
}
244 changes: 244 additions & 0 deletions circuits/bitify/bitGates.circom
Original file line number Diff line number Diff line change
@@ -0,0 +1,244 @@
pragma circom 2.1.6;

// Here are templates for all bit gates for any 1 or 2 inputs
// for 1-input gates interface is input in and output out
// for 2-input gates interface is input in[2] and output out
// 3-input gates may be added later


//One input gates
//------------------------------------------------------------------------------------------------------------------------------------------------

// a
// 0 -> 0
// 1 -> 1
template BUFFER(){
signal input in;
signal output out;

out <== in;
}

// !a
// !0 = 1
// !1 = 0
template NOT(){
signal input in;
signal output out;

out <== 1 - in;
}


//------------------------------------------------------------------------------------------------------------------------------------------------
//Two input gates
//------------------------------------------------------------------------------------------------------------------------------------------------


// a ∧ b
// 0 ∧ 0 = 0
// 1 ∧ 0 = 0
// 0 ∧ 1 = 0
// 1 ∧ 1 = 1
template AND(){
signal input in[2];
signal output out;

out <== in[0] * in[1];
}

// a ∨ b
// 0 ∨ 0 = 0
// 1 ∨ 0 = 1
// 0 ∨ 1 = 1
// 1 ∨ 1 = 1
template OR(){
signal input in[2];
signal output out;

out <== in[0] + in[1] - in[0] * in[1];
}

// !(a ∧ b)
// !(0 ∧ 0) = 1
// !(1 ∧ 0) = 1
// !(0 ∧ 1) = 1
// !(1 ∧ 1) = 0
template NAND(){
signal input in[2];
signal output out;

out <== 1 - in[0] * in[1];
}

// !(a ∨ b)
// !(0 ∨ 0) = 1
// !(1 ∨ 0) = 0
// !(0 ∨ 1) = 0
// !(1 ∨ 1) = 0
template NOR(){
signal input in[2];
signal output out;

out <== 1 - in[0] + in[1] + in[0] * in[1];
}

// A ⊕ B
// 0 ⊕ 0 = 0
// 1 ⊕ 0 = 1
// 0 ⊕ 1 = 1
// 1 ⊕ 1 = 0
template XOR(){
signal input in[2];
signal output out;

out <== in[0] + in[1] - 2 * in[0] * in[1];
}

// !(A ⊕ B)
// !(0 ⊕ 0) = 1
// !(1 ⊕ 0) = 0
// !(0 ⊕ 1) = 0
// !(1 ⊕ 1) = 1
template XNOR(){
signal input in[2];
signal output out;

out <== 1 - in[0] - in[1] + 2 * in[0] * in[1];
}

// A → B
// 0 → 0 = 1
// 1 → 0 = 1
// 0 → 1 = 0
// 1 → 1 = 1
template IMPLY(){
signal input in[2];
signal output out;

out <== 1 - in[0] + in[1] - (1 - in[0]) * in[1];
}

// !(A → B)
// !(0 → 0) = 0
// !(1 → 0) = 0
// !(0 → 1) = 1
// !(1 → 1) = 0
template NIMPLY(){
signal input in[2];
signal output out;

out <== in[0] - in[1] + (1 - in[0]) * in[1];
}

// A
// 0 0 -> 0
// 1 0 -> 1
// 0 1 -> 0
// 1 1 -> 1
template A(){
signal input in[2];
signal output out;

out <== in[0];
}

// !A
// 0 0 -> 1
// 1 0 -> 0
// 0 1 -> 1
// 1 1 -> 0
template NOTA(){
signal input in[2];
signal output out;

out <== 1 - in[0];
}

// B
// 0 0 -> 0
// 1 0 -> 0
// 0 1 -> 1
// 1 1 -> 1
template B(){
signal input in[2];
signal output out;

out <== in[1];
}

// !B
// 0 0 -> 1
// 1 0 -> 1
// 0 1 -> 0
// 1 1 -> 0
template NOTB(){
signal input in[2];
signal output out;

out <== 1 - in[1];
}


// true
// 0 0 -> 1
// 1 0 -> 1
// 0 1 -> 1
// 1 1 -> 1
template TRUE(){
signal input in[2];
signal output out;

out <== 1;
}

// true
// 0 0 -> 0
// 1 0 -> 0
// 0 1 -> 0
// 1 1 -> 0
template FALSE(){
signal input in[2];
signal output out;

out <== 0;
}

// B → A
// 0 0 -> 0
// 1 0 -> 1
// 0 1 -> 0
// 1 1 -> 0
template INVIMPLY(){
signal input in[2];
signal output out;

out <== 1 + in[0] - in[1] - in[0] * (1 - in[1]);
}

// !(B → A)
// 0 0 -> 1
// 1 0 -> 0
// 0 1 -> 1
// 1 1 -> 1
template NINVNIMPLY(){
signal input in[2];
signal output out;

out <== in[1] - in[0] + in[0] * (1 - in[1]);
}

// Xor for n pairs
template Xor2(n) {
signal input in1[n];
signal input in2[n];
signal output out[n];

for (var k = 0; k < n; k++) {
out[k] <== in1[k] + in2[k] - 2 * in1[k] * in2[k];
}
}

//------------------------------------------------------------------------------------------------------------------------------------------------
//Three input gates (not all cases!!!)
//------------------------------------------------------------------------------------------------------------------------------------------------
55 changes: 55 additions & 0 deletions circuits/bitify/bitify.circom
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
pragma circom 2.1.6;

// Here is operation to convert number to bit array and bit array to number
// There are reasons for code to look so bad
// We don`t use loop because of circom compiler
// Circom compiler just ignores linear constraints (only +):
// if u compile circuits with only linear constraints with --O2 flag (maybe --O1 too), there will be 0 constraints
// It means that u can can put literally anything in witness and get valid proof, and we don`t want this to happen
// To avoid it we must use quadratic constraints (where * is).
// Here we use bit * bit instead bit in one place of constraint, and it doesn`t affects logic (0 * 0 == 0 and 1 * 1 == 1)
// Where we can`t use it we use dummy input - it must be zero to pass dummy * dummy === 0 check, and add it to any linear constaint:
// signal a <== b + c + dummy * dummy;
// Nothing changes for arithmetic, but we turned linear contraint into quadratic, any compiler optimisation will not affect it.
// Hope this will be changed in future circom version, but this is the best way to deal with it for now.

//------------------------------------------------------------------------------------------------------------------------------------------------------------------

// Convert number to bit array of len
// We are checking if out[i] is a bit, so LEN + 1 constraints
template Num2Bits(LEN){
assert(LEN <= 253);
assert(LEN > 0);
signal input in;
signal output out[LEN];
for (var i = 0; i < LEN; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] - 1) === 0;
}
signal sum[LEN];
sum[0] <== out[0] * out[0];
for (var i = 1; i < LEN; i++){
sum[i] <== 2 ** i * out[i] + sum[i - 1];
}

in === sum[LEN - 1];
}


//------------------------------------------------------------------------------------------------------------------------------------------------------------------
// Here bit check is not present, use only with bits else error will appear!!!
// No bit check so only 1 constarint
template Bits2Num(LEN){
assert(LEN <= 253);
assert(LEN > 0);
signal input in[LEN];
signal output out;

signal sum[LEN];
sum[0] <== in[0] * in[0];

for (var i = 1; i < LEN; i++){
sum[i] <== 2 ** i * in[i] + sum[i - 1];
}
out <== sum[LEN-1];
}
Loading
Loading