Συμβολική δοκιμή με Halmos: Αξιοποίηση υπαρχόντων δοκιμών για επίσημη επαλήθευση

Η επίσημη επαλήθευση — η διαδικασία χρήσης μαθηματικών μεθόδων για την «επιθεώρηση» ενός προγράμματος ή ενός έξυπνου συμβολαίου σε οποιονδήποτε αριθμό εισόδων — θεωρείται γενικά ως η πιο συνοπτική, πιο ολοκληρωμένη εναλλακτική λύση σε σχέση με τις παραδοσιακές δοκιμές για τη σύνταξη υψηλότερης ποιότητας και ασφαλέστερου κώδικα. Αλλά στην πραγματικότητα, η επίσημη επαλήθευση είναι μια διαδικασία ανοιχτού τύπου και αλληλεπιδραστική. Όπως και οι δοκιμές μονάδων, οι προγραμματιστές πρέπει να ορίζουν δυναμικά και να στρώνουν επίσημες προδιαγραφές, επαναλαμβάνοντας την προσέγγισή τους καθώς ο κώδικας και οι αναλύσεις τους εξελίσσονται. Επιπλέον, η επίσημη επαλήθευση είναι τόσο αποτελεσματική όσο οι προδιαγραφές της, η οποία μπορεί να είναι χρονοβόρα για τη σύνταξη (και συχνά συνοδεύεται από μια απότομη καμπύλη εκμάθησης). 

Για πολλούς προγραμματιστές που βρίσκουν τη διαδικασία τρομακτική, οι δοκιμές μονάδων είναι συχνά η πιο οικονομική και χρονικά αποδοτική οδός για να υποστηρίξουν την ορθότητα ενός προγράμματος. Στην πράξη, η επίσημη επαλήθευση δεν είναι μια πιο ολοκληρωμένη εναλλακτική λύση στη δοκιμή μονάδας, αλλά μια συμπληρωματική. Αυτές οι διαδικασίες έχουν διαφορετικά πλεονεκτήματα και περιορισμούς, παρέχοντας ακόμη μεγαλύτερη βεβαιότητα όταν χρησιμοποιούνται μαζί. Οι προγραμματιστές θα πρέπει πάντα να γράφουν δοκιμές μονάδων — οπότε τι θα γινόταν αν μπορούσαμε να χρησιμοποιήσουμε τις ίδιες ιδιότητες για επίσημη επαλήθευση;

Χαλμός, το εργαλείο επίσημης επαλήθευσης ανοιχτού κώδικα, επιτρέπει στους προγραμματιστές να επαναχρησιμοποίηση οι ίδιες ιδιότητες που γράφτηκαν για μοναδιαίες δοκιμές για επίσημες προδιαγραφές μέσω συμβολικών δοκιμών. Αντί να χρειάζεται να δημιουργήσουν ένα ισχυρό σύνολο ιδιοτήτων από την αρχή, οι προγραμματιστές μπορούν να αποφύγουν την διπλή εργασία και να βελτιώσουν τις δοκιμές τους μερικές προδιαγραφές κάθε φορά χωρίς να ξεκινήσουν από την αρχή. Σχεδιάσαμε αυτό το εργαλείο για χρήση, μαζί με άλλα στη διαδικασία επίσημης επαλήθευσης, ως μια ράμπα στην επίσημη επαλήθευση. Οι προγραμματιστές μπορούν να ξεκινήσουν με μερικές αναλύσεις με ελάχιστη προσπάθεια, πριν προσθέσουν περισσότερες αργότερα στη διαδικασία.

Σε αυτήν την ανάρτηση, καλύπτουμε τις προκλήσεις της επίσημης επαλήθευσης και τη δυνατότητα να γεφυρωθεί το χάσμα μεταξύ της δοκιμής μονάδας και της επίσημης επαλήθευσης με συμβολικές δοκιμές. Στη συνέχεια, περπατάμε σε μια επίδειξη του Halmos χρησιμοποιώντας τον υπάρχοντα κώδικα έξυπνης σύμβασης και ρίχνουμε μια γρήγορη ματιά σε άλλα επίσημα εργαλεία επαλήθευσης (πολλά ανοιχτού κώδικα) που είναι διαθέσιμα στους προγραμματιστές.

Επίσημη επαλήθευση έναντι δοκιμής

