ആദ്യം മുതൽ ഒരു ഔപചാരിക സ്ഥിരീകരണ സംവിധാനം സൃഷ്ടിക്കുന്നു. ഭാഗം 1: PHP, Python എന്നിവയിലെ ക്യാരക്ടർ വെർച്വൽ മെഷീൻ

ഔപചാരിക സ്ഥിരീകരണം എന്നത് ഒരു പ്രോഗ്രാമിന്റെ അല്ലെങ്കിൽ മറ്റൊന്ന് ഉപയോഗിച്ച് അൽഗോരിതം പരിശോധിച്ചുറപ്പിക്കുന്നതാണ്.

ഒരു പ്രോഗ്രാമിലെ എല്ലാ കേടുപാടുകളും കണ്ടെത്താനോ അവ നിലവിലില്ലെന്ന് തെളിയിക്കാനോ നിങ്ങളെ അനുവദിക്കുന്ന ഏറ്റവും ശക്തമായ രീതികളിൽ ഒന്നാണിത്.

ഔപചാരിക സ്ഥിരീകരണത്തിന്റെ കൂടുതൽ വിശദമായ വിവരണം പ്രശ്നം പരിഹരിക്കുന്നതിനുള്ള ഉദാഹരണത്തിൽ കാണാം ചെന്നായ, ആട്, കാബേജ് എന്റെ മുൻ ലേഖനത്തിൽ.

ഈ ലേഖനത്തിൽ ഞാൻ പ്രശ്നങ്ങളുടെ ഔപചാരിക പരിശോധനയിൽ നിന്ന് പ്രോഗ്രാമുകളിലേക്ക് നീങ്ങുകയും എങ്ങനെയെന്ന് വിവരിക്കുകയും ചെയ്യുന്നു
അവ എങ്ങനെ സ്വയമേവ ഔപചാരിക നിയമ സംവിധാനങ്ങളാക്കി മാറ്റാം.

ഇത് ചെയ്യുന്നതിന്, പ്രതീകാത്മക തത്വങ്ങൾ ഉപയോഗിച്ച് ഞാൻ ഒരു വെർച്വൽ മെഷീന്റെ സ്വന്തം അനലോഗ് എഴുതി.

ഇത് പ്രോഗ്രാം കോഡ് പാഴ്‌സ് ചെയ്യുകയും അതിനെ ഒരു സമവാക്യ സംവിധാനത്തിലേക്ക് (SMT) വിവർത്തനം ചെയ്യുകയും ചെയ്യുന്നു, അത് ഇതിനകം തന്നെ പ്രോഗ്രാമാറ്റിക് ആയി പരിഹരിക്കാൻ കഴിയും.

ഇൻറർനെറ്റിൽ പ്രതീകാത്മക കണക്കുകൂട്ടലുകളെക്കുറിച്ചുള്ള വിവരങ്ങൾ ശിഥിലമായി അവതരിപ്പിക്കുന്നതിനാൽ,
അത് എന്താണെന്ന് ഞാൻ ചുരുക്കമായി വിവരിക്കും.

സിംബോളിക് കംപ്യൂട്ടേഷൻ എന്നത് വിശാലമായ ഡാറ്റയിൽ ഒരു പ്രോഗ്രാം ഒരേസമയം എക്സിക്യൂട്ട് ചെയ്യുന്നതിനുള്ള ഒരു മാർഗമാണ്, കൂടാതെ ഔപചാരിക പ്രോഗ്രാം സ്ഥിരീകരണത്തിനുള്ള പ്രധാന ഉപകരണവുമാണ്.

ഉദാഹരണത്തിന്, ആദ്യത്തെ ആർഗ്യുമെന്റിന് ഏതെങ്കിലും പോസിറ്റീവ് മൂല്യങ്ങൾ എടുക്കാൻ കഴിയുന്ന ഇൻപുട്ട് വ്യവസ്ഥകൾ, രണ്ടാമത്തെ നെഗറ്റീവ്, മൂന്നാമത്തെ പൂജ്യം, ഔട്ട്പുട്ട് ആർഗ്യുമെന്റ്, ഉദാഹരണത്തിന്, 42 എന്നിവ സജ്ജീകരിക്കാം.

