ფორმალური გადამოწმების სისტემის შექმნა ნულიდან. ნაწილი 1: პერსონაჟების ვირტუალური მანქანა PHP-სა და Python-ში

ფორმალური გადამოწმება არის ერთი პროგრამის ან ალგორითმის გადამოწმება მეორის გამოყენებით.

ეს არის ერთ-ერთი ყველაზე ძლიერი მეთოდი, რომელიც საშუალებას გაძლევთ იპოვოთ ყველა დაუცველობა პროგრამაში ან დაამტკიცოთ, რომ ისინი არ არსებობს.

ფორმალური გადამოწმების უფრო დეტალური აღწერა შეგიძლიათ იხილოთ პრობლემის გადაჭრის მაგალითში მგელი, თხა და კომბოსტო ჩემს წინა სტატიაში.

ამ სტატიაში მე გადავდივარ პრობლემების ოფიციალური გადამოწმებიდან პროგრამებზე და აღვწერ როგორ
როგორ შეიძლება ისინი ავტომატურად გარდაიქმნას ფორმალური წესების სისტემებად.

ამისათვის მე დავწერე ვირტუალური მანქანის საკუთარი ანალოგი სიმბოლური პრინციპების გამოყენებით.

ის აანალიზებს პროგრამის კოდს და თარგმნის მას განტოლებათა სისტემად (SMT), რომლის ამოხსნა უკვე შესაძლებელია პროგრამულად.

ვინაიდან სიმბოლური გამოთვლების შესახებ ინფორმაცია ინტერნეტში საკმაოდ ფრაგმენტულად არის წარმოდგენილი,
მოკლედ აღვწერ რა არის.

სიმბოლური გამოთვლა არის პროგრამის ერთდროული განხორციელების საშუალება მონაცემთა ფართო დიაპაზონზე და არის პროგრამის ოფიციალური გადამოწმების მთავარი ინსტრუმენტი.

მაგალითად, ჩვენ შეგვიძლია დავაყენოთ შეყვანის პირობები, სადაც პირველ არგუმენტს შეუძლია მიიღოს ნებისმიერი დადებითი მნიშვნელობა, მეორე უარყოფითი, მესამე ნული და გამომავალი არგუმენტი, მაგალითად, 42.

სიმბოლური გამოთვლები ერთ პერსპექტივაში მოგვცემს პასუხს, შესაძლებელია თუ არა ჩვენთვის სასურველი შედეგის მიღება და ასეთი შეყვანის პარამეტრების ნაკრების მაგალითი. ან მტკიცებულება იმისა, რომ ასეთი პარამეტრები არ არსებობს.

უფრო მეტიც, ჩვენ შეგვიძლია დავაყენოთ შეყვანის არგუმენტები ყველა შესაძლოზე და შევარჩიოთ მხოლოდ გამომავალი არგუმენტები, მაგალითად, ადმინისტრატორის პაროლი.

ამ შემთხვევაში, ჩვენ ვიპოვით პროგრამის ყველა დაუცველობას ან მივიღებთ მტკიცებულებას, რომ ადმინისტრატორის პაროლი უსაფრთხოა.

შეიძლება აღინიშნოს, რომ პროგრამის კლასიკური შესრულება კონკრეტული შეყვანის მონაცემებით არის სიმბოლური შესრულების განსაკუთრებული შემთხვევა.

ამიტომ, ჩემს პერსონაჟ VM-ს შეუძლია იმუშაოს სტანდარტული ვირტუალური მანქანის ემულაციის რეჟიმში.

წინა სტატიის კომენტარებში შეგიძლიათ იხილოთ ოფიციალური გადამოწმების სამართლიანი კრიტიკა მისი სისუსტეების განხილვით.

ძირითადი პრობლემებია:

