Санҷиши расмӣ ин санҷиши як барнома ё алгоритм бо истифода аз барномаи дигар мебошад.
Ин яке аз усулҳои пурқувватест, ки ба шумо имкон медиҳад тамоми осебпазириҳои барномаро пайдо кунед ё исбот кунед, ки онҳо вуҷуд надоранд.
Тавсифи муфассали санҷиши расмиро дар мисоли ҳалли масъала дидан мумкин аст дар мақолаи қаблии ман.
Дар ин мақола ман аз санҷиши расмии мушкилот ба барномаҳо мегузарам ва тавсиф мекунам, ки чӣ тавр
чӣ тавр онҳо метавонанд ба таври худкор ба системаҳои қоидаҳои расмӣ табдил дода шаванд.
Барои ин ман аналоги шахсии мошини виртуалиро бо истифода аз принсипҳои рамзӣ навиштам.
Он рамзи барномаро таҳлил мекунад ва онро ба системаи муодилаҳо (SMT) тарҷума мекунад, ки онро аллакай ба таври барномавӣ ҳал кардан мумкин аст.
Азбаски маълумот дар бораи ҳисобҳои рамзӣ дар Интернет ба таври ҷудогона пешниҳод карда мешавад,
Ман ба таври мухтасар тавсиф мекунам, ки он чӣ аст.
Ҳисобкунии рамзӣ роҳи дар як вақт иҷро кардани барнома дар доираи васеи додаҳо буда, воситаи асосии санҷиши расмии барнома мебошад.
Масалан, мо метавонем шартҳои вурудро муқаррар кунем, ки дар он аргументи аввал метавонад ҳама гуна қиматҳои мусбӣ, дуюм манфӣ, сифри сеюм ва аргументи баромадро, масалан, 42 қабул кунад.
Ҳисобҳои рамзӣ дар як давр ба мо ҷавоб медиҳанд, ки оё имкон дорад, ки мо натиҷаи дилхоҳро ба даст орем ва намунаи маҷмӯи чунин параметрҳои воридотӣ. Ё далели он, ки чунин параметрҳо вуҷуд надоранд.
Ғайр аз он, мо метавонем далелҳои вурудро ба ҳама далелҳои имконпазир муқаррар кунем ва танҳо далелҳои баромадро интихоб кунем, масалан, пароли администратор.
Дар ин ҳолат, мо тамоми осебпазирии барномаро пайдо хоҳем кард ё далели бехатар будани пароли администраторро ба даст меорем.
Қайд кардан мумкин аст, ки иҷрои классикии барнома бо маълумоти мушаххаси воридшуда як ҳолати махсуси иҷрои рамзӣ мебошад.
Аз ин рӯ, хислати ман VM инчунин метавонад дар реҷаи эмуляцияи як мошини стандартии виртуалӣ кор кунад.
Дар шарҳҳои мақолаи қаблӣ метавон танқиди одилонаро аз санҷиши расмӣ бо муҳокимаи камбудиҳои он пайдо кард.
Мушкилоти асосӣ инҳоянд:
- Таркишҳои комбинаторӣ, зеро санҷиши расмӣ дар ниҳоят ба P = NP мерасад
- Санҷиши коркарди зангҳо ба системаи файлӣ, шабакаҳо ва дигар нигаҳдории беруна мушкилтар аст
- Хатогиҳо дар мушаххасот, вақте ки фармоишгар ё барномасоз як чизро ният карда буд, аммо онро дар тавсифи техникӣ ба таври кофӣ дақиқ тавсиф накардааст.
Дар натиҷа, барнома санҷида мешавад ва ба мушаххасот мувофиқат мекунад, аммо аз он чизе, ки эҷодкорон аз он интизор буданд, комилан фарқ мекунад.
Азбаски дар ин мақола ман асосан истифодаи санҷиши расмиро дар амал баррасӣ мекунам, ман ҳоло сари худро ба девор намезанам ва системаеро интихоб мекунам, ки мураккабии алгоритмӣ ва шумораи зангҳои беруна ҳадди ақалл бошад.
Азбаски шартномаҳои оқилона ба ин талабот мувофиқат мекунанд, интихоб ба шартномаҳои RIDE аз платформаи Waves афтод: онҳо Тюринг пурра нестанд ва мураккабии максималии онҳо ба таври сунъӣ маҳдуд аст.
Аммо мо онҳоро танҳо аз ҷониби техникӣ баррасӣ хоҳем кард.
Илова ба ҳама чиз, санҷиши расмӣ махсусан барои ҳама гуна шартномаҳо талаб карда мешавад: одатан ислоҳ кардани хатогии шартнома пас аз оғози он ғайриимкон аст.
Ва арзиши чунин хатогиҳо метавонад хеле баланд бошад, зеро миқдори зиёди маблағҳо аксар вақт дар шартномаҳои интеллектуалӣ нигоҳ дошта мешаванд.
Мошини виртуалии рамзии ман дар PHP ва Python навишта шудааст ва Z3Prover аз Microsoft Research барои ҳалли формулаҳои SMT-ро истифода мебарад.
Дар асо-си он чустучуи пуриктидори бисёр-трансакционй, ки
ба шумо имкон медиҳад, ки ҳалли мушкилот ё осебпазириро пайдо кунед, ҳатто агар он амалиёти зиёдеро талаб кунад.
Ҳатто , яке аз пурқувваттарин чаҳорчӯбаҳои рамзӣ барои дарёфти осебпазирии Ethereum, танҳо чанд моҳ пеш ин қобилиятро илова кард.
Аммо бояд қайд кард, ки шартномаҳои эфирӣ мураккабтар ва Тюринг пурра мебошанд.
PHP рамзи сарчашмаи шартномаи интеллектуалии RIDE-ро ба скрипти python тарҷума мекунад, ки дар он барнома ҳамчун системаи мувофиқи Z3 SMT ҳолати шартнома ва шартҳои гузариши онҳо пешниҳод карда мешавад:
Ҳоло ман дар дохили он чӣ рӯй дода истодааст, муфассалтар тасвир мекунам.
Аммо аввал, чанд сухан дар бораи забони шартномаи интеллектуалии RIDE.
Ин як забони барномасозии функсионалӣ ва ифодаист, ки аз рӯи тарҳ танбал аст.
RIDE дар ҷудогона дар дохили blockchain кор мекунад ва метавонад маълумотро аз анборе, ки ба ҳамёни корбар алоқаманд аст, дарёфт ва нависад.
Шумо метавонед ба ҳар як ҳамён шартномаи RIDE замима кунед ва натиҷаи иҷро танҳо TRUE ё FALSE хоҳад буд.
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 мувофиқ дар Python табдил медиҳад.
Маълумот дар як ҳалқа печонида мешавад, ки дар он тағирёбандаҳои нигаҳдорӣ индекси 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 дар Python тарҳрезӣ карда мешаванд ва ворид карда мешаванд.
Шаблон холӣ
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
}
Азбаски ин версияи аввалин аст, синтаксис хеле маҳдуд аст ва хатогиҳо вуҷуд доранд.
Дар мақолаҳои зерин, ман нақша дорам, ки рушди минбаъдаи VM-ро фаро гирам ва нишон диҳам, ки чӣ гуна шумо метавонед бо ёрии он шартномаҳои интеллектуалии расман тасдиқшуда эҷод кунед, на танҳо онҳоро ҳал кунед.
Мошини виртуалии аломат дар он дастрас аст
Пас аз ба тартиб даровардани рамзи сарчашмаи VM рамзӣ ва илова кардани шарҳҳо, ман ният дорам, ки онро дар GitHub барои дастрасии ройгон ҷойгир кунам.
Манбаъ: will.com