Επίσημη επαλήθευση — που γενικά προτιμάται από τους προγραμματιστές blockchain για την αυστηρότητα και την περιεκτικότητά του — είναι η διαδικασία απόδειξης της ορθότητας ενός προγράμματος με την επαλήθευση ότι ικανοποιεί ορισμένες ιδιότητες ορθότητας. Οι ιδιότητες, που είναι συγκεκριμένες για το πρόγραμμα, παρέχονται συνήθως εξωτερικά και εκφράζονται χρησιμοποιώντας μια επίσημη γλώσσα ή σημειογραφία που υποστηρίζεται από το εργαλείο επαλήθευσης που χρησιμοποιείται. Οι προγραμματιστές συχνά αντιλαμβάνονται την επίσημη επαλήθευση ως μια λύση με το πάτημα του κουμπιού για αυτόματη δοκιμή ιδιοτήτων σε όλα τα πιθανά σενάρια, αλλά στην πραγματικότητα, η επίσημη επαλήθευση μπορεί να είναι μια διαδικασία έντασης εργασίας και εξαιρετικά διαδραστική.

Όπως η επίσημη επαλήθευση, η δοκιμή μονάδας περιλαμβάνει την αξιολόγηση εάν ένα πρόγραμμα λειτουργεί όπως αναμένεται. Η δοκιμή, ωστόσο, ελέγχει μόνο τη συμπεριφορά του προγράμματος για μερικοί εισόδους, ενώ η επίσημη επαλήθευση μπορεί να το ελέγξει όλοι πιθανές εισροές. Τόσο η δοκιμή όσο και η επίσημη επαλήθευση απαιτούν περιγραφή της αναμενόμενης συμπεριφοράς του προγράμματος (με περιπτώσεις δοκιμής που χρησιμοποιούνται στις δοκιμές και επίσημες προδιαγραφές που χρησιμοποιούνται στην επίσημη επαλήθευση). Όμως, όταν χρησιμοποιούνται μαζί, μπορούν να παρέχουν μια πιο ενδελεχή εξέταση ενός προγράμματος. Η δοκιμή, για παράδειγμα, είναι αποτελεσματική στην εύρεση απλών σφαλμάτων και λαθών, αλλά γενικά είναι ταχύτερη και ευκολότερη στην εκτέλεση. Η επίσημη επαλήθευση, αν και είναι πιο επαχθής στη χρήση, είναι αρκετά ισχυρή ώστε να αποδείξει την απουσία σφαλμάτων ή να αποκαλύψει ανεπαίσθητα σφάλματα που είναι εύκολο να χάσετε στις δοκιμές ή στις αξιολογήσεις κώδικα.

Επιβάρυνση προδιαγραφών

Μία από τις κύριες προκλήσεις της επίσημης επαλήθευσης είναι η επιβάρυνση της σύνταξης και της διατήρησης των επίσημων προδιαγραφών. Αυτή η διαδικασία συχνά περιλαμβάνει τη χρονοβόρα εργασία της μη αυτόματης εγγραφής των προδιαγραφών χρησιμοποιώντας μια εξειδικευμένη γλώσσα (που πολλοί προγραμματιστές θα πρέπει πρώτα να μάθουν). Η διαδικασία είναι επίσης σταδιακή, συνήθως ξεκινά με τη σύνταξη απλών ιδιοτήτων και την επαλήθευση τους πρώτα και στη συνέχεια προσθέτοντας σταδιακά πιο σύνθετες ιδιότητες στην κορυφή. Όπως και η δοκιμή, είναι μια διαδικασία ανοιχτού τύπου, χωρίς σαφές σημείο τερματισμού και μπορεί κανείς να προσθέσει όσο το δυνατόν περισσότερες ιδιότητες εντός του διαθέσιμου χρονικού πλαισίου. Επιπλέον, όταν οι προγραμματιστές αλλάζουν τον κώδικα καθώς επαληθεύεται, πρέπει επίσης να ενημερώσουν τις υπάρχουσες προδιαγραφές τους, με αποτέλεσμα επιπλέον προσπάθειες συντήρησης. Αυτοί οι παράγοντες μπορούν να καταστήσουν την επίσημη επαλήθευση δύσκολη εργασία για ορισμένους προγραμματιστές που διστάζουν να δεσμευτούν για τα επιπλέον έξοδα.

Και παρόλο που η δοκιμή και η επίσημη επαλήθευση μπορούν να βελτιώσουν την ποιότητα του κώδικα όταν χρησιμοποιούνται μαζί, και οι δύο απαιτούν (μερικές φορές παρόμοιες) περιγραφές της αναμενόμενης συμπεριφοράς ενός προγράμματος σε διαφορετικές γλώσσες και μορφές. Η συγγραφή και η διατήρηση αυτών των περιγραφών απαιτεί ένταση εργασίας και η διατήρηση δύο διαφορετικών μορφών της ίδιας περιγραφής μπορεί να μοιάζει με διπλή προσπάθεια. Αυτό εγείρει το ακόλουθο ερώτημα: Είναι δυνατόν να περιγραφεί η αναμενόμενη συμπεριφορά με τρόπο που οι προγραμματιστές μπορούν να χρησιμοποιήσουν τόσο για δοκιμή όσο και για επαλήθευση;