ഒരു റണ്ണിലെ പ്രതീകാത്മക കണക്കുകൂട്ടലുകൾ നമുക്ക് ആവശ്യമുള്ള ഫലം നേടാൻ കഴിയുമോ എന്നതിനുള്ള ഉത്തരവും അത്തരം ഇൻപുട്ട് പാരാമീറ്ററുകളുടെ ഒരു സെറ്റിന്റെ ഉദാഹരണവും നൽകും. അല്ലെങ്കിൽ അത്തരം പാരാമീറ്ററുകൾ ഇല്ല എന്നതിന്റെ തെളിവ്.

മാത്രമല്ല, സാധ്യമായ എല്ലാ കാര്യങ്ങളിലും നമുക്ക് ഇൻപുട്ട് ആർഗ്യുമെന്റുകൾ സജ്ജമാക്കാൻ കഴിയും, കൂടാതെ ഔട്ട്പുട്ട് മാത്രം തിരഞ്ഞെടുക്കുക, ഉദാഹരണത്തിന്, അഡ്മിനിസ്ട്രേറ്റർ പാസ്വേഡ്.

ഈ സാഹചര്യത്തിൽ, പ്രോഗ്രാമിന്റെ എല്ലാ കേടുപാടുകളും ഞങ്ങൾ കണ്ടെത്തും അല്ലെങ്കിൽ അഡ്മിനിസ്ട്രേറ്ററുടെ പാസ്‌വേഡ് സുരക്ഷിതമാണെന്നതിന് തെളിവ് ലഭിക്കും.

നിർദ്ദിഷ്ട ഇൻപുട്ട് ഡാറ്റയുള്ള ഒരു പ്രോഗ്രാമിന്റെ ക്ലാസിക്കൽ എക്സിക്യൂഷൻ പ്രതീകാത്മക നിർവ്വഹണത്തിന്റെ ഒരു പ്രത്യേക കേസാണെന്ന് ശ്രദ്ധിക്കാവുന്നതാണ്.

അതിനാൽ, ഒരു സ്റ്റാൻഡേർഡ് വെർച്വൽ മെഷീന്റെ എമുലേഷൻ മോഡിലും എന്റെ പ്രതീകം VM പ്രവർത്തിക്കാൻ കഴിയും.

മുമ്പത്തെ ലേഖനത്തിലെ അഭിപ്രായങ്ങളിൽ, ഔപചാരികമായ സ്ഥിരീകരണത്തെക്കുറിച്ചുള്ള ന്യായമായ വിമർശനം അതിന്റെ ദൗർബല്യങ്ങളെക്കുറിച്ചുള്ള ചർച്ചയും കണ്ടെത്താനാകും.

പ്രധാന പ്രശ്നങ്ങൾ ഇവയാണ്:

1. ഔപചാരികമായ സ്ഥിരീകരണം ആത്യന്തികമായി P=NP ലേക്ക് വരുന്നതിനാൽ സംയോജിത സ്ഫോടനം
2. ഫയൽ സിസ്റ്റം, നെറ്റ്‌വർക്കുകൾ, മറ്റ് ബാഹ്യ സംഭരണം എന്നിവയിലേക്കുള്ള കോളുകൾ പ്രോസസ്സ് ചെയ്യുന്നത് പരിശോധിക്കുന്നത് കൂടുതൽ ബുദ്ധിമുട്ടാണ്
3. സ്പെസിഫിക്കേഷനിലെ ബഗുകൾ, ഉപഭോക്താവോ പ്രോഗ്രാമറോ ഒരു കാര്യം ഉദ്ദേശിക്കുമ്പോൾ, എന്നാൽ സാങ്കേതിക സ്പെസിഫിക്കേഷനിൽ അത് വേണ്ടത്ര കൃത്യമായി വിവരിച്ചില്ല.

