अभी तक, हमने व्यक्तिगत methods या methods के अनुक्रमों के व्यवहार को सत्यापित करने पर ध्यान केंद्रित किया है — यह सुनिश्चित करना कि एक विशिष्ट function कॉल या कॉल्स का सेट, कुछ inputs दिए जाने पर, state में सही परिवर्तन उत्पन्न करता है। लेकिन सत्यापन (verification) का एक और, अधिक सार्वभौमिक पहलू है: invariants।

Invariants वे शर्तें हैं जो contract की state के लिए हमेशा सत्य होनी चाहिए, चाहे कोई भी function कॉल किया गया हो या किसी भी क्रम में। यदि कोई भी execution — चाहे प्रत्यक्ष हो या कॉल्स के अनुक्रम के माध्यम से — किसी invariant का उल्लंघन करता है, तो यह contract के डिज़ाइन में एक मूलभूत दोष का संकेत देता है, जो संभावित रूप से किसी बग या भेद्यता (vulnerability) को उजागर करता है।

इस लेख में, हम यह पता लगाएंगे कि Certora के CVL built-in invariant construct का उपयोग करके ऐसे गुणों (properties) को औपचारिक रूप से कैसे निर्दिष्ट और सत्यापित किया जाए।

CVL में Invariants को परिभाषित करना

CVL का built-in invariant construct एक औपचारिक विनिर्देश (formal specification) तंत्र है जो डेवलपर्स को सार्वभौमिक गुणों (invariants) को परिभाषित करने की अनुमति देता है जो एक smart contract के पूरे जीवनकाल में सत्य रहने चाहिए, अर्थात, constructor के निष्पादित होने के समय से लेकर भविष्य में contract जिस भी state तक पहुंच सकता है।

CVL में Invariants को invariant कीवर्ड का उपयोग करके परिभाषित किया जाता है, जिसके बाद एक अद्वितीय नाम (identifier), वैकल्पिक पैरामीटर, और एक boolean expression होता है जो उस स्थिति का वर्णन करता है जो हमेशा सत्य होनी चाहिए, जैसा कि नीचे दिखाया गया है:

Copy
invariant invariant_name(optional_parameter_1, optional_parameter_2, ...)
    boolean_expression_in_CVL;

एक invariant को सत्य माना जाता है और उसे सत्यापित (✅) के रूप में रिपोर्ट किया जाता है यदि invariant में परिभाषित इसका boolean expression, contract की प्रत्येक पहुँच योग्य state में और इसके मापदंडों (parameters) के सभी संभावित मानों के लिए true का मूल्यांकन करता है। हम इस अध्याय में बाद में invariant सत्यापन प्रक्रिया के बारे में अधिक विस्तार से जानेंगे।

Invariants, Rules से कैसे भिन्न हैं

CVL में एक rule यह जांचने के लिए डिज़ाइन किया गया है कि क्या कोई विशिष्ट गुण (property) एक परिभाषित परिदृश्य के भीतर सत्य है: एक निश्चित state से शुरू करना, कुछ कार्य (actions) करना, और फिर परिणाम की जांच करना।

Copy
rule check_balance_updates(env e) {

    // 1. Starting State
    address user = e.msg.sender;
    uint initial_balance = balanceOf(user);

    // 2. Actions
    uint amount;
    deposit(amount); // Call the deposit function

    // 3. Outcome Check
    uint final_balance = balanceOf(user);
    assert final_balance == initial_balance + amount, "Deposit did not correctly update balance";
}

दूसरे शब्दों में, यह इस प्रश्न का उत्तर देता है: “क्या यह विशेष कार्य (या कार्यों का अनुक्रम) अपेक्षित परिणाम की ओर ले जाता है?”

Rules के विपरीत, जो विशिष्ट परिदृश्यों पर ध्यान केंद्रित करते हैं, CVL में एक invariant एक ऐसी शर्त व्यक्त करता है जो contract की प्रत्येक पहुँच योग्य state (reachable state) में हमेशा सत्य होनी चाहिए, चाहे कौन से functions कॉल किए गए हों या किस क्रम में।

