पिछले अध्याय में, हमने सीखा कि कैसे घोस्ट वेरिएबल्स (ghost variables) जानकारी को हुक्स (hooks) से रूल्स (rules) में प्रवाहित होने देते हैं। हमने यह भी सीखा कि:
- वेरिफिकेशन रन की शुरुआत में, Prover घोस्ट वेरिएबल्स के लिए कोई भी मनमानी (havoced) वैल्यू चुनता है।
- घोस्ट वेरिएबल्स को कॉन्ट्रैक्ट के स्टोरेज के विस्तार के रूप में माना जाता है। यदि सिम्बॉलिक एक्ज़ीक्यूशन (symbolic execution) के दौरान कोई ट्रांजेक्शन रिवर्ट (revert) हो जाता है, तो Prover उस पाथ से किसी भी घोस्ट अपडेट को भी रिवर्ट कर देता है, जिससे वे कॉन्ट्रैक्ट की स्टोरेज स्टेट के साथ कंसिस्टेंट (consistent) रहते हैं।
दूसरा मामला आमतौर पर चिंता का विषय नहीं होता है, क्योंकि ट्रांजेक्शन्स के दौरान घोस्ट वैल्यूज का रिवर्ट होना सामान्य स्टोरेज व्यवहार को दर्शाता है। हालाँकि, पहला मामला गलत या भ्रामक वेरिफिकेशन रिज़ल्ट का कारण बन सकता है।
इस अध्याय में, हम प्रदर्शित करेंगे कि यह समस्या वेरिफिकेशन को कैसे प्रभावित कर सकती है और require स्टेटमेंट का उपयोग करके घोस्ट वेरिएबल्स और कॉन्ट्रैक्ट स्टेट के बीच कंसिस्टेंसी (consistency) स्थापित करके इसे कैसे ठीक किया जाए, यह स्पष्ट करेंगे।
अनकंस्ट्रेन्ड (Unconstrained) घोस्ट्स के खतरे को समझना
यह देखने के लिए कि एक अनकंस्ट्रेन्ड (unconstrained) घोस्ट वेरिएबल वेरिफिकेशन को कैसे प्रभावित कर सकता है, आइए पिछले अध्यायों में उपयोग किए गए Counter कॉन्ट्रैक्ट को फिर से देखें।
//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {
uint256 public count;
function increment() external {
count++;
}
}
नीचे दिए गए स्पेसिफिकेशन (specification) पर विचार करें, जिसका उद्देश्य यह सत्यापित करना है कि increment() फंक्शन की हर कॉल count वेरिएबल को ठीक से बढ़ाती है या नहीं। यह सुनिश्चित करता है कि count में कुल परिवर्तन उस संख्या से मेल खाता है जितनी बार फंक्शन को इनवोक (invoke) किया गया था, जिसे countIncrementCall घोस्ट वेरिएबल द्वारा ट्रैक किया जाता है।
methods {
function increment() external envfree;
function count() external returns (uint) envfree;
}
// Ghost variable to track how many times the `count` variable is updated
ghost mathint countIncrementCall;
// Hook triggered before `count` is updated via SSTORE
hook Sstore count uint256 updatedValue (uint256 prevValue) {
// Increment the ghost each time `count` is about to be modified
countIncrementCall = countIncrementCall + 1;
}
/*
*Rule to verify that count increases by exactly the number of times increment()
is called
*/
rule checkCounterIncrements() {
// Capture the value of `count` before any updates
mathint precallCountValue = count();
// Perform three increment operations
increment();
increment();
increment();
// Capture the value of `count` after updates
mathint postCallCountValue = count();
// Assert that `count` increased by the same amount as tracked by the ghost
assert postCallCountValue == precallCountValue + countIncrementCall;
}
उपरोक्त स्पेक (spec) निम्नलिखित कार्य करता है:
- हम
mathintप्रकार का एक घोस्ट वेरिएबल,countIncrementCallडिक्लेयर करते हैं, जो हमारे स्वतंत्र काउंटर के रूप में कार्य करता है। - हम एक
Sstoreहुक का उपयोग करते हैं जोcountवेरिएबल पर नज़र रखता है। हर बार जब कॉन्ट्रैक्टcountमें एक नई वैल्यू लिखता है, तो यह हुक ट्रिगर होता है और यहcountIncrementCallघोस्ट को इंक्रीमेंट (increment) करता है। checkCounterIncrementsरूल एक टेस्ट सिनेरियो स्थापित करता है। यहcountकी प्रारंभिक वैल्यू पढ़ता है,increment()को तीन बार कॉल करता है, और फिर अंतिम वैल्यू पढ़ता है।- अंत में, यह दावा (assert) करता है कि अंतिम काउंट प्रारंभिक काउंट और हमारे घोस्ट द्वारा ट्रैक किए गए इंक्रीमेंट्स की संख्या के योग के बराबर होना चाहिए। चूंकि हमने
increment()को तीन बार कॉल किया है, इसलिएcountIncrementCall3 होना चाहिए, इसलिए assertion के सही होने की उम्मीद है।
पहली नज़र में, यह स्पेसिफिकेशन तार्किक रूप से सही लगता है। हालाँकि, जब इसे Certora Prover के माध्यम से रन किया जाता है, तो यह checkCounterIncrements रूल को वेरीफाई करने में विफल रहता है, जैसा कि नीचे दिखाए गए आउटपुट में दर्शाया गया है:
यह समझने के लिए कि assertion विफल क्यों होता है, आइए Prover द्वारा प्रदान किए गए कॉल ट्रेस (call trace) को गहराई से समझें।
वेरिफिकेशन विफल क्यों हुआ
कॉल ट्रेस के हमारे विश्लेषण से पता चलता है कि रूल लॉजिक में किसी खामी के कारण विफल नहीं हुआ, बल्कि इसलिए विफल हुआ क्योंकि घोस्ट वेरिएबल countIncrementCall एक ऐसी वैल्यू से शुरू हुआ जिसे Prover द्वारा एडवर्सरियली (adversarially) चुना गया था, इस मामले में -0x2 (या -2)। महत्वपूर्ण बात यह है कि यह वैल्यू गलती से नहीं चुनी गई थी। इसके बजाय, इसे एक व्यवस्थित प्रक्रिया के माध्यम से जानबूझकर असाइन किया गया था जिसे havocing कहा जाता है।
Havocing वह तंत्र है जिसके द्वारा Prover स्टेट या घोस्ट वेरिएबल्स को मनमानी (unconstrained) प्रारंभिक वैल्यू असाइन करता है। यहां “मनमानी” का अर्थ है कि वेरिएबल अपने प्रकार (type) की रेंज के भीतर कोई भी वैल्यू लेने के लिए स्वतंत्र है। ऐसा करने से, Prover व्यवस्थित रूप से एज केसेस (edge cases) और चरम परिदृश्यों (extreme scenarios) की जांच कर सकता है जो वेरिफिकेशन के विफल होने का कारण बन सकते हैं। यह तकनीक वेरिफिकेशन प्रक्रिया को विस्तृत (exhaustive) बनाती है, जिससे Prover उन सभी संभावित स्टेट्स के बारे में तर्क कर पाता है जहाँ तक कॉन्ट्रैक्ट पहुँच सकता है।
इस विशेष मामले में, स्टोरेज वेरिएबल count 0xA (दशमलव में 10) से शुरू हुआ, जबकि countIncrementCall -2 से शुरू हुआ। increment() को तीन बार कॉल करने के बाद, count 0xD (दशमलव में 13) तक पहुंच गया, और घोस्ट वेरिएबल -2 से बढ़कर 1 हो गया। हालाँकि, assertion की यह उम्मीद थी:
postCallCountValue == precallCountValue + countIncrementCall;
जो, वास्तविक वैल्यूज को प्रतिस्थापित करने पर, यह बन गया:
13 == 10 + 1
यह स्पष्ट रूप से गलत है, इसलिए वेरिफिकेशन विफल हो गया।
याद रखने योग्य “सबक” (Lesson)
यह विफलता Prover के काम करने के तरीके के बारे में एक महत्वपूर्ण कांसेप्ट (concept) को उजागर करती है। वेरिफिकेशन के दौरान, Prover कॉन्ट्रैक्ट स्टोरेज या घोस्ट वेरिएबल्स के लिए किसी भी डिफ़ॉल्ट या कंस्ट्रक्टर-डिफाइंड प्रारंभिक वैल्यू को नहीं मानता है। इसके बजाय, यह उन्हें havoc करता है — उनकी अनुमत रेंज के भीतर मनमानी सिम्बॉलिक (symbolic) वैल्यू असाइन करता है। यह व्यवहार Prover को कॉन्ट्रैक्ट की सभी संभावित प्रारंभिक स्टेट्स के बारे में तर्क करने की अनुमति देता है, यह सुनिश्चित करते हुए कि प्रॉपर्टीज (properties) सार्वभौमिक रूप से लागू होती हैं, न कि केवल विशिष्ट प्रारंभिक कॉन्फ़िगरेशन के लिए।
हालांकि यह दृष्टिकोण वेरिफिकेशन को विस्तृत बनाता है, लेकिन यह अवास्तविक प्रारंभिक स्थितियां (unrealistic initial conditions) भी पेश कर सकता है। यदि कोई रूल कॉन्ट्रैक्ट के स्टोरेज और घोस्ट वेरिएबल के बीच सार्थक संबंध (meaningful relationship) पर निर्भर करता है, तो havocing उन्हें असंबंधित वैल्यूज से शुरू करके उस संबंध को तोड़ सकता है। उदाहरण के लिए, एक घोस्ट जो increment() कॉल्स की संख्या का प्रतिनिधित्व करता है, वह -2 या 5 से शुरू हो सकता है, भले ही increment() फंक्शन को अभी तक कोई कॉल नहीं की गई हो।
जब ऐसा होता है, तो रूल विफल हो सकता है — इसलिए नहीं कि इसका लॉजिक त्रुटिपूर्ण है, बल्कि इसलिए क्योंकि वेरिफिकेशन एक ऐसी स्टेट से शुरू हुआ जो व्यवहार में कभी अस्तित्व में नहीं हो सकती। ऐसी विफलताएं फ़ॉल्स पॉज़िटिव (false positives) होती हैं: वे कॉन्ट्रैक्ट में किसी वास्तविक समस्या के बजाय सिम्बॉलिक इनिशियलाइज़ेशन और सिमेंटिक इंटेंट (semantic intent) के बीच बेमेल को उजागर करती हैं।
“समाधान” (Solution) क्या है
इन गलत विफलताओं से बचने की कुंजी यह सुनिश्चित करना है कि वेरिफिकेशन शुरू होने से पहले एक घोस्ट वेरिएबल और कॉन्ट्रैक्ट के स्टोरेज के बीच का प्रारंभिक संबंध तार्किक रूप से सही हो। इसका मतलब उनकी सटीक वैल्यूज को फिक्स करना नहीं है, बल्कि उन्हें इस तरह कंस्ट्रेन (constrain) करना है ताकि वे एक ऐसी स्टेट में शुरू हों जिसका कोई अर्थ हो।
उदाहरण के लिए, हमारे रूल में, घोस्ट वेरिएबल countIncrementCall का उद्देश्य यह दर्शाना है कि increment() को कितनी बार इनवोक किया गया है। रूल की शुरुआत में, किसी भी कॉल के होने से पहले, यह संख्या शून्य (zero) होनी चाहिए। कॉन्ट्रैक्ट का count वेरिएबल किसी भी वैल्यू — 0, 10, या 100 — से शुरू हो सकता है, लेकिन घोस्ट हमेशा 0 से शुरू होना चाहिए, क्योंकि अभी तक कोई इंक्रीमेंट नहीं हुआ है।
ऐसी तार्किक कंसिस्टेंसी को लागू करने के लिए, हम CVL में require स्टेटमेंट का उपयोग करते हैं। CVL में, require स्टेटमेंट एक लॉजिकल प्रीकंडीशन (logical precondition) के रूप में कार्य करता है, जो Prover को केवल उन प्रारंभिक स्टेट्स से सभी संभावित व्यवहारों का पता लगाने के लिए कहता है जो उस निर्दिष्ट संबंध को पूरा करते हैं। एक साधारण कंस्ट्रेंट (constraint) जोड़कर जैसे कि:
require countIncrementCall == 0;
हम प्रभावी रूप से उन अर्थहीन कॉन्फ़िगरेशन को फ़िल्टर कर देते हैं जहां घोस्ट की प्रारंभिक वैल्यू इसके इच्छित अर्थ का खंडन करती है।
इस कंस्ट्रेंट के लागू होने के साथ, Prover अभी भी एडवर्सरियल एक्सप्लोरेशन करता है, लेकिन यह सिमेंटिक रूप से मान्य (semantically valid) स्टेट्स से शुरू करके ऐसा करता है। यह सुनिश्चित करता है कि कंस्ट्रेंट लागू करने के बाद होने वाली कोई भी वेरिफिकेशन विफलता रूल या कॉन्ट्रैक्ट लॉजिक में एक वास्तविक समस्या से मेल खाती है — न कि मनमाने इनिशियलाइज़ेशन (initialization) के साइड इफ़ेक्ट से।
require स्टेटमेंट के साथ घोस्ट्स को कंस्ट्रेन (Constrain) करना
जैसा कि पहले चर्चा की गई है, हमारे मामले में, घोस्ट वेरिएबल countIncrementCall का उद्देश्य यह दर्शाना है कि increment() फंक्शन को कितनी बार कॉल किया गया है। रूल के एक्ज़ीक्यूशन की शुरुआत में, ऐसी कोई कॉल अभी तक नहीं हुई है — जिसका अर्थ है कि इस घोस्ट के लिए सही प्रारंभिक वैल्यू शून्य होनी चाहिए।
हम रूल की शुरुआत में केवल require countIncrementCall == 0; जोड़कर इस कंस्ट्रेंट को सीधे अपने रूल में एनकोड (encode) कर सकते हैं।
// Rule to verify that `increment()` increases `count` by exactly the number of times it's called
rule checkCounterIncrements() {
//Add the require statement to constrain the ghost
require countIncrementCall == 0;
// Capture the value of `count` before any updates
mathint precallCountValue = count();
// Perform three increment operations
increment();
increment();
increment();
// Capture the value of `count` after updates
mathint postCallCountValue = count();
// Assert that `count` increased by the same amount as tracked by the ghost
assert postCallCountValue == precallCountValue + countIncrementCall;
}
इस प्रीकंडीशन (precondition) को शामिल करके, हम यह सुनिश्चित करते हैं कि Prover रूल एक्ज़ीक्यूशन को तार्किक रूप से सार्थक स्टेट में शुरू करता है, जहाँ कॉन्ट्रैक्ट का स्टोरेज और घोस्ट के सिमेंटिक्स संरेखित (aligned) होते हैं। Prover अभी भी पूर्ण सिम्बॉलिक और एडवर्सरियल एक्सप्लोरेशन करता है, लेकिन अब यह असंभव स्टेट्स का पता लगाने से बचता है जैसे कि घोस्ट वेरिएबल countIncrementCall का -2 या 5 से शुरू होना।
जब वेरिफिकेशन को फिर से रन किया जाता है, तो count और countIncrementCall दोनों तार्किक रूप से कंसिस्टेंट स्टेट्स में शुरू होते हैं। उनकी वैल्यूज भिन्न हो सकती हैं — उदाहरण के लिए, count 10 पर और countIncrementCall 0 पर शुरू हो सकता है — फिर भी उनका संबंध ठोस रहता है।
यहाँ से, increment() की प्रत्येक कॉल कॉन्ट्रैक्ट के स्टोरेज और घोस्ट दोनों को एकदम सिंक (sync) में अपडेट करती है। तीन कॉल्स के बाद, count तीन से बढ़ जाता है, और countIncrementCall भी तीन अपडेट्स रिकॉर्ड करता है। परिणामस्वरूप, यह assertion
assert postCallCountValue == precallCountValue + countIncrementCall;
सभी मान्य एक्ज़ीक्यूशन पाथ्स (valid execution paths) में सही रहता है, यह पुष्टि करते हुए कि रूल अब सफलतापूर्वक वेरीफाई हो गया है।
यह प्रदर्शित करता है कि कैसे एक सिंगल लाइन require countIncrementCall == 0 Prover के विश्लेषण को तार्किक रूप से मजबूत शुरुआती बिंदु पर एंकर (anchor) करके फॉल्स वेरिफिकेशन विफलताओं को समाप्त कर सकती है। यह वेरिफिकेशन के दायरे को सीमित नहीं करता है; इसके बजाय, यह सुनिश्चित करता है कि एक्सप्लोरेशन स्पेस सिमेंटिक रूप से मान्य है और कोई भी रूल विफलता मनमाने इनिशियलाइज़ेशन आर्टिफैक्ट (initialization artifact) के बजाय एक वास्तविक तार्किक समस्या को दर्शाती है।
हालाँकि, इस स्पेसिफिकेशन में एक महत्वपूर्ण धारणा (assumption) है जिस पर करीब से विचार करने की आवश्यकता है।
यहाँ, घोस्ट countIncrementCall को count स्टोरेज स्लॉट पर लिखे जाने पर इंक्रीमेंट किया जाता है, जो काम करता है क्योंकि count को वर्तमान में केवल increment() के अंदर ही मॉडिफाई किया गया है। लेकिन क्या होगा अगर कोई अन्य फंक्शन—मान लीजिए, reset() या setCount()—भी count को मॉडिफाई करता है? घोस्ट तब भी इंक्रीमेंट होगा, भले ही increment() को कॉल नहीं किया गया था।
यह एक महत्वपूर्ण डिज़ाइन विचार (design consideration) को उजागर करता है: क्या हुक करना है, यह चुनाव निर्धारित करता है कि घोस्ट वास्तव में क्या ट्रैक करता है। इस मामले में, हम फंक्शन कॉल्स को नहीं, बल्कि स्टोरज़ राइट्स (storage writes) को ट्रैक कर रहे हैं। सरल कॉन्ट्रैक्ट्स के लिए, ये समतुल्य हो सकते हैं—लेकिन जैसे-जैसे कॉन्ट्रैक्ट्स अधिक जटिल होते जाते हैं, वह समतुल्यता (equivalence) टूट सकती है। हम बाद के एक अध्याय में वैकल्पिक हुकिंग रणनीतियों का पता लगाएंगे जो इस सीमा को संबोधित करती हैं।
निष्कर्ष (Conclusion)
अनकंस्ट्रेन्ड घोस्ट वेरिएबल्स Prover को अवास्तविक स्टेट्स का पता लगाने के लिए प्रेरित कर सकते हैं, जिसके परिणामस्वरूप भ्रामक वेरिफिकेशन विफलताएं हो सकती हैं। require स्टेटमेंट का उपयोग करके उनकी प्रारंभिक वैल्यूज को कंस्ट्रेन करके, हम यह सुनिश्चित कर सकते हैं कि घोस्ट्स एक ऐसी स्टेट से शुरू हों जो कॉन्ट्रैक्ट के स्टोरेज के साथ तार्किक रूप से संरेखित (aligned) हो। यह छोटा लेकिन महत्वपूर्ण कदम वेरिफिकेशन को विस्तृत (exhaustive) और सिमेंटिक रूप से मान्य दोनों बनाए रखता है, जिससे Prover को केवल वास्तविक तार्किक समस्याओं की रिपोर्ट करने की अनुमति मिलती है।
यह लेख Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन (formal verification using the Certora Prover) पर एक श्रृंखला का हिस्सा है।