Local Refinement Typing

TL;DR

The paper presents Fusion, an SMT-based local refinement type inference algorithm that efficiently verifies programs with polymorphic and higher-order functions, reducing false alarms and improving speed.

Contribution

Fusion introduces a concise, SMT-based approach for local refinement type inference that synthesizes the most precise types for program verification.

Findings

Fusion checks benchmarks with half as many templates as before

Fusion is 10-50x faster on theorem proving benchmarks

Fusion avoids false alarms by synthesizing precise types

Abstract

We introduce the Fusion algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. Fusion is concise as the programmer need only write signatures for (externally exported) top-level functions and places with cyclic (recursive) dependencies, after which Fusion can predictably synthesize the most precise refinement types for all intermediate terms (expressible in the decidable refinement logic), thereby checking the program without false alarms. We have implemented Fusion and evaluated it on the benchmarks from the LiquidHaskell suite totalling about 12KLOC. Fusion checks an existing safety benchmark suite using about half as many templates as previously required and nearly 2x faster. In a new set of theorem proving benchmarks Fusion is both 10 - 50x faster and, by synthesizing the most precise types, avoids false alarms to make verification possible.

Figures

Tables

Table 1. Table 1. Comparing Liquid inference (L)  (Rondon et al . , 2008 ) with Fusion (F). The number of modules (files) per benchmark is listed in parentheses. Code is the total number of lines of non-comment and non-whitespace lines of code and Spec is the total number of lines of specification ( i.e. top-level signatures), computed by sloccount . Qualifiers is the number of qualifiers needed for refinement inference; * means a false-positive, i.e. the benchmark could not be verified using the qualifiers provided as the intermediate terms have refinements not expressible using the given qualifiers. Time(s) is the total time in seconds needed to verify the benchmark (or to return a false positive, for times with a *).

Benchmark	Code	Spec	Qualifiers		Time(s)
			L	F	L	F
Data-Struct (8)	1818	408	5	4	126	94
Vec-Algos (11)	1252	279	4	4	78	61
Bytestring (11)	4811	726	18	11	233	136
Text (17)	3157	818	9	5	349	231
Arith (2)	270	46	*	0	*63	5
Fold (1)	70	29	0	0	78	1
Monoid (2)	85	16	0	0	3	1
Functor (3)	137	28	0	0	55	3
Applicative (2)	146	36	*	0	*70	2
Monad (3)	180	42	*	0	*35	3
Sat-Solver (1)	98	31	*	0	*48	1
Unification (1)	139	53	*	1	*240	3

Equations

$$\forall n.$$

$$\displaystyle\wedge\$$

$$\text{y}::\exists 0\le \text{t}.\{\nu :\text{Int}\mid \nu =\text{t}-1\}$$

$$\forall \text{y}.(\exists \text{t}.0\le \text{t}\wedge \text{y}=\text{t}-1)\Rightarrow \forall \nu .\nu =\text{y}+1\Rightarrow 0\le \nu$$

$$::\{\nu :\text{Int}\mid 0\le \nu \}$$

$$::\{\nu :\text{Int}\mid \nu =\text{x}\}$$

$$::\{\nu :\text{Int}\mid \nu =\text{t}-1\}$$

$$::\{\nu :\text{Int}\mid \kappa (\nu )\}$$

$$::\{\nu :\text{Int}\mid \nu =\text{y}+1\}$$

$$\displaystyle\forall{\texttt{x}}.\ {0\leq\texttt{x}}\ \Rightarrow\$$

$$\displaystyle\wedge\ \$$

$$\kappa (z)$$

$$::\{\nu :\text{Int}\mid \nu =\text{x}-1\}$$

$$::\{\nu :\text{Int}\mid \nu =\text{x}+1\}$$

$$::\text{List}\{\nu :\text{Int}\mid {\kappa }_x(\nu )\}$$

$$::\text{List}\{\nu :\text{Int}\mid {\kappa }_y(\nu )\}$$

$$::\{\nu :\text{Int}\mid {\kappa }_y(\nu )\}$$

$$::\{\nu :\text{Int}\mid \nu =\text{y}+1\}$$

$$\forall \text{x}.0\le \text{x}\Rightarrow$$

$$\displaystyle\quad{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\wedge}}\ \forall{\texttt{n}}.\ {\texttt{n}=\texttt{x}-1}\Rightarrow$$

$$\forall \text{p}.\text{p}=\text{x}+1\Rightarrow$$

$$\wedge \forall \nu .\nu =\text{n}\Rightarrow {\kappa }_x(\nu )$$

$$\wedge \forall \nu .\nu =\text{p}\Rightarrow {\kappa }_y(\nu )$$

$$\wedge \forall \nu .{\kappa }_x(\nu )\Rightarrow {\kappa }_y(\nu )$$

$$\wedge \forall \text{y}.{\kappa }_y(\text{y})\Rightarrow$$

$$\forall \nu .\nu =\text{y}+1\Rightarrow 0\le \nu$$

$${\kappa }_x(z)$$

$$\exists \text{n}.\text{n}=\text{x}-1\wedge$$

$$\exists \text{p}.\text{p}=\text{x}+1\wedge$$

$$\exists \nu .\nu =n\wedge \nu =z$$

$${\kappa }_y(z)$$

$$\exists \text{n}.\text{n}=\text{x}-1\wedge$$

$$\exists \text{p}.\text{p}=\text{x}+1\wedge$$

$$\vee \exists \nu .\nu =\text{p}\wedge \nu =z$$

$$\vee \exists \nu .\nu =\text{n}\wedge \nu =z$$

$$::\{a:\text{Int}\mid {\kappa }_a(a)\}$$

$$::\{b:\text{Int}\mid {\kappa }_b(b)\}$$

$$::\{a:\text{Int}\mid {\kappa }_a(a)\}$$

$$\forall a.{\kappa }_a(a)$$

$$\wedge$$

$${\kappa }_a(z)$$

$${\kappa }_b(z)$$

$${\kappa }_c(z)$$

$$::\text{List}\{a\mid {\kappa }_a(a)\}$$

$$::\text{List}\{b\mid {\kappa }_b(b)\}$$

Full text

Refinement Types, Program Logics, SMT, Verification

††journal: PACMPL††conference: ACM SIGPLAN Conference on Programming Languages; January 01–03, 2017; New York, NY, USA††journalyear: 2017††isbn: 978-x-xxxx-xxxx-x/YY/MM††doi: 10.1145/3110270††copyright: rightsretained

1. Introduction

Refinement types are a generalization of Floyd-Hoare logics to the higher-order setting. Assertions are generalized to types by constraining basic types so that their inhabitants satisfy predicates drawn from SMT-decidable refinement logics. Assertion checking can then be generalized to a form of subtyping, where subtyping for basic types reduces to checking implications between their refinement predicates (Constable, 1986; Rushby et al., 1998). Thus, thanks to the SMT revolution (Barrett et al., 2016), refinement types have emerged as a modular and programmer-extensible means of expressing and verifying properties of polymorphic, higher order programs in languages like ML (Xi and Pfenning, 1998; Dunfield, 2007; Rondon et al., 2008), Haskell (Vazou et al., 2014b), Racket (Kent et al., 2016), $F^{\sharp}$ (Bengtson et al., 2008), and TypeScript (Vekris et al., 2016).

The Problem  Unfortunately, the expressiveness and extensibility offered by predicate refinements comes at a price. Existing refinement type systems are either not concise, i.e. require many type annotations (not just for top-level functions), or not complete, i.e. programs fail to type check because the checker cannot synthesize suitable types for intermediate terms, or not terminating, i.e. the checker can diverge while trying to synthesize suitable types for intermediate terms in an iterative counterexample-guided manner. We show that the presence of logical predicates relating multiple program variables renders classical approaches like unification or set-constraint based subtyping – even when used in a bidirectional (Pierce and Turner, 1998) or local fashion (Odersky et al., 2001) – not up to the task of inference. The problem is especially acute for programs that make ubiquitous use of polymorphic datatypes and higher-order combinators. Consequently, to use refinement types, the programmer must accept one of several distasteful choices: litter her code with type annotations (everywhere), or eschew polymorphic combinators (§ 2).

Fusion: Local Refinement Typing  In this paper, we introduce the Fusion algorithm that permits local refinement type inference. Fusion is concise as the programmer need only write signatures for (externally exported) top-level functions, and places with cyclic dependencies on refinements, either explicit (e.g. recursive functions) or implicit (e.g. calls to inductive library functions like fold). Fusion then synthesizes the most precise refinement types for all intermediate terms that are expressible in the refinement logic, and hence checks the specified signatures. Finally, Fusion ensures that verification remains decidable by using the framework of Liquid Typing (Rondon et al., 2008) to synthesize refinements from user-defined templates (“qualifiers”) in the presence of cyclic dependencies. Fusion reconciles concision, precision and decidability with three contributions.

1. (1)

From Programs to NNF Horn Constraints Our first insight is that we can phrase the problem of refinement type checking as that of checking the satisfiability of (nested) Horn Clause Constraints in Negation Normal Form (NNF). The NNF constraints are implications between refinement variables denoting the unknown, to-be-synthesized refinements; a satisfying assignment for these constraints yields refinement types for all intermediate terms, that satisfy the subtyping obligations that must hold for the program to meet its specification. Crucially, our novel NNF constraint formulation retains the scoping structure of bindings that makes precise constraint solving practical (§ 4). 2. (2)

