यह साबित करने के लिए कि कोई प्रॉपर्टी या इनवेरिएंट (invariant) बना रहता है, अक्सर विशिष्ट स्टोरेज लोकेशन पर बदलावों का निरीक्षण करना आवश्यक हो जाता है, खासकर तब जब स्टोरेज बाहरी रूप से एक्सेस करने योग्य नहीं होता है या जब रुचि के मान स्पष्ट रूप से कैलकुलेट या कॉन्ट्रैक्ट द्वारा उजागर नहीं किए जाते हैं।

उदाहरण के लिए, मान लें कि हम यह सत्यापित (verify) करना चाहते हैं कि, एक ERC-20 इम्प्लीमेंटेशन में, totalSupply का मान हमेशा सभी व्यक्तिगत अकाउंट बैलेंस के योग के बराबर होता है। पहली नज़र में, यह सीधा लगता है: हम assert totalSupply() == sumOfBalances() कर सकते हैं।

हालाँकि, कठिनाई यह है कि कॉन्ट्रैक्ट वास्तव में कभी भी इस संचयी योग (cumulative sum) को मेंटेन नहीं करता है; यह केवल एक मैपिंग में प्रत्येक अकाउंट के बैलेंस को स्टोर करता है। totalSupply के विपरीत, जिसे स्पष्ट रूप से स्टोर किया जाता है और सीधे क्वेरी किया जा सकता है, कॉन्ट्रैक्ट के स्टेट में “sum of balances” मौजूद नहीं होता है। इसके बजाय, यह जानकारी कई स्टोरेज स्लॉट्स में वितरित (distributed) होती है, जिससे यह देखे बिना कि उन स्लॉट्स को कैसे एक्सेस और अपडेट किया जाता है, इस संबंध को सत्यापित करना असंभव हो जाता है। चुनौती तब और भी बड़ी हो जाती है जब इनमें से कुछ वेरिएबल्स प्राइवेट (private) होते हैं।

इस चुनौती से निपटने के लिए, CVL हुक्स (hooks) और घोस्ट वेरिएबल्स (ghost variables) प्रदान करता है। हुक्स हमें लो-level इवेंट्स जैसे स्टोरेज में रीड्स (reads) और राइट्स (writes) को देखने की सुविधा देते हैं, जबकि घोस्ट वेरिएबल्स हमें उन अवलोकनों को कैप्चर करने, एग्रीगेट करने और शेयर करने की अनुमति देते हैं ताकि स्पेसिफिकेशन में कहीं और उनका संदर्भ (reference) दिया जा सके। साथ मिलकर, वे आंतरिक कॉन्ट्रैक्ट व्यवहार और हाई-लेवल वेरिफिकेशन रूल्स के बीच की खाई को पाटते हैं, जिससे हमें उन प्रॉपर्टीज़ के बारे में तर्क करने की अनुमति मिलती है जो छिपे हुए या निहित (implicit) स्टेट परिवर्तनों पर निर्भर करती हैं।

इस अध्याय में, आप सीखेंगे कि हुक्स कैसे काम करते हैं, उपलब्ध विभिन्न प्रकार क्या हैं, और उनके साथ जुड़ी सीमाएँ क्या हैं। हम आपको घोस्ट वेरिएबल्स से भी परिचित कराएंगे, जो एक मुख्य CVL फीचर है और हुक्स और रूल्स के बीच संचार (communication) को सक्षम करता है, जिससे आप उन जटिल करेक्टनेस प्रॉपर्टीज़ को सत्यापित कर सकते हैं जो अन्यथा कॉन्ट्रैक्ट के आंतरिक स्टोरेज में छिपी रहती हैं।

“ज़रूरत” को समझना (“the Need”)

हम जिन समस्याओं के बारे में बात कर रहे हैं, उन्हें बेहतर ढंग से समझने के लिए, नीचे दिए गए स्मार्ट कॉन्ट्रैक्ट पर विचार करें जो डिप्लॉयमेंट के समय सेट किए गए एक प्राइवेट count और एक owner को रखता है। increment() और resetCounter() दोनों ही onlyOwner मॉडिफायर द्वारा सुरक्षित हैं: increment() प्राइवेट count को एक से बढ़ाता है और resetCounter() इसे शून्य पर रीसेट करता है, और केवल कॉन्ट्रैक्ट में स्टोर किया गया owner एड्रेस ही किसी भी फ़ंक्शन को कॉल कर सकता है।

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


contract Counter {

    // State variables
    address private owner;
    uint256 private count;



    /// @notice Initializes the contract and sets the deployer as the owner
    constructor() {
        owner = msg.sender;
    }


    /// @notice Restricts function calls to the contract owner only
    modifier onlyOwner() {
        require(msg.sender == owner, "Counter: caller is not the owner");
        _;
    }

    // External functions

    /// @notice Increments the counter by 1
    /// @dev Only callable by the owner
    function increment() external onlyOwner {
        count++;
    }

    /// @notice Resets the counter to 0
    /// @dev Only callable by the owner
    function resetCounter() external onlyOwner {
        count = 0;
    }
}