नीचे एक सरल invariant का उदाहरण दिया गया है जो बताता है कि count का मान कभी भी नकारात्मक (negative) नहीं होना चाहिए:

Copy
invariant count_cannot_be_negative()
    count() >= 0;

सरल शब्दों में, यह इस प्रश्न का उत्तर देता है: “क्या यह स्थिति सार्वभौमिक रूप से सत्य है, चाहे contract का उपयोग कैसे भी किया जाए?"

Invariants बनाम Rules का उपयोग कब करें

CVL में rule या invariant का उपयोग करने का निर्णय उस गुण (property) की प्रकृति पर निर्भर करता है जिसे हम सत्यापित करना चाहते हैं।

Rule का उपयोग कब करें: विशिष्ट परिदृश्यों का सत्यापन

जब आपका लक्ष्य किसी परिभाषित संदर्भ या संचालन (operations) के विशिष्ट अनुक्रम के भीतर व्यवहार को सत्यापित करना हो, तो rule चुनें। उदाहरण के लिए:

1. withdraw(amount) function को कॉलर के बैलेंस से amount को सही ढंग से काटना और ट्रांसफर करना चाहिए, लेकिन केवल तभी जब balanceOf(caller) >= amount हो।
2. यह सत्यापित करना कि अधिकतम सप्लाई कैप (supply cap) से अधिक mint करने का प्रयास सही ढंग से revert हो जाता है।
3. यह जाँचना कि कोई एडमिन function केवल निर्धारित एडमिन एड्रेस द्वारा ही सफलतापूर्वक कॉल किया जा सकता है।

संक्षेप में, rules इस बात का उत्तर देने का आपका मुख्य तरीका हैं: “क्या यह function (या functions का अनुक्रम) इस विशेष स्थिति में सही ढंग से काम करता है?”

Invariant का उपयोग कब करें: मूलभूत सत्यों को लागू करना

जब आप किसी ऐसे गुण (property) को सत्यापित करना चाहते हैं जो हर संभावित state और function कॉल्स के हर संभावित अनुक्रम में सत्य होना चाहिए, तो invariant चुनें। उदाहरण के लिए:

1. एक ERC-20 कार्यान्वयन में, totalSupply हमेशा सभी व्यक्तिगत उपयोगकर्ता बैलेंस के योग के बराबर होनी चाहिए।
2. एक लेंडिंग प्रोटोकॉल में, संपार्श्विक (collateral) का कुल मूल्य हमेशा कुल ऋण के एक निश्चित प्रतिशत से अधिक या उसके बराबर होना चाहिए, यह मानते हुए कि लिक्विडेशन ठीक से काम कर रहे हैं।
3. एक टोकन contract में, किसी उपयोगकर्ता का बैलेंस कभी भी नकारात्मक नहीं हो सकता है।

Invariants आपके contract की state की दीर्घकालिक अखंडता और सुरक्षा के बारे में सबसे मजबूत गारंटी प्रदान करते हैं। वे इस महत्वपूर्ण प्रश्न का उत्तर देते हैं: “क्या मेरे contract का यह मूलभूत गुण अटूट है, चाहे कुछ भी हो जाए?”

सत्यापन का दायरा (Scope of Verification): Rules बनाम Invariants

जब किसी rule को सत्यापित किया जाता है, तो Prover यह जाँचता है कि प्रारंभिक state, किए गए कार्यों और किन्हीं मान्यताओं (assumptions) के आधार पर rule में परिभाषित विशिष्ट परिदृश्य के लिए assertions सत्य हैं या नहीं। Rules कस्टम पथों (paths) या एज केसेस (edge cases) की खोज के लिए लचीलापन प्रदान करते हैं, लेकिन वे केवल विनिर्देश (specification) में स्पष्ट रूप से बनाए गए execution paths पर ही शुद्धता (correctness) को सत्यापित करते हैं।

