Niki Vazou
Philip Wadler
Abstract
We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function’s (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user to write equational proofs of programs just by writing other programs using pattern-matching and recursion to perform case-splitting and induction. Thus, via the propositions-as-types principle, we show that reflection permits the specification of arbitrary functional correctness properties. Finally, we introduce a proof-search algorithm called Proof by Logical Evaluation that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.
Supplemental Material
Available for Download
- N. Amin, K. R. M. L., and T. Rompf. 2014. Computing with an SMT Solver. In TAP.Google Scholar
- A. Appel. 2016. Verified Functional Algorithms. https://www.cs.princeton.edu/~appel/vfa/Perm.html .Google Scholar
- K. Asada, R. Sato, and N. Kobayashi. 2015. Verifying Relational Properties of Functional Programs by First-Order Refinement. In PEPM. Google ScholarDigital Library
- L. Augustsson. 1998. Cayenne - a Language with Dependent Types.. In ICFP.Google Scholar
- C. Barrett, A. Stump, and C. Tinelli. 2010. The SMT-LIB Standard: Version 2.0.Google Scholar
- J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Maffeis. 2008. Refinement Types for Secure Implementations. In CSF . Google ScholarDigital Library
- Y. Bertot and P. Castéran. 2004. Coq’Art: The Calculus of Inductive Constructions. Springer Verlag.Google Scholar
- R. S. Bird. 1989. Algebraic Identities for Program Calculation. In The Computer Journal. Google ScholarDigital Library
- J. C. Blanchette, S. Böhme, and L. C. Paulson. 2011. Extending Sledgehammer with SMT Solvers. In CADE. Google ScholarCross Ref
- Jr. Bocchino, L. Robert, V. S. Adve, S. V. Adve, and M. Snir. 2009. Parallel Programming Must Be Deterministic by Default. In HotPar .Google Scholar
- C. Casinghino, V. Sjöberg, and S. Weirich. 2014. Combining proofs and programs in a dependently typed language. In POPL. Google ScholarDigital Library
- J. Chen, R. Chugh, and N. Swamy. 2010. Type-preserving Compilation of End-to-end Verification of Security Enforcement. In PLDI. Google ScholarDigital Library
- K. Claessen and J. Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ICFP. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D.E. Long. 1992. Model checking and abstraction. In POPL. Google ScholarDigital Library
- J. Condit, M. Harren, Z. R. Anderson, D. Gay, and G. C. Necula. 2007. Dependent Types for Low-Level Programming. In ESOP . Google ScholarCross Ref
- R. L. Constable and S. F. Smith. 1987. Partial Objects In Constructive Type Theory. In LICS.Google Scholar
- P. Cousot and R. Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for the Static Analysis of Programs. In POPL . Google ScholarDigital Library
- E. W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. In Communications of the ACM .Google Scholar
- E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall.Google ScholarDigital Library
- R. A. Eisenberg and J. Stolarek. 2014. Promoting functions to type families in Haskell. In Haskell. Google ScholarDigital Library
- A. Farmer, N. Sculthorpe, and A. Gill. 2015. Reasoning with the HERMIT: Tool Support for Equational Reasoning on GHC Core Programs. In Haskell.Google Scholar
- G. Gentzen. 1935. Inverstigations into Logical Deduction. In American Philosophical Quarterly.Google Scholar
- W. A. Howard. 1980. The formulae-as-types notion of construction. In Essays on Combinatory Logic, Lambda Calculus and Formalism .Google Scholar
- G. Hutton. 1999. A tutorial on the universality and expressiveness of fold. J. Functional Programming (1999).Google Scholar
- A. M. Kent, D. Kempe, and S. Tobin-Hochstadt. 2016. Occurrence typing modulo theories. In PLDI. Google ScholarDigital Library
- K. W. Knowles and C. Flanagan. 2010. Hybrid type checking. In TOPLAS. Google ScholarDigital Library
- L. Kuper, A. Turon, N. R Krishnaswami, and R. R Newton. 2014. Freeze after writing: quasi-deterministic parallel programming with LVars. In POPL. Google ScholarDigital Library
- K. R. M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR.Google Scholar
- K. R. M. Leino and C. Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers. In CAV. Google ScholarCross Ref
- K. R. M. Leino and N. Polikarpova. 2016. Verified Calculations. In VSTTE.Google Scholar
- R. Leino. 2016. Dafny. (2016). https://github.com/Microsoft/dafny/blob/master/Test/dafny0/Fuel.dfy .Google Scholar
- S. Marlow, R. Newton, and S. Peyton-Jones. 2011. A Monad for Deterministic Parallelism. In Haskell. Google ScholarDigital Library
- S. C. Mu, H. S. Ko, and P. Jansson. 2009. Algebra of Programming in Agda: Dependent Types for Relational Program Derivation. In J. Funct. Program.Google Scholar
- G. C. Necula. 1997. Proof carrying code. In POPL. Google ScholarDigital Library
- C. G. Nelson. 1980. Techniques for Program Verification. Ph.D. Dissertation. Stanford University.Google Scholar
- T. Nipkow, L.C. Paulson, and M. Wenzel. 2002. Isabelle/HOL — A Proof Assistant for Higher-Order Logic.Google Scholar
- U. Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers.Google Scholar
- X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. 2004. Dynamic Typing with Dependent Types. In IFIP TCS. Google ScholarCross Ref
- J. C. Reynolds. 1972. Definitional interpreters for higher-order programming languages. In ACM National Conference. Google ScholarDigital Library
- P. Rondon, M. Kawaguchi, and R. Jhala. 2008. Liquid Types. In PLDI. Google ScholarDigital Library
- P. Rondon, M. Kawaguchi, and R. Jhala. 2010. Low-Level Liquid Types. In POPL. Google ScholarDigital Library
- J. Rushby, S. Owre, and N. Shankar. 1998. Subtypes for Specifications: Predicate Subtyping in PVS. TSE.Google Scholar
- E. L. Seidel, N. Vazou, and R. Jhala. 2015. Type Targeted Testing. In ESOP. Google ScholarDigital Library
- V. Sjöberg and S. Weirich. 2015. Programming Up to Congruence. In POPL. Google ScholarDigital Library
- W. Sonnex, S. Drossopoulou, and S. Eisenbach. 2012. Zeno: An Automated Prover for Properties of Recursive Data Structures. In TACAS.Google Scholar
- M. Sousa and I. Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In PLDI. Google ScholarDigital Library
- P. Suter, M. Dotta, and V. Kuncak. 2010. Decision Procedures for Algebraic Data Types with Abstractions. In POPL. Google ScholarDigital Library
- P. Suter, A. Sinan Köksal, and V. Kuncak. 2011. Satisfiability Modulo Recursive Programs. In SAS. Google ScholarCross Ref
- N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P. Y. Strub, M. Kohlweiss, J. K. Zinzindohoue, and S. Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In POPL.Google Scholar
- G. Tourlakis. 2008. Ackermann’s Function. (2008). http://www.cs.yorku.ca/~gt/papers/Ackermann-function.pdf .Google Scholar
- N. Vazou, L. Lampropoulos, and J. Polakow. 2017a. A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq. In Haskell.Google Scholar
- N. Vazou, P. Rondon, and R. Jhala. 2013. Abstract Refinement Types. In ESOP. Google ScholarDigital Library
- N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. Peyton-Jones. 2014. Refinement Types for Haskell. In ICFP. Google ScholarDigital Library
- N. Vazou, A. Tondwalkar, V. Choudhury, R. G. Scott, R. R. Newton, P. Wadler, and R. Jhala. 2017b. Extended Version: Refinement Reflection: Complete Verification with SMT. (2017). https://nikivazou.github.io/static/popl18/ extended-refinement-reflection.pdfGoogle Scholar
- P. Vekris, B. Cosman, and R. Jhala. 2016. Refinement types for TypeScript. In PLDI. Google ScholarDigital Library
- D. Vytiniotis, S. L. Peyton-Jones, K. Claessen, and D. Rosén. 2013. HALO: Haskell to Logic through Denotational Semantics. In POPL.Google ScholarDigital Library
- P. Wadler. 1987. A Critique of Abelson and Sussman or Why Calculating is Better Than Scheming. In SIGPLAN Not. Google ScholarDigital Library
- P. Wadler. 2015. Propositions As Types. In Communications of the ACM. Google ScholarDigital Library
- H. Xi and F. Pfenning. 1998. Eliminating Array Bound Checking Through Dependent Types. In PLDI. Google ScholarDigital Library
Index Terms
- Refinement reflection: complete verification with SMT
Recommendations
Programmed Strategies for Program Verification
Plover is an automated property-verifier for Haskell programs that has been under development for the past three years as a component of the Programatica project. In Programatica, predicate definitions and property assertions written in P-logic, a ...
Relatively complete refinement type system for verification of higher-order non-deterministic programs
This paper considers verification of non-deterministic higher-order functional programs. Our contribution is a novel type system in which the types are used to express and verify (conditional) safety, termination, non-safety, and non-termination ...
Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System
Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this ...
Comments