परिचय

“Introduction to Storage Hooks And Ghosts” अध्याय में, हमने साधारण स्टोरेज वेरिएबल्स के साथ स्टोरेज हुक्स (storage hooks) और घोस्ट्स (ghosts) को कवर किया था। हमने दिखाया कि हुक्स उन स्टोरेज वेरिएबल्स को ट्रैक करना संभव बनाते हैं जो सीधे public या external मेथड्स के माध्यम से सुलभ नहीं हैं। हमने यह भी प्रदर्शित किया कि जब कुछ मात्राओं को स्पष्ट रूप से स्टोर नहीं किया जाता है लेकिन specifications में तर्क (reasoning) के लिए आवश्यक होती है, तो उन मानों (values) की गणना करने और उन्हें बनाए रखने के लिए घोस्ट वेरिएबल्स के साथ हुक्स का उपयोग किया जा सकता है।

यदि ये वेरिएबल्स public या externally accessible होते, तो उनके मानों को सीधे CVL में invoke करके आसानी से पढ़ा जा सकता था, जिससे आवश्यकतानुसार किसी भी व्युत्पन्न मात्रा (derived quantities) की गणना की जा सकती।

हालाँकि, Mappings अलग होते हैं। वे गणनीय (enumerable) नहीं हैं — किसी मान (value) तक पहुँचने के लिए, किसी को पहले से ही key पता होनी चाहिए, और किसी mapping से “सभी keys” या “सभी values” प्राप्त करने का कोई built-in तरीका नहीं है।

यह सीमा वेरिफिकेशन के लिए एक बड़ी चुनौती पैदा करती है: कई महत्वपूर्ण कॉन्ट्रैक्ट प्रॉपर्टीज के लिए mapping की सभी एंट्रीज के आधार पर तर्क (reasoning) की आवश्यकता होती है। चूँकि हम सीधे सभी keys की गणना या निरीक्षण नहीं कर सकते हैं, इसलिए हमें mapping में होने वाले बदलावों को ट्रैक करने के लिए एक तंत्र (mechanism) की आवश्यकता है।

इस अध्याय में, हम Sstore हुक्स के उपयोग को integers, addresses, और booleans से आगे बढ़ाते हैं, और उन्हें storage mappings पर लागू करते हैं — specifications में यह एक सामान्य पैटर्न है, क्योंकि कई कॉन्ट्रैक्ट्स mappings पर बहुत अधिक निर्भर करते हैं।

Mappings के लिए Sstore Hook सिंटैक्स

कोड प्रदर्शन (code demonstrations) के साथ आगे बढ़ने से पहले, आइए पहले mappings के लिए Sstore हुक्स के कोड सिंटैक्स / पैटर्न सीखें।

Sstore hook — नए और पुराने values को कैप्चर करना

यहाँ एक storage mapping के नए और पुराने मानों (values) को कैप्चर करने के लिए Sstore हुक सिंटैक्स दिया गया है:

Copy
hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    // Implement hook logic for the balances mapping where:
		// - KEY is `user`
		// - old (previous) value is `oldVal`
		// - new (current) value is `newVal`
}

जब भी किसी mapping value में कुछ लिखा जाता है, तो पुराने और नए दोनों मानों को कैप्चर किया जा सकता है।

उदाहरण के लिए, यह वेरिफाई करने के लिए कि किसी उपयोगकर्ता का बैलेंस 10 से अधिक नहीं बढ़ता है, हम पुराने और नए बैलेंस के बीच के अंतर (difference) की गणना करते हैं और परिणाम को घोस्ट वेरिएबल g_balanceDelta में असाइन करते हैं:

Copy
ghost mathint g_balanceDelta;


hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    g_balanceDelta = newVal - oldVal;
}

हुक डेल्टा (newVal - oldVal) की गणना करता है और इसे घोस्ट वेरिएबल g_balanceDelta में स्टोर करता है, जो यह दर्शाता है कि उस स्टोरेज अपडेट के दौरान उपयोगकर्ता का बैलेंस कितना बदलता है।

इसके बाद बदलाव की सीमाओं को वेरिफाई करने के लिए g_balanceDelta वैल्यू का उपयोग किया जा सकता है। उदाहरण के लिए:

Copy
rule deltaNotMoreThan10() {
    ...
    assert g_balanceDelta <= 10;
}

Sstore hook — केवल नई value कैप्चर करना

हम केवल नए मान को कैप्चर करना चुन सकते हैं और पुराने मान को छोड़ सकते हैं, क्योंकि बाद वाला वैकल्पिक (optional) है:

Copy
hook Sstore balances[KEY address user] uint256 newVal {
	// implement hook logic
}