Solving Constraints via Elimination Our second insight is that we can find a satisfying assignment for the NNF constraint, by systematically computing the most precise assignment for each refinement variable, and using it to eliminate the variable from the constraints. Unfortunately, we find that a direct application of the elimination algorithm, inspired by the classical notion of “unfolding” from the Logic Programming literature (Burstall and Darlington, 1977; Tamaki and Sato, 1984), leads to an exponential blowup even for simple programs that arise in practice. We show that such a blowup cannot be avoided in general as the problem of refinement type checking is ExpTime-hard. Fortunately, we show how to exploit the scoping structure present in NNF constraints to get compact solutions for real-world programs (§ 5). 3. (3)

Refinement Typing: Faster and without False Alarms We have implemented Fusion and evaluated its effectiveness on all the benchmarks from the LiquidHaskell suite (Vazou et al., 2014b). We show that in existing safety benchmarks where qualifiers were supplied or extracted from top-level type signatures, Fusion is able to synthesize the types about $2\times$ faster and requires only about half the qualifiers (needed e.g. to synthesize types for non-top-level recursive functions). Further, in a new set of theorem proving benchmarks which make heavy use of polymorphic higher-order functions and data types, global template-based inference of LiquidHaskell is both prohibitively slow and unpredictable, failing with false alarms. In contrast, Fusion is more than $10\times$ faster and, by synthesizing the most precise types, makes verification possible (§ 6).

2. Overview

We start with a high-level overview illustrating how refinement types can be used to verify programs, the problems that refinements pose for local inference, and our techniques for addressing them. We have picked obviously contrived examples that distill the problem down to its essence: for real-world programs we refer the reader to (Vazou et al., 2014a; Swamy et al., 2011).

Refinement Types  We can precisely describe subsets of values corresponding to a type by composing basic types with logical predicates that are satisfied by values inhabiting the type. For example, Nat describes the subset of Int comprising (non-negative) natural numbers:

⬇

type Nat = {v:Int | 0 <= v}

Verification Conditions  A refinement type checker can use the above signature to check:

⬇

abs :: Int -> Nat

abs n | 0 <= n = n

    | otherwise = 0 - n

by generating a verification condition (VC) (Nelson, 1981):

[TABLE]

whose validity can be checked by an SMT solver (Nelson, 1981; Barrett et al., 2016) to ensure that the program meets the given specification.

2.1. The Problem

For simple, first-order programs like abs, VC generation is analogous to the classical Floyd-Hoare approach used e.g. by EscJava (Flanagan et al., 2002). Namely, we have constraints assuming the path conditions (and pre-conditions), and asserting the post-conditions. Next, we illustrate how VC generation and checking is problematic in the presence of local variables, collections, and polymorphic, higher order functions. We do so with a series of small but idiomatic examples comprising “straight-line” code (no explicit looping or recursion), decorated with top-level specifications as required for local type inference. We show how the presence of the above features necessitates the synthesis of intermediate refinement types, which is beyond the scope of existing approaches.

Library Functions  Our examples use a library of functions with types as shown in Fig. 1.

Example 1: Local Variables  In ex1 in Figure 2, we illustrate the problem posed by local binders that lack (refinement) type signatures. Here, we need to check that inc y is a Nat i.e. non-negative, assuming the input x is. To do so, we must synthesize a sufficiently strong type for the local binder y which says that its value is an almost-Nat, i.e. that y has the type ${{\{{\texttt{y}}\!:\!{\texttt{{Int}}}\mid 0\leq\texttt{y}+1\}}}$.

Example 2: Collections  In ex2 in Figure 2 we show how the idiom of creating intermediate collections of values complicates refinement type checking. Here, we use a Nat to create a list ys whose last element is extracted and incremented, yielding a Nat. The challenge is to infer that the intermediate collection ys is a list of almost-Nats.

Example 3: Higher Order Functions  Function ex3 shows the idiom of composing two functions with the (.) operator whose type is in Figure 1. To verify the type specification for ex3 we need to synthesize suitable instantiations for the type variables a, b and c. Unlike with classical types, unification is insufficient, as while a and c may be instantiated to Nat, we need to infer that b must be instantiated with almost-Nat.

Example 4: Iteration  Finally ex4 shows how the higher-order map and (.) are used to idiomatically refactor transformations of collections in a “wholemeal” style (Hinze, 2009). This straight-line function (treating map as a library function, abstracted by its type signature) vexes existing refinement type systems (Knowles and Flanagan, 2010; Swamy et al., 2011) that cannot infer that map dec (resp. map inc) transforms a Nat list (resp. almost-Nat list) into an almost-Nat list (resp. Nat list).

2.2. Existing Approaches

Existing tools use one of three approaches, each of which is stymied by programs like the above.

1. Existentials  First, (Knowles and Flanagan, 2009; Kent et al., 2016) shows how to use existentials to hide the types of local binders. In ex1, this yields

[TABLE]

As inc y has the type ${\{\nu\mid\nu=\texttt{y}+1\}}$ we get the VC:

[TABLE]

which is proved valid by an SMT solver. Sage (Knowles and Flanagan, 2010), F* (Swamy et al., 2011) and Racket (Kent et al., 2016) use this method to check ex1. However, it is not known how to scale this method beyond local variable hiding, i.e. to account for collections, lambdas, higher-order functions etc.. Consequently, the above systems fail to check ex2, ex3 and ex4.

2. Counterexample-Guided Refinement  Second, as in Mochi (Unno et al., 2013) we can use counterexample-guided abstraction-refinement (CEGAR) to iteratively compute stronger refinements until the property is verified. This approach has two drawbacks. First, it is non-modular in that it requires closed programs – e.g. the source of library functions like map and (.) – in order to get counterexamples. Second, more importantly, it is limited to logical fragments like linear arithmetic where Craig Interpolation based “predicate discovery” is predictable, and is notoriously prone to divergence otherwise (Jhala and McMillan, 2006). Consequently, the method has only been applied to small but tricky programs comprising tens of lines, but not scaled to large real-world libraries spanning thousands of lines, and which typically require refinements over uninterpreted function symbols or modular arithmetic (Vazou et al., 2014a).

3. Abstract Interpretation  Finally, the framework of Liquid Typing (Rondon et al., 2008) shows how to synthesize suitable refinement types via abstract interpretation. The key idea is to:

1. (1)

Represent types as templates that use $\kappa$ variables to represent unknown refinements. 2. (2)

Generate subtyping constraints over the templates, that reduce to implications between the $\kappa$ variables, 3. (3)

Solve the implications over an abstract domain, e.g. the lattice of formulas generated by conjunctions of user-supplied atomic predicates, to find an assignment for the $\kappa$-variables that satisfies the constraints.

Unfortunately, this approach also has several limitations. First, the user must supply atomic predicates (or more generally, a suitable abstract domain) which should be superfluous in “straight line” code as in ex1, ex2, ex3, and ex4. Unfortunately, without the atomic predicate hints, Liquid Typing fails to check any of the above examples. Specifically, unless the user provides the qualifier or template ${0\leq\texttt{v}+1}$ (which does not appear anywhere in the code or specifications), the system cannot synthesise the almost-Nat types for the various intermediate terms in the above examples. Consequently LiquidHaskell (which implements Liquid Typing) rejects safe (and checkable) programs, leaving the user with the unpleasant task of debugging false alarms. Second, in predicate abstraction, the so-called abstraction operator “$\alpha$” makes many expensive SMT queries, which can slow down verification, or render it impossible when the specifications, and hence predicates, are complicated (§ 6).

2.3. Our Solution: Refinement Fusion

Next, we describe our Fusion algorithm for local refinement typing and show how it allows us to automatically, predictably and efficiently check refinement types in the presence of variable hiding, collections, lambdas and polymorphic, higher order functions. The key insight is two-fold. First, we present a novel reduction from type inference to the checking the satisfaction of a system of NNF Horn Constraints (over refinement variables) that preserve the scoping structure of bindings in the original source program. Second, we show how to check satisfaction of the NNF constraints by exploiting the scoping structure to compute the strongest possible solutions for the refinement variables. The above steps yield a method that is concise, i.e. requires no intermediate signatures, and complete, i.e. is guaranteed to check a program whenever suitable signatures exist, instead of failing with false alarms when suitable qualifiers are not provided. Finally, the method terminates, as the acyclic variables can be eliminated (by replacing them with their most precise solution), after which any remaining cyclic variables can be solved via abstract interpretation (Rondon et al., 2008).

Example 1: Local Variables

First, let us see how Fusion synthesizes types for local binders that lack (refinement) type signatures.

1. Templates  Fusion starts by generating templates for terms whose type must be synthesized. From the input type of ex1 (Fig 2), the fact that t is bound to x, and the output type of dec we have:

[TABLE]

