xGov-18 Coq-avm library for AVM version 8

Governance xGov Proposals
1

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

2

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