Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:45 - 19:00 at CPP - Security, Blockchains, and Smart Contracts Chair(s): Andreas Lochbihler

We implement extraction of Coq programs to functional languages based on MetaCoq’s certified erasure. As part of this, we implement an optimization pass to remove unused arguments of functions and constructors, making integration with the (often polymorphic) extracted code easier. This pass is proven correct over a weak call by value operational semantics that fits well with many functional languages. We argue that our extraction pipeline applies generally to these functional languages with a small trusted computing base of only MetaCoq and the pretty-printers into these languages. We apply this to two functional smart contract languages, Liquidity and Midlang, which are respectively similar to Ocaml and Elm. This is done in the context of the ConCert framework that allows proving properties of functional smart contracts. The extraction is exemplified by several programs, including a smart contract that uses dependent types, showing that we are able to handle non-trivial programs. We also contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. With ConCert’s executable specification our contracts are furthermore fully testable from within Coq. This enables us to integrate property-based testing into ConCert using QuickChick. We show that this is successful by testing complex contracts such as the congress contract (the essence of TheDAO), an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify them, and then extract them to functional smart contract languages, while retaining a small TCB.

Presentation Slides (extracting-smart-contracts-CPP2021.pdf)629KiB

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:45 - 19:30: Security, Blockchains, and Smart ContractsCPP at CPP
Chair(s): Andreas LochbihlerDigital Asset

Streamed session: https://youtu.be/Qak5mK92etU?t=2832

18:45 - 19:00
Extracting Smart Contracts Tested and Verified in Coq
Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Mikkel MiloConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University
Pre-print Media Attached File Attached
19:00 - 19:15
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari MiraldoDFINITY Foundation, Harold CarrOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Lisandra SilvaUniversity of Minho, Guy L. Steele Jr.Oracle Labs
Pre-print Media Attached
19:15 - 19:30
Towards formally verified compilation of tag-based policy enforcement
CHR ChhakPortland State University, Andrew TolmachPortland State University, Sean AndersonPortland State University
Pre-print Media Attached