Ijẹrisi deede jẹ ijẹrisi ti eto kan tabi algorithm nipa lilo omiiran.
Eyi jẹ ọkan ninu awọn ọna ti o lagbara julọ ti o fun ọ laaye lati wa gbogbo awọn ailagbara ninu eto tabi fihan pe wọn ko si.
Apejuwe alaye diẹ sii ti ijẹrisi deede ni a le rii ni apẹẹrẹ ti ipinnu iṣoro ti ninu mi ti tẹlẹ article.
Ninu nkan yii Mo gbe lati ijẹrisi deede ti awọn iṣoro si awọn eto ati ṣapejuwe bii
bawo ni wọn ṣe le yipada si awọn eto ofin deede laifọwọyi.
Lati ṣe eyi, Mo kọ afọwọṣe ti ara mi ti ẹrọ foju kan, ni lilo awọn ipilẹ apẹẹrẹ.
O ṣe itupalẹ koodu eto ati tumọ rẹ sinu eto awọn idogba (SMT), eyiti o le yanju tẹlẹ ni eto.
Niwọn igba ti alaye nipa awọn iṣiro aami ti gbekalẹ lori Intanẹẹti kuku ni aibikita,
Emi yoo ṣe apejuwe ni ṣoki kini o jẹ.
Iṣiro aami jẹ ọna lati ṣe eto nigbakanna lori ọpọlọpọ data ati pe o jẹ irinṣẹ akọkọ fun ijẹrisi eto deede.
Fun apẹẹrẹ, a le ṣeto awọn ipo titẹ sii nibiti ariyanjiyan akọkọ le gba eyikeyi awọn iye to dara, odi keji, odo kẹta, ati ariyanjiyan abajade, fun apẹẹrẹ, 42.
Awọn iṣiro aami ni ṣiṣe kan yoo fun wa ni idahun si boya o ṣee ṣe fun wa lati gba abajade ti o fẹ ati apẹẹrẹ ti ṣeto iru awọn aye titẹ sii. Tabi ẹri ti ko si iru paramita.
Pẹlupẹlu, a le ṣeto awọn ariyanjiyan igbewọle si gbogbo awọn ti o ṣeeṣe, ati yan awọn ti o wu jade nikan, fun apẹẹrẹ, ọrọ igbaniwọle alakoso.
Ni ọran yii, a yoo rii gbogbo awọn ailagbara eto tabi gba ẹri pe ọrọ igbaniwọle alakoso jẹ ailewu.
O le ṣe akiyesi pe ipaniyan kilasika ti eto kan pẹlu data titẹ sii kan pato jẹ ọran pataki ti ipaniyan aami.
Nitorinaa, ohun kikọ mi VM tun le ṣiṣẹ ni ipo emulation ti ẹrọ foju foju kan.
Ninu awọn asọye si nkan ti tẹlẹ ọkan le rii atako ododo ti ijẹrisi deede pẹlu ijiroro ti awọn ailagbara rẹ.
Awọn iṣoro akọkọ ni:
- Bugbamu idapọmọra, niwọn igba ti ijerisi iṣe deede de nikẹhin si P=NP
- Ṣiṣe awọn ipe si eto faili, awọn nẹtiwọọki ati ibi ipamọ ita miiran jẹ diẹ sii nira sii lati mọ daju
- Awọn idun ni sipesifikesonu, nigbati alabara tabi pirogirama ti pinnu ohun kan, ṣugbọn ko ṣe apejuwe rẹ ni pipe ni sipesifikesonu imọ-ẹrọ.
Bi abajade, eto naa yoo jẹri ati ni ibamu pẹlu sipesifikesonu, ṣugbọn yoo ṣe nkan ti o yatọ patapata si ohun ti awọn olupilẹṣẹ nireti lati ọdọ rẹ.
Niwọn bi ninu nkan yii Mo n ṣakiyesi nipa lilo iṣeduro iṣe deede ni iṣe, Emi kii yoo kọ ori mi si odi ni bayi, ati pe yoo yan eto kan nibiti idiju algorithmic ati nọmba awọn ipe ita jẹ iwonba.
Niwọn igba ti awọn adehun smati dara julọ baamu awọn ibeere wọnyi, yiyan naa ṣubu lori awọn adehun RIDE lati pẹpẹ Waves: wọn ko pari Turing, ati pe eka ti o pọju wọn jẹ opin lainidi.
Ṣugbọn a yoo ṣe akiyesi wọn ni iyasọtọ lati ẹgbẹ imọ-ẹrọ.
Ni afikun si ohun gbogbo, ijẹrisi iṣe deede yoo jẹ pataki ni ibeere fun eyikeyi awọn ifowo siwe: igbagbogbo ko ṣee ṣe lati ṣatunṣe aṣiṣe adehun lẹhin ti o ti ṣe ifilọlẹ.
Ati pe idiyele iru awọn aṣiṣe bẹ le ga pupọ, nitori iye owo ti o tobi pupọ ti wa ni ipamọ nigbagbogbo lori awọn adehun ọlọgbọn.
Ẹrọ foju aami mi ni kikọ ni PHP ati Python, o si nlo Z3Prover lati inu Iwadi Microsoft lati yanju awọn agbekalẹ SMT ti o yọrisi.
Ni awọn oniwe-mojuto ni a alagbara olona-idunadura search, eyi ti
gba ọ laaye lati wa awọn solusan tabi awọn ailagbara, paapaa ti o ba nilo ọpọlọpọ awọn iṣowo.
Ani awọn , Ọkan ninu awọn ilana aami ti o lagbara julọ fun wiwa awọn ailagbara Ethereum, nikan fi kun agbara yii ni awọn osu diẹ sẹhin.
Ṣugbọn o tọ lati ṣe akiyesi pe awọn adehun ether jẹ eka sii ati pe Turing ti pari.
PHP tumọ koodu orisun ti adehun ijafafa RIDE sinu iwe afọwọkọ Python, ninu eyiti eto naa ti gbekalẹ bi eto ibaramu Z3 SMT ti awọn ipinlẹ adehun ati awọn ipo fun awọn iyipada wọn:
Bayi Emi yoo ṣe apejuwe ohun ti n ṣẹlẹ inu ni awọn alaye diẹ sii.
Ṣugbọn akọkọ, awọn ọrọ diẹ nipa ede adehun ijafafa RIDE.
O jẹ ede siseto iṣẹ-ṣiṣe ati ikosile ti o jẹ ọlẹ nipasẹ apẹrẹ.
RIDE nṣiṣẹ ni ipinya laarin blockchain ati pe o le gba pada ati kọ alaye lati ibi ipamọ ti o sopọ mọ apamọwọ olumulo.
O le so iwe adehun RIDE kan si apamọwọ kọọkan, ati abajade ti ipaniyan yoo jẹ TÒÓTỌ tabi Eke nikan.
TÒÓTỌ tumo si wipe smart guide faye gba awọn idunadura, ati FALSE tumo si o fàyègba o.
Apeere ti o rọrun: iwe afọwọkọ le ṣe idiwọ gbigbe kan ti iwọntunwọnsi apamọwọ ba kere ju 100.
Bi apẹẹrẹ, Emi yoo mu Wolf kanna, Ewúrẹ, ati eso kabeeji, ṣugbọn ti gbekalẹ tẹlẹ ni irisi adehun ọlọgbọn kan.
Olumulo naa kii yoo ni anfani lati yọ owo kuro ninu apamọwọ ti a fiweranṣẹ naa titi o fi fi gbogbo eniyan ranṣẹ si apa keji.
#Извлекаем положение всех объектов из блокчейна
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 kọkọ yọ gbogbo awọn oniyipada jade lati inu adehun ọlọgbọn ni irisi awọn bọtini wọn ati iyipada ikosile Boolean ti o baamu.
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 lẹhinna yi wọn pada si apejuwe eto ibaramu Z3Prover SMT ni Python.
Awọn data ti wa ni we ni a lupu, ibi ti ipamọ oniyipada gba Atọka i, idunadura oniyipada atọka i + 1, ati oniyipada pẹlu expressions ṣeto awọn ofin fun iyipada lati išaaju ipinle si tókàn.
Eyi ni ọkan-ọkan ti ẹrọ fojufoju wa, eyiti o pese ẹrọ wiwa ti iṣowo pupọ.
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] )
Awọn ipo ti wa ni lẹsẹsẹ ati fi sii sinu awoṣe iwe afọwọkọ ti a ṣe lati ṣe apejuwe eto SMT ni Python.
Awoṣe òfo
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()
Fun awọn ti o kẹhin ipinle ni gbogbo pq, awọn ofin ti o ti wa ni pato ninu awọn gbigbe idunadura apakan ti wa ni lo.
Eyi tumọ si pe Z3Prover yoo wa deede iru awọn ipo ti awọn ipo ti yoo gba awọn owo laaye lati yọkuro kuro ninu adehun naa.
Bi abajade, a laifọwọyi gba awoṣe SMT ti o ṣiṣẹ ni kikun ti adehun wa.
O le rii pe o jọra pupọ si awoṣe lati nkan iṣaaju mi, eyiti Mo ṣajọ pẹlu ọwọ.
Awoṣe ti o ti pari
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()
Lẹhin ifilọlẹ, Z3Prover yanju adehun ọlọgbọn ati pese wa pẹlu pq awọn iṣowo ti yoo gba wa laaye lati yọ owo kuro:
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
Ni afikun si adehun ọkọ oju omi, o le ṣe idanwo pẹlu awọn adehun tirẹ tabi gbiyanju apẹẹrẹ ti o rọrun yii, eyiti o yanju ni awọn iṣowo 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
}
Niwọn igba ti eyi jẹ ẹya akọkọ pupọ, sintasi naa ni opin pupọ ati pe awọn idun le wa.
Ninu awọn nkan wọnyi, Mo gbero lati bo idagbasoke siwaju ti VM, ati ṣafihan bi o ṣe le ṣẹda awọn adehun oye ti o ni idaniloju pẹlu iranlọwọ rẹ, kii ṣe yanju wọn nikan.
Ẹrọ foju ohun kikọ wa ni
Lẹhin fifi koodu orisun ti VM aami ni aṣẹ ati ṣafikun awọn asọye nibẹ, Mo gbero lati fi si GitHub fun iwọle ọfẹ.
orisun: www.habr.com