अब मान लें कि हम निम्नलिखित प्रॉपर्टीज़ को औपचारिक रूप से सत्यापित (formally verify) करना चाहते हैं:

1. कंस्ट्रक्टर में एक बार सेट होने के बाद owner कभी नहीं बदलना चाहिए।
2. increment() को कॉल करने पर count ठीक एक से बढ़ना चाहिए।

पहली नज़र में, दोनों प्रॉपर्टीज़ सीधी लगती हैं। हालाँकि, उन्हें CVL रूल्स के रूप में व्यक्त करने में कुछ चुनौतियाँ हैं। पहली प्रॉपर्टी को CVL रूल के रूप में व्यक्त करने में समस्या यह है कि owner वेरिएबल को private मार्क किया गया है, और कॉन्ट्रैक्ट इसका मान उजागर करने के लिए कोई गेटर (getter) प्रदान नहीं करता है। इसे किसी रूल से एक्सेस करने में सक्षम हुए बिना, हम यह दावा (assert) नहीं कर सकते कि यह कंस्ट्रक्टर में सेट होने के बाद अपरिवर्तित रहता है।

दूसरी प्रॉपर्टी एक अलग चुनौती पेश करती है। हालाँकि हम किसी रूल के अंदर increment() को कॉल कर सकते हैं, लेकिन वेरिएबल count प्राइवेट है, और कॉन्ट्रैक्ट इसका मान पढ़ने के लिए कोई गेटर प्रदान नहीं करता है। इसका मतलब है कि रूल सीधे यह नहीं देख सकता कि फ़ंक्शन के चलने पर count के साथ क्या होता है।

चूँकि रूल्स केवल फ़ंक्शन के इनपुट्स और आउटपुट्स का निरीक्षण कर सकते हैं, आंतरिक स्टोरेज में होने वाले परिवर्तनों का नहीं, इसलिए उनके पास अपडेट होने पर count के पुराने और नए मानों को कैप्चर करने का कोई तरीका नहीं होता है। उस दृश्यता (visibility) के बिना, Prover इस बात की पुष्टि नहीं कर सकता कि increment() पर प्रत्येक कॉल वास्तव में काउंटर को एक से बढ़ाती है।

सरल शब्दों में कहें तो, समस्या यह नहीं है कि प्रॉपर्टीज़ को बताना मुश्किल है, बल्कि यह है कि वे लो-लेवल स्टोरेज व्यवहार (low-level storage behavior) पर निर्भर करती हैं और इसके लिए प्रत्यक्ष अवलोकन (direct observation) की आवश्यकता होती है कि निष्पादन (execution) के दौरान स्टोरेज कैसे अपडेट होता है। मानक CVL रूल्स कॉन्ट्रैक्ट के सार्वजनिक इंटरफ़ेस (public interface) के माध्यम से इसके साथ इंटरैक्ट करने तक सीमित हैं, इसलिए वे इन आंतरिक परिवर्तनों को कैप्चर नहीं कर सकते। ओनर (owner) की अपरिवर्तनीयता (immutability) या काउंटर के सटीक इंक्रीमेंट (exact increments) जैसी प्रॉपर्टीज़ को सत्यापित करने के लिए, हमें ऐसे टूल्स की आवश्यकता होती है जो हमें कॉन्ट्रैक्ट के अंदर झांकने, इसके स्टोरेज ऑपरेशन्स की निगरानी करने और उन अवलोकनों को हमारे स्पेसिफिकेशन्स में ले जाने की अनुमति दें।

यहीं पर हुक्स (hooks) काम आते हैं।

हुक्स क्या हैं?

CVL में, हुक्स कोड के ऐसे ब्लॉक्स होते हैं जो वेरिफिकेशन प्रक्रिया के दौरान स्वचालित रूप से चलते हैं जब भी कोई स्मार्ट कॉन्ट्रैक्ट लो-लेवल EVM ऑपरेशन्स करता है, जैसे कि स्टोरेज से पढ़ना या लिखना, किसी ओपकोड (opcode) को निष्पादित करना, या ट्रांसिएंट (transient) डेटा को संशोधित करना।

एक हुक को hook कीवर्ड का उपयोग करके परिभाषित किया जाता है, और प्रत्येक CVL हुक निम्नलिखित को निर्दिष्ट करता है:

1. वह ऑपरेशन (operation) जिसे वह सुनता है (उदाहरण के लिए, SLOAD, SSTORE, या कोई विशिष्ट EVM ओपकोड)।
2. CVL कोड का एक ब्लॉक (block of CVL code) जो उस ऑपरेशन के पकड़े जाने पर निष्पादित होता है, जो उस इवेंट से प्रासंगिक डेटा तक एक्सेस प्रदान करता है।

