xGov-18 Coq-avm library for AVM version 8

Author Mark (@mpetruska)

Category Tools

Focus Area Teal

Open-Source Yes

ALGO Requested 250000

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]

Link for details

1 Like

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.

A good overview on formal verification can be found here:
Formal Verification: Tezosā€™s Feature Nobody Talks About ā€“ Tezos Ukraine)
(although it is Tezos 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:

  • Coq is a general purpose interactive theorem prover
  • K framework is a specialized semantics framework
  • Coq is developed from the 1980s
  • K framework is fairly new, first publication is around the 2010s

Advantages/disadvantages of using Coq:

  • Coq is regarded as a highly trusted tool when used with the Coq standard
    library (no additional axioms). (See also: Presentation Ā· coq/coq Wiki Ā· GitHub, foundations - How true are theorems proved by Coq? - MathOverflow)
  • 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.)
2 Likes

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?

2 Likes

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.

3 Likes

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

1 Like

Hello, Can someone explain what COQ-AVM in laymen terms is?
Whatā€™s the purpose of coq-avm library?

The coq-avm library, once it is finished will:

  1. Make it possible to use Coq to prove mathematical properties of Algorand smart contracts
  2. These proofs can be used in code audits.
  3. Aid in future TEAL language/op code design.
  4. Provide formal specifications of the behavior of TEAL scripts
  5. Potentially provide formal proofs on smart contract/logicsig execution consistency between different versions of AVM.

I hope this clears it up, please ask away, if anything needs more details. ā€œThere are no stupid questions.ā€

1 Like

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.

No one in the Inc. is working anything similar to this, double checked it with them.

1 Like