अब तक, हमने या तो विशिष्ट व्यवहारों को verify करने के लिए एक rule लिखा है या उन properties को verify करने के लिए एक invariant लिखा है जो contract के पूरे जीवनकाल में हमेशा सत्य रहनी चाहिए। हालाँकि, नई properties को verify करते समय, हम अक्सर यह मान लेना चाहते हैं कि जो अन्य properties हम पहले ही साबित कर चुके हैं, वे आगे भी लागू रहेंगी।

उदाहरण के लिए, टोकन ट्रांसफर के लिए किसी rule को verify करते समय, हम यह मान सकते हैं कि total supply अभी भी सभी balances के योग के बराबर है—एक ऐसी property जिसे पहले ही एक अलग invariant द्वारा साबित किया जा चुका है। साबित किए गए invariants को मान्यताओं (assumptions) के रूप में उपयोग करने से rules उन अवास्तविक contract states (ऐसी states जो उन properties का उल्लंघन करती हैं जिनके बारे में हम पहले ही साबित कर चुके हैं कि वे कभी नहीं हो सकतीं) के कारण विफल (fail) होने से बच जाते हैं।

यहीं पर CVL का requireInvariant स्टेटमेंट काम आता है। requireInvariant स्टेटमेंट हमें उस invariant को लेने की अनुमति देता है जिसे हम पहले ही साबित कर चुके हैं और नए rules या invariants को verify करते समय इसे एक मान्यता के रूप में उपयोग करने की सुविधा देता है।

इस अध्याय में, हम जानेंगे कि requireInvariant क्या है, यह क्यों उपयोगी है, और CVL में rules और invariants लिखते समय इसे प्रभावी ढंग से कैसे लागू किया जाए।

requireInvariant स्टेटमेंट को समझना

requireInvariant स्टेटमेंट एक CVL कंस्ट्रक्ट है जो हमें एक rule या किसी अन्य invariant में एक अतिरिक्त शर्त (condition) के रूप में साबित किए गए invariant को इंजेक्ट करने की अनुमति देता है।

requireInvariant कैसे काम करता है

जब requireInvariant स्टेटमेंट को किसी rule या अन्य invariant में शामिल किया जाता है, तो Prover स्वचालित रूप से यह मान लेता है कि रेफर किया गया invariant verification के दौरान पहले से ही सत्य है। परिणामस्वरूप, यह केवल उन contract states को एक्सप्लोर करता है जो इस शर्त को पूरा करती हैं।

Rules और Invariants में requireInvariant का उपयोग

किसी rule में requireInvariant का उपयोग करने के लिए, बस rule की शुरुआत में invariant को उसके नाम से रेफर करें:

Copy
rule ruleName(env e, ...) {

    requireInvariant invariantName();

    // rule logic here
}

जब invariant (rule के बजाय) के अंदर requireInvariant का उपयोग किया जाता है, तो सिंटैक्स अलग होता है। इस स्टेटमेंट को एक preserved ब्लॉक के भीतर रखा जाता है, जैसा कि नीचे दिखाया गया है:

Copy
invariant invariantName()
    conditionExpression;

{
    preserved with (env e) {
        requireInvariant otherInvariantName();
    }
}

अब जब हम requireInvariant स्टेटमेंट के उद्देश्य को समझ गए हैं और यह कैसे साबित किए गए invariants का पुन: उपयोग (reuse) करने में हमारी मदद करता है, तो आइए देखें कि यह व्यवहार में कैसे काम करता है।

totalSupplyEqSumOfBalances() Invariant पर फिर से विचार करना

ERC20 टोकन के साथ काम करते समय, सबसे बुनियादी सुरक्षा जाँचों (safety checks) में से एक यह सुनिश्चित करना है कि सभी balances का योग हमेशा कुल टोकन सप्लाई (total token supply) के बराबर होना चाहिए। इस invariant को अक्सर token integrity कहा जाता है, जो यह गारंटी देता है कि टोकन अनजाने में बनाए (create) या नष्ट (destroy) नहीं किए जा सकते हैं और सभी व्यक्तिगत balances का योग कुल सप्लाई के बराबर होता है।