തൽഫലമായി, പ്രോഗ്രാം പരിശോധിച്ചുറപ്പിക്കുകയും സ്പെസിഫിക്കേഷനുമായി പൊരുത്തപ്പെടുകയും ചെയ്യും, എന്നാൽ സ്രഷ്‌ടാക്കൾ അതിൽ നിന്ന് പ്രതീക്ഷിച്ചതിൽ നിന്ന് തികച്ചും വ്യത്യസ്തമായ എന്തെങ്കിലും ചെയ്യും.

ഈ ലേഖനത്തിൽ, പ്രായോഗികമായി ഔപചാരികമായ സ്ഥിരീകരണത്തിന്റെ ഉപയോഗം ഞാൻ പ്രധാനമായും പരിഗണിക്കുന്നതിനാൽ, ഞാൻ ഇപ്പോൾ ചുവരിൽ തല കുനിക്കുന്നില്ല, കൂടാതെ അൽഗോരിതം സങ്കീർണ്ണതയും ബാഹ്യ കോളുകളുടെ എണ്ണവും കുറവുള്ള ഒരു സിസ്റ്റം തിരഞ്ഞെടുക്കും.

സ്‌മാർട്ട് കരാറുകൾ ഈ ആവശ്യകതകൾക്ക് ഏറ്റവും അനുയോജ്യമായതിനാൽ, വേവ്സ് പ്ലാറ്റ്‌ഫോമിൽ നിന്നുള്ള റൈഡ് കരാറുകളിൽ ചോയ്‌സ് വന്നു: അവ ട്യൂറിംഗ് പൂർത്തിയായിട്ടില്ല, മാത്രമല്ല അവയുടെ പരമാവധി സങ്കീർണ്ണത കൃത്രിമമായി പരിമിതപ്പെടുത്തിയിരിക്കുന്നു.

എന്നാൽ ഞങ്ങൾ അവ സാങ്കേതിക വശത്തുനിന്ന് മാത്രമായി പരിഗണിക്കും.

എല്ലാത്തിനും പുറമേ, ഏതെങ്കിലും കരാറുകൾക്കായി ഔപചാരിക സ്ഥിരീകരണം പ്രത്യേകിച്ചും ആവശ്യക്കാരായിരിക്കും: സമാരംഭിച്ചതിന് ശേഷം ഒരു കരാർ പിശക് തിരുത്തുന്നത് സാധാരണയായി അസാധ്യമാണ്.
അത്തരം പിശകുകളുടെ വില വളരെ ഉയർന്നതായിരിക്കും, കാരണം വളരെ വലിയ അളവിലുള്ള ഫണ്ടുകൾ പലപ്പോഴും സ്മാർട്ട് കരാറുകളിൽ സൂക്ഷിക്കുന്നു.

എന്റെ സിംബോളിക് വെർച്വൽ മെഷീൻ PHP, Python എന്നിവയിൽ എഴുതിയിരിക്കുന്നു, തത്ഫലമായുണ്ടാകുന്ന SMT ഫോർമുലകൾ പരിഹരിക്കാൻ Microsoft റിസർച്ചിൽ നിന്നുള്ള Z3Prover ഉപയോഗിക്കുന്നു.

അതിന്റെ കാതൽ ശക്തമായ ഒരു മൾട്ടി-ഇടപാട് തിരയലാണ്, അത്
നിരവധി ഇടപാടുകൾ ആവശ്യമായി വന്നാലും, പരിഹാരങ്ങളോ കേടുപാടുകളോ കണ്ടെത്താൻ നിങ്ങളെ അനുവദിക്കുന്നു.
പോലും മൈഥിൽ, Ethereum കേടുപാടുകൾ കണ്ടെത്തുന്നതിനുള്ള ഏറ്റവും ശക്തമായ പ്രതീകാത്മക ചട്ടക്കൂടുകളിൽ ഒന്ന്, കുറച്ച് മാസങ്ങൾക്ക് മുമ്പ് ഈ കഴിവ് ചേർത്തു.

എന്നാൽ ഈതർ കരാറുകൾ കൂടുതൽ സങ്കീർണ്ണവും ട്യൂറിംഗ് പൂർണ്ണവുമാണ് എന്നത് ശ്രദ്ധിക്കേണ്ടതാണ്.