इसके विपरीत, एक invariant का सत्य होना आवश्यक है, चाहे कौन से functions कॉल किए गए हों, किन मापदंडों के साथ, या किस क्रम में। Prover को यह सुनिश्चित करना चाहिए कि invariant को contract की प्रत्येक पहुँच योग्य state में बनाए रखा गया है। यह गणितीय आगमन (mathematical induction) पर आधारित दो-भाग वाले प्रमाण सिद्धांत (two-part proof principle) के माध्यम से प्राप्त किया जाता है:

1. आधार स्थिति (Base Case): Contract परिनियोजन (deployment) के तुरंत बाद गुण (property) सत्य होना चाहिए—अर्थात, इसे constructor द्वारा स्थापित किया जाना चाहिए।
2. आगमनात्मक चरण (Inductive Step): Contract में प्रत्येक public या external function के लिए, यदि गुण function को कॉल किए जाने से पहले सत्य है, तो इसे function कॉल के बाद भी सत्य होना चाहिए।

यदि base case और inductive step दोनों सिद्ध हो जाते हैं, तो prover invariant को सत्यापित (verified) (✅) के रूप में रिपोर्ट करता है।

Certora में Invariant लिखना

अभ्यास में invariant सत्यापन कैसे काम करता है, यह समझने के लिए, आइए Certora documentation से सरल Voting contract को देखें:

Copy
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

/// @title A simple voting contract
contract Voting {

    // `hasVoted[user]` is true if the user voted.
    mapping(address => bool) public hasVoted;

    uint256 public votesInFavor;  // keep the count of votes in favor

    uint256 public votesAgainst;  // keep the count of votes against
    uint256 public totalVotes;    // keep the count of total votes cast


    /// @notice Allows a user to vote in favor of the proposal.
    function voteInFavor() external {
        // Ensure the user has not already voted
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

        votesInFavor += 1;
        totalVotes += 1;
    }

    /// @notice Allows a user to vote against the proposal.
    function voteAgainst() external {
        // Ensure the user has not already voted
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

        votesAgainst += 1;
        totalVotes += 1;
    }
    
    
}

उपरोक्त Voting contract उपयोगकर्ताओं को किसी प्रस्ताव के पक्ष या विपक्ष में एक ही वोट डालने की अनुमति देता है। दोहरे मतदान (double voting) को रोकने के लिए, contract एक hasVoted मैपिंग का उपयोग करता है जो रिकॉर्ड करता है कि क्या किसी एड्रेस ने पहले ही भाग लिया है। यह तीन अलग-अलग काउंटरों के माध्यम से वोटों को ट्रैक करता है: votesInFavor, votesAgainst, और totalVotes। जब कोई उपयोगकर्ता voteInFavor() या voteAgainst() functions का उपयोग करके वोट डालता है, तो उपयुक्त काउंटर बढ़ जाता है (incremented), और hasVoted स्थिति अपडेट हो जाती है।

Voting Contract में प्रमुख Invariant की पहचान करना

चूँकि हमारा लक्ष्य हमारे Voting contract के invariants को औपचारिक रूप से सत्यापित करना है, इसलिए हमें सबसे पहले इसके प्रमुख गुणों की पहचान करने की आवश्यकता है। हमारे Voting contract को देखते हुए, महत्वपूर्ण invariants में से एक यह है कि वोटों की कुल संख्या हमेशा पक्ष में और विपक्ष में पड़े वोटों के योग के बराबर होनी चाहिए।

इस प्रमुख invariant की पहचान होने के बाद, आइए Certora का उपयोग करके इसे औपचारिक रूप से निर्दिष्ट और सत्यापित करने की प्रक्रिया को समझते हैं।

अपने प्रोजेक्ट एनवायरनमेंट को सेट अप करना

हमारे invariant को सत्यापित करना शुरू करने के लिए, हमें पहले अपने प्रोजेक्ट संरचना और वातावरण को स्थापित करने की आवश्यकता है। ऐसा करने के लिए, नीचे दिए गए निर्देशों का पालन करें:

1. certora-invariants-examples नाम की एक खाली डायरेक्टरी बनाएं, और उसमें नेविगेट करें।
2. अपनी प्रोजेक्ट डायरेक्टरी के अंदर, निम्नलिखित कमांड चलाकर प्रोजेक्ट के लिए एक Python वर्चुअल एनवायरनमेंट बनाएं।

