पिछले अध्याय में, हमने देखा कि कैसे unconstrained ghost variables के कारण false positives आ सकते हैं। हमने यह भी सीखा कि नियमों (rules) के भीतर ghost values को प्रभावी ढंग से constrain करने के लिए require स्टेटमेंट का उपयोग कैसे किया जा सकता है।

हालाँकि, जबकि require rules के लिए अच्छी तरह काम करता है, इस दृष्टिकोण का उपयोग invariant verification के लिए नहीं किया जा सकता है। इस अध्याय में, हम जानेंगे कि require स्टेटमेंट invariants के साथ असंगत (incompatible) क्यों है, और invariants में ghost variables के मानों (values) को सुरक्षित रूप से constrain करने की उचित तकनीक के रूप में axioms को पेश करेंगे।

समस्या को समझना

यह समझने के लिए कि एक unconstrained ghost variable invariant verification को कैसे प्रभावित कर सकता है, नीचे दिए गए Voting कॉन्ट्रैक्ट पर विचार करें। यह कॉन्ट्रैक्ट उपयोगकर्ताओं को inFavor() या against() फ़ंक्शंस का उपयोग करके किसी प्रस्ताव के पक्ष में (in favor) या विरोध में (against) वोट करने की अनुमति देता है।

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;

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

    // keep the count of votes against
    uint256 public votesAgainst; 


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

        votesInFavor += 1;
    }

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

        votesAgainst += 1;
  }
}

यह कॉन्ट्रैक्ट तीन पब्लिक स्टेट वेरिएबल्स मेंटेन करता है:

• hasVoted यह ट्रैक करता है कि किसी दिए गए उपयोगकर्ता ने पहले ही वोट कर दिया है या नहीं।
• votesInFavor और votesAgainst क्रमशः पक्ष और विपक्ष में पड़े वोटों की संख्या का ट्रैक रखते हैं।

अब नीचे दिए गए स्पेसिफिकेशन (specification) पर विचार करें, जो एक invariant totalVotesSum को परिभाषित करता है और एक ghost variable totalVotes को पेश करता है जो डाले गए वोटों की कुल संख्या को ट्रैक करता है — एक ऐसी वैल्यू जिसे कॉन्ट्रैक्ट स्वयं रिकॉर्ड नहीं करता है।

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

ghost mathint totalVotes;


hook Sstore hasVoted[KEY address voter] bool newStatus(bool oldStatus) {
    totalVotes = totalVotes + 1;
}

invariant totalVotesSum()
    totalVotes == votesInFavor() + votesAgainst();

ऊपर दिए गए spec का विस्तृत स्पष्टीकरण यहाँ दिया गया है:

• methods block दो पब्लिक व्यू फ़ंक्शंस, votesInFavor() और votesAgainst() को डिक्लेयर करता है, जिन्हें हम invariant में रेफ़र करना चाहते हैं। उन्हें envfree के रूप में मार्क किया गया है क्योंकि उनका निष्पादन (execution) msg.sender, msg.value, आदि जैसे environment variables पर निर्भर नहीं करता है।
• ghost variable totalVotes को उन उपयोगकर्ताओं की संख्या गिनने के लिए परिभाषित किया गया है जिन्होंने वोट किया है। चूँकि कॉन्ट्रैक्ट इस वैल्यू को सीधे तौर पर उजागर (expose) नहीं करता है, इसलिए हम एक ghost का उपयोग करके इसे सिमुलेट करते हैं।
• hook को hasVoted मैपिंग के Sstore ऑपरेशन के साथ जोड़ा गया है। यह hook हर बार तब ट्रिगर होता है जब hasVoted मैपिंग में कोई वैल्यू अपडेट होती है, जो केवल तभी होता है जब कोई उपयोगकर्ता वोट डालता है। hook में, हम totalVotes को 1 से बढ़ाते हैं—प्रभावी रूप से हर नए मतदाता को गिनते हैं, भले ही उन्होंने पक्ष में वोट दिया हो या विपक्ष में।
• invariant totalVotesSum यह दावा (assert) करता है कि ghost (totalVotes) द्वारा ट्रैक किए गए वोटों की संख्या हमेशा कॉन्ट्रैक्ट से प्राप्त वोटों के वास्तविक योग (votesInFavor + votesAgainst) से मेल खानी चाहिए।

