CVL में, mathint टाइप unbounded integers को दर्शाता है, जो Solidity के fixed-size टाइप जैसे uint256 से अलग है। यह overflow या underflow के बिना arithmetic (अंकगणित) करता है, जो शुद्ध गणित के आधार पर reasoning (तर्क) करने की अनुमति देता है। इसलिए, यह उन overflow या underflow को उजागर करता है जो अन्यथा unchecked ब्लॉक्स या inline assembly में पकड़े नहीं जा सकते हैं।

इस अध्याय में, आप सीखेंगे:

• mathint क्या है और यह डिफ़ॉल्ट टाइप क्यों है
• mathint से uint256 में cast कैसे करें और ऐसा करने के क्या खतरे हैं
• हम कैसे optimized assembly कोड की तुलना “intended” (लक्षित) फॉर्मूले से कर सकते हैं और देख सकते हैं कि assumptions (मान्यताएं) सही साबित होती हैं या नहीं

Unchecked Block

Solidity में, एक unchecked ब्लॉक overflow/underflow चेक्स को डिसेबल कर देता है। इसलिए CVL में, हमें इन overflow/underflow स्थितियों को उजागर करने के लिए mathint का उपयोग करके तर्क करना चाहिए।

इसे प्रदर्शित करने के लिए, average() फंक्शन पर विचार करें जो दो unsigned integers को स्वीकार करता है और उनका औसत (average) निकालता है:

Copy
/// Solidity

function average(uint256 x, uint256 y) external pure returns (uint256) {
    unchecked {
        return (x + y) / 2;
    }
}

आइए नीचे दिए गए रूल (rule) को लिखकर formally verify करें कि क्या यह फंक्शन सही ढंग से दो unsigned integers का औसत लौटाता है:

Copy
/// CVL

rule average_overflow() {
    uint256 x;
    uint256 y;

    
mathint returnVal = average(x, y);

    assert returnVal == (x + y) / 2;
}

यह रूल फेल हो जाता है, जो यह दर्शाता है कि x + y के इवैल्यूएशन के दौरान एक overflow हुआ था। हम आगे इसका कारण समझाएंगे।

CVL Arithmetic डिफ़ॉल्ट रूप से mathint पर Evaluate होता है

Overflow इसलिए डिटेक्ट हुआ क्योंकि CVL assertion के right-hand side (x + y) / 2 का डिफ़ॉल्ट टाइप mathint था। Certora mathint को इस प्रकार परिभाषित करता है: _“… एक ऐसा टाइप जो किसी भी आकार के integer को दर्शा सकता है; _ mathint पर ऑपरेशन्स कभी भी overflow या underflow नहीं हो सकते हैं।” - source

यह देखने के लिए कि overflow कैसे डिटेक्ट हुआ, आइए assertion के दोनों तरफ़ एक त्वरित कैलकुलेशन (calculation) करें:

Copy
// assert `left-hand side` == `right-hand-side`
assert returnVal == (x + y) / 2;

आइए औसत निकालने के लिए उन्हीं values का उपयोग करें जो Prover ने इस्तेमाल की थीं (2^256 - 3 और 3, जैसा कि छवि में दिखाया गया है) और समझें कि रूल क्यों फेल हुआ।

चूंकि right-hand side (x + y) / 2 डिफ़ॉल्ट रूप से mathint में evaluate होता है, यह सही ढंग से औसत की गणना 2^255 के रूप में करता है:

• x + y = 2^256 (x = 2^256 - 3 और y = 0x3 के साथ)
• 2^256 / 2 = 2^255

Left-hand side, जो कि Solidity द्वारा invoke किए गए average() फंक्शन की रिटर्न वैल्यू (returnVal) है, वह 0 में evaluate हुई:

• x + y = 0 (x = 2^256 - 3 और y = 0x3 के साथ) overflow के कारण
• 0 / 2 = 0

जबकि right-hand side ने unbounded mathint के कारण सही ढंग से औसत की गणना की, left-hand side का returnVal (Solidity फंक्शन की रिटर्न वैल्यू) x + y के एग्जीक्यूशन के दौरान overflow हो गया और शून्य (zero) पर रैप अराउंड (wrapped around) हो गया। इसके कारण कैलकुलेशंस में मिसमैच (mismatch) हुआ। इसलिए, 0 != 2^255, जिसके परिणामस्वरूप equality चेक फेल हो गया।

