شروع کان هڪ رسمي تصديق واري نظام ٺاهڻ. حصو 1: PHP ۽ پٿون ۾ ڪردار ورچوئل مشين

رسمي تصديق هڪ پروگرام يا ٻئي استعمال ڪندي الگورتھم جي تصديق آهي.

هي هڪ تمام طاقتور طريقن مان آهي جيڪو توهان کي پروگرام ۾ سڀني ڪمزورين کي ڳولڻ جي اجازت ڏئي ٿو يا ثابت ڪري ٿو ته اهي موجود نه آهن.

رسمي تصديق جي وڌيڪ تفصيلي وضاحت جي مسئلي کي حل ڪرڻ جي مثال ۾ ڏسي سگھجي ٿو بگھڙ، ٻڪري ۽ گوبي منهنجي پوئين مضمون ۾.

هن آرٽيڪل ۾ آئون مسئلن جي رسمي تصديق کان پروگرامن ڏانهن منتقل ڪريان ٿو ۽ بيان ڪريان ٿو ته ڪيئن
انهن کي ڪيئن خودڪار طريقي سان رسمي ضابطي جي نظام ۾ تبديل ڪري سگهجي ٿو.

هن کي ڪرڻ لاء، مون هڪ مجازي مشين جو پنهنجو اينالاگ لکيو، علامتي اصولن کي استعمال ڪندي.

اهو پروگرام ڪوڊ کي پارس ڪري ٿو ۽ ان کي مساوات جي سسٽم (SMT) ۾ ترجمو ڪري ٿو، جيڪو اڳ ۾ ئي پروگرام سان حل ڪري سگهجي ٿو.

جيئن ته علامتي حسابن بابت معلومات انٽرنيٽ تي پيش ڪئي وئي آهي بلڪه ٽڪرا ٽڪرا،
مان مختصر طور بيان ڪندس ته اهو ڇا آهي.

علامتي ڳڻپيوڪر هڪ طريقو آهي هڪ پروگرام کي گڏ ڪرڻ لاءِ هڪ ئي وقت ۾ ڊيٽا جي وسيع رينج تي ۽ رسمي پروگرام جي تصديق لاءِ مکيه اوزار آهي.

مثال طور، اسان ان پٽ شرطن کي سيٽ ڪري سگھون ٿا جتي پھريون دليل ڪو به مثبت قدر وٺي سگھي ٿو، ٻيو منفي، ٽيون صفر، ۽ ٻاھرين دليل، مثال طور، 42.

هڪ رن ۾ سمبولڪ حساب اسان کي اهو جواب ڏيندو ته ڇا اسان لاءِ گهربل نتيجو حاصل ڪرڻ ممڪن آهي ۽ اهڙي ان پٽ پيرا ميٽرن جي سيٽ جو هڪ مثال. يا ثبوت آهي ته اهڙا ڪي به معيار نه آهن.

ان کان علاوه، اسان ان پٽ دليلن کي سيٽ ڪري سگھون ٿا سڀني ممڪنن لاءِ، ۽ صرف آئوٽ پُٽ کي چونڊيو، مثال طور، ايڊمنسٽريٽر پاسورڊ.

انهي صورت ۾، اسان پروگرام جي سڀني ڪمزورين کي ڳوليندا سين يا ثبوت حاصل ڪنداسين ته منتظم جو پاسورڊ محفوظ آهي.

اهو نوٽ ڪري سگهجي ٿو ته مخصوص ان پٽ ڊيٽا سان گڏ هڪ پروگرام جي ڪلاسيڪل عملدرآمد علامتي عمل جي هڪ خاص صورت آهي.

تنهن ڪري، منهنجو ڪردار VM هڪ معياري مجازي مشين جي ايموليشن موڊ ۾ پڻ ڪم ڪري سگهي ٿو.

پوئين مضمون جي تبصرن ۾، توهان کي ان جي ڪمزورين جي بحث سان رسمي تصديق جي منصفانه تنقيد ڳولي سگهو ٿا.

مکيه مسئلا آهن:

  1. گڏيل ڌماڪو، ڇاڪاڻ ته رسمي تصديق آخرڪار P=NP تي اچي ٿي
  2. فائل سسٽم، نيٽ ورڪ ۽ ٻين خارجي اسٽوريج کي پروسيسنگ ڪالن جي تصديق ڪرڻ وڌيڪ ڏکيو آهي
  3. وضاحتن ۾ بگ، جڏهن گراهڪ يا پروگرامر هڪ شيء جو ارادو ڪيو، پر ٽيڪنيڪل وضاحتن ۾ ان کي صحيح طور تي بيان نه ڪيو.

نتيجي طور، پروگرام جي تصديق ڪئي ويندي ۽ وضاحت سان عمل ڪيو ويندو، پر ڪجهه مڪمل طور تي مختلف ڪندو جيڪو ان کان ٺاهيندڙن جي توقع ڪئي.

