Abstract
The aim is to finish the implementation of the coq-avm library for version 8 af the AVM. A summary of
the library can be found here: [coq-avm-introduction.pdf][1]
It seems that the initial proposal and document needs some further details to help
the community to measure its values. More details are below for those interested:
Clarification
The aim of the coq-avm library is to provide a toolset that helps developing
formal verification proofs for smart contracts in Coq.
Coq was around for longer, used in more projects, hence inconsistencies/problems are
much more likely to have been discovered/fixed.
Since it was around longer, it is much more discussed in academia and in engineering
circles, hence it is likely that developers/researchers are more experienced in its
use.
Coq has plenty of useful libraries implemented over the years, more tooling and
also has general purpose mathematics modules.
The coq-avm library targets AVM byte code, not a specific language (TEAL, pyTeal,
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:
Specialized framework, potentially more easy to develop executable sematics modules
targetting different languages.
Language specific implementation, it seems to me that KAVM targets the TEAL language
only.
Opportunities
An open source coq-avm library could help in designing new AVM instructions.
Possible to prove compiler consistency (e.g. all programs executed with version 7
provide the same results when theyāre executed with version 8).
Utilizing Coq program extraction would make it possible to generate AVM implementations
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.
Currently coq-avm provides a way to execute and āstep throughā (debug) 25 of the
AVM version 8 op codes. (Although using this tool might be unintuitive for developers not
familiar with Coq.)
Iāve read up on this as much as I think Iāll be able to understand. I admire wanting to expand the general tool set of Algorand, but Iām not sure about funding this through xGov at this time given the amount requested and that there are currently alternative methods for achieving the same result from what little I understand. That said, I understand very little of this except that it would be a new way to verify AVM development.
would appreciate any devs commenting on this since i definitely dont know enough about it to make a statement that is really informedā¦ @BunsanMuchi could you or someone else from vestige help here?
I know very little about Coq, since everything Iāve done with regards to formal theorem provers (which mind you, is not a lot) has been on Isabelleā¦
These type of tools are definitely interesting and needed, but as the application says kAVM was developed as a type of tool to do this (from my high level POV) and afaik it hasnāt become a standard tool used by developers today. So I donāt see how a Coq version would change this. Iām also wondering what the AlgoKit development team inside the foundation is building, and whether or not there might be a duplication of efforts. But Iām by no means qualified enough to make a full evaluation of this application. Also, considering the amount of resources and grants given to RunTime for the the development of kAVM the ask amount (believe it or not) seems to me slightly on the low side.
I am a bit late to comment but I support this proposal. Coq is an excellent tool and language and was actually used for formal verification of algorand consensus GitHub repo and Arxiv paper. I feel that having a coq implementation is more flexible (K limited to TEAL as mentioned in the op) and more community oriented as K is specific to runtime verification (actually I had never heard of it before reading this post) while coq is a well established academically-used language.
Although I think it would be interesting to get in touch with Algorand, Inc directly as they might also work on some coq development for algorand
Iām no specialist in this domain either, but if Coq provides a more widely accepted standard for formal verification that makes it easier, faster, and more cost-efficient to do, I think itās potentially worthwhile. Iād be interested to hear how much time could be saved by both developers and auditors if this was available.
As others have noted, I do think it would make sense to first check for any existing work in this area by the Inc., Foundation, and/or other known 3rd parties.