Расмий текшерүү – бул бир программаны же алгоритмди башкасын колдонуу менен текшерүү.
Бул программадагы бардык кемчиликтерди табууга же алардын жок экенин далилдөөгө мүмкүндүк берген эң күчтүү ыкмалардын бири.
Формалдуу текшерүүнүн кеңири сүрөттөлүшүн маселени чечүүнүн мисалында көрүүгө болот менин мурунку макаламда.
Бул макалада мен көйгөйлөрдү формалдуу текшерүүдөн программаларга өтүп, кантип сүрөттөп берем
аларды кантип автоматтык түрдө формалдуу эреже системаларына айландырса болот.
Бул үчүн мен символикалык принциптерди колдонуп, виртуалдык машинанын өз аналогун жаздым.
Ал программалык кодду талдап, аны программалык түрдө чечүүгө мүмкүн болгон теңдемелер системасына (SMT) которот.
Символикалык эсептөөлөр жөнүндө маалымат Интернетте үзүндү түрдө берилгендиктен,
Мен анын эмне экенин кыскача айтып берейин.
Символикалык эсептөө – бул программаны бир эле учурда кеңири диапазондо аткаруунун жолу жана программаны формалдуу текшерүүнүн негизги куралы.
Мисалы, биз биринчи аргумент каалаган оң маанилерди, экинчи терс, үчүнчү нөл жана чыгуу аргументи, мисалы, 42 кабыл ала турган киргизүү шарттарын орното алабыз.
Символикалык эсептөөлөр бизге каалаган натыйжаны алуу мүмкүнбү деген суроого жооп берет жана мындай киргизүү параметрлеринин жыйындысынын мисалын берет. Же андай параметрлер жок экендигинин далили.
Мындан тышкары, биз киргизүү аргументтерин бардык мүмкүн болгон аргументтерге коюп, бир гана чыгарууну тандай алабыз, мисалы, администратордун сырсөзүн.
Бул учурда, биз программанын бардык кемчиликтерин табабыз же администратордун сырсөзүнүн коопсуз экендигинин далилин алабыз.
Белгилүү киргизүү маалыматтары менен программанын классикалык аткарылышы символикалык аткаруунун өзгөчө учуру экенин белгилей кетүү керек.
Ошондуктан, менин каарманым VM стандарттык виртуалдык машинанын эмуляция режиминде да иштей алат.
Мурунку макалага комментарийлерде анын алсыз жактарын талкуулоо менен формалдуу текшерүүнү адилеттүү сынга алууга болот.
негизги көйгөйлөр болуп төмөнкүлөр саналат:
- Комбинатордук жарылуу, анткени формалдуу текшерүү акыры P=NPге чейин жетет
- Файлдык тутумга, тармактарга жана башка тышкы сактагычка чалууларды иштетүүнү текшерүү кыйыныраак
- Спецификациядагы мүчүлүштүктөр, кардар же программист бир нерсеге ниеттенип, бирок техникалык спецификацияда аны жетиштүү түрдө так сүрөттөп бербеген.
Натыйжада, программа текшерилет жана спецификацияга ылайык келет, бирок жаратуучулар андан күткөндөн таптакыр башка нерсени жасайт.
Бул макалада мен негизинен расмий текшерүүнү практикада колдонууну карап жаткандыктан, мен азыр башымды дубалга урбайм, алгоритмдик татаалдыгы жана тышкы чалуулардын саны минималдуу болгон системаны тандайм.
Акылдуу келишимдер бул талаптарга эң ылайыктуу болгондуктан, тандоо Waves платформасындагы RIDE келишимдерине туура келген: алар Тьюринг толук эмес жана алардын максималдуу татаалдыгы жасалма түрдө чектелген.
Бирок биз аларды техникалык жактан гана карайбыз.
Мындан тышкары, расмий текшерүү ар кандай келишимдер үчүн өзгөчө суроо-талапка ээ болот: ал ишке киргизилгенден кийин келишим катасын оңдоо мүмкүн эмес.
Ал эми мындай каталардын баасы өтө чоң болушу мүмкүн, анткени көп учурда акылдуу контракттарда көп каражаттар сакталат.
Менин символикалык виртуалдык машинам PHP жана Python тилдеринде жазылган жана натыйжада SMT формулаларын чечүү үчүн Microsoft Research компаниясынан Z3Prover колдонот.
Анын өзөгүн күчтүү көп транзакциялуу издөө түзөт
көптөгөн транзакцияларды талап кылса да, чечимдерди же аялуу жерлерди табууга мүмкүндүк берет.
ал тургай, , Ethereum аялуу табуу үчүн абдан күчтүү каймана алкактарынын бири, бир нече ай мурун гана бул мүмкүнчүлүктү кошкон.
Бирок бул эфир келишимдери татаал жана Тьюринг толук экенин белгилей кетүү керек.
PHP RIDE акылдуу келишиминин баштапкы кодун питон скриптине которот, мында программа келишим мамлекеттеринин жана алардын өтүү шарттарынын Z3 SMT шайкеш системасы катары берилген:
Эми мен ичинде эмне болуп жатканын кененирээк сүрөттөп берем.
Бирок, биринчиден, RIDE акылдуу келишим тили жөнүндө бир нече сөз.
Бул дизайн боюнча жалкоо функционалдык жана экспрессияга негизделген программалоо тили.
RIDE блокчейндин ичинде обочолонуп иштейт жана колдонуучунун капчыгына байланышкан сактагычтан маалыматты алып жана жаза алат.
Сиз ар бир капчыкка RIDE келишимин тиркөөгө болот жана аткаруунун натыйжасы ЧЫНДЫК же ЖАЛГАН гана болот.
TRUE акылдуу келишим транзакцияга уруксат берет, ал эми ЖАЛГАН ага тыюу салат дегенди билдирет.
Жөнөкөй мисал: эгер капчыктын балансы 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 аларды Pythonдо Z3Prover SMT-шайкеш системанын сүрөттөмөсүнө айлантат.
Маалыматтар циклге оролгон, мында сактагыч өзгөрмөлөр индекси 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] )
Шарттар иргелип, Pythonдо SMT тутумун сүрөттөө үчүн иштелип чыккан скрипт шаблонуна киргизилет.
Бош шаблон
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'ка бекер жетүү үчүн коюуну пландап жатам.
Source: www.habr.com