Copy
virtualenv certora-env

3. नीचे दिए गए कमांड को चलाकर आपके द्वारा बनाए गए Python वर्चुअल एनवायरनमेंट को सक्रिय (activate) करें।

Copy
source certora-env/bin/activate

4. अपने वर्चुअल एनवायरनमेंट में Certora-CLI स्थापित करने के लिए नीचे दिया गया कमांड चलाएँ।

Copy
pip3 install certora-cli

5. अपने वर्चुअल एनवायरनमेंट में solc-select स्थापित करने के लिए नीचे दिया गया कमांड चलाएँ।

Copy
pip3 install solc-select

6. अपनी प्रोजेक्ट डायरेक्टरी में, contracts, specs, और confs नाम की तीन सबडायरेक्टरीज़ (subdirectories) बनाएँ।
7. अपनी प्रोजेक्ट डायरेक्टरी में, contracts सबफ़ोल्डर में नेविगेट करें और Voting.sol नाम की एक फ़ाइल बनाएँ। फिर, ऊपर चर्चा किए गए Voting contract को उस फ़ाइल में पेस्ट करें।

Specification File में Invariant को परिभाषित करना

एक बार प्रोजेक्ट एनवायरनमेंट तैयार हो जाने के बाद, अगला कदम एक specification फ़ाइल बनाना है जहाँ हम अपने invariant को परिभाषित करेंगे।

1. एक Specification फ़ाइल बनाएँ: अपनी प्रोजेक्ट डायरेक्टरी में, specs सबफ़ोल्डर में नेविगेट करें और एक specification फ़ाइल (जैसे, invariant.spec) बनाएँ। इस फ़ाइल में आपके CVL rules शामिल होंगे, जिनमें वे invariants भी शामिल हैं जिन्हें आप सत्यापित करना चाहते हैं।

2. Invariant घोषित करें: अपनी specification फ़ाइल के अंदर, एक invariant को परिभाषित करने के लिए invariant कीवर्ड का उपयोग करें। इसे एक वर्णनात्मक (descriptive) नाम दें जो स्पष्ट रूप से बताए कि rule क्या जाँचता है।

Copy
invariant totalVotesMatch()

3. Invariant स्थिति को CVL Expression के रूप में सम्मिलित करें: इसके बाद, उस स्थिति को निर्दिष्ट करें जो हमेशा सत्य होनी चाहिए। Voting contract के मामले में, हम यह सुनिश्चित करना चाहते हैं कि वोटों की कुल संख्या हमेशा पक्ष में और विपक्ष में पड़े वोटों के योग के बराबर हो:

Copy
invariant totalVotesMatch()
  to_mathint(totalVotes()) == votesInFavor() + votesAgainst();

नोट: to_mathint का उपयोग सुरक्षित तुलना के लिए Solidity के uint256 को Certora के गणितीय पूर्णांकों (mathematical integers) में बदलने के लिए किया जाता है। इसे समीकरण के दाईं ओर लागू करने की आवश्यकता नहीं है, क्योंकि CVL में, सभी अंकगणितीय संचालन (arithmetic operations) के परिणाम स्वचालित रूप से mathint प्रकार के होते हैं।

4. Methods Block जोड़ें: इसके बाद, आइए सही प्रविष्टियों (entries) के साथ अपने विनिर्देश (specification) के शीर्ष पर एक Methods Block जोड़ें।

Copy
methods {
    function totalVotes() external returns(uint256);
    function votesInFavor() external returns(uint256);
    function votesAgainst() external returns(uint256);
}


invariant totalVotesMatch()
    to_mathint(totalVotes()) == votesInFavor() + votesAgainst();

Functions को envfree के रूप में घोषित करना: चूँकि getter functions votesInFavor(), votesAgainst(), और totalVotes() execution एनवायरनमेंट पर निर्भर नहीं करते हैं (अर्थात, वे msg.sender, msg.value, या किसी अन्य वैश्विक चर (global variables) से नहीं पढ़ते हैं), हम उन्हें envfree के रूप में घोषित कर सकते हैं।