चूंकि CVL arithmetic डिफ़ॉल्ट रूप से mathint का उपयोग करता है, इसलिए स्पेसिफिकेशन्स (specifications) लिखना अधिक सुरक्षित है क्योंकि यह गलती से arithmetic ऑपरेशन्स को bounded टाइप में cast करने की संभावना को खत्म कर देता है। हालाँकि, यह हमें uint256 में cast करने से नहीं रोकता है, जो खतरनाक हो सकता है, जैसा कि हम अगले सेक्शन में देखेंगे।

mathint को uint256 में Downcast करना Overflow/Underflow समस्याओं को खतरनाक रूप से छिपा सकता है

require_uint256 एक built-in CVL फंक्शन है जो एक unbounded mathint को bounded uint256 में cast करता है। Certora के अनुसार:

“… _ require _ कास्ट उन counterexamples को नज़रअंदाज़ कर देगा जहाँ cast वैल्यू रेंज से बाहर है।” - source

इसे प्रदर्शित करने के लिए, हम पिछले रूल पर फिर से विचार करेंगे और इसे इस तरह से दोबारा लिखेंगे ताकि CVL ऑपरेशन्स “जानबूझकर” require_uint256 के माध्यम से uint256 का उपयोग करें। इसलिए, महत्वपूर्ण रूल उल्लंघनों को नज़रअंदाज़ कर दिया जाएगा।

यहाँ CVL रूल है:

Copy
/// CVL

rule average_overflowIgnored() {
    uint256 x;
    uint256 y;

    mathint returnVal = average(x, y);
    
    uint256 numerator = require_uint256(x + y);
    uint256 expectedVal = r
equire_uint256(numerator / 2);


    assert returnVal == expectedVal;
}

उपरोक्त रूल में, assertion के right-hand side (expectedVal) को require_uint256 का उपयोग करके uint256 रेंज तक सीमित कर दिया गया था, जो स्वाभाविक रूप से किसी भी ऐसे इनपुट को बाहर कर देता है जो overflow का कारण बनेगा।

नतीजतन, expectedVal हमेशा returnVal के बराबर होता है, जिससे overflow को चुपचाप नज़रअंदाज़ करते हुए रूल पास हो जाता है:

Prover रन: link

Inline Assembly

Overflow/underflow का एक अन्य स्रोत inline assembly है। हालाँकि यह gas-efficient कोड को सक्षम बनाता है, यह Solidity के सुरक्षा चेक्स (safety checks) को बायपास करता है, जिसमें overflows और underflows के चेक्स भी शामिल हैं।

इसे प्रदर्शित करने के लिए, flawedCeilDiv() फंक्शन पर विचार करें, जो inline assembly का उपयोग करके ceiling division लागू करता है। यह गणितीय सूत्र (mathematical formula) (n + d - 1) / d की नकल करता है, जो गैर-शून्य (non-zero) remainder (शेषफल) होने पर integer division के परिणाम को राउंड अप (round up) करता है। उदाहरण के लिए, 6 / 3, 2 में evaluate होता है क्योंकि विभाजन (division) सटीक है, जबकि 5 / 2, 3 में evaluate होता है क्योंकि शेषफल राउंड-अप के लिए मजबूर करता है।

नीचे फंक्शन इम्प्लीमेंटेशन दिया गया है:

Copy
/// Solidity

function flawedCeilDiv(uint256 n, uint256 d) external pure returns (uint256 z) {
    assembly { 
        z := div(sub(add(n, d), 1), d) 
    }
}

यहाँ बताया गया है कि assembly कैसे काम करती है:

• add(n, d) → n + d की गणना करता है
• sub(..., 1) → 1 घटाता है → n + d - 1
• div(..., d) → विभाजन (division) करता है

अब आइए formally verify करें कि क्या फॉर्मूला (n + d - 1) / d फंक्शन flawedCeilDiv() के intended व्यवहार के समतुल्य (equivalent) है:

Copy
/// CVL

rule flawedCeilDiv_overflow() {
    uint256 n;
    uint256 d;

    require d != 0;
    
    mathint returnVal = flawedCeilDiv(n, d);
    mathint expectedVal = (n + d - 1) / d;

    assert returnVal == expectedVal;   
}

नोट: Precondition require d != 0 प्रदर्शन के उद्देश्य से division-by-zero त्रुटियों को बाहर रखता है, क्योंकि हमारा ध्यान यहाँ overflow व्यवहार का पता लगाने पर है, न कि शून्य से विभाजन (division by zero) पर।

जैसा कि अपेक्षित था, n + d के इवैल्यूएशन (evaluation) के दौरान एक overflow के कारण यहाँ एक उल्लंघन (violation) हुआ है:

हम विशेष रूप से यह जांचना चाहते हैं कि क्या flawedCeilDiv(), (n + d - 1) / d के समान व्यवहार करता है, लेकिन हम अप्रत्याशित रूप से यह भी पता लगाते हैं कि एक overflow होता है। यह इस बात पर प्रकाश डालता है कि CVL arithmetic ऑपरेशन्स का डिफ़ॉल्ट mathint क्यों होता है।

इस बात पर ज़ोर देना कि mathint को Downcast करना Overflow/Underflow को छिपा सकता है

CVL arithmetic ऑपरेशन्स को uint256 में downcast करने से क्यों बचना चाहिए, इस पर ज़ोर देने के लिए, हमने जानबूझकर expectedVal (जो डिफ़ॉल्ट रूप से mathint है) को uint256 रेंज तक सीमित कर दिया है:

Copy
/// CVL

rule flawedCeilDiv_overflowIgnored() {
    uint256 n;
    uint256 d;

    require d != 0;
    mathint returnVal = flawedCeilDiv(n, d);

    uint256 numerator = require_uint256(n + d - 1);         
    uint256 expectedVal = require_uint256(numerator / d);  
                               
    assert returnVal == expectedVal;
}

नतीजतन, uint256 रेंज के बाहर के counterexamples को नज़रअंदाज़ कर दिया जाता है; इसलिए, overflow के व्यवहार को छिपाते हुए रूल पास हो जाता है:

Prover रन: link

unsafeDivUp के Non-Overflow व्यवहार को Verify करना

आइए Solidity फंक्शन flawedCeilDiv() को एक ऐसे विकल्प से बदलें जो overflow नहीं होता है। ऐसा ही एक इम्प्लीमेंटेशन Solmate का unsafeDivUp() फंक्शन है, जिसे नीचे दिखाया गया है:

Copy
/// Solidity

function unsafeDivUp(uint256 x, uint256 y) external pure returns (uint256 z) {
    /// @solidity memory-safe-assembly
    assembly {
        // Add 1 to x * y if x % y > 0. Note this will
        // return 0 instead of reverting if y is zero.
        z := add(gt(mod(x, y), 0), div(x, y))
    }
}

नोट: हमने फंक्शन की विज़िबिलिटी को बदलकर external कर दिया है ताकि harness के उपयोग से बचा जा सके, जो इस लेख के दायरे से बाहर है।

अब आइए formally verify करें कि क्या (n + d - 1) / d, unsafeDivUp() के intended व्यवहार के बराबर है:

Copy
/// CVL

rule unsafeDivUp_noOverflow() {
    uint256 n;
    uint256 d;

    require d != 0;
    mathint result = unsafeDivUp(n, d);        
    
    mathint expected = (n + d - 1) / d;
    assert result == expected;
}

जैसा कि हम देखते हैं, फंक्शन इस मान्यता (assumption) के तहत सही (hold) साबित होता है कि यह (n + d - 1) / d के समतुल्य व्यवहार करता है। चूंकि CVL ऑपरेशन्स स्वाभाविक रूप से mathint का डिफ़ॉल्ट रूप लेते हैं, इसलिए हम देख सकते हैं कि कोई overflow नहीं होता है (इसके बारे में सक्रिय रूप से सोचे बिना भी)।

Prover रन: link

नोट: Precondition require d != 0 शून्य से विभाजन (division by zero) को बाहर रखता है, क्योंकि यह रूल केवल non-overflow व्यवहार को verify करने पर केंद्रित है।

अंतिम नोट के रूप में, Certora निम्नलिखित व्यावहारिक दिशानिर्देश (practical guideline) प्रदान करता है:

“सामान्य नियम (rule of thumb) यह है कि आपको जब भी संभव हो mathint का उपयोग करना चाहिए; कॉन्ट्रैक्ट फंक्शन्स में इनपुट के रूप में पास किए जाने वाले डेटा के लिए ही uint या int टाइप्स का उपयोग करें।” - source

सारांश

• mathint CVL में एक unbounded टाइप है जो overflow या underflow के बिना arithmetic को मॉडल करता है।
• CVL में Arithmetic डिफ़ॉल्ट रूप से mathint होता है, जो गलती से bounded टाइप्स में casting से बचकर स्पेसिफिकेशन्स को सुरक्षित बनाता है।
• require_uint256 एक mathint टाइप को uint256 रेंज तक सीमित करता है, इसलिए max_uint256 से अधिक की values को नज़रअंदाज़ कर देता है। इस प्रकार, यह overflows को छिपा सकता है।
• जब भी संभव हो mathint का उपयोग करें, और कॉन्ट्रैक्ट फंक्शन आर्गुमेंट्स के लिए uint या int का उपयोग करें।

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