Stream: Coq workshop 2020

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


view this post on Zulip 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".

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:50):

Talk starting now!

view this post on Zulip 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)

view this post on Zulip 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,...

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 13:13):

Did you look into CertiCoq for extraction?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Hugo Herbelin (Jul 06 2020 at 13:16):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Arthur Charguéraud (Jul 06 2020 at 13:27):

(deleted)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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. ]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: Feb 06 2023 at 06:29 UTC