Ukudala isistimu yokuqinisekisa esemthethweni kusukela ekuqaleni. Ingxenye 1: Umshini Obonakalayo Wezinhlamvu ku-PHP nePython

Ukuqinisekisa okusemthethweni ukuqinisekiswa kohlelo noma i-algorithm ethile kusetshenziswa olunye.

Lena enye yezindlela ezinamandla kakhulu ezikuvumela ukuthi uthole bonke ubungozi kuhlelo noma ufakazele ukuthi azikho.

Incazelo enemininingwane eminingi yokuqinisekisa okusemthethweni ingabonakala esibonelweni sokuxazulula inkinga ye Impisi, Imbuzi, Neklabishi esihlokweni sami esandulele.

Kulesi sihloko ngisuka ekuqinisekiseni okusemthethweni kwezinkinga ngiye ezinhlelweni futhi ngichaze ukuthi kanjani
zingaguqulwa kanjani zibe yizimiso ezisemthethweni ngokuzenzakalelayo.

Ukwenza lokhu, ngibhale i-analogue yami yomshini obonakalayo, ngisebenzisa izimiso ezingokomfanekiso.

Incozulula ikhodi yohlelo bese iyihumushela ohlelweni lwezibalo (SMT), oseluvele luxazululwe ngokohlelo.

Njengoba ulwazi olumayelana nezibalo ezingokomfanekiso zivezwa ku-inthanethi ngokwehlukana,
Ngizochaza kafushane ukuthi kuyini.

Ukubala okungokomfanekiso kuyindlela yokwenza ngesikhathi esisodwa uhlelo kudatha ebanzi futhi iyithuluzi eliyinhloko lokuqinisekisa uhlelo olusemthethweni.

Isibonelo, singasetha izimo zokufaka lapho i-agumenti yokuqala ingathatha noma yimaphi amanani avumayo, eyesibili enegethivu, enguziro wesithathu, kanye ne-agumenti yokukhiphayo, isibonelo, 42.

Izibalo ezingokomfanekiso ekugijimeni okukodwa zizosinika impendulo yokuthi kuyenzeka yini ukuthi sithole umphumela esiwufunayo kanye nesibonelo sesethi yamapharamitha anjalo okokufaka. Noma ubufakazi bokuthi awekho amapharamitha anjalo.

Ngaphezu kwalokho, singasetha ama-agumenti okokufaka kubo bonke abangaba khona, bese sikhetha okuphumayo kuphela, isibonelo, iphasiwedi yomlawuli.

Kulokhu, sizothola bonke ubungozi bohlelo noma sithole ubufakazi bokuthi iphasiwedi yomlawuli iphephile.

Kungaqashelwa ukuthi ukwenziwa kwakudala kohlelo olunedatha ethile yokufaka kuyisimo esikhethekile sokubulawa okungokomfanekiso.

Ngakho-ke, uhlamvu lwami lwe-VM lungasebenza futhi kumodi yokulingisa yomshini ojwayelekile we-virtual.

Emazwaneni esihlokweni esandulele umuntu angathola ukugxekwa okufanele kokuqinisekisa okusemthethweni ngengxoxo yobuthakathaka bayo.

Izinkinga ezinkulu yilezi:

1. Ukuqhuma okuyinhlanganisela, njengoba ukuqinisekiswa okusemthethweni kugcina kwehla ku-P=NP
2. Ukucubungula amakholi kusistimu yefayela, amanethiwekhi nokunye ukulondoloza kwangaphandle kunzima kakhulu ukuqinisekisa
3. Iziphazamisi esimisweni, lapho ikhasimende noma umhleli ehlose into eyodwa, kodwa engazange ayichaze ngokunembile ngokwanele ekucacisweni kobuchwepheshe.

Ngenxa yalokho, uhlelo luzoqinisekiswa futhi luhambisane nencazelo, kodwa luzokwenza okuthile okuhluke ngokuphelele kulokho ababekulindele abadali kulo.

Njengoba kulesi sihloko ngicabangela ikakhulukazi ukusetshenziswa kokuqinisekisa okusemthethweni ekusebenzeni, ngeke ngiqhume ikhanda lami odongeni okwamanje, futhi ngizokhetha uhlelo lapho ubunzima be-algorithmic kanye nenani lezingcingo zangaphandle zincane.

Njengoba izinkontileka ezihlakaniphile zifanelana kangcono nalezi zidingo, ukukhetha kuwele kuzinkontileka ze-RIDE ezivela kuplathifomu ye-Waves: azikaqedwa i-Turing, futhi ubunkimbinkimbi bazo obukhulu bukhawulelwe ngokwenziwa.

Kodwa sizozicabangela ngokukhethekile ohlangothini lwezobuchwepheshe.

Ngaphezu kwakho konke, ukuqinisekiswa okusemthethweni kuzoba yisidingo ikakhulukazi sanoma yiziphi izinkontileka: ngokuvamile akunakwenzeka ukulungisa iphutha lenkontileka ngemva kokwethulwa.
Futhi izindleko zamaphutha anjalo zingaba phezulu kakhulu, ngoba izimali eziningi zivame ukugcinwa kuzinkontileka ezihlakaniphile.

Umshini wami we-virtual ongokomfanekiso ubhalwe nge-PHP ne-Python, futhi usebenzisa i-Z3Prover evela ku-Microsoft Research ukuxazulula amafomula e-SMT angumphumela.

Emgogodleni walo usesho olunamandla lwe-multi-transactional, okuyinto
ikuvumela ukuthi uthole izixazululo noma ubungozi, noma ngabe kudinga ukuthengiselana okuningi.
Ngisho no I-Mythril, enye yezinhlaka ezingokomfanekiso ezinamandla kakhulu zokuthola ubungozi be-Ethereum, yengeze leli khono ezinyangeni ezimbalwa ezedlule.

Kodwa kufanelekile ukuqaphela ukuthi izinkontileka ze-ether ziyinkimbinkimbi futhi i-Turing iphelele.

I-PHP ihumusha ikhodi yomthombo yenkontileka ehlakaniphile ye-RIDE ibe iskripthi se-python, lapho uhlelo lwethulwa njengohlelo oluhambisana ne-Z3 SMT lwezimo zenkontileka nezimo zoshintsho lwazo:

Manje ngizochaza okwenzeka ngaphakathi ngokuningiliziwe.

Kodwa okokuqala, amagama ambalwa mayelana nolimi lwenkontileka ehlakaniphile ye-RIDE.

Kuwulimi lokuhlela olusebenzayo nolusekelwe emazwini oluvilapha ngokuklama.
I-RIDE isebenza yodwa ngaphakathi kwe-blockchain futhi ingathola futhi ibhale ulwazi olusuka kusitoreji esixhunywe esikhwameni somsebenzisi.

Ungakwazi ukunamathisela inkontileka ye-RIDE esikhwameni ngasinye, futhi umphumela wokusebenzisa uzoba kuphela IQINISO noma AMANGA.

I-TRUE isho ukuthi inkontileka ehlakaniphile ivumela umsebenzi, futhi FALSE isho ukuthi iyakwenqabela.
Isibonelo esilula: iskripthi singavimbela ukudluliswa uma ibhalansi yesikhwama ingaphansi kuka-100.

Njengesibonelo, ngizothatha iMpisi, Imbuzi, kanye neKhabishi efanayo, kodwa eseyethulwe ngendlela yenkontileka ehlakaniphile.

Umsebenzisi ngeke akwazi ukukhipha imali esikhwameni lapho inkontileka isetshenziswa kuze kube yilapho esethumele wonke umuntu kolunye uhlangothi.

#Извлекаем положение всех объектов из блокчейна
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 iqala ngokukhipha zonke izinto eziguquguqukayo kusukela kunkontileka ehlakaniphile ngendlela yokhiye bazo kanye nokuguquguquka kwesisho se-Boolean esihambisanayo.

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 ibese iwaguqulela kuncazelo yesistimu ehambisana ne-Z3Prover SMT kuPython.
Idatha isongwe nge-loop, lapho okuguquguqukayo kwesitoreji kuthola khona inkomba i, inkomba ye-transaction variables i + 1, futhi okuguquguqukayo okunezinkulumo kusetha imithetho yokuguquka ukusuka kusimo sangaphambili kuya kwesilandelayo.

Lona kanye inhliziyo yomshini wethu we-virtual, ohlinzeka ngenjini yokusesha enemisebenzi eminingi.

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] )  

Izimo ziyahlungwa futhi zifakwe kusifanekiso sombhalo esidizayinelwe ukuchaza uhlelo lwe-SMT kuPython.

Isifanekiso esingenalutho

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()
 

Esimeni sokugcina kulo lonke iketango, imithetho eshiwo esigabeni sokushintshana sokudlulisa isetshenziswa.

Lokhu kusho ukuthi i-Z3Prover izobheka amasethi anjalo emibandela ayogcina evumele ukuthi izimali zihoxiswe kwinkontileka.

Ngenxa yalokho, sithola ngokuzenzakalelayo imodeli ye-SMT esebenza ngokugcwele yenkontileka yethu.
Uyabona ukuthi ifana kakhulu nemodeli evela esihlokweni sami sangaphambilini, engayihlanganisa ngesandla.

Isifanekiso esiqediwe

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()
 

Ngemuva kokwethulwa, i-Z3Prover ixazulula inkontileka ehlakaniphile futhi isinikeze uchungechunge lwemisebenzi oluzosivumela ukuthi sikhiphe 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

Ngokungeziwe kwinkontileka yesikebhe, ungazama izinkontileka zakho noma uzame lesi sibonelo esilula, esixazululwa emisebenzini emi-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

}

Njengoba lena kuyinguqulo yokuqala, i-syntax ilinganiselwe kakhulu futhi kungase kube nezimbungulu.
Ezihlokweni ezilandelayo, ngihlela ukumboza ukuthuthukiswa okuqhubekayo kwe-VM, futhi ngibonise ukuthi ungakha kanjani izinkontileka ezihlakaniphile eziqinisekisiwe ngokusemthethweni ngosizo lwayo, hhayi nje ukuzixazulula.

Umshini obonakalayo wezinhlamvu uyatholakala ku http://2.59.42.98/hyperbox/
Ngemuva kokubeka ikhodi yomthombo ye-VM engokomfanekiso ngokulandelana kanye nokwengeza amazwana lapho, ngihlela ukuyibeka ku-GitHub ukuze ngifinyeleleke mahhala.

Source: www.habr.com