एक बार जब आप उपरोक्त spec को अपनी प्रोजेक्ट डायरेक्टरी में रख लेते हैं, तो certoraRun कमांड का उपयोग करके verification प्रक्रिया चलाएँ। इसके बाद, परिणाम देखने के लिए अपने टर्मिनल में दिखाए गए verification रिज़ल्ट लिंक को खोलें, जो नीचे दी गई छवि के समान दिखना चाहिए।

हम देख सकते हैं कि Prover हमारे invariant को verify करने में विफल रहा है। आइए जानें कि ऐसा क्यों हुआ और हम इसे कैसे ठीक कर सकते हैं।

Violation के कारण को समझना

एक invariant चेक में दो चरण शामिल होते हैं: base case (कंस्ट्रक्टर के बाद प्रारंभिक अवस्था की जाँच करना) और inductive step (सभी बाद के state transitions की जाँच करना)।

हमारी स्थिति में, Prover base case पर विफल हो जाता है, जिसका अर्थ है कि यह पुष्टि नहीं कर सकता कि invariant कॉन्ट्रैक्ट की प्रारंभिक अवस्था (initial state) से ही मान्य है।

हमारा invariant base case पर विफल हो जाता है क्योंकि किसी भी invariant को verify करते समय, Prover को कॉन्ट्रैक्ट की प्रारंभिक अवस्था में invariant की जाँच करनी होती है। हालाँकि, चूँकि हमने totalVotes के लिए कभी कोई प्रारंभिक वैल्यू (initial value) निर्दिष्ट नहीं की, इसलिए Prover ने प्रतिकूल (adversarially) रूप से हमारे लिए एक चुन ली। कॉल ट्रेस में, हम देख सकते हैं कि इसने -2 को चुना।

इसके कारण invariant totalVotes == votesInFavor() + votesAgainst() तुरंत विफल हो जाता है, क्योंकि Prover जाँचता है कि क्या -2 == 0 + 0 है, जो कि गलत (false) है। इसे ठीक करने के लिए, हमें ghost की प्रारंभिक वैल्यू को 0 पर सेट करना होगा। हालाँकि, rules के विपरीत, हम ghost की प्रारंभिक वैल्यू को constrain करने के लिए require स्टेटमेंट का उपयोग नहीं कर सकते हैं। इसका मतलब यह नहीं है कि invariants में require का कोई स्थान नहीं है। इसका उपयोग एक preserved ब्लॉक के अंदर किया जा सकता है।

CVL में preserved ब्लॉक एक विशेष कंस्ट्रक्ट है जो आपको एक invariant verify करते समय अतिरिक्त मान्यताएँ (extra assumptions) जोड़ने की अनुमति देता है। हम एक अलग अध्याय में preserved ब्लॉक्स के बारे में अधिक जानेंगे।

इससे पहले कि हम जानें कि invariants के भीतर ghost variables को कैसे constrain किया जाए, आइए पहले यह समझें कि इस संदर्भ में require का उपयोग क्यों नहीं किया जा सकता है।

हम require स्टेटमेंट का उपयोग क्यों नहीं कर सकते?

CVL में, एक require स्टेटमेंट का उपयोग एक rule के भीतर एक precondition के रूप में कार्य करने के लिए किया जाता है। यह Prover को बताता है, “केवल उन परिदृश्यों के लिए निम्नलिखित assertions की जाँच करें जहाँ ये विशिष्ट शर्तें लागू होती हैं।” यह उन execution paths या input combinations को फ़िल्टर करने में मदद करता है जिन्हें Prover rule का मूल्यांकन करते समय एक्सप्लोर करता है।

हालाँकि, एक invariant बहुत अलग है। एक invariant कॉन्ट्रैक्ट की प्रारंभिक अवस्था सहित हर संभव अवस्था (every possible state) में लागू होना चाहिए, बिना किसी precondition पर निर्भर हुए। दूसरे शब्दों में, invariants सिस्टम के बारे में unconditional truths (बिना शर्त सच्चाइयों) को व्यक्त करते हैं।

एक invariant के अंदर require स्टेटमेंट का उपयोग करने का कोई मतलब नहीं है, क्योंकि require केवल rule execution के दौरान रास्तों (paths) को सीमित करता है — यह यह परिभाषित नहीं करता है कि verification शुरू होने से पहले क्या सच है। इसके बजाय हमें Prover के लिए initial state assumptions स्थापित करने के एक तरीके की आवश्यकता है।

