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