RIDE സ്‌മാർട്ട് കരാറിന്റെ സോഴ്‌സ് കോഡ് ഒരു പൈത്തൺ സ്‌ക്രിപ്റ്റിലേക്ക് PHP വിവർത്തനം ചെയ്യുന്നു, അതിൽ പ്രോഗ്രാം Z3 SMT-അനുയോജ്യമായ കോൺട്രാക്ട് സ്റ്റേറ്റുകളും അവയുടെ സംക്രമണത്തിനുള്ള വ്യവസ്ഥകളും ആയി അവതരിപ്പിക്കുന്നു:

ഉള്ളിൽ എന്താണ് സംഭവിക്കുന്നതെന്ന് ഇപ്പോൾ ഞാൻ കൂടുതൽ വിശദമായി വിവരിക്കും.

എന്നാൽ ആദ്യം, റൈഡ് സ്മാർട്ട് കരാർ ഭാഷയെക്കുറിച്ച് കുറച്ച് വാക്കുകൾ.

രൂപകല്പനയിൽ അലസമായ പ്രവർത്തനപരവും ആവിഷ്കാരത്തെ അടിസ്ഥാനമാക്കിയുള്ളതുമായ പ്രോഗ്രാമിംഗ് ഭാഷയാണിത്.
ബ്ലോക്ക്‌ചെയിനിനുള്ളിൽ ഒറ്റപ്പെട്ട നിലയിലാണ് RIDE പ്രവർത്തിക്കുന്നത്, ഉപയോക്താവിന്റെ വാലറ്റിലേക്ക് ലിങ്ക് ചെയ്‌തിരിക്കുന്ന സ്റ്റോറേജിൽ നിന്ന് വിവരങ്ങൾ വീണ്ടെടുക്കാനും എഴുതാനും കഴിയും.

ഓരോ വാലറ്റിലും നിങ്ങൾക്ക് ഒരു റൈഡ് കരാർ അറ്റാച്ചുചെയ്യാം, കൂടാതെ നിർവ്വഹണത്തിന്റെ ഫലം ശരിയോ തെറ്റോ ആയിരിക്കും.

TRUE അർത്ഥമാക്കുന്നത് സ്‌മാർട്ട് കരാർ ഇടപാട് അനുവദിക്കുന്നു, FALSE എന്നാൽ അത് നിരോധിക്കുന്നു എന്നാണ്.
ഒരു ലളിതമായ ഉദാഹരണം: വാലറ്റ് ബാലൻസ് 100-ൽ കുറവാണെങ്കിൽ ഒരു സ്ക്രിപ്റ്റിന് ഒരു കൈമാറ്റം നിരോധിക്കാനാകും.

ഒരു ഉദാഹരണമായി, ഞാൻ അതേ വുൾഫ്, ആട്, കാബേജ് എന്നിവ എടുക്കും, പക്ഷേ ഇതിനകം ഒരു സ്മാർട്ട് കരാറിന്റെ രൂപത്തിൽ അവതരിപ്പിച്ചു.

എല്ലാവരെയും മറുവശത്തേക്ക് അയക്കുന്നതുവരെ, കരാർ വിന്യസിച്ചിരിക്കുന്ന വാലറ്റിൽ നിന്ന് ഉപയോക്താവിന് പണം പിൻവലിക്കാൻ കഴിയില്ല.

#Извлекаем положение всех объектов из блокчейна
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))

