திறன் ஒப்பந்தங்களின் முறைசார் சரிபார்ப்பு
திறன் ஒப்பந்தங்கள் புதிய பயன்பாட்டு நிகழ்வுகளை அறிமுகப்படுத்தும் மற்றும் பயனர்களுக்கான மதிப்பைத் திறக்கும் பரவலாக்கப்பட்ட, நம்பிக்கை தேவையில்லாத மற்றும் வலுவான செயலிகளை உருவாக்குவதை சாத்தியமாக்குகின்றன. திறன் ஒப்பந்தங்கள் அதிக அளவிலான மதிப்பைக் கையாளுவதால், உருவாக்குநர்களுக்குப் பாதுகாப்பு என்பது ஒரு முக்கியமான கருத்தாகும்.
திறன் ஒப்பந்தப் பாதுகாப்பை மேம்படுத்துவதற்குப் பரிந்துரைக்கப்படும் நுட்பங்களில் முறைசார் சரிபார்ப்பும் ஒன்றாகும். நிரல்களைக் குறிப்பிடவும், வடிவமைக்கவும் மற்றும் சரிபார்க்கவும் முறைசார் வழிமுறைகளைப் (opens in a new tab) பயன்படுத்தும் முறைசார் சரிபார்ப்பு, முக்கியமான வன்பொருள் மற்றும் மென்பொருள் அமைப்புகளின் சரியான தன்மையை உறுதிப்படுத்த பல ஆண்டுகளாகப் பயன்படுத்தப்பட்டு வருகிறது.
திறன் ஒப்பந்தங்களில் செயல்படுத்தப்படும்போது, ஒரு ஒப்பந்தத்தின் வணிக தர்க்கம் முன்வரையறுக்கப்பட்ட விவரக்குறிப்பைப் பூர்த்தி செய்கிறது என்பதை முறைசார் சரிபார்ப்பு நிரூபிக்க முடியும். சோதனை போன்ற ஒப்பந்தக் குறியீட்டின் சரியான தன்மையை மதிப்பிடுவதற்கான பிற முறைகளுடன் ஒப்பிடுகையில், ஒரு திறன் ஒப்பந்தம் செயல்பாட்டு ரீதியாகச் சரியானது என்பதற்கான வலுவான உத்தரவாதங்களை முறைசார் சரிபார்ப்பு வழங்குகிறது.
முறைசார் சரிபார்ப்பு என்றால் என்ன?
முறைசார் சரிபார்ப்பு என்பது ஒரு முறைசார் விவரக்குறிப்பைப் பொறுத்து ஒரு அமைப்பின் சரியான தன்மையை மதிப்பிடும் செயல்முறையைக் குறிக்கிறது. எளிமையான வார்த்தைகளில் கூறுவதானால், ஒரு அமைப்பின் நடத்தை சில தேவைகளைப் பூர்த்தி செய்கிறதா (அதாவது, நாம் விரும்புவதை அது செய்கிறதா) என்பதைச் சரிபார்க்க முறைசார் சரிபார்ப்பு அனுமதிக்கிறது.
அமைப்பின் (இந்த நிலையில் ஒரு திறன் ஒப்பந்தம்) எதிர்பார்க்கப்படும் நடத்தைகள் முறைசார் மாதிரியாக்கத்தைப் பயன்படுத்தி விவரிக்கப்படுகின்றன, அதே நேரத்தில் விவரக்குறிப்பு மொழிகள் முறைசார் பண்புகளை உருவாக்க உதவுகின்றன. முறைசார் சரிபார்ப்பு நுட்பங்கள் ஒரு ஒப்பந்தத்தின் செயலாக்கம் அதன் விவரக்குறிப்புடன் இணங்குகிறதா என்பதைச் சரிபார்த்து, முந்தையதின் சரியான தன்மைக்கான கணித ஆதாரத்தைப் பெறலாம். ஒரு ஒப்பந்தம் அதன் விவரக்குறிப்பைப் பூர்த்தி செய்யும் போது, அது "செயல்பாட்டு ரீதியாகச் சரியானது", "வடிவமைப்பின்படி சரியானது" அல்லது "கட்டமைப்பின்படி சரியானது" என்று விவரிக்கப்படுகிறது.
முறைசார் மாதிரி என்றால் என்ன?
கணினி அறிவியலில், முறைசார் மாதிரி (opens in a new tab) என்பது ஒரு கணக்கீட்டு செயல்முறையின் கணித விளக்கமாகும். நிரல்கள் கணிதச் சார்புகளாக (சமன்பாடுகள்) சுருக்கப்படுகின்றன, ஒரு உள்ளீடு கொடுக்கப்பட்டால் சார்புகளுக்கான வெளியீடுகள் எவ்வாறு கணக்கிடப்படுகின்றன என்பதை மாதிரி விவரிக்கிறது.
முறைசார் மாதிரிகள் ஒரு நிரலின் நடத்தை பற்றிய பகுப்பாய்வை மதிப்பிடக்கூடிய ஒரு சுருக்க நிலையை வழங்குகின்றன. முறைசார் மாதிரிகளின் இருப்பு ஒரு முறைசார் விவரக்குறிப்பை உருவாக்க அனுமதிக்கிறது, இது கேள்விக்குரிய மாதிரியின் விரும்பிய பண்புகளை விவரிக்கிறது.
முறைசார் சரிபார்ப்பிற்காகத் திறன் ஒப்பந்தங்களை மாதிரியாக்க பல்வேறு நுட்பங்கள் பயன்படுத்தப்படுகின்றன. எடுத்துக்காட்டாக, ஒரு திறன் ஒப்பந்தத்தின் உயர்மட்ட நடத்தை பற்றி நியாயப்படுத்த சில மாதிரிகள் பயன்படுத்தப்படுகின்றன. இந்த மாதிரியாக்க நுட்பங்கள் திறன் ஒப்பந்தங்களுக்கு ஒரு பிளாக்-பாக்ஸ் (black-box) பார்வையைப் பயன்படுத்துகின்றன, அவற்றை உள்ளீடுகளை ஏற்றுக்கொண்டு அந்த உள்ளீடுகளின் அடிப்படையில் கணக்கீட்டைச் செயல்படுத்தும் அமைப்புகளாகப் பார்க்கின்றன.
உயர்மட்ட மாதிரிகள் திறன் ஒப்பந்தங்கள் மற்றும் வெளிப்புற முகவர்களான வெளிப்புறமாகச் சொந்தமான கணக்குகள் (EOAs), ஒப்பந்தக் கணக்குகள் மற்றும் தொகுதிச்சங்கிலி சூழல் ஆகியவற்றுக்கு இடையேயான உறவில் கவனம் செலுத்துகின்றன. சில பயனர் தொடர்புகளுக்குப் பதிலளிக்கும் வகையில் ஒரு ஒப்பந்தம் எவ்வாறு செயல்பட வேண்டும் என்பதைக் குறிப்பிடும் பண்புகளை வரையறுக்க இத்தகைய மாதிரிகள் பயனுள்ளதாக இருக்கும்.
மாறாக, பிற முறைசார் மாதிரிகள் ஒரு திறன் ஒப்பந்தத்தின் கீழ்மட்ட நடத்தையில் கவனம் செலுத்துகின்றன. உயர்மட்ட மாதிரிகள் ஒரு ஒப்பந்தத்தின் செயல்பாட்டைப் பற்றி நியாயப்படுத்த உதவினாலும், செயலாக்கத்தின் உள் செயல்பாடுகள் பற்றிய விவரங்களைப் படம்பிடிக்கத் தவறலாம். கீழ்மட்ட மாதிரிகள் நிரல் பகுப்பாய்விற்கு ஒரு ஒயிட்-பாக்ஸ் (white-box) பார்வையைப் பயன்படுத்துகின்றன மற்றும் ஒரு ஒப்பந்தத்தின் செயலாக்கத்திற்குத் தொடர்புடைய பண்புகளைப் பற்றி நியாயப்படுத்த நிரல் தடயங்கள் மற்றும் கட்டுப்பாட்டு ஓட்ட வரைபடங்கள் (opens in a new tab) போன்ற திறன் ஒப்பந்தச் செயலிகளின் கீழ்மட்டப் பிரதிநிதித்துவங்களை நம்பியுள்ளன.
எத்திரியத்தின் செயலாக்கச் சூழலில் (அதாவது, EVM) ஒரு திறன் ஒப்பந்தத்தின் உண்மையான செயலாக்கத்தைப் பிரதிநிதித்துவப்படுத்துவதால் கீழ்மட்ட மாதிரிகள் சிறந்தவையாகக் கருதப்படுகின்றன. திறன் ஒப்பந்தங்களில் முக்கியமான பாதுகாப்புப் பண்புகளை நிறுவுவதற்கும் சாத்தியமான பாதிப்புகளைக் கண்டறிவதற்கும் கீழ்மட்ட மாதிரியாக்க நுட்பங்கள் குறிப்பாகப் பயனுள்ளதாக இருக்கும்.
முறைசார் விவரக்குறிப்பு என்றால் என்ன?
விவரக்குறிப்பு என்பது ஒரு குறிப்பிட்ட அமைப்பு பூர்த்தி செய்ய வேண்டிய ஒரு தொழில்நுட்பத் தேவையாகும். நிரலாக்கத்தில், விவரக்குறிப்புகள் ஒரு நிரலின் செயலாக்கம் பற்றிய பொதுவான யோசனைகளைக் குறிக்கின்றன (அதாவது, நிரல் என்ன செய்ய வேண்டும்).
திறன் ஒப்பந்தங்களின் சூழலில், முறைசார் விவரக்குறிப்புகள் பண்புகளைக் குறிக்கின்றன—ஒரு ஒப்பந்தம் பூர்த்தி செய்ய வேண்டிய தேவைகளின் முறைசார் விளக்கங்கள். இத்தகைய பண்புகள் "மாறிலிகள்" (invariants) என்று விவரிக்கப்படுகின்றன மற்றும் எந்தவொரு விதிவிலக்கும் இல்லாமல், சாத்தியமான ஒவ்வொரு சூழ்நிலையிலும் உண்மையாக இருக்க வேண்டிய ஒரு ஒப்பந்தத்தின் செயலாக்கம் பற்றிய தர்க்கரீதியான உறுதிப்படுத்தல்களைக் குறிக்கின்றன.
எனவே, ஒரு திறன் ஒப்பந்தத்தின் உத்தேசிக்கப்பட்ட செயலாக்கத்தை விவரிக்கும் முறைசார் மொழியில் எழுதப்பட்ட அறிக்கைகளின் தொகுப்பாக முறைசார் விவரக்குறிப்பை நாம் கருதலாம். விவரக்குறிப்புகள் ஒரு ஒப்பந்தத்தின் பண்புகளை உள்ளடக்குகின்றன மற்றும் வெவ்வேறு சூழ்நிலைகளில் ஒப்பந்தம் எவ்வாறு செயல்பட வேண்டும் என்பதை வரையறுக்கின்றன. முறைசார் சரிபார்ப்பின் நோக்கம், ஒரு திறன் ஒப்பந்தம் இந்தப் பண்புகளை (மாறிலிகள்) கொண்டிருக்கிறதா என்பதையும், செயலாக்கத்தின் போது இந்தப் பண்புகள் மீறப்படவில்லையா என்பதையும் தீர்மானிப்பதாகும்.
திறன் ஒப்பந்தங்களின் பாதுகாப்பான செயலாக்கங்களை உருவாக்குவதில் முறைசார் விவரக்குறிப்புகள் முக்கியமானவை. மாறிலிகளைச் செயல்படுத்தத் தவறிய அல்லது செயலாக்கத்தின் போது அவற்றின் பண்புகள் மீறப்படும் ஒப்பந்தங்கள், செயல்பாட்டிற்குத் தீங்கு விளைவிக்கும் அல்லது தீங்கிழைக்கும் சுரண்டல்களை ஏற்படுத்தும் பாதிப்புகளுக்கு ஆளாகின்றன.
திறன் ஒப்பந்தங்களுக்கான முறைசார் விவரக்குறிப்புகளின் வகைகள்
முறைசார் விவரக்குறிப்புகள் நிரல் செயலாக்கத்தின் சரியான தன்மை பற்றிய கணிதப் பகுத்தறிவைச் செயல்படுத்துகின்றன. முறைசார் மாதிரிகளைப் போலவே, முறைசார் விவரக்குறிப்புகளும் உயர்மட்டப் பண்புகள் அல்லது ஒப்பந்தச் செயலாக்கத்தின் கீழ்மட்ட நடத்தையைப் படம்பிடிக்க முடியும்.
முறைசார் விவரக்குறிப்புகள் நிரல் தர்க்கத்தின் (opens in a new tab) கூறுகளைப் பயன்படுத்திப் பெறப்படுகின்றன, இது ஒரு நிரலின் பண்புகள் பற்றிய முறைசார் பகுத்தறிவை அனுமதிக்கிறது. ஒரு நிரல் தர்க்கம் ஒரு நிரலின் எதிர்பார்க்கப்படும் நடத்தையை (கணித மொழியில்) வெளிப்படுத்தும் முறைசார் விதிகளைக் கொண்டுள்ளது. அணுகக்கூடிய தர்க்கம் (reachability logic) (opens in a new tab), கால தர்க்கம் (temporal logic) (opens in a new tab) மற்றும் ஹோர் தர்க்கம் (Hoare logic) (opens in a new tab) உள்ளிட்ட பல்வேறு நிரல் தர்க்கங்கள் முறைசார் விவரக்குறிப்புகளை உருவாக்குவதில் பயன்படுத்தப்படுகின்றன.
திறன் ஒப்பந்தங்களுக்கான முறைசார் விவரக்குறிப்புகளை உயர்மட்ட அல்லது கீழ்மட்ட விவரக்குறிப்புகள் எனப் பரவலாக வகைப்படுத்தலாம். ஒரு விவரக்குறிப்பு எந்த வகையைச் சேர்ந்தது என்பதைப் பொருட்படுத்தாமல், அது பகுப்பாய்வில் உள்ள அமைப்பின் பண்பைப் போதுமான அளவு மற்றும் சந்தேகத்திற்கு இடமின்றி விவரிக்க வேண்டும்.
உயர்மட்ட விவரக்குறிப்புகள்
பெயருக்கு ஏற்றாற்போல், ஒரு உயர்மட்ட விவரக்குறிப்பு ("மாதிரி சார்ந்த விவரக்குறிப்பு" என்றும் அழைக்கப்படுகிறது) ஒரு நிரலின் உயர்மட்ட நடத்தையை விவரிக்கிறது. உயர்மட்ட விவரக்குறிப்புகள் ஒரு திறன் ஒப்பந்தத்தை வரையறுக்கப்பட்ட நிலை இயந்திரமாக (opens in a new tab) (FSM) மாதிரியாக்குகின்றன, இது செயல்பாடுகளைச் செய்வதன் மூலம் நிலைகளுக்கு இடையில் மாறலாம், FSM மாதிரிக்கான முறைசார் பண்புகளை வரையறுக்கக் கால தர்க்கம் பயன்படுத்தப்படுகிறது.
கால தர்க்கங்கள் (opens in a new tab) என்பவை "நேரத்தின் அடிப்படையில் தகுதிபெற்ற முன்மொழிவுகளைப் பற்றி நியாயப்படுத்துவதற்கான விதிகள் (எ.கா., "நான் எப்போதும் பசியுடன் இருக்கிறேன்" அல்லது "நான் இறுதியில் பசியுடன் இருப்பேன்")." முறைசார் சரிபார்ப்பிற்குப் பயன்படுத்தப்படும்போது, நிலை-இயந்திரங்களாக மாதிரியாக்கப்பட்ட அமைப்புகளின் சரியான நடத்தை பற்றிய உறுதிப்படுத்தல்களைக் கூற கால தர்க்கங்கள் பயன்படுத்தப்படுகின்றன. குறிப்பாக, ஒரு கால தர்க்கம் ஒரு திறன் ஒப்பந்தம் இருக்கக்கூடிய எதிர்கால நிலைகளையும் அது நிலைகளுக்கு இடையில் எவ்வாறு மாறுகிறது என்பதையும் விவரிக்கிறது.
உயர்மட்ட விவரக்குறிப்புகள் பொதுவாகத் திறன் ஒப்பந்தங்களுக்கான இரண்டு முக்கியமான காலப் பண்புகளைப் படம்பிடிக்கின்றன: பாதுகாப்பு மற்றும் உயிரோட்டம் (liveness). பாதுகாப்புப் பண்புகள் "எந்தவொரு கெட்டதும் நடக்காது" என்ற கருத்தைக் குறிக்கின்றன மற்றும் பொதுவாக மாறிலித்தன்மையை வெளிப்படுத்துகின்றன. ஒரு பாதுகாப்புப் பண்பு முட்டுக்கட்டையிலிருந்து (deadlock) (opens in a new tab) விடுபடுவது போன்ற பொதுவான மென்பொருள் தேவைகளை வரையறுக்கலாம் அல்லது ஒப்பந்தங்களுக்கான டொமைன்-குறிப்பிட்ட பண்புகளை வெளிப்படுத்தலாம் (எ.கா., சார்புகளுக்கான அணுகல் கட்டுப்பாட்டின் மாறிலிகள், நிலை மாறிகளின் அனுமதிக்கக்கூடிய மதிப்புகள் அல்லது வில்லைப் பரிமாற்றங்களுக்கான நிபந்தனைகள்).
ERC-20 வில்லை ஒப்பந்தங்களில் transfer() அல்லது transferFrom() ஐப் பயன்படுத்துவதற்கான நிபந்தனைகளை உள்ளடக்கிய இந்தப் பாதுகாப்புத் தேவையை எடுத்துக்காட்டாக எடுத்துக்கொள்ளுங்கள்: "அனுப்புநரின் இருப்பு அனுப்பக் கோரப்பட்ட வில்லைகளின் அளவை விடக் குறைவாக இருக்காது.". ஒரு ஒப்பந்த மாறிலியின் இந்த இயற்கை மொழி விளக்கத்தை ஒரு முறைசார் (கணித) விவரக்குறிப்பாக மொழிபெயர்க்கலாம், பின்னர் அது செல்லுபடியாகும் தன்மைக்காகக் கடுமையாகச் சரிபார்க்கப்படலாம்.
உயிரோட்டப் பண்புகள் "இறுதியில் ஏதோ நல்லது நடக்கும்" என்று உறுதிப்படுத்துகின்றன மற்றும் வெவ்வேறு நிலைகளில் முன்னேறும் ஒப்பந்தத்தின் திறனைப் பற்றியது. உயிரோட்டப் பண்பிற்கு ஒரு எடுத்துக்காட்டு "நீர்மைத்தன்மை", இது கோரிக்கையின் பேரில் பயனர்களுக்குத் தனது இருப்புகளைப் பரிமாற்றம் செய்யும் ஒப்பந்தத்தின் திறனைக் குறிக்கிறது. இந்தப் பண்பு மீறப்பட்டால், Parity பணப்பைச் சம்பவத்தில் (opens in a new tab) நடந்தது போல, ஒப்பந்தத்தில் சேமிக்கப்பட்டுள்ள சொத்துகளைப் பயனர்களால் திரும்பப் பெற முடியாது.
கீழ்மட்ட விவரக்குறிப்புகள்
உயர்மட்ட விவரக்குறிப்புகள் ஒரு ஒப்பந்தத்தின் வரையறுக்கப்பட்ட-நிலை மாதிரியைத் தொடக்கப் புள்ளியாக எடுத்துக்கொண்டு இந்த மாதிரியின் விரும்பிய பண்புகளை வரையறுக்கின்றன. இதற்கு மாறாக, கீழ்மட்ட விவரக்குறிப்புகள் ("பண்பு சார்ந்த விவரக்குறிப்புகள்" என்றும் அழைக்கப்படுகின்றன) பெரும்பாலும் நிரல்களை (திறன் ஒப்பந்தங்கள்) கணிதச் சார்புகளின் தொகுப்பைக் கொண்ட அமைப்புகளாக மாதிரியாக்குகின்றன மற்றும் அத்தகைய அமைப்புகளின் சரியான நடத்தையை விவரிக்கின்றன.
எளிமையான வார்த்தைகளில் கூறுவதானால், கீழ்மட்ட விவரக்குறிப்புகள் நிரல் தடயங்களை பகுப்பாய்வு செய்கின்றன மற்றும் இந்தத் தடயங்களில் ஒரு திறன் ஒப்பந்தத்தின் பண்புகளை வரையறுக்க முயற்சிக்கின்றன. தடயங்கள் என்பது ஒரு ஒப்பந்தத்தின் நிலையை மாற்றும் சார்புச் செயலாக்கங்களின் வரிசைகளைக் குறிக்கின்றன; எனவே, ஒரு ஒப்பந்தத்தின் உள் செயலாக்கத்திற்கான தேவைகளைக் குறிப்பிடக் கீழ்மட்ட விவரக்குறிப்புகள் உதவுகின்றன.
கீழ்மட்ட முறைசார் விவரக்குறிப்புகளை ஹோர்-பாணி பண்புகளாகவோ அல்லது செயலாக்கப் பாதைகளில் மாறிலிகளாகவோ கொடுக்கலாம்.
ஹோர்-பாணி பண்புகள்
ஹோர் தர்க்கம் (opens in a new tab) திறன் ஒப்பந்தங்கள் உட்பட நிரல்களின் சரியான தன்மை பற்றி நியாயப்படுத்துவதற்கான முறைசார் விதிகளின் தொகுப்பை வழங்குகிறது. ஒரு ஹோர்-பாணி பண்பு ஹோர் மும்மை {P}c{Q} மூலம் குறிக்கப்படுகிறது, இதில் c என்பது ஒரு நிரல் மற்றும் P மற்றும் Q என்பவை c இன் (அதாவது, நிரல்) நிலையின் மீதான முன்கணிப்புகள் ஆகும், இவை முறையே முன்நிபந்தனைகள் மற்றும் பின்நிபந்தனைகள் என முறைப்படி விவரிக்கப்படுகின்றன.
முன்நிபந்தனை என்பது ஒரு சார்பின் சரியான செயலாக்கத்திற்குத் தேவையான நிபந்தனைகளை விவரிக்கும் ஒரு முன்கணிப்பு ஆகும்; ஒப்பந்தத்தை அழைக்கும் பயனர்கள் இந்தத் தேவையைப் பூர்த்தி செய்ய வேண்டும். பின்நிபந்தனை என்பது ஒரு சார்பு சரியாகச் செயல்படுத்தப்பட்டால் அது நிறுவும் நிபந்தனையை விவரிக்கும் ஒரு முன்கணிப்பு ஆகும்; சார்பை அழைத்த பிறகு பயனர்கள் இந்த நிபந்தனை உண்மையாக இருக்கும் என்று எதிர்பார்க்கலாம். ஹோர் தர்க்கத்தில் ஒரு மாறிலி என்பது ஒரு சார்பின் செயலாக்கத்தால் பாதுகாக்கப்படும் (அதாவது, அது மாறாது) ஒரு முன்கணிப்பு ஆகும்.
ஹோர்-பாணி விவரக்குறிப்புகள் பகுதி சரியான தன்மை அல்லது முழுமையான சரியான தன்மை ஆகிய இரண்டில் ஒன்றுக்கு உத்தரவாதம் அளிக்க முடியும். சார்பு செயல்படுத்தப்படுவதற்கு முன்பு முன்நிபந்தனை உண்மையாக இருந்தால், மற்றும் செயலாக்கம் முடிவடைந்தால், பின்நிபந்தனையும் உண்மையாக இருந்தால், ஒரு ஒப்பந்தச் சார்பின் செயலாக்கம் "பகுதியளவு சரியானது". சார்பு செயல்படுவதற்கு முன்பு ஒரு முன்நிபந்தனை உண்மையாக இருந்தால், செயலாக்கம் முடிவடைவது உறுதிசெய்யப்பட்டு, அது முடிவடையும் போது, பின்நிபந்தனை உண்மையாக இருந்தால் முழுமையான சரியான தன்மைக்கான ஆதாரம் பெறப்படுகிறது.
சில செயலாக்கங்கள் முடிவடைவதற்கு முன்பு தாமதமாகலாம் அல்லது ஒருபோதும் முடிவடையாமல் போகலாம் என்பதால் முழுமையான சரியான தன்மைக்கான ஆதாரத்தைப் பெறுவது கடினம். எத்திரியத்தின் எரிவாயு பொறிமுறையானது எல்லையற்ற நிரல் சுழல்களைத் தடுப்பதால் (செயலாக்கம் வெற்றிகரமாக முடிவடைகிறது அல்லது 'எரிவாயு தீர்ந்துவிட்டது' பிழையால் முடிவடைகிறது) செயலாக்கம் முடிவடைகிறதா என்ற கேள்வி விவாதத்திற்குரியது.
ஹோர் தர்க்கத்தைப் பயன்படுத்தி உருவாக்கப்பட்ட திறன் ஒப்பந்த விவரக்குறிப்புகள் ஒரு ஒப்பந்தத்தில் சார்புகள் மற்றும் சுழல்களின் செயலாக்கத்திற்காக வரையறுக்கப்பட்ட முன்நிபந்தனைகள், பின்நிபந்தனைகள் மற்றும் மாறிலிகளைக் கொண்டிருக்கும். முன்நிபந்தனைகள் பெரும்பாலும் ஒரு சார்பிற்கான தவறான உள்ளீடுகளின் சாத்தியக்கூறுகளை உள்ளடக்குகின்றன, பின்நிபந்தனைகள் அத்தகைய உள்ளீடுகளுக்கு எதிர்பார்க்கப்படும் பதிலளிப்பை விவரிக்கின்றன (எ.கா., ஒரு குறிப்பிட்ட விதிவிலக்கை எறிதல்). இந்த முறையில் ஒப்பந்தச் செயலாக்கங்களின் சரியான தன்மையை உறுதிப்படுத்த ஹோர்-பாணி பண்புகள் பயனுள்ளதாக இருக்கும்.
பல முறைசார் சரிபார்ப்பு கட்டமைப்புகள் சார்புகளின் சொற்பொருள் சரியான தன்மையை நிரூபிக்க ஹோர்-பாணி விவரக்குறிப்புகளைப் பயன்படுத்துகின்றன. Solidity இல் require மற்றும் assert அறிக்கைகளைப் பயன்படுத்துவதன் மூலம் ஹோர்-பாணி பண்புகளை (உறுதிப்படுத்தல்களாக) நேரடியாக ஒப்பந்தக் குறியீட்டில் சேர்க்க முடியும்.
require அறிக்கைகள் ஒரு முன்நிபந்தனை அல்லது மாறிலியை வெளிப்படுத்துகின்றன மற்றும் பெரும்பாலும் பயனர் உள்ளீடுகளைச் சரிபார்க்கப் பயன்படுத்தப்படுகின்றன, அதே நேரத்தில் assert பாதுகாப்பிற்குத் தேவையான பின்நிபந்தனையைப் படம்பிடிக்கிறது. எடுத்துக்காட்டாக, அழைக்கும் கணக்கின் அடையாளத்தின் மீதான முன்நிபந்தனைச் சரிபார்ப்பாக require ஐப் பயன்படுத்துவதன் மூலம் சார்புகளுக்கான சரியான அணுகல் கட்டுப்பாட்டை (பாதுகாப்புப் பண்பின் எடுத்துக்காட்டு) அடையலாம். இதேபோல், ஒரு ஒப்பந்தத்தில் உள்ள நிலை மாறிகளின் அனுமதிக்கக்கூடிய மதிப்புகளின் மீதான மாறிலியை (எ.கா., புழக்கத்தில் உள்ள வில்லைகளின் மொத்த எண்ணிக்கை) சார்புச் செயலாக்கத்திற்குப் பிறகு ஒப்பந்தத்தின் நிலையை உறுதிப்படுத்த assert ஐப் பயன்படுத்துவதன் மூலம் மீறலில் இருந்து பாதுகாக்க முடியும்.
தடய-நிலை பண்புகள்
தடய அடிப்படையிலான விவரக்குறிப்புகள் ஒரு ஒப்பந்தத்தை வெவ்வேறு நிலைகளுக்கு இடையில் மாற்றும் செயல்பாடுகளையும் இந்தச் செயல்பாடுகளுக்கு இடையிலான உறவுகளையும் விவரிக்கின்றன. முன்னரே விளக்கியபடி, தடயங்கள் என்பது ஒரு ஒப்பந்தத்தின் நிலையை ஒரு குறிப்பிட்ட வழியில் மாற்றும் செயல்பாடுகளின் வரிசைகளாகும்.
இந்த அணுகுமுறை திறன் ஒப்பந்தங்களின் மாதிரியை முன்வரையறுக்கப்பட்ட மாற்றங்களின் தொகுப்புடன் (ஒப்பந்தச் சார்புகளால் விவரிக்கப்படுகிறது) சில முன்வரையறுக்கப்பட்ட நிலைகளுடன் (நிலை மாறிகளால் விவரிக்கப்படுகிறது) நிலை-மாற்ற அமைப்புகளாக நம்பியுள்ளது. மேலும், ஒரு நிரலின் செயலாக்க ஓட்டத்தின் வரைகலை பிரதிநிதித்துவமான கட்டுப்பாட்டு ஓட்ட வரைபடம் (opens in a new tab) (CFG), பெரும்பாலும் ஒரு ஒப்பந்தத்தின் செயல்பாட்டுச் சொற்பொருளை விவரிக்கப் பயன்படுத்தப்படுகிறது. இங்கே, ஒவ்வொரு தடயமும் கட்டுப்பாட்டு ஓட்ட வரைபடத்தில் ஒரு பாதையாகக் குறிக்கப்படுகிறது.
முதன்மையாக, திறன் ஒப்பந்தங்களில் உள் செயலாக்கத்தின் வடிவங்களைப் பற்றி நியாயப்படுத்தத் தடய-நிலை விவரக்குறிப்புகள் பயன்படுத்தப்படுகின்றன. தடய-நிலை விவரக்குறிப்புகளை உருவாக்குவதன் மூலம், ஒரு திறன் ஒப்பந்தத்திற்கான அனுமதிக்கக்கூடிய செயலாக்கப் பாதைகளை (அதாவது, நிலை மாற்றங்கள்) நாங்கள் உறுதிப்படுத்துகிறோம். குறியீட்டுச் செயலாக்கம் போன்ற நுட்பங்களைப் பயன்படுத்தி, முறைசார் மாதிரியில் வரையறுக்கப்படாத பாதையைச் செயலாக்கம் ஒருபோதும் பின்பற்றாது என்பதை நாம் முறைப்படி சரிபார்க்கலாம்.
தடய-நிலை பண்புகளை விவரிக்கப் பொதுவில் அணுகக்கூடிய சில சார்புகளைக் கொண்ட DAO ஒப்பந்தத்தின் எடுத்துக்காட்டைப் பயன்படுத்துவோம். இங்கே, DAO ஒப்பந்தம் பயனர்களைப் பின்வரும் செயல்பாடுகளைச் செய்ய அனுமதிக்கிறது என்று கருதுகிறோம்:
-
நிதியை வைப்பிலிடுதல்
-
நிதியை வைப்பிலிட்ட பிறகு ஒரு முன்மொழிவுக்கு வாக்களித்தல்
-
அவர்கள் ஒரு முன்மொழிவுக்கு வாக்களிக்கவில்லை என்றால் பணத்தைத் திரும்பப் பெற உரிமைக்கோரல்
எடுத்துக்காட்டுத் தடய-நிலை பண்புகள் "நிதியை வைப்பிலிடாத பயனர்கள் ஒரு முன்மொழிவுக்கு வாக்களிக்க முடியாது" அல்லது "ஒரு முன்மொழிவுக்கு வாக்களிக்காத பயனர்கள் எப்போதும் பணத்தைத் திரும்பப் பெற உரிமைக்கோர முடியும்" என்பதாக இருக்கலாம். இரண்டு பண்புகளும் விருப்பமான செயலாக்க வரிசைகளை உறுதிப்படுத்துகின்றன (நிதியை வைப்பிலிடுவதற்கு முன்பு வாக்களிப்பது நடக்க முடியாது மற்றும் ஒரு முன்மொழிவுக்கு வாக்களித்த பிறகு பணத்தைத் திரும்பப் பெற உரிமைக்கோருவது நடக்க முடியாது).
திறன் ஒப்பந்தங்களின் முறைசார் சரிபார்ப்பிற்கான நுட்பங்கள்
மாதிரிச் சரிபார்ப்பு
மாதிரிச் சரிபார்ப்பு என்பது ஒரு முறைசார் சரிபார்ப்பு நுட்பமாகும், இதில் ஒரு வழிமுறை ஒரு திறன் ஒப்பந்தத்தின் முறைசார் மாதிரியை அதன் விவரக்குறிப்புக்கு எதிராகச் சரிபார்க்கிறது. மாதிரிச் சரிபார்ப்பில் திறன் ஒப்பந்தங்கள் பெரும்பாலும் நிலை-மாற்ற அமைப்புகளாகக் குறிக்கப்படுகின்றன, அதே நேரத்தில் அனுமதிக்கக்கூடிய ஒப்பந்த நிலைகளின் பண்புகள் கால தர்க்கத்தைப் பயன்படுத்தி வரையறுக்கப்படுகின்றன.
மாதிரிச் சரிபார்ப்பிற்கு ஒரு அமைப்பின் (அதாவது, ஒரு ஒப்பந்தம்) சுருக்கமான கணிதப் பிரதிநிதித்துவத்தை உருவாக்குவது மற்றும் முன்மொழிவு தர்க்கத்தில் (propositional logic) (opens in a new tab) வேரூன்றிய சூத்திரங்களைப் பயன்படுத்தி இந்த அமைப்பின் பண்புகளை வெளிப்படுத்துவது தேவைப்படுகிறது. இது மாதிரிச் சரிபார்ப்பு வழிமுறையின் பணியை எளிதாக்குகிறது, அதாவது ஒரு கணித மாதிரி கொடுக்கப்பட்ட தர்க்கரீதியான சூத்திரத்தைப் பூர்த்தி செய்கிறது என்பதை நிரூபிக்கிறது.
முறைசார் சரிபார்ப்பில் மாதிரிச் சரிபார்ப்பு முதன்மையாகக் காலப்போக்கில் ஒரு ஒப்பந்தத்தின் நடத்தையை விவரிக்கும் காலப் பண்புகளை மதிப்பிடப் பயன்படுத்தப்படுகிறது. திறன் ஒப்பந்தங்களுக்கான காலப் பண்புகளில் பாதுகாப்பு மற்றும் உயிரோட்டம் ஆகியவை அடங்கும், இவற்றை நாங்கள் முன்னரே விளக்கினோம்.
எடுத்துக்காட்டாக, அணுகல் கட்டுப்பாடு தொடர்பான பாதுகாப்புப் பண்பை (எ.கா., ஒப்பந்தத்தின் உரிமையாளர் மட்டுமே selfdestruct ஐ அழைக்க முடியும்) முறைசார் தர்க்கத்தில் எழுதலாம். அதன்பிறகு, ஒப்பந்தம் இந்த முறைசார் விவரக்குறிப்பைப் பூர்த்தி செய்கிறதா என்பதை மாதிரிச் சரிபார்ப்பு வழிமுறை சரிபார்க்கலாம்.
மாதிரிச் சரிபார்ப்பு நிலை வெளி ஆய்வைப் பயன்படுத்துகிறது, இது ஒரு திறன் ஒப்பந்தத்தின் சாத்தியமான அனைத்து நிலைகளையும் உருவாக்குவது மற்றும் பண்பு மீறல்களை ஏற்படுத்தும் அடையக்கூடிய நிலைகளைக் கண்டறிய முயற்சிப்பது ஆகியவற்றை உள்ளடக்கியது. இருப்பினும், இது எண்ணற்ற நிலைகளுக்கு வழிவகுக்கும் ("நிலை வெடிப்புச் சிக்கல்" என்று அழைக்கப்படுகிறது), எனவே திறன் ஒப்பந்தங்களின் திறமையான பகுப்பாய்வைச் சாத்தியமாக்க மாதிரிச் சரிபார்ப்பவர்கள் சுருக்க நுட்பங்களை நம்பியுள்ளனர்.
தேற்றம் நிரூபித்தல்
தேற்றம் நிரூபித்தல் என்பது திறன் ஒப்பந்தங்கள் உட்பட நிரல்களின் சரியான தன்மை பற்றி கணித ரீதியாக நியாயப்படுத்தும் ஒரு முறையாகும். இது ஒரு ஒப்பந்த அமைப்பின் மாதிரி மற்றும் அதன் விவரக்குறிப்புகளைக் கணிதச் சூத்திரங்களாக (தர்க்க அறிக்கைகள்) மாற்றுவதை உள்ளடக்கியது.
தேற்றம் நிரூபிப்பதன் நோக்கம் இந்த அறிக்கைகளுக்கு இடையிலான தர்க்கரீதியான சமநிலையைச் சரிபார்ப்பதாகும். "தர்க்கரீதியான சமநிலை" ("தர்க்கரீதியான இரு-உட்குறிப்பு" என்றும் அழைக்கப்படுகிறது) என்பது இரண்டு அறிக்கைகளுக்கு இடையிலான ஒரு வகையான உறவாகும், அதாவது இரண்டாவது அறிக்கை உண்மையாக இருந்தால் மற்றும் இருந்தால் மட்டுமே முதல் அறிக்கை உண்மையாக இருக்கும்.
ஒரு ஒப்பந்தத்தின் மாதிரி மற்றும் அதன் பண்பு பற்றிய அறிக்கைகளுக்கு இடையிலான தேவையான உறவு (தர்க்கரீதியான சமநிலை) நிரூபிக்கக்கூடிய அறிக்கையாக (தேற்றம் என்று அழைக்கப்படுகிறது) உருவாக்கப்படுகிறது. அனுமானத்தின் முறைசார் அமைப்பைப் பயன்படுத்தி, தானியங்கு தேற்றம் நிரூபிப்பவர் தேற்றத்தின் செல்லுபடியாகும் தன்மையைச் சரிபார்க்க முடியும். வேறு வார்த்தைகளில் கூறுவதானால், ஒரு திறன் ஒப்பந்தத்தின் மாதிரி அதன் விவரக்குறிப்புகளுடன் துல்லியமாகப் பொருந்துகிறது என்பதை ஒரு தேற்றம் நிரூபிப்பவர் உறுதியாக நிரூபிக்க முடியும்.
மாதிரிச் சரிபார்ப்பு ஒப்பந்தங்களை வரையறுக்கப்பட்ட நிலைகளைக் கொண்ட மாற்ற அமைப்புகளாக மாதிரியாக்கும் அதே வேளையில், தேற்றம் நிரூபித்தல் எல்லையற்ற-நிலை அமைப்புகளின் பகுப்பாய்வைக் கையாள முடியும். இருப்பினும், ஒரு தர்க்கச் சிக்கல் "தீர்மானிக்கக்கூடியதா" இல்லையா என்பதைத் தானியங்கு தேற்றம் நிரூபிப்பவர் எப்போதும் அறிய முடியாது என்பதே இதன் பொருளாகும்.
இதன் விளைவாக, சரியான தன்மைக்கான ஆதாரங்களைப் பெறுவதில் தேற்றம் நிரூபிப்பவரை வழிநடத்த மனித உதவி பெரும்பாலும் தேவைப்படுகிறது. தேற்றம் நிரூபிப்பதில் மனித முயற்சியைப் பயன்படுத்துவது, முழுமையாகத் தானியங்குபடுத்தப்பட்ட மாதிரிச் சரிபார்ப்பை விடப் பயன்படுத்துவதற்கு அதிகச் செலவுமிக்கதாக ஆக்குகிறது.
குறியீட்டுச் செயலாக்கம்
குறியீட்டுச் செயலாக்கம் என்பது திட்டவட்டமான மதிப்புகளுக்கு (எ.கா., x == 5) பதிலாக குறியீட்டு மதிப்புகளைப் (எ.கா., x > 5) பயன்படுத்திச் சார்புகளைச் செயல்படுத்துவதன் மூலம் ஒரு திறன் ஒப்பந்தத்தைப் பகுப்பாய்வு செய்யும் முறையாகும். ஒரு முறைசார் சரிபார்ப்பு நுட்பமாக, ஒரு ஒப்பந்தத்தின் குறியீட்டில் உள்ள தடய-நிலை பண்புகளைப் பற்றி முறைப்படி நியாயப்படுத்தக் குறியீட்டுச் செயலாக்கம் பயன்படுத்தப்படுகிறது.
குறியீட்டுச் செயலாக்கம் ஒரு செயலாக்கத் தடயத்தைக் குறியீட்டு உள்ளீட்டு மதிப்புகளின் மீதான கணிதச் சூத்திரமாகக் குறிக்கிறது, இது பாதை முன்கணிப்பு என்று அழைக்கப்படுகிறது. ஒரு பாதை முன்கணிப்பு "திருப்திகரமானதா" (அதாவது, சூத்திரத்தைப் பூர்த்தி செய்யக்கூடிய ஒரு மதிப்பு உள்ளதா) என்பதைச் சரிபார்க்க ஒரு SMT தீர்ப்பான் (opens in a new tab) பயன்படுத்தப்படுகிறது. பாதிக்கப்படக்கூடிய பாதை திருப்திகரமாக இருந்தால், SMT தீர்ப்பான் அந்தப் பாதையை நோக்கிச் செயலாக்கத்தைத் தூண்டும் ஒரு திட்டவட்டமான மதிப்பை உருவாக்கும்.
ஒரு திறன் ஒப்பந்தத்தின் சார்பு ஒரு uint மதிப்பை (x) உள்ளீடாக எடுத்துக்கொள்கிறது மற்றும் x ஆனது 5 ஐ விட அதிகமாகவும் 10 ஐ விடக் குறைவாகவும் இருக்கும்போது திரும்பப் பெறுகிறது என்று வைத்துக்கொள்வோம். ஒரு சாதாரணச் சோதனை நடைமுறையைப் பயன்படுத்திப் பிழையைத் தூண்டும் x க்கான மதிப்பைக் கண்டறிவதற்கு, பிழையைத் தூண்டும் உள்ளீட்டை உண்மையில் கண்டறிவதற்கான உத்தரவாதம் இல்லாமல் டஜன் கணக்கான சோதனை நிகழ்வுகளை (அல்லது அதற்கு மேற்பட்டவை) இயக்க வேண்டும்.
மாறாக, ஒரு குறியீட்டுச் செயலாக்கக் கருவி குறியீட்டு மதிப்புடன் சார்பைச் செயல்படுத்தும்: X > 5 ∧ X < 10 (அதாவது, x ஆனது 5 ஐ விடப் பெரியது மற்றும் x ஆனது 10 ஐ விடச் சிறியது). தொடர்புடைய பாதை முன்கணிப்பு x = X > 5 ∧ X < 10 பின்னர் தீர்க்க ஒரு SMT தீர்ப்பானுக்கு வழங்கப்படும். ஒரு குறிப்பிட்ட மதிப்பு x = X > 5 ∧ X < 10 சூத்திரத்தைப் பூர்த்தி செய்தால், SMT தீர்ப்பான் அதைக் கணக்கிடும்—எடுத்துக்காட்டாக, தீர்ப்பான் x க்கான மதிப்பாக 7 ஐ உருவாக்கலாம்.
குறியீட்டுச் செயலாக்கம் ஒரு நிரலுக்கான உள்ளீடுகளை நம்பியிருப்பதாலும், அடையக்கூடிய அனைத்து நிலைகளையும் ஆராய்வதற்கான உள்ளீடுகளின் தொகுப்பு எல்லையற்றதாக இருப்பதாலும், இது இன்னும் ஒரு வகையான சோதனையாகவே உள்ளது. இருப்பினும், எடுத்துக்காட்டில் காட்டப்பட்டுள்ளபடி, பண்பு மீறல்களைத் தூண்டும் உள்ளீடுகளைக் கண்டறிவதற்கு வழக்கமான சோதனையை விடக் குறியீட்டுச் செயலாக்கம் மிகவும் திறமையானது.
மேலும், ஒரு சார்புக்குத் தோராயமாக உள்ளீடுகளை உருவாக்கும் பிற பண்பு அடிப்படையிலான நுட்பங்களை (எ.கா., ஃபஸ்ஸிங்) விடக் குறியீட்டுச் செயலாக்கம் குறைவான தவறான நேர்மறைகளை (false positives) உருவாக்குகிறது. குறியீட்டுச் செயலாக்கத்தின் போது ஒரு பிழை நிலை தூண்டப்பட்டால், பிழையைத் தூண்டும் ஒரு திட்டவட்டமான மதிப்பை உருவாக்கிச் சிக்கலை மீண்டும் உருவாக்க முடியும்.
குறியீட்டுச் செயலாக்கம் சரியான தன்மைக்கான சில அளவிலான கணித ஆதாரத்தையும் வழங்க முடியும். அளவுமீறல் பாதுகாப்புடன் கூடிய ஒப்பந்தச் சார்பின் பின்வரும் எடுத்துக்காட்டைக் கவனியுங்கள்:
function safe_add(uint x, uint y) returns(uint z){
z = x + y;
require(z>=x);
require(z>=y);
return z;
}
முழு எண் அளவுமீறலை ஏற்படுத்தும் ஒரு செயலாக்கத் தடயம் சூத்திரத்தைப் பூர்த்தி செய்ய வேண்டும்: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) அத்தகைய சூத்திரம் தீர்க்கப்படுவது சாத்தியமில்லை, எனவே safe_add சார்பு ஒருபோதும் அளவுமீறாது என்பதற்கான கணித ஆதாரமாக இது செயல்படுகிறது.
திறன் ஒப்பந்தங்களுக்கு முறைசார் சரிபார்ப்பை ஏன் பயன்படுத்த வேண்டும்?
நம்பகத்தன்மையின் தேவை
இறப்பு, காயம் அல்லது நிதி அழிவு போன்ற பேரழிவு விளைவுகளை ஏற்படுத்தக்கூடிய பாதுகாப்பு-முக்கியமான அமைப்புகளின் சரியான தன்மையை மதிப்பிட முறைசார் சரிபார்ப்பு பயன்படுத்தப்படுகிறது. திறன் ஒப்பந்தங்கள் மகத்தான அளவிலான மதிப்பைக் கட்டுப்படுத்தும் அதிக மதிப்புள்ள செயலிகளாகும், மேலும் வடிவமைப்பில் உள்ள எளிய பிழைகள் பயனர்களுக்கு மீளமுடியாத இழப்புகளுக்கு (opens in a new tab) வழிவகுக்கும். இருப்பினும், நிலைநிறுத்தத்திற்கு முன்பு ஒரு ஒப்பந்தத்தை முறைப்படி சரிபார்ப்பது, அது தொகுதிச்சங்கிலியில் இயங்கியவுடன் எதிர்பார்த்தபடி செயல்படும் என்பதற்கான உத்தரவாதங்களை அதிகரிக்கலாம்.
எந்தவொரு திறன் ஒப்பந்தத்திலும் நம்பகத்தன்மை என்பது மிகவும் விரும்பப்படும் தரமாகும், குறிப்பாக எத்திரியம் மெய்நிகர் இயந்திரத்தில் (EVM) நிலைநிறுத்தப்பட்ட குறியீடு பொதுவாக மாற்றவியலாதது என்பதால். வெளியீட்டிற்குப் பிந்தைய மேம்படுத்தல்களை எளிதில் அணுக முடியாத நிலையில், ஒப்பந்தங்களின் நம்பகத்தன்மைக்கு உத்தரவாதம் அளிக்க வேண்டிய தேவை முறைசார் சரிபார்ப்பை அவசியமாக்குகிறது. தணிக்கையாளர்கள் மற்றும் சோதனையாளர்களைத் தாண்டிச் செல்லக்கூடிய முழு எண் குறைவு மற்றும் அளவுமீறல், மறு-நுழைவு மற்றும் மோசமான எரிவாயு மேம்படுத்தல்கள் போன்ற தந்திரமான சிக்கல்களை முறைசார் சரிபார்ப்பால் கண்டறிய முடியும்.
செயல்பாட்டுச் சரியான தன்மையை நிரூபித்தல்
ஒரு திறன் ஒப்பந்தம் சில தேவைகளைப் பூர்த்தி செய்கிறது என்பதை நிரூபிப்பதற்கான மிகவும் பொதுவான முறை நிரல் சோதனையாகும். இது ஒரு ஒப்பந்தம் கையாள எதிர்பார்க்கப்படும் தரவின் மாதிரியுடன் அதைச் செயல்படுத்துவது மற்றும் அதன் நடத்தையைப் பகுப்பாய்வு செய்வது ஆகியவற்றை உள்ளடக்கியது. மாதிரித் தரவிற்கான எதிர்பார்க்கப்படும் முடிவுகளை ஒப்பந்தம் வழங்கினால், உருவாக்குநர்கள் அதன் சரியான தன்மைக்கான புறநிலை ஆதாரத்தைக் கொண்டுள்ளனர்.
இருப்பினும், மாதிரியின் பகுதியாக இல்லாத உள்ளீட்டு மதிப்புகளுக்கான சரியான செயலாக்கத்தை இந்த அணுகுமுறையால் நிரூபிக்க முடியாது. எனவே, ஒரு ஒப்பந்தத்தைச் சோதிப்பது பிழைகளைக் கண்டறிய உதவலாம் (அதாவது, செயலாக்கத்தின் போது சில குறியீட்டுப் பாதைகள் விரும்பிய முடிவுகளை வழங்கத் தவறினால்), ஆனால் பிழைகள் இல்லை என்பதை அதனால் உறுதியாக நிரூபிக்க முடியாது.
மாறாக, ஒப்பந்தத்தை இயக்காமலேயே எல்லையற்ற செயலாக்கங்களுக்கான தேவைகளை ஒரு திறன் ஒப்பந்தம் பூர்த்தி செய்கிறது என்பதை முறைசார் சரிபார்ப்பு முறைப்படி நிரூபிக்க முடியும். இதற்குச் சரியான ஒப்பந்த நடத்தைகளைத் துல்லியமாக விவரிக்கும் முறைசார் விவரக்குறிப்பை உருவாக்குவது மற்றும் ஒப்பந்த அமைப்பின் முறைசார் (கணித) மாதிரியை உருவாக்குவது தேவைப்படுகிறது. பின்னர் ஒப்பந்தத்தின் மாதிரிக்கும் அதன் விவரக்குறிப்புக்கும் இடையிலான நிலைத்தன்மையைச் சரிபார்க்க முறைசார் ஆதார நடைமுறையை நாம் பின்பற்றலாம்.
முறைசார் சரிபார்ப்பின் மூலம், ஒரு ஒப்பந்தத்தின் வணிக தர்க்கம் தேவைகளைப் பூர்த்தி செய்கிறதா என்பதைச் சரிபார்க்கும் கேள்வி என்பது நிரூபிக்கப்படக்கூடிய அல்லது நிராகரிக்கப்படக்கூடிய ஒரு கணித முன்மொழிவாகும். ஒரு முன்மொழிவை முறைப்படி நிரூபிப்பதன் மூலம், வரையறுக்கப்பட்ட படிகளுடன் எண்ணற்ற சோதனை நிகழ்வுகளை நாம் சரிபார்க்கலாம். இந்த முறையில் ஒரு விவரக்குறிப்பைப் பொறுத்து ஒரு ஒப்பந்தம் செயல்பாட்டு ரீதியாகச் சரியானது என்பதை நிரூபிப்பதற்கான சிறந்த வாய்ப்புகளை முறைசார் சரிபார்ப்பு கொண்டுள்ளது.
சிறந்த சரிபார்ப்பு இலக்குகள்
ஒரு சரிபார்ப்பு இலக்கு முறைப்படி சரிபார்க்கப்பட வேண்டிய அமைப்பை விவரிக்கிறது. முறைசார் சரிபார்ப்பு "உட்பொதிக்கப்பட்ட அமைப்புகளில்" (ஒரு பெரிய அமைப்பின் பகுதியாக இருக்கும் சிறிய, எளிமையான மென்பொருள் துண்டுகள்) சிறப்பாகப் பயன்படுத்தப்படுகிறது. சில விதிகளைக் கொண்ட சிறப்பு டொமைன்களுக்கும் அவை சிறந்தவை, ஏனெனில் இது டொமைன்-குறிப்பிட்ட பண்புகளைச் சரிபார்ப்பதற்கான கருவிகளை மாற்றுவதை எளிதாக்குகிறது.
திறன் ஒப்பந்தங்கள்—குறைந்தபட்சம், ஓரளவிற்காவது—இரண்டு தேவைகளையும் பூர்த்தி செய்கின்றன. எடுத்துக்காட்டாக, எத்திரியம் ஒப்பந்தங்களின் சிறிய அளவு அவற்றை முறைசார் சரிபார்ப்புக்கு ஏற்றதாக ஆக்குகிறது. இதேபோல், EVM எளிய விதிகளைப் பின்பற்றுகிறது, இது EVM இல் இயங்கும் நிரல்களுக்கான சொற்பொருள் பண்புகளைக் குறிப்பிடுவதையும் சரிபார்ப்பதையும் எளிதாக்குகிறது.
வேகமான மேம்பாட்டுச் சுழற்சி
மாதிரிச் சரிபார்ப்பு மற்றும் குறியீட்டுச் செயலாக்கம் போன்ற முறைசார் சரிபார்ப்பு நுட்பங்கள் பொதுவாகத் திறன் ஒப்பந்தக் குறியீட்டின் வழக்கமான பகுப்பாய்வை விட (சோதனை அல்லது தணிக்கையின் போது செய்யப்படுகிறது) மிகவும் திறமையானவை. ஏனென்றால், திட்டவட்டமான மதிப்புகளைப் பயன்படுத்தும் சோதனையைப் போலல்லாமல் ("ஒரு பயனர் 5 ஈதரைத் திரும்பப் பெற முயற்சித்தால் என்ன செய்வது?"), உறுதிப்படுத்தல்களைச் சோதிக்க முறைசார் சரிபார்ப்பு குறியீட்டு மதிப்புகளை நம்பியுள்ளது ("ஒரு பயனர் n ஈதரைத் திரும்பப் பெற முயற்சித்தால் என்ன செய்வது?").
குறியீட்டு உள்ளீட்டு மாறிகள் பல வகுப்புகளின் திட்டவட்டமான மதிப்புகளை உள்ளடக்கும், எனவே முறைசார் சரிபார்ப்பு அணுகுமுறைகள் குறுகிய காலக்கட்டத்தில் அதிகக் குறியீட்டுத் கவரேஜை உறுதியளிக்கின்றன. திறம்படப் பயன்படுத்தப்படும்போது, முறைசார் சரிபார்ப்பு உருவாக்குநர்களுக்கான மேம்பாட்டுச் சுழற்சியை துரிதப்படுத்தலாம்.
விலையுயர்ந்த வடிவமைப்புப் பிழைகளைக் குறைப்பதன் மூலம் பரவலாக்கப்பட்ட செயலிகளை (dapps) உருவாக்கும் செயல்முறையையும் முறைசார் சரிபார்ப்பு மேம்படுத்துகிறது. பாதிப்புகளைச் சரிசெய்ய ஒப்பந்தங்களை மேம்படுத்துவதற்கு (சாத்தியமான இடங்களில்) குறியீட்டுத் தளங்களை விரிவாக மீண்டும் எழுதுவது மற்றும் மேம்பாட்டிற்கு அதிக முயற்சி செலவிடுவது தேவைப்படுகிறது. சோதனையாளர்கள் மற்றும் தணிக்கையாளர்களைத் தாண்டிச் செல்லக்கூடிய ஒப்பந்தச் செயலாக்கங்களில் உள்ள பல பிழைகளை முறைசார் சரிபார்ப்பால் கண்டறிய முடியும் மற்றும் ஒரு ஒப்பந்தத்தை நிலைநிறுத்துவதற்கு முன்பு அந்தச் சிக்கல்களைச் சரிசெய்யப் போதுமான வாய்ப்பை வழங்குகிறது.
முறைசார் சரிபார்ப்பின் குறைபாடுகள்
உடல் உழைப்பின் செலவு
முறைசார் சரிபார்ப்பு, குறிப்பாகச் சரியான தன்மைக்கான ஆதாரங்களைப் பெற ஒரு மனிதன் நிரூபிப்பவரை வழிநடத்தும் அரை-தானியங்கு சரிபார்ப்பிற்கு, கணிசமான உடல் உழைப்பு தேவைப்படுகிறது. மேலும், முறைசார் விவரக்குறிப்பை உருவாக்குவது என்பது உயர் மட்டத் திறன் தேவைப்படும் ஒரு சிக்கலான செயலாகும்.
இந்தக் காரணிகள் (முயற்சி மற்றும் திறன்) சோதனை மற்றும் தணிக்கைகள் போன்ற ஒப்பந்தங்களில் சரியான தன்மையை மதிப்பிடுவதற்கான வழக்கமான முறைகளுடன் ஒப்பிடும்போது முறைசார் சரிபார்ப்பை அதிகத் தேவையுள்ளதாகவும் செலவுமிக்கதாகவும் ஆக்குகின்றன. ஆயினும்கூட, திறன் ஒப்பந்தச் செயலாக்கங்களில் உள்ள பிழைகளின் விலையைக் கருத்தில் கொண்டு, முழுமையான சரிபார்ப்புத் தணிக்கைக்கான செலவைச் செலுத்துவது நடைமுறைக்குரியது.
தவறான எதிர்மறைகள் (False negatives)
திறன் ஒப்பந்தத்தின் செயலாக்கம் முறைசார் விவரக்குறிப்புடன் பொருந்துகிறதா என்பதை மட்டுமே முறைசார் சரிபார்ப்பால் சரிபார்க்க முடியும். எனவே, ஒரு திறன் ஒப்பந்தத்தின் எதிர்பார்க்கப்படும் நடத்தைகளை விவரக்குறிப்புச் சரியாக விவரிக்கிறதா என்பதை உறுதிப்படுத்துவது முக்கியம்.
விவரக்குறிப்புகள் மோசமாக எழுதப்பட்டிருந்தால், பண்புகளின் மீறல்களை—பாதிக்கப்படக்கூடிய செயலாக்கங்களைக் குறிக்கும்—முறைசார் சரிபார்ப்புத் தணிக்கையால் கண்டறிய முடியாது. இந்த நிலையில், ஒப்பந்தம் பிழையற்றது என்று ஒரு உருவாக்குநர் தவறாகக் கருதலாம்.
செயல்திறன் சிக்கல்கள்
முறைசார் சரிபார்ப்பு பல செயல்திறன் சிக்கல்களைச் சந்திக்கிறது. எடுத்துக்காட்டாக, மாதிரிச் சரிபார்ப்பு மற்றும் குறியீட்டுச் சரிபார்ப்பின் போது முறையே எதிர்கொள்ளப்படும் நிலை மற்றும் பாதை வெடிப்புச் சிக்கல்கள் சரிபார்ப்பு நடைமுறைகளைப் பாதிக்கலாம். மேலும், முறைசார் சரிபார்ப்புக் கருவிகள் பெரும்பாலும் SMT தீர்ப்பான்கள் மற்றும் பிற கட்டுப்பாட்டுத் தீர்ப்பான்களை அவற்றின் அடிப்படை அடுக்கில் பயன்படுத்துகின்றன, மேலும் இந்தத் தீர்ப்பான்கள் கணக்கீட்டு ரீதியாகத் தீவிரமான நடைமுறைகளை நம்பியுள்ளன.
மேலும், ஒரு பண்பு (தர்க்கரீதியான சூத்திரமாக விவரிக்கப்பட்டுள்ளது) திருப்திப்படுத்தப்பட முடியுமா இல்லையா என்பதை நிரல் சரிபார்ப்பவர்கள் தீர்மானிப்பது எப்போதும் சாத்தியமில்லை ("தீர்மானிக்கக்கூடிய சிக்கல் (opens in a new tab)") ஏனெனில் ஒரு நிரல் ஒருபோதும் முடிவடையாமல் போகலாம். எனவே, ஒரு ஒப்பந்தம் நன்கு குறிப்பிடப்பட்டிருந்தாலும் அதற்கான சில பண்புகளை நிரூபிப்பது சாத்தியமற்றதாக இருக்கலாம்.
எத்திரியம் திறன் ஒப்பந்தங்களுக்கான முறைசார் சரிபார்ப்புக் கருவிகள்
முறைசார் விவரக்குறிப்புகளை உருவாக்குவதற்கான விவரக்குறிப்பு மொழிகள்
Act: சேமிப்பகப் புதுப்பிப்புகள், முன்/பின் நிபந்தனைகள் மற்றும் ஒப்பந்த மாறிலிகளின் விவரக்குறிப்பை Act அனுமதிக்கிறது. இதன் கருவித் தொகுப்பு Coq, SMT தீர்ப்பான்கள் அல்லது hevm வழியாகப் பல பண்புகளை நிரூபிக்கக்கூடிய ஆதாரப் பின்தளங்களையும் கொண்டுள்ளது.
Scribble - Scribble விவரக்குறிப்பு மொழியில் உள்ள குறியீட்டுக் குறிப்புகளை விவரக்குறிப்பைச் சரிபார்க்கும் திட்டவட்டமான உறுதிப்படுத்தல்களாக Scribble மாற்றுகிறது.
Dafny - Dafny என்பது சரிபார்ப்புக்குத் தயாராக உள்ள நிரலாக்க மொழியாகும், இது குறியீட்டின் சரியான தன்மையைப் பற்றி நியாயப்படுத்தவும் நிரூபிக்கவும் உயர்மட்டக் குறிப்புகளை நம்பியுள்ளது.
சரியான தன்மையைச் சரிபார்ப்பதற்கான நிரல் சரிபார்ப்பவர்கள்
Certora Prover - Certora Prover என்பது திறன் ஒப்பந்தங்களில் குறியீட்டின் சரியான தன்மையைச் சரிபார்ப்பதற்கான ஒரு தானியங்கி முறைசார் சரிபார்ப்புக் கருவியாகும். விவரக்குறிப்புகள் CVL (Certora Verification Language) இல் எழுதப்பட்டுள்ளன, நிலையான பகுப்பாய்வு மற்றும் கட்டுப்பாட்டுத் தீர்வு ஆகியவற்றின் கலவையைப் பயன்படுத்திப் பண்பு மீறல்கள் கண்டறியப்படுகின்றன.
Solidity SMTChecker - Solidity இன் SMTChecker என்பது SMT (Satisfiability Modulo Theories) மற்றும் ஹார்ன் தீர்வு (Horn solving) ஆகியவற்றை அடிப்படையாகக் கொண்ட ஒரு உள்ளமைக்கப்பட்ட மாதிரிச் சரிபார்ப்பாகும். தொகுப்பின் போது ஒரு ஒப்பந்தத்தின் மூலக் குறியீடு விவரக்குறிப்புகளுடன் பொருந்துகிறதா என்பதை இது உறுதிப்படுத்துகிறது மற்றும் பாதுகாப்புப் பண்புகளின் மீறல்களை நிலையாகச் சரிபார்க்கிறது.
solc-verify - solc-verify என்பது Solidity தொகுப்பியின் நீட்டிக்கப்பட்ட பதிப்பாகும், இது குறிப்புகள் மற்றும் மட்டு நிரல் சரிபார்ப்பைப் பயன்படுத்தி Solidity குறியீட்டில் தானியங்கு முறைசார் சரிபார்ப்பைச் செய்ய முடியும்.
KEVM - KEVM என்பது K கட்டமைப்பில் எழுதப்பட்ட எத்திரியம் மெய்நிகர் இயந்திரத்தின் (EVM) முறைசார் சொற்பொருளாகும். KEVM செயல்படுத்தக்கூடியது மற்றும் அணுகக்கூடிய தர்க்கத்தைப் பயன்படுத்திச் சில பண்பு தொடர்பான உறுதிப்படுத்தல்களை நிரூபிக்க முடியும்.
தேற்றம் நிரூபிப்பதற்கான தர்க்கரீதியான கட்டமைப்புகள்
Isabelle - Isabelle/HOL என்பது கணிதச் சூத்திரங்களை ஒரு முறைசார் மொழியில் வெளிப்படுத்த அனுமதிக்கும் மற்றும் அந்தச் சூத்திரங்களை நிரூபிப்பதற்கான கருவிகளை வழங்கும் ஒரு ஆதார உதவியாளராகும். கணித ஆதாரங்களை முறைப்படுத்துவது மற்றும் குறிப்பாக முறைசார் சரிபார்ப்பு ஆகியவை இதன் முக்கியப் பயன்பாடாகும், இதில் கணினி வன்பொருள் அல்லது மென்பொருளின் சரியான தன்மையை நிரூபிப்பது மற்றும் கணினி மொழிகள் மற்றும் நெறிமுறைகளின் பண்புகளை நிரூபிப்பது ஆகியவை அடங்கும்.
Rocq - Rocq என்பது ஒரு ஊடாடும் தேற்றம் நிரூபிப்பவராகும், இது தேற்றங்களைப் பயன்படுத்தி நிரல்களை வரையறுக்கவும் மற்றும் இயந்திரத்தால் சரிபார்க்கப்பட்ட சரியான தன்மைக்கான ஆதாரங்களை ஊடாடும் வகையில் உருவாக்கவும் உங்களை அனுமதிக்கிறது.
திறன் ஒப்பந்தங்களில் பாதிக்கப்படக்கூடிய வடிவங்களைக் கண்டறிவதற்கான குறியீட்டுச் செயலாக்க அடிப்படையிலான கருவிகள்
மேண்டிகோர் - குறியீட்டுச் செயலாக்கத்தின் அடிப்படையில் EVM பைட் குறியீட்டைப் பகுப்பாய்வு செய்வதற்கான ஒரு கருவி.
hevm - hevm என்பது EVM பைட் குறியீட்டிற்கான ஒரு குறியீட்டுச் செயலாக்க இயந்திரம் மற்றும் சமநிலைச் சரிபார்ப்பாகும்.
Mythril - எத்திரியம் திறன் ஒப்பந்தங்களில் உள்ள பாதிப்புகளைக் கண்டறிவதற்கான ஒரு குறியீட்டுச் செயலாக்கக் கருவி
மேலும் படிக்க
- திறன் ஒப்பந்தங்களின் முறைசார் சரிபார்ப்பு எவ்வாறு செயல்படுகிறது (opens in a new tab)
- எத்திரியம் சுற்றுச்சூழல் அமைப்பில் உள்ள முறைசார் சரிபார்ப்புத் திட்டங்களின் மேலோட்டம் (opens in a new tab)
- எத்திரியம் 2.0 வைப்புத் திறன் ஒப்பந்தத்தின் எண்ட்-டு-எண்ட் முறைசார் சரிபார்ப்பு (opens in a new tab)
- உலகின் மிகவும் பிரபலமான திறன் ஒப்பந்தத்தை முறைப்படி சரிபார்த்தல் (opens in a new tab)
- SMTChecker மற்றும் முறைசார் சரிபார்ப்பு (opens in a new tab)
பக்கம் கடைசியாகப் புதுப்பிக்கப்பட்டது: 28 ஏப்ரல், 2026