हुक्स के प्रकार

CVL 3 अलग-अलग प्रकार के हुक्स प्रदान करता है, जिन्हें उनके द्वारा मॉनिटर किए जाने वाले ऑपरेशन के प्रकार के आधार पर वर्गीकृत किया गया है। वे 3 प्रकार हैं:

1. Storage Hooks
2. Opcode Hooks
3. Transient Storage Hooks

इस विशिष्ट अध्याय के लिए, हम Storage Hooks पर ध्यान केंद्रित करेंगे, क्योंकि वे सबसे अधिक व्यापक रूप से लागू होते हैं और CVL में हुक्स कैसे काम करते हैं, इसे समझने की नींव बनाते हैं। हुक्स के अन्य प्रकार विशिष्ट संदर्भों में समान रूप से उपयोगी हैं, और हम उन्हें बाद के अध्यायों में कवर करेंगे।

Storage Hooks क्या हैं?

Storage hooks CVL में एक विशिष्ट प्रकार के हुक हैं जो तब ट्रिगर होते हैं जब भी किसी कॉन्ट्रैक्ट के स्टोरेज वेरिएबल को एक्सेस किया जाता है, चाहे वह पढ़ने के लिए हो या लिखने के लिए। दूसरे शब्दों में, वे तब सक्रिय होते हैं जब EVM मॉनिटर किए जा रहे स्टोरेज स्लॉट पर एक रीड (SLOAD) या राइट (SSTORE) ऑपरेशन करता है, जिससे हमें इसकी अनुमति मिलती है:

• पढ़े या लिखे जा रहे मान को कैप्चर करना।
• जब भी किसी वेरिएबल को एक्सेस या संशोधित किया जाता है, तो शर्तों (conditions) को लागू करना।
• यह ट्रैक करना कि विभिन्न निष्पादनों (executions) में कॉन्ट्रैक्ट की स्टेट कैसे विकसित (evolve) होती है।

CVL में स्टोरेज हुक्स के दो मुख्य प्रकार हैं:

1. The Load Hooks
2. The Store Hooks

1. The Load Hooks

एक लोड हुक (A load hook) तब ट्रिगर होता है जब मॉनिटर किए जा रहे स्टोरेज वेरिएबल पर रीड ऑपरेशन (SLOAD) होता है और यह आपको पढ़े जा रहे मान को कैप्चर करने की अनुमति देता है।

इसे hook Sload कीवर्ड्स का उपयोग करके परिभाषित किया गया है, जिसके बाद लोड किए गए मान को होल्ड करने वाले CVL वेरिएबल का प्रकार (type) और नाम, और अंत में, मॉनिटर किए जा रहे कॉन्ट्रैक्ट के स्टोरेज वेरिएबल का नाम होता है।

Copy
hook Sload address contractOwner owner { ... }

उपरोक्त हुक तब निष्पादित होगा जब भी सत्यापन के अधीन कॉन्ट्रैक्ट रीड ऑपरेशन के लिए अपने address प्रकार के owner स्टोरेज वेरिएबल को एक्सेस करेगा। फिर मान को एक CVL वेरिएबल, contractOwner में स्टोर किया जाएगा।

2. The Store Hooks

स्टोर हुक्स (The store hooks) किसी भी विशिष्ट स्टोरेज वेरिएबल पर कोई भी राइट (write) ऑपरेशन होने से पहले निष्पादित होते हैं।

स्टोर हुक्स को भी hook कीवर्ड का उपयोग करके परिभाषित किया जाता है, जिसके बाद Sstore कीवर्ड होता है। इसके बाद, आप मॉनिटर किए जा रहे कॉन्ट्रैक्ट के स्टोरेज वेरिएबल के नाम को निर्दिष्ट करते हैं, साथ ही उस CVL वेरिएबल का प्रकार और नाम जो उस स्टोरेज लोकेशन पर लिखे जाने वाले मान को होल्ड करेगा।

Copy
hook Sstore owner address newOwner{...}

वैकल्पिक रूप से, पैटर्न में ओवरराइट (overwrite) किए जा रहे पिछले मान को स्टोर करने के लिए एक वेरिएबल का प्रकार और नाम भी शामिल हो सकता है।

Copy
hook Sstore owner address newOwner (address oldOwner) {...}

इससे पहले कि हम Counter कॉन्ट्रैक्ट की प्रॉपर्टीज़ को सत्यापित करने के लिए हुक्स लागू करें, समझने के लिए एक महत्वपूर्ण सीमा है: हुक्स के अंदर घोषित (declared) वेरिएबल्स हुक ब्लॉक के लिए स्थानीय (local) होते हैं और रूल्स को सीधे दिखाई नहीं देते हैं।