#Это так называемая дата-транзакция, в которой пользователь присылает новые 4 переменные.
#Контракт разрешит её только в случае если все объекты останутся в сохранности.
match tx {
case t:DataTransaction =>
   #Извлекаем будущее положение всех объектов из транзакции
   let newHuman= extract(getInteger(t.data,"human")) 
   let newWolf= extract(getInteger(t.data,"wolf"))
   let newGoat= extract(getInteger(t.data,"goat"))
   let newCabbage= extract(getInteger(t.data,"cabbage"))
   
   #0 обозначает, что объект на левом берегу, а 1 что на правом
   let humanSide= human == 0 || human == 1
   let wolfSide= wolf == 0 || wolf == 1
   let goatSide= goat == 0 || goat == 1
   let cabbageSide= cabbage == 0 || cabbage == 1
   let side= humanSide && wolfSide && goatSide && cabbageSide

   #Будут разрешены только те транзакции, где с козой никого нет в отсутствии фермера.
   let safeAlone= newGoat != newWolf && newGoat != newCabbage
   let safe= safeAlone || newGoat == newHuman
   let humanTravel= human != newHuman 

   #Способы путешествия фермера туда и обратно, с кем-то либо в одиночку.
   let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage 
   let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
   let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
   let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
   let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
   let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
   let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
   let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
   
   #Последняя строка в разделе транзакции описывает разрешающее транзакцию условие.
   #Переменные транзакции должны иметь значения 1 или 0, все объекты должны
   #быть в безопасности, а фермер должен переплывать реку в одиночку 
   #или с кем-то на каждом шагу
   side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
   #Транзакция вывода средств разрешена только в случае если все переплыли на другой берег
   human == 1 && wolf == 1 && goat == 1 && cabbage == 1

#Все прочие типы транзакций запрещены
case _ => false

}

PHP ആദ്യം സ്മാർട്ട് കരാറിൽ നിന്ന് എല്ലാ വേരിയബിളുകളും അവയുടെ കീകളുടെയും അനുബന്ധ ബൂളിയൻ എക്സ്പ്രഷൻ വേരിയബിളിന്റെയും രൂപത്തിൽ വേർതിരിച്ചെടുക്കുന്നു.

cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState: 
wolf: 
goat: 
cabbage: 
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7

PHP പിന്നീട് അവയെ പൈത്തണിലെ Z3Prover SMT-അനുയോജ്യമായ സിസ്റ്റം വിവരണമായി പരിവർത്തനം ചെയ്യുന്നു.
ഡാറ്റ ഒരു ലൂപ്പിൽ പൊതിഞ്ഞിരിക്കുന്നു, അവിടെ സ്റ്റോറേജ് വേരിയബിളുകൾക്ക് സൂചിക i, ട്രാൻസാക്ഷൻ വേരിയബിളുകൾ സൂചിക i + 1 എന്നിവ ലഭിക്കുന്നു, കൂടാതെ എക്സ്പ്രഷനുകളുള്ള വേരിയബിളുകൾ മുമ്പത്തെ അവസ്ഥയിൽ നിന്ന് അടുത്ത അവസ്ഥയിലേക്ക് മാറുന്നതിനുള്ള നിയമങ്ങൾ സജ്ജമാക്കുന്നു.

ഇത് ഞങ്ങളുടെ വെർച്വൽ മെഷീന്റെ ഹൃദയമാണ്, ഇത് ഒരു മൾട്ടി-ഇടപാട് തിരയൽ സംവിധാനം നൽകുന്നു.

fState:  And( And( And( human[Steps]  ==  1 , wolf[Steps]  ==  1 )  , goat[Steps]  ==  1 )  , cabbage[Steps]  ==  1 )  
final:  fState[Steps] 
fState:   
wolf:   
goat:   
cabbage:   
cabbageSide:  Or( cabbage[i]  ==  0 , cabbage[i]  ==  1 )  
goatSide:  Or( goat[i]  ==  0 , goat[i]  ==  1 )  
humanSide:  Or( human[i]  ==  0 , human[i]  ==  1 )  
t7:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] )  
t3:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] + 1 )  
t6:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] - 1 )  
t2:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] + 1 )  , cabbage  ==  cabbage[i] )  
t5:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] )  , goat[i+1]  ==  goat[i] - 1 )  , cabbage  ==  cabbage[i] )  
t1:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] + 1 )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] )  
t4:  And( And( And( humanTravel[i] , wolf  ==  wolf[i] - 1 )  , goat[i+1]  ==  goat[i] )  , cabbage  ==  cabbage[i] )  
safeAlone:  And( goat[i+1] != wolf , goat[i+1] != cabbage )  
wolfSide:  Or( wolf[i]  ==  0 , wolf[i]  ==  1 )  
humanTravel:  human[i] != human[i+1] 
side:  And( And( And( humanSide[i] , wolfSide[i] )  , goatSide[i] )  , cabbageSide[i] )  
safe:  Or( safeAlone[i] , goat[i+1]  ==  human[i+1] )  
objectTravel:  Or( Or( Or( Or( Or( Or( t1[i] , t2[i] )  , t3[i] )  , t4[i] )  , t5[i] )  , t6[i] )  , t7[i] )  
data:  And( And( And( side[i] , safe[i] )  , humanTravel[i] )  , objectTravel[i] )  