Γεφύρωση του χάσματος μεταξύ δοκιμών και επίσημης επαλήθευσης με συμβολικές δοκιμές και Halmos

Η συμβολική δοκιμή, η πρακτική της εκτέλεσης δοκιμών με συμβολικές εισόδους, είναι μια αποτελεσματική μέθοδος επίσημης επαλήθευσης που μειώνει τα έξοδα προδιαγραφών. Αυτή η προσέγγιση επιτρέπει τη χρήση των ίδιων περιπτώσεων δοκιμής τόσο για δοκιμές όσο και για επίσημη επαλήθευση. Σε αντίθεση με την παραδοσιακή δοκιμή, η οποία επαληθεύει ότι ένα πρόγραμμα λειτουργεί σωστά για ένα περιορισμένο σύνολο εισόδων, η συμβολική δοκιμή ελέγχει το πρόγραμμα για όλες τις πιθανές εισόδους, επομένως ένα πρόγραμμα που περνάει από συμβολική δοκιμή μπορεί να θεωρηθεί επίσημα επαληθευμένο.

Το Halmos είναι ένα επίσημο εργαλείο επαλήθευσης σχεδιασμένο για συμβολικές δοκιμές. Αντί να απαιτεί ξεχωριστές προδιαγραφές ή να μάθει μια νέα γλώσσα, το Halmos χρησιμοποιεί υπάρχοντα τεστ ως επίσημες προδιαγραφές. Οι δοκιμές που εκτελούνται μέσω του Halmos θα επαληθεύουν αυτόματα ότι περνούν για όλες τις πιθανές εισροές ή θα παρέχουν αντιπαραδείγματα. Αυτό όχι μόνο εξαλείφει την ανάγκη για πρόσθετη εγγραφή προδιαγραφών, αλλά επιτρέπει επίσης την επαναχρησιμοποίηση δοκιμών που έχουν γραφτεί για δοκιμή μονάδας ή ασάφεια, για λόγους επίσημης επαλήθευσης.

Οι προγραμματιστές έχουν επομένως μεγαλύτερη ευελιξία να επιλέξουν από μια σειρά επιλογών διασφάλισης ποιότητας, συμπεριλαμβανομένων των δοκιμών μονάδας, της ασάφειας και της επίσημης επαλήθευσης, ανάλογα με τις τρέχουσες ανάγκες τους. Για παράδειγμα, οι δοκιμές μπορούν να εντοπίσουν γρήγορα απλά λάθη, πιθανώς με τη βοήθεια ενός fuzzer που δημιουργεί τυχαίες εισόδους και, στη συνέχεια, το Halmos μπορεί να αυξήσει περαιτέρω την εμπιστοσύνη στην ορθότητα του προγράμματος σε όλες τις εισόδους.

Παράδειγμα: Δοκιμή του isPowerOfTwo() λειτουργία

Ως παράδειγμα, λάβετε υπόψη τα ακόλουθα isPowerOfTwo() συνάρτηση, η οποία καθορίζει εάν ένας δεδομένος αριθμός είναι δύναμη του δύο. Αυτή η συνάρτηση χρησιμοποιεί α αλγόριθμος χειρισμού bit για αποτελεσματικότητα, αλλά μπορεί να είναι δύσκολο να αποδειχθεί η ορθότητά του, ιδιαίτερα στην περίπτωση που η είσοδος δεν είναι δύναμη δύο.

Φανταστείτε το παρακάτω τεστ για το isPowerOfTwo() συνάρτηση: συγκρίνει την πραγματική έξοδο της συνάρτησης με την αναμενόμενη έξοδο για μια δεδομένη είσοδο. Αυτή είναι μια παραμετροποιημένη δοκιμή (γνωστή και ως δοκιμή βασισμένη σε ιδιότητες), που σημαίνει ότι μπορείτε εύκολα να την εκτελέσετε με διαφορετικές τιμές εισαγωγής, πιθανώς με εργαλεία fuzzing όπως το Foundry.

Μπορείτε να χρησιμοποιήσετε αυτό το τεστ για να εξετάσετε το isPowerOfTwo() λειτουργούν μέσω δοκιμής μονάδας ή δοκιμής fuzz, εκτελώντας το με μια επιλογή εισόδων. Τέτοιες δοκιμές δεν μπορούν να αποδείξουν επίσημα την ορθότητα της συνάρτησης, καθώς είναι υπολογιστικά ανέφικτο να εκτελεστεί η δοκιμή για κάθε δυνατή είσοδο.

Το Halmos, ωστόσο, επιτρέπει στους προγραμματιστές να επαναχρησιμοποιήσουν αυτές τις προϋπάρχουσες δοκιμές για επίσημη επαλήθευση με λίγη επιπλέον προσπάθεια. Το εργαλείο ελέγχει ότι οι δοκιμές περνούν για όλες τις πιθανές εισόδους εκτελώντας συμβολική εκτέλεση της δοκιμής και στη συνέχεια επαληθεύοντας ότι ο ισχυρισμός δεν παραβιάζεται ποτέ, (ή, εάν ο ισχυρισμός is παραβιαστεί, παρέχοντας ένα αντιπαράδειγμα). Αυτό σημαίνει ότι εάν το τεστ περάσει στο Halmos, η ορθότητα της συνάρτησης επαληθεύεται επίσημα, που σημαίνει ότι ο αλγόριθμος έχει εφαρμοστεί σωστά και έχει μεταφραστεί με ακρίβεια από τον μεταγλωττιστή σε bytecode.

Περιορισμός: Οριοθετημένη συμβολική εκτέλεση

Γενικά δεν είναι δυνατό να πραγματοποιηθεί πλήρως αυτόματη, πλήρης συμβολική δοκιμή, καθώς αυτό θα απαιτούσε την επίλυση του πρόβλημα διακοπής, που είναι γνωστό ότι είναι αναποφάσιστος. Ένας λόγος για αυτό είναι ότι είναι συχνά αδύνατο να προσδιοριστεί αυτόματα πόσες φορές ένας βρόχος πρέπει να επαναλαμβάνεται συμβολικά. Ως αποτέλεσμα, η πλήρως αυτόματη επίσημη επαλήθευση είναι γενικά αδιευκρίνιστη.

Δεδομένων αυτών των θεμελιωδών περιορισμών, η Halmos δίνει προτεραιότητα στον αυτοματισμό έναντι της πληρότητας. Για το σκοπό αυτό, το Halmos έχει σχεδιαστεί για να εκτελεί περιορισμένο συμβολικό συλλογισμό για απεριόριστους βρόχους (όπου ο αριθμός των επαναλήψεων εξαρτάται από τις εισόδους του προγράμματος) ή πίνακες μεταβλητού μήκους (συμπεριλαμβανομένων των συμβολοσειρών). Αυτό θυσιάζει κάποια πληρότητα, αλλά επιτρέπει στο Halmos να αποφύγει την απαίτηση από τον χρήστη να παρέχει πρόσθετους σχολιασμούς, όπως αμετάβλητους βρόχους.

Για παράδειγμα, εξετάστε την ακόλουθη επαναληπτική έκδοση του isPowerOfTwo() συνάρτηση, η οποία διαθέτει έναν απεριόριστο βρόχο while, όπου ο αριθμός των επαναλήψεων βρόχου καθορίζεται από τον ελάχιστο αριθμό bit που απαιτείται για την αναπαράσταση του αριθμού εισόδου.

Ο Halmos επαναλαμβάνει συμβολικά αυτόν τον απεριόριστο βρόχο μόνο μέχρι ένα καθορισμένο όριο. Για παράδειγμα, εάν το όριο οριστεί στο 3, το Halmos θα επαναλάβει τον βρόχο το πολύ 3 φορές και δεν θα λάβει υπόψη τιμές εισόδου που θα προκαλούσαν τον βρόχο να επαναληφθεί περισσότερες από 3 φορές (δηλαδή, οποιεσδήποτε τιμές μεγαλύτερες ή ίσες με 2^3 ). Στη συγκεκριμένη περίπτωση, η ρύθμιση του ορίου στο 256 ή υψηλότερο θα επέτρεπε στον Χαλμό να ολοκληρωθεί.

Επίδειξη: Επίσημη επαλήθευση του ERC721A με το Halmos