Copy
methods {
    function totalVotes() external returns(uint256) envfree;
    function votesAgainst() external returns(uint256) envfree;
    function votesInFavor() external returns(uint256) envfree;
}

invariant totalVotesMatch()
    to_mathint(totalVotes()) == votesInFavor() + votesAgainst();

सत्यापन (Verification) चलाना

एक बार जब आपकी प्रोजेक्ट डायरेक्टरी सही ढंग से सेट हो जाती है, तो Certora Prover चलाने और अपने invariant को सत्यापित करने के लिए नीचे दिए गए चरणों का पालन करें।

1. एक Configuration फ़ाइल बनाएँ: confs सबफ़ोल्डर में, एक कॉन्फ़िगरेशन फ़ाइल बनाएँ (जैसे, invariant.conf) और नीचे दिए गए कोड को उसमें पेस्ट करें।

Copy
{
    "files": [
        "contracts/Voting.sol:Voting"
    ],
    "verify": "Voting:specs/invariant.spec",
    "msg": "Testing Invariant"
}

2. Certora Personal Access Key जोड़ें: अपनी प्रोजेक्ट डायरेक्टरी में, एक .profile, .bashrc, या .zshenv फ़ाइल बनाएँ (आपके ऑपरेटिंग सिस्टम और शेल के आधार पर) और अपनी Certora Personal Access Key को environment variable के रूप में सेट करने के लिए निम्नलिखित लाइन जोड़ें।

Copy
#certora access key
export CERTORAKEY=<add-your-certora-access-key-here>

3. Environment Variable लोड करें: Key जोड़ने के बाद, नीचे दिए गए उपयुक्त कमांड को चलाकर environment variables को अपने वर्तमान टर्मिनल सत्र (session) में लोड करें।

Copy
# For bash users
source .profile

# For zsh users
source .zshenv

4. Solidity Compiler जोड़ना: इससे पहले कि हम Prover चलाएँ, हमें सही Solidity compiler जोड़ने की आवश्यकता है। सही Solidity compiler वर्ज़न जोड़ने और उपयोग करने के लिए, नीचे दिए गए कमांड चलाएँ।

Copy
solc-select install 0.8.25
solc-select use 0.8.25

5. Prover चलाना: अपने invariant को सत्यापित करने के लिए, अपने प्रोजेक्ट की रूट (root) डायरेक्टरी से निम्नलिखित कमांड चलाएँ।

Copy
certoraRun confs/invariant.conf

यदि Prover आपके smart contract और specification फ़ाइल को सफलतापूर्वक संकलित (compile) करता है—बिना किसी सिंटैक्स या अर्थ संबंधी त्रुटियों (semantic errors) का सामना किए, तो यह सत्यापन रिपोर्ट का एक लिंक उत्पन्न करेगा और इसे आपके टर्मिनल आउटपुट में प्रिंट करेगा।

सत्यापन परिणाम देखने के लिए, अपने टर्मिनल में मुद्रित (printed) लिंक को ब्राउज़र का उपयोग करके खोलें। परिणाम नीचे दी गई छवि (image) के समान दिखने चाहिए:

नोट: आपके विनिर्देश (specification) की जटिलता और वर्तमान Prover कतार (queue) के आधार पर, आपके जॉब स्टेटस को Queued से Executed में बदलने में कुछ मिनट लग सकते हैं। यह देरी सामान्य है, इसलिए चिंता न करें।

ऊपर दिखाया गया सत्यापन परिणाम इस बात की पुष्टि करता है कि Prover ने हमारे invariant को सफलतापूर्वक मान्य (validate) कर दिया है। इसका मतलब यह है कि, विश्लेषण के आधार पर, ऐसा कोई परिदृश्य (scenario) नहीं मिला जहाँ invariant को तोड़ा जा सके, जो यह दर्शाता है कि यह contract के पूरे व्यवहार के दौरान लगातार सत्य बना रहता है।