इस तरह के प्रारंभिक सत्यों (initial truths) को स्थापित करने के लिए — जैसे कि ghost variable की शुरुआती वैल्यू सेट करना — हमें एक अलग कंस्ट्रक्ट की आवश्यकता होती है: axioms।

“Axioms” का परिचय

चूँकि invariants preconditions पर निर्भर नहीं हो सकते हैं, इसलिए हमें यह परिभाषित करने के लिए एक तरीके की आवश्यकता है कि verification शुरू होने से पहले Prover को सिस्टम के बारे में क्या मानना (assume) चाहिए। यहीं पर axioms काम आते हैं।

CVL में, एक axiom हमें एक ऐसे तथ्य या संबंध को घोषित करने की अनुमति देता है जिसे Prover को हमेशा सत्य मानना चाहिए। require की तरह state space को फ़िल्टर करने के बजाय, एक axiom अपने तार्किक ब्रह्मांड (logical universe) में मौजूद सच्चाइयों को निर्दिष्ट करके Prover की तर्क क्षमता (reasoning) को आकार (shapes) देता है।

सरल शब्दों में:

• एक require स्टेटमेंट यह सीमित करता है कि Prover क्या जाँचता है (यह states को फ़िल्टर करता है)।
• एक axiom यह परिभाषित करता है कि Prover क्या मानता है (यह सच्चाइयों को स्थापित करता है)।

Axioms का उपयोग करके, हम ठीक से नियंत्रित कर सकते हैं कि invariant verification के दौरान ghost variables कैसा व्यवहार करते हैं। उदाहरण के लिए, हम Prover को यह मानने का निर्देश दे सकते हैं कि एक ghost variable कंस्ट्रक्टर से पहले एक निश्चित वैल्यू से शुरू होता है, या कि यह हमेशा सभी states में दी गई शर्त को पूरा करता है।

CVL में ghost variables के लिए उपयोग किए जाने वाले दो प्राथमिक प्रकार के axioms हैं:

1. Initial State Axioms
2. Global Axioms

“Initial State Axioms” क्या हैं

एक initial state axiom एक ऐसी प्रॉपर्टी को परिभाषित करता है जिसे prover को invariant चेकिंग के base step में या कॉन्ट्रैक्ट के कंस्ट्रक्टर के निष्पादित होने से ठीक पहले सत्य मानना चाहिए।

दूसरे शब्दों में, यह Prover को बताता है, “मान लें कि यह स्थिति तब सत्य है जब कॉन्ट्रैक्ट पहली बार डिप्लॉय किया जाता है।” यह आपको ghost variables की प्रारंभिक वैल्यूज़ को नियंत्रित करने और उन मनमानी शुरुआती अवस्थाओं (arbitrary starting states) को खत्म करने की अनुमति देता है जो अन्यथा invariant failures का कारण बन सकती हैं।

Initial state axiom को init_state कीवर्ड का उपयोग करके घोषित किया जाता है, जिसके बाद axiom कीवर्ड आता है, और फिर वह शर्त आती है जो ghost variable की प्रारंभिक अवस्था को परिभाषित करती है, जैसा कि नीचे दिखाया गया है:

Copy
ghost type_of_ghost name_of_ghost {
    init_state axiom boolean_expression;
}

उदाहरण के लिए, नीचे दिया गया कोड mathint प्रकार के एक ghost variable sum_of_balances को परिभाषित करता है और निर्दिष्ट करता है कि कॉन्ट्रैक्ट का कंस्ट्रक्टर रन होने से पहले इसकी वैल्यू 0 होनी चाहिए।

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

यह सुनिश्चित करेगा कि Prover इस धारणा के साथ verification शुरू करता है कि sum_of_balances शून्य से शुरू होता है, जिससे इसे प्रारंभिक अवस्था में एक मनमानी वैल्यू (arbitrary value) के रूप में माने जाने से रोका जा सके।

“Global Axioms” क्या हैं

जबकि initial state axioms केवल कॉन्ट्रैक्ट की पहली अवस्था (first state) पर लागू होते हैं, global axioms उन गुणों को परिभाषित करते हैं जिन्हें पूरे verification के दौरान हर अवस्था (every state) में लागू होना चाहिए।