“Verifying an Invariant Using Ghosts and Hooks” नामक अध्याय में, हमने निम्नलिखित स्पेसिफिकेशन का उपयोग करके Transmission11 की Solmate लाइब्रेरी से ERC20 इम्प्लीमेंटेशन की इस महत्वपूर्ण सुरक्षा property को औपचारिक रूप से (formally) verify किया था:

Copy
methods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}


invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

आइए देखें कि हम साबित किए गए totalSupplyEqSumOfBalances() invariant को किसी अन्य rule या invariant में एक मान्यता (assumption) के रूप में कैसे उपयोग कर सकते हैं।

Rules में requireInvariant लागू करना

मान लीजिए कि हम अपने ERC20 contract में transfer() फ़ंक्शन की शुद्धता (correctness) को verify करने के लिए एक rule checkTransferSuccess() को परिभाषित करना चाहते हैं। विशेष रूप से, हम यह सुनिश्चित करना चाहते हैं कि एक सफल ट्रांसफर कुल सप्लाई को अपरिवर्तित छोड़ते हुए भेजने वाले (sender) और प्राप्तकर्ता (recipient) के balances को सही ढंग से अपडेट करे।

इस तरह के rule को व्यक्त करने के लिए, हम इन स्टेप्स का पालन करते हैं:

1. transfer() फ़ंक्शन के अपेक्षित व्यवहार (expected behavior) को समझें।
2. इस व्यवहार को verify करने के लिए एक CVL rule लिखें।
3. Verification चलाएं और परिणाम (result) का निरीक्षण करें।

जैसा कि हम देखेंगे, प्रारंभिक verification विफल (fail) हो जाएगा—contract में किसी बग के कारण नहीं, बल्कि इसलिए क्योंकि Prover अवास्तविक (unrealistic) states को एक्सप्लोर करता है। यह हमें समाधान के रूप में requireInvariant को पेश करने की ओर ले जाएगा।

आइए इन स्टेप्स को व्यवहार में लाएं।

transfer() फ़ंक्शन की अपेक्षा (Expectation) को समझना

transfer() सक्सेस कॉल के लिए स्पेसिफिकेशन को परिभाषित करने के लिए, आइए पहले Solmate के ERC20 contract से फ़ंक्शन के इम्प्लीमेंटेशन की जाँच करें:

Copy
function transfer(address to, uint256 amount) public virtual returns (bool) {

    balanceOf[msg.sender] -= amount;

    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

उपरोक्त कोड से, हम देख सकते हैं कि transfer() फ़ंक्शन भेजने वाले (sender) के अकाउंट से प्राप्तकर्ता (recipient) के अकाउंट (to) में एक निर्दिष्ट संख्या में टोकन (amount) ले जाता है। फ़ंक्शन इस लॉजिक का पालन करता है:

• यदि sender के पास पर्याप्त टोकन हैं: sender का बैलेंस amount से घट जाता है, और recipient का बैलेंस उसी मात्रा से बढ़ जाता है।
• यदि sender के पास पर्याप्त टोकन नहीं हैं: operation अंकगणितीय अंडरफ्लो (arithmetic underflow) के कारण स्वचालित रूप से revert हो जाता है, और कोई state परिवर्तन नहीं होता है।

CVL में हमारी transfer() कॉल की अपेक्षा (Expectation) को व्यक्त करना

अब जब हमें transfer() फ़ंक्शन के अपेक्षित व्यवहार की स्पष्ट समझ हो गई है, तो हम इन स्टेप्स का पालन करके इसे CVL कोड में बदल सकते हैं:

1. स्पेसिफिकेशन फ़ाइल खोलें: अपनी Certora प्रोजेक्ट डायरेक्टरी के अंदर, specs सबडायरेक्टरी में नेविगेट करें और उस erc20.spec फ़ाइल को खोलें जिसे हमने totalSupplyEqSumOfBalances() invariant को verify करने के लिए बनाया था। फ़ाइल में निम्नलिखित स्पेसिफिकेशन होना चाहिए:

Copy
methods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

2. एक rule जोड़ें: checkTransferCall() नामक एक नया rule ब्लॉक जोड़कर erc20.spec फ़ाइल का विस्तार (extend) करें।

Copy
rule checkTransferSuccess() {
    // we’ll fill this step by step
}

3. Environment आर्गुमेंट को शामिल करें: चूँकि हमारी transfer() कॉल को ट्रांज़ैक्शन environment (जैसे msg.sender और अन्य EVM context variables) तक पहुँच की आवश्यकता होती है, इसलिए हम इस environment को env e प्रकार के आर्गुमेंट के रूप में पास करते हैं।

Copy
rule checkTransferSuccess(env e) {
    // we’ll fill this step by step
}

4. Inputs डिक्लेयर करें: transfer() फ़ंक्शन के लिए दो inputs की आवश्यकता होती है: एक प्राप्तकर्ता (recipient) एड्रेस (address) और ट्रांसफर करने के लिए टोकन की मात्रा (amount)। हम इन्हें अपने rule में लोकल वेरिएबल्स (local variables) के रूप में घोषित (declare) करते हैं।

Copy
rule checkTransferSuccess(env e){

    // NEWLY ADDED //
    address to;
    uint256 amount;
    
}

5. Environment में न्यूनतम शर्तें (minimal constraints) जोड़ें: प्रत्येक इनपुट कॉम्बिनेशन (input combination) verification के लिए एक वैध परिदृश्य (valid scenario) का प्रतिनिधित्व नहीं करता है। उदाहरण के लिए, हम नहीं चाहते कि कॉलर (msg.sender) स्वयं contract हो, और हम उन ट्रांसफर्स की अनुमति नहीं देना चाहते जहाँ भेजने वाला (sender) और प्राप्तकर्ता (recipient) एक ही अकाउंट हों। हम इन अमान्य परिदृश्यों (invalid scenarios) को बाहर करने (exclude) के लिए require स्टेटमेंट्स जोड़ते हैं।

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;
    
    // NEWLY ADDED //
    require e.msg.sender != currentContract;
    require e.msg.sender != to;
}

6. प्री-कॉल (pre-call) state कैप्चर करें: transfer() कॉल करने से पहले, हम sender का बैलेंस, recipient का बैलेंस और कुल सप्लाई (total supply) रिकॉर्ड करते हैं। ये मान एक बेसलाइन (baseline) के रूप में कार्य करते हैं जिसके विरुद्ध हम कॉल के बाद होने वाले बदलावों को verify करते हैं।

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;
    
    // NEWLY ADDED //
    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();
}

7. transfer() फ़ंक्शन को कॉल (Invoke) करें: अब हम environment e का उपयोग करके, recipient एड्रेस to और ट्रांसफर की मात्रा amount के साथ transfer() फ़ंक्शन को कॉल करते हैं।

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();
    
    // NEWLY ADDED //
    transfer(e,to,amount);
    
}

नोट: हम @withrevert मॉडिफायर (modifier) के बिना transfer() को कॉल करते हैं—इसका मतलब है कि rule केवल उन executions को verify करता है जहाँ ट्रांसफर सफल होता है। यदि ट्रांसफर रिवर्ट (revert) हो जाता है (उदाहरण के लिए, अपर्याप्त बैलेंस के कारण), तो Prover बस उस पथ (path) को verification से बाहर कर देता है।

8. पोस्ट-कॉल (post-call) state कैप्चर करें: ट्रांसफर निष्पादित (execute) होने के बाद, हम एक बार फिर sender का बैलेंस, recipient का बैलेंस और कुल सप्लाई (total supply) कैप्चर करते हैं ताकि हम उनकी तुलना अपनी अपेक्षाओं (expectations) से कर सकें।