हुक्स की सीमाओं (Limitations) को समझना

एक हुक न केवल हमें किसी विशिष्ट स्टोरेज वेरिएबल को मॉनिटर करने की अनुमति देता है बल्कि उपयोग के लिए इसे CVL वेरिएबल में स्टोर करके इसके मान तक एक्सेस भी प्रदान करता है। हालाँकि, एक सीमा यह है कि हुक्स के अंदर परिभाषित CVL वेरिएबल्स स्थानीय रूप से हुक के स्कोप में होते हैं, जिसका अर्थ है कि उन्हें सीधे रूल्स से एक्सेस नहीं किया जा सकता है।

इस सीमा को समझने के लिए, नीचे दिए गए स्पेसिफिकेशन पर विचार करें जिसका उद्देश्य यह साबित करना है कि Counter कॉन्ट्रैक्ट का owner कंस्ट्रक्टर में पहली बार सेट होने के बाद कभी नहीं बदलता है:

Copy
hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;


}

उपरोक्त स्पेक (spec) में, हुक Sload प्राइवेट owner वेरिएबल को जब भी पढ़ा जाता है तो देखने योग्य (observable) बनाता है, और इसके मान को contractOwner में स्टोर करता है। रूल में, स्पेक इस अवलोकित मान को prevOwner के रूप में सेव करता है, किसी भी (arbitrary) इनपुट्स के साथ किसी भी कॉन्ट्रैक्ट फ़ंक्शन को एक सिम्बोलिक कॉल करता है, फिर से owner को currentOwner के रूप में अवलोकित करता है। अंत में, यह दावा करता है कि prevOwner == currentOwner, जिसका अर्थ है कि सभी संभावित कॉल्स में, ओनर सुसंगत (consistent) रहना चाहिए।

हालाँकि, जब आप Certora Prover चलाते हैं, तो आपको निम्नलिखित एरर (error) का अनुभव होगा:

उपरोक्त एरर केवल इस तथ्य पर प्रकाश डालती है कि रूल checkOwnerConsistency() हमारे लोड हुक के अंदर घोषित contractOwner को एक्सेस और उपयोग नहीं कर सकता है।

इससे यह सवाल उठ सकता है: यदि हुक्स को डेटा कैप्चर करने और स्टोर करने के लिए डिज़ाइन किया गया है, तो हम उस डेटा का सीधे अपने रूल्स में उपयोग क्यों नहीं कर सकते?

इसका उत्तर हुक्स के भीतर परिभाषित वेरिएबल्स के स्कोप (scope) में निहित है।

हुक्स की स्कोप लिमिटेशन (Scope Limitation)

जब आप किसी हुक के अंदर कोई वेरिएबल परिभाषित करते हैं, तो उसका स्कोप केवल उस हुक तक ही सीमित (local) होता है। यह किसी फ़ंक्शन के अंदर वेरिएबल को परिभाषित करने जैसा है—इसे उस ब्लॉक के भीतर उपयोग किया जा सकता है लेकिन यह बाहर दिखाई नहीं देता है। इसीलिए contractOwner हुक के अंदर पूरी तरह से मान्य (valid) है, लेकिन रूल checkOwnerConsistency() के लिए पूरी तरह से अज्ञात (unknown) है।

इसका मतलब है कि CVL रूल्स और हुक्स वेरिएबल्स साझा (share) नहीं करते हैं—वे अलग-अलग स्कोप्स में काम करते हैं।

तो हम उपयोगी रूल्स लिखने के लिए हुक में निकाली गई जानकारी का उपयोग कैसे कर सकते हैं?

इसका उत्तर है ghost variables.

Ghost के साथ Scope Limitation का समाधान

यद्यपि हम रूल्स के अंदर सीधे हुक वेरिएबल्स को एक्सेस नहीं कर सकते हैं, लेकिन हुक्स और रूल्स के बीच जानकारी संचारित करने के लिए हम ghost variables (या केवल ghosts) नामक विशेष वेरिएबल्स को परिभाषित कर सकते हैं।

नीचे दिखाए अनुसार एक घोस्ट को ghost कीवर्ड का उपयोग करके उसके प्रकार और नाम के साथ घोषित किया जाता है।

Copy
ghost bool hasVoted;
ghost uint x;
ghost mathint numVoted;
ghost mapping(address => mathint) balances;

घोस्ट वेरिएबल कोई भी CVL समर्थित प्रकार (supported type) या मैपिंग हो सकता है। मैपिंग के मामले में, इसकी कीज़ (keys) CVL समर्थित प्रकार की होनी चाहिए, और इसके मान (values) या तो CVL प्रकार या अन्य मैपिंग हो सकते हैं।

Counter कॉन्ट्रैक्ट में Owner की Consistency को सत्यापित करना

