Tabbatarwa na yau da kullun shine tabbatar da shirin ɗaya ko algorithm ta amfani da wani.
Wannan hanya ce mafi ƙarfi wacce ke ba ku damar nemo duk lahani a cikin shirin ko tabbatar da cewa babu su.
Ana iya ganin ƙarin cikakken bayanin tabbaci na yau da kullun a cikin misalin warware matsalar a labarina na baya.
A cikin wannan labarin na ƙaura daga tabbatar da matsaloli na yau da kullun zuwa shirye-shirye da bayyana yadda
ta yaya za a iya canza su zuwa tsarin mulki na yau da kullun ta atomatik.
Don yin wannan, na rubuta nawa analogue na injin kama-da-wane, ta amfani da ƙa'idodin alama.
Yana rarraba lambar shirin kuma ya fassara shi zuwa tsarin daidaitawa (SMT), wanda za a iya warware shi ta hanyar shirye-shirye.
Tun da yake an gabatar da bayanai game da ƙididdiga na alama akan Intanet maimakon ɓarna.
Zan yi bayanin abin da yake a takaice.
Ƙididdigar alamar wata hanya ce ta aiwatar da shirin a lokaci guda akan bayanai masu yawa kuma shine babban kayan aiki don tabbatar da shirin na yau da kullun.
Misali, zamu iya saita yanayin shigarwa inda hujja ta farko zata iya ɗaukar kowane ƙima mai kyau, na biyu mara kyau, sifili na uku, da hujjar fitarwa, misali, 42.
Ƙididdigar alamomi a cikin gudu ɗaya zai ba mu amsar ko zai yiwu mu sami sakamakon da ake so da kuma misali na saitin irin waɗannan sigogin shigarwa. Ko tabbacin cewa babu irin waɗannan sigogi.
Bugu da ƙari, za mu iya saita gardamar shigarwa zuwa duk masu yiwuwa, kuma zaɓi waɗanda aka fitar kawai, misali, kalmar sirri na mai gudanarwa.
A wannan yanayin, za mu sami duk raunin shirin ko samun tabbacin cewa kalmar sirrin mai gudanarwa ba ta da lafiya.
Ana iya lura da cewa aiwatar da shirye-shirye na gargajiya tare da takamaiman bayanan shigarwa wani lamari ne na musamman na kisa na alama.
Don haka, halina VM kuma yana iya aiki a cikin yanayin kwaikwayi na ingantacciyar injin kama-da-wane.
A cikin sharhin labarin da ya gabata za a iya samun sukar gaskiya game da tabbatarwa na yau da kullun tare da tattaunawa kan rauninsa.
Manyan matsalolin su ne:
- Fashewar haɗin gwiwa, tunda tabbaci na yau da kullun ya sauko zuwa P=NP
- Gudanar da kira zuwa tsarin fayil, cibiyoyin sadarwa da sauran ma'ajiyar waje ya fi wahalar tantancewa
- Bugs a cikin ƙayyadaddun bayanai, lokacin da abokin ciniki ko mai tsara shirye-shirye suka yi nufin abu ɗaya, amma bai bayyana shi daidai ba a cikin ƙayyadaddun fasaha.
Sakamakon haka, shirin za a tabbatar da shi kuma ya bi ƙayyadaddun ƙayyadaddun bayanai, amma zai yi wani abu da ya bambanta da abin da masu ƙirƙira suke tsammani daga gare shi.
Tun da a cikin wannan labarin na fi la'akari da yin amfani da tabbaci na yau da kullun a aikace, ba zan buga kaina a bango a yanzu ba, kuma zan zaɓi tsarin da ƙayyadaddun algorithmic da adadin kiran waje ba su da yawa.
Tunda kwangiloli masu wayo sun fi dacewa da waɗannan buƙatun, zaɓin ya faɗi akan kwangilolin RIDE daga dandamali na Waves: ba su cika Turing ba, kuma matsakaicin matsakaicin ƙarfin su yana iyakance.
Amma za mu yi la'akari da su musamman daga bangaren fasaha.
Baya ga komai, tabbatarwa na yau da kullun zai kasance musamman a buƙatar kowane kwangila: yawanci ba shi yiwuwa a gyara kuskuren kwangila bayan an ƙaddamar da shi.
Kuma farashin irin waɗannan kurakurai na iya zama babba, tunda yawancin kuɗi ana adana su akan kwangiloli masu wayo.
An rubuta na'ura ta alama ta a cikin PHP da Python, kuma tana amfani da Z3Prover daga Microsoft Research don warware sakamakon SMT dabaru.
A ainihinsa akwai bincike mai ƙarfi da yawa, wanda
yana ba ku damar nemo mafita ko lahani, koda kuwa yana buƙatar ma'amaloli da yawa.
Ko da , ɗaya daga cikin mafi girman ƙaƙƙarfan tsarin alamar alama don gano raunin Ethereum, kawai ya kara wannan damar 'yan watanni da suka wuce.
Amma yana da mahimmanci a lura cewa kwangilar ether sun fi rikitarwa kuma Turing cikakke.
PHP yana fassara lambar tushe na kwangilar wayo ta RIDE zuwa rubutun Python, wanda aka gabatar da shirin azaman tsarin Z3 SMT mai jituwa na jihohin kwangila da yanayin canjin su:
Yanzu zan yi bayanin abin da ke faruwa a ciki daki-daki.
Amma da farko, ƴan kalmomi game da yaren kwangilar wayo na RIDE.
Yaren shirye-shirye ne mai aiki da magana wanda ke da kasala ta hanyar ƙira.
RIDE yana gudana a keɓance a cikin blockchain kuma yana iya dawo da rubuta bayanai daga ma'adanar da ke da alaƙa da jakar mai amfani.
Kuna iya haɗa kwangilar RIDE zuwa kowane walat, kuma sakamakon aiwatarwa zai zama GASKIYA ko KARYA kawai.
GASKIYA yana nufin cewa kwangila mai wayo yana ba da izinin ciniki, kuma KARYA yana nufin ya hana shi.
Misali mai sauƙi: rubutun zai iya hana canja wuri idan ma'aunin walat ɗin bai wuce 100 ba.
A matsayin misali, zan ɗauki Wolf iri ɗaya, Goat, da Kabeji, amma an riga an gabatar da su ta hanyar kwangilar wayo.
Mai amfani ba zai iya cire kuɗi daga walat ɗin da aka sanya kwangilar ba har sai ya aika kowa da kowa zuwa wancan gefe.
#Извлекаем положение всех объектов из блокчейна
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 ya fara fitar da duk masu canji daga kwangilar wayo ta hanyar maɓallan su da madaidaicin furcin Boolean.
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 sannan ya canza su zuwa bayanin tsarin Z3Prover SMT mai jituwa a cikin Python.
An nannade bayanan a cikin madauki, inda masu canjin ajiya ke karɓar fihirisar i, masu canjin ma'amalar ma'amalar i + 1, da masu canji tare da maganganu suna saita ƙa'idodi don sauyawa daga jihar da ta gabata zuwa na gaba.
Wannan ita ce ainihin zuciyar injin mu, wanda ke ba da tsarin neman ma'amala da yawa.
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] )
An jera sharuɗɗan kuma an saka su cikin samfurin rubutun da aka tsara don kwatanta tsarin SMT a Python.
Samfurin Blank
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()
Don jihar ta ƙarshe a cikin dukan sarkar, ana amfani da ka'idodin da aka ƙayyade a cikin sashin musayar musayar.
Wannan yana nufin cewa Z3Prover zai nemo daidai irin waɗannan sharuɗɗan da za su ba da izinin cire kuɗi daga kwangilar.
Sakamakon haka, muna karɓar cikakken samfurin SMT na kwangilar mu ta atomatik.
Kuna iya ganin cewa yana kama da samfurin daga labarin da na gabata, wanda na tattara da hannu.
Samfurin da ya cika
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()
Bayan ƙaddamarwa, Z3Prover yana warware kwangilar wayo kuma yana ba mu jerin ma'amaloli waɗanda za su ba mu damar karɓar kuɗi:
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
Baya ga kwangilar jirgin ruwa, zaku iya gwaji tare da kwangilolin ku ko gwada wannan misali mai sauƙi, wanda aka warware a cikin ma'amaloli 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
}
Tunda wannan shine sigar farko ta farko, tsarin haɗin gwiwar yana da iyaka sosai kuma ana iya samun kurakurai.
A cikin labarai masu zuwa, na yi shirin rufe ci gaban ci gaban VM, kuma in nuna yadda zaku iya ƙirƙirar kwangiloli masu kaifin basira tare da taimakon sa, ba kawai warware su ba.
Ana samun injin kama-da-wane a
Bayan sanya lambar tushe na VM na alama a cikin tsari da ƙara sharhi a can, na shirya sanya shi akan GitHub don samun dama kyauta.
source: www.habr.com