-
Notifications
You must be signed in to change notification settings - Fork 99
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
xGov-18 - coq-avm library #18
Conversation
Hi, i am programmer, but i dont know much about formal proofs.. Can you elaborate little more on the benefits? Who will benefit from this? I did read
By "Executable semantics for TEAL programs" you mean that we will have nice flow charts on the teal apps? By "Formal verification" you mean that if anybody writes any byte code, you tell true or false if it complies with specific standard of teal? Can you just decompile teal and compile and check if it produce same bytes? By "Toolset/tactics for developers to create formal proofs of AVM programs" you mean that developers have to write some proofs that their programs are really compiled to teal? Or do you mean that you create some testing framework for algorand smart contacts/logic sigs that runs without the node? Btw if you are deep into teal, please consider working on teal to pyteal decomiler. I think whole community would appriciate this. It would boost growth of the ecosystem as anybody could just decompile into more readable programs any applications out there, it would easy the audits and more.. |
Hi! |
Ok, let me rephrase the question.. The AMM algorighm is simple matematical formula which should be implemented in the smart contract. Do you expect AMM providers to create "mathematical proof" that their smart contracts are valid? How would it look like? What advantages would this type of proof would have in comparision with standard unit,integration and end2end testing? |
I think there is a huge misunderstanding. I do not expect anyone to do anything, except myself. |
The specifics of this proposal go beyond my understanding and I'd image similar applies also for many xGovs.
P.S. Perhaps @joe-p, @jannotti, @cusma, @FrankSzendzielarz could chime in to help xGovs understand the soundness of this proposal. |
Clarification
The aim of the coq-avm library is to provide a toolset that helps developing
formal verification proofs for smart contracts in Coq.
A good overview on formal verification can be found here:
https://ethereum.org/en/developers/docs/smart-contracts/formal-verification/
(although it is Ethereum related, the main concepts still apply).
Dfferences to K framework
Runtime Verification Inc. created the K framework also
implemented an
AVM semantics module
that can be used to verify programs that target the AVM.
How K framework differs from Coq:
Advantages/disadvantages of using Coq:
library (no additional axioms). (See also: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq, https://mathoverflow.net/questions/59520/how-true-are-theorems-proved-by-coq)
much more likely to have been discovered/fixed.
circles, hence it is likely that developers/researchers are more experienced in its
use.
also has general purpose mathematics modules.
etc.), thus language independent (any program that is compiled to AVM byte code
can be used as a source).
Advantages/disadvantages of using K framework:
targetting different languages.
only.
Opportunities
provide the same results when they're executed with version 8).
in the supported languages (e.g. OCaml, Scheme and Haskell). However, since the main
purpose of the library is precision not performance, the extracted programs may not
be the most effective.
AVM version 8 op codes. (Although using this tool might be unintuitive for developers not
familiar with Coq.)