Hostname: page-component-745bb68f8f-g4j75 Total loading time: 0 Render date: 2025-01-12T04:28:38.133Z Has data issue: false hasContentIssue false
  • English
  • Français

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Part of: ICFP2018

Published online by Cambridge University Press:  26 February 2021

JOACHIM BREITNER ,
ANTAL SPECTOR-ZABUSKY Open the ORCID record for ANTAL SPECTOR-ZABUSKY [Opens in a new window] ,
YAO LI Open the ORCID record for YAO LI [Opens in a new window] ,
CHRISTINE RIZKALLAH ,
JOHN WIEGLEY ,
JOSHUA COHEN  and
STEPHANIE WEIRICH
JOACHIM BREITNER
Affiliation:
DFINITY Stiftung, Zug, Switzerland (e-mail: [email protected])
ANTAL SPECTOR-ZABUSKY
Affiliation:
University of Pennsylvania, Philadelphia, USA (e-mail: [email protected])
YAO LI
Affiliation:
University of Pennsylvania, Philadelphia, USA (e-mail: [email protected])
CHRISTINE RIZKALLAH
Affiliation:
University of New South Wales, Sydney, Australia (e-mail: [email protected])
JOHN WIEGLEY
Affiliation:
DFINITY Stiftung, Zug, Switzerland (e-mail: [email protected])
JOSHUA COHEN
Affiliation:
University of Pennsylvania, Philadelphia, USA (e-mail: [email protected])
STEPHANIE WEIRICH
Affiliation:
University of Pennsylvania, Philadelphia, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library’s test suite, and interfaces from Coq’s standard library. Our work shows that it is feasible to verify mature, widely used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and – since we found no bugs – attest to the superb quality of well-tested functional code.