2. Constraints  Next, Fusion generates constraints between the various refinements. At each application, the parameter must be a subtype of the input type; dually, in each function definition, the body must be a subtype of the output type, and at each let-bind the body must be a subtype of the whole let-in expression. For base types, subtyping is exactly implication between the refinement formulas (Constable, 1986; Rushby et al., 1998). For ex1 we get two constraints. The first relates the body of the let-in with its template; the second the body of ex1 with the specified output:

[TABLE]

Fusion ensures that the constraints preserve the scoping structure of bindings. Each subtyping (i.e. implication) happens under a context where the program variables in scope are bound and required to satisfy the refinements from their previously computed templates. Further, shared binders are explicit in the NNF constraint. For example, in the NNF constraint above, the shared binder x in the source program is also shared across the two implications 1 and 2. This sharing crucially allows Fusion to compute the most precise solution.

3. Solution  To solve the constraints we need to find a well-formed assignment mapping each $\kappa$-variable to a predicate over variables in scope wherever the $\kappa$-variable appears, such that the formula obtained by replacing the $\kappa$ with its assignment is valid. If no such interpretation exists, then the constraints are unsatisfiable and the program is ill-typed.

Fusion computes an interpretation called the strongest refinements using a method inspired by the classical notion of “unfolding” from the Logic Programming literature (Burstall and Darlington, 1977; Tamaki and Sato, 1984). In essence, if we have implications of the form: $P_{i}\Rightarrow\kappa({\nu})$ then we can assign $\kappa$ to the disjunction $\kappa({\overline{x}})\doteq\vee_{i}P_{i}$ after taking care to existentially quantify variables. In our example, $\kappa$ is a unary refinement predicate, and so we use (1) to obtain the assignment

[TABLE]

which simplifies to ${0\leq z+1}$. The computed assignment above is simply the (existentially quantified) hypotheses arising in the conjunction where $\kappa({\cdot})$ is the goal. The “simplification” done above and in the sequel is purely for exposition: to compute it we would have to resort to quantifier elimination procedures which are prohibitively expensive in practice, and hence avoided by Fusion.

It is easy to check that the above assignment renders the constraint valid (post-substitution). In particular, the solution (3) precisely captures the almost-Nat property which allows an SMT solver to prove (2) valid. While the substituted VC contains existential quantifiers, the SMT solver can handle the resulting validity query easily as the quantifiers appear negatively, i.e. in the antecedents of the implication. Consequently, they can be removed by a simple variable renaming (“skolemization”) as the VC $(\exists x.P(x))\Rightarrow Q$ is equivalent to the VC $P(z)\Rightarrow Q$, where z is a fresh variable name.

Thus, for local variables, Fusion synthesizes the same intermediate types as the existentials-based method of (Knowles and Flanagan, 2009; Kent et al., 2016), and, unlike Liquid Types, is able to verify ex1 without requiring any predicate templates. However, as we see next, Fusion generalizes the existentials based approach to handle collections, lambdas, and polymorphic, higher order functions.

Example 2: Collections

Next, let us see how Fusion precisely synthesizes types for intermediate collections without requiring user-defined qualifiers or annotations.

1. Templates  From the output types of inc and dec we get

[TABLE]

2. Constraints  We get four implication constraints from ex2.

[TABLE]

As n is passed into “cons” to get xs, we get that ${\{\nu\mid\nu=\texttt{n}\}}$ must be a subtype of ${\{\nu\mid\kappa_{x}({\nu})\}}$, yielding (4). Similarly, as p is “cons”-ed to xs to get ys, we get that ${\{\nu\mid\nu=\texttt{p}\}}$ and ${\{\nu\mid\kappa_{x}({\nu})\}}$ must be subtypes of ${\{\nu\mid\kappa_{y}({\nu})\}}$ yielding (5) and (6) respectively. Finally, the type of the return value y+1 must be a subtype of Nat yielding (7). Each implication appears under a context in which the variables in scope are bound to satisfy their template’s refinement.

3. Solution  Again, we compute the strongest refinements as the (existentially quantified) disjunctions of the hypotheses under which each $\kappa$ appears. Thus, implication (4) yields:

[TABLE]

which is also $0\leq z+1$. Substituting the strongest refinements into (7) yields a valid formula, verifying ex2.

Example 3: Composition

Next, we describe how Fusion synthesizes precise types for inner lambda-terms like those bound to fn and fp, and simultaneously determines how the polymorphic type variables for the (.) combinator can be instantiated in order to verify ex3

1. Templates  Fusion scales up to polymorphic higher-order operators like “compose” (.) by using the same approach as for collections: create $\kappa$-variables for the unknown instantiated refinements, and then find the strongest solution. In ex3, this process works by respectively instantiating the a, b and c in the signature for (.) (Fig 1) with fresh templates ${\{\nu\mid\kappa_{a}({\nu})\}}$, ${\{\nu\mid\kappa_{b}({\nu})\}}$, and ${\{\nu\mid\kappa_{c}({\nu})\}}$ respectively. Consequently, the arguments and output to . at this instance get the templates:

[TABLE]

2. Constraints  Next, the bodies of fn and fp must be subtypes of the above templates. By decomposing function subtyping into input- and output- subtyping, we get the following implications. We omit the trivial constraints on the input types; the above correspond to checking the output types in an environment assuming the stronger (super-) input type:

[TABLE]

3. Solution  Finally Fusion computes the strongest refinements by assigning $\kappa_{a}$ to its single hypothesis:

[TABLE]

Example 4: Iteration

Finally, Fusion uses types to scale up to higher-order iterators over collections. As in ex3 we generate fresh templates for fn (8) and fp (9). When applied to map the above return as output the templates:

[TABLE]

Consequently, the subtyping constraints for ex4 are the same as for ex3 but lifted to lists. Co-variant list subtyping reduces those into the exact same set of implications as ex3. Thus, Fusion computes the same strongest refinements as in ex3 and hence, verifies ex4.

2.4. Avoiding Exponential Blowup

The reader may be concerned that substituting the strongest solution may cause the formulas to expand, leading to an exponential blowup. Recall that, in our examples, we “simplified” the formulas before substituting to keep the exposition short. In general this is not possible as it requires expensive quantifier elimination. We show that the concern is justified in theory, and that a direct substitution strategy leads to a blowup even in practice. Fortunately, we show that a simple optimization that uses the scoping structure of bindings that we have carefully preserved in the NNF constraints allows us to avoid blowups in practice.

Local Refinement Typing is ExpTime-Hard  The bad news is that local refinement typing in general, and thus, constraint solving in particular are both ExpTime-hard. This result follows from the result that reachability (i.e. safety) of non-recursive first order boolean programs is ExpTime-complete (Godefroid and Yannakakis, 2013). We can encode the reachability problem directly as checking a given refinement type signature over programs using just boolean valued data, and so local refinement typing is ExpTime-hard. Thus, deciding constraint satisfaction is also ExpTime-hard, which means that we cannot avoid exponential blowups in general. Propositional validity queries are in Np so ExpTime-hardness means we must make an exponential number of queries, or a polynomial number of exponential size queries.

Let-chains cause exponential blowup  Indeed, the direct “unfolding” based approach (Burstall and Darlington, 1977; Tamaki and Sato, 1984) that we have seen so far blows up due to a simple and ubiquitous pattern: sequences of let-binders. Consider the constraint generated by the program:

⬇

exp :: Nat -> Nat

exp $\texttt{x}_{0}$ = let $\texttt{x}_{1}$ = id $\texttt{x}_{0}$

           $\vdots$

           $\texttt{x}_{n}$ = id $\texttt{x}_{n-1}$

       **in** $\texttt{x}_{n}$

The $i^{th}$ invocation of id :: a -> a creates a fresh $\kappa_{i}$, which is then used as the template for $\texttt{x}_{i}$. Consequently, we get the NNF constraint:

[TABLE]

Since each $\kappa_{i}$ has in its hypotheses, all of $\kappa_{1}\ldots\kappa_{i-1}$, the strongest solution for $\kappa_{i}$ ends up with $2^{i}$ copies of ${0\leq x_{0}}$! While this example is contrived, it represents an idiomatic pattern: long sequences of let-binders (e.g. introduced by ANF-conversion) with polymorphic instantiation. Due to the ubiquity of the pattern, a direct unfolding based computation of the strongest refinement fails for all but the simplest programs.

Sharing makes Solutions Compact  This story has a happy ending. Fortunately, our constraints preserve the scoping structure of binders. Thus, the exponentially duplicated $0\leq x_{0}$ is “in scope” everywhere each $\kappa_{i}$ appears. Consequently, we can omit it entirely from the strongest solutions, collapsing each to the compact solution (15), $\kappa_{i}({z})\doteq z=x_{i-1}$. In § 4 we formalize our algorithm for generating such nested constraints, and in § 5 we show how to use the above insight to derive an optimized solving algorithm, which yields compact, shared solutions and hence, dramatically improves refinement type checking in practice § 6.

The Importance of Preserving Scope  Note that the sharing observation and optimization seem obvious at this juncture, precisely because of our novel NNF formulation which carefully preserves the scoping structure of binders. Previous approaches for constraint based refinement synthesis (Knowles and Flanagan, 2007; Rondon et al., 2008; Hashimoto and Unno, 2015; Polikarpova et al., 2016) yield constraints that discard the scoping structure, yielding the flat (i.e. non-nested) constraints