एक global axiom आपको ghost variables के बारे में सार्वभौमिक सत्य (universal truths) व्यक्त करने की अनुमति देता है — ऐसी शर्तें जो सभी संभावित कॉन्ट्रैक्ट निष्पादनों में सुसंगत (consistent) रहती हैं। एक बार परिभाषित होने के बाद, Prover इन कथनों को ऐसे तथ्यों के रूप में स्वीकार करता है जो हमेशा मान्य होते हैं और जिन्हें कभी भी फिर से साबित करने की आवश्यकता नहीं होती है।

एक global ghost axiom को ghost variable डिक्लेरेशन ब्लॉक के अंदर axiom कीवर्ड शामिल करके परिभाषित किया जाता है, जिसके बाद एक ऐसी शर्त आती है जिसे सभी प्रोग्राम states में लागू होना चाहिए, जैसा कि नीचे दिखाया गया है:

Copy
ghost type_of_ghost name_of_ghost {    
  axiom boolean_expression;
}

उदाहरण के लिए, नीचे दिया गया कोड mathint प्रकार के एक ghost variable x को परिभाषित करता है और यह दावा (assert) करता है कि verification प्रक्रिया के दौरान हर state में इसकी वैल्यू हमेशा शून्य से अधिक होती है:

Copy
ghost mathint x {    
  axiom x > 0;
}

इसका मतलब है कि verification के दौरान, Prover यह मान लेगा कि शर्त $x > 0$ सभी states में लागू होती है, जो प्रभावी रूप से ghost variable को कभी भी शून्य या नकारात्मक (negative) वैल्यूज़ न लेने के लिए constrain करता है।

हमारे Spec में init_state Axiom का उपयोग करना

अब जब हम एक init_state axiom का उद्देश्य समझ गए हैं, तो आइए इसे उस उदाहरण पर लागू करें जिसे हमने पहले देखा था, जहाँ हमारा invariant विफल हो गया था क्योंकि ghost variable totalVotes एक मनमानी वैल्यू के साथ शुरू हुआ था।

इसे ठीक करने के लिए, हमें Prover को यह बताना होगा कि कंस्ट्रक्टर रन होने से ठीक पहले totalVotes 0 से शुरू होना चाहिए। हम ghost डिक्लेरेशन को अपडेट करके उसमें एक init_state axiom शामिल करके ऐसा करते हैं, जैसा कि नीचे दिखाया गया है:

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

एक बार जब आप ऊपर दिखाए गए अनुसार init_state axiom को शामिल करने के लिए spec को अपडेट कर लेते हैं, तो Prover को फिर से चलाएँ और verification रिज़ल्ट खोलें। हमारा नया verification रिज़ल्ट नीचे दिए गए परिणाम के समान दिखना चाहिए।

इस बार, हम देख सकते हैं कि Prover ने base case और inductive step दोनों को पास करके हमारे invariant को सफलतापूर्वक verify कर दिया है, यह पुष्टि करते हुए कि वोटों की कुल संख्या हमेशा पक्ष में डाले गए वोटों और विपक्ष में डाले गए वोटों के योग के बराबर होती है।

व्यवहार में Global Axiom का उपयोग करना

यह समझने के लिए कि global axioms व्यवहार में कैसे काम करते हैं, नीचे दिए गए स्पेसिफिकेशन (specification) पर विचार करें:

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

ghost mathint totalVotes {
    axiom totalVotes >= 0;
}

hook Sstore hasVoted[KEY address voter] bool newStatus(bool oldStatus) {
    totalVotes = totalVotes + 1;
}

invariant totalVotesShouldAlwaysGtInFavorVotes()
    totalVotes >= votesInFavor();

उपरोक्त स्पेसिफिकेशन यह दावा करता है कि वोटों की कुल संख्या (totalVotes) हमेशा पक्ष में पड़े वोटों (votesInFavor) की संख्या से अधिक या उसके बराबर होनी चाहिए। उपरोक्त spec में, मुख्य भाग axiom totalVotes >= 0 लाइन है, जो एक global axiom पेश करती है जो Prover को हमेशा यह मानने का निर्देश देती है कि totalVotes हर प्रोग्राम state में गैर-नकारात्मक (non-negative) है। इसका अर्थ है कि Prover कभी भी ऐसे किसी execution path को एक्सप्लोर नहीं करेगा जहाँ totalVotes नकारात्मक हो जाए।

