Aarhus University Seal / Aarhus Universitets segl

Extracting smart contracts tested and verified in Coq

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Standard

Extracting smart contracts tested and verified in Coq. / Annenkov, Danil; Milo, Mikkel; Nielsen, Jakob Botsch; Spitters, Bas.

CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. ed. / Catalin Hritcu; Andrei Popescu. Association for Computing Machinery, 2021. p. 105-121.

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Harvard

Annenkov, D, Milo, M, Nielsen, JB & Spitters, B 2021, Extracting smart contracts tested and verified in Coq. in C Hritcu & A Popescu (eds), CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Association for Computing Machinery, pp. 105-121, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021, Virtual, Online, Denmark, 17/01/2021. https://doi.org/10.1145/3437992.3439934

APA

Annenkov, D., Milo, M., Nielsen, J. B., & Spitters, B. (2021). Extracting smart contracts tested and verified in Coq. In C. Hritcu, & A. Popescu (Eds.), CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021 (pp. 105-121). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439934

CBE

Annenkov D, Milo M, Nielsen JB, Spitters B. 2021. Extracting smart contracts tested and verified in Coq. Hritcu C, Popescu A, editors. In CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Association for Computing Machinery. pp. 105-121. https://doi.org/10.1145/3437992.3439934

MLA

Annenkov, Danil et al. "Extracting smart contracts tested and verified in Coq". and Hritcu, Catalin Popescu, Andrei (editors). CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Association for Computing Machinery. 2021, 105-121. https://doi.org/10.1145/3437992.3439934

Vancouver

Annenkov D, Milo M, Nielsen JB, Spitters B. Extracting smart contracts tested and verified in Coq. In Hritcu C, Popescu A, editors, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Association for Computing Machinery. 2021. p. 105-121 https://doi.org/10.1145/3437992.3439934

Author

Annenkov, Danil ; Milo, Mikkel ; Nielsen, Jakob Botsch ; Spitters, Bas. / Extracting smart contracts tested and verified in Coq. CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. editor / Catalin Hritcu ; Andrei Popescu. Association for Computing Machinery, 2021. pp. 105-121

Bibtex

@inproceedings{4f516ec723314b358c2c085622517949,
title = "Extracting smart contracts tested and verified in Coq",
abstract = "We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We 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. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, 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, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages. ",
keywords = "Blockchain, Certified programming, Code extraction, Coq, Formal verification, Proof assistants, Property-based testing, Smart contracts, Software correctness",
author = "Danil Annenkov and Mikkel Milo and Nielsen, {Jakob Botsch} and Bas Spitters",
year = "2021",
month = jan,
doi = "10.1145/3437992.3439934",
language = "English",
pages = "105--121",
editor = "Catalin Hritcu and Andrei Popescu",
booktitle = "CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021",
publisher = "Association for Computing Machinery",
address = "United States",
note = "10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 ; Conference date: 17-01-2021 Through 19-01-2021",

}

RIS

TY - GEN

T1 - Extracting smart contracts tested and verified in Coq

AU - Annenkov, Danil

AU - Milo, Mikkel

AU - Nielsen, Jakob Botsch

AU - Spitters, Bas

PY - 2021/1

Y1 - 2021/1

N2 - We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We 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. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, 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, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.

AB - We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We 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. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, 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, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.

KW - Blockchain

KW - Certified programming

KW - Code extraction

KW - Coq

KW - Formal verification

KW - Proof assistants

KW - Property-based testing

KW - Smart contracts

KW - Software correctness

UR - http://www.scopus.com/inward/record.url?scp=85100550870&partnerID=8YFLogxK

U2 - 10.1145/3437992.3439934

DO - 10.1145/3437992.3439934

M3 - Article in proceedings

AN - SCOPUS:85100550870

SP - 105

EP - 121

BT - CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021

A2 - Hritcu, Catalin

A2 - Popescu, Andrei

PB - Association for Computing Machinery

T2 - 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021

Y2 - 17 January 2021 through 19 January 2021

ER -