checkOwnerConsistency() रूल को उम्मीद के मुताबिक काम कराने के लिए, हुक के अंदर देखे गए मान को रूल के स्कोप में उपलब्ध कराने की आवश्यकता है। हम देखे गए मान को एक घोस्ट वेरिएबल में स्टोर करके ऐसा कर सकते हैं। इसे प्राप्त करने के चरण नीचे दिए गए हैं:

1. owner के देखे गए मान को होल्ड करने के लिए एक घोस्ट घोषित करें: हमारे स्पेसिफिकेशन के शीर्ष स्तर (top level) पर, ghostOwner नामक एक घोस्ट वेरिएबल पेश करें। यह घोस्ट कॉन्ट्रैक्ट के owner स्लॉट के मान के लिए एक कंटेनर के रूप में काम करेगा जब भी इसे पढ़ा जाएगा।

Copy

/// Top-level ghost variable to mirror the contract's `owner` slot
ghost address ghostOwner;

hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;

}

घोस्ट वेरिएबल्स घोषित करते समय, उन्हें Solidity स्टोरेज वेरिएबल्स और हुक-लोकल CVL वेरिएबल्स से स्पष्ट रूप से अलग करने के लिए उनके आगे ghost या ghost_ (उदाहरण के लिए, ghostOwner, ghost_owner) उपसर्ग (prefix) लगाना महत्वपूर्ण है।

इस स्तर पर, घोस्ट वेरिएबल ghostOwner घोषित किया गया है लेकिन अभी तक कॉन्ट्रैक्ट के स्टोरेज के साथ सिंक्रोनाइज़ (synchronized) नहीं हुआ है।

2. हुक के अंदर घोस्ट को सिंक्रोनाइज़ करें: इसके बाद, Sload हुक को इस तरह संशोधित करें कि जब भी कॉन्ट्रैक्ट owner स्टोरेज स्लॉट पर रीड ऑपरेशन करता है, तो हुक मान को कैप्चर कर लेता है और इसे घोस्ट में लिख देता है।

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    //assign captured value to ghost
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;


}

यह कॉन्ट्रैक्ट के प्राइवेट स्टोरेज से हुक में, और हुक से एक घोस्ट वेरिएबल में एक पुल (bridge) बनाता है जो हुक के लोकल स्कोप से परे बना रहता है। हर बार जब कॉन्ट्रैक्ट owner को पढ़ता है, घोस्ट ghostOwner उस स्टोरेज मान के साथ सिंक्रोनाइज़ हो जाता है।

3. रूल के अंदर घोस्ट का उपयोग करें: अंत में, checkOwnerConsistency() रूल को अपडेट करें ताकि हुक-लोकल contractOwner का उपयोग करने के बजाय, यह घोस्ट ghostOwner को संदर्भित (reference) करे।

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

    //Take a snapshot of the ghost before the call
    address prevOwner = ghostOwner;

    //parametric call
    method f;
    calldataarg args;
    f(e,args);
     
    //Take another snapshot after the call
    address currentOwner = ghostOwner;

     
    assert prevOwner == currentOwner;
}

एक बार जब आप ऊपर दिए गए निर्देशों के अनुसार अपने स्पेसिफिकेशन को अपडेट कर लेते हैं, तो certoraRun कमांड का उपयोग करके Certora Prover को फिर से चलाएं। इस बार Prover हमारे रूल को बिना किसी एरर के कंपाइल करेगा और आपके टर्मिनल में वेरिफिकेशन परिणाम प्रिंट करेगा। परिणाम नीचे दी गई छवि (image) के समान होगा:

उपरोक्त परिणाम देखने के बाद, आपको आश्चर्य हो सकता है और आप सोच सकते हैं कि हमारा रूल अभी भी विफल क्यों हुआ, भले ही Counter कॉन्ट्रैक्ट कभी भी स्पष्ट रूप से अपने ओनर को अपडेट नहीं करता है। इसका कारण Solidity कोड में नहीं बल्कि इस बात में है कि Prover घोस्ट्स की व्याख्या कैसे करता है और वेरिफिकेशन रन के दौरान हुक्स कैसे निष्पादित किए जाते हैं।

Ghosts को Storage के साथ सिंक्रोनाइज़ करना

घोस्ट वेरिएबल्स स्वचालित रूप से कॉन्ट्रैक्ट के स्टोरेज से बंधे (tied) नहीं होते हैं। निष्पादन की शुरुआत में, Prover उन्हें हैवोक्ड वैल्यूज़ (havoced values) प्रदान करता है — ऐसे यादृच्छिक प्लेसहोल्डर्स (arbitrary placeholders) जो ट्रेसेस (traces) में बदल सकते हैं जब तक कि उन्हें स्पष्ट रूप से इनिशियलाइज़ नहीं किया जाता है। हमारे मामले में, घोस्ट ghostOwner केवल तभी अपडेट होता है जब owner स्लॉट पढ़ा जाता है (Sload के माध्यम से)। यदि रूल द्वारा prevOwner और currentOwner की तुलना करने से पहले कोई रीड ऑपरेशन नहीं होता है, तो घोस्ट अन-इनिशियलाइज़्ड (uninitialised) रहता है, और वास्तविक स्टोरेज से असंबद्ध एक यादृच्छिक मान रखता है।

वास्तव में यही हुआ: owner के स्टोरेज स्लॉट में एक एड्रेस (जैसे, 0x2712 या 0x2711) था, लेकिन घोस्ट ghostOwner में एक बिल्कुल अलग मान (जैसे, 0x401) था।

चूँकि घोस्ट कभी भी स्टोरेज के साथ अलाइन (aligned) नहीं था, इसलिए हमारे रूल ने दो अर्थहीन मानों की तुलना कर दी, और Prover ने बिल्कुल सही ढंग से विफलता (failure) की रिपोर्ट की।

हम देख सकते हैं कि मुख्य समस्या यह है कि घोस्ट वेरिएबल्स स्वचालित रूप से कॉन्ट्रैक्ट स्टोरेज को प्रतिबिंबित (mirror) नहीं करते हैं। इसे ठीक करने के लिए, हमें यह सुनिश्चित करने की आवश्यकता है कि किसी रूल में उपयोग किए जाने से पहले घोस्ट को हुक के माध्यम से स्पष्ट रूप से अपडेट किया जाए। व्यवहार में, इसका मतलब है कि कॉन्ट्रैक्ट को प्रासंगिक स्टोरेज स्लॉट को पढ़ने के लिए मजबूर करना ताकि Sload हुक ट्रिगर हो सके और घोस्ट को स्टोरेज में मौजूद वास्तविक मान के साथ सिंक्रोनाइज़ कर सके।

इसे प्राप्त करने के लिए, हम बस एक प्रारंभिक कॉल करते हैं जिसके कारण कॉन्ट्रैक्ट owner स्लॉट को पढ़ता है, जो बदले में Sload हुक को फायर करता है और हमारे घोस्ट को अपडेट करता है। हमारे मामले में, हम रूल की शुरुआत में resetCounter(e) को कॉल करके ऐसा करेंगे। चूँकि resetCounter(e) onlyOwner मॉडिफायर द्वारा सुरक्षित है, इसलिए EVM को मॉडिफायर की स्थिति जांचने के लिए ओनर स्टोरेज स्लॉट को पढ़ना ही होगा। यह रीड ऑपरेशन स्वचालित रूप से हुक को फायर करता है, यह सुनिश्चित करता है कि ghostOwner को हमारे द्वारा prevOwner में कैप्चर करने से पहले अपडेट कर दिया गया है।

नीचे अपडेटेड स्पेसिफिकेशन (updated specification) दिया गया है जो संशोधित रूल को पूरी तरह से दिखाता है:

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

// Updated rule: now includes an initial sync call
rule checkOwnerConsistency(env e) {

    // NEW: Force an SLOAD of `owner` so the hook fires and syncs `ghostOwner`
    resetCounter(e);
    
    /// Take the first snapshot after synchronization
    address prevOwner = ghostOwner;
    
    //parametric call
    method f;
    calldataarg args;
    f(e, args);

    // Take another snapshot after the call
    address currentOwner = ghostOwner;

    // The owner must not change across any call
    assert prevOwner == currentOwner;
}

रूल के अंदर पहली पंक्ति (resetCounter(e);) मुख्य जोड़ (addition) है।

घोस्ट के अब ठीक से सिंक्रोनाइज़ हो जाने के साथ, prevOwner और currentOwner के बीच की तुलना अर्थपूर्ण हो जाती है, जिससे Prover owner वेरिएबल की निरंतरता (consistency) को सही ढंग से सत्यापित कर पाता है।

आइए कदम दर कदम समझते हैं कि यहाँ क्या हुआ:

1. प्रारंभिक सिंक कॉल (resetCounter(e))
   • रूल resetCounter(e) को कॉल करके शुरू होता है।
   • onlyOwner मॉडिफायर को चेक करने के लिए, कॉन्ट्रैक्ट को owner स्लॉट (SLOAD) पढ़ना ही चाहिए।
   • वह रीड ऑपरेशन Sload हुक को फायर करता है, जो देखे गए मान को घोस्ट ghostOwner में लिखता है।
   • परिणामस्वरूप, ghostOwner अब हमारे द्वारा कोई स्नैपशॉट लेने से पहले वास्तविक स्टोरेज मान के साथ सिंक्रोनाइज़ हो गया है।
2. पहला स्नैपशॉट (prevOwner)
   • सिंक के ठीक बाद, रूल address prevOwner = ghostOwner; को निष्पादित करता है।
   • चरण 1 के कारण, prevOwner कॉन्ट्रैक्ट में स्टोर किया गया असली ओनर (real owner) है।
3. आर्बिट्रेरी कॉल (method f; calldataarg args; f(e, args);)
   • Prover अब सिम्बोलिक इनपुट्स के साथ एक आर्बिट्रेरी बाहरी कॉल (arbitrary external call) का अन्वेषण (explore) करता है।
   • इस कॉन्ट्रैक्ट में, इसका अर्थ है किसी भी (arbitrary) आर्गुमेंट्स के साथ increment(...) या resetCounter(...)।
   • दोनों फ़ंक्शन्स onlyOwner द्वारा सुरक्षित हैं और ओनर को राइट (write) नहीं करते हैं।
   • इस कॉल के दौरान, owner का कोई भी अतिरिक्त रीड (onlyOwner के कारण) Sload हुक को फिर से फायर करेगा, लेकिन यह घोस्ट में वही मान (same value) लिखेगा।
4. दूसरा स्नैपशॉट (currentOwner)
   • आर्बिट्रेरी कॉल के वापस आने (return) के बाद, रूल address currentOwner = ghostOwner; को निष्पादित करता है।
   • चूँकि कॉन्ट्रैक्ट कभी भी owner को नहीं बदलता (mutate) है, और हुक केवल रीड्स को प्रतिबिंबित (mirror) करता है, इसलिए currentOwner पहले कैप्चर किए गए उसी स्टोरेज-समर्थित मान के बराबर होता है।
5. कथन (Assertion)
   • रूल assert prevOwner == currentOwner; की जाँच करता है।
   • चूँकि डिप्लॉयमेंट के बाद कॉन्ट्रैक्ट कभी भी owner को संशोधित नहीं करता है, इसलिए ऐसा कोई कोड पाथ (code path) नहीं है जहाँ ये दो स्नैपशॉट्स भिन्न हो सकें।
   • इसलिए, सभी एक्सप्लोर किए गए निष्पादनों (executions) में, prevOwner और currentOwner हमेशा समान रहते हैं।
   • परिणामस्वरूप, Prover को कोई काउंटर-एग्जांपल (counterexample) नहीं मिलता है और रूल को वेरिफाइड (verified) के रूप में रिपोर्ट करता है।

ओनर प्रॉपर्टी के सत्यापित होने के साथ, आइए अब उस दूसरी प्रॉपर्टी की ओर मुड़ते हैं जिसे हमने पहले पहचाना था।

Counter Contract में Increment() Call को सत्यापित करना

दूसरी प्रॉपर्टी जिसे हम साबित करना चाहते हैं वह यह है कि increment() पर कॉल से count ठीक एक से बढ़ना चाहिए। क्योंकि count प्राइवेट है, केवल रूल्स count++ द्वारा किए गए वास्तविक स्टोरेज राइट को नहीं देख सकते हैं। इस प्रॉपर्टी को साबित करने के लिए, हम count स्लॉट में एक store hook संलग्न (attach) करते हैं, राइट से पहले और बाद के मानों को कैप्चर करते हैं, उन्हें घोस्ट्स में स्टोर (persist) करते हैं, और अंततः रूल में अंकगणितीय संबंध (arithmetic relation) का दावा करते हैं।

पूरा स्पेसिफिकेशन कुछ इस तरह दिखता है:

Copy
methods {
    function increment() external;
}


ghost mathint ghost_prevCount;

ghost mathint ghost_currentCount;

hook Sstore count uint256 postcallValue (uint256 precallValue) {
    ghost_prevCount = precallValue;
    ghost_currentCount = postcallValue;
}

rule checkCounter() {

    env e;

    //call to increment
    increment(e);

    assert ghost_currentCount == ghost_prevCount + 1; 
}

ऊपर दिए गए स्पेक में, हुक count स्टोरेज स्लॉट में अपडेट को देखता है जब भी increment() फ़ंक्शन को कॉल किया जाता है। पुराना मान (precallValue) एक घोस्ट वेरिएबल (ghost_prevCount) में स्टोर किया जाता है, जबकि नया मान (postcallValue) दूसरे (ghost_currentCount) में स्टोर किया जाता है। यह रूल को यह जाँचने की अनुमति देता है कि क्या काउंटर उम्मीद के मुताबिक, increment() फ़ंक्शन पर कॉल के बाद ठीक एक से बढ़ा है।

जब हम ऊपर दिए गए स्पेक पर Prover चलाते हैं, तो हम देखेंगे कि रूल सत्यापित (verified) हो गया है, जैसा कि नीचे दी गई छवि में दिखाया गया है:

आइए इसे कदम दर कदम समझते हैं कि यहाँ क्या होता है:

1. कॉल से पहले: कॉन्ट्रैक्ट के प्राइवेट वेरिएबल count का कुछ प्रारंभिक मान (मान लीजिए X) होता है।
2. increment() कॉल के दौरान:
   • EVM count++ स्टेटमेंट को निष्पादित करता है, जो count स्टोरेज स्लॉट पर एक रीड और उसके बाद एक राइट ऑपरेशन में अनुवादित (translate) होता है।
   • राइट ऑपरेशन होने से ठीक पहले, Sstore हुक ट्रिगर होता है।
   • हुक उस मान को कैप्चर करता है जो ओवरराइट होने वाला था (precallValue) और जो नया मान लिखा जा रहा है (postcallValue)।
   • इन्हें घोस्ट वेरिएबल्स ghost_prevCount और ghost_currentCount में स्टोर किया जाता है।
3. रूल चेक:
   • फ़ंक्शन कॉल पूरी होने के बाद, रूल दावा करता है कि ghost_currentCount == ghost_prevCount + 1।
   • यह देखते हुए कि ghost_currentCount = X + 1 और ghost_prevCount = X, यह कथन (assertion) सही साबित होता है।

इसलिए, हमें Prover से एक सत्यापित (verified) परिणाम मिला। दूसरे शब्दों में, increment() पर कोई भी कॉल काउंटर को ठीक एक से बढ़ा देती है, और Prover बिना कोई काउंटर-एग्जांपल पाए इस प्रॉपर्टी को औपचारिक रूप से सत्यापित करने में सक्षम था।

Storage के एक्सटेंशन (Extension) के रूप में Ghost Variables

हम देख सकते हैं कि कॉन्ट्रैक्ट के स्टोरेज पर विशिष्ट रीड या राइट ऑपरेशन्स का पता लगाकर डेटा का निरीक्षण करने और एकत्र करने के लिए हुक्स का उपयोग किया जाता है। हालाँकि, चूँकि हुक्स के अंदर घोषित वेरिएबल्स हुक के लिए स्थानीय (local) होते हैं, हुक के निष्पादन के समाप्त होते ही उनके मान गायब हो जाते हैं। पूरे स्पेसिफिकेशन में इस जानकारी को बनाए रखने और पुन: उपयोग करने के लिए, CVL ghost variables पेश करता है — पर्सिस्टेंट (persistent), स्पेसिफिकेशन-लेवल स्टोरेज जो कॉन्ट्रैक्ट की वास्तविक स्टेट को प्रतिबिंबित (mirror) या विस्तारित (extend) करता है। इस वजह से, घोस्ट वेरिएबल्स को कॉन्ट्रैक्ट के स्टोरेज के एक्सटेंशन के रूप में देखा और माना जा सकता है।

वास्तव में, Certora Prover घोस्ट वेरिएबल्स को नियमित स्टोरेज की तरह ही मानता है:

• स्टोरेज की तरह ही, यदि बाद में प्रगति पर चल रहा ट्रांज़ेक्शन रिवर्ट (revert) होता है, तो घोस्ट में किया गया कोई भी अपडेट स्वचालित रूप से रिवर्ट हो जाता है।
• वेरिफिकेशन रन की शुरुआत में, घोस्ट्स (अन्य CVL वेरिएबल्स की तरह) यादृच्छिक (havoced) मानों का प्रतिनिधित्व करते हैं जब तक कि उन्हें स्पष्ट रूप से स्पेसिफिकेशन में सेट नहीं किया जाता है, जो स्टोरेज के प्रति Prover के सिम्बोलिक दृष्टिकोण (symbolic view) को दर्शाता है।

हम बाद के अध्याय में इन व्यवहारों का अधिक विस्तार से पता लगाएंगे, जहाँ हम यह भी सीखेंगे कि अनपेक्षित हैवोकिंग (unintended havocing) से बचने और अधिक अनुमानित वेरिफिकेशन परिणामों को सुनिश्चित करने के लिए घोस्ट वेरिएबल्स को स्पष्ट रूप से कैसे इनिशियलाइज़ (initialize) किया जाए।

निष्कर्ष (Conclusion)

Certora हुक्स स्टोरेज और EVM ऑपरेशन्स में शक्तिशाली देखने की क्षमता (observability) प्रदान करते हैं। हालाँकि, उनके वेरिएबल्स प्रत्येक हुक के स्थानीय स्कोप तक सीमित होते हैं। घोस्ट वेरिएबल्स हुक्स से डेटा कैप्चर करके और इसे रूल्स के लिए सुलभ बनाकर इस समस्या को हल करते हैं, जिससे वेरिफिकेशन के दौरान कॉन्ट्रैक्ट की आंतरिक स्टेट के बारे में प्रभावी और व्यापक तर्क (reasoning) सक्षम होता है।

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