Ukuqinisekiswa okusesikweni kukuqinisekiswa kwenkqubo enye okanye i-algorithm usebenzisa enye.
Le yenye yezona ndlela zinamandla ezikuvumela ukuba ufumane bonke ubuthathaka kwiprogram okanye ubonise ukuba azikho.
Inkcazo ethe kratya yokuqinisekisa ngokusesikweni inokubonwa kumzekelo wokusombulula ingxaki ye kwinqaku lam langaphambili.
Kweli nqaku ndisuka ekuqinisekiseni ngokusemthethweni iingxaki ukuya kwiinkqubo kwaye ndichaze ukuba njani
zingaguqulwa njani zibe ziinkqubo ezisemthethweni ngokuzenzekelayo.
Ukwenza oku, ndabhala i-analogue yam yomatshini obonakalayo, usebenzisa imigaqo engokomfanekiso.
Icazulula ikhowudi yeprogram kwaye iyiguqulele kwi-system of equations (SMT), esele isonjululwe ngenkqubo.
Kuba ulwazi malunga nokubala okungokomfuziselo luboniswe kwi-Intanethi ngokwamaqhekeza,
Ndiza kuchaza ngokufutshane ukuba yintoni na.
Ubalo lweSimboli yindlela yokwenza ngaxeshanye inkqubo kuluhlu olubanzi lwedatha kwaye sisixhobo esiphambili sokuqinisekiswa kwenkqubo esemthethweni.
Umzekelo, sinokuseta iimeko zegalelo apho impikiswano yokuqala inokuthatha nawaphi na amaxabiso alungileyo, eyesibini engalunganga, eyesithathu enguziro, kunye nempikiswano yokuphuma, umzekelo, 42.
Ubalo lweSimboli kwintsebenzo enye luya kusinika impendulo yokuba ngaba kunokwenzeka ukuba sifumane umphumo ofunekayo kunye nomzekelo weseti yeeparameters zegalelo. Okanye ubungqina bokuba akukho parameters ezinjalo.
Ngaphezu koko, sinokuseta iingxoxo zegalelo kuzo zonke ezinokwenzeka, kwaye ukhethe kuphela ezo ziphumayo, umzekelo, igama eligqithisiweyo lomlawuli.
Kule meko, siya kufumana bonke ubuthathaka beprogram okanye sifumane ubungqina bokuba igama eliyimfihlo lomlawuli likhuselekile.
Kunokuqatshelwa ukuba ukuphunyezwa kweklasikhi yeprogram eneenkcukacha zegalelo elithile yimeko ekhethekileyo yokubulawa kwesimboli.
Ke ngoko, umlinganiswa wam weVM unokusebenza kwindlela yokulinganisa yomatshini oqhelekileyo wenyani.
Kwizimvo kwinqaku elidlulileyo umntu unokufumana ukugxekwa ngokufanelekileyo kokuqinisekiswa okusemthethweni kunye nengxoxo yobuthathaka bayo.
Ezona ngxaki ziphambili zezi:
- Ugqabhuko-dubulo oludityanisiweyo, kuba ukuqinisekiswa okusesikweni ekugqibeleni kwehla ku-P=NP
- Ukucubungula iifowuni kwisixokelelwano sefayile, uthungelwano kunye nolunye ugcino lwangaphandle kunzima kakhulu ukuqinisekisa
- Iibugs kwinkcazo, xa umthengi okanye umdwelisi enenjongo enye, kodwa akazange ayichaze ngokuchanekileyo ngokwaneleyo kwiinkcukacha zobugcisa.
Ngenxa yoko, inkqubo iya kuqinisekiswa kwaye ihambelane nenkcazo, kodwa iya kwenza into eyahlukileyo ngokupheleleyo kwinto elindelwe ngabadali kuyo.
Ekubeni kweli nqaku ndiqwalasela ngokukodwa ukusetyenziswa kokuqinisekiswa okusemthethweni ekusebenzeni, andiyi kubethelela intloko yam eludongeni ngoku, kwaye ndiya kukhetha inkqubo apho ubunzima be-algorithmic kunye nenani leefowuni zangaphandle zincinci.
Ekubeni iikontraki ezihlakaniphile zihambelana kakuhle nezi mfuno, ukhetho lwawela kwiikontrakthi ze-RIDE ezivela kwiqonga lama-Waves: azikho i-Turing epheleleyo, kwaye ubunzima babo obukhulu bulinganiselwe.
Kodwa siya kuziqwalasela kuphela kwicala lobugcisa.
Ukongeza kuyo yonke into, ukuqinisekiswa okusemthethweni kuya kuba yimfuneko ngokukodwa kuzo naziphi na iikontrakthi: ngokuqhelekileyo akunakwenzeka ukulungisa impazamo yekhontrakthi emva kokuba iqaliswe.
Kwaye iindleko zeempazamo ezinjalo zinokuphakama kakhulu, kuba imali eninzi kakhulu igcinwa kwiikontraki ezihlakaniphile.
Umatshini wam ongumfuziselo wenyani ubhalwe kwi-PHP kunye nePython, kwaye usebenzisa i-Z3Prover evela kuPhando lweMicrosoft ukusombulula iifomyula ze-SMT.
Embindini wayo uphendlo olunamandla lwentengiselwano emininzi, leyo
ikuvumela ukuba ufumane izisombululo okanye ubuthathaka, nokuba ifuna intengiselwano ezininzi.
Njalo , enye yezona zikhokelo ezinamandla zomfuziselo zokufumana ubuthathaka be-Ethereum, yongeza kuphela obu buchule kwiinyanga ezimbalwa ezidlulileyo.
Kodwa kuyafaneleka ukuba uqaphele ukuba iikhontrakthi ze-ether zinzima ngakumbi kwaye iTuring igqityiwe.
I-PHP iguqulela ikhowudi yomthombo we-RIDE smart contract kwi-python script, apho inkqubo inikezelwa njengenkqubo ehambelana ne-Z3 ye-SMT yesivumelwano kunye neemeko zokutshintshwa kwazo:
Ngoku ndiza kuchaza okwenzekayo ngaphakathi ngokweenkcukacha ngakumbi.
Kodwa kuqala, amagama ambalwa malunga RIDE smart contract ulwimi.
Lulwimi lwenkqubo olusebenzayo nolusekwe kwintetho eyonqena ngokuyila.
I-RIDE ibaleka yodwa ngaphakathi kwe-blockchain kwaye inokubuyisela kwaye ibhale ulwazi olusuka kwindawo yokugcina edityaniswe kwi-wallet yomsebenzisi.
Unokuqhoboshela ikhontrakthi ye-RIDE kwi-wallet nganye, kwaye umphumo wokubulawa uya kuba yi-TRUE okanye FALSE kuphela.
TRUE ithetha ukuba ikhontrakthi ehlakaniphile ivumela ukuthengiselana, kwaye FALSE ithetha ukuba iyayinqanda.
Umzekelo olula: iskripthi sinokuthintela ukudluliselwa ukuba ibhalansi ye-wallet ingaphantsi kwe-100.
Njengomzekelo, ndiza kuthatha i-Wolf, ibhokhwe, kunye neKhaphetshu efanayo, kodwa sele inikezelwe ngendlela yekhontrakthi ehlakaniphile.
Umsebenzisi akayi kukwazi ukuhoxisa imali kwi-wallet apho ikhontrakthi isetyenziswe khona de ithumele wonke umntu kwelinye icala.
#Извлекаем положение всех объектов из блокчейна
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
}
I-PHP kuqala ikhupha zonke izinto eziguquguqukayo kwikhontrakthi ehlakaniphile ngendlela yezitshixo zazo kunye ne-Boolean expression variable.
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
I-PHP emva koko ibaguqulele kwinkcazo yenkqubo ehambelana ne-Z3Prover SMT kwiPython.
Idatha ihlanganiswe kwi-loop, apho iinguqu zokugcina zifumana i-index i, i-transaction variables index i + 1, kunye neenguqu ezinamazwi abeka imigaqo yokuguquka ukusuka kwimeko yangaphambili ukuya kwelinye.
Le yeyona ntliziyo yomatshini wethu wenyani, obonelela ngeendlela ezininzi zokukhangela.
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] )
Iimeko zihlelwe kwaye zifakwe kwitemplate yeskripthi eyenzelwe ukuchaza inkqubo ye-SMT kwiPython.
Itemplate engenanto
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()
Kwimeko yokugqibela kulo lonke ikhonkco, imigaqo echazwe kwicandelo lokuthengiselana lokudluliselwa isetyenziswa.
Oku kuthetha ukuba i-Z3Prover iya kukhangela ngokuchanekileyo iiseti zemiqathango eziya kuthi ekugqibeleni zivumele ukurhoxiswa kweemali kwikhontrakthi.
Ngenxa yoko, ngokuzenzekelayo sifumana imodeli ye-SMT esebenza ngokupheleleyo yekhontrakthi yethu.
Uyabona ukuba ifana kakhulu nemodeli evela kwinqaku lam langaphambili, endiliqulunqe ngesandla.
Ithempleyithi egqityiweyo
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()
Emva kokusungulwa, i-Z3Prover isombulula ikhontrakthi ehlakaniphile kwaye isinika ikhonkco lentengiselwano eya kusivumela ukuba sirhoxise imali:
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
Ukongeza kwikhontrakthi yesikhephe, unokuzama iikhontrakthi zakho okanye uzame lo mzekelo olula, osonjululwe kwiintengiselwano ezi-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
}
Kuba le yinguqulelo yokuqala, i-syntax ilinganiselwe kakhulu kwaye kunokubakho iimpazamo.
Kumanqaku alandelayo, ndiceba ukugubungela uphuhliso olongezelelweyo lwe-VM, kwaye ndibonise indlela onokwenza ngayo izivumelwano eziqinisekisiweyo ngokusemthethweni ngoncedo lwayo, kwaye ungazisombululi nje.
Umatshini wenyani weempawu uyafumaneka kwi
Emva kokubeka ikhowudi yomthombo weVM yomfuziselo ngokulandelelana kunye nokongeza izimvo apho, ndiceba ukuyibeka kwi-GitHub yokufikelela simahla.
umthombo: www.habr.com