Για να δείξουμε τις δυνατότητες του Χαλμού, το χρησιμοποιήσαμε για να δοκιμάσουμε συμβολικά και να επαληθεύσουμε επίσημα ERC721A, μια εξαιρετικά βελτιστοποιημένη για αέρια εφαρμογή του προτύπου ERC721 που επιτρέπει τη κοπή κατά παρτίδες με σχεδόν το ίδιο κόστος με την απλή κοπή. Το ERC721A περιλαμβάνει πολλά καινοτόμα βελτιστοποιήσεις για να επιτευχθεί αυτή η αποτελεσματικότητα· Για παράδειγμα, το αέριο μπορεί να εξοικονομηθεί καθυστερώντας τις ενημερώσεις στα δεδομένα ιδιοκτησίας του διακριτικού έως ότου μεταφερθεί το διακριτικό και όχι κατά τη στιγμή της κοπής. Αυτό απαιτεί τη χρήση πολύπλοκων δομών δεδομένων και αλγορίθμων για την αποτελεσματική ανάκτηση πληροφοριών ιδιοκτησίας από τη δομή δεδομένων τεμπέλης. Και παρόλο που αυτή η βελτιστοποίηση βελτιώνει την απόδοση του αερίου, αυξάνει επίσης την πολυπλοκότητα του κώδικα και καθιστά δύσκολη την απόδειξη της ορθότητας της υλοποίησης. Αυτό καθιστά το ERC721A καλό υποψήφιο για επίσημη επαλήθευση, καθώς μπορεί να αυξήσει την εμπιστοσύνη στην υλοποίηση και να ωφελήσει τους πιθανούς χρήστες.

Συμβολικές ιδιότητες δοκιμής

Δεδομένου ότι οι υπάρχουσες δοκιμές για το ERC721A γράφτηκαν σε JavaScript με Hardhat (το οποίο δεν υποστηρίζεται προς το παρόν από το Halmos), γράψαμε νέες δοκιμές στο Solidity για τις λειτουργίες του κύριου σημείου εισόδου: mint(), burn(), να transfer(). Αυτές οι δοκιμές έλεγξαν ότι κάθε συνάρτηση ενημερώνει σωστά την ιδιοκτησία και το υπόλοιπο του διακριτικού και επηρεάζει μόνο τους σχετικούς χρήστες χωρίς να αλλάζει το υπόλοιπο ή την ιδιοκτησία άλλων χρηστών. Το τελευταίο δεν είναι ασήμαντο να αποδειχθεί λόγω της χρήσης του αλγόριθμου lazy δομής δεδομένων στο ERC721A. Για παράδειγμα, η ακόλουθη δοκιμή ελέγχει ότι το transfer() Η συνάρτηση ενημερώνει σωστά την ιδιοκτησία του καθορισμένου διακριτικού:

Μια άλλη δοκιμή ελέγχει ότι το transfer() Η συνάρτηση δεν αλλάζει την ισορροπία για άλλες διευθύνσεις, κάτι που είναι δύσκολο να αποδειχθεί όπως αναφέρθηκε προηγουμένως:

Αποτελέσματα επαλήθευσης

Πραγματοποιήσαμε ένα πείραμα επαλήθευσης χρησιμοποιώντας το Halmos στο έξυπνο συμβόλαιο ERC721A γράφοντας ένα σύνολο Δοκιμή 19. Οι δοκιμές διεξήχθησαν μέσω του Χαλμού με ένα όριο ξετυλίγματος βρόχου 3, το οποίο χρειάστηκε 16 λεπτά για να ολοκληρωθεί. Η ανάλυση του χρόνου επαλήθευσης φαίνεται στον παρακάτω πίνακα. Το πείραμα διεξήχθη σε MacBook Pro με τσιπ M1 Pro και 16 GB μνήμης.

Δοκιμή	Φορές)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testBurnOtherBalancePreservation	5.69
testBurnOtherOwnershipPreservation	189.70
testBurnOwnershipUpdate	3.81
testBurnΑπαιτήσεις	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOwnershipPreservation	5.74
testMintOwnershipUpdate	1.38
testMintΑπαιτήσεις	0.09
testTransferBalance Αμετάβλητο	9.03
TestTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanged	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOwnership Preservation	430.61
testTransferOwnershipUpdate	18.71
testTransfer Requirements	149.18

Ενώ οι περισσότερες δοκιμές ολοκληρώθηκαν σε λίγα δευτερόλεπτα, μερικές από αυτές χρειάστηκαν αρκετά λεπτά. Αυτές οι χρονοβόρες δοκιμές ήταν δύσκολο να επαληθευτούν λόγω της περίπλοκης φύσης των περιπτώσεων που έπρεπε να εξεταστούν και σχετίζονταν στενά με την ορθότητα του αλγορίθμου lazy δομής δεδομένων.