किसी invariant के “सफलतापूर्वक मान्य (successfully validated)” होने का क्या अर्थ है, यह बेहतर ढंग से समझने के लिए, आइए जाँच करें कि Prover पर्दे के पीछे invariants को कैसे सत्यापित करता है।

Invariants को कैसे सत्यापित किया जाता है?

जब किसी invariant को सत्यापन के लिए सबमिट किया जाता है, तो Prover इसकी शुद्धता सुनिश्चित करने के लिए दो आवश्यक जाँच करता है, जो सीधे पहले चर्चा किए गए दो-भाग वाले प्रमाण सिद्धांत (two-part proof principle) (गणितीय आगमन पर आधारित) से मेल खाते हैं:

• प्रारंभिक अवस्था की जाँच (Initial-state Check): सबसे पहले, Prover यह सत्यापित करता है कि contract का constructor का निष्पादन (execution) समाप्त होने के तुरंत बाद invariant सत्य है। यह हमारे आगमनात्मक प्रमाण (inductive proof) का Base Case है।
• आगमनात्मक चरण (Inductive Step): इसके बाद, Prover जाँचता है कि प्रत्येक public और external method अपने निष्पादन (execution) के दौरान invariant को संरक्षित (preserve) करता है। यह Inductive Step से मेल खाता है, यह सुनिश्चित करते हुए कि यदि गुण किसी function कॉल से पहले सत्य है, तो यह बाद में भी सत्य बना रहता है।

Prover UI के बाएं पैनल में invariant totalVotesMatch() को विस्तारित (expand) करके इन दोनों जाँचों के परिणाम देखे जा सकते हैं।

Initial-state check का परिणाम “Induction base: After the constructor” के अंतर्गत प्रदर्शित होता है, जो इस बात की पुष्टि करता है कि contract एक वैध (valid) state में शुरू होता है जहाँ invariant सत्य है।

Inductive step का परिणाम “Induction step: after external (non-view) methods” के अंतर्गत प्रदर्शित होता है। प्रमाण के इस हिस्से को यह दिखाने के लिए डिज़ाइन किया गया है कि सभी public और external functions invariant को संरक्षित करते हैं।

तो, रिपोर्ट केवल “non-view” (state बदलने वाले) methods क्यों दिखाती है?

यह Prover द्वारा किया गया एक चतुर अनुकूलन (optimization) है। Solidity compiler गारंटी देता है कि view और pure functions contract की state को नहीं बदलते हैं। इसका तर्क इस प्रकार है:

1. हम मान लेते हैं कि किसी भी function कॉल से पहले invariant सत्य है (आगमन परिकल्पना / induction hypothesis)।
2. एक view function कॉल किया जाता है।
3. चूँकि contract की state वैसी ही (identical) रहती है, इसलिए कॉल के बाद भी invariant सत्य होना चाहिए।

चूँकि view और pure functions कभी भी contract की state नहीं बदलते हैं, इसलिए inductive step के दौरान उन्हें फिर से सत्यापित करने की कोई आवश्यकता नहीं है। उनकी शुद्धता (correctness) पहले से ही induction base जाँच द्वारा सुनिश्चित की जाती है जो इस बात की पुष्टि करती है कि contract एक वैध state में शुरू होता है। इन अनावश्यक जाँचों को छोड़ने से Prover को सत्यापन संसाधनों को बचाने और रिपोर्ट से अनावश्यक अव्यवस्था (clutter) को दूर करने में मदद मिलती है।

इसलिए, inductive step जाँच उन methods पर केंद्रित होती है जो state को बदल सकते हैं।

हमारे मामले में, इस जाँच के तहत voteAgainst() और voteInFavor() दोनों का विश्लेषण किया जाता है। प्रत्येक function के आगे हरे चेकमार्क (✅) यह दर्शाते हैं कि, जब इन methods को लागू (invoke) किया जाता है, तो वे invariant का उल्लंघन नहीं करते हैं। यह इस बात की पुष्टि करता है कि contract का लॉजिक (logic) सभी state-changing संचालन में invariant को सही ढंग से संरक्षित करता है।

