Document Open Access Logo

Formally Specifying Contract Optimizations with Bisimulations in Coq

Author Derek Sorensen

PDF HTML 5

Files

Thumbnail PDF
PDF
OASIcs.FMBC.2025.11.pdf
  • Filesize: 0.63 MB
  • 13 pages
HTML5 Logo HTML (experimental)
OASIcs.FMBC.2025.11.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • smart contract verification
  • formal methods
  • interactive theorem prover
  • smart contract upgradeability

Metrics

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

Abstract

The efficacy of formal verification of smart contracts depends on being able to correctly specify and carry out the verification of optimized code. However, code optimized for performance is rarely optimized for intelligibility, which can make formally verifying optimized code difficult and costly. To address this issue, we present a formal tool for reasoning about an optimized contract in terms of its reference implementation. This tool reduces the work of formally verifying an optimized contract to proving behavioral equivalence to the reference implementation.

Cite As Get BibTex

Derek Sorensen. Formally Specifying Contract Optimizations with Bisimulations in Coq. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/OASIcs.FMBC.2025.11

Author Details

Derek Sorensen
  • Department of Computer Science and Technology, University of Cambridge, UK

Supplementary Materials

References

  1. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. ConCert: A smart contract certification framework in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 215-228, New York, NY, USA, January 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373829.
  2. Cyril Cohen, Enzo Crance, and Assia Mahboubi. Trocq: proof transfer for free, with or without univalence. In European Symposium on Programming, pages 239-268. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_10.
  3. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In International Conference on Certified Programs and Proofs, pages 147-162. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_10.
  4. Hubert Garavel and Frédéric Lang. Equivalence checking 40 years after: A review of bisimulation tools. A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, pages 213-265, 2022. URL: https://doi.org/10.1007/978-3-031-15629-8_13.
  5. Osman Hasan and Sofiene Tahar. Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition, pages 7162-7170. IGI global, 2015. Google Scholar
  6. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, January 1985. URL: https://doi.org/10.1145/2455.2460.
  7. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, and Mooly Sagiv. Effectively-propositional reasoning about reachability in linked data structures. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 756-772, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39799-8_53.
  8. Kim G Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72(2-3):265-288, 1990. URL: https://doi.org/10.1016/0304-3975(90)90038-J.
  9. Robin Milner. Communication and concurrency. Prentice Hall International, 13, 1989. Google Scholar
  10. Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. Proof repair across type equivalences. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 112-127, 2021. URL: https://doi.org/10.1145/3453483.3454033.
  11. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, October 1998. URL: https://doi.org/10.1017/S0960129598002527.
  12. Davide Sangiorgi. Introduction to bisimulation and coinduction. Cambridge University Press, 2011. Google Scholar
  13. Derek Sorensen. FinCert. Software (visited on 2025-05-08). URL: https://github.com/dhsorens/FinCert/tree/FMBC-25, URL: https://doi.org/10.4230/artifacts.23081.
  14. Derek Sorensen. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. 5th International Workshop on Formal Methods for Blockchains (FMBC 2024), 2024. Google Scholar
  15. Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. Equivalences for free: univalent parametricity for effective transport. Proceedings of the ACM on Programming Languages, 2(ICFP):1-29, 2018. URL: https://doi.org/10.1145/3236787.
  16. Johan Van Benthem and Jan Bergstra. Logic of transition systems. Journal of Logic, Language and Information, 3:247-283, 1994. URL: https://doi.org/10.1007/BF01160018.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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