इसका उपयोग अधिकतर तब किया जाता है जब स्टोरेज को केवल सेट किया जा रहा हो और वेरिफिकेशन लॉजिक में डेल्टा (बदलाव) की आवश्यकता नहीं होती है।

उदाहरण के लिए, यदि हम यह तर्क देना चाहते हैं कि किसी उपयोगकर्ता का बैलेंस 2000 से अधिक नहीं होना चाहिए, तो हमें केवल newVal को कैप्चर करना होगा और इसे एक घोस्ट वेरिएबल में असाइन करना होगा:

Copy
ghost mathint g_balance;


hook Sstore balances[KEY address user] uint256 newVal {
	g_balance = newVal;
}

इसके बाद g_balance मान का उपयोग यह वेरिफाई करने के लिए किया जा सकता है कि बैलेंस निर्धारित सीमाओं के भीतर रहता है या नहीं। उदाहरण के लिए:

Copy
rule balanceDoesNotExceed2000() {
	...
	assert g_balance <= 2000;
}

Sstore hook के बिना mapping में सभी keys और values को ट्रैक करना असंभव है

यह समझने के लिए कि mappings से जुड़ी प्रॉपर्टीज को वेरिफाई करने के लिए हुक्स क्यों आवश्यक हैं, आइए एक साधारण कॉन्ट्रैक्ट, PointSystem, से शुरुआत करें, जो निम्नलिखित कार्य करता है:

• किसी विशिष्ट उपयोगकर्ता में पॉइंट्स जोड़ता है और कुल पॉइंट्स (total points) बढ़ाता है।
• pointsOf[address] mapping में प्रति-उपयोगकर्ता रिकॉर्ड रखता है।
• वेरिएबल totalPoints में समग्र कुल (overall total) को ट्रैक करता है।

Copy
contract PointSystem {
    mapping (address => uint256) public pointsOf;
    uint256 public totalPoints;

    function addPoints(address _user, uint256 _amount) external {
        pointsOf[_user] += _amount;
        totalPoints += _amount;
    }
}

अब, आइए इस प्रॉपर्टी को वेरिफाई करें: “व्यक्तिगत उपयोगकर्ता पॉइंट्स का योग कुल पॉइंट्स के बराबर होता है।”

Sstore हुक का उपयोग किए बिना, एक दृष्टिकोण सीमित संख्या में उपयोगकर्ताओं (उदाहरण के लिए, दो) के साथ काम करना है। हम सीधे mapping pointsOf से उनके बैलेंस पढ़ते हैं, उनके पॉइंट्स जोड़ते हैं, और यह assert करते हैं कि यह योग totalPoints के बराबर है।

नीचे दिया गया नियम इस दृष्टिकोण को प्रदर्शित करता है, जिसमें totalPoints और सभी pointsOf मान शून्य से शुरू होते हैं:

Copy
rule sumOfUserPointsEqualsTotalPoints() {
    address account1; address account2; 
    uint256 amount1; uint256 amount2;   

    require account1 != account2;
    require pointsOf(account1) == 0 && pointsOf(account2) == 0; // points per user starts at zero
    require totalPoints() == 0; // total starts at zero

    addPoints(account1, amount1);
    addPoints(account2, amount2);

    assert to_mathint(totalPoints()) == pointsOf(account1) + pointsOf(account2);
}

इस Prover रन में, हम देखते हैं कि प्रॉपर्टी वेरिफाई हो गई है:

Prover रन: link

केवल दो उपयोगकर्ताओं का उपयोग करके समानता (equality) assert करने से (भले ही अतिरिक्त अकाउंट वेरिएबल्स घोषित करके मैन्युअल रूप से अधिक जोड़े गए हों), यह प्रॉपर्टी अकाउंट्स के उस सबसेट (subset) तक सीमित हो जाती है। यह वह सटीक प्रॉपर्टी नहीं है जिसे हम वेरिफाई करना चाहते हैं, क्योंकि mapping में कई अन्य उपयोगकर्ता मौजूद हो सकते हैं जिनके पॉइंट्स इस जाँच से बाहर रह गए हैं।

अब, आइए नियम में सुधार करें। require pointsOf(account1) == 0 && pointsOf(account2) == 0 और require totalPoints() == 0 preconditions को हटाकर totalPoints और उपयोगकर्ता पॉइंट्स (pointsOf[address]) को शून्य के बजाय किसी भी मान से शुरू होने दें।

फिर हम addPoints() मेथड कॉल से पहले और बाद में totalPoints और pointsOf[address] के मान रिकॉर्ड करते हैं। ऐसा करने से हमें कॉल के कारण होने वाले डेल्टा की गणना करने और यह निर्धारित करने की अनुमति मिलती है कि प्रत्येक वेरिएबल कितना बदल गया है।