1. კომბინატორული აფეთქება, ვინაიდან ფორმალური გადამოწმება საბოლოოდ მცირდება P=NP-მდე
2. ზარების დამუშავება ფაილურ სისტემაში, ქსელებში და სხვა გარე საცავებში უფრო რთულია გადამოწმება
3. ხარვეზები სპეციფიკაციაში, როდესაც მომხმარებელმა ან პროგრამისტმა განიზრახა ერთი რამ, მაგრამ საკმარისად ზუსტად არ აღწერს მას ტექნიკურ სპეციფიკაციაში.

შედეგად, პროგრამა გადამოწმებული იქნება და შეესაბამება სპეციფიკაციას, მაგრამ გააკეთებს რაღაც სრულიად განსხვავებულს, რასაც შემქმნელები მისგან მოელოდნენ.

ვინაიდან ამ სტატიაში მე ძირითადად განვიხილავ პრაქტიკაში ფორმალური გადამოწმების გამოყენებას, ამ დროისთვის თავს კედელს არ დავაკაკუნებ და ავირჩევ სისტემას, სადაც ალგორითმული სირთულე და გარე ზარების რაოდენობა მინიმალურია.

ვინაიდან ჭკვიანი კონტრაქტები საუკეთესოდ ერგება ამ მოთხოვნებს, არჩევანი დაეცა RIDE კონტრაქტებზე Waves პლატფორმიდან: ისინი არ არიან ტურინგი დასრულებული და მათი მაქსიმალური სირთულე ხელოვნურად შეზღუდულია.

მაგრამ ჩვენ განვიხილავთ მათ ექსკლუზიურად ტექნიკური მხრიდან.

ყველაფრის გარდა, ფორმალური გადამოწმება განსაკუთრებით მოთხოვნადი იქნება ნებისმიერ კონტრაქტზე: როგორც წესი, შეუძლებელია ხელშეკრულების შეცდომის გამოსწორება მისი გაშვების შემდეგ.
და ასეთი შეცდომების ღირებულება შეიძლება იყოს ძალიან მაღალი, რადგან საკმაოდ დიდი თანხები ხშირად ინახება ჭკვიან კონტრაქტებზე.

ჩემი სიმბოლური ვირტუალური მანქანა დაწერილია PHP-ში და Python-ში და იყენებს Z3Prover-ს Microsoft Research-ისგან მიღებული SMT ფორმულების გადასაჭრელად.

მის ბირთვში არის მძლავრი მრავალტრანზაქციის ძიება, რომელიც
საშუალებას გაძლევთ იპოვოთ გადაწყვეტილებები ან დაუცველობა, მაშინაც კი, თუ ეს მოითხოვს ბევრ ტრანზაქციას.
მაშინაც კი, მითრიერთ-ერთმა ყველაზე მძლავრმა სიმბოლურმა ჩარჩომ Ethereum-ის დაუცველობის აღმოსაჩენად, ეს შესაძლებლობა მხოლოდ რამდენიმე თვის წინ დაამატა.

მაგრამ აღსანიშნავია, რომ ეთერული კონტრაქტები უფრო რთულია და ტურინგის სრული.

PHP თარგმნის RIDE ჭკვიანი კონტრაქტის საწყის კოდს პითონის სკრიპტში, რომელშიც პროგრამა წარმოდგენილია როგორც Z3 SMT-თან თავსებადი ხელშეკრულების მდგომარეობებისა და მათი გადასვლის პირობების სახით:

ახლა უფრო დეტალურად აღვწერ რა ხდება შიგნით.

მაგრამ პირველი, რამდენიმე სიტყვა RIDE ჭკვიანი კონტრაქტის ენის შესახებ.

ეს არის ფუნქციური და ექსპრესიაზე დაფუძნებული პროგრამირების ენა, რომელიც დიზაინით ზარმაცია.
RIDE მუშაობს იზოლირებულად ბლოკჩეინში და შეუძლია ინფორმაციის მოძიება და ჩაწერა მომხმარებლის საფულესთან დაკავშირებული საცავიდან.

თქვენ შეგიძლიათ დაურთოთ 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] )  

პირობები დალაგებულია და ჩასმულია სკრიპტის შაბლონში, რომელიც შექმნილია 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