అధికారిక ధృవీకరణ అనేది ఒక ప్రోగ్రామ్ లేదా మరొకదాన్ని ఉపయోగించి అల్గోరిథం యొక్క ధృవీకరణ.
ప్రోగ్రామ్‌లోని అన్ని దుర్బలత్వాలను కనుగొనడానికి లేదా అవి ఉనికిలో లేవని నిరూపించడానికి మిమ్మల్ని అనుమతించే అత్యంత శక్తివంతమైన పద్ధతుల్లో ఇది ఒకటి.
యొక్క సమస్యను పరిష్కరించే ఉదాహరణలో అధికారిక ధృవీకరణ యొక్క మరింత వివరణాత్మక వర్ణనను చూడవచ్చు నా మునుపటి వ్యాసంలో.
ఈ వ్యాసంలో నేను సమస్యల యొక్క అధికారిక ధృవీకరణ నుండి ప్రోగ్రామ్‌లకు వెళ్లి ఎలా వివరిస్తాను
వాటిని స్వయంచాలకంగా అధికారిక నియమ వ్యవస్థలుగా ఎలా మార్చవచ్చు.
దీన్ని చేయడానికి, నేను సింబాలిక్ సూత్రాలను ఉపయోగించి వర్చువల్ మెషీన్ యొక్క నా స్వంత అనలాగ్‌ను వ్రాసాను.
ఇది ప్రోగ్రామ్ కోడ్‌ను అన్వయిస్తుంది మరియు దానిని సమీకరణాల వ్యవస్థ (SMT)లోకి అనువదిస్తుంది, ఇది ఇప్పటికే ప్రోగ్రామాటిక్‌గా పరిష్కరించబడుతుంది.
సింబాలిక్ లెక్కల గురించిన సమాచారం అంతర్జాలంలో ఛిన్నాభిన్నంగా ప్రదర్శించబడుతుంది కాబట్టి,
అది ఏమిటో నేను క్లుప్తంగా వివరిస్తాను.
సింబాలిక్ కంప్యూటేషన్ అనేది విస్తృత శ్రేణి డేటాపై ప్రోగ్రామ్‌ను ఏకకాలంలో అమలు చేయడానికి ఒక మార్గం మరియు ఇది అధికారిక ప్రోగ్రామ్ ధృవీకరణకు ప్రధాన సాధనం.
ఉదాహరణకు, మేము ఇన్‌పుట్ పరిస్థితులను సెట్ చేయవచ్చు, ఇక్కడ మొదటి ఆర్గ్యుమెంట్ ఏదైనా సానుకూల విలువలు, రెండవ ప్రతికూల, మూడవ సున్నా మరియు అవుట్‌పుట్ ఆర్గ్యుమెంట్, ఉదాహరణకు, 42.
ఒక పరుగులో సింబాలిక్ లెక్కలు మనకు కావలసిన ఫలితాన్ని పొందడం సాధ్యమేనా అనేదానికి సమాధానాన్ని మరియు అటువంటి ఇన్‌పుట్ పారామితుల సమితికి ఉదాహరణను ఇస్తుంది. లేదా అలాంటి పారామితులు లేవని రుజువు చేయండి.
అంతేకాకుండా, మేము ఇన్‌పుట్ ఆర్గ్యుమెంట్‌లను సాధ్యమయ్యే అన్ని వాటికి సెట్ చేయవచ్చు మరియు అవుట్‌పుట్ వాటిని మాత్రమే ఎంచుకోవచ్చు, ఉదాహరణకు, నిర్వాహక పాస్‌వర్డ్.
ఈ సందర్భంలో, మేము ప్రోగ్రామ్ యొక్క అన్ని దుర్బలత్వాలను కనుగొంటాము లేదా నిర్వాహకుని పాస్‌వర్డ్ సురక్షితంగా ఉందని రుజువును పొందుతాము.
నిర్దిష్ట ఇన్‌పుట్ డేటాతో ప్రోగ్రామ్ యొక్క క్లాసికల్ ఎగ్జిక్యూషన్ సింబాలిక్ ఎగ్జిక్యూషన్ యొక్క ప్రత్యేక సందర్భం అని గమనించవచ్చు.
కాబట్టి, నా అక్షరం VM కూడా ప్రామాణిక వర్చువల్ మిషన్ యొక్క ఎమ్యులేషన్ మోడ్‌లో పని చేస్తుంది.
మునుపటి కథనానికి చేసిన వ్యాఖ్యలలో దాని బలహీనతల చర్చతో అధికారిక ధృవీకరణపై న్యాయమైన విమర్శలను కనుగొనవచ్చు.
ప్రధాన సమస్యలు:
- కాంబినేటోరియల్ పేలుడు, ఎందుకంటే అధికారిక ధృవీకరణ చివరికి P=NPకి వస్తుంది
- ఫైల్ సిస్టమ్, నెట్‌వర్క్‌లు మరియు ఇతర బాహ్య నిల్వకు కాల్‌లను ప్రాసెస్ చేయడం ధృవీకరించడం చాలా కష్టం
- స్పెసిఫికేషన్‌లోని బగ్‌లు, కస్టమర్ లేదా ప్రోగ్రామర్ ఒక విషయాన్ని ఉద్దేశించినప్పుడు, కానీ సాంకేతిక వివరణలో దానిని సరిగ్గా వివరించలేదు.
ఫలితంగా, ప్రోగ్రామ్ ధృవీకరించబడుతుంది మరియు స్పెసిఫికేషన్‌కు అనుగుణంగా ఉంటుంది, అయితే దాని నుండి సృష్టికర్తలు ఆశించిన దాని నుండి పూర్తిగా భిన్నమైన పనిని చేస్తుంది.
ఈ వ్యాసంలో నేను ఆచరణలో అధికారిక ధృవీకరణను ఉపయోగించడాన్ని ప్రధానంగా పరిశీలిస్తున్నాను కాబట్టి, నేను ప్రస్తుతానికి గోడకు వ్యతిరేకంగా నా తలని కొట్టను మరియు అల్గోరిథమిక్ సంక్లిష్టత మరియు బాహ్య కాల్‌ల సంఖ్య తక్కువగా ఉండే వ్యవస్థను ఎంచుకుంటాను.
స్మార్ట్ ఒప్పందాలు ఈ అవసరాలకు బాగా సరిపోతాయి కాబట్టి, ఎంపిక వేవ్స్ ప్లాట్‌ఫారమ్ నుండి RIDE ఒప్పందాలపై పడింది: అవి ట్యూరింగ్ పూర్తి కాలేదు మరియు వాటి గరిష్ట సంక్లిష్టత కృత్రిమంగా పరిమితం చేయబడింది.
కానీ మేము వాటిని సాంకేతిక వైపు నుండి ప్రత్యేకంగా పరిశీలిస్తాము.
ప్రతిదానితో పాటు, అధికారిక ధృవీకరణకు ప్రత్యేకించి ఏదైనా ఒప్పందాలకు డిమాండ్ ఉంటుంది: ఇది ప్రారంభించబడిన తర్వాత ఒప్పంద లోపాన్ని సరిదిద్దడం సాధారణంగా అసాధ్యం.
మరియు అటువంటి లోపాల ధర చాలా ఎక్కువగా ఉంటుంది, ఎందుకంటే చాలా పెద్ద మొత్తంలో నిధులు తరచుగా స్మార్ట్ కాంట్రాక్టులలో నిల్వ చేయబడతాయి.
నా సింబాలిక్ వర్చువల్ మెషీన్ PHP మరియు పైథాన్‌లో వ్రాయబడింది మరియు ఫలితంగా వచ్చే SMT ఫార్ములాలను పరిష్కరించడానికి Microsoft రీసెర్చ్ నుండి Z3Proverని ఉపయోగిస్తుంది.
దాని ప్రధాన భాగంలో శక్తివంతమైన బహుళ-లావాదేవీ శోధన ఉంది, ఇది
అనేక లావాదేవీలు అవసరం అయినప్పటికీ, పరిష్కారాలు లేదా దుర్బలత్వాలను కనుగొనడానికి మిమ్మల్ని అనుమతిస్తుంది.
కూడా , Ethereum దుర్బలత్వాలను కనుగొనడానికి అత్యంత శక్తివంతమైన సింబాలిక్ ఫ్రేమ్‌వర్క్‌లలో ఒకటి, కొన్ని నెలల క్రితం మాత్రమే ఈ సామర్థ్యాన్ని జోడించింది.
కానీ ఈథర్ కాంట్రాక్టులు మరింత క్లిష్టంగా మరియు ట్యూరింగ్ పూర్తి కావడం గమనించదగ్గ విషయం.
PHP RIDE స్మార్ట్ కాంట్రాక్ట్ యొక్క సోర్స్ కోడ్‌ను పైథాన్ స్క్రిప్ట్‌గా అనువదిస్తుంది, దీనిలో ప్రోగ్రామ్ Z3 SMT-అనుకూలమైన కాంట్రాక్ట్ స్టేట్‌లు మరియు వాటి పరివర్తనల కోసం షరతులుగా ప్రదర్శించబడుతుంది:
ఇప్పుడు నేను లోపల ఏమి జరుగుతుందో మరింత వివరంగా వివరిస్తాను.
అయితే ముందుగా, 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 మొదట స్మార్ట్ కాంట్రాక్ట్ నుండి అన్ని వేరియబుల్స్‌ను వాటి కీల రూపంలో మరియు సంబంధిత బూలియన్ ఎక్స్‌ప్రెషన్ వేరియబుల్ రూపంలో సంగ్రహిస్తుంది.
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-అనుకూల సిస్టమ్ వివరణగా మారుస్తుంది.
డేటా లూప్‌లో చుట్టబడి ఉంటుంది, ఇక్కడ నిల్వ వేరియబుల్స్ ఇండెక్స్ 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 యొక్క మరింత అభివృద్ధిని కవర్ చేయడానికి ప్లాన్ చేస్తున్నాను మరియు దాని సహాయంతో మీరు అధికారికంగా ధృవీకరించబడిన స్మార్ట్ ఒప్పందాలను ఎలా సృష్టించవచ్చో చూపుతాను మరియు వాటిని పరిష్కరించడం మాత్రమే కాదు.
అక్షర వర్చువల్ మిషన్ అందుబాటులో ఉంది
సింబాలిక్ VM యొక్క సోర్స్ కోడ్‌ను క్రమంలో ఉంచి, అక్కడ వ్యాఖ్యలను జోడించిన తర్వాత, ఉచిత యాక్సెస్ కోసం నేను దానిని GitHubలో ఉంచాలని ప్లాన్ చేస్తున్నాను.
మూలం: www.habr.com