इन दो मुख्य जाँचों के अलावा, Prover envFreeFuncsStaticCheck नामक एक rule भी चलाता है, जो यह सत्यापित करता है कि specification में envfree के रूप में चिह्नित सभी functions निष्पादन वातावरण (execution environment) जैसे msg.sender या msg.value से वास्तव में स्वतंत्र हैं।

Prover UI में अतिरिक्त जाँचों को समझना

यदि आप Certora Prover के किसी नए वर्ज़न का उपयोग कर रहे हैं, तो Prover UI में किसी invariant परिणाम को विस्तारित (expand) करते समय आप अतिरिक्त प्रविष्टियाँ देख सकते हैं, जैसे rule_not_vacuous और invariant_not_trivial_postcondition, जैसा कि नीचे दिखाया गया है:

ये अतिरिक्त प्रविष्टियाँ Prover द्वारा ही जोड़ी गई स्वचालित विवेक जाँच (automatic sanity checks) हैं। वे कोई ऐसी चीज़ नहीं हैं जो आपने लिखी हो, और उनका यह अर्थ नहीं है कि अतिरिक्त invariants या rules सत्यापित किए जा रहे हैं। उनका उद्देश्य यह सुनिश्चित करना है कि आपका invariant वास्तव में सार्थक (meaningful) है और केवल तुच्छ रूप से संतुष्ट (trivially satisfied) नहीं है।

नोट: Certora Prover v8.1.0 से, बुनियादी विवेक जाँच (basic sanity checks) डिफ़ॉल्ट रूप से चलती हैं ("rule_sanity": "basic" सेट करने के बराबर)। पहले, डिफ़ॉल्ट "none" था। आप इन जाँचों को अक्षम (disable) करने के लिए --rule_sanity CLI विकल्प का उपयोग करके या अपनी कॉन्फ़िगरेशन फ़ाइल में "rule_sanity": "none" जोड़कर इस व्यवहार को नियंत्रित कर सकते हैं। उपलब्ध सभी sanity checks के विस्तृत विवरण के लिए, Rule Sanity Checks documentation देखें।

ये जाँचें क्या सत्यापित करती हैं:

• rule_not_vacuous: इस बात की पुष्टि करता है कि invariant का वास्तव में यथार्थवादी (realistic) परिस्थितियों में मूल्यांकन किया जा रहा है। “Vacuous” (शून्य/अर्थहीन) परिणाम का अर्थ होगा कि invariant केवल इसलिए पास हो जाता है क्योंकि पूर्व शर्तें (preconditions) कभी पूरी नहीं होती हैं—मूल रूप से, इसका कभी भी सही मायने में परीक्षण नहीं किया गया है।
• invariant_not_trivial_postcondition: यह सुनिश्चित करता है कि invariant की स्थिति contract की state की परवाह किए बिना तुच्छ रूप से सत्य (trivially true) नहीं है (उदाहरण के लिए, कोई ऐसा expression जिसका मूल्यांकन हमेशा true होता हो)।

ये अतिरिक्त जाँचें मुख्य सत्यापन प्रक्रिया को नहीं बदलती हैं। Prover अभी भी वही दो-भाग वाला आगमनात्मक प्रमाण (two-part inductive proof) करता है: यह सत्यापित करना कि constructor (base case) के बाद invariant सत्य है और यह कि हर state बदलने वाला function इसे संरक्षित करता है (inductive step)। Sanity checks केवल यह अतिरिक्त विश्वास प्रदान करते हैं कि आपके सत्यापन परिणाम सार्थक हैं और specification त्रुटियों की वजह से उत्पन्न नहीं हुए हैं।

निष्कर्ष

Smart contract invariants आपके contract की state के बारे में महत्वपूर्ण दावे (assertions) हैं जो हमेशा सत्य रहने चाहिए। इन invariants को औपचारिक रूप से सत्यापित करना यह सुनिश्चित करता है कि contract सभी संभावित states और method निष्पादन (executions) में अपने इच्छित व्यवहार और शुद्धता को बनाए रखता है।

यह लेख Certora Prover का उपयोग करके औपचारिक सत्यापन (formal verification) पर एक श्रृंखला का हिस्सा है।