पिछले अध्याय में, हमने formal verification के सैद्धांतिक पक्ष (theoretical side) के बारे में सीखा था, जिसमें यह क्या है और कैसे काम करता है शामिल है। इस मॉड्यूल में, हम थ्योरी से आगे बढ़ेंगे और निम्नलिखित चीजें सीखेंगे:
- Certora Prover के साथ काम करने के लिए प्रोजेक्ट कैसे सेट अप करें।
- Certora access key कैसे प्राप्त करें और उसका उपयोग कैसे करें।
- Certora Prover का उपयोग करके formal verification कैसे करें।
आइए Certora Prover के लिए प्रोजेक्ट एनवायरनमेंट सेट अप करने से शुरू करते हैं।
आवश्यक Prerequisites Tools को इंस्टॉल करना
प्रोजेक्ट डायरेक्टरी सेट अप करने से पहले, यह सुनिश्चित करें कि आपकी लोकल मशीन में निम्नलिखित prerequisites इंस्टॉल हैं:
आप अपने टर्मिनल में python3 --version और java --version कमांड रन करके यह जांच सकते हैं कि आपकी मशीन में ये दोनों इंस्टॉल हैं या नहीं।
💡 Windows यूज़र्स के लिए, हम बेहतर अनुभव के लिए Windows Subsystem for Linux (WSL) का उपयोग करने की अत्यधिक अनुशंसा (recommend) करते हैं।
अपनी Project Directory सेट अप करना
Prerequisites इंस्टॉल हो जाने के बाद, certora-counter नाम की एक खाली डायरेक्टरी बनाएं, उसमें नेविगेट करें, और अपनी प्रोजेक्ट डायरेक्टरी को सही तरीके से सेट अप करने के लिए नीचे दिए गए निर्देशों का पालन करें।
- अपनी लोकल मशीन में, नीचे दिए गए कमांड को रन करके virtualenv इंस्टॉल करें। यह टूल हमें एक Python virtual environment बनाने की अनुमति देगा, जो आपकी प्रोजेक्ट डायरेक्टरी के भीतर डिपेंडेंसीज़ (dependencies) को मैनेज करने के लिए आवश्यक है।
pip3 install virtualenv
- एक बार जब हमारे पास virtualenv इंस्टॉल हो जाए, तो अपने टर्मिनल में नीचे दिए गए कमांड को रन करके अपने प्रोजेक्ट के लिए एक Python virtual environment बनाएं।
virtualenv certora-env
- इसके बाद, अपने टर्मिनल में नीचे दिए गए कमांड को रन करके अपने द्वारा बनाए गए Python virtual environment को एक्टिवेट करें।
source certora-env/bin/activate
- इसके बाद, Prover इंस्टॉल करने के लिए अपने टर्मिनल में नीचे दिया गया कमांड रन करें।
pip3 install certora-cli
- इसके बाद, नीचे दिए गए कमांड का उपयोग करके अपने virtual environment में solc-select इंस्टॉल करें। यह हमें हमारे द्वारा उपयोग किए जा रहे Solidity compiler के वर्ज़न को आसानी से बदलने की अनुमति देगा।
pip3 install solc-select
Certora Personal Access Key ऐड करना
Prover को रन करने के लिए, आपको एक system variable के रूप में एक access key सेट अप करने की आवश्यकता है। अपना पर्सनल एक्सेस प्राप्त करने के लिए, Certora website पर रजिस्टर करें। रजिस्टर करने के बाद, आपको Certora से एक ईमेल प्राप्त होगा जिसमें access key और आपके Certora अकाउंट के लिए एक शुरुआती (initial) पासवर्ड होगा।
Access key को system variable के रूप में ऐड करने के लिए, निम्नलिखित निर्देशों का पालन करें:
Linux यूज़र्स के लिए
- एक टर्मिनल खोलें और सुनिश्चित करें कि आप प्रोजेक्ट डायरेक्टरी में हैं।
nano .profileकमांड का उपयोग करके .profile फ़ाइल बनाएं और खोलें।- Access key को environment variable के रूप में ऐड करने के लिए, इसमें निम्नलिखित टेक्स्ट जोड़ें।
#certora access key
export CERTORAKEY=<your-certora-access-key>
- बदलावों को सेव करने के लिए,
CTRL + Oदबाएं और फिरEnterदबाएं। - बाहर निकलने के लिए,
CTRL + Xदबाएं। - .profile फ़ाइल में हमारे द्वारा किए गए हाल के बदलावों को लोड करने के लिए, अपने टर्मिनल में नीचे दिया गया कमांड रन करें।
source .profile
zsh का उपयोग करने वाले Mac यूज़र्स के लिए
- एक टर्मिनल खोलें और सुनिश्चित करें कि आप
certora-counterडायरेक्टरी में हैं। - अपने टर्मिनल में
nano .zshenvकमांड रन करके .zshenv नाम की एक फ़ाइल बनाएं। .zshenvफ़ाइल को अपने पसंदीदा टेक्स्ट एडिटर में खोलें।- Access key को environment variable के रूप में ऐड करने के लिए, इसमें निम्नलिखित टेक्स्ट जोड़ें।
#certora access key
export CERTORAKEY=<your-certora-access-key>
- बदलावों को सेव करने के लिए,
CTRL + Oदबाएं और फिरEnterदबाएं। - बाहर निकलने के लिए,
CTRL + Xदबाएं। - अभी बनाए गए environment variable को अप्लाई करने के लिए, अपने टर्मिनल में नीचे दिया गया कमांड रन करें।
source .zshenv
कृपया ध्यान दें कि जब भी आप नया टर्मिनल खोलें, तो environment variables को लोड करने के लिए source .zshenv या source .profile कमांड रन करना सुनिश्चित करें; अन्यथा, आपको Prover से The environment variable CERTORAKEY does not contain a Certora key एरर मैसेज मिलेगा।
Project Directory में Contract ऐड करना
certora-counter डायरेक्टरी में, contracts नामक एक सबफ़ोल्डर ऐड करें। इसके हो जाने के बाद, इसमें Counter.sol नामक एक फ़ाइल बनाएं, और नीचे दिया गया कॉन्ट्रैक्ट ऐड करें।
//SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Counter {
uint256 public count;
function increment() external {
count++;
}
}
उपरोक्त कॉन्ट्रैक्ट एक साधारण स्मार्ट कॉन्ट्रैक्ट है जिसमें count नामक केवल एक पब्लिक स्टेट वेरिएबल है, जिसकी वैल्यू को एक्सटर्नल फ़ंक्शन increment() द्वारा बढ़ाया (increment) जा सकता है।
Certora Verification Language LSP सेट अप करना
यदि आप Microsoft’s VS Code एडिटर या इसके किसी फ़ोर्क (fork) का उपयोग करते हैं, तो हम नीचे दिए गए निर्देशों का पालन करते हुए सिंटैक्स चेकिंग (syntax checking), सिंटैक्स हाइलाइटिंग (syntax highlighting), और कोड कंप्लीशन (code completion) के साथ अपने डेवलपमेंट अनुभव को बेहतर बनाने के लिए Certora Verification Language LSP इंस्टॉल करने की सलाह देते हैं:
- अपनी मशीन पर VS Code खोलें।
- साइडबार में Extensions आइकन पर क्लिक करके Extensions Marketplace खोलें।
- Extensions सर्च बार में “Certora Verification Language LSP” सर्च करें।
- Certora द्वारा पब्लिश किए गए एक्सटेंशन पर “Install” पर क्लिक करें।
- एक्सटेंशन को पूरी तरह से एक्टिवेट करने और सभी बदलावों को अप्लाई करने के लिए VS Code को रीस्टार्ट करें।
अपना पहला Specification लिखना
certora-counter डायरेक्टरी में, specs नाम का एक सबफ़ोल्डर ऐड करें। इसके हो जाने के बाद, इसमें counter.spec नाम की एक फ़ाइल बनाएं और नीचे दिया गया कोड ऐड करें।
methods {
function count() external returns(uint256) envfree;
function increment() external envfree;
}
rule checkCounter() {
// Pre-Call State
uint256 precallCount = count();
// Method Call
increment();
// Post-call state
uint256 postcallCount = count();
// Assert that the post-call count is exactly one more than the pre-call count
assert postcallCount == precallCount + 1;
}
अभी के लिए, कोड के बारे में चिंता न करें। हम अगले अध्याय में इसे ब्रेक डाउन करेंगे और प्रत्येक भाग को विस्तार से समझाएंगे।
Solidity Compiler ऐड करना
Prover को रन करने से पहले, हमें सही Solidity compiler ऐड करने की आवश्यकता है। अपने प्रोजेक्ट के लिए सही Solidity compiler वर्ज़न को ऐड और उपयोग करने के लिए, अपने टर्मिनल में नीचे दिए गए दो कमांड रन करें।
solc-select install 0.8.25
solc-select use 0.8.25
Verification रन करना
एक बार जब हमारे पास एक कॉन्ट्रैक्ट और एक स्पेसिफिकेशन (specification) हो जाता है, तो हम certoraRun कमांड रन करके उन्हें verification प्रोसेस के लिए Certora prover को सबमिट कर सकते हैं। सफलतापूर्वक एक्ज़ीक्यूट होने के लिए इस कमांड को Solidity कॉन्ट्रैक्ट और उससे जुड़ी .spec फ़ाइल के पाथ (path) की आवश्यकता होती है, जैसा कि नीचे दिखाया गया है।
certoraRun contractFilePath:contractName --verify contractName:specFilePath
अपने स्पेसिफिकेशन को वेरीफाई (verify) करने के लिए, सुनिश्चित करें कि आप certora-counter डायरेक्टरी में हैं, और फिर अपने टर्मिनल में नीचे दिया गया कमांड रन करें।
certoraRun contracts/Counter.sol:Counter --verify Counter:specs/counter.spec
उपरोक्त कमांड रन करने के बाद, आपको नीचे दिए गए आउटपुट जैसा कुछ दिखना चाहिए।
Verification रिज़ल्ट देखने के लिए, अपने टर्मिनल में प्रिंट किए गए verification लिंक को खोलें। रिज़ल्ट नीचे दी गई इमेज के समान दिखना चाहिए।
हालाँकि, एक बड़े प्रोजेक्ट के लिए, सीधे टर्मिनल में कई आर्गुमेंट्स के साथ certoraRun कमांड का उपयोग करना बोझिल (cumbersome) हो सकता है। इसलिए, कॉन्फ़िगरेशन फ़ाइल (configuration file) का उपयोग करने की सलाह दी जाती है।
certoraRun Command को Streamline करने के लिए Config File का उपयोग करना
Certora में, कॉन्फ़िग फ़ाइल (config file) .conf एक्सटेंशन के साथ लिखी गई एक साधारण JSON5 फ़ाइल होती है, जिसमें अन्य कॉन्फ़िगरेशन विकल्पों के साथ कम से कम दो प्रमुख पैरामीटर्स की आवश्यकता होती है:
- files: कॉन्ट्रैक्ट नाम के साथ, हमारे कॉन्ट्रैक्ट का पाथ।
- verify: स्पेसिफिकेशन फ़ाइल का पाथ।
कॉन्फ़िग फ़ाइल का उपयोग करने के लिए, अपनी प्रोजेक्ट डायरेक्टरी में confs नाम का एक सबफ़ोल्डर बनाएं। फिर, confs फ़ोल्डर के अंदर counter.conf नाम की एक फ़ाइल बनाएं और नीचे दिया गया कंटेंट ऐड करें।
{
"files": [
"contracts/Counter.sol:Counter"
],
"verify": "Counter:specs/counter.spec",
}
एक बार जब हमने कॉन्फ़िगरेशन फ़ाइल को सही ढंग से रख दिया है, तो हम बस certoraRun कमांड रन करके और कॉन्फ़िगरेशन फ़ाइल का पाथ रेफ़र करके verification प्रोसेस को पूरा कर सकते हैं, जैसा कि नीचे दिखाया गया है:
certoraRun confs/counter.conf
यदि कमांड सफलतापूर्वक एक्ज़ीक्यूट होता है, तो आपको निम्नलिखित जैसा आउटपुट दिखना चाहिए, जिसमें verification रिज़ल्ट का लिंक शामिल होता है।
Verification का रिज़ल्ट देखने के लिए अपने टर्मिनल में प्रिंट किए गए verification लिंक को खोलें। रिज़ल्ट नीचे दी गई इमेज के समान दिखना चाहिए।
अभी के लिए, बस यह समझें कि हरा चेक (✅) यह दर्शाता है कि Prover ने spec फ़ाइल (counter.spec) में निर्दिष्ट (specified) शर्तों को सफलतापूर्वक वेरीफाई कर लिया है। इसका मतलब है कि कॉन्ट्रैक्ट ने spec में बताए गए एशर्सन्स (assertions) और लॉजिक के आधार पर उम्मीद के मुताबिक व्यवहार किया है।
निष्कर्ष
बधाई हो! आपने सफलतापूर्वक अपना डेवलपमेंट एनवायरनमेंट सेट अप कर लिया है और अपना पहला formal verification रन एक्ज़ीक्यूट कर लिया है। हालाँकि, अब तक, हमने स्पेसिफिकेशन फ़ाइल (.spec) को एक ‘ब्लैक बॉक्स (black box)’ के रूप में माना है। हमने इसे रन तो किया, लेकिन इसके अंदर नहीं देखा। अगले अध्याय में, हम उस बॉक्स को खोलेंगे और एक Certora स्पेसिफिकेशन की संरचना (anatomy) का विश्लेषण (dissect) करेंगे। हम इसके दो आवश्यक घटकों (components), Rule Blocks और Methods Blocks, को ब्रेक डाउन करेंगे और सीखेंगे कि अपने पहले स्मार्ट कॉन्ट्रैक्ट को वेरीफाई करने के लिए आवश्यक pre-conditions, actions, और post-conditions कैसे परिभाषित करें।
यह लेख Certora Prover का उपयोग करके formal verification पर एक सीरीज़ का हिस्सा है।