इस अध्याय में, हम सीखेंगे कि स्मार्ट कॉन्ट्रैक्ट के निष्पादन (execution) में अपेक्षित (expected) reverts को verify करने के लिए CVL में method tags (@withrevert और @norevert) और विशेष वेरिएबल lastReverted का उपयोग कैसे करें।
Add() फंक्शन के लिए वेरिफिकेशन परिदृश्यों (Scenarios) को सेट करना
निम्नलिखित Math कॉन्ट्रैक्ट पर विचार करें, जिसमें एक बुनियादी add() फंक्शन है जो अपने इनपुट के रूप में दो unsigned integers लेता है और उनके योग (sum) को अपने आउटपुट के रूप में लौटाता है।
//SPDX-License-Identifier : MIT
pragma solidity 0.8.25;
contract Math {
function add(uint256 x, uint256 y) public pure returns (uint256) {
return x + y;
}
}
add() फंक्शन निम्नानुसार व्यवहार करता है:
- जब वैध (valid) इनपुट दिए जाते हैं, तो इसे
xऔरyके योग (sum) की सही ढंग से गणना (calculate) करनी चाहिए, और परिणाम कोuint256वैल्यू के रूप में लौटाना चाहिए। उदाहरण के लिए,add(15, 10), 25 लौटाएगा। - चूँकि कॉन्ट्रैक्ट Solidity संस्करण 0.8.0 या उसके बाद के संस्करण का उपयोग करता है, यदि योग (sum) the maximum value of
uint256(2^256 - 1) से अधिक हो जाता है तो ट्रांजेक्शन revert हो जाएगा। उदाहरण के लिए, यदिx = 2^256 - 1औरy = 1है, तो ओवरफ्लो (overflow) के कारण ट्रांजेक्शन कोई परिणाम लौटाने के बजाय revert हो जाएगा।
add() फंक्शन स्पेसिफिकेशन को Verify करना
Math कॉन्ट्रैक्ट से add() फंक्शन की सत्यता (correctness) को verify करने के लिए निम्नलिखित स्पेसिफिकेशन पर विचार करें:
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule checkAdd() {
uint256 a;
uint256 b;
uint256 c = add(a,b);
assert a + b == c;
}
उपरोक्त spec के वेरिफिकेशन परिणाम को देखने के लिए, Prover चलाएं और नीचे दी गई छवि (image) के समान परिणाम देखने के लिए वेरिफिकेशन लिंक खोलें।
यह आश्चर्यजनक लग सकता है क्योंकि जब x और y का योग अधिकतम uint256 वैल्यू से अधिक हो जाता है तो add() फंक्शन के revert होने की उम्मीद होती है। चूँकि Prover सत्यता (correctness) को verify करने के लिए विभिन्न execution paths की जांच करता है, इसलिए किसी को यह उम्मीद होगी कि यह revert परिदृश्य (scenario) का भी सामना करेगा। ऐसे मामलों में, assert स्टेटमेंट का मूल्यांकन (evaluate) false होना चाहिए, और रूल को वेरिफिकेशन में विफल (fail) होना चाहिए।
हालाँकि, ऐसा नहीं हुआ, और हमारे रूल को अभी भी Prover द्वारा verify कर दिया गया। ऐसा इसलिए है क्योंकि, डिफ़ॉल्ट रूप से, Prover वेरिफिकेशन के दौरान revert मामलों को अनदेखा (ignore) कर देता है।
इससे एक महत्वपूर्ण सवाल उठता है: Prover वेरिफिकेशन के दौरान revert मामलों को अनदेखा करना क्यों चुनता है?
Prover Reverts Path को अनदेखा (Ignore) क्यों करता है?
इसका कारण यह है कि reverts ऑपरेशन का एक सामान्य हिस्सा हो सकते हैं—उदाहरण के लिए, यदि कॉन्ट्रैक्ट ओनर के अलावा कोई अन्य व्यक्ति किसी विशेषाधिकार प्राप्त (privileged) क्रिया को करने का प्रयास करता है। ऐसे मामलों में, revert को विफलता (failure) नहीं माना जाता है; यह अपेक्षित (expected) व्यवहार है।
Revert paths को अनदेखा करके, Prover उन सफल निष्पादन परिदृश्यों (successful execution scenarios) को verify करने पर ध्यान केंद्रित करता है जहाँ फंक्शन बिना किसी त्रुटि (errors) के पूरा होता है। हालाँकि, हम CVL द्वारा प्रदान किए गए @withrevert method tag का उपयोग करके इस डिफ़ॉल्ट व्यवहार को बदल (override) सकते हैं।
CVL Method Tags का परिचय
Certora हमें दो method tags प्रदान करता है, @norevert और @withrevert, जिन्हें method के नाम के बाद लेकिन method के arguments से पहले रखा जा सकता है, जैसा कि नीचे दिखाया गया है:
function_name@norevert();
function_name@withrevert();
जब हम किसी method call के साथ @norevert tag का उपयोग करते हैं, तो Prover उन सभी execution paths को सक्रिय रूप से अनदेखा कर देता है जिनके परिणामस्वरूप revert होता है। दूसरे शब्दों में, function_name@norevert(), function_name() के समान ही व्यवहार करता है।
दूसरी ओर, जब हम किसी method call के साथ @withrevert tag का उपयोग करते हैं, तो Prover अब revert मामलों को अनदेखा नहीं करता है। इसके बजाय, यह किसी भी ऐसे परिदृश्य (scenario) को उल्लंघन (violation) के रूप में मानता है जहाँ revert होता है। उदाहरण के लिए, @withrevert tag के साथ नीचे दिए गए checkAdd() रूल पर विचार करें:
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule checkAdd() {
uint256 a;
uint256 b;
uint256 c = add@withrevert(a,b);
assert a + b == c;
}
जब हम इस अपडेट किए गए स्पेसिफिकेशन के साथ Prover को फिर से चलाते हैं, तो परिणाम बदल जाता है: रूल अब वेरिफिकेशन में विफल (fail) हो जाता है, जैसा कि नीचे दी गई छवि (image) में दिखाया गया है:
चूँकि हमने add() फंक्शन कॉल के साथ @withrevert tag का उपयोग किया है, इसलिए Prover अब revert मामलों को अनदेखा नहीं करता है। परिणामस्वरूप, यदि a और b का योग अधिकतम uint256 वैल्यू से अधिक हो जाता है, तो रूल revert को एक उल्लंघन (violation) मानता है। Verifier इस समस्या का पता लगाता है और एक काउंटरएग्जांपल (counterexample) रिपोर्ट करता है—एक ऐसा उदाहरण जो ओवरफ्लो और revert का कारण बनता है, जिससे अंततः assertion विफल (fail) हो जाता है। जब कोई revert होता है, तो कोई रिटर्न वैल्यू नहीं होती है—c अनकन्स्ट्रेंड (unconstrained) होता है और कोई भी मनमाना (arbitrary) मान ले सकता है। इस वजह से, assertion a + b == c सत्य नहीं हो सकता है।
CVL Special Variable: lastReverted का परिचय
CVL में, हमारे पास lastReverted नामक एक विशेष बूलियन (boolean) वेरिएबल तक पहुंच होती है, जो प्रत्येक method call के बाद अपडेट होता है—जिसमें बिना @withrevert के किए गए कॉल भी शामिल हैं। यह वेरिएबल इंगित (indicate) करता है कि सबसे हालिया कॉन्ट्रैक्ट फंक्शन revert हुआ है (lastReverted = true) या सफलतापूर्वक निष्पादित (executed) हुआ है (lastReverted = false)।
हालाँकि, डिफ़ॉल्ट रूप से, Prover उन सभी execution paths को अनदेखा (ignores) कर देता है जिनके परिणामस्वरूप revert हो सकता है। इसका मतलब यह है कि जब किसी फंक्शन को बिना @withrevert के कॉल किया जाता है—जैसे कि डिफ़ॉल्ट कॉल के साथ या @norevert tag का उपयोग करके—तो Prover revert परिदृश्यों का पता नहीं लगाता है, और lastReverted की वैल्यू हमेशा false पर सेट रहेगी।
यह सटीक रूप से ट्रैक करने के लिए कि कोई फंक्शन revert होता है या नहीं, हमें @withrevert tag का उपयोग करके revert paths पर विचार करने के लिए Prover को स्पष्ट रूप से निर्देश (explicitly instruct) देना चाहिए। जब किसी फंक्शन को @withrevert के साथ कॉल किया जाता है, तो Prover अब revert परिदृश्यों को अनदेखा नहीं करता है, और यदि कोई revert होता है, तो lastReverted को true में अपडेट कर दिया जाता है।
उदाहरण: ओवरफ्लो (Overflow) के कारण होने वाले Reverts का पता लगाना
अब, आइए देखें कि व्यावहारिक (practical) वेरिफिकेशन रूल्स में lastReverted का उपयोग कैसे किया जा सकता है। हम एक फंक्शन add() का परीक्षण (test) करेंगे, यह सुनिश्चित करते हुए कि यह उन मामलों में सही ढंग से व्यवहार करता है जहाँ ओवरफ्लो होता है और नहीं होता है।
केस 1: ओवरफ्लो होने पर फंक्शन को Revert होना चाहिए
नीचे दिए गए addShouldRevert() रूल पर विचार करें, जिसका उद्देश्य यह verify करना है कि जब ओवरफ्लो होता है तो add() फंक्शन सही ढंग से revert होता है।
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule addShouldRevert() {
uint256 a;
uint256 b;
require(a + b > max_uint256);
add@withrevert(a,b);
assert lastReverted; // This is the same as assert lastReverted == true;
}
addShouldRevert() रूल में require(a + b > max_uint256); स्टेटमेंट यह सुनिश्चित करता है कि इनपुट a और b को इस तरह से चुना गया है कि उनका योग एक uint256 द्वारा स्टोर किए जा सकने वाले अधिकतम मान से अधिक हो जाता है, जिससे ओवरफ्लो होता है। Solidity के अंकगणितीय (arithmetic) संचालन (operations) ओवरफ्लो के मामलों में स्वचालित रूप से revert हो जाते हैं, जो add(a, b) फंक्शन कॉल के लिए revert को ट्रिगर करता है।
नोट: CVL में, विभिन्न इंटीजर (integer) प्रकारों के अधिकतम मान (maximum values) वेरिएबल्स के रूप में उपलब्ध हैं, जैसे कि max_uint8, max_uint16, …, max_uint256, आदि।
क्योंकि फंक्शन को @withrevert का उपयोग करके इनवोक (invoke) किया गया है, इसलिए Prover इस revert परिदृश्य को अनदेखा नहीं करता है और इसका सही ढंग से पता लगाता है। परिणामस्वरूप, lastReverted को true पर सेट किया जाता है, जो यह दर्शाता है कि फंक्शन निष्पादन (execution) revert हो गया था। Assertion assert lastReverted; तब true का मूल्यांकन (evaluate) करता है, क्योंकि lastReverted अपेक्षित परिणाम (expected outcome) से मेल खाता है। नतीजतन, रूल पास होना चाहिए, जैसा कि नीचे दी गई छवि (image) में दिखाया गया है।
केस 2: वैध (Valid) जोड़ (Addition) पर फंक्शन को Revert नहीं होना चाहिए
इसी तरह, addShouldNotRevert() रूल पर विचार करें, जिसका उद्देश्य यह verify करना है कि जब a और b का योग वैध (valid) uint256 रेंज के भीतर रहता है तो add() फंक्शन revert नहीं होता है।
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule addShouldNotRevert() {
uint256 a;
uint256 b;
require(a + b <= max_uint256);
add@withrevert(a,b);
assert !lastReverted;
}
उपरोक्त रूल में, स्टेटमेंट require(a + b <= max_uint256); यह सुनिश्चित करता है कि इनपुट a और b को इस तरह से चुना गया है कि उनके योग से ओवरफ्लो नहीं होता है। चूँकि Solidity के अंकगणितीय (arithmetic) संचालन (operations) केवल तभी revert होते हैं जब कोई ओवरफ्लो या कोई अन्य स्पष्ट विफलता (explicit failure) होती है, इसलिए add(a, b) फंक्शन बिना revert हुए सफलतापूर्वक निष्पादित (execute) होता है।
चूँकि फंक्शन को @withrevert के साथ कॉल किया गया है, Prover ट्रैक करता है कि क्या कोई revert होता है। हालाँकि, क्योंकि जोड़ (addition) uint256 सीमा से अधिक नहीं है, इसलिए कोई revert नहीं होता है, और lastReverted false रहता है। Assertion assert !lastReverted; इसे verify करता है, यह सुनिश्चित करते हुए कि रूल सफलतापूर्वक पास हो जाता है, जैसा कि नीचे दिखाया गया है।
lastReverted को ओवरराइट (Overwrite) होने से बचाना
चूँकि हर फंक्शन कॉल के बाद lastReverted अपडेट होता है, इसलिए बाद के कॉल्स इसकी वैल्यू को ओवरराइट कर सकते हैं। इसका मतलब यह है कि यदि कोई फंक्शन revert होता है लेकिन उसके तुरंत बाद कोई दूसरा फंक्शन निष्पादित (execute) होता है, तो मूल (original) revert स्थिति (status) खो जाती है।
वेरिफिकेशन त्रुटियों (errors) को रोकने के लिए, इसकी वैल्यू को ओवरराइट करने वाले अतिरिक्त कॉल करने से पहले, हमेशा प्रासंगिक (relevant) फंक्शन कॉल के तुरंत बाद lastReverted को कैप्चर (capture) करें।
इसे समझाने के लिए, आइए एक सरल अंकगणितीय (arithmetic) कॉन्ट्रैक्ट पर विचार करें:
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Math {
function add(uint256 x, uint256 y) public pure returns (uint256) {
return x + y;
}
function divide(uint256 x, uint256 y) public pure returns (uint256) {
return x / y;
}
}
उपरोक्त कॉन्ट्रैक्ट दो बुनियादी फंक्शन को परिभाषित करता है:
add(x, y)बसxऔरyका योग लौटाता है।divide(x, y)इंटीजर (integer) डिवीजन करता है, जो Solidity की अंतर्निहित (built-in) डिवीजन बाय ज़ीरो सुरक्षा के कारणy == 0होने पर reverts हो जाता है।
अब, यह verify करने के लिए डिज़ाइन किए गए निम्नलिखित रूल पर विचार करें कि जब दूसरे argument के रूप में 0 प्राप्त होता है तो दोनों फंक्शन कैसा व्यवहार करते हैं:
methods {
function divide(uint256,uint256) external returns(uint256) envfree;
function add(uint256,uint256) external returns(uint256) envfree;
}
rule checkMath() {
uint256 a;
divide@withrevert(a,0);
bool divideCallStatus = lastReverted;
add@withrevert(a,0);
bool addCallStatus = lastReverted;
assert divideCallStatus == true;
assert addCallStatus == false;
}
यदि हम divide(a, 0) को कॉल करने के तुरंत बाद lastReverted को स्टोर नहीं करते हैं, तो अगला फंक्शन कॉल (add(a, 0)) इसे फिर से अपडेट कर देगा, जिससे डिवीजन ऑपरेशन के विफल होने की जानकारी पूरी तरह से मिट जाएगी (erasing)।
इसका मतलब यह है कि यदि कोई रूल बाद में यह जांचता है कि क्या divide(a, 0) revert हुआ है, तो यह गलत तरीके से निष्कर्ष निकाल सकता है कि फंक्शन सफलतापूर्वक निष्पादित (execute) हुआ—भले ही वह वास्तव में विफल (fail) हो गया हो। इस तरह के गलत वेरिफिकेशन के परिणामस्वरूप कॉन्ट्रैक्ट का गलत विश्लेषण हो सकता है, जिससे महत्वपूर्ण लॉजिक (critical logic) में सुरक्षा भेद्यता (security vulnerabilities) या दोषपूर्ण मान्यताएं (faulty assumptions) पैदा हो सकती हैं।
divide(a, 0) को कॉल करने के तुरंत बाद lastReverted को स्टोर करके, हम यह सुनिश्चित करते हैं कि हम कोई अन्य कॉल करने से पहले फंक्शन के व्यवहार को सटीक रूप से कैप्चर करें। यह सही निष्पादन इतिहास (execution history) को सुरक्षित रखता है, अनपेक्षित (unintended) ओवरराइट्स को रोकता है और विश्वसनीय (reliable) वेरिफिकेशन सुनिश्चित करता है।
निष्कर्ष (Wrapping Up)
किसी method का फॉर्मल वेरिफिकेशन करने के लिए सफलता (success) और revert दोनों मामलों का परीक्षण करना महत्वपूर्ण है, क्योंकि यह बेहतर कवरेज प्रदान करता है और यह सुनिश्चित करता है कि method सभी संभावित इनपुट स्थितियों के तहत सही ढंग से व्यवहार करता है, जिसमें ओवरफ्लो या अमान्य इनपुट जैसे एज केसेस (edge cases) भी शामिल हैं।
यह लेख formal verification using the Certora Prover श्रृंखला (series) का एक हिस्सा है