Συνολικά, τα αποτελέσματα αυτού του πειράματος δείχνουν ότι ο Halmos είναι σε θέση να επαληθεύσει αποτελεσματικά την ορθότητα του κώδικα έξυπνου συμβολαίου. Παρέχει αυξημένη εμπιστοσύνη στην ακεραιότητα του κώδικα, παρά την πολυπλοκότητα και τις πιθανές περιπτώσεις αιχμής του έξυπνου συμβολαίου.

Πειραματιστείτε με ένεση σφάλματα

Για να δείξουμε την αποτελεσματικότητα του περιορισμένου συλλογισμού του Halmos, το χρησιμοποιήσαμε για να εντοπίσουμε σφάλματα σε μια προηγούμενη έκδοση του συμβολαίου ERC721A. Αυτή η έκδοση είχε ένα πρόβλημα που δεν χειριζόταν σωστά την αριθμητική υπερχείλιση και δυνητικά επέτρεψε τη δημιουργία ομαδικής κοπής μεγάλου αριθμού διακριτικών, γεγονός που θα μπορούσε να σπάσει την ακεραιότητα της τεμπέλης δομής δεδομένων και να οδηγήσει σε ορισμένους χρήστες να χάσουν την ιδιοκτησία τους (πρόβλημα επιλυθεί στην τρέχουσα έκδοση). Πραγματοποιήσαμε το ίδιο σύνολο 19 δοκιμών για το ERC721A στην έκδοση buggy και ο Halmos μπόρεσε να βρει ένα αντιπαράδειγμα για τις ιδιότητες του mint() λειτουργία. Συγκεκριμένα, ο Halmos παρείχε τιμές εισόδου που οδήγησαν στο σενάριο εκμετάλλευσης που περιγράφηκε παραπάνω. Τα αποτελέσματα αυτού του πειράματος υποδεικνύουν ότι, παρά την ελλιπή του, ο περιορισμένος συλλογισμός του Halmos μπορεί να είναι ένας αποτελεσματικός τρόπος ανίχνευσης και πρόληψης εκμεταλλεύσιμων σφαλμάτων σε έξυπνα συμβόλαια.

Σχετική δουλειά

Επίσημα εργαλεία επαλήθευσης για το bytecode έξυπνου συμβολαίου Ethereum έχουν αναπτυχθεί από διάφορες ομάδες. Αυτά τα εργαλεία, συμπεριλαμβανομένου του Halmos, μπορούν να χρησιμοποιηθούν για τη διασφάλιση της ασφάλειας και της ορθότητας των έξυπνων συμβολαίων. Η σύγκριση και η κατανόηση των διαφορετικών χαρακτηριστικών, δυνατοτήτων και περιορισμών αυτών των εργαλείων μπορεί να βοηθήσει τους προγραμματιστές να επιλέξουν το καταλληλότερο για τις μοναδικές τους ανάγκες.

Ενώ το Halmos είναι μια πολύτιμη προσθήκη στο σύνολο εργαλείων που διατίθεται για την επαλήθευση έξυπνων συμβολαίων, προορίζεται να συμπληρώσει (όχι να αντικαταστήσει) τα υπάρχοντα εργαλεία. Οι προγραμματιστές μπορούν να συνδυάσουν το Halmos με άλλα εργαλεία για να επιτύχουν υψηλότερο επίπεδο διασφάλισης στα συμβόλαιά τους. Παρακάτω, συγκρίνουμε το Halmos με μερικά επιλεγμένα επίσημα εργαλεία που υποστηρίζουν bytecode EVM.