Copy
rule checkTransferSuccess(env e) {

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;


    mathint precallSenderBalance = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer@withrevert(e,to,amount);
    bool transferCallStatus = lastReverted;

    // NEWLY ADDED //
    mathint postcallSenderBalance = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();
    
}

9. परिणामों (outcomes) की शुद्धता (correctness) का दावा (Assert) करें: इसके बाद, हम अपनी अपेक्षाओं को assertions के रूप में एनकोड करते हैं:

• Sender का बैलेंस ठीक amount से कम होना चाहिए।
• Recipient का बैलेंस ठीक amount से बढ़ना चाहिए।
• कुल सप्लाई (Total supply) अपरिवर्तित रहनी चाहिए (ट्रांसफर टोकन को एक स्थान से दूसरे स्थान पर ले जाते हैं, वे उन्हें बनाते या नष्ट नहीं करते हैं)।

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer(e, to, amount);

    mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();
    
    // NEWLY ADDED //
    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;
}

10. Methods ब्लॉक को अपडेट करें: पहले, हमारे methods ब्लॉक में केवल totalSupply() फ़ंक्शन शामिल था, क्योंकि स्पेसिफिकेशन में स्पष्ट रूप से केवल इसी को कॉल (invoke) किया गया था। अब, हमें balanceOf() फ़ंक्शन को भी शामिल करने की आवश्यकता है, क्योंकि हमारा rule अकाउंट के balances को पढ़ने के लिए इसे रेफर करता है।

Copy
methods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree; // Add this
}

totalSupply() के समान, balanceOf() फ़ंक्शन ट्रांज़ैक्शन environment पर निर्भर नहीं करता है (उदाहरण के लिए, यह msg.sender या msg.value का उपयोग नहीं करता है)। इसलिए, हम इसे envfree के रूप में डिक्लेयर करते हैं।

नोट: यदि आप सोच रहे हैं कि हम balanceOf() फ़ंक्शन का उपयोग कैसे कर रहे हैं, भले ही यह contract सोर्स (source) में दिखाई नहीं देता है, तो इसका उत्तर इस बात में निहित है कि Solidity पब्लिक स्टेट वेरिएबल्स (public state variables) को कैसे हैंडल करती है। जब आप mapping(address => uint256) public balanceOf; जैसे वेरिएबल को डिक्लेयर करते हैं, तो कंपाइलर स्वचालित रूप से इस सिग्नेचर (signature) के साथ एक getter फ़ंक्शन उत्पन्न (generate) करता है:

Copy
function balanceOf(address) external view returns (uint256);

यह getter कंपाइल किए गए contract के इंटरफ़ेस का हिस्सा है, भले ही इसे सोर्स में स्पष्ट रूप से नहीं लिखा गया हो।

वैकल्पिक (Optionally) रूप से, हम methods ब्लॉक में transfer() फ़ंक्शन के सिग्नेचर को भी शामिल कर सकते हैं। हालाँकि, ऐसा करने से verification के प्रदर्शन (performance) में सुधार नहीं होगा, क्योंकि यह फ़ंक्शन envfree नहीं है।

Copy
methods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree;
    function transfer(address,uint256) external returns(bool);
}

प्रारंभिक (Initial) Verification चलाना

अब जब हमारा rule checkTransferSuccess() पूरा हो गया है, तो आइए Prover को चलाकर (run करके) देखें कि क्या यह verification को पास करता है।

Verification चलाने के लिए, नीचे दिए गए निर्देशों (instructions) का पालन करें:

1. सुनिश्चित करें कि आपकी .conf फ़ाइल नीचे दिए गए कॉन्फ़िगरेशन (configuration) से मेल खाती है:

Copy
{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}

2. इसके बाद, अपने टर्मिनल में निम्नलिखित कमांड निष्पादित (execute) करें:

Copy
certoraRun confs/erc20.conf

यह आपके स्पेसिफिकेशन और contract को verification के लिए Certora Prover को भेज देगा।

