Document Open Access Logo

Towards a Mechanization of Fraud Proof Games in Lean

Authors Martín Ceresa , César Sánchez

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2025.5.pdf
  • Filesize: 0.61 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Software and its engineering → Correctness
  • Software and its engineering → Software libraries and repositories
  • Theory of computation → Interactive proof systems
  • Theory of computation → Program reasoning
  • Theory of computation → Program constructs
Keywords
  • blockchain
  • formal methods
  • layer-2
  • optimistic rollups
  • arbitration games

Metrics

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

Abstract

Arbitration games from Referee Delegation of Computations are central to layer two optimistic rollup architectures (L2), one of the most prominent mechanisms for scaling blockchains. L2 blockchains operate on the principle that computations are valid unless proven otherwise. Challenging incorrect computations requires users to construct fraud proofs through a dispute resolution process that involves two opposing players. Fraud proofs are objects that establish when proposed computations are invalid, and they are so computationally small and cheap that can be checked by the underlying trusted blockchain. Arbitration games, this challenging process, involve one player posing strategic questions and another player revealing details about computations.
Arbitration games start from the posting of Disputable Assertions (DAs), DAs contain partial information about computations including their result. Since there is no trust between players, hashes are posted as compact witnesses of knowledge. One player provides information decomposing hashes while the other decides which "path" to take navigating the computation trace. When a path is exhausted, all the required information to compute the result from the data provided following the path has been revealed and the path can be proven to be faulty or correct.
We explore in this paper the formalization of arbitration games in Lean4, introducing the first machine-checkable strategies that honest players can play guaranteeing success. These strategies ensure: on one side, the successful debunking of dishonest computations via the construction of fraud proofs, while in the other, the successful navigation of the challenge process through correct answers. In short, these are the winning strategies that honest players (on both sides) can follow. We explore in this paper formal abstractions to capture disputable assertions, arbitration games on finite binary trees asserting data-availability and membership, game transformations, and then discuss how to work towards a general formal framework for referee delegation of computations.

Cite As Get BibTex

Martín Ceresa and César Sánchez. Towards a Mechanization of Fraud Proof Games in Lean. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/OASIcs.FMBC.2025.5

Author Details

Martín Ceresa
  • IMDEA Software Institute, Madrid, Spain
César Sánchez
  • IMDEA Software Institute, Madrid, Spain

Funding

Partially funded by DECO Project (PID2022-138072OB-I00) - funded by MCIN/AEI/ 10.13039/501100011033 and by the ESF+ - and by grant from Nomadic Labs and the Tezos Foundation.

Acknowledgements

Thanks to Margarita Capretto for her insightful ideas and help.