[TABLE]

in which the sharing is not explicit as the shared variables are alpha-renamed. Absent sharing, unfolding yields a solution for each $\kappa_{i}$ that is exponential in $i$ without any syntactic duplication of a common conjunct, rendering the computation of precise solutions infeasible.

2.5. Relatively Complete Local Refinement Typing

By fusing together the constraints appearing as hypotheses for each refinement variable $\kappa$, our approach synthesizes the most precise refinements expressible in the decidable refinement logic (Lemma 5.6), and hence, makes local refinement typing relatively complete. That is, (assuming no recursion) if there exist type ascriptions for intermediate binders and terms that allow a program to typecheck, then Fusion is guaranteed to find them. The above examples do in fact typecheck with existing systems but only if the user annotated local variables with their signatures. For example, (Swamy et al., 2011) can check ex2 (Figure 2) if the programmer annotates the type of the local xs as an almost Nat. Unfortunately, such superfluous annotations impose significant overhead in code size as well as effort: the user must painstakingly debug false alarms to find where information was lost due to incompleteness. In contrast, our completeness guarantee means that once the user has annotated top-level and recursive binders, Fusion will not return false alarms due to missing templates, i.e. will typecheck the program if and only if it can be, which crucially makes verification concise, precise and decidable, enabling the results in § 6.

Precise Refinements vs. Pre- and Post-Conditions  As discussed in § 7, our notion of most precise refinements can be viewed as the analog of the method of strongest postconditions from Floyd-Hoare style program logics. F* introduces the notion of Dijkstra Monads (Swamy et al., 2013) as a way to generalize the dual notion of weakest preconditions (WP) to the higher-order setting. Hence, F* can use the notion of Dijkstra Monads to verify the following variant of ex3 that uses Floyd-Hoare style specification instead of refinement types:

⬇

let inc x = x + 1

let dec x = x - 1

let compose f g x = f (g x)

let ex3 : i:int -> Pure int

(**requires** (0 <= i)) (**ensures** (fun j -> 0 <= j))

= compose inc dec

However, this approach has a key limitation relative to Fusion in that it requires an implementation or logically equivalent strong specification of the compose operator (.), instead of the weaker polymorphic type signature required by Fusion. The WP machinery crucially relies upon the strong specification to makes the chaining of functions explicit. When the chaining is obscured, e.g. by the use of map in ex4, the WP method is insufficient, and so F* fails to verify ex4. In contrast, Fusion uses only the implicit subtyping dependencies between refinement types. Hence, the same compositional, type-directed machinery that checks ex3 carries over to successfully verify ex4.

3. Programs

We start by formalizing the syntax and operational semantics of a core source language $\lambda^{R}$ (Knowles and Flanagan, 2010; Vazou et al., 2014b).

3.1. Syntax

Terms  Figure 4 summarizes the syntax of the terms of $\lambda^{R}$. The values of $\lambda^{R}$ comprise primitive constants $\mathsf{c}$ and functions $\lambda{x}\!:\!{\tau}.{e}$. The terms of $\lambda^{R}$ include values and additionally, variables $x$, $y$, $z$ …, let-binders $\texttt{let}\;x=e\;\texttt{in}\;e$, applications ${e}\;{x}$ (in ANF, to simplify the application rule (Rondon et al., 2008)). Polymorphism is accounted for via type abstraction $\Lambda{\alpha}.{e}$ and instantiation $[e]\;{\tau}$. We assume that the source program has been annotated with unrefined types at $\lambda$-abstractions and type abstraction and instantiations, either by the programmer or via classical (unrefined) type inference.

Types  The types of $\lambda^{R}$ include unrefined types, written $\tau$, and refined types, written $t$. The unrefined types include basic types like Int, Bool, type variables $\alpha$, functions ${{x}\!:\!{\tau}}\rightarrow{\tau^{\prime}}$ where the input is bound to the name $x$, and type schemes $\forall{\alpha}.{\tau}$. We refine basic types with refinement predicates $r$ to get refined types. The formulas $r$ are drawn from a decidable refinement logic, e.g. QF_UFLIA: the quantifier free theory of linear arithmetic and uninterpreted functions.

Notation  We write $\{\nu\mid r\}$ when the base $b$ is clear from the context. We write $b$ to abbreviate $\{{\nu}\!:\!{b}\mid\mathit{true}\}$, and write ${t\rightarrow t^{\prime}}$ to abbreviate ${{x}\!:\!{t}}\rightarrow{t^{\prime}}$ if $x$ does not appear in $t^{\prime}$.

Typing Constants  We assume that each constant $\mathsf{c}$ is equipped with a type $\mathsf{prim}(\mathsf{c})$ that characterizes its semantics (Knowles and Flanagan, 2010; Vazou et al., 2014b). For example, literals are assigned their corresponding singleton type and operators have types representing their pre- and post-conditions:

[TABLE]

3.2. Semantics

$\lambda^{R}$ has a standard small-step, contextual call-by-value semantics; we write ${e}\hookrightarrow{e^{\prime}}$ to denote that term $e$ steps to $e^{\prime}$. We write ${e}\hookrightarrow^{j}{e^{\prime}}$ if there exists $e_{1},\ldots,e_{j}$ such that $e\equiv e_{1}$, $e^{\prime}\equiv e_{j}$, and for all $1\leq i<j$, we have ${e_{i}}\hookrightarrow{e_{i+1}}$. We write ${e}\hookrightarrow^{*}{e^{\prime}}$ if for some (finite) $j$ we have ${e}\hookrightarrow^{j}{e^{\prime}}$.

Constants  We assume that when values are applied to a primitive constant, the expression is reduced to the output of the primitive constant operation in a single step. For example, consider +, the primitive Int addition operator. We assume that $\llbracket{\texttt{+}}\rrbracket(n)$ equals $\texttt{+}_{n}$ where for all $m$, $\llbracket{\texttt{+}_{n}}\rrbracket(m)$ equals the integer sum of $n$ and $m$.

Safety  We say a term $e$ is stuck if there does not exist any $e^{\prime}$ such that ${e}\hookrightarrow{e^{\prime}}$. We say that a term $e$ is safe, if whenever ${e}\hookrightarrow^{*}{e^{\prime}}$ then either $e^{\prime}$ is a value or $e^{\prime}$ is not stuck. We write $\mathsf{safe}(e)$ to denote that $e$ is safe. Informally, we assume that the primitive operations (e.g. division) get stuck on values that do not satisfy their input refinements (e.g. when the divisor is 0). Thus, $e$ is safe when every (primitive) operation is invoked with values on which it is defined (e.g. there are no divisions by 0.)

4. Constraints

Local refinement typing proceeds in two steps. First, we use $\lambda^{R}$ terms to generate a system of constraints (§ 4.1) whose satisfiability (§ 4.2) implies that the term is safe (§ 4.4). Second, we solve the constraints to find a satisfying assignment (§ 5).

4.1. Syntax

Refinement Variables  Figure 5 describes the syntax of constraints. A refinement variable represents an unknown $n$-ary relation, i.e. is an unknown refinement over the free variables $z_{1},\ldots,z_{n}$ (abbreviated to $\overline{z}$). We refer to $\overline{{z}\!:\!{\tau}}$ as the parameters of a variable $\kappa$, written $\mathsf{params}(\kappa)$, and say that $n$ is the arity of $\kappa$. We write $K$ for the set of all refinement variables.

Predicates  A predicate is a refinement $r$ from a decidable logic, or a refinement variable application $\kappa({x_{1},\ldots,x_{n}})$, or a conjunction of two sub-predicates. We assume each $\kappa$ is applied to the same number of variables as its arity.

Constraints  A constraint is a “tree” where each “leaf” is a goal and each “internal” node either (1) universally quantifies some variable $x$ of a basic type $b$, subjecting it to satisfy a hypothesis $p$, or (2) conjoins two sub-constraints.

NNF Horn Clauses  Our constraints are Horn Clauses in Negation Normal Form (Bjørner et al., 2015). NNF constraints are a generalization of the “flat” Constraint Horn Clause (CHC) formulation used in Liquid Typing (Rondon et al., 2008). Intuitively, each root-to-leaf path in the tree is a CHC that requires that the leaf’s goal be implied by the internal nodes’ hypotheses. The nesting structure of NNF permits the scope-based optimization that makes Fusion practical (§ 5.1).

4.2. Semantics

We describe the semantics of constraints by formalizing the notion of constraint satisfaction. Intuitively, a constraint is satisfiable if there is an interpretation or assignment of the $\kappa$-variables to concrete refinements $r$ such that the resulting logical formula is well-formed and valid.

Well-formedness  An environment $\mathrm{\Gamma}$ is a set of type bindings ${x}\!:\!{\tau}$. We write $\mathrm{\Gamma}\vdash c$ to denote that $c$ is well-formed under environment $\mathrm{\Gamma}$. Figure 5 summarizes the rules for establishing well-formedness. We write $\mathrm{\Gamma}\vdash r:\texttt{Bool}$ if $r$ can be typed as a Bool using the standard (non-refined) rules, and use it to check individual refinements (W-Ref). A conjunction of sub-constraints is well-formed if each conjunct is well-formed (W-And). Finally, each implication is well formed if the hypothesis is well-formed and the consequent is well-formed under the extended environment (W-Imp). (Note that a constraint containing a $\kappa$-application is not well-formed.)

