Stream: Coq workshop 2020

Topic: [M6] Verifying, testing and running smart contracts in...

Théo Zimmermann (Jun 24 2020 at 11:22):

This is the topic to ask questions on the talk "Verifying, testing and running smart contracts in ConCert".

Emilio Jesús Gallego Arias (Jul 06 2020 at 12:50):

Talk starting now!

Anton Trunov (Jul 06 2020 at 13:11):

Thanks for the talk!
Q: Could you expand a bit more on the manual generators for randomized testing? (this is something that reasonates with my experience as well)

Emilio Jesús Gallego Arias (Jul 06 2020 at 13:12):

Q: Do you expect having to use at some point some logical framework, such as Iris, CFML, some relational logic,...

Michael Soegtrop (Jul 06 2020 at 13:13):

Did you look into CertiCoq for extraction?

Bas Spitters (Jul 06 2020 at 13:15):

@Michael Soegtrop Yes, that's the plan. We are using metacoq and when certicoq becomes available it will compile everything for us to Clight.
In fact, as @Danil Annenkov mentioned we are already doing some optimizations that could benefit certicoq.

Jakob Botsch Nielsen (Jul 06 2020 at 13:15):

@Emilio Jesús Gallego Arias So far we have not felt the need for it, we represent the semantics of blockchain execution as a simple inductive relation in Coq and then provide some tactics to make reasoning about it easy. It means we generally are able to lift many functional correctness proofs about smart contracts (i.e. about their functions) directly to proofs about their visible behavior in traces

Hugo Herbelin (Jul 06 2020 at 13:16):

How is produced the actual Liquidity or Midlang code (if there is such)? With a plugin?

Jakob Botsch Nielsen (Jul 06 2020 at 13:16):

The main reason we don't need a complicated program logic is probably that many of the newer blockchains use simple functional languages without the imperative features that are usually hard to reason about

Danil Annenkov (Jul 06 2020 at 13:16):

@Anton Trunov Generating random states and traces turns out to give many discards due to not meeting various well-formedness conditions. So tailoring the generators gives a much better result.

Jakob Botsch Nielsen (Jul 06 2020 at 13:18):

Hugo Herbelin said:

How is produced the actual Liquidity or Midlang code (if there is such)? With a plugin?