പൈത്തണിലെ SMT സിസ്റ്റത്തെ വിവരിക്കാൻ രൂപകൽപ്പന ചെയ്ത ഒരു സ്ക്രിപ്റ്റ് ടെംപ്ലേറ്റിലേക്ക് വ്യവസ്ഥകൾ അടുക്കി ചേർക്കുന്നു.

ശൂന്യമായ ടെംപ്ലേറ്റ്

import json

from z3 import *

s = Solver()

  
  
    
Steps=7
Num= Steps+1

$code$



#template, only start rest
s.add(data + start)

#template
s.add(final)




ind = 0

f = open("/var/www/html/all/bin/python/log.txt", "a")



while s.check() == sat:
  ind = ind +1
  

  print ind
  m = s.model()
  print m

  print "traversing model..." 
  #for d in m.decls():
	#print "%s = %s" % (d.name(), m[d])

  
 
  f.write(str(m))
  f.write("nn")
  exit()
  #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model



print "Total solution number: "
print ind  

f.close()
 

മുഴുവൻ ശൃംഖലയിലെയും അവസാന സംസ്ഥാനത്തിന്, ട്രാൻസ്ഫർ ഇടപാട് വിഭാഗത്തിൽ വ്യക്തമാക്കിയിരിക്കുന്ന നിയമങ്ങൾ ബാധകമാണ്.

കരാറിൽ നിന്ന് പണം പിൻവലിക്കാൻ ആത്യന്തികമായി അനുവദിക്കുന്ന അത്തരം വ്യവസ്ഥകൾക്കായി Z3Prover നോക്കും എന്നാണ് ഇതിനർത്ഥം.

തൽഫലമായി, ഞങ്ങളുടെ കരാറിന്റെ പൂർണ്ണമായും പ്രവർത്തനക്ഷമമായ SMT മോഡൽ ഞങ്ങൾക്ക് സ്വയമേവ ലഭിക്കും.
ഞാൻ സ്വമേധയാ സമാഹരിച്ച എന്റെ മുൻ ലേഖനത്തിൽ നിന്നുള്ള മോഡലുമായി ഇത് വളരെ സാമ്യമുള്ളതാണെന്ന് നിങ്ങൾക്ക് കാണാൻ കഴിയും.

പൂർത്തിയായ ടെംപ്ലേറ്റ്

import json

from z3 import *

s = Solver()

  
  
    
Steps=7
Num= Steps+1

human = [ Int('human_%i' % (i + 1)) for i in range(Num) ]
wolf = [ Int('wolf_%i' % (i + 1)) for i in range(Num) ]
goat = [ Int('goat_%i' % (i + 1)) for i in range(Num) ]
cabbage = [ Int('cabbage_%i' % (i + 1)) for i in range(Num) ]
nothing= [  And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] )   for i in range(Num-1) ]


start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]