• K είναι ένα ισχυρό επίσημο πλαίσιο επαλήθευσης που επιτρέπει την απαγωγική επαλήθευση και την απόδειξη διαδραστικών θεωρημάτων. Η υποκείμενη θεωρία και η εφαρμογή του παρέχουν υψηλό επίπεδο εκφραστικότητας, καθιστώντας το κατάλληλο για την επαλήθευση πολύπλοκων προγραμμάτων και αλγορίθμων. Ωστόσο, θα πρέπει να σημειωθεί ότι το K δεν έχει σχεδιαστεί με μεγάλη έμφαση στην αυτοματοποιημένη επαλήθευση και στερείται ορισμένων χαρακτηριστικών αυτοματισμού που μπορεί να απαιτήσουν μεγαλύτερη μη αυτόματη προσπάθεια κατά τη διαδικασία επαλήθευσης. Για να χρησιμοποιήσετε το πλαίσιο K, οι επίσημες προδιαγραφές είναι γραμμένες στη γλώσσα K, η οποία πρέπει να μάθετε πριν τη χρήση. Η δύναμή του είναι ιδιαίτερα χρήσιμη για την επαλήθευση πολύπλοκων συστημάτων, τα οποία μπορεί να είναι δύσκολο να αναλυθούν με τη χρήση αυτοματοποιημένης συλλογιστικής.
• Certora είναι ένα επίσημο εργαλείο επαλήθευσης για έξυπνες συμβάσεις που εστιάζει στην αυτοματοποιημένη επαλήθευση και υποστηρίζει περιορισμένο έλεγχο μοντέλων, παρόμοιο με το Halmos. Για να χρησιμοποιήσετε το Certora, οι προγραμματιστές πρέπει να μάθουν τη νέα τους γλώσσα, CVL, για να γράψετε προδιαγραφές. Αυτή η γλώσσα επιτρέπει τη συνοπτική περιγραφή πολλών κρίσιμων ιδιοτήτων μέσω αμετάβλητων συμβολαίων, μια δυνατότητα που επί του παρόντος δεν υποστηρίζει ο Halmos. Παρά το γεγονός ότι είναι ένα ιδιόκτητο εργαλείο κλειστού κώδικα, το Certora παρέχει ισχυρά εργαλεία επίσημης επαλήθευσης, με συνεχή ανάπτυξη και καλή υποστήριξη χρηστών.
  
  Το Halmos, από την άλλη πλευρά, είναι ένα εργαλείο ανοιχτού κώδικα που είναι μικρότερης κλίμακας και επί του παρόντος δεν διαθέτει ορισμένες δυνατότητες που παρέχονται από την Certora, αλλά προορίζεται να χρησιμεύσει ως δημόσιο αγαθό και προορίζεται ως μια εξειδικευμένη λύση για γρήγορη επαλήθευση έξυπνων συμβολαίων χωρίς την ανάγκη για εκτεταμένη εγκατάσταση και συντήρηση.
• HEVM είναι ένα άλλο επίσημο εργαλείο επαλήθευσης που είναι παρόμοιο με το Halmos. Προηγουμένως ήταν μέρος του DappTools, το οποίο είναι πρόδρομος του Foundry. Τόσο το HEVM όσο και το Halmos έχουν το χαρακτηριστικό ότι δεν απαιτούν ξεχωριστή προδιαγραφή και μπορούν να εκτελέσουν συμβολικά υπάρχουσες δοκιμές για τον εντοπισμό παραβιάσεων ισχυρισμών. Αυτό επιτρέπει στους χρήστες να χρησιμοποιούν και τα δύο εργαλεία εναλλακτικά ή να τα εκτελούν παράλληλα για τις ίδιες δοκιμές, παρέχοντάς τους πολλαπλές επιλογές για συμβολικές δοκιμές.
  
  Αξίζει να σημειωθεί ότι, παρά τις ομοιότητές τους, τα HEVM και Halmos έχουν αναπτυχθεί ανεξάρτητα και διαφέρουν στις λεπτομέρειες εφαρμογής τους. ιδιαίτερα όσον αφορά τις βελτιστοποιήσεις και τις στρατηγικές συμβολικής συλλογιστικής. Επιπλέον, το HEVM είναι γραμμένο σε Haskell, ενώ το Halmos είναι γραμμένο σε Python, παρέχοντας έκθεση στο πλούσιο οικοσύστημα Python. Η δυνατότητα χρήσης και των δύο εργαλείων παρέχει στους χρήστες μεγαλύτερη ευελιξία και επιλογές για τη διασφάλιση της ασφάλειας και της ορθότητας των έξυπνων συμβολαίων.

Χαλμός είναι ανοιχτού κώδικα και αυτή τη στιγμή βρίσκεται σε φάση beta. Εργαζόμαστε ενεργά για νέα χαρακτηριστικά και λειτουργικότητα, συμπεριλαμβανομένων των κωδικών απάτης Foundry και πολλών άλλων βασικών χαρακτηριστικών χρηστικότητας. Θα εκτιμούσαμε πολύ τις σκέψεις σας σχετικά με το ποια χαρακτηριστικά είναι πιο σημαντικά και θα χαιρετούσαμε οποιαδήποτε σχόλια, προτάσεις και συνεισφορές για να κάνουμε το Halmos ένα καλύτερο εργαλείο για όλους.

**