3. एक बार जब Prover अपना काम पूरा कर लेता है (जिसमें कुछ मिनट लग सकते हैं), तो यह आपके टर्मिनल में verification रिपोर्ट का एक विशिष्ट (unique) लिंक आउटपुट करेगा। नीचे दी गई इमेज के समान परिणाम (result) देखने के लिए अपने ब्राउज़र में लिंक खोलें:

परिणाम से पता चलता है कि checkTransferSuccess() verification में विफल (failed) हो गया है।

विफलता (Failure) को समझना

Rule विफल क्यों हुआ, यह समझने के लिए आइए कॉल ट्रेस (call trace) की जाँच करें। Global State #1 के अंतर्गत Storage State सेक्शन में, हम Prover द्वारा चुने गए प्रारंभिक मान (initial values) देख सकते हैं:

Prover ने निम्नलिखित मानों के साथ एक state से शुरुआत की:

Storage State (ERC20):

• balanceOf[0x2712] = 0x7 (7 टोकन)
• balanceOf[0x25fc] = 2^256 - 5 (एक खगोलीय रूप से बड़ा मान)
• totalSupply = 0x6 (केवल 5 टोकन)
• sumOfBalances = 2^256 + 8 ( Ghost State)

प्रत्येक मान के दाईं ओर HAVOC लेबल पर ध्यान दें। यह इंगित करता है कि ये मान Prover द्वारा मनमाने ढंग से (arbitrarily) चुने गए थे।

यहाँ विसंगति (inconsistency) चौंकाने वाली है: एक अकाउंट में 2^256 - 5 टोकन हैं, फिर भी कुल सप्लाई (total supply) केवल 6 है। एक अन्य अकाउंट में 7 टोकन हैं—जो कुल सप्लाई से एक अधिक है। इस बीच, घोस्ट (ghost) वेरिएबल sumOfBalances को 2^256 + 8 पर सेट किया गया है, जिसका न तो व्यक्तिगत balances से और न ही कुल सप्लाई से कोई संबंध है।

ऐसा इसलिए होता है क्योंकि Prover किसी नए rule को verify करते समय स्वचालित रूप से यह नहीं मान लेता है कि हमारा पहले से साबित किया गया invariant totalSupplyEqSumOfBalances() लागू है। प्रत्येक rule एक नए सिम्बोलिक स्टेट (symbolic state) से शुरू होता है जहाँ स्टोरेज वेरिएबल्स और घोस्ट्स (ghosts) को मनमाने मान सौंपे जाते हैं, जब तक कि हम स्पष्ट रूप से उन्हें बाध्य (constrain) नहीं करते। परिणामस्वरूप, Prover उन states को एक्सप्लोर करता है जो वास्तविक ERC-20 execution में कभी नहीं हो सकतीं—ऐसी states जहाँ balances, ghost और कुल सप्लाई के बीच का अकाउंटिंग संबंध (accounting relationship) पूरी तरह से टूटा हुआ होता है।

जब transfer() इन अवास्तविक स्थितियों के तहत निष्पादित (execute) होता है, तो बैलेंस में बदलाव के बारे में हमारे assertions विफल हो जाते हैं, भले ही contract का लॉजिक सही हो।

requireInvariant के साथ विफलता (Failure) को ठीक करना

ऐसी असंगत states को बाहर करने (rule out) के लिए, हमें Prover को यह बताना होगा कि checkTransferCall() को केवल इस मान्यता (assumption) के तहत जाँचा जाना चाहिए कि totalSupplyEqSumOfBalances() पहले से ही लागू है।

हम rule की शुरुआत में ही निम्नलिखित लाइन डालकर ऐसा करते हैं:

Copy
requireInvariant totalSupplyEqSumOfBalances();

यह लाइन Prover को एक ऐसी state से verification शुरू करने के लिए कहती है जहाँ हमारा पहले का invariant पहले से ही सत्य है। सरल शब्दों में, Prover केवल उन स्थितियों में rule की जाँच करेगा जहाँ कुल सप्लाई (total supply) पहले से ही सभी balances के योग के बराबर हो।

यहाँ requireInvariant के साथ पूरा rule दिया गया है:

Copy
// Our Rule
rule checkTransferSuccess(env e){
   
   requireInvariant totalSupplyEqSumOfBalances();

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer(e,to,amount);

    mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();
    
    
    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;
 
}

Verification को फिर से चलाना

अब requireInvariant स्टेटमेंट के साथ Prover को फिर से चलाते हैं:

Copy
certoraRun confs/erc20.conf

परिणाम देखने के लिए verification लिंक खोलें:

हमारा verification परिणाम स्पष्ट रूप से दिखाता है कि Prover ने rule को verify कर लिया है। इसका मतलब है कि transfer() फ़ंक्शन balances को सही ढंग से अपडेट करता है और total supply invariant को सुरक्षित (preserve) रखता है।

ऊपर चर्चा किया गया उदाहरण यह स्पष्ट करता है कि requireInvariant को जोड़ने से यह सुनिश्चित होता है कि Prover केवल यथार्थवादी (realistic) contract states पर विचार करता है जो पहले से साबित हुई ग्लोबल properties का सम्मान करते हैं। अगले सेक्शन में, हम देखेंगे कि किसी अन्य invariant परिभाषा (definition) के भीतर requireInvariant का उपयोग कैसे किया जाए।

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

यह समझने के लिए कि CVL के invariant कंस्ट्रक्ट के अंदर requireInvariant का उपयोग कैसे किया जा सकता है, आइए अपनी erc20.spec फ़ाइल के अंदर (ठीक totalSupplyEqSumOfBalances() invariant के नीचे) indBalanceCap() नामक एक अन्य invariant को परिभाषित करें।

Copy
///..
invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

// Our new Invariant
invariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) <= to_mathint(totalSupply());
//.....

यह नया invariant एक मूलभूत ERC-20 सुरक्षा property को एनकोड करता है: किसी भी अकाउंट का बैलेंस कभी भी कुल सप्लाई (total supply) से अधिक नहीं होना चाहिए।

हमारे नए Invariant को Verify करना

अब Prover को चलाते हैं, और फिर नीचे दी गई इमेज के समान परिणाम देखने के लिए Prover द्वारा प्रदान किए गए verification लिंक को खोलते हैं:

उपरोक्त परिणाम दिखाता है कि हमारा invariant indBalanceCap() verification प्रक्रिया में विफल हो गया है।

Prover रिपोर्ट के आगे के विश्लेषण (analysis) से पता चलता है कि invariant इंडक्शन जाँच (induction check) में विफल रहा। विशेष रूप से, Prover ने transfer() और transferFrom() फ़ंक्शन कॉल्स के माध्यम से invariant के उल्लंघनों (violations) की पहचान की, जैसा कि नीचे दी गई इमेज में दिखाया गया है:

उल्लंघन (violation) के कारण को समझने के लिए, आइए transfer() कॉल ट्रेस का विश्लेषण करें। (नोट: transferFrom() भी इसी कारण से विफल होता है, इसलिए transfer() का विश्लेषण करने से दोनों मामले कवर हो जाते हैं)

उल्लंघन (Violation) को समझना

आइए Prover रिपोर्ट के Storage State सेक्शन के साथ अपना विश्लेषण शुरू करें। यह सेक्शन verification के प्रारंभिक बिंदु (initial point) पर contract के स्टोरेज वेरिएबल्स के वास्तविक मान दिखाता है।

Storage State में, हम देख सकते हैं कि व्यक्तिगत अकाउंट balances इस प्रकार हैं:

• balanceOf[0x2711] = 0x5 (अकाउंट 0x2711 में 5 टोकन हैं)
• balanceOf[0x2713] = 0x4 (अकाउंट 0x2713 में 4 टोकन हैं)

जबकि टोकन की totalSupply केवल 0x4 (यानी 4 टोकन) के रूप में दर्ज की गई है।