safeAlone= [  And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] )   for i in range(Num-1) ]
safe= [  Or( safeAlone[i] , goat[i+1]  ==  human[i+1] )   for i in range(Num-1) ]
humanTravel= [  human[i] != human[i+1]  for i in range(Num-1) ]
cabbageSide= [  Or( cabbage[i]  ==  0 , cabbage[i]  ==  1 )   for i in range(Num-1) ]
goatSide= [  Or( goat[i]  ==  0 , goat[i]  ==  1 )   for i in range(Num-1) ]
humanSide= [  Or( human[i]  ==  0 , human[i]  ==  1 )   for i in range(Num-1) ]
t7= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t3= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] + 1 )   for i in range(Num-1) ]
t6= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] - 1 )   for i in range(Num-1) ]
t2= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] + 1 )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t5= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] )  , goat[i+1]  ==  goat[i] - 1 )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t1= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] + 1 )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
t4= [  And( And( And( humanTravel[i] , wolf[i+1]  ==  wolf[i] - 1 )  , goat[i+1]  ==  goat[i] )  , cabbage[i+1]  ==  cabbage[i] )   for i in range(Num-1) ]
wolfSide= [  Or( wolf[i]  ==  0 , wolf[i]  ==  1 )   for i in range(Num-1) ]
side= [  And( And( And( humanSide[i] , wolfSide[i] )  , goatSide[i] )  , cabbageSide[i] )   for i in range(Num-1) ]
objectTravel= [  Or( Or( Or( Or( Or( Or( t1[i] , t2[i] )  , t3[i] )  , t4[i] )  , t5[i] )  , t6[i] )  , t7[i] )   for i in range(Num-1) ]
data= [ Or(  And( And( And( side[i] , safe[i] )  , humanTravel[i] )  , objectTravel[i] )   , nothing[i]) for i in range(Num-1) ]


fState=  And( And( And( human[Steps]  ==  1 , wolf[Steps]  ==  1 )  , goat[Steps]  ==  1 )  , cabbage[Steps]  ==  1 )  
final=  fState 




#template, only start rest
s.add(data + start)

#template
s.add(final)




ind = 0

f = open("/var/www/html/all/bin/python/log.txt", "a")



while s.check() == sat:
  ind = ind +1
  

  print ind
  m = s.model()
  print m

  print "traversing model..." 
  #for d in m.decls():
	#print "%s = %s" % (d.name(), m[d])

  
 
  f.write(str(m))
  f.write("nn")
  exit()
  #s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model



print "Total solution number: "
print ind  

f.close()
 

സമാരംഭിച്ചതിന് ശേഷം, Z3Prover സ്മാർട്ട് കരാർ പരിഹരിക്കുകയും പണം പിൻവലിക്കാൻ ഞങ്ങളെ അനുവദിക്കുന്ന ഇടപാടുകളുടെ ഒരു ശൃംഖല നൽകുകയും ചെയ്യുന്നു:

Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction

കടത്തുവള്ള കരാറിന് പുറമേ, നിങ്ങൾക്ക് നിങ്ങളുടെ സ്വന്തം കരാറുകൾ ഉപയോഗിച്ച് പരീക്ഷിക്കാം അല്ലെങ്കിൽ 2 ഇടപാടുകളിൽ പരിഹരിച്ച ഈ ലളിതമായ ഉദാഹരണം പരീക്ഷിക്കാം.

let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))

match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a")) 
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
   
   nd == 0 || a == 100 - 5
case s:TransferTransaction =>
   ( a + b - c ) * d == 12

case _ => true

}

ഇത് ആദ്യ പതിപ്പായതിനാൽ, വാക്യഘടന വളരെ പരിമിതമാണ് കൂടാതെ ബഗുകൾ ഉണ്ടാകാം.
ഇനിപ്പറയുന്ന ലേഖനങ്ങളിൽ, വി‌എമ്മിന്റെ കൂടുതൽ വികസനം കവർ ചെയ്യാനും അതിന്റെ സഹായത്തോടെ നിങ്ങൾക്ക് എങ്ങനെ ഔപചാരികമായി പരിശോധിച്ചുറപ്പിച്ച സ്‌മാർട്ട് കരാറുകൾ സൃഷ്‌ടിക്കാമെന്നും കാണിക്കാൻ ഞാൻ പദ്ധതിയിടുന്നു, മാത്രമല്ല അവ പരിഹരിക്കുക മാത്രമല്ല.

അക്ഷര വെർച്വൽ മെഷീൻ ഇവിടെ ലഭ്യമാണ് http://2.59.42.98/hyperbox/
പ്രതീകാത്മക VM-ന്റെ സോഴ്സ് കോഡ് ക്രമീകരിച്ച് അവിടെ അഭിപ്രായങ്ങൾ ചേർത്ത ശേഷം, സൗജന്യ ആക്‌സസ്സിനായി അത് GitHub-ൽ ഇടാൻ ഞാൻ ആഗ്രഹിക്കുന്നു.

അവലംബം: www.habr.com