Οι απόψεις που εκφράζονται εδώ είναι αυτές του μεμονωμένου προσωπικού της AH Capital Management, LLC ("a16z") που αναφέρεται και δεν είναι απόψεις της a16z ή των θυγατρικών της. Ορισμένες πληροφορίες που περιέχονται εδώ έχουν ληφθεί από τρίτες πηγές, συμπεριλαμβανομένων των εταιρειών χαρτοφυλακίου κεφαλαίων που διαχειρίζεται η a16z. Αν και λαμβάνεται από πηγές που πιστεύεται ότι είναι αξιόπιστες, το a16z δεν έχει επαληθεύσει ανεξάρτητα τέτοιες πληροφορίες και δεν κάνει δηλώσεις σχετικά με την τρέχουσα ή διαρκή ακρίβεια των πληροφοριών ή την καταλληλότητά τους για μια δεδομένη κατάσταση. Επιπλέον, αυτό το περιεχόμενο μπορεί να περιλαμβάνει διαφημίσεις τρίτων. Η a16z δεν έχει ελέγξει τέτοιες διαφημίσεις και δεν υποστηρίζει κανένα διαφημιστικό περιεχόμενο που περιέχεται σε αυτές.

Αυτό το περιεχόμενο παρέχεται μόνο για ενημερωτικούς σκοπούς και δεν θα πρέπει να βασίζεται ως νομική, επιχειρηματική, επενδυτική ή φορολογική συμβουλή. Θα πρέπει να συμβουλευτείτε τους δικούς σας συμβούλους για αυτά τα θέματα. Οι αναφορές σε οποιουσδήποτε τίτλους ή ψηφιακά περιουσιακά στοιχεία είναι μόνο για ενδεικτικούς σκοπούς και δεν αποτελούν επενδυτική σύσταση ή προσφορά για παροχή επενδυτικών συμβουλευτικών υπηρεσιών. Επιπλέον, αυτό το περιεχόμενο δεν απευθύνεται ούτε προορίζεται για χρήση από επενδυτές ή υποψήφιους επενδυτές και δεν μπορεί σε καμία περίπτωση να γίνει επίκληση του κατά τη λήψη απόφασης για επένδυση σε οποιοδήποτε αμοιβαίο κεφάλαιο που διαχειρίζεται η a16z. (Μια προσφορά για επένδυση σε ένα αμοιβαίο κεφάλαιο a16z θα γίνει μόνο από το μνημόνιο ιδιωτικής τοποθέτησης, τη συμφωνία εγγραφής και άλλη σχετική τεκμηρίωση οποιουδήποτε τέτοιου κεφαλαίου και θα πρέπει να διαβαστεί στο σύνολό τους.) Τυχόν επενδύσεις ή εταιρείες χαρτοφυλακίου που αναφέρονται, αναφέρονται ή που περιγράφονται δεν είναι αντιπροσωπευτικές όλων των επενδύσεων σε οχήματα που διαχειρίζεται η a16z και δεν μπορεί να υπάρξει διαβεβαίωση ότι οι επενδύσεις θα είναι κερδοφόρες ή ότι άλλες επενδύσεις που θα πραγματοποιηθούν στο μέλλον θα έχουν παρόμοια χαρακτηριστικά ή αποτελέσματα. Μια λίστα με επενδύσεις που πραγματοποιήθηκαν από αμοιβαία κεφάλαια που διαχειρίζεται ο Andreessen Horowitz (εξαιρουμένων των επενδύσεων για τις οποίες ο εκδότης δεν έχει παράσχει άδεια για δημοσιοποίηση της a16z καθώς και των απροειδοποίητων επενδύσεων σε δημόσια διαπραγματεύσιμα ψηφιακά περιουσιακά στοιχεία) είναι διαθέσιμη στη διεύθυνση https://a16z.com/investments /.

Τα γραφήματα και τα γραφήματα που παρέχονται εντός προορίζονται αποκλειστικά για ενημερωτικούς σκοπούς και δεν θα πρέπει να βασίζονται σε αυτά όταν λαμβάνεται οποιαδήποτε επενδυτική απόφαση. Οι προηγούμενες αποδόσεις δεν είναι ενδεικτικές των μελλοντικών αποτελεσμάτων. Το περιεχόμενο μιλά μόνο από την ημερομηνία που υποδεικνύεται. Οποιεσδήποτε προβλέψεις, εκτιμήσεις, προβλέψεις, στόχοι, προοπτικές και/ή απόψεις που εκφράζονται σε αυτό το υλικό υπόκεινται σε αλλαγές χωρίς προειδοποίηση και μπορεί να διαφέρουν ή να είναι αντίθετες με τις απόψεις που εκφράζονται από άλλους. Ανατρέξτε στη διεύθυνση https://a16z.com/disclosures για πρόσθετες σημαντικές πληροφορίες.