Coq-avm library

General
1

Project introduction document:

Any feedbacks are welcome.

2

Do you know about KAVM from Runtime Verification?

3

Yes, I even mention it in the pdf.

4

I read it twice and don’t see it. Am I missing something?

5

Well, it’s kind of hidden… mention in point 2.2.

6

Ah I see it now thanks.

  1. How do you see the key differences between coq-avm and KAVM?
  2. In both cases, what do you think should be the strategy for maintaining the model as AVM (and ABI) evolves?

We were talking with RV about the idea of having a langspec be an input to some process where one of the KAVM’s outputs is a langspec, so discrepancies can be highlighted. The obvious “ideal” solution would be to have the go-lang Assembler itself generated directly from the model, so there is a single source of truth, but that would mean putting RV on the critical path of Algorand as a project in its entirety.

7

The key differences between KAVM and coq-avm are the underlying technologies:
The K framework is “a rewrite-based executable semantic framework”, it specializes in semantics and program execution.
Coq is a more “general” interactive theorem prover with very good modelling capabilities. In my opinion modelling the interactions of a more complex dapp with multiple smart contracts/smart signatures in Coq would be much easier with the help of the coq-avm library, because of this.

My plan for the maintenance of coq-avm is to implement version 8 first and have other versions in the same library, but completely separate from each other to make sure that unintended changes do not “bleed” over to other versions. I’m planning to do the implementation purely based on the documentation, and then have a thorough test phase to check that the semantics of the AVM accurately describe the actual go implementation. This way it would be easy to spot problems/typos in the documentation.

I can showcase the library over a zoom call to clarify other questions.

8

Here is a more thorough explanation of the differences of K framework and Coq: K vs. Coq as Language Verification Frameworks (Part 1 of 3)

There are some things that not entirely correct in the summary (part 3). The main problem is that they provide a method of developing operational semantics for the given language, which of course is not executable directly. My approach is different in coq-avm, as the main intention was to provide executable semantics for AVM programs, which Coq is perfectly capable of. Also about the “missing” features for language declarations: Coq supports very flexible custom notations, most mentioned missing features can be implemented/simulated by these notations.