जब आप इस spec को Prover को सबमिट करते हैं, तो यह सफलतापूर्वक invariant को verify कर देता है, जैसा कि नीचे दिए गए रिज़ल्ट में दिखाया गया है:

जैसा कि हम जानते हैं, जब verification के लिए कोई invariant सबमिट किया जाता है, तो Prover इसकी शुद्धता (correctness) सुनिश्चित करने के लिए दो आवश्यक जाँच (checks) करता है:

1. Base Case: इस चरण में, Prover पहले यह जाँचता है कि क्या invariant कॉन्ट्रैक्ट के कंस्ट्रक्टर के निष्पादित होने के तुरंत बाद लागू होता है। हमारे उदाहरण में, इसका मतलब यह जाँचना है कि क्या कॉन्ट्रैक्ट की प्रारंभिक अवस्था में totalVotes >= votesInFavor() सत्य है। डिप्लॉयमेंट के तुरंत बाद, votesInFavor() 0 होता है, जबकि Prover यह मानता है कि totalVotes कोई भी गैर-नकारात्मक (non-negative) वैल्यू हो सकती है। चूँकि कोई भी गैर-नकारात्मक संख्या totalVotes >= votesInFavor() शर्त को पूरा करती है, इसलिए base case लागू हो जाता है।
2. Inductive Step: आगे, Prover यह सुनिश्चित करता है कि यदि invariant किसी भी फ़ंक्शन के निष्पादन से पहले लागू होता है, तो यह बाद में सभी संभावित transitions के लिए भी लागू होता रहे। यहाँ, हर बार जब कोई उपयोगकर्ता वोट डालता है, तो hasVoted मैपिंग अपडेट हो जाती है और hook totalVotes को बढ़ा (increment) देता है।
   • जब कोई उपयोगकर्ता पक्ष में (in favor) वोट करता है, तो votesInFavor और totalVotes दोनों एक-एक बढ़ जाते हैं, जिससे असमानता (inequality) सुरक्षित रहती है।
   • जब कोई उपयोगकर्ता विरोध में (against) वोट करता है, तो केवल totalVotes बढ़ता है, जो अभी भी invariant को बनाए रखता है।

क्योंकि दोनों शर्तें लागू होती हैं, Prover सफलतापूर्वक invariant को verify कर देता है। यह पुष्टि करता है कि global assumption totalVotes >= 0 के तहत, totalVotes और votesInFavor के बीच का संबंध सभी संभावित कॉन्ट्रैक्ट states में मान्य रहता है।

इस तरह एक global axiom Prover को उन गुणों (properties) के बारे में तर्क (reason) करने में मदद करता है जो हर प्रोग्राम state में सार्वभौमिक रूप से सत्य (universally true) हैं। axiom totalVotes >= 0 को परिभाषित करके, हम एक तार्किक तथ्य (logical fact) स्थापित करते हैं जो पूरे verification के दौरान लागू रहता है, बिना हर state transition के बाद इसे फिर से साबित करने की आवश्यकता के। इस मामले में, axiom इस सहज सत्य (intuitive truth) को पकड़ता है कि वोटों की कुल संख्या कभी भी नकारात्मक नहीं हो सकती है, और Prover को कुशलतापूर्वक और ठोस रूप से (soundly) invariant को verify करने की अनुमति देता है।

निष्कर्ष

इस अध्याय में, हमने प्रदर्शित किया कि कैसे unconstrained ghost variables के कारण invariant proofs base case पर विफल हो सकते हैं। चूँकि invariants के भीतर इनिशियलाइज़ेशन (initialization) के लिए require का उपयोग करना मान्य नहीं है, इसलिए हमने सही विकल्प के रूप में axioms को पेश किया। विशेष रूप से, init_state axiom ghosts के लिए मान्य शुरुआती वैल्यूज़ को परिभाषित करके इनिशियलाइज़ेशन समस्या का समाधान करता है, जबकि global axioms उन गुणों को व्यक्त करते हैं जो सभी कॉन्ट्रैक्ट states में सत्य रहते हैं।

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