Assignments  An assignment $\sigma$ is a map from the set of refinement variables $K$ to the set of refinements $R$. An assignment is partial if its range is predicates (containing $\kappa$-variables, not just refinements). The function $\sigma(\cdot)$ substitutes $\kappa$-variables in predicates $p$, constraints $c$, and sets of constraints $C$ with their $\sigma$-assignments:

[TABLE]

Satisfaction  A verification condition (VC) is a constraint $c$ that has no $\kappa$ applications; i.e. $\mathsf{kvars}(c)=\emptyset$. We say that an assignment $\sigma$ satisfies constraint $c$, written $\sigma\models c$, if $\sigma(c)$ is a VC that is: (a) well-formed, and (b) logically valid (Nelson, 1981). Figure 5 formalizes the notion of satisfaction and lifts it to sets of constraints. We say that $c$ is satisfiable if some assignment $\sigma$ satisfies $c$. The following lemmas follow from the definition of satisfaction and validity:

Lemma 4.1 (Weaken).

*If $G\models p$ then $G\models p\leavevmode\nobreak\ \vee\leavevmode\nobreak\ p^{\prime}$. *

Lemma 4.2 (Strengthen).

If $\sigma\models\forall{{x}\!:\!{b}}.\ {p}\Rightarrow{c}$ and $\sigma\models\forall{{x}\!:\!{b}}.\ {p^{\prime}}\Rightarrow{p}$ then $\sigma\models\forall{{x}\!:\!{b}}.\ {p^{\prime}}\Rightarrow{c}$.

Composing Assignments  For two assignments $\sigma$ and $\sigma^{\prime}$ we write $\sigma\!\cdot\!\sigma^{\prime}$ to denote the assignment:

[TABLE]

The following Lemmas, proved by induction on the structure of $c$, characterize the relationship between assignment composition and satisfaction.

Lemma 4.3 (Composition-Preserves-Sat).

If $\sigma\models c$ then $\sigma^{\prime}\!\cdot\!\sigma\models c$.

Lemma 4.4 (Composition-Validity).

$\sigma\!\cdot\!\sigma^{\prime}\models c$* if and only if $\sigma\models\sigma^{\prime}(c)$.*

4.3. Dependencies and Decomposition

Next, we describe various properties of constraints that we will exploit to determine satisfiability.

Flat Constraints  A flat or non-nested constraint $c$ is of the form:

[TABLE]

By induction on the structure of $c$ we can show that the procedure $\mathsf{flat}(c)$, shown in Figure 12, returns a set of flat constraints that are satisfiable exactly when $c$ is satisfiable.

Lemma 4.5 (Flattening).

$\sigma\models c$* if and only if $\sigma\models\mathsf{flat}(c)$.*

Heads and Bodies  Let $c\equiv\forall{{x_{1}}\!:\!{b_{1}}}.\ {p_{1}}\Rightarrow{\ldots\Rightarrow\forall{{x_{n}}\!:\!{b_{n}}}.\ {p_{n}}\Rightarrow{p}}$ be a flat constraint. We write $\mathsf{head}(c)$ for the predicate $p$ that is the right-most “consequent” of $c$. We write $\mathsf{body}(c)$ for the set of predicates $p_{1},\ldots,p_{n}$ that are the “antecedents” of $c$.

Dependencies  Let $\mathsf{kvars}(c)$ denote the the set of $\kappa$-variables in a constraint $c$. We can define the following sets of dependencies:

[TABLE]

We write $\mathsf{deps}^{*}(c)$ (resp. $\mathsf{deps}^{*}(\hat{K},\ c)$) for the reflexive and transitive closure of $\mathsf{deps}(c)$ (resp. $\mathsf{deps}(\hat{K},\ c)$). Intuitively, the dependencies of a constraint comprise the set of pairs $(\kappa,\kappa^{\prime})$ where $\kappa$ appears in a body (hypothesis) for a clause where $\kappa^{\prime}$ is in the head (goal).

Cuts and Cycles  A set of variables $\hat{K}$ cuts $c$ if the relation $\mathsf{deps}^{*}(\hat{K},\ c)$ is acyclic. A set of variables $K^{\prime}$ is acyclic in $c$ if $K-K^{\prime}$ cuts $c$. Intuitively, a set $K^{\prime}$ is acyclic in $c$ if the closure of dependencies restricted to $K^{\prime}$ (i.e. excluding variables not in $K^{\prime}$) has no cycles. A single variable $\kappa$ is acyclic in $c$ if $\{\kappa\}$ is acyclic in $c$. Intuitively, a single variable $\kappa$ is acyclic in $c$ if there is no clause in $c$ where $\kappa$ appears in both the head and the body. A constraint is acyclic if the set of all $K$ is acyclic in $c$, i.e. if $\mathsf{deps}^{*}(c)$ is acyclic. In the sequel, for clarity of exposition we assume the invariant that whenever relevant, $\kappa$ is acyclic in $c$. (Of course, our algorithm maintains this property, as described in § 5.5.)

Definitions and Uses  The definitions (resp. uses) of $\kappa$ in $c$, written $c\!\downarrow\!\kappa$ (resp. $c\!\uparrow\!\kappa$), are the subset of $\mathsf{flat}(c)$ such that the head contains (resp. does not contain) $\kappa$:

[TABLE]

By induction on the structure of $c$ we can check that:

Lemma 4.6 (Flatten-Definitions).

$\forall{x}.\ {p}\Rightarrow{c\!\downarrow\!\kappa}\equiv(\forall{x}.\ {p}\Rightarrow{c})\!\downarrow\!\kappa$**

Since the definitions and uses of a $\kappa$ partition $\mathsf{flat}(c)$, we can show that $\sigma$ satisfies $c$ if it satisfies the definitions and uses of $\kappa$ in $c$:

Lemma 4.7 (Partition).

If $\kappa$ is acyclic in $c$ then $\sigma\models c$ if and only if $\sigma\models c\!\downarrow\!\kappa$ and $\sigma\models c\!\uparrow\!\kappa$.

4.4. Generation

Next, we show how to map a term $e$ into a constraint $c$ whose satisfiability implies the safety of $e$.

Shapes ($\mathsf{shape}$)  Procedure $\mathsf{shape}$, elided for brevity, takes as input a refined type $t$ and returns as output the non-refined version obtained by erasing the refinements from $t$.

Templates ($\mathsf{fresh}$)  Procedure $\mathsf{fresh}(\mathrm{\Gamma},\ \tau)$ (Figure 6) takes as input an environment and a non-refined type $\tau$, and returns a template whose $\mathsf{shape}$ is $\tau$. Recall that each refinement variable denotes an $n$-ary relation. For example, a refinement variable that appears in the output type of a function can refer to the input parameter, i.e. can be a binary relation between the input and the output value. We track the allowed parameters by using the environment $\mathrm{\Gamma}$. In the base case, $\mathsf{fresh}$ generates a fresh $\kappa$ whose parameters correspond to the binders of $\mathrm{\Gamma}$. In the function type case, $\mathsf{fresh}$ recursively generates templates for the input and output refinements, extending the environment for the output with the input binder.

Subtyping ($\mathsf{sub}$)  Procedure $\mathsf{sub}(t,\ t^{\prime})$ (Figure 7) returns the constraint $c$ that must be satisfied for $t$ to be a subtype of $t^{\prime}$, which intuitively means, the set of values denoted by $t$ to be subsumed by those denoted by $t^{\prime}$. (See (Knowles and Flanagan, 2010; Vazou et al., 2014b) for details.) In the base case, the sub-type’s predicate must imply the super-type’s predicate. In the function case, we conjoin the contra-variant input constraint and the co-variant output constraint. For the latter, we additionally add a hypothesis assuming the stronger input type, using a generalized implication that drops binders with non-basic types as they are not supported by the first-order refinement logic:

[TABLE]

Generation ($\mathsf{cgen}$)  Finally, procedure $\mathsf{cgen}(\mathrm{\Gamma},\ e)$ (Figure 8) takes as input an environment $\mathrm{\Gamma}$ and term $e$ and returns as output a pair $(c,t)$ where $e$ typechecks if $c$ holds, and has the (refinement) template $t$. The procedure computes the template and constraint by a syntax-directed traversal of the input term. The key idea is two-fold. First: generate a fresh template for each position where the (refinement) types cannot be directly synthesized – namely, function inputs, let-binders, and polymorphic instantiation sites. Second: generate subtyping constraints at each position where values flow from one position into another.

• •

Constants and Variables yield the trivial constraint $\mathit{true}$, and templates corresponding to their primitive types, or environment bindings respectively. (The helper $\mathsf{single}$ strengthens the refinement to state the value equals the given variable, dubbed “selfification” by (Ou et al., 2004), enabling path-sensitivity  (Rondon et al., 2008; Knowles and Flanagan, 2010).)

• •

Let-binders ($\texttt{let}\;x=e_{1}\;\texttt{in}\;e_{2})$ yield the conjunction of three sub-constraints. First, we get a constraint $c_{1}$ and template $t_{1}$ from $e_{1}$. Second, we get a constraint $c_{2}$ and template $t_{2}$ from $e_{2}$ checked under the environment extended with $t_{1}$ for $x$. Third, to hide $x$ which may appear in $t_{2}$, we generate a fresh template $\hat{t}$ with the shape of $t_{2}$ and use $\mathsf{sub}$ to constrain $t_{2}$ to be a subtype of $\hat{t}$. The well-formedness requirement ensures $\hat{t}$, which is returned as the expression’s template, is assigned a well-scoped refinement type.

• •

Functions ($\lambda{x}\!:\!{\tau}.{e}$) yield a template where the input is assigned a fresh template of shape $\tau$, and the output is the template for $e$.

• •

Applications (${e}\;{y}$) yield the output template with the formal $x$ substituted for the actual $y$. (ANF ensures the substitution does not introduce arbitrary expressions into the refinements.) Furthermore, the input value $y$ is constrained to be a subtype of the function’s input type.

• •

Type-Instantiation ($e[\tau]$) is handled by generating a fresh template whose shape is that of the polymorphic instance $\tau$, and substituting that in place of the type variable $\alpha$ in the type (scheme) obtained for $e$.

Soundness of Constraint Generation  We can prove by induction on the structure of $e$ that the NNF constraints generated by $\mathsf{cgen}$ capture the refinement type checking obligations of (Knowles and Flanagan, 2010; Vazou et al., 2014b). Let $\mathsf{cgen}(e)$ denote the constraint returned by $\mathsf{cgen}(\emptyset,\ e)$. We prove that if $\mathsf{cgen}(e)$ is satisfiable, then ${\emptyset\vdash e:t}$ for some refinement type $t$. This combined with the soundness of refinement typing (Theorem 1, (Vazou et al., 2014b)) yields:

Theorem 4.8.

If $\mathsf{cgen}(e)$ is satisfiable then $e$ is safe.

5. Algorithm

Next, we describe our algorithm for solving the constraints generated by $\mathsf{cgen}$, i.e. for for finding a satisfying assignment – and hence inferring suitable refinement types. Our algorithm is an instance of the classical “unfolding” method for logic programs (Burstall and Darlington, 1977; Pettorossi and Proietti, 1994; Tamaki and Sato, 1984). We show how to apply unfolding to the NNF constraints derived from refinement typing, in a scoped fashion that avoids the blowup caused by long let-chains. First, we describe a procedure for computing the scope of a $\kappa$ variable (§ 5.1). Second, we show how to use the scope to compute the strongest solution for a single $\kappa$ variable (§ 5.2). Third, we describe how we can eliminate a $\kappa$ by replacing it with its strongest solution (§ 5.3). Fourth, we show how the above procedure can be repeated when the constraints are acyclic (§ 5.4). Finally, we describe how to use our method when the constraints have cycles (§ 5.5).

5.1. The Scope of a Variable

Procedure $\mathsf{scope}(\kappa,c)$ (Fig. 9) returns a sub-constraint of $c$ of the form: ${\forall(\overline{{{x_{i}}\!:\!{p_{i}}}})\Rightarrow c^{\prime}}$ such that (1) $\kappa$ does not occur in any $p_{i}$, and (2) all occurrences of $\kappa$ in $c$ occur in $c^{\prime}$. As occurrences of $\kappa$ in $c$ occur under $\overline{{{x_{i}}\!:\!{p_{i}}}}$, we can omit these binders from the solution of $\kappa$, thereby avoiding the blowup from unfolding let-chains described in § 2.4. Restricting unfolding to $\mathsf{scope}(\kappa,c)$ does not affect satisfiability. The omitted hypotheses are redundant as they are already present at all uses of $\kappa$. This intuition is captured by the following lemmas that follow by induction on $c$.

Lemma 5.1 (Scoped-Definitions).

$c\!\downarrow\!\kappa\equiv\mathsf{scope}(\kappa,c)\!\downarrow\!\kappa$**

Lemma 5.2 (Scoped-Uses).

$c\!\uparrow\!\kappa\equiv\mathsf{scope}(\kappa,c)\!\uparrow\!\kappa\cup C$* for some flat constraints $C$ such that $\kappa\not\in C$.*

Lemma 5.3 (Scoped-Satisfaction).

If $\sigma\models c$ then $\sigma\models\mathsf{scope}(\kappa,c)$.

5.2. The Strongest Solution

Procedure $\mathsf{sol1}(\kappa,c)$ (Fig. 10) returns a predicate that is guaranteed to satisfy all the clauses where $\kappa$ appears as the head. The procedure recursively traverses $c$ to compute the returned predicate as the disjunction of those bodies in $c$ where $\kappa$ appears as the head. When the head does not contain $\kappa$, the output predicate is the empty disjunction, $\mathit{false}$.

The Strongest Solution  The strongest (resp. scoped) solution for $\kappa$ in $c$, written $\sigma^{c}_{\kappa}$ (resp. $\hat{\sigma}^{c}_{\kappa}$) is:

[TABLE]

The name “strongest solution” is justified by the following theorems. First, we prove that $\sigma^{c}_{\kappa}$ satisfies the definitions of $\kappa$ in $c$.

Lemma 5.4 (Strongest-Sat-Definitions).

$\sigma^{c}_{\kappa}\models c\!\downarrow\!\kappa$**

As an example, consider the constraint: ${c_{5}\doteq\forall{a}.\ {p\ a}\Rightarrow{\forall{b}.\ {q\ b}\Rightarrow{\kappa(a)\wedge\kappa(b)}}}.$ Below, we show each sub-constraint $c_{i}$, and the corresponding solution returned by $\mathsf{sol1}(\kappa,c_{i})$:

[TABLE]

Note that in essence, $\sigma^{c_{5}}_{\kappa}\doteq[\kappa\mapsto\lambda x.\mathsf{sol1}(\kappa,c_{5})]$ maps $\kappa$ to the disjunction of the two hypotheses (bodies) under which $\kappa$ appears, thereby satisfying both implications, and hence satisfying $c_{5}\!\downarrow\!\kappa$.

The Strongest Scoped Solution  The addition of hypotheses – the binders $\overline{{{x_{i}}\!:\!{p_{i}}}}$ under which $\kappa$ always occurs – preserves validity. Thus, Lemma 5.4 implies that the strongest scoped solution satisfies the definitions of $\kappa$ in $c$.

Theorem 5.5 (Strongest-Scoped-Sat-Definitions).

$\hat{\sigma}^{c}_{\kappa}\models c\!\downarrow\!\kappa$.

Furthermore, if there exists a solution $\sigma$ that satisfies $c$ then the composition of $\sigma$ and the strongest scoped solution also satisfies $c$.

Theorem 5.6 (Strongest-Scoped-Sat-Uses).

If $\sigma\models c$ then $\sigma\!\cdot\!\hat{\sigma}^{c}_{\kappa}\models c$.

By Theorem 5.5 and Lemma 4.7 it suffices to restrict attention to uses of $\kappa$, i.e. to prove that if $\sigma\models c\!\uparrow\!\kappa$ then $\sigma\!\cdot\!\hat{\sigma}^{c}_{\kappa}\models c\!\uparrow\!\kappa$. We show this via a key lemma that states that any solution $\sigma$ that satisfies $c$, must assign $\kappa$ to a predicate that is implied by, i.e. weaker than, $\mathsf{sol1}(\kappa,c)$.

Lemma 5.7 (Strongest-Solution).

If $\sigma,\overline{{{x_{i}}\!:\!{p_{i}}}}\models c$ then $\sigma,\overline{{{x_{i}}\!:\!{p_{i}}}}\models\sigma^{c}_{\kappa}(p)\Rightarrow p$.

We use the above lemma to conclude that the hypotheses in $c\!\uparrow\!\kappa$ are strengthened under $\sigma\!\cdot\!\hat{\sigma}^{c}_{\kappa}$, and hence, that each corresponding goal remains valid under the composed assignment.

5.3. Eliminating One Variable

Next, we show how to eliminate a single $\kappa$ variable by replacing it with its strongest solution.

Variable Elimination ($\mathsf{elim^{*}}(\sigma,c)$)  Procedure $\mathsf{elim^{*}}(\sigma,c)$ (Fig. 11) eliminates from $c$ all the $\kappa$ variables defined in $\sigma$ by replacing them with $\sigma(\kappa)$. That is, the procedure returns as output a constraint $c^{\prime}$ where: (1) every body-occurrence of a $\kappa$ i.e. where $\kappa$ appears as a hypothesis, is replaced by $\sigma(\kappa)$, and (2) every head-occurrence of a $\kappa$ i.e. where $\kappa$ appears as a goal, is replaced by $\mathit{true}$ if $\kappa$ is in the domain of $\sigma$, and left unchanged otherwise. We prove by induction over $c$ that eliminating a single variable $\kappa$ yields a constraint over just the uses of that variable:

Lemma 5.8 ($\mathsf{elim^{*}}$).

