Document Open Access Logo

Towards Contract Modules for the Tezos Blockchain (Short Paper)

Authors Thi Thu Ha Doan, Peter Thiemann

PDF
Thumbnail PDF

File

OASIcs.FMBC.2021.5.pdf
  • Filesize: 0.52 MB
  • 9 pages

Document Identifiers

Author Details

Thi Thu Ha Doan
  • University of Freiburg, Germany
Peter Thiemann
  • University of Freiburg, Germany

Funding

  • Doan, Thi Thu Ha: supported by a grant from the Tezos foundation.

Cite As Get BibTex

Thi Thu Ha Doan and Peter Thiemann. Towards Contract Modules for the Tezos Blockchain (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 5:1-5:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/OASIcs.FMBC.2021.5

Abstract

Programmatic interaction with a blockchain is often clumsy. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees.
Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entry point of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Specification languages
Keywords
  • contract API
  • modules
  • static checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter Schmitt, and Mattias Ulbrich. Deductive Software Verification – The KeY Book: From Theory to Practice, volume 10001. Springer-Verlag, January 2016. URL: https://doi.org/10.1007/978-3-319-49812-6.
  2. Davide Ancona, Giovanni Lagorio, and Elena Zucca. A core calculus for Java exceptions. In Linda M. Northrop and John M. Vlissides, editors, Proceedings of the 2001 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2001, Tampa, Florida, USA, October 14-18, 2001, pages 16-30. ACM, 2001. URL: https://doi.org/10.1145/504282.504284.
  3. Massimo Bartoletti. Smart contracts contracts. Frontiers Blockchain, 3:27, 2020. URL: https://doi.org/10.3389/fbloc.2020.00027.
  4. Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph M. Wintersteiger. Programming Z3. In Jonathan P. Bowen, Zhiming Liu, and Zili Zhang, editors, Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, volume 11430 of Lecture Notes in Computer Science, pages 148-201. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-17601-3_4.
  5. Giulio Caldarelli. Understanding the blockchain oracle problem: A call for action. Information, 11(11), 2020. Google Scholar
  6. Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO'05, page 342–363, Berlin, Heidelberg, 2005. Springer-Verlag. Google Scholar
  7. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  8. L. Goodman. Tezos - A self-amending crypto-ledger, 2014. URL: https://www.tezos.com/static/papers/white-paper.pdf.
  9. Martin Hentschel, Richard Bubel, and Reiner Hähnle. The symbolic execution debugger (SED): a platform for interactive symbolic execution, debugging, verification and more. International Journal on Software Tools for Technology Transfer, 21, October 2019. Google Scholar
  10. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969. Google Scholar
  11. Gary Leavens and Yoonsik Cheon. Design by contract with JML, 2006. URL: https://www.cs.ucf.edu/~leavens/JML/index.shtml.
  12. Kamran Mammadzada, Mubashar Iqbal, Fredrik Milani, Luciano García-Bañuelos, and Raimundas Matulevičius. Blockchain Oracles: A Framework for Blockchain-Based Applications, pages 19-34. Springer Verlag, September 2020. Google Scholar
  13. Roman Mühlberger, Stefan Bachhofner, Eduardo Castelló Ferrer, Claudio Di Ciccio, Ingo Weber, Maximilian Wöhrer, and Uwe Zdun. Foundational oracle patterns: Connecting blockchain to the off-chain world. Business Process Management: Blockchain and Robotic Process Automation Forum, page 35–51, 2020. Google Scholar
  14. Peter W. V. Tran-Jørgensen. Automated translation of VDM-SL to JML-annotated Java. Technical Report Electronics and Computer Engineering, 5(29), March 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact