رسمي تایید د یو پروګرام یا د بل په کارولو سره د الګوریتم تصدیق دی.
دا یو له خورا پیاوړې میتودونو څخه دی چې تاسو ته اجازه درکوي په برنامه کې ټول زیانونه ومومئ یا ثابت کړئ چې دوی شتون نلري.
د رسمي تایید نور تفصيلي توضیحات د ستونزې حل کولو مثال کې لیدل کیدی شي زما په تیرو مقاله کې.
پدې مقاله کې زه د ستونزو رسمي تایید څخه برنامو ته حرکت کوم او تشریح کوم چې څنګه
دوی څنګه په اتوماتيک ډول د رسمي قواعدو سیسټمونو کې بدلیدلی شي.
د دې کولو لپاره، ما د سمبولیک اصولو په کارولو سره د مجازی ماشین خپل انلاګ ولیکه.
دا د پروګرام کوډ تجزیه کوي او دا د مساواتو سیسټم (SMT) ته ژباړي، کوم چې دمخه په پروګرام کې حل کیدی شي.
څرنګه چې د سمبولیک حسابونو په اړه معلومات په انټرنیټ کې وړاندې شوي نه په ټوټه ټوټه،
زه به په لنډه توګه تشریح کړم چې دا څه دي.
سمبولیک محاسبه د ډیټا په پراخه لړۍ کې د برنامه اجرا کولو یوه لاره ده او د رسمي برنامې تصدیق لپاره اصلي وسیله ده.
د مثال په توګه، موږ کولی شو د ننوتلو شرایط تنظیم کړو چیرې چې لومړی دلیل کولی شي کوم مثبت ارزښتونه واخلي، دویم منفي، دریم صفر، او د تولید دلیل، د بیلګې په توګه، 42.
سمبولیک حسابونه به موږ ته دا ځواب راکړي چې ایا دا ممکنه ده چې مطلوب پایله ترلاسه کړو او د ورته ان پټ پیرامیټرو سیټ مثال. یا ثبوت چې داسې پیرامیټونه شتون نلري.
برسېره پردې، موږ کولی شو د ان پټ دلیلونه ټولو ممکنه کسانو ته وټاکو، او یوازې د محصولاتو غوره کول، د بیلګې په توګه، د مدیر پاسورډ.
په دې حالت کې، موږ به د پروګرام ټول زیانونه ومومئ یا دا ثبوت ترلاسه کړو چې د مدیر پټنوم خوندي دی.
د یادونې وړ ده چې د ځانګړي ان پټ ډیټا سره د برنامې کلاسیک اجرا کول د سمبولیک اجرا کولو ځانګړې قضیه ده.
له همدې امله ، زما کرکټر VM کولی شي د معیاري مجازی ماشین ایمولیشن حالت کې هم کار وکړي.
د تیرې مقالې په نظرونو کې یو څوک کولی شي د دې ضعیف بحث سره د رسمي تایید عادلانه انتقاد ومومي.
اصلي ستونزې دا دي:
- ګډې چاودنې، ځکه چې رسمي تایید په پای کې P=NP ته راځي
- د فایل سیسټم، شبکو او نورو خارجي ذخیرې ته د تلیفونونو پروسس کول تصدیق کول خورا ستونزمن دي
- په مشخصاتو کې کیګونه ، کله چې پیرودونکي یا برنامه یو شی اراده کړي ، مګر په تخنیکي توضیحاتو کې یې په کافي اندازه توضیح نه کوي.
د پایلې په توګه ، برنامه به تایید شي او د توضیحاتو سره مطابقت ولري ، مګر یو څه به په بشپړ ډول د هغه څه څخه توپیر وکړي چې جوړونکي یې تمه درلوده.
څرنګه چې پدې مقاله کې زه په اصل کې په عمل کې د رسمي تایید کارولو په اړه فکر کوم، زه به د اوس لپاره خپل سر د دیوال په وړاندې ودروم، او یو سیسټم به غوره کړم چیرې چې د الګوریتمیک پیچلتیا او د بهرنیو تلیفونونو شمیر لږ وي.
څرنګه چې سمارټ قراردادونه د دې اړتیاو سره سم دي، انتخاب د ویوز پلیټ فارم څخه د RIDE قراردادونو باندې راوتلی: دوی بشپړ ندي، او د دوی اعظمي پیچلتیا په مصنوعي توګه محدوده ده.
مګر موږ به دوی په ځانګړي ډول د تخنیکي اړخ څخه په پام کې ونیسو.
د هر څه سربیره، رسمي تایید به په ځانګړې توګه د هر ډول قراردادونو په غوښتنه کې وي: دا معمولا ناشونې ده چې د تړون خطا د پیل کولو وروسته سم شي.
او د دې ډول غلطیتونو لګښت خورا لوړ کیدی شي، ځکه چې ډیری پیسې په سمارټ قراردادونو کې ساتل کیږي.
زما سمبولیک مجازی ماشین په PHP او Python کې لیکل شوی، او د مایکروسافټ ریسرچ څخه Z3Prover کاروي ترڅو د پایلې SMT فورمول حل کړي.
د دې په اصلي برخه کې یو پیاوړی څو اړخیزه لټون دی، کوم چې
تاسو ته اجازه درکوي حلونه یا زیانونه ومومئ، حتی که دا ډیری معاملو ته اړتیا ولري.
حتی ، د Ethereum زیانونو موندلو لپاره یو له خورا پیاوړي سمبولیک چوکاټ څخه ، یوازې څو میاشتې دمخه دا وړتیا اضافه کړه.
مګر دا د یادونې وړ ده چې د ایتر قراردادونه خورا پیچلي او د تورینګ بشپړ دي.
PHP د RIDE سمارټ قرارداد سرچینې کوډ په پیتون سکریپټ کې وژباړي، په کوم کې چې برنامه د Z3 SMT سره مطابقت لرونکي سیسټم په توګه وړاندې کیږي د قرارداد حالتونو او د دوی د لیږد لپاره شرایط:
اوس زه به په تفصیل سره تشریح کړم چې دننه څه پیښیږي.
مګر لومړی، د RIDE سمارټ قرارداد ژبې په اړه یو څو ټکي.
دا یوه فعاله او د بیان پراساس برنامه ژبه ده چې د ډیزاین لخوا سست ده.
RIDE د بلاکچین دننه په انزوا کې پرمخ ځي او کولی شي د کارونکي بټوې پورې تړلي ذخیره کولو څخه معلومات ترلاسه او ولیکئ.
تاسو کولی شئ په هر بټوه کې د RIDE قرارداد ضمیمه کړئ، او د اجرا کولو پایله به یوازې ریښتیا یا غلط وي.
ریښتیا پدې مانا ده چې سمارټ قرارداد د لیږد اجازه ورکوي، او 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 بیا دوی په 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 سرچینې کوډ په ترتیب کولو او هلته د نظرونو اضافه کولو وروسته ، زه پلان لرم چې دا د وړیا لاسرسي لپاره ګیټ هب کې واچوم.
سرچینه: www.habr.com