Type
Research Article
Information
Journal of Functional Programming , Volume 31 , 2021 , e5
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Abel, A., Benke, M., Bove, A., Hughes, J., & Norell, U. (2005) Verifying Haskell programs using constructive type theory. In Haskell Workshop. ACM, pp. 62–73.CrossRefGoogle Scholar
Adams, S. (1992) Implementing sets efficiently in a functional language,. Research Report CSTR 92-10. University of Southampton.Google Scholar
Amani, S., Hixon, A., Chen, Z., Rizkallah, C., Chubb, P., O’Connor, L., Beeren, J., Nagashima, Y., Lim, J., Sewell, T., Tuong, J., Keller, G., Murray, T., Klein, G. & Heiser, G. (2016) Cogent: Verifying high-assurance file system implementations. In International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175–188.CrossRefGoogle Scholar
Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Savary Belanger, O., Sozeau, M. & Weaver, M. (2017) CertiCoq: A verified compiler for Coq. In CoqPL Workshop, CoqPL 2017.Google Scholar
Appel, A. W. (2011) Efficient Verified Red-Black Trees.Google Scholar
Appel, A. W., Beringer, L., Chlipala, A., Pierce, B. C., Shao, Z., Weirich, S. & Zdancewic, S. (2017) Position paper: The science of deep specification. Philos. Trans. R. Soc. A 375(2104).CrossRefGoogle ScholarPubMed
Besson, F. (2006) Fast reflexive arithmetic tactics: the linear case and beyond. In TYPES. Lecture Notes in Computer Science, vol. 4502. Springer, pp. 48–62.Google Scholar
Blanc, R., Kuncak, V., Kneuss, E. & Suter, P. (2013) An overview of the Leon verification system: verification by translation to recursive functions. In Proceedings of the 4th Workshop on Scala, SCALA@ECOOP 2013, Montpellier, France, July 2, 2013. ACM, pp. 1:1–1:10.CrossRefGoogle Scholar
Bove, A., Dybjer, P. & Norell, U. (2009) A brief overview of Agda – A functional language with dependent types. In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Berghofer, S., Nipkow, T., Urban, C. & Wenzel, M. (eds), Lecture Notes in Computer Science, vol. 5674. Springer.Google Scholar
Brady, E. (2017) Type-driven development with Idris. Manning.Google Scholar
Campbell, T. (2010) Bug in Data.Map. e-mail to the Haskell libraries mailing list.Google Scholar
Charguéraud, A. (2010a) The optimal fixed point combinator. In Proceedings of the First International Conference on Interactive Theorem Proving. ITP 2010. Berlin, Heidelberg: Springer-Verlag, pp. 195–210.CrossRefGoogle Scholar
Charguéraud, A. (2010b) Program verification through characteristic formulae. In ICFP. ACM, pp. 321–332.Google Scholar
Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M. F. & Zeldovich, N. (2015) Using Crash Hoare logic for certifying the FSCQ file system. SOSP. ACM, pp. 18–37.CrossRefGoogle Scholar
Chen, Z., O’Connor, L., Keller, G., Klein, G. & Heiser, G. (2017) The Cogent case for property-based testing. Workshop on Programming Languages and Operating Systems (PLOS). Shanghai, China: ACM, pp. 1–7.Google Scholar
Claessen, K. & Hughes, J. (2000) QuickCheck: A lightweight tool for random testing of Haskell programs. ICFP, ACM, pp. 268–279.Google Scholar
Coquand, T. (1989) Metamathematical investigations of a calculus of constructions. Tech. rept. RR-1088. INRIA.Google Scholar
Coquand, T. & Huet, G. P. (1988) The calculus of constructions. Information and computation, 76(2/3), 95–120.CrossRefGoogle Scholar
Derrin, P., Elphinstone, K., Klein, G., Cock, D. & Chakravarty, M. M. T. (2006) Running the manual: An approach to high-assurance microkernel development. In Haskell Symposium. ACM, pp. 60–71.Google Scholar
Dybjer, P., Haiyan, Q. & Takeyama, M. (2004) Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Inform. Softw. Technol. 46(15), 1011–1025.CrossRefGoogle Scholar
Filliâtre, J.-C. & Letouzey, P. (2004) Functors for proofs and programs. In Programming Languages and Systems, Schmidt, D. (ed). Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 370–384.CrossRefGoogle Scholar
Hallgren, T., Hook, J., Jones, M. P. & Kieburtz, R. B. (2004) An overview of the Programatica toolset. In HCSS.Google Scholar
Hirai, Y. & Yamamoto, K. (2011) Balancing weight-balanced trees. J. Function. Program. 21(3), 287–307.CrossRefGoogle Scholar
Joseph, A. M. (2014) Generalized arrows. Ph.D. thesis, EECS Department, University of California, Berkeley.Google Scholar
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H. & Winwood, S. (2009) seL4: Formal verification of an OS kernel. In ACM Symposium on Operating Systems Principles. Big Sky, MT, USA: ACM, pp. 207–220.CrossRefGoogle Scholar
Krauss, A. (2006) Partial recursive functions in higher-order logic. In IJCAR. LNCS, vol. 4130. Springer, pp. 589–603.CrossRefGoogle Scholar
Kröning, D., Rümmer, P. & Weissenbacher, G. (2009) A proposal for a theory of finite sets, lists, and maps for the SMT-Lib standard. In Informal Proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE, vol. 22.Google Scholar
Kumar, R., Myreen, M. O., Norrish, M. & Owens, S. (2014). CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014. New York, NY, USA: ACM, pp. 179–191.CrossRefGoogle Scholar
Letouzey, P. (2002) A new extraction for Coq. In TYPES. LNCS, vol. 2646. Springer, pp. 200–219.Google Scholar
Licata, D. (2012) 15–150 Lecture 21: Red-black trees. Lecture at the Oregon Programming Language Summer School.Google Scholar
The, Coq development team. (2016) The Coq proof assistant reference manual. LogiCal Project. Version 8.6.1.Google Scholar
McBride, C. T. (2014) How to keep your neighbours in order. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014. New York, NY, USA: ACM, pp. 297–309.CrossRefGoogle Scholar
Morrison, D. R. (1968) PATRICIA—Practical Algorithm To Retrieve Information Coded in Alphanumeric. J. ACM 15(4), 514–534.Google Scholar
Mullen, E., Pernsteiner, S., Wilcox, J. R., Tatlock, Z. & Grossman, D. (2018) Œuf: Minimizing the Coq extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018. New York, NY, USA: ACM, pp. 172–185.CrossRefGoogle Scholar
Myreen, M. O. & Owens, S. (2014) Proof-producing translation of higher-order logic into pure and stateful ML. Journal of Functional Programming, 24(May), 284–315.CrossRefGoogle Scholar
Nievergelt, J. & Reingold, E. M. (1972) Binary search trees of bounded balance. In STOC. ACM, pp. 137–142.CrossRefGoogle Scholar
Nipkow, T. (2016) Automatic functional correctness proofs for functional search trees. In Interactive Theorem Proving (ITP) 2016, Blanchette, J. & Merz, S. (eds), vol. 9807, pp. 307–322.Google Scholar
Nipkow, T. & Dirix, S. (2018) Weight-balanced trees. In Archive of Formal Proofs, http://isa-afp.org/entries/Weight_Balanced_Trees.html, Formal proof development.Google Scholar
Nipkow, T., Paulson, L. C. & Wenzel, M. (2002) Isabelle/HOL – A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer.CrossRefGoogle Scholar
O’Connor, L., Chen, Z., Rizkallah, C., Amani, S., Lim, J., Murray, T., Nagashima, Y., Sewell, T. & Klein, G. (2016) Refinement through restraint: Bringing down the cost of verification. International Conference on Functional Programming.CrossRefGoogle Scholar
Okasaki, C. (1999) Purely Functional Data Structures. Cambridge University Press.CrossRefGoogle Scholar
Okasaki, C. & Gill, A. (1998) Fast mergeable integer maps. In Workshop on ML, pp. 77–86.Google Scholar
Peyton Jones, S., Tolmach, A. & Hoare, T. (2001) Playing by the rules: rewriting as a practical optimisation technique in GHC. In Haskell Workshop.Google Scholar
Protzenko, J., Zinzindohoué, J.-K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-Béguelin, S., Delignat-Lavaud, A., Hriţcu, C., Bhargavan, K., Fournet, C. & Swamy, N. (2017) Verified low-level programming embedded in F*. Proc. ACM program. lang., 1(ICFP), 17:1–17:29.CrossRefGoogle Scholar
Ralston, R. (2009) ACL2-certified AVL trees. In Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2009. New York, NY, USA: ACM, pp. 71–74.CrossRefGoogle Scholar
Rizkallah, C., Lim, J., Nagashima, Y., Sewell, T., Chen, Z., O’Connor, L., Murray, T., Keller, G. & Klein, G. (2016) A framework for the automatic formal verification of refinement from Cogent to C. In International Conference on Interactive Theorem Proving.CrossRefGoogle Scholar
Spector-Zabusky, A., Breitner, J., Rizkallah, C. & Weirich, S. (2018) Total Haskell is reasonable Coq. In CPP. ACM, pp. 14–27.Google Scholar
Straka, M. (2010) The performance of the Haskell containers package. Proceedings of the Third ACM Haskell Symposium on Haskell, Haskell 2010. New York, NY, USA: ACM, pp. 13–24.Google Scholar
Swamy, N., Hriţcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoue, J.-K. & Zanella-Béguelin, S. (2016) Dependent types and multi-monadic effects in F*. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016. New York, NY, USA: ACM, pp. 256–270.CrossRefGoogle Scholar
Vazou, N., Rondon, P. M. & Jhala, R. (2013) Abstract refinement types. In Proceedings of the 22nd European Conference on Programming Languages and Systems, ESOP 2013. Berlin, Heidelberg: Springer-Verlag, pp. 209–228.CrossRefGoogle Scholar
Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis, D. & Peyton-Jones, S. (2014) Refinement types for Haskell. ICFP. ACM, pp. 269–282.Google Scholar
Vazou, N., Lampropoulos, L. & Polakow, J. (2017) A tale of two provers: Verifying monoidal string matching in Liquid Haskell and Coq. In Haskell Symposium. ACM, pp. 63–74.Google Scholar
Vazou, N., Tondwalkar, A., Choudhury, V., Scott, R. G., Newton, R. R., Wadler, P. & Jhala, R. (2018) Refinement reflection: Complete verification with SMT. PACMPL, 2(POPL), 53:1–53:31.Google Scholar
Vytiniotis, D., Peyton Jones, S., Claessen, K. & Rosén, D. (2013) HALO: Haskell to logic through denotational semantics. In POPL. ACM, pp. 431–442.CrossRefGoogle Scholar
Wiegley, J. (2017) coq-haskell: A Library for Formalizing Haskell Types and Functions in Coq. https://github.com/jwiegley/coq-haskell.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.