جيئن ته هن آرٽيڪل ۾ مان بنيادي طور تي عملي طور تي رسمي تصديق جي استعمال تي غور ڪري رهيو آهيان، مان هن وقت پنهنجو مٿو ڀت سان نه ٽنگندس، ۽ هڪ سسٽم چونڊيندس جتي الگورتھم پيچيدگي ۽ خارجي ڪالن جو تعداد گهٽ ۾ گهٽ هجي.

جيئن ته سمارٽ معاهدا انهن گهرجن کي بهترين طور تي پورو ڪن ٿا، چونڊ Waves پليٽ فارم تان RIDE معاهدي تي ٿي وئي: اهي ٽريننگ مڪمل نه آهن، ۽ انهن جي وڌ ۾ وڌ پيچيدگي مصنوعي طور تي محدود آهي.

پر اسان انهن تي غور ڪنداسين خاص طور تي ٽيڪنيڪل پاسي کان.

هر شي کان علاوه، رسمي تصديق خاص طور تي ڪنهن به معاهدي جي طلب ۾ هوندي: اهو عام طور تي ناممڪن آهي ته هڪ معاهدي جي غلطي کي درست ڪرڻ کان پوء ان کي شروع ڪيو ويو آهي.
۽ اهڙين غلطين جي قيمت تمام گهڻي ٿي سگهي ٿي، ڇاڪاڻ ته فنڊ جي وڏي مقدار اڪثر سمارٽ معاهدي تي ذخيرو ٿيل آهن.

منهنجي علامتي ورچوئل مشين PHP ۽ Python ۾ لکيل آهي، ۽ Microsoft ريسرچ مان Z3Prover استعمال ڪري ٿي نتيجي ۾ SMT فارمولن کي حل ڪرڻ لاءِ.

ان جي بنياد تي هڪ طاقتور ملٽي ٽرانزيڪشنل ڳولا آهي، جيڪا
توهان کي حل يا ڪمزوريون ڳولڻ جي اجازت ڏئي ٿي، جيتوڻيڪ اهو ڪيترن ئي ٽرانزيڪشن جي ضرورت آهي.
اڃا به ميٿرلEthereum جي ڪمزورين کي ڳولڻ لاء سڀ کان وڌيڪ طاقتور علامتي فريم ورڪ مان، صرف چند مهينا اڳ هن صلاحيت کي شامل ڪيو ويو آهي.

پر اهو نوٽ ڪرڻ جي قابل آهي ته ايٿير معاهدو وڌيڪ پيچيده ۽ ٽريننگ مڪمل آهن.

PHP RIDE سمارٽ ڪانٽريڪٽ جي سورس ڪوڊ کي پٿون اسڪرپٽ ۾ ترجمو ڪري ٿو، جنهن ۾ پروگرام پيش ڪيو ويو آهي Z3 SMT-مطابقت واري نظام جي معاهدي جي رياستن ۽ انهن جي منتقلي لاءِ شرط:

شروع کان هڪ رسمي تصديق واري نظام ٺاهڻ. حصو 1: PHP ۽ پٿون ۾ ڪردار ورچوئل مشين

هاڻي مان وڌيڪ تفصيل سان بيان ڪندس ته اندر ڇا ٿي رهيو آهي.

پر پهرين، RIDE سمارٽ معاهدي جي ٻولي بابت ڪجهه لفظ.

اها هڪ فنڪشنل ۽ اظهار جي بنياد تي پروگرامنگ ٻولي آهي جيڪا ڊيزائن جي لحاظ کان سست آهي.
RIDE بلاڪچين ۾ اڪيلائي ۾ هلندو آهي ۽ صارف جي والٽ سان ڳنڍيل اسٽوريج مان معلومات ٻيهر حاصل ڪري ۽ لکي سگهي ٿو.

توھان ھر ھڪ پرس سان RIDE معاهدو ڳنڍي سگھو ٿا، ۽ عمل جو نتيجو صرف سچ يا غلط ھوندو.

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 سڀ کان پهريان سمارٽ ڪانٽريڪٽ مان سڀني متغيرن کي ڪڍي ٿو انهن جي ڪيز جي صورت ۾ ۽ لاڳاپيل 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 وري انھن کي تبديل ڪري ٿو 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] )  

شرطن کي ترتيب ڏنو ويو آهي ۽ هڪ اسڪرپٽ ٽيمپليٽ ۾ داخل ڪيو ويو آهي 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 جي وڌيڪ ترقي کي ڍڪڻ جو منصوبو ڪريان ٿو، ۽ ڏيکاريو ته توهان ڪيئن ٺاهي سگهو ٿا رسمي طور تي تصديق ٿيل سمارٽ معاهدو ان جي مدد سان، ۽ نه صرف انهن کي حل ڪريو.

ڪردار مجازي مشين تي موجود آهي http://2.59.42.98/hyperbox/
علامتي VM جو سورس ڪوڊ ترتيب ڏيڻ ۽ اتي رايا شامل ڪرڻ کان پوءِ ، مان ان کي مفت رسائي لاءِ GitHub تي رکڻ جو ارادو ڪريان ٿو.

جو ذريعو: www.habr.com

تبصرو شامل ڪريو