किसी भी सही ERC20 इम्प्लीमेंटेशन में, सभी अकाउंट बैलेंस का योग हमेशा कुल टोकन सप्लाई (total token supply) के बराबर होना चाहिए। यह प्रॉपर्टी किसी भी स्टेट चेंज (state changes) के दौरान हमेशा सत्य रहनी चाहिए। यदि कोई कॉल, चाहे वह डायरेक्ट हो या कॉल्स के सीक्वेंस का हिस्सा हो, इस invariant का उल्लंघन करती है, तो यह कॉन्ट्रैक्ट के लॉजिक और डिज़ाइन में एक बुनियादी खामी (fundamental flaw) का संकेत देता है।
इस अध्याय (chapter) में, हम इस महत्वपूर्ण invariant को formally verify करने के लिए पिछले अध्यायों से ghost variables और hooks के बारे में जो कुछ हमने सीखा है, उसका उपयोग करेंगे।
Verification के लिए Smart Contracts जोड़ना
इस ट्यूटोरियल के लिए, हम Transmission11 द्वारा विकसित the Solmate library से ERC20 कॉन्ट्रैक्ट का उपयोग करेंगे। इस कॉन्ट्रैक्ट को अपने प्रोजेक्ट में शामिल करने के लिए, अपनी Certora प्रोजेक्ट डायरेक्टरी की contracts सबडायरेक्टरी के अंदर ERC20.sol नाम की एक नई फ़ाइल बनाएँ। फिर, Solmate’s ERC20 implementation के कोड को कॉपी करें और उसे उस फ़ाइल में पेस्ट करें।
// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity 0.8.25;
/// @notice Modern and gas efficient ERC20 + EIP-2612 implementation.
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author Modified from Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev Do not manually set balances without updating totalSupply, as the sum of all user balances must not exceed it.
contract ERC20 {
/*//////////////////////////////////////////////////////////////
EVENTS
//////////////////////////////////////////////////////////////*/
event Transfer(address indexed from, address indexed to, uint256 amount);
event Approval(address indexed owner, address indexed spender, uint256 amount);
/*//////////////////////////////////////////////////////////////
METADATA STORAGE
//////////////////////////////////////////////////////////////*/
string public name;
string public symbol;
uint8 public immutable decimals;
/*//////////////////////////////////////////////////////////////
ERC20 STORAGE
//////////////////////////////////////////////////////////////*/
uint256 public totalSupply;
mapping(address => uint256) public balanceOf;
mapping(address => mapping(address => uint256)) public allowance;
/*//////////////////////////////////////////////////////////////
EIP-2612 STORAGE
//////////////////////////////////////////////////////////////*/
uint256 internal immutable INITIAL_CHAIN_ID;
bytes32 internal immutable INITIAL_DOMAIN_SEPARATOR;
mapping(address => uint256) public nonces;
/*//////////////////////////////////////////////////////////////
CONSTRUCTOR
//////////////////////////////////////////////////////////////*/
constructor(
string memory _name,
string memory _symbol,
uint8 _decimals
) {
name = _name;
symbol = _symbol;
decimals = _decimals;
INITIAL_CHAIN_ID = block.chainid;
INITIAL_DOMAIN_SEPARATOR = computeDomainSeparator();
}
/*//////////////////////////////////////////////////////////////
ERC20 LOGIC
//////////////////////////////////////////////////////////////*/
function approve(address spender, uint256 amount) public virtual returns (bool) {
allowance[msg.sender][spender] = amount;
emit Approval(msg.sender, spender, amount);
return true;
}
function transfer(address to, uint256 amount) public virtual returns (bool) {
balanceOf[msg.sender] -= amount;
// Cannot overflow because the sum of all user
// balances can't exceed the max uint256 value.
unchecked {
balanceOf[to] += amount;
}
emit Transfer(msg.sender, to, amount);
return true;
}
function transferFrom(
address from,
address to,
uint256 amount
) public virtual returns (bool) {
uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.
if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;
balanceOf[from] -= amount;
// Cannot overflow because the sum of all user
// balances can't exceed the max uint256 value.
unchecked {
balanceOf[to] += amount;
}
emit Transfer(from, to, amount);
return true;
}
/*//////////////////////////////////////////////////////////////
EIP-2612 LOGIC
//////////////////////////////////////////////////////////////*/
function permit(
address owner,
address spender,
uint256 value,
uint256 deadline,
uint8 v,
bytes32 r,
bytes32 s
) public virtual {
require(deadline >= block.timestamp, "PERMIT_DEADLINE_EXPIRED");
// Unchecked because the only math done is incrementing
// the owner's nonce which cannot realistically overflow.
unchecked {
address recoveredAddress = ecrecover(
keccak256(
abi.encodePacked(
"\x19\x01",
DOMAIN_SEPARATOR(),
keccak256(
abi.encode(
keccak256(
"Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"
),
owner,
spender,
value,
nonces[owner]++,
deadline
)
)
)
),
v,
r,
s
);
require(recoveredAddress != address(0) && recoveredAddress == owner, "INVALID_SIGNER");
allowance[recoveredAddress][spender] = value;
}
emit Approval(owner, spender, value);
}
function DOMAIN_SEPARATOR() public view virtual returns (bytes32) {
return block.chainid == INITIAL_CHAIN_ID ? INITIAL_DOMAIN_SEPARATOR : computeDomainSeparator();
}
function computeDomainSeparator() internal view virtual returns (bytes32) {
return
keccak256(
abi.encode(
keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"),
keccak256(bytes(name)),
keccak256("1"),
block.chainid,
address(this)
)
);
}
/*//////////////////////////////////////////////////////////////
INTERNAL MINT/BURN LOGIC
//////////////////////////////////////////////////////////////*/
function _mint(address to, uint256 amount) internal virtual {
totalSupply += amount;
// Cannot overflow because the sum of all user
// balances can't exceed the max uint256 value.
unchecked {
balanceOf[to] += amount;
}
emit Transfer(address(0), to, amount);
}
function _burn(address from, uint256 amount) internal virtual {
balanceOf[from] -= amount;
// Cannot underflow because a user's balance
// will never be larger than the total supply.
unchecked {
totalSupply -= amount;
}
emit Transfer(from, address(0), amount);
}
}
Challenge को समझना
हमारे invariant को CVL एक्सप्रेशन के रूप में व्यक्त करने के लिए, हमें दो वैल्यूज़ की आवश्यकता है:
- कुल टोकन सप्लाई (The total token supply)
- सभी अकाउंट बैलेंस का योग (The sum of all account balances)
हमारे कॉन्ट्रैक्ट में totalSupply नामक एक पब्लिक स्टेट वेरिएबल है जो किसी भी स्टेट में कुल टोकन सप्लाई का ट्रैक रखता है और जिसकी वैल्यू को totalSupply() नामक गेटर फंक्शन (getter function) का उपयोग करके पढ़ा जा सकता है। हालाँकि, मुख्य चुनौती यह है कि कॉन्ट्रैक्ट सभी बैलेंस का कुल योग प्राप्त करने का कोई इन-बिल्ट (built-in) तरीका प्रदान नहीं करता है।
“समाधान” (The Solution)
सभी अकाउंट्स के बैलेंस का योग प्राप्त करने के लिए, हम sumOfBalances नामक एक ghost वेरिएबल बनाएँगे जिसकी प्रारंभिक वैल्यू (initial value) init_state axiom का उपयोग करके 0 पर सेट की जाएगी। balanceOf मैपिंग में जब भी कोई राईट ऑपरेशन (write operation) होगा, तो हर बार एक स्टोर हुक (store hook) के माध्यम से ghost sumOfBalances को अपडेट किया जाएगा।
जैसा कि हम जानते हैं, स्टोर हुक हमें अपडेट किए जा रहे बैलेंस की पुरानी और नई दोनों वैल्यूज़ तक एक्सेस दे सकता है। हम इन वैल्यूज़ का उपयोग बदलाव (change) की गणना करने और तदनुसार अपने ghost को अपडेट करने के लिए करते हैं:
sumOfBalances = sumOfBalances - oldValue + newValue;
उदाहरण के लिए, यदि किसी यूज़र का बैलेंस 100 से बढ़कर 150 हो जाता है, तो हमारा हुक sumOfBalances से 100 घटाता है और उसमें 150 जोड़ता है, जिससे कुल योग सही ढंग से 50 बढ़ जाता है। हर बैलेंस अपडेट के लिए इस डेल्टा कैलकुलेशन (delta calculation) को लागू करके, हमारा ghost sumOfBalances कॉन्ट्रैक्ट स्टेट में होने वाले बदलावों को ट्रैक करेगा, जो सभी बैलेंस के योग को बिल्कुल सही तरीके से दर्शाएगा।
एक बार जब Prover के पास ये दोनों वैल्यूज़ उपलब्ध हो जाती हैं (कॉन्ट्रैक्ट से वास्तविक totalSupply और हमारा सटीक रूप से मेंटेन किया गया sumOfBalances ghost), तो हम CVL में invariant ब्लॉक का उपयोग करके formally यह दावा (assert) कर सकते हैं कि कुल सप्लाई हमेशा सभी अकाउंट बैलेंस के योग के बराबर होती है।
स्टेप-बाय-स्टेप Full Specification लिखना
आइए अब तक हमने जो भी चर्चा की है, उसे व्यवहार में लाएं और नीचे दिए गए स्टेप्स का पालन करते हुए एक पूर्ण स्पेसिफिकेशन (complete specification) लिखें जो यह वेरिफाई करे कि क्या सभी बैलेंस का योग कुल टोकन सप्लाई से मेल खाता है:
- अपनी Certora प्रोजेक्ट डायरेक्टरी के अंदर,
specsसबडायरेक्टरी में जाएँ औरerc20.specनाम की एक नई फ़ाइल बनाएँ। erc20.specके अंदर,sumOfBalancesनामक एक ghost वेरिएबल को डिफाइन करें।
ghost mathint sumOfBalances;
- इसके बाद, हम invariant बेस केस (base case) में
sumOfBalancesकी प्रारंभिक वैल्यू को0पर सेट करने के लिएinit_stateaxiom का उपयोग करते हैं**।**
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
यह axiom केवल invariant बेस केस में ghost वेरिएबल को कंस्ट्रेन (constrain) करता है, जिससे एक सुसंगत (consistent) पोस्ट-कंस्ट्रक्टर स्टेट स्थापित होती है। इस बेसलाइन के बिना, Prover ghost के लिए कोई भी मनमानी (arbitrary) प्रारंभिक वैल्यू मान सकता है, जिससे invariant preservation अर्थहीन हो जाएगा।
- एक स्टोर हुक (store hook) को डिफाइन करें जो
balanceOfमैपिंग में होने वाले बदलावों को ट्रैक करे और उसके अनुसार हमारे ghost वेरिएबलsumOfBalancesको अपडेट करे।
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
- चूँकि अब हमारे पास दोनों वैल्यूज़ हैं — कॉन्ट्रैक्ट का
totalSupply()और हमारा ghostsumOfBalances— हम कोर (core) invariant को नीचे दिखाए गए अनुसार डिफाइन कर सकते हैं:
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
- अंत में, एक methods ब्लॉक जोड़ें जिसमें
totalSupply()का फंक्शन सिग्नेचर शामिल होगा।
methods {
function totalSupply() external returns(uint256) envfree;
}
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
confsसबडायरेक्टरी में जाएँ औरerc20.confनाम की एक नई फ़ाइल बनाएँ।
{
"files": [
"contracts/ERC20.sol:ERC20"
],
"verify": "ERC20:specs/erc20.spec",
"msg": "Testing erc20 functionality"
}
Verification को रन करना
एक बार जब आप उपरोक्त सभी स्टेप्स को निष्पादित (execute) कर लेते हैं, तो अपने टर्मिनल में कमांड certoraRun confs/erc20.conf चलाकर वेरिफिकेशन के लिए कोड सबमिट करें।
नीचे दी गई इमेज के समान परिणाम देखने के लिए अपनी पसंद के किसी भी वेब ब्राउज़र में Prover द्वारा प्रदान किए गए verification result को खोलें:
हमारे वेरिफिकेशन रिज़ल्ट में, हम देख सकते हैं कि invariant चेक दोनों जगहों पर विफल (fail) हो गया: कंस्ट्रक्टर कॉल के बाद और मेथड एग्जीक्यूशन (method execution) के दौरान।
जब हम “induction base: After the constructor” वायलेशन (violation) पर क्लिक करते हैं, तो Prover आपके कॉन्फ़िगरेशन में optimistic_loop की (key) जोड़ने और उसकी वैल्यू को true पर सेट करने की सिफारिश करता है, या इसके विकल्प के रूप में loop_iter को 1 से अधिक वैल्यू तक बढ़ाने का सुझाव देता है।
अभी के लिए, आइए optimistic_loop की (key) को true पर सेट करके कॉन्फ़िगरेशन फ़ाइल को अपडेट करते हुए Prover की सिफारिश का पालन करें। हम इस मुद्दे को बाद के एक अध्याय में अधिक गहराई से समझेंगे जिसका शीर्षक है “How Strings Lead to Loops?”।
{
"files": [
"contracts/ERC20.sol:ERC20"
],
"verify": "ERC20:specs/erc20.spec",
"optimistic_loop": true,
"msg": "Testing erc20 functionality"
}
एक बार हो जाने के बाद, टर्मिनल में कमांड certoraRun confs/erc20.conf चलाकर Prover को फिर से रन करें। हमारे नए वेरिफिकेशन रिज़ल्ट में, हम देख सकते हैं कि हमारा invariant कंस्ट्रक्टर एग्जीक्यूशन के दौरान सफलतापूर्वक पास हो जाता है लेकिन मेथड एग्जीक्यूशन के दौरान विफल (fail) हो जाता है, विशेष रूप से transfer() और transferFrom() फंक्शन्स के लिए।
वायलेशन के कारण को समझने के लिए, transfer() या transferFrom() फंक्शन के कॉल ट्रेस (call trace) पर क्लिक करें। हमारे मामले में, हम transfer() फंक्शन के कॉल ट्रेस का विश्लेषण करेंगे।
पूरा कॉल ट्रेस देखने के लिए, Call Trace पैनल के ऊपरी-दाएँ कोने पर उपलब्ध “Expand” बटन पर क्लिक करें।
कॉल ट्रेस में, हम देख सकते हैं कि व्यक्तिगत अकाउंट्स 0x7 और 0x8200 के प्रारंभिक बैलेंस क्रमशः 2^256 − 4 और 0xf000000000000000000000000000000000000000000000000000000000000000 पर सेट हैं। डेसीमल रूप (decimal form) में, ये 115792089237316195423570985008687907853269984665640564039457584007913129639932 और 108890810646419256008710686707116392212123736112785533035372916772359555072000 के बराबर हैं।
ये दोनों वैल्यूज़ Prover द्वारा havocing के माध्यम से असाइन की गई हैं और संख्यात्मक सीमा (numerical range) 0 से 2^{256} - 1 के अंतर्गत आती हैं। हालाँकि, किसी भी सही ढंग से इम्प्लीमेंट किए गए ERC20 कॉन्ट्रैक्ट में, किसी भी व्यक्तिगत अकाउंट का बैलेंस कभी भी सभी बैलेंस के कुल योग से अधिक नहीं होना चाहिए। इस परिदृश्य में, दोनों अकाउंट्स उन बैलेंस के साथ शुरू होते हैं जो कुल सप्लाई (0xa) और sumOfBalances से बहुत अधिक हैं, जो एक असंभव प्रारंभिक स्टेट (impossible initial state) बनाता है जो वास्तविक डिप्लॉयमेंट में कभी मौजूद नहीं हो सकती।
Prover ऐसा इसलिए करता है क्योंकि यह स्वाभाविक रूप से ERC20 टोकन के बिज़नेस लॉजिक को नहीं समझता है; यह केवल स्टोरेज को कच्चे डेटा (raw data) के रूप में मानता है। जब तक कि स्पष्ट रूप से कंस्ट्रेन (constrain) न किया जाए, यह मानता है कि कोई भी uint256 वैल्यू एक वैध शुरुआती बिंदु (valid starting point) है।
इससे बचने के लिए, हमें विशेष रूप से Prover को यह बताना होगा कि प्रारंभिक व्यक्तिगत अकाउंट बैलेंस sumOfBalances से अधिक नहीं होना चाहिए। ऐसा करने के लिए, हम उन वैल्यूज़ को कंस्ट्रेन करने के लिए CVL द्वारा प्रदान किए गए require स्टेटमेंट का उपयोग करेंगे जिन पर Prover को विचार करना चाहिए।
require स्टेटमेंट का उपयोग करके Initial Balances को Constrain करना
हमारी erc20.spec फ़ाइल में, किसी भी अकाउंट के बैलेंस को असाइन की जा सकने वाली वैल्यूज़ के दायरे को सीमित करने के लिए हमारे स्टोर हुक में नीचे दिखाया गया कोड जोड़ें। एक बार हो जाने के बाद, वेरिफिकेशन रिज़ल्ट देखने के लिए Prover को फिर से रन करें।
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
require oldAmount <= sumOfBalances; //add this line
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
नए परिणाम (new result) में, आप देखेंगे कि Prover को अब कोई वायलेशन (violation) नहीं मिलता है।
हमारा invariant totalSupplyEqSumOfBalances वेरिफिकेशन में पास हो गया क्योंकि, स्टोर हुक में require oldAmount <= sumOfBalances; लाइन जोड़ने के बाद, Prover केवल उन एग्जीक्यूशन पाथ (execution paths) को एक्सप्लोर करेगा जहाँ यह स्थिति सत्य होती है। यह प्रभावी रूप से उन काउंटरएग्जांपल (counterexamples) को खारिज कर देता है जो कुल योग से अधिक एक सिंगल बैलेंस पर निर्भर करते हैं (उदाहरण के लिए, transfer में सेंडर या रिसीवर का बैलेंस), यह सुनिश्चित करते हुए कि Prover उन परिदृश्यों पर ध्यान केंद्रित करता है जहाँ व्यक्तिगत बैलेंस कुल सप्लाई की तार्किक सीमाओं (logical bounds) के भीतर रहते हैं। परिणामस्वरूप, वेरिफिकेशन सफल होता है, यह पुष्टि करते हुए कि invariant सभी अनुमत ट्रांज़िशन (allowed transitions) के तहत संरक्षित (preserved) रहता है।
एक वैकल्पिक तरीका (An Alternate Approach): लोड हुक (The Load Hook)
हालाँकि Sstore हुक में कंस्ट्रेंट जोड़ना काम करता है, लेकिन एक और तरीका है जहाँ हम व्यक्तिगत बैलेंस पर कंस्ट्रेंट को लोड हुक (Load Hook) के अंदर जोड़ते हैं।
इस तरीके को लागू करने के लिए, नीचे दिए गए स्टेप्स का पालन करें:
balanceOfमैपिंग पर एक लोड हुक को डिफाइन करें जोbalanceOfके हर रीड (read) को इंटरसेप्ट (intercept) करता है।
hook Sload uint256 balance balanceOf[KEY address addr] {}
- इस हुक के अंदर
require sumOfBalances >= to_mathint(balance);का उपयोग करके एक कंस्ट्रेंट (constraint) प्रस्तुत करें।
hook Sload uint256 balance balanceOf[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
Sstoreहुक से कंस्ट्रेंट को हटा दें ताकि हम पूरी तरह से लोड हुक लॉजिक पर निर्भर रहें।
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
require oldAmount <= sumOfBalances; //remove this line
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
ऊपर सुझाए गए बदलावों के बाद अपडेटेड स्पेसिफिकेशन कुछ इस तरह दिखना चाहिए:
methods {
function totalSupply() external returns(uint256) envfree;
}
ghost mathint sumOfBalances {
// Constraining pre-constructor ghost value through axiom
init_state axiom sumOfBalances == 0;
}
// Added a load hook on balanceOf mapping
hook Sload uint256 balance balanceOf[KEY address addr] {
// Introduce a constraint
require sumOfBalances >= to_mathint(balance);
}
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
// Delta Update
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
यदि आप इस बदलाव के साथ वेरिफिकेशन को फिर से रन करते हैं (Sstore हुक से require को हटाकर और इसे केवल Sload हुक में रखकर), तो invariant totalSupplyEqSumOfBalances तब भी पास हो जाएगा।
यह काम करता है क्योंकि लोड हुक स्पष्ट रूप से किसी भी ऐसी स्टेट (state) को फ़िल्टर कर देता है जहाँ किसी व्यक्तिगत अकाउंट का बैलेंस सभी बैलेंस के कुल योग से बड़ा होता है। यदि Prover ऐसी असंभव प्रारंभिक स्टेट का उपयोग करके एक काउंटरएग्जांपल (counterexample) बनाने का प्रयास करता है, तो यह अंततः कॉन्ट्रैक्ट लॉजिक का मूल्यांकन करते समय उस बैलेंस को रीड (read) करेगा। जिस क्षण यह रीड होता है, लोड हुक के अंदर require स्टेटमेंट यह जाँच करता है कि क्या वह बैलेंस हमारे ghost वेरिएबल के अनुरूप है या नहीं। चूँकि बैलेंस अवास्तविक रूप से बड़ा होता है, इसलिए कंडीशन (condition) विफल हो जाती है, और Prover को उस पूरे एग्जीक्यूशन पाथ (execution path) को रद्द (discard) करने के लिए मजबूर होना पड़ता है।
Sstore बनाम Sload: Constraints को कहाँ रखें?
दोनों वर्ज़न “काम करते हैं” क्योंकि वे उन असंभव स्टेट्स को बाहर कर देते हैं जो हमारे invariant का उल्लंघन करेंगी, लेकिन लोड हुक एप्रोच एक अधिक विश्वसनीय और व्यापक (comprehensive) सुरक्षा प्रदान करता है। आइए समझते हैं कि क्यों:
Store Hook वास्तव में क्या गारंटी देता है
जब हम कंस्ट्रेंट को स्टोर हुक में डालते हैं:
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
require oldAmount <= sumOfBalances;
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
उपरोक्त कोड में, हम प्रभावी रूप से Prover को बता रहे हैं: “जब भी आप balanceOf[account] में राईट (write) करते हैं, तो सुनिश्चित करें कि पिछली वैल्यू (oldAmount), sumOfBalances से बड़ी नहीं थी”
यह एक ब्लाइंड स्पॉट (blind spot) बनाता है:
- यदि Prover किसी निश्चित
balanceOf[addr]स्लॉट में कभी राईट नहीं करता है, तो इस हुक को उस एड्रेस के लिए कभी भी ट्रिगर नहीं किया जाता है। - इसका मतलब है कि Prover अभी भी एक अजीब प्रारंभिक वैल्यू (havoc के माध्यम से) से शुरू करने के लिए स्वतंत्र है, जैसे
balanceOf[addr] = 2^{256} - 1, भले हीsumOfBalances = 10हो। - जब तक कॉन्ट्रैक्ट उस स्लॉट में राईट करने का प्रयास नहीं करता है, तब तक
Sstoreमेंrequireको कभी चेक नहीं किया जाता है, और असंभव स्टेट को रीड्स (reads) और तार्किक तर्क (logical reasoning) के दौरान बने रहने की अनुमति मिल जाती है।
संक्षेप में, स्टोर हुक केवल यह कहता है: “यदि आप कभी भी इस स्लॉट में राईट करके इसे टच करते हैं, तो पिछली वैल्यू उचित (reasonable) होनी चाहिए।” यह यह नहीं कहता है: “जब भी आप उन्हें देखते हैं तो सभी बैलेंस हमेशा उचित होते हैं।”
इसके बजाय Load Hook क्या गारंटी देता है
अब, लोड हुक वर्ज़न को देखें:
hook Sload uint256 balance balanceOf[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
यह हर बार रन होता है जब Prover balanceOf से बैलेंस रीड करता है। यहाँ, हम Prover को बता रहे हैं: “जब भी आप कोई बैलेंस रीड करते हैं, तो वह बैलेंस sumOfBalances से कम या उसके बराबर होना चाहिए”
इसके दो महत्वपूर्ण प्रभाव (effects) हैं:
- Prover किसी भी कैलकुलेशन में एक असंभव बैलेंस का उपयोग नहीं कर सकता है। यदि यह यह मानने की कोशिश करता है कि
balanceOf[addr],sumOfBalancesसे बड़ा है और फिर इसे रीड करता है, तो लोड हुक मेंrequireविफल हो जाता है, और उस एग्जीक्यूशन पाथ को तुरंत रद्द कर दिया जाता है। - यह तब भी लागू होता है भले ही स्लॉट में कभी राईट न किया गया हो। Prover शुरुआत में
balanceOf[addr]को किसी मनमानी (arbitrary) वैल्यू में havoc कर सकता है, लेकिन जिस क्षण यह उस वैल्यू को रीड (read) करता है, लोड हुक इसे चेक करता है। यदि वैल्यू असंभव है, तो उस पूरे पाथ को हटा दिया जाता है।
लोड हुक एक ग्लोबल सैनिटी चेक (global sanity check) की तरह काम करता है: “आप जो भी बैलेंस देखते हैं, वह ghost sumOfBalances के संबंध में तर्कसंगत (make sense) होना चाहिए”
यही कारण है कि, जब हम sumOfBalances को वास्तविक बैलेंस के साथ संरेखित (aligned) रखने और असंभव ERC20 स्टेट्स से बचने की परवाह करते हैं, तो लोड हुक एप्रोच आमतौर पर बेहतर विकल्प होता है।
निष्कर्ष (Conclusion)
इस अध्याय में, हमने मूलभूत (fundamental) ERC20 invariant को वेरिफाई किया: Total Supply = Sum of All Balances।
हमने कुल योग को ट्रैक करने के लिए एक ghost variable और उस ghost को कॉन्ट्रैक्ट की स्टोरेज के साथ सिंक्रोनाइज़ (synchronize) करने के लिए hooks का उपयोग करके इसे प्राप्त किया। सबसे महत्वपूर्ण बात यह है कि हमने प्रदर्शित किया कि Sload हुक में कंस्ट्रेंट्स को रखना अक्सर Sstore हुक की तुलना में अधिक सुरक्षित क्यों होता है। जब भी वैल्यूज़ को रीड किया जाता है तो उन पर नियंत्रण (policing) रखकर, हमने प्रभावी रूप से उस “ब्लाइंड स्पॉट” को बंद कर दिया जहाँ अन्यथा Prover असंभव प्रारंभिक स्टेट्स को मान सकता था।
ये तकनीकें आपको लो-लेवल स्टोरेज के ऊपर हाई-लेवल बिज़नेस रूल्स को सिद्ध (prove) करने की अनुमति देती हैं, यह सुनिश्चित करते हुए कि आपका वेरिफिकेशन पूरी तरह से वैध, यथार्थवादी कॉन्ट्रैक्ट व्यवहारों पर केंद्रित हो।
यह लेख formal verification using the Certora Prover पर एक सीरीज़ का हिस्सा है।