diff --git a/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/README.md b/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/README.md new file mode 100644 index 0000000..582ff37 --- /dev/null +++ b/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/README.md @@ -0,0 +1,35 @@ +# Under-Constrained + +* Id: succinctlabs/telepathy-circuits/veridise-V-SUC-VUL-002-simplified +* Project: https://github.com/succinctlabs/telepathy-circuits +* Commit: 9c84fb0f38531718296d9b611f8bd6107f61a9b8 +* Fix Commit: b0c839cef30c3c25ef41d1ad3000081784766934 +* DSL: Circom +* Vulnerability: Under-Constrained +* Location + - Path: circuits/bls_signature.circom + - Function: CoreVerifyPubkeyG1ToyExample + - Line: 77-95 +* Source: Audit Report + - Source Link: https://veridise.com/wp-content/uploads/2023/04/VAR-Succinct.pdf + - Bug ID: V-SUC-VUL-002: Template CoreVerifyPubkeyG1 does not perform input validation +* Commands + - Setup Environment: `./zkbugs_setup.sh` + - Reproduce: `./zkbugs_exploit.sh` + - Compile and Preprocess: `./zkbugs_compile_setup.sh` + - Positive Test: `./zkbugs_positive_test.sh` + - Find Exploit: `./zkbugs_find_exploit.sh` + - Clean: `./zkbugs_clean.sh` + +## Short Description of the Vulnerability + +This bug is in the circom-pairing BLS signature verification logic. pubkey, signature and hash are divided into 7-entry chunks of 55-bit data, and each entry is checked against according entry in `p`. When calling `BigLessThan()`, the output isn't verified therefore attacker can manipulate the input so that it overflows p. + +## Short Description of the Exploit + +The circuit had been simplified to demonstrate the bug, the attack idea is calculating a `delta` such that it makes the input overflow but still bounded by 2**55 - 1 to pass the range check inside `BigLessThan()`. In reality, attacker would bruteforce a special set of inputs satisfying a list of constraints. The details are explained in the PR comment. + +## Proposed Mitigation + +In each iteration of the for loop, add a constraint `lt[idx].out === 1` to make sure the input is indeed bounded by `p`. + diff --git a/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/circuits/bigint.circom b/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/circuits/bigint.circom new file mode 100644 index 0000000..9c0b9c3 --- /dev/null +++ b/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/circuits/bigint.circom @@ -0,0 +1,989 @@ +pragma circom 2.0.3; + +include "../../../dependencies/circomlib/circuits/comparators.circom"; +include "../../../dependencies/circomlib/circuits/bitify.circom"; +include "../../../dependencies/circomlib/circuits/gates.circom"; + +include "bigint_func.circom"; + +// addition mod 2**n with carry bit +template ModSum(n) { + assert(n <= 252); + signal input a; + signal input b; + signal output sum; + signal output carry; + + component n2b = Num2Bits(n + 1); + n2b.in <== a + b; + carry <== n2b.out[n]; + sum <== a + b - carry * (1 << n); +} + +// check if k-register variables a, b are equal everywhere +template BigIsEqual(k) { + signal input a[k]; + signal input b[k]; + signal output out; + + component isEquals[k]; + var total = k; + for (var i = 0; i < k; i ++) { + isEquals[i] = IsEqual(); + isEquals[i].in[0] <== a[i]; + isEquals[i].in[1] <== b[i]; + total -= isEquals[i].out; + } + component checkZero = IsZero(); + checkZero.in <== total; + out <== checkZero.out; +} + +// check if k-register variable a is equal to zero +template BigIsZero(k) { + signal input in[k]; + signal output out; + + component isZeros[k]; + var total = k; + for (var i = 0; i < k; i ++) { + isZeros[i] = IsZero(); + isZeros[i].in <== in[i]; + total -= isZeros[i].out; + } + component checkZero = IsZero(); + checkZero.in <== total; + out <== checkZero.out; +} + + +// a - b +template ModSub(n) { + assert(n <= 252); + signal input a; + signal input b; + signal output out; + signal output borrow; + component lt = LessThan(n); + lt.in[0] <== a; + lt.in[1] <== b; + borrow <== lt.out; + out <== borrow * (1 << n) + a - b; +} + +// a - b - c +// assume a - b - c + 2**n >= 0 +template ModSubThree(n) { + assert(n + 2 <= 253); + signal input a; + signal input b; + signal input c; + assert(a - b - c + (1 << n) >= 0); + signal output out; + signal output borrow; + signal b_plus_c; + b_plus_c <== b + c; + component lt = LessThan(n + 1); + lt.in[0] <== a; + lt.in[1] <== b_plus_c; + borrow <== lt.out; + out <== borrow * (1 << n) + a - b_plus_c; +} + +template ModSumThree(n) { + assert(n + 2 <= 253); + signal input a; + signal input b; + signal input c; + signal output sum; + signal output carry; + + component n2b = Num2Bits(n + 2); + n2b.in <== a + b + c; + carry <== n2b.out[n] + 2 * n2b.out[n + 1]; + sum <== a + b + c - carry * (1 << n); +} + +template ModSumFour(n) { + assert(n + 2 <= 253); + signal input a; + signal input b; + signal input c; + signal input d; + signal output sum; + signal output carry; + + component n2b = Num2Bits(n + 2); + n2b.in <== a + b + c + d; + carry <== n2b.out[n] + 2 * n2b.out[n + 1]; + sum <== a + b + c + d - carry * (1 << n); +} + +// product mod 2**n with carry +template ModProd(n) { + assert(n <= 126); + signal input a; + signal input b; + signal output prod; + signal output carry; + + component n2b = Num2Bits(2 * n); + n2b.in <== a * b; + + component b2n1 = Bits2Num(n); + component b2n2 = Bits2Num(n); + var i; + for (i = 0; i < n; i++) { + b2n1.in[i] <== n2b.out[i]; + b2n2.in[i] <== n2b.out[i + n]; + } + prod <== b2n1.out; + carry <== b2n2.out; +} + +// split a n + m bit input into two outputs +template Split(n, m) { + assert(n <= 126); + signal input in; + signal output small; + signal output big; + + small <-- in % (1 << n); + big <-- in \ (1 << n); + + component n2b_small = Num2Bits(n); + n2b_small.in <== small; + component n2b_big = Num2Bits(m); + n2b_big.in <== big; + + in === small + big * (1 << n); +} + +// split a n + m + k bit input into three outputs +template SplitThree(n, m, k) { + assert(n <= 126); + signal input in; + signal output small; + signal output medium; + signal output big; + + small <-- in % (1 << n); + medium <-- (in \ (1 << n)) % (1 << m); + big <-- in \ (1 << n + m); + + component n2b_small = Num2Bits(n); + n2b_small.in <== small; + component n2b_medium = Num2Bits(m); + n2b_medium.in <== medium; + component n2b_big = Num2Bits(k); + n2b_big.in <== big; + + in === small + medium * (1 << n) + big * (1 << n + m); +} + +// a[i], b[i] in 0... 2**n-1 +// represent a = a[0] + a[1] * 2**n + .. + a[k - 1] * 2**(n * k) +template BigAdd(n, k) { + assert(n <= 252); + signal input a[k]; + signal input b[k]; + signal output out[k + 1]; + + component unit0 = ModSum(n); + unit0.a <== a[0]; + unit0.b <== b[0]; + out[0] <== unit0.sum; + + component unit[k - 1]; + for (var i = 1; i < k; i++) { + unit[i - 1] = ModSumThree(n); + unit[i - 1].a <== a[i]; + unit[i - 1].b <== b[i]; + if (i == 1) { + unit[i - 1].c <== unit0.carry; + } else { + unit[i - 1].c <== unit[i - 2].carry; + } + out[i] <== unit[i - 1].sum; + } + out[k] <== unit[k - 2].carry; +} + +/* +Polynomial Multiplication +Inputs: + - a = a[0] + a[1] * X + ... + a[k-1] * X^{k-1} + - b = b[0] + b[1] * X + ... + b[k-1] * X^{k-1} +Output: + - out = out[0] + out[1] * X + ... + out[2 * k - 2] * X^{2*k - 2} + - out = a * b as polynomials in X +Notes: + - Optimization due to xJsnark: + -- witness is calculated by normal polynomial multiplication + -- out is contrained by evaluating out(X) === a(X) * b(X) at X = 0, ..., 2*k - 2 + - If a[i], b[j] have absolute value < B, then out[i] has absolute value < k * B^2 +m_out is the expected max number of bits in the output registers +*/ +template BigMultShortLong(n, k, m_out) { + assert(n <= 126); + signal input a[k]; + signal input b[k]; + signal output out[2 * k - 1]; + + var prod_val[2 * k - 1]; + for (var i = 0; i < 2 * k - 1; i++) { + prod_val[i] = 0; + if (i < k) { + for (var a_idx = 0; a_idx <= i; a_idx++) { + prod_val[i] = prod_val[i] + a[a_idx] * b[i - a_idx]; + } + } else { + for (var a_idx = i - k + 1; a_idx < k; a_idx++) { + prod_val[i] = prod_val[i] + a[a_idx] * b[i - a_idx]; + } + } + out[i] <-- prod_val[i]; + } + + var k2 = 2 * k - 1; + var pow[k2][k2]; // we cache the exponent values because it makes a big difference in witness generation time + for(var i = 0; i 1) { + var sumAndCarry[2] = SplitFn(split[0][1] + split[1][0], n, n); + out[1] <-- sumAndCarry[0]; + carry[1] = sumAndCarry[1]; + } + if (k > 2) { + for (var i = 2; i < k; i++) { + var sumAndCarry[2] = SplitFn(split[i][0] + split[i-1][1] + split[i-2][2] + carry[i-1], n, n); + out[i] <-- sumAndCarry[0]; + carry[i] = sumAndCarry[1]; + } + out[k] <-- split[k-1][1] + split[k-2][2] + carry[k-1]; + } + + component outRangeChecks[k+1]; + for (var i = 0; i < k+1; i++) { + outRangeChecks[i] = Num2Bits(n); + outRangeChecks[i].in <== out[i]; + } + + signal runningCarry[k]; + component runningCarryRangeChecks[k]; + runningCarry[0] <-- (in[0] - out[0]) / (1 << n); + runningCarryRangeChecks[0] = Num2Bits(n + log_ceil(k)); + runningCarryRangeChecks[0].in <== runningCarry[0]; + runningCarry[0] * (1 << n) === in[0] - out[0]; + for (var i = 1; i < k; i++) { + runningCarry[i] <-- (in[i] - out[i] + runningCarry[i-1]) / (1 << n); + runningCarryRangeChecks[i] = Num2Bits(n + log_ceil(k)); + runningCarryRangeChecks[i].in <== runningCarry[i]; + runningCarry[i] * (1 << n) === in[i] - out[i] + runningCarry[i-1]; + } + runningCarry[k-1] === out[k]; +} + +template BigMult(n, k) { + signal input a[k]; + signal input b[k]; + signal output out[2 * k]; + + var LOGK = log_ceil(k); + component mult = BigMultShortLong(n, k, 2*n + LOGK); + for (var i = 0; i < k; i++) { + mult.a[i] <== a[i]; + mult.b[i] <== b[i]; + } + + // no carry is possible in the highest order register + component longshort = LongToShortNoEndCarry(n, 2 * k - 1); + for (var i = 0; i < 2 * k - 1; i++) { + longshort.in[i] <== mult.out[i]; + } + for (var i = 0; i < 2 * k; i++) { + out[i] <== longshort.out[i]; + } +} + +/* +Inputs: + - BigInts a, b +Output: + - out = (a < b) ? 1 : 0 +*/ +template BigLessThan(n, k){ + signal input a[k]; + signal input b[k]; + signal output out; + + component lt[k]; + component eq[k]; + for (var i = 0; i < k; i++) { + lt[i] = LessThan(n); + lt[i].in[0] <== a[i]; + lt[i].in[1] <== b[i]; + eq[i] = IsEqual(); + eq[i].in[0] <== a[i]; + eq[i].in[1] <== b[i]; + } + + // ors[i] holds (lt[k - 1] || (eq[k - 1] && lt[k - 2]) .. || (eq[k - 1] && .. && lt[i])) + // ands[i] holds (eq[k - 1] && .. && lt[i]) + // eq_ands[i] holds (eq[k - 1] && .. && eq[i]) + component ors[k - 1]; + component ands[k - 1]; + component eq_ands[k - 1]; + for (var i = k - 2; i >= 0; i--) { + ands[i] = AND(); + eq_ands[i] = AND(); + ors[i] = OR(); + + if (i == k - 2) { + ands[i].a <== eq[k - 1].out; + ands[i].b <== lt[k - 2].out; + eq_ands[i].a <== eq[k - 1].out; + eq_ands[i].b <== eq[k - 2].out; + ors[i].a <== lt[k - 1].out; + ors[i].b <== ands[i].out; + } else { + ands[i].a <== eq_ands[i + 1].out; + ands[i].b <== lt[i].out; + eq_ands[i].a <== eq_ands[i + 1].out; + eq_ands[i].b <== eq[i].out; + ors[i].a <== ors[i + 1].out; + ors[i].b <== ands[i].out; + } + } + out <== ors[0].out; +} + +// leading register of b should be non-zero +template BigMod(n, k) { + assert(n <= 126); + signal input a[2 * k]; + signal input b[k]; + + signal output div[k + 1]; + signal output mod[k]; + + var longdiv[2][50] = long_div(n, k, a, b); + for (var i = 0; i < k; i++) { + div[i] <-- longdiv[0][i]; + mod[i] <-- longdiv[1][i]; + } + div[k] <-- longdiv[0][k]; + component div_range_checks[k + 1]; + for (var i = 0; i <= k; i++) { + div_range_checks[i] = Num2Bits(n); + div_range_checks[i].in <== div[i]; + } + component mod_range_checks[k]; + for (var i = 0; i < k; i++) { + mod_range_checks[i] = Num2Bits(n); + mod_range_checks[i].in <== mod[i]; + } + + component mul = BigMult(n, k + 1); + for (var i = 0; i < k; i++) { + mul.a[i] <== div[i]; + mul.b[i] <== b[i]; + } + mul.a[k] <== div[k]; + mul.b[k] <== 0; + + for (var i = 0; i < 2 * k + 2; i++) { + //log(mul.out[i]); + } + + component add = BigAdd(n, 2 * k + 2); + for (var i = 0; i < 2 * k; i++) { + add.a[i] <== mul.out[i]; + if (i < k) { + add.b[i] <== mod[i]; + } else { + add.b[i] <== 0; + } + } + add.a[2 * k] <== mul.out[2 * k]; + add.a[2 * k + 1] <== mul.out[2 * k + 1]; + add.b[2 * k] <== 0; + add.b[2 * k + 1] <== 0; + + for (var i = 0; i < 2 * k + 2; i++) { + //log(add.out[i]); + } + + for (var i = 0; i < 2 * k; i++) { + add.out[i] === a[i]; + } + add.out[2 * k] === 0; + add.out[2 * k + 1] === 0; + + component lt = BigLessThan(n, k); + for (var i = 0; i < k; i++) { + lt.a[i] <== mod[i]; + lt.b[i] <== b[i]; + } + lt.out === 1; +} + +// copied from BigMod to allow a to have m registers and use long_div2 +template BigMod2(n, k, m) { + assert(n <= 126); + signal input a[m]; + signal input b[k]; + + signal output div[m - k + 1]; + signal output mod[k]; + + var longdiv[2][50] = long_div2(n, k, m-k, a, b); + for (var i = 0; i < k; i++) { + mod[i] <-- longdiv[1][i]; + } + for (var i = 0; i <= m-k; i++) { + div[i] <-- longdiv[0][i]; + } + component div_range_checks[m - k + 1]; + for (var i = 0; i <= m-k; i++) { + div_range_checks[i] = Num2Bits(n); + div_range_checks[i].in <== div[i]; + } + component mod_range_checks[k]; + for (var i = 0; i < k; i++) { + mod_range_checks[i] = Num2Bits(n); + mod_range_checks[i].in <== mod[i]; + } + + component mul = BigMult(n, m-k + 1); + // this might need to be optimized since b has less registers than div + for (var i = 0; i < k; i++) { + mul.a[i] <== div[i]; + mul.b[i] <== b[i]; + } + for (var i = k; i <= m-k; i++) { + mul.a[i] <== div[i]; + mul.b[i] <== 0; + } + + // mul shouldn't have more registers than a + for (var i = m; i < 2*(m-k)+2; i++) { + mul.out[i] === 0; + } + + component add = BigAdd(n, m); + for (var i = 0; i < m; i++) { + add.a[i] <== mul.out[i]; + if (i < k) { + add.b[i] <== mod[i]; + } else { + add.b[i] <== 0; + } + } + + for (var i = 0; i < m; i++) { + add.out[i] === a[i]; + } + add.out[m] === 0; + + component lt = BigLessThan(n, k); + for (var i = 0; i < k; i++) { + lt.a[i] <== mod[i]; + lt.b[i] <== b[i]; + } + lt.out === 1; +} + + + +// a[i], b[i] in 0... 2**n-1 +// represent a = a[0] + a[1] * 2**n + .. + a[k - 1] * 2**(n * k) +// calculates (a+b)%p, where 0<= a,b < p +template BigAddModP(n, k){ + assert(n <= 252); + signal input a[k]; + signal input b[k]; + signal input p[k]; + signal output out[k]; + + component add = BigAdd(n,k); + for (var i = 0; i < k; i++) { + add.a[i] <== a[i]; + add.b[i] <== b[i]; + } + component lt = BigLessThan(n, k+1); + for (var i = 0; i < k; i++) { + lt.a[i] <== add.out[i]; + lt.b[i] <== p[i]; + } + lt.a[k] <== add.out[k]; + lt.b[k] <== 0; + + component sub = BigSub(n,k+1); + for (var i = 0; i < k; i++) { + sub.a[i] <== add.out[i]; + sub.b[i] <== (1-lt.out) * p[i]; + } + sub.a[k] <== add.out[k]; + sub.b[k] <== 0; + + sub.out[k] === 0; + for (var i = 0; i < k; i++) { + out[i] <== sub.out[i]; + } +} + +/* +Inputs: + - BigInts a, b + - Assume a >= b +Output: + - BigInt out = a - b + - underflow = how much is borrowed at the highest digit of subtraction, only nonzero if a < b +*/ +template BigSub(n, k) { + assert(n <= 252); + signal input a[k]; + signal input b[k]; + signal output out[k]; + signal output underflow; + + component unit0 = ModSub(n); + unit0.a <== a[0]; + unit0.b <== b[0]; + out[0] <== unit0.out; + + component unit[k - 1]; + for (var i = 1; i < k; i++) { + unit[i - 1] = ModSubThree(n); + unit[i - 1].a <== a[i]; + unit[i - 1].b <== b[i]; + if (i == 1) { + unit[i - 1].c <== unit0.borrow; + } else { + unit[i - 1].c <== unit[i - 2].borrow; + } + out[i] <== unit[i - 1].out; + } + underflow <== unit[k - 2].borrow; +} + +// calculates (a - b) % p, where a, b < p +// note: does not assume a >= b +template BigSubModP(n, k){ + assert(n <= 252); + signal input a[k]; + signal input b[k]; + signal input p[k]; + signal output out[k]; + component sub = BigSub(n, k); + for (var i = 0; i < k; i++){ + sub.a[i] <== a[i]; + sub.b[i] <== b[i]; + } + signal flag; + flag <== sub.underflow; + component add = BigAdd(n, k); + for (var i = 0; i < k; i++){ + add.a[i] <== sub.out[i]; + add.b[i] <== p[i]; + } + signal tmp[k]; + for (var i = 0; i < k; i++){ + tmp[i] <== (1 - flag) * sub.out[i]; + out[i] <== tmp[i] + flag * add.out[i]; + } +} + +// Note: deprecated +template BigMultModP(n, k) { + assert(n <= 252); + signal input a[k]; + signal input b[k]; + signal input p[k]; + signal output out[k]; + + component big_mult = BigMult(n, k); + for (var i = 0; i < k; i++) { + big_mult.a[i] <== a[i]; + big_mult.b[i] <== b[i]; + } + component big_mod = BigMod(n, k); + for (var i = 0; i < 2 * k; i++) { + big_mod.a[i] <== big_mult.out[i]; + } + for (var i = 0; i < k; i++) { + big_mod.b[i] <== p[i]; + } + for (var i = 0; i < k; i++) { + out[i] <== big_mod.mod[i]; + } +} + +template BigModInv(n, k) { + assert(n <= 252); + signal input in[k]; + signal input p[k]; + signal output out[k]; + + // length k + var inv[50] = mod_inv(n, k, in, p); + for (var i = 0; i < k; i++) { + out[i] <-- inv[i]; + } + component range_checks[k]; + for (var i = 0; i < k; i++) { + range_checks[i] = Num2Bits(n); + range_checks[i].in <== out[i]; + } + + component mult = BigMult(n, k); + for (var i = 0; i < k; i++) { + mult.a[i] <== in[i]; + mult.b[i] <== out[i]; + } + component mod = BigMod(n, k); + for (var i = 0; i < 2 * k; i++) { + mod.a[i] <== mult.out[i]; + } + for (var i = 0; i < k; i++) { + mod.b[i] <== p[i]; + } + mod.mod[0] === 1; + for (var i = 1; i < k; i++) { + mod.mod[i] === 0; + } +} + +/* Taken from circom-ecdsa +Input: + - in = in[0] + in[1] * X + ... + in[k-1] * X^{k-1} as signed overflow representation + - Assume each in[i] is in range (-2^{m-1}, 2^{m-1}) +Implements: + - constrain that in[] evaluated at X = 2^n as a big integer equals zero +*/ +template CheckCarryToZero(n, m, k) { + assert(k >= 2); + + var EPSILON = 1; // see below for why 1 is ok + + signal input in[k]; + + signal carry[k]; + component carryRangeChecks[k]; + for (var i = 0; i < k-1; i++){ + carryRangeChecks[i] = Num2Bits(m + EPSILON - n); + if( i == 0 ){ + carry[i] <-- in[i] / (1<= k, we precompute X^i = r[i] mod p, where r[i] represented as k registers with r[i][j] in [0, 2^n) + - in[i] * X^i is replaced by sum_j in[i] * r[i][j] * X^j +Notes: + - If each in[i] has absolute value 2*l-1) ? 2*k-1 : 2*l-1; + var pow[k2][k2]; + for(var i = 0; i la + lb -1) ? ka + kb - 1 : la + lb -1; + var pow[k2][k2]; + for(var i = 0; i b) + return a; + return b; +} + +function log_ceil(n) { + var n_temp = n; + for (var i = 0; i < 254; i++) { + if (n_temp == 0) { + return i; + } + n_temp = n_temp \ 2; + } + return 254; +} + +function SplitFn(in, n, m) { + return [in % (1 << n), (in \ (1 << n)) % (1 << m)]; +} + +function SplitThreeFn(in, n, m, k) { + return [in % (1 << n), (in \ (1 << n)) % (1 << m), (in \ (1 << n + m)) % (1 << k)]; +} + +// 1 if true, 0 if false +function long_gt(n, k, a, b) { + for (var i = k - 1; i >= 0; i--) { + if (a[i] > b[i]) { + return 1; + } + if (a[i] < b[i]) { + return 0; + } + } + return 0; +} + +function long_is_zero(k, a){ + for(var idx=0; idx k2 +// output has k1+1 registers +function long_add_unequal(n, k1, k2, a, b){ + var carry = 0; + var sum[50]; + for(var i=0; i= b +function long_sub(n, k, a, b) { + var diff[50]; + var borrow[50]; + for (var i = 0; i < k; i++) { + if (i == 0) { + if (a[i] >= b[i]) { + diff[i] = a[i] - b[i]; + borrow[i] = 0; + } else { + diff[i] = a[i] - b[i] + (1 << n); + borrow[i] = 1; + } + } else { + if (a[i] >= b[i] + borrow[i - 1]) { + diff[i] = a[i] - b[i] - borrow[i - 1]; + borrow[i] = 0; + } else { + diff[i] = (1 << n) + a[i] - b[i] - borrow[i - 1]; + borrow[i] = 1; + } + } + } + return diff; +} + +// a is a n-bit scalar +// b has k registers +function long_scalar_mult(n, k, a, b) { + var out[50]; + for (var i = 0; i < 50; i++) { + out[i] = 0; + } + for (var i = 0; i < k; i++) { + var temp = out[i] + (a * b[i]); + out[i] = temp % (1 << n); + out[i + 1] = out[i + 1] + temp \ (1 << n); + } + return out; +} + + +// n bits per register +// a has k + m registers +// b has k registers +// out[0] has length m + 1 -- quotient +// out[1] has length k -- remainder +// implements algorithm of https://people.eecs.berkeley.edu/~fateman/282/F%20Wright%20notes/week4.pdf +// b[k-1] must be nonzero! +function long_div2(n, k, m, a, b){ + var out[2][50]; + // assume k+m < 50 + var remainder[50]; + for (var i = 0; i < m + k; i++) { + remainder[i] = a[i]; + } + + var dividend[50]; + for (var i = m; i >= 0; i--) { + if (i == m) { + dividend[k] = 0; + for (var j = k - 1; j >= 0; j--) { + dividend[j] = remainder[j + m]; + } + } else { + for (var j = k; j >= 0; j--) { + dividend[j] = remainder[j + i]; + } + } + out[0][i] = short_div(n, k, dividend, b); + var mult_shift[50] = long_scalar_mult(n, k, out[0][i], b); + var subtrahend[50]; + for (var j = 0; j < m + k; j++) { + subtrahend[j] = 0; + } + for (var j = 0; j <= k; j++) { + if (i + j < m + k) { + subtrahend[i + j] = mult_shift[j]; + } + } + remainder = long_sub(n, m + k, remainder, subtrahend); + } + for (var i = 0; i < k; i++) { + out[1][i] = remainder[i]; + } + out[1][k] = 0; + return out; +} + +function long_div(n, k, a, b) { + return long_div2(n, k, k, a, b); +} + +// n bits per register +// a has k + 1 registers +// b has k registers +// assumes leading digit of b is at least 2^(n - 1) +// 0 <= a < (2**n) * b +function short_div_norm(n, k, a, b) { + var qhat = (a[k] * (1 << n) + a[k - 1]) \ b[k - 1]; + if (qhat > (1 << n) - 1) { + qhat = (1 << n) - 1; + } + + var mult[50] = long_scalar_mult(n, k, qhat, b); + if (long_gt(n, k + 1, mult, a) == 1) { + mult = long_sub(n, k + 1, mult, b); + if (long_gt(n, k + 1, mult, a) == 1) { + return qhat - 2; + } else { + return qhat - 1; + } + } else { + return qhat; + } +} + +// n bits per register +// a has k + 1 registers +// b has k registers +// assumes leading digit of b is non-zero +// 0 <= a < b * 2^n +function short_div(n, k, a, b) { + var scale = (1 << n) \ (1 + b[k - 1]); + // k + 2 registers now + var norm_a[50] = long_scalar_mult(n, k + 1, scale, a); + // k + 1 registers now + var norm_b[50] = long_scalar_mult(n, k, scale, b); + + var ret; + if (norm_b[k] != 0) { + ret = short_div_norm(n, k + 1, norm_a, norm_b); + } else { + ret = short_div_norm(n, k, norm_a, norm_b); + } + return ret; +} + +// a = a0 + a1 * X + ... + a[k-1] * X^{k-1} with X = 2^n +// a_i can be "negative" assume a_i in (-2^251, 2^251) +// output is the value of a with a_i all of the same sign +// out[50] = 0 if positive, 1 if negative +function signed_long_to_short(n, k, a){ + var out[51]; + var MAXL = 50; + var temp[51]; + + // is a positive? + for(var i=0; i= 0){ // circom automatically takes care of signs in comparator + out[i] = temp[i] % X; + temp[i+1] += temp[i] \ X; + }else{ + var borrow = (-temp[i] + X - 1 ) \ X; + out[i] = temp[i] + borrow * X; + temp[i+1] -= borrow; + } + } + if(temp[MAXL] >= 0){ + assert(temp[MAXL]==0); // otherwise not enough registers! + out[MAXL] = 0; + return out; + } + + // must be negative then, reset + for(var i=0; i 1) { + var sumAndCarry[2] = SplitFn(split[0][1] + split[1][0], n, n); + out[1] = sumAndCarry[0]; + carry[1] = sumAndCarry[1]; + } + if (2 * k - 1 > 2) { + for (var i = 2; i < 2 * k - 1; i++) { + var sumAndCarry[2] = SplitFn(split[i][0] + split[i-1][1] + split[i-2][2] + carry[i-1], n, n); + out[i] = sumAndCarry[0]; + carry[i] = sumAndCarry[1]; + } + out[2 * k - 1] = split[2*k-2][1] + split[2*k-3][2] + carry[2*k-2]; + } + return out; +} + + +// n bits per register +// a and b both have l x k registers +// out has length 2l - 1 x 2k +// adapted from BigMultShortLong2D and LongToShortNoEndCarry2 witness computation +function prod2D(n, k, l, a, b) { + // first compute the intermediate values. taken from BigMulShortLong + var prod_val[20][50]; // length is 2l - 1 by 2k - 1 + for (var i = 0; i < 2 * k - 1; i++) { + for (var j = 0; j < 2 * l - 1; j ++) { + prod_val[j][i] = 0; + } + } + for (var i1 = 0; i1 < k; i1 ++) { + for (var i2 = 0; i2 < k; i2 ++) { + for (var j1 = 0; j1 < l; j1 ++) { + for (var j2 = 0; j2 < l; j2 ++) { + prod_val[j1+j2][i1+i2] = prod_val[j1+j2][i1+i2] + a[j1][i1] * b[j2][i2]; + } + } + } + } + + // now do a bunch of carrying to make sure registers not overflowed. taken from LongToShortNoEndCarry2 + var out[20][50]; // length is 2 * l by 2 * k + + var split[20][50][3]; // second dimension has length 2 * k - 1 + for (var j = 0; j < 2 * l - 1; j ++) { + for (var i = 0; i < 2 * k - 1; i++) { + split[j][i] = SplitThreeFn(prod_val[j][i], n, n, n); + } + } + + var carry[20][50]; // length is 2l-1 x 2k + var sumAndCarry[20][2]; + for ( var j = 0; j < 2 * l - 1; j ++) { + carry[j][0] = 0; + out[j][0] = split[j][0][0]; + if (2 * k - 1 > 1) { + sumAndCarry[j] = SplitFn(split[j][0][1] + split[j][1][0], n, n); + out[j][1] = sumAndCarry[j][0]; + carry[j][1] = sumAndCarry[j][1]; + } + if (2 * k - 1 > 2) { + for (var i = 2; i < 2 * k - 1; i++) { + sumAndCarry[j] = SplitFn(split[j][i][0] + split[j][i-1][1] + split[j][i-2][2] + carry[j][i-1], n, n); + out[j][i] = sumAndCarry[j][0]; + carry[j][i] = sumAndCarry[j][1]; + } + out[j][2 * k - 1] = split[j][2*k-2][1] + split[j][2*k-3][2] + carry[j][2*k-2]; + } + } + + return out; +} + +// Put all modular arithmetic, aka F_p field stuff, at the end + +function long_add_mod(n, k, a, b, p) { + var sum[50] = long_add(n,k,a,b); + var temp[2][50] = long_div2(n,k,1,sum,p); + return temp[1]; +} + +function long_sub_mod(n, k, a, b, p) { + if(long_gt(n, k, b, a) == 1){ + return long_add(n, k, a, long_sub(n,k,p,b)); + }else{ + return long_sub(n, k, a, b); + } +} + +function prod_mod(n, k, a, b, p) { + var prod[50] = prod(n,k,a,b); + var temp[2][50] = long_div(n,k,prod,p); + return temp[1]; +} + + +// n bits per register +// a has k registers +// p has k registers +// e has k registers +// k * n <= 500 +// p is a prime +// computes a^e mod p +function mod_exp(n, k, a, p, e) { + var eBits[500]; // length is k * n + var bitlength; + for (var i = 0; i < k; i++) { + for (var j = 0; j < n; j++) { + eBits[j + n * i] = (e[i] >> j) & 1; + if(eBits[j + n * i] == 1) + bitlength = j + n * i + 1; + } + } + + var out[50]; // length is k + for (var i = 0; i < 50; i++) { + out[i] = 0; + } + out[0] = 1; + + // repeated squaring + for (var i = bitlength-1; i >= 0; i--) { + // multiply by a if bit is 0 + if (eBits[i] == 1) { + var temp[50]; // length 2 * k + temp = prod(n, k, out, a); + var temp2[2][50]; + temp2 = long_div(n, k, temp, p); + out = temp2[1]; + } + + // square, unless we're at the end + if (i > 0) { + var temp[50]; // length 2 * k + temp = prod(n, k, out, out); + var temp2[2][50]; + temp2 = long_div(n, k, temp, p); + out = temp2[1]; + } + + } + return out; +} + +// n bits per register +// a has k registers +// p has k registers +// k * n <= 500 +// p is a prime +// if a == 0 mod p, returns 0 +// else computes inv = a^(p-2) mod p +function mod_inv(n, k, a, p) { + var isZero = 1; + for (var i = 0; i < k; i++) { + if (a[i] != 0) { + isZero = 0; + } + } + if (isZero == 1) { + var ret[50]; + for (var i = 0; i < k; i++) { + ret[i] = 0; + } + return ret; + } + + var pCopy[50]; + for (var i = 0; i < 50; i++) { + if (i < k) { + pCopy[i] = p[i]; + } else { + pCopy[i] = 0; + } + } + + var two[50]; + for (var i = 0; i < 50; i++) { + two[i] = 0; + } + two[0] = 2; + + var pMinusTwo[50]; + pMinusTwo = long_sub(n, k, pCopy, two); // length k + var out[50]; + out = mod_exp(n, k, a, pCopy, pMinusTwo); + return out; +} + diff --git a/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/circuits/bls12_381_func.circom b/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/circuits/bls12_381_func.circom new file mode 100644 index 0000000..19ed1f7 --- /dev/null +++ b/dataset/circom/succinctlabs_telepathy-circuits/veridise_template_CoreVerifyPubkeyG1_does_not_perform_input_validation_simplified_original/circuits/bls12_381_func.circom @@ -0,0 +1,2933 @@ +pragma circom 2.0.3; + + +function get_BLS12_381_parameter(){ + return 15132376222941642752; +} + +function get_BLS12_381_prime(n, k){ + var p[50]; + assert( (n==96 && k==4) || (n==77 && k==5) || (n==55 && k==7)); + if( n==96 && k==4 ){ + p = [54880396502181392957329877675, 31935979117156477062286671870, 20826981314825584179608359615, 8047903782086192180586325942]; + } + if( n==77 && k==5 ){ + p = [151110683138771015150251, 101672770061349971921567, 5845403419599137187901, 110079541992039310225047, 7675079137884323292337]; + } + if( n==55 && k==7 ){ + p = [35747322042231467, 36025922209447795, 1084959616957103, 7925923977987733, 16551456537884751, 23443114579904617, 1829881462546425]; + } + return p; +} + +// half of 8th roots of unity, up to negation +function get_roots_of_unity(n, k){ + assert( n == 55 && k == 7 ); + var roots[4][2][50]; + for(var idx=0; idx