શરૂઆતથી ઔપચારિક ચકાસણી સિસ્ટમ બનાવવી. ભાગ 1: PHP અને Python માં અક્ષર વર્ચ્યુઅલ મશીન

ઔપચારિક ચકાસણી એ એક પ્રોગ્રામ અથવા બીજાનો ઉપયોગ કરીને અલ્ગોરિધમની ચકાસણી છે.

આ એક સૌથી શક્તિશાળી પદ્ધતિઓ છે જે તમને પ્રોગ્રામમાં બધી નબળાઈઓ શોધવા અથવા સાબિત કરવાની મંજૂરી આપે છે કે તે અસ્તિત્વમાં નથી.

ની સમસ્યાને ઉકેલવાના ઉદાહરણમાં ઔપચારિક ચકાસણીનું વધુ વિગતવાર વર્ણન જોઈ શકાય છે વરુ, બકરી અને કોબી મારા અગાઉના લેખમાં.

આ લેખમાં હું સમસ્યાઓની ઔપચારિક ચકાસણીથી પ્રોગ્રામ્સ તરફ આગળ વધીશ અને કેવી રીતે તેનું વર્ણન કરું છું
તેઓને ઔપચારિક નિયમ પ્રણાલીમાં આપમેળે કેવી રીતે રૂપાંતરિત કરી શકાય છે.

આ કરવા માટે, મેં પ્રતીકાત્મક સિદ્ધાંતોનો ઉપયોગ કરીને વર્ચ્યુઅલ મશીનનું મારું પોતાનું એનાલોગ લખ્યું.

તે પ્રોગ્રામ કોડને પાર્સ કરે છે અને તેને સમીકરણોની સિસ્ટમ (એસએમટી) માં અનુવાદિત કરે છે, જે પહેલાથી જ પ્રોગ્રામેટિક રીતે ઉકેલી શકાય છે.

સાંકેતિક ગણતરીઓ વિશેની માહિતી ઇન્ટરનેટ પર ખંડિત રીતે રજૂ કરવામાં આવી હોવાથી,
હું તે શું છે તેનું ટૂંકમાં વર્ણન કરીશ.

સાંકેતિક ગણતરી એ ડેટાની વિશાળ શ્રેણી પર એક સાથે પ્રોગ્રામ ચલાવવાનો એક માર્ગ છે અને ઔપચારિક પ્રોગ્રામ ચકાસણી માટેનું મુખ્ય સાધન છે.

ઉદાહરણ તરીકે, અમે ઇનપુટ શરતો સેટ કરી શકીએ છીએ જ્યાં પ્રથમ દલીલ કોઈપણ હકારાત્મક મૂલ્યો લઈ શકે છે, બીજી નકારાત્મક, ત્રીજી શૂન્ય અને આઉટપુટ દલીલ, ઉદાહરણ તરીકે, 42.

એક રનમાં સાંકેતિક ગણતરીઓ આપણને ઇચ્છિત પરિણામ મેળવવાનું શક્ય છે કે કેમ તેનો જવાબ અને આવા ઇનપુટ પરિમાણોના સમૂહનું ઉદાહરણ આપશે. અથવા પુરાવા છે કે આવા કોઈ પરિમાણો નથી.

તદુપરાંત, અમે તમામ સંભવિત મુદ્દાઓ પર ઇનપુટ દલીલો સેટ કરી શકીએ છીએ, અને ફક્ત આઉટપુટ પસંદ કરી શકીએ છીએ, ઉદાહરણ તરીકે, એડમિનિસ્ટ્રેટર પાસવર્ડ.

આ કિસ્સામાં, અમે પ્રોગ્રામની તમામ નબળાઈઓ શોધીશું અથવા એડમિનિસ્ટ્રેટરનો પાસવર્ડ સુરક્ષિત છે તેની સાબિતી મેળવીશું.

તે નોંધી શકાય છે કે ચોક્કસ ઇનપુટ ડેટા સાથે પ્રોગ્રામનું ક્લાસિકલ એક્ઝેક્યુશન એ સિમ્બોલિક એક્ઝેક્યુશનનો એક ખાસ કેસ છે.

તેથી, મારું પાત્ર VM પ્રમાણભૂત વર્ચ્યુઅલ મશીનના ઇમ્યુલેશન મોડમાં પણ કામ કરી શકે છે.

અગાઉના લેખની ટિપ્પણીઓમાં તેની નબળાઈઓની ચર્ચા સાથે ઔપચારિક ચકાસણીની વાજબી ટીકા મળી શકે છે.

મુખ્ય સમસ્યાઓ છે:

1. સંયુક્ત વિસ્ફોટ, કારણ કે ઔપચારિક ચકાસણી આખરે P=NP પર આવે છે
2. ફાઇલ સિસ્ટમ, નેટવર્ક્સ અને અન્ય બાહ્ય સ્ટોરેજ પરના કૉલ્સની પ્રક્રિયા ચકાસવી વધુ મુશ્કેલ છે
3. સ્પષ્ટીકરણમાં ભૂલો, જ્યારે ગ્રાહક અથવા પ્રોગ્રામર એક વસ્તુનો ઇરાદો ધરાવે છે, પરંતુ તકનીકી સ્પષ્ટીકરણમાં તેનું ચોક્કસ વર્ણન કર્યું નથી.

પરિણામે, પ્રોગ્રામ ચકાસવામાં આવશે અને સ્પષ્ટીકરણનું પાલન કરશે, પરંતુ નિર્માતાઓ તેનાથી જે અપેક્ષા રાખતા હતા તેનાથી સંપૂર્ણપણે અલગ કંઈક કરશે.

આ લેખમાં હું મુખ્યત્વે પ્રેક્ટિસમાં ઔપચારિક ચકાસણીનો ઉપયોગ કરવાનું વિચારી રહ્યો હોવાથી, હું હમણાં માટે મારું માથું દીવાલ સાથે અથડાવીશ નહીં, અને એવી સિસ્ટમ પસંદ કરીશ જ્યાં અલ્ગોરિધમિક જટિલતા અને બાહ્ય કૉલ્સની સંખ્યા ન્યૂનતમ હોય.

સ્માર્ટ કોન્ટ્રાક્ટ્સ આ જરૂરિયાતોને શ્રેષ્ઠ રીતે અનુરૂપ હોવાથી, પસંદગી વેવ્ઝ પ્લેટફોર્મ પરથી રાઇડ કોન્ટ્રાક્ટ પર પડી: તે ટ્યુરિંગ પૂર્ણ નથી, અને તેમની મહત્તમ જટિલતા કૃત્રિમ રીતે મર્યાદિત છે.

પરંતુ અમે તેમને ફક્ત તકનીકી બાજુથી ધ્યાનમાં લઈશું.

વધુમાં, કોઈપણ કરાર માટે ઔપચારિક ચકાસણી ખાસ કરીને માંગમાં હશે: કરારની ભૂલ શરૂ થયા પછી તેને સુધારવાનું સામાન્ય રીતે અશક્ય છે.
અને આવી ભૂલોની કિંમત ઘણી વધારે હોઈ શકે છે, કારણ કે ઘણી વખત સ્માર્ટ કોન્ટ્રાક્ટ પર મોટી માત્રામાં ભંડોળ સંગ્રહિત કરવામાં આવે છે.

મારું સાંકેતિક વર્ચ્યુઅલ મશીન PHP અને Python માં લખાયેલું છે, અને પરિણામી SMT સૂત્રોને ઉકેલવા માટે Microsoft સંશોધનમાંથી Z3Prover નો ઉપયોગ કરે છે.

તેના મૂળમાં એક શક્તિશાળી મલ્ટિ-ટ્રાન્ઝેક્શનલ શોધ છે, જે
તમને ઉકેલો અથવા નબળાઈઓ શોધવાની મંજૂરી આપે છે, ભલે તેને ઘણા વ્યવહારોની જરૂર હોય.
પણ મિથ્રિલ, Ethereum નબળાઈઓ શોધવા માટે સૌથી શક્તિશાળી સાંકેતિક માળખામાંની એક, માત્ર થોડા મહિના પહેલા જ આ ક્ષમતા ઉમેરાઈ.

પરંતુ એ નોંધવું યોગ્ય છે કે ઈથર કોન્ટ્રાક્ટ વધુ જટિલ અને ટ્યુરિંગ પૂર્ણ છે.

PHP RIDE સ્માર્ટ કોન્ટ્રેક્ટના સોર્સ કોડને પાયથોન સ્ક્રિપ્ટમાં અનુવાદિત કરે છે, જેમાં પ્રોગ્રામને Z3 SMT-સુસંગત સિસ્ટમ તરીકે કોન્ટ્રાક્ટ સ્ટેટ્સ અને તેમના સંક્રમણો માટેની શરતો તરીકે રજૂ કરવામાં આવે છે:

હવે હું અંદર શું થઈ રહ્યું છે તેનું વધુ વિગતવાર વર્ણન કરીશ.

પરંતુ પ્રથમ, 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 સૌપ્રથમ સ્માર્ટ કોન્ટ્રાક્ટમાંથી તમામ ચલોને તેમની કીના સ્વરૂપમાં અને અનુરૂપ બુલિયન એક્સપ્રેશન વેરીએબલને બહાર કાઢે છે.

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] )  

શરતોને પાયથોનમાં 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