Supplementary Materials

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3-27, 2005. Applied Semantics: Selected Topics. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  2. Wolfgang Ahrendt and Richard Bubel. Functional verification of smart contracts via strong data integrity. In Proc. of ISoLA (3), number 12478 in LNCS, pages 9-24. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_2.
  3. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. ConCert: a smart contract certification framework in Coq. In Proc. of the 9th ACM SIGPLAN Int'l Conf. on Certified Programs and Proofs (CPP'20), pages 215-218. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373829.
  4. Shaun Azzopardi, Joshua Ellul, and Gordon J. Pace. Monitoring smart contracts: ContractLarva and open challenges beyond. In Proc. of the 18th International Conference on Runtime Verification (RV'18), volume 11237 of LNCS, pages 113-137. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03769-7_8.
  5. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In Proc. of the FM 2019 International Workshops, Part I, volume 12232 of LNCS, pages 368-379. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_28.
  6. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fourneta, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella Béguelin. Formal verification of smart contracts: Short paper. In Proc. of Workshop on Programming Languages and Analysis for Security (PLAS@CCS'16), pages 91-96. ACM, 2016. URL: https://doi.org/10.1145/2993600.2993611.
  7. Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, and Yannick Zakowski. Games and strategies using coinductive types. In International Conference on Types for Proofs and Programs, 2023. Google Scholar
  8. Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, and Yannick Zakowski. An abstract, certified account of operational game semantics. In European Symposium on Programming, (to appear in) 2025. Google Scholar
  9. Vitalik Buterin. Ethereum: A next-generation smart contract and decentralized application platform, 2014. Accessed: 2025-05-06. URL: https://github.com/ethereum/wiki/wiki/White-Paper.
  10. Ran Canetti, Ben Riva, and Guy N. Rothblum. Refereed delegation of computation. Information and Computation, 226:16-36, 2013. URL: https://doi.org/10.1016/J.IC.2013.03.003.
  11. Margarita Capretto, Martín Ceresa, and César Sánchez. Transaction monitoring of smart contracts. In Thao Dang and Volker Stolz, editors, Proc. of the 22nd Int'l Conf. on Runtime Verification (RV'22), volume 13498 of LNCS, pages 162-180. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17196-3_9.
  12. Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sánchez, and César Sánchez. A decentralized sequencer and data availability committee for rollups using set consensus, 2025. URL: https://doi.org/10.48550/arXiv.2503.05451.
  13. Martín Ceresa and César Sánchez. Fraud Proof Games. Software, version 1., (visited on 2025-05-06). URL: https://gitlab.software.imdea.org/martin.ceresa/leanfpgames
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23003
  14. Martín Ceresa and César Sánchez. Multi: A Formal Playground for Multi-Smart Contract Interaction. In Zaynah Dargaye and Clara Schneidewind, editors, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022), volume 105 of Open Access Series in Informatics (OASIcs), pages 5:1-5:16, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2022.5.
  15. Sylvain Conchon, Alexandrina Korneva, and Fatiha Zaïdi. Verifying smart contracts with Cubicle. In Proc. of the 1st Workshop on Formal Methods for Blockchains (FMBC'19), volume 12232 of LNCS, pages 312-324. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_23.
  16. Tyler Crain, Christopher Natoli, and Vincent Gramoli. Redbelly: A secure, fair and scalable open blockchain. In 2021 IEEE Symposium on Security and Privacy (SP), pages 466-483, 2021. URL: https://doi.org/10.1109/SP40001.2021.00087.
  17. Joshua Ellul and Gordon J. Pace. Runtime verification of Ethereum smart contracts. In Proc. of the 14th European Dependable Computing Conference (EDCC'18), pages 158-163. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/EDCC.2018.00036.
  18. J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24(1):68-95, January 1977. URL: https://doi.org/10.1145/321992.321997.
  19. Abdelatif Hafid, Abdelhakim Senhaji Hafid, and Mustapha Samih. Scaling blockchains: A comprehensive survey. IEEE Access, 8:125244-125262, 2020. URL: https://doi.org/10.1109/ACCESS.2020.3007251.
  20. Peter Hancock and Pierre Hyvernat. Programming interfaces and basic topology. Annals of Pure and Applied Logic, 137(1):189-239, 2006. URL: https://doi.org/10.1016/j.apal.2005.05.022.
  21. Harry Kalodner, Steven Goldfeder, Xiaoqi Chen, S. Matthew Weinberg, and Edward W. Felten. Arbitrum: Scalable, private smart contracts. In 27th USENIX Security Symposium, pages 1353-1370. USENIX Assoc., 2018. URL: https://www.usenix.org/conference/usenixsecurity18/presentation/kalodner.
  22. Ryan Lavin, Xuekai Liu, Hardhik Mohanty, Logan Norman, Giovanni Zaarour, and Bhaskar Krishnamachari. A survey on the applications of zero-knowledge proofs, 2024. URL: https://doi.org/10.48550/arXiv.2408.00243.
  23. Ao Li, Jemin Andrew Choi, and an. Long. Securing smart contract with runtime validation. In Proc. of ACM PLDI'20, pages 438-453. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385982.
  24. Andrew Miller, Michael Hicks, Jonathan Katz, and Elaine Shi. Authenticated data structures, generically. SIGPLAN Not., 49(1):411-423, January 2014. URL: https://doi.org/10.1145/2578855.2535851.
  25. Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system, December 2008. Accessed: 2025-05-06. URL: https://bitcoin.org/bitcoin.pdf.
  26. Zeinab Nehaï and François Bobot. Deductive proof of industrial smart contracts using Why3. In Proc. of the 1st Workshop on Formal Methods for Blockchains (FMBC'19), volume 12232 of LNCS, pages 299-311. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_22.
  27. Sebastiano Peluso, Alexandru Turcu, Roberto Palmieri, Giuliano Losa, and Binoy Ravindran. Making fast consensus generally faster. In 2016 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pages 156-167, 2016. URL: https://doi.org/10.1109/DSN.2016.23.
  28. Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. VerX: Safety verification of smart contracts. In Proc of the 41st IEEE Symp. on Security and Privacy (S&P'20), pages 1661-1677. IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00024.
  29. Daian Phil. Analysis of the DAO exploit, 2016. URL: https://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/.
  30. Matija Pretnar. An introduction to algebraic effects and handlers. invited tutorial paper. Electronic Notes in Theoretical Computer Science, 319:19-35, 2015. The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI). URL: https://doi.org/10.1016/j.entcs.2015.12.003.
  31. Jonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert, and Richard Bubel. Formal analysis of smart contracts: Applying the KeY system. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich, editors, Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, volume 12345 of Lecture Notes in Computer Science, pages 204-218. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64354-6_8.
  32. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Scilla: a smart contract intermediate-level Language. CoRR, abs/1801.00687, 2018. URL: https://arxiv.org/abs/1801.00687.
  33. Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. SmartPulse: Automated checking of temporal properties in smart contracts. In Proc. of the 42nd IEEE Symp. on Security and Privacy (S&P'21). IEEE, May 2021. URL: https://www.microsoft.com/en-us/research/publication/smartpulse-automated-checking-of-temporal-properties-in-smart-contracts/.
  34. Nick Szabo. Smart contracts: Building blocks for digital markets. Extropy, 16, 1996. Google Scholar
  35. Louis Tremblay Thibault, Tom Sarry, and Abdelhakim Senhaji Hafid. Blockchain scaling using rollups: A comprehensive survey. IEEE Access, 10:93039-93054, 2022. URL: https://doi.org/10.1109/ACCESS.2022.3200051.
  36. Gang Wang, Zhijie Jerry Shi, Mark Nixon, and Song Han. SoK: Sharding on blockchain. In Proceedings of the 1st ACM Conference on Advances in Financial Technologies, pages 41-61, 2019. URL: https://doi.org/10.1145/3318041.3355457.
  37. Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, 151:1-32, 2014. Google Scholar
  38. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in coq. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371119.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact