implement signature verification

This commit is contained in:
turnoffthiscomputer
2024-09-17 16:28:38 +02:00
parent d79f1c2eec
commit efcf097a40
8 changed files with 356 additions and 197 deletions

View File

@@ -1,16 +1,11 @@
pragma circom 2.1.6;
// include "circomlib/circuits/poseidon.circom";
// include "@zk-email/circuits/utils/bytes.circom";
// include "./passport_verifier_sha256WithRSAEncryption_65537.circom";
// include "./utils/chunk_data.circom";
// include "./utils/compute_pubkey_leaf.circom";
include "../utils/passport/customHashers.circom";
include "../utils/computeCommitment.circom";
include "../utils/passport/computeCommitment.circom";
include "../utils/passport/signatureAlgorithm.circom";
include "../utils/passport/passportVerifier.circom";
template OPENPASSPORT_REGISTER(signatureAlgorithm, n, k, max_padded_econtent_len, max_padded_signed_attr_len) {
template OPENPASSPORT_REGISTER(signatureAlgorithm, n, k, MAX_ECONTENT_PADDED_LEN, MAX_SIGNED_ATTR_PADDED_LEN) {
var kLengthFactor = getKLengthFactor(signatureAlgorithm);
var kScaled = k * kLengthFactor;
@@ -18,9 +13,9 @@ template OPENPASSPORT_REGISTER(signatureAlgorithm, n, k, max_padded_econtent_len
signal input dsc_secret;
signal input dg1[93];
signal input dg1_hash_offset;
signal input econtent[max_padded_econtent_len];
signal input econtent[MAX_ECONTENT_PADDED_LEN];
signal input econtent_padded_length;
signal input signed_attr[max_padded_signed_attr_len];
signal input signed_attr[MAX_SIGNED_ATTR_PADDED_LEN];
signal input signed_attr_padded_length;
signal input signed_attr_econtent_hash_offset;
signal input signature[kScaled];
@@ -29,10 +24,8 @@ template OPENPASSPORT_REGISTER(signatureAlgorithm, n, k, max_padded_econtent_len
signal input attestation_id;
// var hashlen = getHashLength(signatureAlgorithm);
// passport verifier
PassportVerifier(signatureAlgorithm, n, k, max_padded_econtent_len, max_padded_signed_attr_len)(dg1,dg1_hash_offset,econtent);
PassportVerifier(signatureAlgorithm, n, k, MAX_ECONTENT_PADDED_LEN, MAX_SIGNED_ATTR_PADDED_LEN)(dg1,dg1_hash_offset,econtent,econtent_padded_length, signed_attr, signed_attr_padded_length, signed_attr_econtent_hash_offset, pubKey, signature);
// leaf
signal leaf <== LeafHasher(kScaled)(pubKey, signatureAlgorithm);

View File

@@ -19,5 +19,4 @@ template ComputeCommitment() {
poseidon_hasher.inputs[i + 3] <== dg1_packed[i];
}
out <== poseidon_hasher.out;
// out <== leaf;
}

View File

@@ -1,23 +1,32 @@
pragma circom 2.1.6;
include "@zk-email/circuits/lib/rsa.circom";
include "@zk-email/circuits/utils/bytes.circom";
include "@zk-email/circuits/utils/array.circom";
include "../shaBytes/shaBytesStatic.circom";
include "../shaBytes/shaBytesDynamic.circom";
include "./signatureAlgorithm.circom";
include "./signatureVerifier.circom";
template PassportVerifier(signatureAlgorithm, n, k, MAX_ECONTENT_LEN, MAX_SIGNED_ATTR_LEN) {
var kLengthFactor = getKLengthFactor(signatureAlgorithm);
var kScaled = k * kLengthFactor;
var HASH_LEN_BITS = getHashLength(signatureAlgorithm);
var HASH_LEN_BYTES = HASH_LEN_BITS / 8;
signal input dg1[93];
signal input dg1_hash_offset;
signal input econtent[MAX_ECONTENT_LEN];
signal input econtent_padded_length;
signal input signed_attr[MAX_SIGNED_ATTR_LEN];
signal input signed_attr_padded_length;
signal input signed_attr_econtent_hash_offset;
signal input pubKey[kScaled];
signal input signature[kScaled];
// compute hash of DG1
signal dg1Sha[HASH_LEN_BITS] <== ShaBytesStatic(HASH_LEN_BITS, 93)(dg1);
component dg1ShaBytes[HASH_LEN_BYTES];
for (var i = 0; i < HASH_LEN_BYTES; i++) {
dg1ShaBytes[i] = Bits2Num(8);
@@ -26,10 +35,33 @@ template PassportVerifier(signatureAlgorithm, n, k, MAX_ECONTENT_LEN, MAX_SIGNED
}
}
// assert DG1 hash matches the one in eContent input
signal dg1Hash[HASH_LEN_BYTES] <== SelectSubArray(MAX_ECONTENT_LEN, HASH_LEN_BYTES)(econtent, dg1_hash_offset, HASH_LEN_BYTES);
// assert DG1 hash matches the one in econtent input
signal dg1Hash[HASH_LEN_BYTES] <== SelectSubArray(MAX_ECONTENT_LEN, HASH_LEN_BYTES)(econtent, dg1_hash_offset, HASH_LEN_BYTES); // TODO: use varShifLeft instead
for(var i = 0; i < HASH_LEN_BYTES; i++) {
dg1Hash[i] === dg1ShaBytes[i].out;
}
// compute hash of econtent
signal eContentSha[HASH_LEN_BITS] <== ShaBytesDynamic(HASH_LEN_BITS,MAX_ECONTENT_LEN)(econtent, econtent_padded_length);
component eContentShaBytes[HASH_LEN_BYTES];
for (var i = 0; i < HASH_LEN_BYTES; i++) {
eContentShaBytes[i] = Bits2Num(8);
for (var j = 0; j < 8; j++) {
eContentShaBytes[i].in[7 - j] <== eContentSha[i * 8 + j];
}
}
// assert econtent hash matches the one in signedAttr
signal eContentHashInSignedAttr[HASH_LEN_BYTES] <== SelectSubArray(MAX_SIGNED_ATTR_LEN, HASH_LEN_BYTES)(signed_attr, signed_attr_econtent_hash_offset, HASH_LEN_BYTES); // TODO: use varShifLeft instead
for(var i = 0; i < HASH_LEN_BYTES; i++) {
eContentHashInSignedAttr[i] === eContentShaBytes[i].out;
}
// compute hash of signedAttr
signal signedAttrSha[HASH_LEN_BITS] <== ShaBytesDynamic(HASH_LEN_BITS, MAX_SIGNED_ATTR_LEN)(signed_attr, signed_attr_padded_length);
SignatureVerifier(signatureAlgorithm, n, k)(signedAttrSha, pubKey, signature);
}

View File

@@ -0,0 +1,46 @@
pragma circom 2.1.6;
include "./signatureAlgorithm.circom";
include "../circom-ecdsa/ecdsa.circom";
template Secp256r1Verifier(signatureAlgorithm, n, k) {
var kLengthFactor = getKLengthFactor(signatureAlgorithm);
var kScaled = k * kLengthFactor;
var HASH_LEN_BITS = getHashLength(signatureAlgorithm);
var msg_len = (HASH_LEN_BITS + n) \ n;
signal input signature[kScaled];
signal input pubKey[kScaled];
signal input hashParsed[msg_len];
// 43 * 6 = 258;
signal msgHash[6];
for(var i = 0; i < msg_len; i++) {
msgHash[i] <== hashParsed[i];
}
signal signature_r[k]; // ECDSA signature component r
signal signature_s[k]; // ECDSA signature component s
signal pubKey_x[k];
signal pubKey_y[k];
for (var i = 0; i < k; i++) {
signature_r[i] <== signature[i];
signature_s[i] <== signature[i + k];
pubKey_x[i] <== pubKey[i];
pubKey_y[i] <== pubKey[i + k];
}
signal pubkey_xy[2][k] <== [pubKey_x, pubKey_y];
// verify eContentHash signature
component ecdsa_verify = ECDSAVerifyNoPubkeyCheck(n, k);
ecdsa_verify.r <== signature_r;
ecdsa_verify.s <== signature_s;
ecdsa_verify.msghash <== msgHash;
ecdsa_verify.pubkey <== pubkey_xy;
1 === ecdsa_verify.result;
}

View File

@@ -69,11 +69,15 @@ function getKLengthFactor(signatureAlgorithm) {
}
function getExponentBits(signatureAlgorithm) {
// returns the amounts of bits of the exponent of type 2^n +1
if (signatureAlgorithm == 1 ) {
return 16;
return 17; // 65537
}
if (signatureAlgorithm == 3) {
return 1;
if (signatureAlgorithm == 3 ) {
return 17;
}
if (signatureAlgorithm == 4 ) {
return 17;
}
return 0;

View File

@@ -0,0 +1,87 @@
pragma circom 2.1.6;
include "@zk-email/circuits/lib/rsa.circom";
include "../rsa/rsaPkcs1.circom";
include "../circom-ecdsa/ecdsa.circom";
include "secp256r1Verifier.circom";
include "../rsapss/rsapss.circom";
template SignatureVerifier(signatureAlgorithm, n, k) {
var kLengthFactor = getKLengthFactor(signatureAlgorithm);
var kScaled = k * kLengthFactor;
var HASH_LEN_BITS = getHashLength(signatureAlgorithm);
signal input hash[HASH_LEN_BITS];
signal input pubKey[kScaled];
signal input signature[kScaled];
var msg_len = (HASH_LEN_BITS + n) \ n;
signal hashParsed[msg_len] <== HashParser(signatureAlgorithm, n, k)(hash);
if (signatureAlgorithm == 1) {
component rsa = RSAVerifier65537(n, k);
for (var i = 0; i < msg_len; i++) {
rsa.message[i] <== hashParsed[i];
}
for (var i = msg_len; i < k; i++) {
rsa.message[i] <== 0;
}
rsa.modulus <== pubKey;
rsa.signature <== signature;
}
if (signatureAlgorithm == 3 ) {
component rsa_pkcs1 = RSAVerifier65537_pkcs1(n, k);
for (var i = 0; i < msg_len; i++) {
rsa_pkcs1.message[i] <== hashParsed[i];
}
for (var i = msg_len; i < k; i++) {
rsa_pkcs1.message[i] <== 0;
}
rsa_pkcs1.modulus <== pubKey;
rsa_pkcs1.signature <== signature;
}
if (signatureAlgorithm == 4) {
var exponentBits = getExponentBits(signatureAlgorithm);
var pubKeyBitsLength = getKeyLength(signatureAlgorithm);
component rsaPssSha256Verification = VerifyRsaPssSig(n, k, exponentBits, HASH_LEN_BITS, pubKeyBitsLength);
rsaPssSha256Verification.pubkey <== pubKey;
rsaPssSha256Verification.signature <== signature;
rsaPssSha256Verification.hashed <== hash; // send the raw hash
}
if (signatureAlgorithm == 7) {
Secp256r1Verifier (signatureAlgorithm,n,k)(signature, pubKey,hashParsed);
}
if (signatureAlgorithm == 8) {
Secp256r1Verifier (signatureAlgorithm,n,k)(signature, pubKey,hashParsed);
}
if (signatureAlgorithm == 9) {
}
}
template HashParser(signatureAlgorithm, n, k) {
var HASH_LEN_BITS = getHashLength(signatureAlgorithm);
var msg_len = (HASH_LEN_BITS + n) \ n;
component hashParser[msg_len];
signal input hash[HASH_LEN_BITS];
for (var i = 0; i < msg_len; i++) {
hashParser[i] = Bits2Num(n);
}
for (var i = 0; i < HASH_LEN_BITS; i++) {
hashParser[i \ n].in[i % n] <== hash[HASH_LEN_BITS - 1 - i];
}
for (var i = HASH_LEN_BITS; i < n * msg_len; i++) {
hashParser[i \ n].in[i % n] <== 0;
}
signal output hashParsed[msg_len];
for (var i = 0; i < msg_len ; i++ ){
hashParsed[i] <== hashParser[i].out;
}
}

View File

@@ -5,7 +5,7 @@ include "@zk-email/circuits/lib/fp.circom";
// Computes base^65537 mod modulus
// Does not necessarily reduce fully mod modulus (the answer could be
// too big by a multiple of modulus)
template FpPow65537Mod(n, k) {
template FpPow65537Mod_pkcs1(n, k) {
signal input base[k];
// Exponent is hardcoded at 65537
signal input modulus[k];
@@ -42,9 +42,9 @@ template FpPow65537Mod(n, k) {
}
}
template RSAPad(n, k) {
template RSAPad_pkcs1(n, k) {
signal input modulus[k];
signal input base_message[k];
signal input message[k];
signal output padded_message[k];
var base_len = 280;
@@ -58,7 +58,7 @@ template RSAPad(n, k) {
signal base_message_bits[n*k];
for (var i = 0; i < k; i++) {
base_message_n2b[i] = Num2Bits(n);
base_message_n2b[i].in <== base_message[i];
base_message_n2b[i].in <== message[i];
for (var j = 0; j < n; j++) {
base_message_bits[i*n+j] <== base_message_n2b[i].out[j];
}
@@ -121,15 +121,15 @@ template RSAPad(n, k) {
}
}
template RSAVerify65537(n, k) {
template RSAVerifier65537_pkcs1(n, k) {
signal input signature[k];
signal input modulus[k];
signal input base_message[k];
signal input message[k];
component padder = RSAPad(n, k);
component padder = RSAPad_pkcs1(n, k);
for (var i = 0; i < k; i++) {
padder.modulus[i] <== modulus[i];
padder.base_message[i] <== base_message[i];
padder.message[i] <== message[i];
}
// Check that the signature is in proper form and reduced mod modulus.
@@ -143,7 +143,7 @@ template RSAVerify65537(n, k) {
}
bigLessThan.out === 1;
component bigPow = FpPow65537Mod(n, k);
component bigPow = FpPow65537Mod_pkcs1(n, k);
for (var i = 0; i < k; i++) {
bigPow.base[i] <== signature[i];
bigPow.modulus[i] <== modulus[i];

View File

@@ -1,11 +1,9 @@
pragma circom 2.1.6;
include "@zk-email/circuits/lib/bigint.circom";
include "../circom-ecdsa/bigInt.circom";
include "../circom-ecdsa/bigInt_func.circom";
// w = 32
// e_bits = 17
// nb is the length of the base and modulus
// calculates (base^exp) % modulus, exp = 2^(e_bits - 1) + 1 = 2^16 + 1
template PowerMod(w, nb, e_bits) {
assert(e_bits >= 2);
@@ -17,7 +15,7 @@ template PowerMod(w, nb, e_bits) {
component muls[e_bits];
for (var i = 0; i < e_bits; i++) {
muls[i] = BigMultModP(w, nb);
muls[i] = BigMultModP_rsapss(w, nb);
for (var j = 0; j < nb; j++) {
muls[i].p[j] <== modulus[j];
@@ -46,8 +44,8 @@ template PowerMod(w, nb, e_bits) {
}
}
// Note: deprecated
template BigMultModP(n, k) {
// // Note: deprecated
template BigMultModP_rsapss(n, k) {
assert(n <= 252);
signal input a[k];
signal input b[k];
@@ -59,7 +57,7 @@ template BigMultModP(n, k) {
big_mult.a[i] <== a[i];
big_mult.b[i] <== b[i];
}
component big_mod = BigMod(n, k);
component big_mod = BigMod_rsapss(n, k);
for (var i = 0; i < 2 * k; i++) {
big_mod.a[i] <== big_mult.out[i];
}
@@ -71,121 +69,121 @@ template BigMultModP(n, k) {
}
}
template BigMult(n, k) {
signal input a[k];
signal input b[k];
signal output out[2 * 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];
}
// 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];
}
}
// // 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];
// }
// }
template LongToShortNoEndCarry(n, k) {
assert(n <= 126);
signal input in[k];
signal output out[k+1];
// template LongToShortNoEndCarry(n, k) {
// assert(n <= 126);
// signal input in[k];
// signal output out[k+1];
var split[k][3];
for (var i = 0; i < k; i++) {
split[i] = SplitThreeFn(in[i], n, n, n);
}
// var split[k][3];
// for (var i = 0; i < k; i++) {
// split[i] = SplitThreeFn(in[i], n, n, n);
// }
var carry[k];
carry[0] = 0;
out[0] <-- split[0][0];
if (k > 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];
}
// var carry[k];
// carry[0] = 0;
// out[0] <-- split[0][0];
// if (k > 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];
}
// 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 BigMultShortLong(n, k, m_out) {
assert(n <= 126);
signal input a[k];
signal input b[k];
signal output out[2 * k - 1];
// 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 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 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<k2; i++)for(var j=0; j<k2; j++)
pow[i][j] = i ** j;
// 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<k2; i++)for(var j=0; j<k2; j++)
// pow[i][j] = i ** j;
var a_poly[2 * k - 1];
var b_poly[2 * k - 1];
var out_poly[2 * k - 1];
for (var i = 0; i < 2 * k - 1; i++) {
out_poly[i] = 0;
a_poly[i] = 0;
b_poly[i] = 0;
for (var j = 0; j < 2 * k - 1; j++) {
out_poly[i] = out_poly[i] + out[j] * pow[i][j];
}
for (var j = 0; j < k; j++) {
a_poly[i] = a_poly[i] + a[j] * pow[i][j];
b_poly[i] = b_poly[i] + b[j] * pow[i][j];
}
}
for (var i = 0; i < 2 * k - 1; i++) {
out_poly[i] === a_poly[i] * b_poly[i];
}
}
template BigMod(n, k) {
// var a_poly[2 * k - 1];
// var b_poly[2 * k - 1];
// var out_poly[2 * k - 1];
// for (var i = 0; i < 2 * k - 1; i++) {
// out_poly[i] = 0;
// a_poly[i] = 0;
// b_poly[i] = 0;
// for (var j = 0; j < 2 * k - 1; j++) {
// out_poly[i] = out_poly[i] + out[j] * pow[i][j];
// }
// for (var j = 0; j < k; j++) {
// a_poly[i] = a_poly[i] + a[j] * pow[i][j];
// b_poly[i] = b_poly[i] + b[j] * pow[i][j];
// }
// }
// for (var i = 0; i < 2 * k - 1; i++) {
// out_poly[i] === a_poly[i] * b_poly[i];
// }
// }
template BigMod_rsapss(n, k) {
assert(n <= 126);
signal input a[2 * k];
signal input b[k];
@@ -253,71 +251,71 @@ template BigMod(n, k) {
}
lt.out === 1;
}
template BigAdd(n, k) {
assert(n <= 252);
signal input a[k];
signal input b[k];
signal output out[k + 1];
// 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 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;
}
// 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;
// }
template ModSum(n) {
assert(n <= 252);
signal input a;
signal input b;
signal output sum;
signal output carry;
// 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);
}
// component n2b = Num2Bits(n + 1);
// n2b.in <== a + b;
// carry <== n2b.out[n];
// sum <== a + b - carry * (1 << n);
// }
template ModSumThree(n) {
assert(n + 2 <= 253);
signal input a;
signal input b;
signal input c;
signal output sum;
signal output carry;
// 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);
}
function SplitFn(in, n, m) {
return [in % (1 << n), (in \ (1 << n)) % (1 << m)];
}
// 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);
// }
// 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)];
}
// function SplitThreeFn(in, n, m, k) {
// return [in % (1 << n), (in \ (1 << n)) % (1 << m), (in \ (1 << n + m)) % (1 << k)];
// }
function long_div_2(n, k, a, b) {
return long_div2(n, k, k, a, b);
return long_div_rsapss(n, k, k, a, b);
}
function long_div2(n, k, m, a, b){
function long_div_rsapss(n, k, m, a, b){
var out[2][150];
// assume k+m < 150
var remainder[150];