If $\mathsf{domain}(\sigma)=\{\kappa\}$ and $c^{\prime}=\mathsf{elim^{*}}(\sigma,c)$ then $\kappa\not\in c^{\prime}$ and $\mathsf{flat}(c^{\prime})=\sigma(c\!\uparrow\!\kappa)$.

Eliminating One Variable  Procedure $\mathsf{elim1}(\kappa,c)$ (Fig. 11) eliminates $\kappa$ from a constraint $c$ by invoking $\mathsf{elim}$ on the strongest (scoped) solution for $\kappa$ in $c$. We prove that if $\kappa$ is acyclic in $c$ then $\mathsf{elim1}(\kappa,c)$ returns an constraint without $\kappa$ that is satisfiable if and only if $c$ is satisfiable.

Theorem 5.9 (Elim-Preserves-Satisfiability).

$\mathsf{elim1}(\kappa,c)$* is satisfiable iff $c$ is satisfiable.*

Intuitively, if $\sigma\models\mathsf{elim1}(\kappa,c)$ then, via Theorem 5.6 and Lemma 4.3, we have $\sigma\!\cdot\!\hat{\sigma}^{c}_{\kappa}$ satisfies $c$. Dually, if $\sigma\models c$ then we show that $\sigma\models\mathsf{elim1}(\kappa,c)$. See § A for details.

5.4. Eliminating Acyclic Variables

When the constraint $c$ is acyclic, we can iteratively eliminate all the variables in $K$ to obtain a VC whose validity determines the satisfiability of $c$, as each elimination preserves acyclicity:

Lemma 5.10 (Elim-Acyclic).

If $K^{\prime}$ is acylic in $c$, ${\mathsf{deps}(\sigma)\subseteq\mathsf{deps}(c)}$ then $K^{\prime}$ is acyclic in $\mathsf{elim^{*}}(\sigma,c)$.

Eliminating Many Variables  Procedure $\mathsf{elim}(K,c)$ (Fig. 12) eliminates a set of acyclic $K$ variables by iteratively eliminating each variable via $\mathsf{elim1}$. Using Theorem 5.9, Lemma 5.8 and Lemma 5.10 we show that the elimination of multiple acyclic $\kappa$-variables also preserves satisfiability.

Corollary 5.11 (Exact-Satisfaction).

Let $c^{\prime}\doteq\mathsf{elim}(K,c)$.

1. (1)

$\mathsf{kvars}(c^{\prime})=\emptyset$, i.e. $c^{\prime}$ is a VC, and 2. (2)

$c^{\prime}$* is satisfiable iff $c$ is satisfiable.*

Unavoidable Worst-Case Blowup  Note that in the worst case, the $\mathsf{elim}$ procedure can cause an exponential blowup in the constraint size. In general some form of blowup is unavoidable as even the Boolean version of the constraint satisfaction problem is complete for exponential time. A boolean constraint is an acyclic constraint where each variable is of type Bool. The Boolean Constraint Satisfaction (BcSat) problem is to decide whether a given boolean constraint is satisfiable.

Theorem 5.12.

BcSat* is ExpTime-complete.*

The above is a corollary of (Godefroid and Yannakakis, 2013) and the fact that reachability of (non-recursive) boolean programs is equivalent to the satisfaction of (acyclic) boolean constraints via the correspondence of  (Jhala et al., 2011). Thus, as validity checking is in Np, it is not possible to always generate compact (polynomial sized) formulas, assuming $\textsc{ExpTime}\not=\textsc{Np}$.

Avoiding Let-Chain Blowup  Recall the example from § 2.4. Let $c$ be the NNF constraint in (14) and consider the sequence of intermediate constraints produced by eliminating $\kappa_{1},\ldots,\kappa_{n}$ from $c$:

[TABLE]

that is easily proved valid by the SMT solver.

5.5. Eliminating Cyclic Variables

When the constraint $c$ is cyclic, the satisfaction problem is undecidable via a reduction from the problem of checking the safety of while-programs (Bjørner et al., 2015). Consequently, we can only compute over-approximate or conservative solutions via abstract interpretation (Jhala et al., 2011). Our approach is to (1) compute the set of variables that make the constraints cyclic (i.e. whose absence would make the constraints acyclic), (2) eliminate all except those variables, and (3) use predicate abstraction to solve the resulting constraint, yielding a method that is much faster and more precise (§ 6), than “global” Liquid Typing (Rondon et al., 2008).

Cut Variables  A set of refinement variables $\hat{K}$ cuts a constraint $c$ if $K-\hat{K}$ is acyclic in $c$. We cannot compute the minimum set of cut variables as this is the NP-Complete minimum feedback vertex set problem (Karp, 1972). Instead we use a greedy heuristic to compute $\hat{K}$. We compute the strongest connected component (SCC) digraph for $\mathsf{deps}^{*}(c)$, and iteratively remove $\kappa$-variables (and recompute the digraph) until each SCC has a single vertex i.e. the graph is acyclic. The reasoning for Lemma 5.11 yields the following corollary:

Corollary 5.13.

If $\hat{K}$ cuts $c$ then $\mathsf{elim}(K-\hat{K},c)$ returns a constraint $c^{\prime}$ such that $\mathsf{kvars}(c^{\prime})\subseteq\hat{K}$ and $c^{\prime}$ is satisfiable iff $c$ is satisfiable.

Exact and Approximate Constraint Satisfaction  Procedure $\mathsf{sat}(c,\mathbb{Q})$ (Fig. 12) computes a set of cut variables $\hat{K}$, and then uses $\mathsf{elim}$ to compute exact solutions for non-cut variables, and finally computes approximate solutions for the residual cut variables left over after elimination, using the $\mathsf{solve}$ procedure from (Rondon et al., 2008) which computes the satisfaction of (non-nested) constrained Horn Clauses (CHC) (obtained via $\mathsf{flat}$) using predicate abstraction (Graf and Saïdi, 1997; Flanagan et al., 2001).

Theorem 5.14 (Satisfaction).

1. (1)

If $\mathsf{sat}(c,\mathbb{Q})$ then $c$ is satisfiable. 2. (2)

If $c$ is acyclic, then $\mathsf{sat}(c,\mathbb{Q})$ iff $c$ is satisfiable.

These results follow from Corollary 5.11,  5.13, the properties of $\mathsf{solve}$ (Theorem 2, (Rondon et al., 2008)), and as $\mathsf{solve}$ reduces to $\mathsf{SmtValid}(c)$ when $\mathsf{kvars}(c)$ is empty.

6. Evaluation

We have implemented Fusion within the LiquidHaskell refinement type checker (Vazou et al., 2014b). It is used by default in the current version 111https://github.com/ucsd-progsys/liquidhaskell. We evaluate the speed and precision of Fusion on two sets of benchmarks from the LiquidHaskell project totalling more than 12KLOC. Our formalism based on call-by-value evaluation is sound for Haskell as we also simultaneously prove termination for all potentially bottom-inhabited terms, as described in (Vazou et al., 2014b). Our results show that Fusion yields nearly $2\times$ speedups for safety verification benchmarks and, by synthesizing the most precise types more than $10\times$ faster, actually enables theorem proving.

Safety Property Benchmarks  The first set of benchmarks are drawn from the Haskell standard libraries and detailed in (Vazou et al., 2014a). Data-Struct comprises applicative data structures like red-black trees, lists (Data.List), splay trees (Data.Set.Splay), and binary search trees (Data.Map.Base); we verify termination and structure specific invariants like ordering and balance. Vector-Algorithms comprises a suite of imperative (i.e. monadic) array-based sorting algorithms; we verify termination and the correctness of array accesses. Text and Bytestring are the standard libraries for high-performance unicode text and byte-array processing which are implemented via low-level pointer arithmetic; we verify termination, memory safety and correctness properties specified by the library API.

Theorem Proving Benchmarks  Recent work shows how refinement typing can convert legacy languages like Haskell into proof assistants where ordinary programs can be used to write arbitrary proofs of correctness about the “deep specifications” of other programs, and have the proofs checked via refinement typing (Vazou and Jhala, 2016). The second set of benchmarks corresponds to a set of programs corresponding to such proofs. Arith includes theorems about the growth of the fibonacci and ackermann functions; Fold includes theorems about the universality of traversals; Monoid, Functor, Applicative and Monad includes proofs of the respective category-theoretic laws for the Maybe, List, and Id instances of the respective typeclasses; and finally, SatSolver and Unification are fully verified implementations of the respective algorithms from the Zombie suite which, absent SMT support, requires significantly more local annotations (proof terms) from the user (Casinghino et al., 2014; Sjöberg and Weirich, 2015).

Methodology  For each benchmark, we compare the performance of LiquidHaskell using the (L) global refinement inference from (Rondon et al., 2008), and using our (F) local refinement algorithm. We compare the amount of Time(s), in seconds, it took to check each benchmark. Each benchmark represents several Haskell files (modules); we report Qualifiers, the average number of qualifiers (predicates) that were required to synthesize the types needed for verification per file. In addition to the variables needed to eliminate cycles, we aggressively mark all refinement variables appearing in templates for “top-level” types as cut-variables to ensure that simple refinements (over qualifiers) are synthesized for such functions. All benchmarks were run on a MacBook Pro with a 2.2 GHz Intel Core i7 processor, using the Z3 SMT solver for checking validity. Table 1 summarizes the results.