चूँकि हम totalSupplyEqSumOfBalances() invariant को पहले ही साबित कर चुके हैं, इसलिए contract के वास्तविक execution के दौरान इस तरह की state कभी नहीं आनी चाहिए। वह invariant कहता है कि हर वैध (valid) state में, कुल सप्लाई (total supply) हमेशा सभी balances के योग के बराबर होनी चाहिए। लेकिन ऊपर दिए गए ट्रेस में, balances का योग 9 हो जाता है जबकि कुल सप्लाई केवल 4 है। यह बेमेलपन (mismatch) दर्शाता है कि Prover ने एक ऐसी state से शुरुआत की है जो वास्तव में हमारे ERC-20 इम्प्लीमेंटेशन में पहुँच योग्य (reachable) नहीं है।

ऐसा इसलिए होता है क्योंकि जब Prover किसी नई property को verify करना शुरू करता है, तो वह स्वचालित रूप से यह नहीं मान लेता है कि पहले साबित किए गए invariants लागू होने चाहिए। प्रत्येक नया rule या invariant एक नए सिम्बोलिक स्टेट से शुरू होता है, जब तक कि हम स्पष्ट रूप से इसे पहले के परिणामों से नहीं जोड़ते। परिणामस्वरूप, Prover एक ऐसा प्रारंभिक कॉन्फ़िगरेशन चुन सकता है जो हमारे द्वारा पहले साबित किए गए invariant का उल्लंघन करता है, भले ही वास्तविक contract execution के दौरान ऐसा कॉन्फ़िगरेशन असंभव हो।

requireInvariant स्टेटमेंट के साथ विफलता (Failure) को ठीक करना

ऐसी असंगत states को बाहर करने के लिए, हमें Prover को यह बताना होगा कि indBalanceCap() को केवल इस मान्यता (assumption) के तहत जाँचा जाना चाहिए कि totalSupplyEqSumOfBalances() पहले से ही लागू है।

इसे लागू (enforce) करने के लिए, हम स्पष्ट रूप से उस invariant को requireInvariant का उपयोग करके इम्पोर्ट करते हैं, जैसा कि नीचे दिखाया गया है:

Copy
invariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) <= to_mathint(totalSupply())
{
    preserved with (env e) {
        // Require that our earlier invariant holds
        requireInvariant totalSupplyEqSumOfBalances();
    }
}

इस तरह, Prover एक ऐसी दुनिया (world) से शुरुआत करता है जो पहले से ही हमारे द्वारा साबित किए गए टोकन-संरक्षण (token-conservation) rule को पूरा करती है और सर्च स्पेस (search space) को असंभव ERC-20 states में भटकने से रोकती है।

मज़बूत (Strengthened) Invariant को Verify करना

अब, यदि हम Prover को इसके साथ फिर से चलाते हैं:

Copy
certoraRun confs/erc20.conf

और verification लिंक खोलते हैं, तो हमें नीचे दी गई इमेज के समान परिणाम दिखाई देगा:

हम देख सकते हैं कि, उम्मीद के मुताबिक, indBalanceCap() अब सफलतापूर्वक verify हो गया है। चूँकि Prover को उन states तक सीमित कर दिया गया था जो पहले से ही totalSupplyEqSumOfBalances() को पूरा करती हैं, इसलिए अब इसका सामना उन असंभव कॉन्फ़िगरेशन से नहीं हुआ जिनके कारण पहले विफलता (failure) हुई थी।

require बनाम requireInvariant: समान फ़िल्टर (Same Filter), अलग गारंटी (Different Guarantee)

दिलचस्प बात यह है कि यदि हम requireInvariant के बजाय एक नियमित require स्टेटमेंट का उपयोग करते हैं, तो indBalanceCap() invariant भी verification पास कर लेगा, जैसा कि नीचे दिखाया गया है:

ऐसा इसलिए होता है क्योंकि, एक preserved ब्लॉक के अंदर, require और requireInvariant दोनों समान परिचालन (operational) उद्देश्य की पूर्ति करते हैं: वे इंडक्शन स्टेप (induction step) की प्री-स्टेट (pre-state) को फ़िल्टर करते हैं। प्रभाव में, दोनों स्टेटमेंट्स Prover को यह निर्देश देते हैं:

“केवल उन ट्रांज़िशन्स (transitions) को एक्सप्लोर करें जो इस शर्त को पूरा करने वाली states से शुरू होते हैं।”

इस कारण से, निम्नलिखित दो लाइनें सर्च स्पेस पर समान कार्यात्मक प्रतिबंध (functional restriction) लगाती हैं:

Copy
requireInvariant totalSupplyEqSumOfBalances();

और

Copy
require to_mathint(totalSupply()) == sumOfBalances;

दोनों Prover को उस असंगत (inconsistent) प्रारंभिक state पर विचार करने से रोकते हैं जो हमने पहले देखी थी, जिससे indBalanceCap() invariant पास हो जाता है।

requireInvariant अभी भी बेहतर (Preferable) क्यों है

हालाँकि दोनों रूप सर्च स्पेस को समान रूप से प्रतिबंधित करते हैं, लेकिन वे इस बात में भिन्न हैं कि परिणामी (resulting) स्पेसिफिकेशन कितना विश्वसनीय (reliable) और सिद्धांतबद्ध (principled) है।

एक requireInvariant अधिक सुरक्षित है क्योंकि यह उस property को इम्पोर्ट करता है जिसे Prover ने सभी पहुँच योग्य (reachable) states में पहले ही सत्य स्थापित कर दिया है। एक साधारण require सही शर्त (condition) बताने के लिए पूरी तरह से स्पेसिफिकेशन लिखने वाले (spec writer) पर निर्भर करता है। उदाहरण के लिए:

Copy
require to_mathint(totalSupply()) == sumOfBalances;

यह Prover को इस समानता (equality) को यह जाँचे बिना स्वीकार करने के लिए बाध्य करता है कि यह वास्तव में सत्य है या नहीं। यदि शर्त थोड़ी सी भी गलत या अधूरी है, तो Prover वास्तविक काउंटर-एग्जांपल (counterexamples) को चुपचाप अनदेखा कर सकता है, जिससे एक भ्रामक (misleadingly) सफल verification मिल सकता है।

इसलिए, मुख्य अंतर सरल है:

• require उस शर्त को लागू करता है जो हम लिखते हैं।
• requireInvariant उस शर्त को लागू करता है जो पहले से ही सार्वभौमिक रूप से (universally) सत्य साबित हो चुकी है।

इस कारण से, requireInvariant मान्यताओं (assumptions) का पुन: उपयोग (reuse) करने का एक अधिक सुरक्षित और सिद्धांतबद्ध तरीका प्रदान करता है, जबकि एक साधारण require अनजाने में वास्तविक उल्लंघनों को छिपा सकता है यदि शर्त गलत या अधूरी है।

निष्कर्ष (Conclusion)

इस तरह से हम अपने स्पेसिफिकेशन्स को अधिक मजबूत, अधिक मॉड्यूलर (modular) और अधिक कुशल (efficient) बनाने के लिए requireInvariant का उपयोग कर सकते हैं।

• Rules में, यह हमें साबित किए गए invariants को पूर्वापेक्षाओं (prerequisites) के रूप में पुन: उपयोग करने की अनुमति देता है, यह सुनिश्चित करते हुए कि प्रत्येक execution पथ (path) की यथार्थवादी (realistic) परिस्थितियों में जाँच की जाती है।
• Invariants में, यह हमें पहले वाली properties को मानकर (assuming) नई properties को साबित करने देता है, जिससे असंगत states से आने वाले अर्थहीन (meaningless) काउंटर-एग्जांपल से बचा जा सकता है।

मुख्य सिद्धांत सरल लेकिन शक्तिशाली है: पहले ग्लोबल invariants को साबित करें, फिर उन्हें बिल्डिंग ब्लॉक्स के रूप में पुन: उपयोग करें जब आप विशिष्ट व्यवहारों या अतिरिक्त invariants को verify कर रहे हों।

यह लेख Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन (formal verification using the Certora Prover) पर एक श्रृंखला का हिस्सा है