We use MetaCoq and then operate purely on the quoted terms, which we do our optimizations on. Then we have some pretty printers written in Gallina that just print the processed ASTs to Midlang/Liquidity (so we just use Compute or MetaCoq's Run TemplateProgram)

Danil Annenkov (Jul 06 2020 at 13:19):

@Anton Trunov E.g. contracts must be deployed on particular addresses, there should be enough balance to perform transfers and so on.

Emilio Jesús Gallego Arias (Jul 06 2020 at 13:21):

@Jakob Botsch Nielsen thanks; I would expected you may need some relational / modal reasoning for example over traces; of even some properties may be inherently relational so you would need to compare to runs of the contract?

Danil Annenkov (Jul 06 2020 at 13:26):

@Michael Soegtrop CertiCoq has many levels, some of them also might be a good point for extraction. But the main issue is that all the code is untyped and "fully certified" extraction should also say something about typing guarantees in a target language. I am not sure it's can be done easily currently.

Karl Palmskog (Jul 06 2020 at 13:27):

comment: I think Obj.magic support in Standard ML is compiler-specific, e.g., https://www.smlnj.org/doc/SMLofNJ/pages/unsafe.html#SIG:UNSAFE.cast:VAL (Unsafe.cast for SMLNJ)

Arthur Charguéraud (Jul 06 2020 at 13:27):

(deleted)

Hugo Herbelin (Jul 06 2020 at 13:29):

@Jakob Botsch Nielsen : When you say pretty-printer, you mean notations (and use of formatting boxes), or idtac-based pretty-printing? And how does the pretty-printed code compare to what Extraction would pretty-print (for say OCaml)? Conversely, are you saying that Extraction pretty-printing part could be rewritten using Print?

Danil Annenkov (Jul 06 2020 at 13:29):

@Emilio Jesús Gallego Arias We have some "rudimentary" machinery (like reachability), we plan to add some temporal operators on traces.

Anton Trunov (Jul 06 2020 at 13:29):

Danil Annenkov said:

Anton Trunov E.g. contracts must be deployed on particular addresses, there should be enough balance to perform transfers and so on.

@Danil Annenkov The address space needs to be trimmed severely in order to get any useful results. Is that correct?

Bas Spitters (Jul 06 2020 at 13:29):

@Karl Palmskog Yes, that was also our conclusion.
@Théo Zimmermann this was the work that I mentioned before, it gives experimental extraction to elm.

Danil Annenkov (Jul 06 2020 at 13:30):

I think Obj.magic support in Standard ML is compiler-specific, e.g., https://www.smlnj.org/doc/SMLofNJ/pages/unsafe.html#SIG:UNSAFE.cast:VAL (Unsafe.cast for SMLNJ)

@Karl Palmskog thanks! Yes, this is also confirms what we found.

Danil Annenkov (Jul 06 2020 at 13:31):

The address space needs to be trimmed severely in order to get any useful results. Is that correct?

@Anton Trunov yes, exactly.

Jakob Botsch Nielsen (Jul 06 2020 at 13:35):

Emilio Jesús Gallego Arias said:

Jakob Botsch Nielsen thanks; I would expected you may need some relational / modal reasoning for example over traces; of even some properties may be inherently relational so you would need to compare to runs of the contract?

Yes you are right, for certain hyper properties you would need this kind of reasoning. However so far we have focused mostly on correctness properties for existing contracts, so have no had a need for this yet

Michael Soegtrop (Jul 06 2020 at 13:38):

@Danil Annenkov : thanks - so the issue is that you do not need just safe executable code, but code which is also understandable / reviewable / trustworthy on its own? Don't some of the blockchains (I think e.g. Ethereum) have assembly code as their contract language?

Bas Spitters (Jul 06 2020 at 13:40):

@Michael Soegtrop The issue is that we want our extracted code to type check. We cannot "cheat" using obj.magic.

[ Ethereum mostly uses solidity (~javascript) and compiles to a custom VM. ]

Danil Annenkov (Jul 06 2020 at 13:41):

@Hugo Herbelin The pretty-printing in our case is just a Coq function producing a string with a program. So it all happens in Coq and we have full control over the implementation without the need of writing OCaml plugin.

Jakob Botsch Nielsen (Jul 06 2020 at 13:42):

Hugo Herbelin said:

Jakob Botsch Nielsen : When you say pretty-printer, you mean notations (and use of formatting boxes), or idtac-based pretty-printing? And how does the pretty-printed code compare to what Extraction would pretty-print (for say OCaml)? Conversely, are you saying that Extraction pretty-printing part could be rewritten using Print?

By pretty printers, I mean just Coq functions that operate on an inductive definition of terms (the code is here: https://github.com/jakobbotsch/ConCert/blob/b3b6cbaf86b2f13cf68d22c4f091bbe8628375f7/extraction/theories/MidlangExtract.v#L285)
The pretty printing is largely similar to what the built in extraction does. We have more separation between erasure and optimization than built in extraction does (i.e. our process is quote -> erase -> optimize -> print, while built-in extraction does something like erase/optimize -> print).

Hugo Herbelin said:

Conversely, are you saying that Extraction pretty-printing part could be rewritten using Print?

Yes, I think this should be very possible. MetaCoq's erasure gets us a lot of the way; the missing bits is erasure of inductives, which we have in ConCert, and then some form of retyping to figure out where to insert Obj.magic (which we don't have). By the way, there has been some discussion on verified extraction to Ocaml in the MetaCoq repo: https://github.com/MetaCoq/metacoq/issues/163

Jakob Botsch Nielsen (Jul 06 2020 at 13:44):

Of course verified extraction takes a lot more effort since it will also require a development of Ocaml's semantics in Coq.

Danil Annenkov (Jul 06 2020 at 13:44):

@Michael Soegtrop True, Ethereum uses byte-code, but there are several implementations that execute something more high-level (e.g. Michelson or Love https://medium.com/dune-network/love-a-new-smart-contract-language-for-the-dune-network-a217ab2255be).

Jakob Botsch Nielsen (Jul 06 2020 at 13:56):

I should also mention that we cannot deal with > rank-1 types in Elm/Liquidity due to the lack of Obj.magic, so our type erasure bails out as soon as it notices the type is not in prenex form. This would need to be expanded for extraction to Ocaml.

Last updated: May 31 2023 at 04:01 UTC