Safety Verification Results  Two points emerge from the safety verification benchmarks. First, for the larger benchmarks (text and bytestring), for which there already exist suitable qualifiers permitting global inference, the new local Fusion algorithm yields significant speedups – often halving the time taken for verification. (Note this includes end-to-end time, including name resolution, plain type checking etc., and so the actual speedup for just refinement checking is even greater.) Second, even for these benchmarks, Fusion reduces (nearly halves) the number of required qualifiers. This makes the checker significantly easier to use, as the programmer does not have reason about which qualifiers to use for intermediate terms. By synthesizing strongest refinements, Fusion removes a key source of unpredictability and hard-to-diagnose false alarms.

Theorem Proving Results  The improvement is more stark for the theorem proving benchmarks: most of them can only be checked using local inference. There are several reasons for this. The proofs are made possible by heavy use of polymorphic proof combinators. As the specifications are much more complicated, the combinators’ type variables must be (automatically) instantiated with significantly more complex refinements that relate many program variables. Thus, it is very difficult for the user to even determine the relevant qualifiers. Even if they could, the qualifiers have many free variable (parameters) which causes an exponential blowup when matching against actual program variables, making global, abstract interpretation based refinement synthesis impossible. In contrast, since the theorem proving benchmarks have almost no cyclic dependencies, Fusion makes short work of automatically synthesizing the relevant refinement instantiations, making complex proofs possible.

Comparison with other Tools  We are not aware of any other tool that scales up to these programs. F* (Swamy et al., 2011) requires local annotations as described in § 2, Mochi (Unno et al., 2013) requires no annotations but may diverge, and does not support uninterpreted functions which precludes all of our benchmarks. Similarly, existing Horn Solvers like $\mu$Z3 may diverge, while Eldarica (Rümmer et al., 2015), HSF (Grebenshchikov et al., 2012), and Spacer (Komuravelli et al., 2016) do not support uninterpreted functions.

7. Related Work

Floyd-Hoare Logics and Model Checking  The process of eliminating refinement variables to get a single verification condition (checked by SMT) is analogous to the VC-generation step used in ESC-style checkers (Nelson, 1981; Flanagan et al., 2002). Indeed we use the term “strongest refinement” or “solution” for the intermediate types to highlight the analogy with the notion of “strongest postconditions” from Floyd-Hoare Logic. While Fusion seeks to minimize the size of the generated VC, unlike in the intra-procedural case (Flanagan and Saxe, 2000; Leino, 2005), ExpTime-completeness means we cannot get compact VCs (Theorem 5.12). In the presence of loops, direct VC generation is insufficient, and one must compute over-approximations. Fusion’s elimination procedure can be viewed as a generalization of the large block encoding method (Beyer et al., 2009) where over-approximation is performed not at each instruction, but only at “back edges” in the control-flow graph. Similarly, in program analyses it is common to “inline” the code for a procedure at a call site to improve precision. In (Swamy et al., 2013), the authors show how to generalize the notions of composing weakest preconditions across higher-order functions via the notion of a Dijkstra Monad. Fusion’s elimination procedure is a way to systematically generalize and lift the Floyd-Hoare notions of strongest-postconditions (dually, weakest-preconditions), large block encodings, and procedure inlining to the typed, higher order setting. However, unlike Dijkstra Monads, Fusion exploits the compositional structure of types to locally synthesize precise refinements (i.e. invariants) in the presence of polymorphic collections and higher-order functions, to allow checking examples like ex2, ex3, and ex4 (§ 2).

Local Type Inference  Fusion performs a local inference in that if the constraints are acyclic, then Fusion is able to synthesize all intermediate refinement types exactly. However, refinements render the problem (and our solution) quite different than classical local typing (Pierce and Turner, 1998), even with subtyping (Odersky et al., 2001). First, even when all top-level (recursive) functions have signatures, the constraints may get cycles, for example, at instantiation sites for fold functions (whose polymorphic type variables must be instantiated with the analogue of a “loop invariant”.) Second, our approach is orthogonal to bidirectional type checking. Indeed, they can be (and in our implementation, are) combined to yield a simpler system of constraints, but we still need $\mathsf{solK}$ and $\mathsf{elim}$ to synthesize the strongest refinements relating different program variables.

Refinement Inference  There are several other approaches to synthesizing refinements. First, (Knowles and Flanagan, 2009) shows how existentials can be used to type let-binders. Second, (Bengtson et al., 2008) shows how a form of bidirectional typing can be used to infer some intermediate types. Third, (Rondon et al., 2008) introduces the liquid typing framework for synthesizing refinements via abstract interpretation. Fourth, (Polikarpova et al., 2016) shows that liquid typing can be made bidirectional and presents a new demand driven (“round trip”) algorithm for doing the abstract interpretation (and also solving for the weakest solution.) However, none of the above approaches is able to handle the idiomatic examples shown in  § 2, or can only do so if given a suitable abstract domain (via templates). We can try to infer such templates via abstraction refinement (Jhala et al., 2011; Kobayashi et al., 2011; Unno et al., 2013) but that approach is notoriously unpredictable and prone to diverging, especially in the presence of uninterpreted functions which are ubiquitous in our examples. Finally, (Zhu et al., 2015) shows how machine learning over dynamic traces can be used to learn refinements (in a generalization of the approach pioneered by (Ernst et al., 2001)). However, this needs closed programs (that can be run), which can limit applicability to higher order functions.

Horn Clauses  Horn clauses have recently become a popular “intermediate representation” for verification problems (Bjørner et al., 2015), as they can be used to encode the proof rules for classical imperative Floyd-Hoare logics, and concurrent programs (Grebenshchikov et al., 2012) among others. However, current Horn Clause solvers e.g. (Hoder and Bjørner, 2012; Grebenshchikov et al., 2012; Rümmer et al., 2015) are based on CEGAR and interpolation and hence, to quote a recent survey (Bjørner et al., 2015): “mainly tuned for real and linear integer arithmetic and Boolean domains” rendering them unable to check any of our benchmarks which make extensive use of uninterpreted functions. Our work shows how to (1) algorithmically generate NNF clauses from typed, higher-order programs, in a way that preserves scoping, (2) use an optimized form of “unfolding” (Burstall and Darlington, 1977; Pettorossi and Proietti, 1994; Tamaki and Sato, 1984) to synthesize the most precise type and (3) thereby, obtain a method for improving the speed, precision and completeness of refinement type checking.

Acknowledgements.

We thank the anonymous referees, Nadia Polikarpova, Eric Seidel and Niki Vazou for their invaluable feedback on earlier drafts of this paper. This material is based upon work supported by the Sponsor National Science Foundation http://dx.doi.org/10.13039/100000001 under Grant Numbers Grant #CCF-1422471, Grant #CCF-1223850, and Grant #CCF-1218344, and a generous gift from Microsoft Research.

Appendix A Appendix: Proofs

We include below the proofs of the key theorems.

Proof.

(Lemma 5.7) Assume that $p\equiv\kappa({\overline{z}})$ where $\overline{z}=\mathsf{params}(\kappa)$ The other cases are trivial as $\sigma^{c}_{\kappa}(p)=p$, and $\sigma(p_{1})\Rightarrow p_{1}$ and $\sigma(p_{2})\Rightarrow p_{2}$ implies $\sigma(p_{1}\wedge p_{2})\Rightarrow p_{1}\wedge p_{2}$. The proof is by induction on the structure of $c$.

[TABLE]

∎

Proof.

(Theorem 5.4) The proof is an induction on the structure of $c$.

[TABLE]

As the above holds for an arbitrary $c^{\prime\prime}\in c^{\prime}\!\downarrow\!\kappa$, we get $\sigma^{c}_{\kappa}\models c\!\downarrow\!\kappa$. ∎

Proof.

(Theorem 5.5)

[TABLE]

∎

Proof.

(Theorem 5.6) By Theorem 5.5 it suffices to prove that if $\sigma\models c$ then $\sigma\!\cdot\!\hat{\sigma}^{c}_{\kappa}\models c\!\uparrow\!\kappa$.

[TABLE]

∎

Lemma A.1 (Eliminate-Definitions).

$\mathsf{flat}(\mathsf{elim1}(\kappa,c))=\hat{\sigma}^{c}_{\kappa}(c\!\uparrow\!\kappa)$.

Proof.

(Lemma A.1) The above follows from the observations that: (a) $\mathsf{domain}(\hat{\sigma}^{c}_{\kappa})=\{\kappa\}$, (b) $\mathsf{elim1}(\kappa,c)=\mathsf{elim^{*}}(\hat{\sigma}^{c}_{\kappa},c)$, and (c) Lemma 5.8, as $\mathsf{domain}(\hat{\sigma}^{c}_{\kappa})=\{\kappa\}$. ∎

Proof.

(Theorem 5.9) Let $c^{\prime}=\mathsf{elim1}(\kappa,c)=\mathsf{elim^{*}}(\hat{\sigma}^{c}_{\kappa},c)$. We prove the two directions separately.

Case: $c^{\prime}$ is satisfiable implies $c$ is satisfiable

[TABLE]

∎