Generic Refinement Types
Authors: 
Nico Lehmann, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, Ranjit JhalaAuthors Info & Claims
Article No.: 49, Pages 1446 - 1474
Abstract
We present Generic Refinement Types: a way to write modular higher-order specifications that abstract invariants over function contracts, while preserving automatic SMT-decidable verification. We show how generic refinements let us write a variety of modular higher-order specifications, including specifications for Rust's traits which abstract over the concrete refinements that hold for different trait implementations. We formalize generic refinements in a core calculus and show how to synthesize the generic instantiations algorithmically at usage sites via a combination of syntactic unification and constraint solving. We give semantics to generic refinements via the intuition that they correspond to ghost parameters, and we formalize this intuition via a type-preserving translation into the polymorphic contract calculus to establish the soundness of generic refinements. Finally, we evaluate generic refinements by implementing them in Flux and using it for two case studies. First, we show how generic refinements let us write modular specifications for Rust's vector indexing API that lets us statically verify the bounds safety of a variety of vector-manipulating benchmarks from the literature. Second, we use generic refinements to refine Rust's Diesel ORM library to track the semantics of the database queries issued by client applications, and hence, statically enforce data-dependent access-control policies in several database-backed web applications.
References
[1]
Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 147, oct, 30 pages. https://doi.org/10.1145/3360573
[2]
Lennart Augustsson and Kent Petersson. 1994. Silly Type Families. https://web.cecs.pdx.edu/ sheard/papers/silly.pdf
[3]
Joao Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C Pierce. 2011. Polymorphic contracts. In Programming Languages and Systems: 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings 20. 18–37. https://doi.org/10.1007/978-3-642-19718-5_2
[4]
Yves Bertot and Pierre Castran. 2010. Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions (1st ed.). Springer Publishing Company, Incorporated. isbn:3642058809
[5]
Aurel Bílý, Jonas Hansen, Peter Müller, and Alexander J. Summers. 2022. Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. CoRR, abs/2210.09857 (2022), https://doi.org/10.48550/ARXIV.2210.09857 arXiv:2210.09857.
[6]
Benjamin Cosman and Ranjit Jhala. 2017. Local Refinement Typing. Proc. ACM Program. Lang., 1, ICFP (2017), Article 26, aug, 27 pages. https://doi.org/10.1145/3110270
[7]
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham. 378–388. isbn:978-3-319-21401-6 https://doi.org/10.1007/978-3-319-21401-6_26
[8]
Xavier Denis and Jacques-Henri Jourdan. 2023. Specifying and Verifying Higher-order Rust Iterators. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, Sriram Sankaranarayanan and Natasha Sharygina (Eds.) (Lecture Notes in Computer Science, Vol. 13994). Springer, 93–110. https://doi.org/10.1007/978-3-031-30820-8_9
[9]
Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering, Adrian Riesco and Min Zhang (Eds.). Springer International Publishing, Cham. 90–105. isbn:978-3-031-17244-1 https://doi.org/10.1007/978-3-031-17244-1_6
[10]
Dimitrios J. Economou, Neel Krishnaswami, and Jana Dunfield. 2023. Focusing on Refinement Typing. ACM Trans. Program. Lang. Syst., 45, 4 (2023), Article 22, dec, 62 pages. issn:0164-0925 https://doi.org/10.1145/3610408
[11]
Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Matthias Felleisen and Philippa Gardner (Eds.) (Lecture Notes in Computer Science, Vol. 7792). Springer, 125–128. https://doi.org/10.1007/978-3-642-37036-6_8
[12]
Lennard Gaher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. 2023. Refined Rust: Towards high-assurance verification of unsafe Rust programs. https://people.mpi-sws.org/~gaeher/slides/refinedrust_rw23.pdf
[13]
Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust Verification by Functional Translation. Proc. ACM Program. Lang., 6, ICFP (2022), Article 116, aug, 31 pages. https://doi.org/10.1145/3547647
[14]
Ranjit Jhala and Niki Vazou. 2021. Refinement Types: A Tutorial. Foundations and Trends® in Programming Languages, 6, 3–4 (2021), 159–317. issn:2325-1107 https://doi.org/10.1561/2500000032
[15]
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), 286–315. https://doi.org/10.1145/3586037
[16]
Nico Lehmann, Adam T. Geller, Niki Vazou, and Ranjit Jhala. 2023. Flux: Liquid Types for Rust. Proc. ACM Program. Lang., 7, PLDI (2023), Article 169, jun, 25 pages. https://doi.org/10.1145/3591283
[17]
Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, and Ranjit Jhala. 2021. STORM: Refinement Types for Secure Web Applications. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 441–459. isbn:978-1-939133-22-9 https://www.usenix.org/conference/osdi21/presentation/lehmann
[18]
Nico Lehmann, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, and Ranjit Jhala. 2025. Generic Refinement Types - Technical Appendix. https://github.com/flux-rs/popl25
[19]
K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). https://doi.org/10.1007/978-3-642-17511-4_20
[20]
Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. https://link.springer.com/book/10.1007/3-540-45949-9
[21]
Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Chalmers.
[22]
Benjamin C. Pierce and David N. Turner. 2000. Local type inference. ACM Trans. Program. Lang. Syst., 22, 1 (2000), jan, 1–44. issn:0164-0925 https://doi.org/10.1145/345099.345100
[23]
Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08). Association for Computing Machinery, New York, NY, USA. 159–169. isbn:9781595938602 https://doi.org/10.1145/1375581.1375602
[24]
Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. 2017. Polymorphic manifest contracts, revised and resolved. ACM Transactions on Programming Languages and Systems (TOPLAS), 39, 1 (2017), 1–36. https://doi.org/10.1145/2994594
[25]
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 266–278. https://doi.org/10.1145/2034773.2034811
[26]
The Diesel Core Team. 2024. Diesel: A Safe, Extensible ORM and Query Builder for Rust. https://diesel.rs
[27]
Niki Vazou, Alexander Bakst, and Ranjit Jhala. 2015. Bounded refinement types. In ICFP. https://doi.org/10.1145/2784731.2784745
[28]
Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Matthias Felleisen and Philippa Gardner (Eds.) (Lecture Notes in Computer Science, Vol. 7792). Springer, 209–228. https://doi.org/10.1007/978-3-642-37036-6_13
[29]
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 269–282. https://doi.org/10.1145/2628136.2628161
[30]
P. Wadler and S. Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’89). Association for Computing Machinery, New York, NY, USA. 60–76. isbn:0897912942 https://doi.org/10.1145/75277.75283
[31]
Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’03). Association for Computing Machinery, New York, NY, USA. 224–235. isbn:1581136285 https://doi.org/10.1145/604131.604150
[32]
Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. SIGPLAN Not., 33, 5 (1998), may, 249–257. issn:0362-1340 https://doi.org/10.1145/277652.277732
[33]
Christoph Zenger. 1997. Indexed types. Theor. Comput. Sci., 187, 1–2 (1997), nov, 147–165. issn:0304-3975 https://doi.org/10.1016/S0304-3975(97)00062-5
Recommendations
Flux: Liquid Types for Rust
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust ...
Refinement types for Haskell
PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program VerificationWe present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses Refinement types, a restricted form of dependent types where relationships between values are encoded by decorating types with logical ...
Mechanizing Refinement Types
Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2025
2363 pages
Copyright © 2025 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 January 2025
Published in PACMPL Volume 9, Issue POPL
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- NSF (National Science Foundation)
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 232Total Downloads
- Downloads (Last 12 months)232
- Downloads (Last 6 weeks)115
Reflects downloads up to 05 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in