अंत में, हम assert करते हैं कि कुल पॉइंट्स (totalPointsAfter) प्रारंभिक कुल पॉइंट्स (totalPointsBefore) और account1 तथा account2 के पॉइंट्स में हुए परिवर्तनों के योग के बराबर हैं। यह समायोजन (adjustment) प्रारंभिक स्थिति (initial state) की परवाह किए बिना नियम को काम करने योग्य बनाता है:

Copy
rule sumOfUserPointsEqualsTotalPoints_modified() {
    address account1; address account2;
    uint256 amount1; uint256 amount2;

    require account1 != account2;

    // Capture the state BEFORE the method call
    mathint totalPointsBefore = totalPoints();
    mathint pointsOfAccount1Before = pointsOf(account1);
    mathint pointsOfAccount2Before = pointsOf(account2);

    // Method call
    addPoints(account1, amount1);
    addPoints(account2, amount2);

    // Capture the state AFTER the method call
    mathint totalPointsAfter = totalPoints();
    mathint pointsOfAccount1After = pointsOf(account1);
    mathint pointsOfAccount2After = pointsOf(account2);

    // Calculate how much each account's points changed
    mathint deltaPointsOfAccount1 = pointsOfAccount1After - pointsOfAccount1Before;
    mathint deltaPointsOfAccount2 = pointsOfAccount2After - pointsOfAccount2Before;

    // Assertion: The total points equal the initial total plus the changes in the points of account1 and account2
    assert totalPointsAfter == totalPointsBefore + deltaPointsOfAccount1 + deltaPointsOfAccount2;
}

Prover रन: link

इस नियम सुधार के बाद भी, यह प्रॉपर्टी का सटीक प्रतिनिधित्व नहीं करता है, क्योंकि यह केवल दो विशिष्ट उपयोगकर्ताओं पर विचार करता है और mapping में अन्य सभी को अनदेखा करता है। यह केवल यह सिद्ध करता है कि उपयोगकर्ताओं का एक सबसेट कुल (total) के अनुरूप है।

Sstore हुक के बिना सभी उपयोगकर्ता पॉइंट्स को ट्रैक करना असंभव है, भले ही mapping externally accessible हो।

Storage mapping values की गणना (enumerate) करने के लिए Sstore hook का उपयोग करना

हर बार जब कॉन्ट्रैक्ट pointsOf[address] में लिखता है, तो Sstore हुक नए मान और पुराने मान को कैप्चर करता है, जो इसे डेल्टा (परिवर्तन) की गणना करने और इसे एक घोस्ट वेरिएबल में असाइन करने की अनुमति देता है। सभी संभावित keys के लिए सीधे mapping (कॉन्ट्रैक्ट से) को क्वेरी करने के बजाय, हम एक घोस्ट वेरिएबल ट्रैकर बनाए रखते हैं जो हर स्टोरेज राइट (storage write) को उसी समय रिकॉर्ड करता है।

आइए Sstore हुक लॉजिक को लागू करें। जैसा कि बताया गया है, हम पुराने और नए मानों को कैप्चर करते हैं, डेल्टा (परिवर्तन) की गणना करते हैं और कुल पॉइंट्स रिकॉर्ड करने के लिए इसे एक घोस्ट वेरिएबल में जोड़ते हैं। हम इस घोस्ट वेरिएबल को g_sumOfUserPoints के रूप में घोषित करते हैं:

Copy
ghost mathint g_sumOfUserPoints;

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}

अब जब व्यक्तिगत उपयोगकर्ता पॉइंट्स का योग घोस्ट वेरिएबल g_sumOfUserPoints में मात्रात्मक (quantifiable) है, तो अगला कदम इसे किसी नियम या invariant में उपयोग करके यह जाँचना है कि यह ट्रैकर हमेशा कॉन्ट्रैक्ट के स्टोरेज वेरिएबल totalPoints के बराबर है या नहीं।

Rules और invariants के भीतर Ghosts

घोस्ट्स का उपयोग rules और invariants दोनों में किया जा सकता है। निम्नलिखित उदाहरण में, हम वेरिफाई करते हैं कि totalPoints (स्टोरेज वेरिएबल) g_sumOfUserPoints (घोस्ट वेरिएबल) के बराबर है, जिसका मान Sstore हुक में ट्रैक और कैलकुलेट किया जाता है।

Verify करें कि rule के रूप में totalPoints() g_sumOfUserPoints के बराबर है

यहाँ नियम पैरामेट्रिक रूप (parametric form) में है, जहाँ f(e, args) Prover को सभी कॉन्ट्रैक्ट फंक्शन्स के विरुद्ध मनमाने (arbitrary) तर्कों के साथ नियम को वेरिफाई करने की अनुमति देता है। नीचे दिए गए नियम के लिए, हमें यह आवश्यक है कि totalPoints और g_sumOfUserPoints शून्य से शुरू हों:

Copy
rule sumOfUserPointsEqualsTotalPoints(env e, method f, calldataarg args) {
    require totalPoints() == 0 && g_sumOfUserPoints == 0;

    f(e, args);
    assert totalPoints() == g_sumOfUserPoints;
}

Prover रन: link

विकल्प के रूप में, हम totalPoints और g_sumOfUserPoints को किसी भी मान से शुरू करने की अनुमति दे सकते हैं, बशर्ते कि वे समान मान से शुरू हों:

Copy
rule sumOfUserPointsEqualsTotalPoints_alt(env e, method f, calldataarg args) {
    require totalPoints() == g_sumOfUserPoints; // starts at any value, as long as they start at the same value
																						    
    f(e, args);
    assert totalPoints() == g_sumOfUserPoints;
}

Prover रन (verified): link

Verify करें कि invariant के रूप में totalPoints() g_sumOfUserPoints के बराबर है

इसी प्रॉपर्टी को आगमनात्मक रूप से (inductively - base case और induction step) वेरिफाई करने के लिए, हम इसे CVL invariant के रूप में लिखते हैं। घोस्ट को शून्य पर इनिशियलाइज़ किया गया है, और पिछले नियम से वही Sstore हुक यहाँ लागू किया गया है:

Copy
ghost mathint g_sumOfUserPoints {
    init_state axiom g_sumOfUserPoints == 0;
}

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}

invariant sumOfUserPointsEqualsTotalPoints_inv() 
    totalPoints() == g_sumOfUserPoints;

Prover रन (verified): link

CVL invariant में घोस्ट्स का उपयोग करते समय, उन्हें init_state axiom के साथ इनिशियलाइज़ करना आवश्यक है जो सही प्रारंभिक मान (starting value) सेट करता है — इस मामले में, g_sumOfUserPoints के लिए शून्य।

चूँकि प्रत्येक उपयोगकर्ता के पॉइंट्स शून्य से शुरू होते हैं, इसलिए सभी उपयोगकर्ता पॉइंट्स का योग (g_sumOfUserPoints) भी शून्य से शुरू होता है। यह मायने रखता है क्योंकि, इंडक्शन प्रक्रिया के हिस्से के रूप में, एक invariant यह जाँचता है कि क्या प्रॉपर्टी base case (constructor के तुरंत बाद) में मान्य है।

जब हमने पहले इस प्रॉपर्टी को एक rule के रूप में वेरिफाई किया था, तो हमने उस मामले का परीक्षण किया जहाँ दोनों शून्य से शुरू हुए और फिर गैर-शून्य (non-zero, लेकिन समान) मान पर। एक invariant के रूप में, हम केवल दोनों का शून्य से शुरू होने वाला परीक्षण करते हैं।

इसका कारण यह है कि invariants को कंस्ट्रक्टर के तुरंत बाद (base case) परीक्षण शुरू करना चाहिए, जहाँ uninitialized स्टोरेज वेरिएबल्स डिफ़ॉल्ट रूप से शून्य होते हैं। इसका मतलब है कि invariants केवल गैर-शून्य मानों से तभी शुरू हो सकते हैं जब कंस्ट्रक्टर स्पष्ट रूप से (explicitly) उन मानों को सेट करता है। हालाँकि, Rules किसी भी मनमानी (arbitrary) प्रारंभिक अवस्था को मान सकते हैं — यह शून्य या गैर-शून्य हो सकता है।

सारांश

• मान बदलने वाली प्रॉपर्टीज को सिद्ध करते समय mappings के लिए Sstore हुक का उपयोग अपरिहार्य (unavoidable) है। यह स्टोरेज स्लॉट्स की निगरानी करके और mapping keys के लिए पुराने और नए मानों को कैप्चर करके गणना (enumeration) की समस्या को हल करता है।
• Sstore हुक के बिना, स्टोरेज की सीधे निगरानी करने के बजाय प्रॉपर्टीज को केवल मैन्युअल रूप से क्वेरी की गई keys के एक सीमित सेट के लिए सिद्ध किया जा सकता है।
• rules में, घोस्ट वेरिएबल्स के प्रारंभिक मान require स्टेटमेंट्स का उपयोग करके प्रतिबंधित (constrained) किए जाते हैं।
• invariants में, घोस्ट वेरिएबल्स को init_state axiom का उपयोग करके इनिशियलाइज़ किया जाता है।

यह लेख formal verification using the Certora Prover पर एक श्रृंखला का हिस्सा है