Circom में एक symbolic variable वह variable होता है जिसे किसी signal से वैल्यू असाइन की गई हो।

जब किसी signal को किसी variable में असाइन किया जाता है (जिससे वह एक symbolic variable बन जाता है), तो वह variable उस signal और उस पर लागू होने वाले किसी भी arithmetic operations के लिए एक कंटेनर बन जाता है। एक symbolic variable को अन्य variables की तरह ही var कीवर्ड का उपयोग करके डिक्लेयर किया जाता है।

उदाहरण के लिए, निम्नलिखित दो circuits समान हैं, यानी वे एक ही underlying R1CS उत्पन्न करते हैं:

Copy
template ExampleA() {
	signal input a;
	signal input b;
	signal input c;
	
	a * b === c;
}

template ExampleB() {
	signal input a;
	signal input b;
	signal input c;
	
	// symbolic variable v "contains" a * b
	var v = a * b;
	
	// a * b === c under the hood
	v === c;
}

ExampleB में, symbolic variable v केवल a * b एक्सप्रेशन के लिए एक प्लेसहोल्डर है। ExampleA और ExampleB दोनों को बिल्कुल समान R1CS का उपयोग करके कंपाइल किया जाता है, और उनके बीच शून्य कार्यात्मक (functional) अंतर होता है।

Symbolic variables के उपयोग

यह जाँचना कि $\sum\texttt{in}[i]=\texttt{sum}$

अगर हम किसी लूप में signals के एक array का योग (sum) करना चाहते हैं, तो Symbolic variables बेहद उपयोगी होते हैं। वास्तव में, लूप में signals का योग करना इनका सबसे आम उपयोग है:

Copy
// assert sum of in === sum
template Sum(n) {
	signal input in[n];
	signal input sum;
	
	var accumulator;
	for (var i = 0; i < n; i++) {
		accumulator += in[i];
	}
	
	// in[0] + in[1] + in[2] + ... + in[n - 1] === sum
	accumulator === sum;
}

यह जाँचना कि in, k का एक Valid Binary Representation है

एक अधिक रोचक उदाहरण यह साबित करना है कि n की एक templated वैल्यू के लिए in[n], k का बाइनरी रिप्रजेंटेशन है। नीचे दिए गए circuit में, हम यह जाँचते हैं कि:

यदि in के सभी signals को $\set{0,1}$ तक सीमित (constrained) किया जाता है, तो इसका अर्थ है कि in[], k का बाइनरी रिप्रजेंटेशन है:

Copy
template IsBinaryRepresentation(n) {

	signal input in[n];
	signal input k;
	
	// in is binary only
	for (var i = 0; i < n; i++) {
		in[i] * (in[i] - 1) === 0;
	}
	
	// in is the binary representation of k
	var acc; // symbolic variable
	var powersOf2 = 1; // regular variable
	for (var i = 0; i < n; i++) {
		acc += powersOf2 * in[i];
		powersOf2 *= 2;
	}
	
	acc === k;
}

Symbolic variables मददगार क्यों होते हैं

यह साबित करने वाले पहले के उदाहरण पर विचार करें कि $\sum\texttt{in}[i]=\texttt{sum}$। Symbolic variables के बिना, इसे व्यक्त करना बहुत ही अटपटा (clumsy) है

Copy
sum === in[0] + in[1] + in[2] + ... + in[n-1];

यदि हमें पहले से पता नहीं है कि n क्या है। यहाँ तक कि अगर n तय (fixed) भी होता, मान लीजिए 32, तो वास्तव में हाथ से 32 variables टाइप करना कष्टप्रद होगा। इस प्रकार, symbolic variables हमें स्पष्ट रूप से signals को लिखे बिना क्रमिक रूप से (incrementally) in[0] + in[1] + in[2] + ... का निर्माण करने में सक्षम बनाते हैं।

Symbolic Variables के साथ Non-quadratic Constraints

चूंकि symbolic variables में दो signals के बीच का गुणा (multiplication) “शामिल” हो सकता है, यदि हम सावधान नहीं हैं तो वे एक constraint में दो गुणा को एम्बेड कर सकते हैं। निम्नलिखित उदाहरण पर विचार करें, जो कंपाइल नहीं होगा:

Copy
template QViolation() {
	signal input a;
	signal input b;
	signal input c;
	signal input d;
	
	// v "contains" a * b
	var v = a * b;
	
	// error: there are two
	// multiplications
	// in this constraint
	v === c * d;
}

उपरोक्त कोड में, symbolic variable v में एक गुणा (multiplication) है और हमने v == a*b डिक्लेयर किया है। इसलिए constraint v === c * d;, a * b = c * d; के बराबर है। अतः, उपरोक्त कोड कंपाइल नहीं होगा।

Non-symbolic variables के साथ Arbitrary operators की अनुमति है

Modulo की गणना करने या bitshifting जैसे operations करने की अनुमति (non-symbolic) variables के साथ है। हालाँकि, इसका मतलब है कि variable का उपयोग अब किसी constraint के हिस्से के रूप में नहीं किया जा सकता है:

Copy
// this has no constraints
// but it will compile
template Ok() {
	signal input a;
	signal input b;
	
	var v = a % b;
}

उपरोक्त उदाहरण कंपाइल हो जाएगा क्योंकि v का उपयोग constraint में नहीं किया गया है। हालाँकि, यदि हम constraint में v का उपयोग करते हैं, तो कोड कंपाइल नहीं होगा। इसका एक उदाहरण नीचे दिखाया गया है:

Copy
template NotOk() {
	signal input a;
	signal input b;
	signal input c;
	
	var v = a % b;
	
	// non-quadratic constraint
	c === v;
}

Symbolic variables का उपयोग लूप की boundary या condition निर्धारित करने के लिए नहीं किया जा सकता है

इसी तरह, केवल regular variables का उपयोग लूप की boundary या if स्टेटमेंट की condition निर्धारित करने के लिए किया जा सकता है। यदि किसी symbolic variable का उपयोग किया जाता है, तो कोड कंपाइल नहीं होगा:

Copy
template NotOk() {
	signal input a;
	signal input b;
	signal input c;
	
	var v = a * b;
	
	// v is a symbolic variable
	// used in an if statement
	if (v == 0) {
		c === 0;
	} else {
		c === 1;
	}
}

सारांश

Symbolic variables वे variables होते हैं जिन्हें किसी signal से कोई वैल्यू असाइन की गई होती है। उनका सबसे अधिक उपयोग signals की एक parameterizable संख्या को एक साथ जोड़ने के लिए किया जाता है, क्योंकि योग को for लूप में संचित (accumulate) किया जा सकता है। वे प्रभावी रूप से एक “कंटेनर” या “बाल्टी” होते हैं जिनमें या तो एक सिंगल signal होता है या signals का एक संग्रह (collection) होता है जिन्हें एक साथ जोड़ा या गुणा किया जाता है। यदि किसी variable को कभी भी किसी signal से वैल्यू असाइन नहीं की जाती है, तो वह symbolic variable नहीं होता है।

चूंकि symbolic variables में signals होते हैं, इसलिए उनका उपयोग करते समय quadratic constraint violations से बचने के लिए सावधानी बरती जानी चाहिए।