xGov-18 - coq-avm library

mpetruska commented 1 year ago

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: https://ethereum.org/en/developers/docs/smart-contracts/formal-verification/ (although it is Ethereum 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: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq, https://mathoverflow.net/questions/59520/how-true-are-theorems-proved-by-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.)

scholtz commented 1 year ago

Hi, i am programmer, but i dont know much about formal proofs.. Can you elaborate little more on the benefits? Who will benefit from this?

I did read


## Benefits for the community
- Executable semantics for TEAL programs.
- Formal verification of Algorand smart contracts using Coq.
- Development of formal specification on the behaviour of op codes.
- Potential to provide formal proofs on smart contract/logicsig execution consistency between
  different versions of AVM. Prerequisite: implementation of the interpreter for other versions.
- Providing alternative to the AVM semantic library of the K Framework.
- Toolset/tactics for developers to create formal proofs of AVM programs.

By "Executable semantics for TEAL programs" you mean that we will have nice flow charts on the teal apps?

By "Formal verification" you mean that if anybody writes any byte code, you tell true or false if it complies with specific standard of teal? Can you just decompile teal and compile and check if it produce same bytes?

By "Toolset/tactics for developers to create formal proofs of AVM programs" you mean that developers have to write some proofs that their programs are really compiled to teal?

Or do you mean that you create some testing framework for algorand smart contacts/logic sigs that runs without the node?

Btw if you are deep into teal, please consider working on teal to pyteal decomiler. I think whole community would appriciate this. It would boost growth of the ecosystem as anybody could just decompile into more readable programs any applications out there, it would easy the audits and more..

mpetruska commented 1 year ago

Hi! Coq is usually used to state and prove mathematical properties of programs through equivalent transformations (reductions based on semantic rules). This way of verfying programs is usually referred to as formal verification. The attached pdf can provide more details, I'm also available for an online discussion to clarify the concepts further.

scholtz commented 1 year ago

Ok, let me rephrase the question..

The AMM algorighm is simple matematical formula which should be implemented in the smart contract.

Do you expect AMM providers to create "mathematical proof" that their smart contracts are valid? How would it look like?

What advantages would this type of proof would have in comparision with standard unit,integration and end2end testing?

mpetruska commented 1 year ago

I think there is a huge misunderstanding. I do not expect anyone to do anything, except myself. Programs/functions are formally specified by providing formal pre- and post-conditions. There is a very good example on page 6 of the pdf present in this PR: https://github.com/algorandfoundation/xGov/blob/759447da9ab17807bfe4f26d0800358d755e0899/Proposals/coq-avm-introduction.pdf , please have a look.

ShaperOfEntropy commented 1 year ago

The specifics of this proposal go beyond my understanding and I'd image similar applies also for many xGovs. Therefore, if you hope to get the grant approved, I would suggest to: 1) Add more of your qualifications to deliver this, e.g. a link to your LinkedIn https://hu.linkedin.com/in/mark-petruska-1a611527, and links to similar projects you have developed/contributed to and how widely used they are. 2) How will xGovs be able to verify your deliverables? Can you for example get some developers experienced in the field to attest to your deliverables? 3) Can you tag some other developers that would use this tool once its built? 4) How will the grant be spent? Will ALGO be sold on the market? If yes, using DEXs or CEXs? Or will a loan be taken against it in DeFi/CeFi?

P.S. Perhaps @joe-p, @jannotti, @cusma, @FrankSzendzielarz could chime in to help xGovs understand the soundness of this proposal.

algorandfoundation / xGov