1

[http://icfp17.sigplan.org/track/icfp-2017-Artifacts]artifact_evaluated-
reusable.png

# Local Refinement Typing

Benjamin Cosman  UC San DiegoUSA<EMAIL_ADDRESS>and  Ranjit Jhala  UC
San DiegoUSA<EMAIL_ADDRESS>
###### 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 $2\times$ faster. In a new set of theorem
proving benchmarks Fusion is both $10-50\times$ faster and, by synthesizing
the most precise types, avoids false alarms to make verification possible.

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):

$\displaystyle\forall{n}.\ {}$ $\displaystyle 0\leq n$ $\displaystyle\
\Rightarrow\ $ $\displaystyle\forall{\nu}.\ {\nu=n}$ $\displaystyle\
\Rightarrow 0\leq\nu$ $\displaystyle\wedge\ $ $\displaystyle 0\not\leq n$
$\displaystyle\ \Rightarrow\ $ $\displaystyle\forall{\nu}.\ {\nu=0-n}$
$\displaystyle\ \Rightarrow 0\leq\nu$

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.

⬇

inc :: x:Int -> {v:Int | v = x + 1} \-- increment by one

dec :: x:Int -> {v:Int | v = x - 1} \-- decrement by one

[] :: List a \-- list : "nil"

(:) :: a -> List a -> List a \-- list : "cons"

last :: List a -> a \-- last element of a list

map :: (a -> b) -> List a -> List b \-- mapping over a list

(.) :: (b -> c) -> (a -> b) -> a -> c \-- function composition

Figure 1. Type specifications for library functions

_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

$\texttt{y}\ ::\ \exists{0\leq\texttt{t}}.\ {}\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{t}-1\\}}}$

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

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

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).

⬇

ex1 :: Nat -> Nat

ex1 x =

let y =

let t = x

in

dec t

in

inc y

${\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}{\wedge}}$

⬇

ex2 :: Nat -> Nat

ex2 x =

let ys = let n = dec x

p = inc x

xs = n : []

in p : xs

y = last ys

in

inc y

Figure 2. Examples: (ex1) Local variables, (ex2) Collections

###  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:

x $\displaystyle\ ::\ {{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid 0\leq\nu\\}}}$ t
$\displaystyle\ ::\ {{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{x}\\}}}$
dec t $\displaystyle\ ::\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{t}-1\\}}}$ The term dec t is
bound to y but as t goes out of scope we assign y a template y $\displaystyle\
::\ {{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa({\nu})\\}}}}$ with a fresh
$\kappa$ denoting the (unknown) refinement for the expression. That is, y is a
Int value $\nu$ that satisfies $\kappa({\nu})$. We will constrain $\kappa$ to
be a well-scoped super-type of its body dec t. Finally, the output of ex1 gets
assigned inc y $\displaystyle\ ::\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{y}+1\\}}}$

_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:

(1) $\displaystyle\forall{\texttt{x}}.\ {0\leq\texttt{x}}\ \Rightarrow\ $
$\displaystyle\forall{\nu}.\ {\nu=\texttt{x}-1}\ \Rightarrow\ \kappa({\nu})$
(2) $\displaystyle\wedge\ \ $ $\displaystyle\forall{\texttt{y}}.\
{\kappa({\texttt{y}})}\ \Rightarrow\ $ $\displaystyle\forall{\nu}.\
{\nu=\texttt{y}+1}\ \Rightarrow\ 0\leq\nu$

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

(3) $\displaystyle\kappa({z})$ $\displaystyle\ \doteq\ \exists{x}.\ {0\leq x\
\wedge(\exists{\nu}.\ {\nu=x-1\ \wedge\ \nu=z})}$

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

n $\displaystyle\ ::\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{x}-1\\}}}$ p $\displaystyle\
::\ {{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{x}+1\\}}}$ The lists xs
and ys are created by invoking the nil and cons constructors (Fig 1.) In the
two cases, we respectively instantiate the polymorphic type variable a (in the
constructors’ signatures from Figure 1) with the (unknown) templates over
fresh $\kappa$ variables to get xs $\displaystyle\ ::\ \texttt{List}\
{{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa_{x}({\nu})\\}}}}$ ys
$\displaystyle\ ::\ \texttt{List}\
{{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa_{y}({\nu})\\}}}}$ as the output
of last has the same type its input list, we get: y $\displaystyle\ ::\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa_{y}({\nu})\\}}}$ inc y
$\displaystyle\ ::\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{y}+1\\}}}$

_2\. Constraints_ We get four implication constraints from ex2.

$\displaystyle\forall{\texttt{x}}.\ {0\leq\texttt{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$
$\displaystyle\quad\quad\quad\forall{\texttt{p}}.\
{\texttt{p}=\texttt{x}+1}\Rightarrow$ (4)
$\displaystyle\quad\quad\quad\quad\wedge\ \forall{\nu}.\
{\nu=\texttt{n}}\Rightarrow\kappa_{x}({\nu})$ (5)
$\displaystyle\quad\quad\quad\quad\wedge\ \forall{\nu}.\
{\nu=\texttt{p}}\Rightarrow\kappa_{y}({\nu})$ (6)
$\displaystyle\quad\quad\quad\quad\wedge\ \forall{\nu}.\
{\kappa_{x}({\nu})}\Rightarrow\kappa_{y}({\nu})$ $\displaystyle\quad\wedge\
\forall{\texttt{y}}.\ {\kappa_{y}({\texttt{y}})}\Rightarrow$ (7)
$\displaystyle\quad\quad\quad\forall{\nu}.\ {\nu=\texttt{y}+1}\Rightarrow
0\leq\nu$

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:

$\displaystyle\kappa_{x}({z})$ $\displaystyle\doteq\ $
$\displaystyle\exists{\texttt{x}}.\ {0\leq\texttt{x}}\ \wedge$
$\displaystyle\quad\exists{\texttt{n}}.\ {\texttt{n}=\texttt{x}-1}\ \wedge$
$\displaystyle\quad\quad\exists{\texttt{p}}.\ {\texttt{p}=\texttt{x}+1}\
\wedge$ $\displaystyle\quad\quad\quad\exists{\nu}.\ {\nu=n\ \wedge\ \nu=z}$
$\displaystyle\ \ldots\mbox{from}\ (\ref{eq:ex2:1})$ which is essentially
$0\leq z+1$, or almost-Nat, and the disjunction of (5, 6) yields
$\displaystyle\kappa_{y}({z})$ $\displaystyle\doteq\ $
$\displaystyle\exists{\texttt{x}}.\ {0\leq\texttt{x}}\ \wedge$
$\displaystyle\quad\exists{\texttt{n}}.\ {\texttt{n}=\texttt{x}-1}\ \wedge$
$\displaystyle\quad\quad\exists{\texttt{p}}.\ {\texttt{p}=\texttt{x}+1}\
\wedge$ $\displaystyle\quad\quad\quad\vee\ \exists{\nu}.\ {\nu=\texttt{p}\
\wedge\ \nu=z}$ $\displaystyle\ \ldots\mbox{from}\ (\ref{eq:ex2:2})$
$\displaystyle\quad\quad\quad\vee\ \exists{\nu}.\ {\nu=\texttt{n}\ \wedge\
\nu=z}$ $\displaystyle\ \ldots\mbox{from}\ (\ref{eq:ex2:3})$

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

⬇

ex3 :: Nat -> Nat

ex3 = let fn = \a -> dec a

fp = \b -> inc b

in fp . fn

⬇

ex4 :: List Nat -> List Nat

ex4 = let fn = \a -> dec a

fp = \b -> inc b

in map fp . map fn

Figure 3. Examples: (ex3) Higher-Order Composition, (ex4) Higher-Order
Iteration.

#### 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:

(8) fn $\displaystyle\ ::\
{{\\{{a}\\!:\\!{\texttt{{Int}}}\mid\kappa_{a}({a})\\}}}$ $\displaystyle\
\rightarrow{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa_{b}({\nu})\\}}}$ (9) fp
$\displaystyle\ ::\ {{\\{{b}\\!:\\!{\texttt{{Int}}}\mid\kappa_{b}({b})\\}}}$
$\displaystyle\
\rightarrow{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa_{c}({\nu})\\}}}$ fp .
fn $\displaystyle\ ::\
{{\\{{a}\\!:\\!{\texttt{{Int}}}\mid\kappa_{a}({a})\\}}}$ $\displaystyle\
\rightarrow{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\kappa_{c}({\nu})\\}}}$

_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:

(10) $\displaystyle\forall{a}.\ {\kappa_{a}({a})}$ $\displaystyle\
\Rightarrow\ \forall{\nu}.\ {\nu=a-1}$ $\displaystyle\ \Rightarrow\
\kappa_{b}({\nu})$ (11) $\displaystyle\wedge\quad$ $\displaystyle\forall{b}.\
{\kappa_{b}({b})}$ $\displaystyle\ \Rightarrow\ \forall{\nu}.\ {\nu=b+1}$
$\displaystyle\ \Rightarrow\ \kappa_{c}({\nu})$ Finally, fp . fn must be a
subtype of the (function) type ascribed to ex3 yielding input and output
constraints: (12) $\displaystyle\wedge\quad$ $\displaystyle\forall{\nu}.\
{0\leq\nu}$ $\displaystyle\ \Rightarrow\ \kappa_{a}({\nu})$ (13)
$\displaystyle\wedge\quad$ $\displaystyle\forall{\nu}.\ {\kappa_{c}({\nu})}$
$\displaystyle\ \Rightarrow\ 0\leq\nu$

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

$\displaystyle\kappa_{a}({z})$ $\displaystyle\ \doteq\ \exists{\nu}.\
{0\leq\nu\wedge\nu=z}$ which simplifies to ${0\leq z}$, which plugged into
(10) gives: $\displaystyle\kappa_{b}({z})$ $\displaystyle\ \doteq\
\exists{a}.\ {0\leq a\wedge\exists{\nu}.\ {\nu=a-1\wedge\nu=z}}$ which
simplifies to ${0\leq z+1}$, which in (11) yields
$\displaystyle\kappa_{c}({z})$ $\displaystyle\ \doteq\ \exists{b}.\ {0\leq
b+1\wedge\exists{\nu}.\ {\nu=b+1\wedge\nu=z}}$ which is just $0\leq z$,
rendering implication (13) valid.

#### 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:

map fn $\displaystyle\ ::\ \texttt{List}\ {{\\{a\mid\kappa_{a}({a})\\}}}$
$\displaystyle\rightarrow\texttt{List}\ {{\\{\nu\mid\kappa_{b}({\nu})\\}}}$
map fp $\displaystyle\ ::\ \texttt{List}\ {{\\{b\mid\kappa_{b}({b})\\}}}$
$\displaystyle\rightarrow\texttt{List}\ {{\\{\nu\mid\kappa_{c}({\nu})\\}}}$
which are the templates from ex3 _lifted_ to lists, yielding map fp . map fn
$\displaystyle\ ::\ \texttt{List}\ {{\\{a\mid\kappa_{a}({a})\\}}}$
$\displaystyle\rightarrow\texttt{List}\ {{\\{\nu\mid\kappa_{c}({\nu})\\}}}$

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:

(14) $\begin{array}[]{l@{\hskip 0.02in}l@{\hskip 0.02in}l@{\hskip
0.02in}l}\forall{\texttt{x}_{0}}.\ {0\leq\texttt{x}_{0}}\hfil\hskip
<EMAIL_ADDRESS>{\nu=\texttt{x}_{0}}\
\Rightarrow\ \kappa_{1}({\nu})\hfil\lx@intercol\\\ \hfil\hskip 1.4457pt&\ \
\wedge\ \forall{\texttt{x}_{1}}.\ {\kappa_{1}({\texttt{x}_{1}})}\hfil\hskip
<EMAIL_ADDRESS>{\nu=\texttt{x}_{1}}\
\Rightarrow\ \kappa_{2}({\nu})\hfil\lx@intercol\\\ \hfil\hskip
1.4457pt&\hfil\hskip 1.4457pt&\ \ \vdots\hfil\hskip 1.4457pt&\\\ \hfil\hskip
1.4457pt&\hfil\hskip 1.4457pt&\ \ \wedge\ \forall{\texttt{x}_{n-1}}.\
{\kappa_{n-1}({\texttt{x}_{n-1}})}\hfil\hskip
1.4457pt&\Rightarrow\forall{\nu}.\ {\nu=\texttt{x}_{n-1}}\ \Rightarrow\
\kappa_{n}({\nu})\\\ \hfil\hskip 1.4457pt&\hfil\hskip 1.4457pt&\hfil\hskip
1.4457pt&\ \ \wedge\ \forall{\texttt{x}_{n}}.\ {\kappa_{n}({\texttt{x}_{n}})}\
\Rightarrow\forall{\nu}.\ {\nu=\texttt{x}_{n}}\ \Rightarrow\
0\leq\nu\end{array}$

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

$\begin{array}[]{rl}&\forall{\texttt{x}_{0,0}}.\
{0\leq\texttt{x}_{0,0}}\Rightarrow\forall{\nu}.\ {\nu=\texttt{x}_{0,0}}\
\Rightarrow\ \kappa_{1}({\nu})\\\ \wedge&\forall{\texttt{x}_{1,0}}.\
{0\leq\texttt{x}_{1,0}}\Rightarrow\forall{\texttt{x}_{1,1}}.\
{\kappa_{1}({\texttt{x}_{1,1}})}\Rightarrow\forall{\nu}.\
{\nu=\texttt{x}_{1,1}}\ \Rightarrow\ \kappa_{2}({\nu})\\\ \vdots&\\\
\wedge&\forall{\texttt{x}_{n-1,0}}.\
{0\leq\texttt{x}_{n-1,0}}\Rightarrow\ldots\Rightarrow\forall{\texttt{x}_{n-1,n-1}}.\
{\kappa_{n-1}({\texttt{x}_{n-1,n-1}})}\Rightarrow\forall{\nu}.\
{\nu=\texttt{x}_{n-1,n-1}}\ \Rightarrow\ \kappa_{n}({\nu})\\\
\wedge&\forall{\texttt{x}_{n,0}}.\
{0\leq\texttt{x}_{n,0}}\Rightarrow\ldots\Rightarrow\forall{\texttt{x}_{n,n-1}}.\
{\kappa_{n-1}({\texttt{x}_{n,n-1}})}\Rightarrow\forall{\texttt{x}_{n,n}}.\
{\kappa_{n}({\texttt{x}_{n,n}})}\ \Rightarrow\forall{\nu}.\
{\nu=\texttt{x}_{n,n}}\ \Rightarrow\ 0\leq\nu\end{array}$

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

Values | $v$ | $::=$ | $\mathsf{c}$ | constants
---|---|---|---|---
|  | $\ \mid$ | $\lambda{x}\\!:\\!{\tau}.{e}$ | function
Terms | $e$ | $::=$ | $v$ | values
|  | $\ \mid$ | $x,y,z,\ldots$ | variables
|  | $\ \mid$ | $\texttt{let}\;x=e\;\texttt{in}\;e^{\prime}$ | let-bind
|  | $\ \mid$ | ${e}\;{x}$ | application
|  | $\ \mid$ | $\Lambda{\alpha}.{e}$ | type-abstraction
|  | $\ \mid$ | $[e]\;{\tau}$ | type instantiation
Refinements | $r$ | $::=$ | $\dots\text{varies}\dots$ |
Basic Types | $b$ | $::=$ | $\texttt{{Int}}\ \mid\ \texttt{Bool}\ \mid\dots$ |
Types | $t$ | $::=$ | $\alpha$ | variable
|  | $\ \mid$ | ${{\\{{x}\\!:\\!{b}\mid r\\}}}$ | base
|  | $\ \mid$ | ${{x}\\!:\\!{t}}\rightarrow{t}$ | function
|  | $\ \mid$ | $\forall{\alpha}.{t}$ | scheme
Unrefined Types | $\tau$ | $::=$ | $\alpha$ | variable
|  | $\ \mid$ | $b$ | base
|  | $\ \mid$ | ${{x}\\!:\\!{\tau}}\rightarrow{\tau}$ | function
|  | $\ \mid$ | $\forall{\alpha}.{\tau}$ | scheme
Figure 4. Syntax of $\lambda^{R}$

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:

$\displaystyle\mathsf{prim}(\texttt{7})$ $\displaystyle\ \doteq\
{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu=\texttt{7}\\}}}$
$\displaystyle\mathsf{prim}(\texttt{+})$ $\displaystyle\ \doteq\
{{x}\\!:\\!{\texttt{{Int}}}}\rightarrow{{{y}\\!:\\!{\texttt{{Int}}}}\rightarrow{{\\{\nu\mid\nu=x+y\\}}}}$
$\displaystyle\mathsf{prim}(\texttt{/})$ $\displaystyle\ \doteq\
\texttt{{Int}}\rightarrow{{\\{{\nu}\\!:\\!{\texttt{{Int}}}\mid\nu\not=\texttt{0}\\}}}\rightarrow\texttt{{Int}}$
$\displaystyle\mathsf{prim}(\texttt{assert})$ $\displaystyle\ \doteq\
{{\\{{\nu}\\!:\\!{\texttt{Bool}}\mid\nu\\}}}\rightarrow\texttt{{Unit}}$

###  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

Constraint Syntaxc

Predicates | $p$ | $::=$ | $r$
---|---|---|---
|  | $\ \mid$ | $\kappa({\overline{y}})$
|  | $\ \mid$ | $p_{1}\wedge p_{2}$
Constraints | $c$ | $::=$ | $p$
|  | $\ \mid$ | $c_{1}\wedge c_{2}$
|  | $\ \mid$ | $\forall{{x}\\!:\\!{b}}.\ {p}\Rightarrow{c}$
Environments | $\mathrm{\Gamma}$ | $::=$ | $\emptyset\ \mid\ \mathrm{\Gamma};{x}\\!:\\!{t}$
Assignment | $\sigma$ | $::=$ | $K\rightarrow R$
Assumption | $G$ | $::=$ | $\sigma\ \mid\ G,{{\\{{x}\\!:\\!{b}\mid p\\}}}$

$\textrm{{Well-formedness}}\hfill\framebox{$\mathrm{\Gamma}\vdash c$}$

$\begin{array}[]{lll}{\vbox{\hbox{\hbox{\small\small{{W-Ref}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
22.81134pt\vbox{\hbox{\hskip-22.81133pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
r:\texttt{Bool}$}}}\vbox{}}}\over\hbox{\hskip
9.96411pt\vbox{\vbox{}\hbox{\hskip-9.9641pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
r$}}}}}}$}}}&{\vbox{\hbox{\hbox{\small\small{{W-And}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
27.26642pt\vbox{\hbox{\hskip-27.2664pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
c_{1}\quad\mathrm{\Gamma}\vdash c_{2}$}}}\vbox{}}}\over\hbox{\hskip
19.14142pt\vbox{\vbox{}\hbox{\hskip-19.1414pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
c_{1}\wedge
c_{2}$}}}}}}$}}}&{\vbox{\hbox{\hbox{\small\small{{W-Imp}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
42.48198pt\vbox{\hbox{\hskip-42.48198pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{x}\\!:\\!{b}\vdash
c\quad\mathrm{\Gamma};{x}\\!:\\!{b}\vdash r$}}}\vbox{}}}\over\hbox{\hskip
32.13133pt\vbox{\vbox{}\hbox{\hskip-32.13132pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\forall{{x}\\!:\\!{b}}.\
{r}\Rightarrow{c}$}}}}}}$}}}\end{array}$

$\textrm{{Satisfaction}}\hfill\framebox{$G\models c$}$

$\begin{array}[]{lll}{\vbox{\hbox{\hbox{\small\small{{Sat-
Base}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
55.18062pt\vbox{\hbox{\hskip-55.1806pt\hbox{\hbox{$\displaystyle\displaystyle\emptyset\vdash\sigma(c)\quad\mathsf{SmtValid}(\sigma(c))$}}}\vbox{}}}\over\hbox{\hskip
10.1597pt\vbox{\vbox{}\hbox{\hskip-10.1597pt\hbox{\hbox{$\displaystyle\displaystyle\sigma\models
c$}}}}}}$}}}&{\vbox{\hbox{\hbox{\small\small{{Sat-
Ext}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
35.1418pt\vbox{\hbox{\hskip-35.1418pt\hbox{\hbox{$\displaystyle\displaystyle
G\models\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c}$}}}\vbox{}}}\over\hbox{\hskip
29.86406pt\vbox{\vbox{}\hbox{\hskip-29.86404pt\hbox{\hbox{$\displaystyle\displaystyle
G,{{\\{{x}\\!:\\!{b}\mid p\\}}}\models
c$}}}}}}$}}}&{\vbox{\hbox{\hbox{\small\small{{Sat-
Many}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
46.25238pt\vbox{\hbox{\hskip-46.25238pt\hbox{\hbox{$\displaystyle\displaystyle
G\models c\ \mbox{for each}\ c\in{cs}$}}}\vbox{}}}\over\hbox{\hskip
13.57764pt\vbox{\vbox{}\hbox{\hskip-13.57762pt\hbox{\hbox{$\displaystyle\displaystyle
G\models{cs}$}}}}}}$}}}\end{array}$

Figure 5. Constraints: Syntax and Semantics

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:

$\begin{array}[]{lcl}\sigma(\kappa({\overline{y}}))&\doteq&{\sigma(\kappa)}\left[\overline{y}/\overline{x}\right]\quad\mbox{where
$\overline{x}=\mathsf{params}(\kappa)$}\\\ \sigma(r)&\doteq&r\\\
\sigma(p\wedge p^{\prime})&\doteq&\sigma(p)\wedge\sigma(p^{\prime})\\\
\sigma(\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c})&\doteq&\forall{{x}\\!:\\!{b}}.\
{\sigma(p)}\Rightarrow{\sigma(c)}\\\ \sigma(c_{1}\wedge
c_{2})&\doteq&\sigma(c_{1})\wedge\sigma(c_{2})\\\
\sigma(C)&\doteq&\\{\sigma(c)\ \mid\ c\in C\\}\end{array}$

_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:

$(\sigma\\!\cdot\\!\sigma^{\prime})(\kappa)\ \doteq\
\sigma(\sigma^{\prime}(\kappa))$

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:

$\forall{{x_{1}}\\!:\\!{b_{1}}}.\
{p_{1}}\Rightarrow{\ldots\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
\forall{{x_{n}}\\!:\\!{b_{n}}}.\ {p_{n}}\Rightarrow{p}}$

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_ :

(of a _solution_ $\sigma$) $\displaystyle\mathsf{deps}(\sigma)$
$\displaystyle\doteq\\{(\kappa,\kappa^{\prime})\ \mid\
\kappa\in\sigma(\kappa^{\prime})\\}$ (of a _flat constraint_ $c$)
$\displaystyle\mathsf{deps}(c)$
$\displaystyle\doteq\\{(\kappa,\kappa^{\prime})\ \mid\
\kappa\in\mathsf{body}(c),\kappa^{\prime}\in\mathsf{head}(c)\\}$ (of an _NNF
constraint_ $c$) $\displaystyle\mathsf{deps}(c)$
$\displaystyle\doteq\cup_{c^{\prime}\in\mathsf{flat}(c)}\mathsf{deps}(c^{\prime})$
(of a constraint _excluding_ $\hat{K}$) $\displaystyle\mathsf{deps}(\hat{K},\
c)$
$\displaystyle\doteq\mathsf{deps}(c)\setminus(K\times\hat{K}\cup\hat{K}\times
K)$

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$:

(definitions) $\displaystyle c\\!\downarrow\\!\kappa$ $\displaystyle\doteq\
\\{c^{\prime}\mid c^{\prime}\in\mathsf{flat}(c),\
\kappa\in\mathsf{head}(c^{\prime})\\}$ (uses) $\displaystyle
c\\!\uparrow\\!\kappa$ $\displaystyle\doteq\ \\{c^{\prime}\mid
c^{\prime}\in\mathsf{flat}(c),\ \kappa\not\in\mathsf{head}(c^{\prime})\\}$

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$.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{fresh}&:&(\mathrm{\Gamma}\times
T)\rightarrow\hat{T}\\\
\hline\cr\mathsf{fresh}([{y_{1}}\\!:\\!{\tau_{1}},\ldots],\
b)&\doteq&{{\\{{\nu}\\!:\\!{b}\mid\kappa({y_{1},\ldots,\nu})\\}}}\\\
\quad\mbox{where}&&\\\ \quad\quad\kappa&=&\mbox{fresh $K$ variable}\\\
\quad\quad\mbox{s.t.}\
\mathsf{params}(\kappa)&=&[{z_{1}}\\!:\\!{\tau_{1}},\ldots,{z}\\!:\\!{b}]\\\\[3.61371pt]
\mathsf{fresh}(\mathrm{\Gamma},\
{{x}\\!:\\!{\tau}}\rightarrow{\tau^{\prime}})&\doteq&{{x}\\!:\\!{t}}\rightarrow{t^{\prime}}\\\
\quad\mbox{where}&&\\\ \quad\quad t&=&\mathsf{fresh}(\mathrm{\Gamma},\
\tau)\\\ \quad\quad
t^{\prime}&=&\mathsf{fresh}(\mathrm{\Gamma};{x}\\!:\\!{\tau},\
\tau^{\prime})\\\\[3.61371pt] \mathsf{fresh}(\mathrm{\Gamma},\
\alpha)&\doteq&\alpha\\\\[3.61371pt] \mathsf{fresh}(\mathrm{\Gamma},\
\forall{\alpha}.{\tau})&\doteq&\forall{\alpha}.{\mathsf{fresh}(\mathrm{\Gamma},\
\tau)}\\\\[7.22743pt] \hline\cr\hline\cr\end{array}$ Figure 6. Fresh
Templates: $\hat{T}$ denotes _templates_ , i.e. types with $\kappa$-variables
representing unknown refinements.
$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{sub}&:&(T\times T)\rightarrow
C\\\ \hline\cr{\mathsf{sub}({{\\{{x}\\!:\\!{b}\mid p\\}}},\
{{\\{{y}\\!:\\!{b}\mid q\\}}})}&\doteq&\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{{q}\left[x/y\right]}\\\\[3.61371pt]
{\mathsf{sub}({{x}\\!:\\!{s}}\rightarrow{s^{\prime}},\
{{y}\\!:\\!{t}}\rightarrow{t^{\prime}})}&\doteq&c\wedge(({{y::t}})\Rightarrow
c^{\prime})\\\ \quad\mbox{where}&&\\\ \quad\quad c&=&\mathsf{sub}(t,\ s)\\\
\quad\quad c^{\prime}&=&\mathsf{sub}({s^{\prime}}\left[y/x\right],\
t^{\prime})\\\\[3.61371pt] {\mathsf{sub}(\alpha,\
\alpha)}&\doteq&\mathit{true}\\\\[3.61371pt]
{\mathsf{sub}(\forall{\alpha}.{t},\
\forall{\alpha}.{t^{\prime}})}&\doteq&\mathsf{sub}(t,\
t^{\prime})\\\\[3.61371pt] \hline\cr\hline\cr\end{array}$ Figure 7. Subtyping
Constraints

_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:

$\begin{array}[]{lcl}({{x::{{\\{{y}\\!:\\!{b}\mid p\\}}}}})\Rightarrow
c&\doteq&\forall{{x}\\!:\\!{b}}.\ {{p}\left[x/y\right]}\Rightarrow{c}\\\
({{x::t}})\Rightarrow c&\doteq&c\\\ \end{array}$

_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.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{cgen}&:&(\mathrm{\Gamma}\times
E)\rightarrow(C\times T)\\\ \hline\cr\mathsf{cgen}(\mathrm{\Gamma},\
\mathsf{c})&\doteq&(\mathit{true},\ \mathsf{prim}(\mathsf{c}))\\\\[3.61371pt]
\mathsf{cgen}(\mathrm{\Gamma},\ x)&\doteq&(\mathit{true},\
\mathsf{single}(\mathrm{\Gamma},\ x))\\\\[3.61371pt]
\mathsf{cgen}(\mathrm{\Gamma},\
\texttt{let}\;x=e_{1}\;\texttt{in}\;e_{2})&\doteq&(c\wedge\mathsf{sub}(t_{2},\
\hat{t}),\ \hat{t})\\\ \quad\mbox{where}&&\\\ \quad\quad
c&=&c_{1}\wedge(({{x::t_{1}}})\Rightarrow c_{2})\\\
\quad\quad\hat{t}&=&\mathsf{fresh}(\emptyset,\ \mathsf{shape}(t_{2}))\\\
\quad\quad(c_{1},t_{1})&=&\mathsf{cgen}(\mathrm{\Gamma},\ e_{1})\\\
\quad\quad(c_{2},t_{2})&=&\mathsf{cgen}(\mathrm{\Gamma};{x}\\!:\\!{t_{1}},\
e_{2})\\\\[3.61371pt] \mathsf{cgen}(\mathrm{\Gamma},\
\lambda{x}\\!:\\!{\tau}.{e})&\doteq&(c,{{x}\\!:\\!{\hat{t}}}\rightarrow{t})\\\
\quad\mbox{where}&&\\\
\quad\quad(c,t)&=&\mathsf{cgen}(\mathrm{\Gamma};{x}\\!:\\!{\hat{t}},\ e)\\\
\quad\quad\hat{t}&=&\mathsf{fresh}(\emptyset,\ \tau)\\\\[3.61371pt]
\mathsf{cgen}(\mathrm{\Gamma},\ {e}\;{y})&\doteq&(c\wedge
c_{y},{t^{\prime}}\left[y/x\right])\\\ \quad\mbox{where}&&\\\ \quad\quad
c_{y}&=&\mathsf{sub}(\mathsf{single}(\mathrm{\Gamma},\ y),\ t)\\\
\quad\quad(c,{{x}\\!:\\!{t}}\rightarrow{t^{\prime}})&=&\mathsf{cgen}(\mathrm{\Gamma},\
e)\\\\[3.61371pt] \mathsf{cgen}(\mathrm{\Gamma},\
\Lambda{\alpha}.{e})&\doteq&(c,\forall{\alpha}.{t})\\\ \quad\mbox{where}&&\\\
\quad\quad(c,t)&=&\mathsf{cgen}(\mathrm{\Gamma};\alpha,\ e)\\\\[3.61371pt]
\mathsf{cgen}(\mathrm{\Gamma},\
e[\tau])&\doteq&(c,{t}\left[\hat{t}/\alpha\right])\\\ \quad\mbox{where}&&\\\
\quad\quad(c,\forall{\alpha}.{t})&=&\mathsf{cgen}(\mathrm{\Gamma},\
e)\\\\[3.61371pt] \quad\quad\hat{t}&=&\mathsf{fresh}(\emptyset,\
\tau)\\\\[7.22743pt]
\hline\cr\hline\cr\mathsf{single}&:&(\mathrm{\Gamma}\times X)\rightarrow T\\\
\hline\cr\mathsf{single}(\mathrm{\Gamma},\ x)&&\\\ \quad\ \mid\
t={{\\{{x}\\!:\\!{b}\mid
p\\}}}&\doteq&{{\\{{\nu}\\!:\\!{b}\mid{p}\left[\nu/x\right]\wedge\nu=x\\}}}\\\
\quad\ \mid\ \mbox{otherwise}&\doteq&t\\\ \quad\mbox{where}\
t&=&\mathrm{\Gamma}(x)\\\\[7.22743pt] \hline\cr\hline\cr\end{array}$ Figure 8.
Constraint Generation

##  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

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{scope}&:&(K\times C)\rightarrow
C\\\ \hline\cr\mathsf{scope}(\kappa,c_{1}\wedge c_{2})&&\\\ \quad\ \mid\
\kappa\in c_{1},\kappa\not\in c_{2}&\doteq&\mathsf{scope}(\kappa,c_{1})\\\
\quad\ \mid\ \kappa\not\in c_{1},\kappa\in
c_{2}&\doteq&\mathsf{scope}(\kappa,c_{2})\\\\[3.61371pt]
\mathsf{scope}(\kappa,\forall{{x}\\!:\\!{b}}.\ {p}\Rightarrow{c^{\prime}})\\\
\quad\ \mid\ \kappa\not\in p&\doteq&\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{\mathsf{scope}(\kappa,c^{\prime})}\\\\[3.61371pt]
\mathsf{scope}(\kappa,c)&\doteq&c\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 9. The scope of a $\kappa$ in constraint
$c$.

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

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{sol1}&:&(K\times C)\rightarrow
P\\\ \hline\cr\mathsf{sol1}(\kappa,c_{1}\wedge
c_{2})&\doteq&\mathsf{sol1}(\kappa,c_{1})\vee\mathsf{sol1}(\kappa,c_{2})\\\\[3.61371pt]
\mathsf{sol1}(\kappa,\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c})&\doteq&\exists{x}\\!:\\!{b}.\
{p\wedge\mathsf{sol1}(\kappa,c)}\\\\[3.61371pt]
\mathsf{sol1}(\kappa,\kappa({\overline{y}}))&\doteq&\bigwedge_{i}x_{i}=y_{i}\quad\mbox{where}\
\overline{x}=\mathsf{params}(\kappa)\\\\[3.61371pt]
\mathsf{sol1}(\kappa,p)&\doteq&\mathit{false}\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 10. The Strongest Solution for a
$\kappa$-Variable.

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:

$\displaystyle\sigma^{c}_{\kappa}\ $ $\displaystyle\doteq\
[\kappa\mapsto\lambda\overline{x}.\mathsf{sol1}(\kappa,c)]$
$\displaystyle\hat{\sigma}^{c}_{\kappa}\ $ $\displaystyle\doteq\
[\kappa\mapsto\lambda\overline{x}.\mathsf{sol1}(\kappa,c^{\prime})]\
\mbox{where}\
\mathsf{scope}(\kappa,c)\equiv\forall(\overline{{{x_{i}}\\!:\\!{p_{i}}}})\Rightarrow
c^{\prime}\mbox{s.t.}\ \kappa\not\in p_{i}$

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})$:

$\begin{array}[]{rclrcl}c_{1}&\doteq&\kappa(a)&\qquad\mathsf{sol1}(\kappa,c_{1})&\doteq&x=a\\\
c_{2}&\doteq&\kappa(b)&\qquad\mathsf{sol1}(\kappa,c_{2})&\doteq&x=b\\\
c_{3}&\doteq&c_{1}\wedge
c_{2}&\qquad\mathsf{sol1}(\kappa,c_{3})&\doteq&x=a\vee x=b\\\
c_{4}&\doteq&\forall{b}.\ {q\
b}\Rightarrow{c_{4}}&\qquad\mathsf{sol1}(\kappa,c_{4})&\doteq&\exists{b}.\ {q\
b\wedge(x=a\vee x=b)}\\\ c_{5}&\doteq&\forall{a}.\ {p\
a}\Rightarrow{c_{4}}&\qquad\mathsf{sol1}(\kappa,c_{5})&\doteq&\exists{a}.\ {p\
a\wedge(\exists{b}.\ {q\ b\wedge(x=a\vee x=b)})}\end{array}$

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

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{elim1}&:&(K\times C)\rightarrow
C\\\
\hline\cr\mathsf{elim1}(\kappa,c)&\doteq&\mathsf{elim^{*}}(\hat{\sigma}^{c}_{\kappa},c)\\\
\quad\mbox{where}&&\\\
\quad\quad\hat{\sigma}^{c}_{\kappa}&=&[\kappa\mapsto\lambda\overline{x}.\mathsf{sol1}(\kappa,c^{\prime})]\\\
\quad\quad\forall(\overline{{{x_{i}}\\!:\\!{p_{i}}}})\Rightarrow
c^{\prime}&=&\mathsf{scope}(\kappa,c)\\\
\quad\quad\overline{x}&=&\mathsf{params}(\kappa)\\\\[3.61371pt]
\hline\cr\hline\cr\mathsf{elim^{*}}&:&(\Sigma\times C)\rightarrow C\\\
\hline\cr\mathsf{elim^{*}}(\sigma,c_{1}\wedge
c_{2})&\doteq&\mathsf{elim^{*}}(\sigma,c_{1})\wedge\mathsf{elim^{*}}(\sigma,c_{2})\\\\[3.61371pt]
\mathsf{elim^{*}}(\sigma,\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c})&\doteq&\forall{{x}\\!:\\!{b}}.\
{\sigma(p)}\Rightarrow{\mathsf{elim^{*}}(\sigma,c)}\\\\[3.61371pt]
\mathsf{elim^{*}}(\sigma,\kappa({\overline{y}}))&&\\\\[3.61371pt] \quad\ \mid\
\kappa\in\mathsf{domain}(\sigma)&\doteq&\mathit{true}\\\\[3.61371pt]
\mathsf{elim^{*}}(\sigma,p)&\doteq&p\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 11. Eliminating Variables.

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$:

$\displaystyle c_{1}$ $\displaystyle\doteq c$ $\displaystyle c_{i+1}$
$\displaystyle\doteq\mathsf{elim1}(\kappa_{i},c_{i})\quad\mbox{for}\quad i\in
1,\ldots,n$ At each step, the strongest solution for $\kappa_{i}$ is computed
from $\mathsf{scope}(\kappa,c_{i})$, i.e. the part of the constraint derived
from the subterm where the binder $\texttt{x}_{i}$ is in scope. Thus, for each
$i\in 1,\ldots,n$ we get solutions (15)
$\displaystyle\mathsf{sol1}(\kappa_{i},c_{i})$
$\displaystyle\doteq\exists\nu.\ \nu=\texttt{x}_{i-1}\wedge z=\nu$ where
$\mathsf{params}(\kappa_{i})=z$. For brevity of exposition, we simplify the
above to $\displaystyle\mathsf{sol1}(\kappa_{i},c_{i})$ $\displaystyle\doteq
z=\texttt{x}_{i-1}$ and hence, note that
$\mathsf{elim}([\kappa_{1},\ldots,\kappa_{n}],c,$) yields the linear-sized VC
$\displaystyle c_{n+1}$ $\displaystyle\doteq\forall{\texttt{x}_{0}}.\
{0\leq\texttt{x}_{0}}\Rightarrow{\forall{\texttt{x}_{1}}.\
{\texttt{x}_{1}=\texttt{x}_{0}}\Rightarrow{\ldots\Rightarrow\forall{\texttt{x}_{n}}.\
{\texttt{x}_{n}=\texttt{x}_{n-1}}\Rightarrow{\forall{\nu}.\
{\nu=\texttt{x}_{n}}\Rightarrow{0\leq\nu}}}}$

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.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{sat}&:&(C\times
2^{R})\rightarrow\\{\textsc{True},\textsc{False}\\}\\\
\hline\cr\mathsf{sat}(c,\mathbb{Q})&\doteq&\mathsf{solve}({cs},\mathbb{Q})\\\
\quad\mbox{where}&&\\\ \quad\quad c^{\prime}&=&\mathsf{elim}(\hat{K},c)\
\mbox{where $\hat{K}$ cuts $c$}\\\
\quad\quad{cs}&=&\mathsf{flat}(c^{\prime})\\\\[7.22743pt]
\hline\cr\hline\cr\mathsf{flat}&:&C\rightarrow 2^{C}\\\
\hline\cr\mathsf{flat}(\mathit{true})&\doteq&\emptyset\\\\[3.61371pt]
\mathsf{flat}(p)&\doteq&\\{p\\}\\\\[3.61371pt] \mathsf{flat}(c\wedge
c^{\prime})&\doteq&\mathsf{flat}(c)\cup\mathsf{flat}(c^{\prime})\\\\[3.61371pt]
\mathsf{flat}(\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c})&\doteq&\\{\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c^{\prime}}\ \mid\
c^{\prime}\in\mathsf{flat}(c)\\}\\\\[7.22743pt]
\hline\cr\hline\cr\mathsf{elim}&:&(2^{K}\times C)\rightarrow C\\\
\hline\cr\mathsf{elim}([],c)&\doteq&c\\\\[3.61371pt]
\mathsf{elim}(\kappa:\kappa s,c)&\doteq&\mathsf{elim}(\kappa
s,\mathsf{elim1}(\kappa,c))\\\\[3.61371pt] \hline\cr\hline\cr\end{array}$
Figure 12. Checking Constraint Satisfaction

_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.

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

##  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.

## References

  * (1)
  * Barrett et al. (2016) C. Barrett, P. Fontaine, and C. Tinelli. 2016.  The Satisfiability Modulo Theories Library (SMT-LIB).  www.SMT-LIB.org. (2016).
  * Bengtson et al. (2008) J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Maffeis. 2008.  Refinement Types for Secure Implementations. In CSF.
  * Beyer et al. (2009) Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. 2009\.  Software model checking via large-block encoding. In FMCAD.
  * Bjørner et al. (2015) Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko. 2015.  Horn Clause Solvers for Program Verification. In Fields of Logic and Computation.
  * Burstall and Darlington (1977) Rod M. Burstall and John Darlington. 1977.  A Transformation System for Developing Recursive Programs.  J. ACM 24, 1 (1977), 44–67.
  * Casinghino et al. (2014) Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014\.  Combining Proofs and Programs in a Dependently Typed Language. In POPL.
  * Constable (1986) R.L. Constable. 1986\.  Implementing Mathematics with the Nuprl Proof Development System.  Prentice-Hall.
  * Dunfield (2007) J. Dunfield. 2007\.  Refined typechecking with Stardust. In PLPV.
  * Ernst et al. (2001) M.D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. 2001\.  Dynamically Discovering Likely Program Invariants to Support Program Evolution.  IEEE TSE 27(2) (2001), 1–25.
  * Flanagan et al. (2001) C. Flanagan, R. Joshi, and K. R. M. Leino. 2001.  Annotation inference for modular checkers.  Inform. Process. Lett. (2001).
  * Flanagan et al. (2002) C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. 2002\.  Extended static checking for Java. In PLDI.
  * Flanagan and Saxe (2000) C. Flanagan and J.B. Saxe. 2000.  Avoiding exponential explosion: generating compact verification conditions. In POPL.
  * Godefroid and Yannakakis (2013) Patrice Godefroid and Mihalis Yannakakis. 2013.  Analysis of Boolean Programs. In TACAS.
  * Graf and Saïdi (1997) S. Graf and H. Saïdi. 1997.  Construction of abstract state graphs with PVS.  In CAV. Springer, 72–83.
  * Grebenshchikov et al. (2012) Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. 2012.  Synthesizing software verifiers from proof rules. In PLDI.
  * Hashimoto and Unno (2015) Kodai Hashimoto and Hiroshi Unno. 2015.  Refinement Type Inference via Horn Constraint Optimization. In Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings. 199–216.  https://doi.org/10.1007/978-3-662-48288-9_12
  * Hinze (2009) Ralf Hinze. 2009\.  Functional pearl: la tour d’Hanoï. In ICFP.
  * Hoder and Bjørner (2012) Kryštof Hoder and Nikolaj Bjørner. 2012.  Generalized Property Directed Reachability. In SAT.
  * Jhala et al. (2011) Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko. 2011\.  HMC: Verifying Functional Programs Using Abstract Interpreters. In CAV.  https://doi.org/10.1007/978-3-642-22110-1_38
  * Jhala and McMillan (2006) R. Jhala and K.L. McMillan. 2006.  A Practical and Complete Approach to Predicate Refinement. In TACAS 06.
  * Karp (1972) Richard M. Karp. 1972\.  Reducibility Among Combinatorial Problems. In Proceedings of a symposium on the Complexity of Computer Computations.
  * Kent et al. (2016) Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt. 2016\.  Occurrence typing modulo theories. In PLDI.
  * Knowles and Flanagan (2007) K. Knowles and C. Flanagan. 2007.  Type Reconstruction for General Refinement Types. In ESOP.  http://kenn.frap.net/publications/knowles-flanagan.esop.07.type.pdf
  * Knowles and Flanagan (2010) K.W. Knowles and C. Flanagan. 2010.  Hybrid type checking.  ACM TOPLAS (2010).
  * Knowles and Flanagan (2009) K. W. Knowles and C. Flanagan. 2009.  Compositional reasoning and decidable checking for dependent contract types. In PLPV.
  * Kobayashi et al. (2011) Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. 2011\.  Predicate abstraction and CEGAR for higher-order model checking. In PLDI.
  * Komuravelli et al. (2016) Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2016\.  SMT-based model checking for recursive programs.  Formal Methods in System Design 48, 3 (2016), 175–205.  https://doi.org/10.1007/s10703-016-0249-4
  * Leino (2005) K. Rustan M. Leino. 2005\.  Efficient weakest preconditions.  Inf. Process. Lett. 93, 6 (2005).
  * Nelson (1981) G. Nelson. 1981\.  Techniques for program verification.  Technical Report CSL81-10. Xerox Palo Alto Research Center.
  * Odersky et al. (2001) Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001\.  Colored local type inference. In POPL.
  * Ou et al. (2004) X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. 2004\.  Dynamic Typing with Dependent Types. In IFIP TCS.
  * Pettorossi and Proietti (1994) Alberto Pettorossi and Maurizio Proietti. 1994.  Transformation of logic programs: Foundations and techniques.  The Journal of Logic Programming 19 (1994), 261 – 320.
  * Pierce and Turner (1998) B. C. Pierce and D. N. Turner. 1998.  Local Type Inference. In POPL.
  * Polikarpova et al. (2016) Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016\.  Program synthesis from polymorphic refinement types. In PLDI.
  * Rondon et al. (2008) P. Rondon, M. Kawaguchi, and R. Jhala. 2008.  Liquid Types. In PLDI.
  * Rümmer et al. (2015) Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak. 2015\.  On recursion-free Horn clauses and Craig interpolation.  Formal Methods in System Design 47, 1 (2015), 1–25.
  * Rushby et al. (1998) J. Rushby, S. Owre, and N. Shankar. 1998.  Subtypes for Specifications: Predicate Subtyping in PVS.  IEEE TSE (1998).
  * Sjöberg and Weirich (2015) Vilhelm Sjöberg and Stephanie Weirich. 2015.  Programming up to Congruence. In POPL.
  * Swamy et al. (2011) N. Swamy, J. Chen, C. Fournet, P-Y. Strub, K. Bhargavan, and J. Yang. 2011\.  Secure distributed programming with value-dependent types. In ICFP.
  * Swamy et al. (2013) N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. 2013.  Verifying Higher-order Programs with the Dijkstra Monad. In PLDI.
  * Tamaki and Sato (1984) Hisao Tamaki and Taisuke Sato. 1984.  Unfold/Fold Transformation of Logic Programs. In Proceedings of the Second International Logic Programming Conference, Uppsala University, Uppsala, Sweden, July 2-6, 1984. 127–138.
  * Unno et al. (2013) H. Unno, T. Terauchi, and N. Kobayashi. 2013.  Relatively complete verification of higher-order functional programs. In POPL.
  * Vazou and Jhala (2016) N. Vazou and R. Jhala. 2016.  Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT).  ArXiv e-prints (Oct. 2016).  arXiv:cs.PL/1610.04641
  * Vazou et al. (2014a) N. Vazou, E. L. Seidel, and R. Jhala. 2014a.  LiquidHaskell: Experience with refinement types in the real world. In Haskell.
  * Vazou et al. (2014b) N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. Peyton Jones. 2014b.  Refinement Types for Haskell. In ICFP.
  * Vekris et al. (2016) Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. 2016\.  Refinement types for TypeScript. In PLDI.
  * Xi and Pfenning (1998) H. Xi and F. Pfenning. 1998\.  Eliminating Array Bound Checking Through Dependent Types.. In PLDI.
  * Zhu et al. (2015) He Zhu, Aditya V. Nori, and Suresh Jagannathan. 2015.  Learning refinement types. In ICFP.

##  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$.

 _Case: $c\equiv\kappa({\overline{y}})$._ (17) By definition of
$\mathsf{sol1}(c,\kappa)$
$\displaystyle\sigma^{c}_{\kappa}(\kappa({\overline{z}}))$
$\displaystyle=\overline{z}=\overline{y}$ Assume
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\kappa({\overline{y}})$ Hence
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\overline{z}=\overline{y}\Rightarrow\kappa({\overline{z}})$
By 17 $\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\sigma^{c}_{\kappa}(\kappa({\overline{z}}))\Rightarrow\kappa({\overline{z}})$
_Case: $c\equiv p^{\prime}$, such that $\kappa\not\in p^{\prime}$._ By
definition of validity
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\mathit{false}\Rightarrow\kappa({\overline{z}})$ By the
definition of $\mathsf{sol1}(c,\kappa)$
$\displaystyle\sigma^{c}_{\kappa}(\kappa({\overline{z}}))$
$\displaystyle=\mathit{false}$ Hence,
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\sigma^{c}_{\kappa}(\kappa({\overline{z}}))\Rightarrow\kappa({\overline{z}})$
_Case: $c\equiv c_{1}\wedge c_{2}$._ Let $p_{j}=\mathsf{sol1}(c_{j},\kappa)$
for $j=1,2$ (18) Thus, by the definition of $\mathsf{sol1}(c,\kappa)$
$\displaystyle\sigma^{c}_{\kappa}(\kappa({\overline{z}}))$
$\displaystyle=p_{1}\vee p_{2}$ Assume, for $j=1,2$
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\wedge_{j}c_{j}$ That is, for $j=1,2$
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$ $\displaystyle\models
c_{j}$ By IH, for $j=1,2$
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$ $\displaystyle\models
p_{j}\Rightarrow\kappa({\overline{z}})$ Hence,
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models(p_{1}\vee p_{2})\Rightarrow\kappa({\overline{z}})$ Thus,
by 18, $\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\sigma^{c}_{\kappa}(\kappa({\overline{z}}))\Rightarrow\kappa({\overline{z}})$
_Case: $c\equiv\forall{{x}\\!:\\!{b}}.\ {p}\Rightarrow{c^{\prime}}$._ Let
$p^{\prime}=\mathsf{sol1}(c^{\prime},\kappa)$. (19) Thus, by the definition of
$\mathsf{sol1}(c,\kappa)$
$\displaystyle\sigma^{c^{\prime}}_{\kappa}(\kappa({\overline{z}}))$
$\displaystyle=p^{\prime}$ (20)
$\displaystyle\sigma^{c}_{\kappa}(\kappa({\overline{z}}))$
$\displaystyle=\exists{x}\\!:\\!{b}.\ {p\wedge p^{\prime}}$ Assume
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\forall{{x}\\!:\\!{b}}.\ {p}\Rightarrow{c^{\prime}}$ By
Sat-Ext
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}},{{x}\\!:\\!{p}}$
$\displaystyle\models c^{\prime}$ By IH
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}},{{x}\\!:\\!{p}}$
$\displaystyle\models\sigma^{c^{\prime}}_{\kappa}(\kappa({\overline{z}}))\Rightarrow\kappa({\overline{z}})$
By 19 $\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}},{{x}\\!:\\!{p}}$
$\displaystyle\models p^{\prime}\Rightarrow\kappa({\overline{z}})$ By Sat-Ext
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{p^{\prime}\Rightarrow\kappa({\overline{z}})}$ That is,
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\forall{{x}\\!:\\!{b}}.\ {(p\wedge
p^{\prime}}\Rightarrow{\kappa({\overline{z}}))}$ As
$x\not\in\kappa({\overline{z}})$
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models(\exists{x}\\!:\\!{b}.\ {p\wedge
p^{\prime}})\Rightarrow\kappa({\overline{z}})$ By 20
$\displaystyle\sigma,\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\sigma^{c}_{\kappa}(\kappa({\overline{z}}))\Rightarrow\kappa({\overline{z}})$

∎

###### Proof.

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

 _Case: $c\equiv\kappa({\overline{y}})$._ By definition $\displaystyle
c\\!\downarrow\\!\kappa$ $\displaystyle\doteq\kappa({\overline{y}})$ and
$\displaystyle\sigma^{c}_{\kappa}(\kappa)$
$\displaystyle\doteq\lambda\overline{x}.\wedge_{i}x_{i}=y_{i}\quad\mbox{ where
}\overline{x}=\mathsf{params}(\kappa)$ (22) Hence,
$\displaystyle\sigma^{c}_{\kappa}(c\\!\downarrow\\!\kappa)$
$\displaystyle\doteq\wedge_{i}y_{i}=y_{i}$ As 22 is a tautology
$\displaystyle\sigma^{c}_{\kappa}$ $\displaystyle\models
c\\!\downarrow\\!\kappa$  _Case: $c\equiv p$._ By definition $\displaystyle
c\\!\downarrow\\!\kappa$ $\displaystyle\doteq\mathit{true}$ (23) Hence,
$\displaystyle\sigma^{c}_{\kappa}(c\\!\downarrow\\!\kappa)$
$\displaystyle\doteq\mathit{true}$ As 23 is a tautology
$\displaystyle\sigma^{c}_{\kappa}$ $\displaystyle\models
c\\!\downarrow\\!\kappa$  _Case: $c\equiv c_{1}\wedge c_{2}$._ For
$i\in\\{1,2\\}$, let $p_{i}=\mathsf{sol1}(\kappa,c_{i})$,
$\sigma^{c_{i}}_{\kappa}(\kappa)=\lambda\overline{x}.p_{i}$. (24) By
definition $\displaystyle c\\!\downarrow\\!\kappa$ $\displaystyle\doteq
c_{1}\\!\downarrow\\!\kappa\cup c_{2}\\!\downarrow\\!\kappa$ (25) By IH
$\displaystyle\sigma^{c_{i}}_{\kappa}$ $\displaystyle\models
c_{i}\\!\downarrow\\!\kappa$ Let $c^{\prime}\in c_{i}\\!\downarrow\\!\kappa$.
As $\kappa$ _only_ in head,
$c^{\prime}\equiv\forall(\overline{{{y}\\!:\\!{p}}})\Rightarrow\kappa({\overline{x}})$.
By 25 $\displaystyle\overline{{{y}\\!:\\!{p}}}$
$\displaystyle\models\sigma^{c_{i}}_{\kappa}(\kappa({\overline{x}}))$ By Lemma
4.1 $\displaystyle\overline{{{y}\\!:\\!{p}}}$
$\displaystyle\models\sigma^{c_{1}}_{\kappa}(\kappa({\overline{x}}))\vee\sigma^{c_{2}}_{\kappa}(\kappa({\overline{x}}))$
That is $\displaystyle\overline{{{y}\\!:\\!{p}}}$
$\displaystyle\models\sigma^{c}_{\kappa}(\kappa({\overline{x}}))$ So for any
$c^{\prime}\in c_{i}\\!\downarrow\\!\kappa$ $\displaystyle\sigma^{c}_{\kappa}$
$\displaystyle\models c^{\prime}$ Hence $\displaystyle\sigma^{c}_{\kappa}$
$\displaystyle\models c_{i}\\!\downarrow\\!\kappa$ and hence, by 24
$\displaystyle\sigma^{c}_{\kappa}$ $\displaystyle\models
c\\!\downarrow\\!\kappa$  _Case: $c\equiv\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c^{\prime}}$._ Let
$p^{\prime}=\mathsf{sol1}(\kappa,c^{\prime})$,
$\sigma^{\prime}=[\kappa\mapsto\lambda\overline{z}.p^{\prime}]$, and
$\sigma^{c}_{\kappa}=[\kappa\mapsto\lambda\overline{z}.\exists{x}\\!:\\!{b}.\
{p\wedge p^{\prime}}]$, (26) By IH $\displaystyle\sigma^{\prime}$
$\displaystyle\models c^{\prime}\\!\downarrow\\!\kappa$ Consider any arbitrary
$c^{\prime\prime}\in c^{\prime}\\!\downarrow\\!\kappa$. (27) As
$\kappa\in\mathsf{head}(c^{\prime\prime})$ $\displaystyle c^{\prime\prime}$
$\displaystyle\doteq\forall{x_{1}}.\
{p_{1}}\Rightarrow{\ldots\Rightarrow\forall{x_{n}}.\
{p_{n}}\Rightarrow{\kappa({\overline{y}})}}$ By 26
$\displaystyle\sigma^{\prime}$ $\displaystyle\models\forall{x_{1}}.\
{p_{1}}\Rightarrow{\ldots\Rightarrow\forall{x_{n}}.\
{p_{n}}\Rightarrow{\kappa({\overline{y}})}}$ By Sat-Base $\displaystyle[]$
$\displaystyle\models\forall{x_{1}}.\
{p_{1}}\Rightarrow{\ldots\Rightarrow\forall{x_{n}}.\
{p_{n}}\Rightarrow{{p^{\prime}}\left[\overline{y}/\overline{z}\right]}}$ (28)
By Sat-Ext $\displaystyle\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models{p^{\prime}}\left[\overline{y}/\overline{z}\right]$ (29)
Trivially, $\displaystyle{{x}\\!:\\!{p}}$ $\displaystyle\models p$ Hence, by
28, 29 $\displaystyle{{x}\\!:\\!{p}},\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models{p\wedge{p^{\prime}}\left[\overline{y}/\overline{z}\right]}$
and so by definition of validity
$\displaystyle{{x}\\!:\\!{p}},\overline{{{x_{i}}\\!:\\!{p_{i}}}}$
$\displaystyle\models\exists{x}\\!:\\!{b}.\
{p\wedge{p^{\prime}}\left[\overline{y}/\overline{z}\right]}$ by 27
$\displaystyle\sigma^{c}_{\kappa}$
$\displaystyle\models\forall{{x}\\!:\\!{b}}.\
{p}\Rightarrow{c^{\prime\prime}}$

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)

(30) Let $\displaystyle\mathsf{scope}(\kappa,c)$
$\displaystyle\doteq\forall(\overline{{{x}\\!:\\!{p}}})\Rightarrow
c^{\prime}\mbox{s.t. $\kappa\not\in\overline{p}$}$ By definition
$\displaystyle\hat{\sigma}^{c}_{\kappa}$
$\displaystyle=\sigma^{c^{\prime}}_{\kappa}$ By Theorem 5.4
$\displaystyle\hat{\sigma}^{c}_{\kappa}$ $\displaystyle\models
c^{\prime}\\!\downarrow\\!\kappa$ By definition of validity
$\displaystyle\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models\forall(\overline{{{x}\\!:\\!{p}}})\Rightarrow(c^{\prime}\\!\downarrow\\!\kappa)$
By Lemma 4.6 $\displaystyle\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models(\forall(\overline{{{x}\\!:\\!{p}}})\Rightarrow
c^{\prime})\\!\downarrow\\!\kappa$ By (30) and Lemma 5.1
$\displaystyle\hat{\sigma}^{c}_{\kappa}$ $\displaystyle\models
c\\!\downarrow\\!\kappa$

∎

###### 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$.

(31) Let $\displaystyle\mathsf{scope}(\kappa,c)$
$\displaystyle\doteq\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow
c^{\prime}\mbox{s.t. $\kappa\not\in\overline{q}$ and
$\hat{\sigma}^{c}_{\kappa}=\sigma^{c^{\prime}}_{\kappa}$}$ (32) Assume
$\displaystyle\sigma$ $\displaystyle\models c$ (33) By (31), Lemma 5.3
$\displaystyle\sigma$
$\displaystyle\models\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow
c^{\prime}$ (34) By Lemma 5.2, (31) $\displaystyle c\\!\uparrow\\!\kappa$
$\displaystyle=\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow(c^{\prime}\\!\uparrow\\!\kappa)\cup
C\quad\mbox{where $\kappa\not\in C$}$ Hence, by (37) and (39)
$\displaystyle\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models c\\!\uparrow\\!\kappa$  _Case:
$\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}\models\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow(c^{\prime}\\!\uparrow\\!\kappa)$_
(37) (35) By (32,34), Lemma 4.7 $\displaystyle\sigma$
$\displaystyle\models\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow(c^{\prime}\\!\uparrow\\!\kappa)$
(36) Let $c^{\prime\prime}\in c^{\prime}\\!\uparrow\\!\kappa$ s.t.
$\displaystyle c^{\prime\prime}$
$\displaystyle\equiv\forall(\overline{{{x_{i}}\\!:\\!{p_{i}}}})\Rightarrow
p\mbox{ and $\kappa\not\in p$}$ By (35) $\displaystyle\sigma$
$\displaystyle\models\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow\forall(\overline{{{x_{i}}\\!:\\!{p_{i}}}})\Rightarrow
p$ By Sat-Ext $\displaystyle\sigma,\overline{{{y}\\!:\\!{q}}}$
$\displaystyle\models\forall(\overline{{{x_{i}}\\!:\\!{p_{i}}}})\Rightarrow p$
By (33) $\displaystyle\sigma,\overline{{{y}\\!:\\!{q}}}$ $\displaystyle\models
c^{\prime}$ By (31), Lemma 5.7, for $i=1\ldots n$
$\displaystyle\sigma,\overline{{{y}\\!:\\!{q}}}$
$\displaystyle\models\sigma^{c^{\prime}}_{\kappa}(p_{i})\Rightarrow p_{i}$ As
$\hat{\sigma}^{c}_{\kappa}=\sigma^{c^{\prime}}_{\kappa}$ (31)
$\displaystyle\sigma,\overline{{{y}\\!:\\!{q}}}$
$\displaystyle\models\hat{\sigma}^{c}_{\kappa}(p_{i})\Rightarrow p_{i}$ By
repeating Lemma 4.2 and $\kappa\not\in p$
$\displaystyle\sigma,\overline{{{y}\\!:\\!{q}}}$
$\displaystyle\models\hat{\sigma}^{c}_{\kappa}(\forall(\overline{{{x_{i}}\\!:\\!{p_{i}}}})\Rightarrow
p)$ That is $\displaystyle\sigma,\overline{{{y}\\!:\\!{q}}}$
$\displaystyle\models\hat{\sigma}^{c}_{\kappa}(c^{\prime\prime})$ As by (31)
$\kappa\not\in\overline{q}$ $\displaystyle\sigma$
$\displaystyle\models\hat{\sigma}^{c}_{\kappa}(\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow
c^{\prime\prime})$ Thus, by (36) $\displaystyle\sigma$
$\displaystyle\models\hat{\sigma}^{c}_{\kappa}(\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow
c^{\prime}\\!\uparrow\\!\kappa)$ (37) And by Lemma 4.4
$\displaystyle\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models\forall(\overline{{{y}\\!:\\!{q}}})\Rightarrow
c^{\prime}\\!\uparrow\\!\kappa$  _Case:
$\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}\models C$_ (39) (38) By (32, 34),
Lemma 4.7 $\displaystyle\sigma$ $\displaystyle\models C$ As $\kappa\not\in C$,
$\mathsf{domain}(\hat{\sigma}^{c}_{\kappa})=\\{\kappa\\}$
$\displaystyle\hat{\sigma}^{c}_{\kappa}(C)$ $\displaystyle=C$ By (38)
$\displaystyle\sigma$ $\displaystyle\models\hat{\sigma}^{c}_{\kappa}(C)$ (39)
By Lemma 4.4 $\displaystyle\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models C$

∎

###### 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_

Assume $c^{\prime}$ is satisfiable with $\displaystyle{\sigma^{\prime}}$
$\displaystyle\models{c^{\prime}}$ (by Lemma 4.5)
$\displaystyle{\sigma^{\prime}}$
$\displaystyle\models{\mathsf{flat}(c^{\prime})}$ (by Lemma A.1)
$\displaystyle{\sigma^{\prime}}$
$\displaystyle\models{\hat{\sigma}^{c}_{\kappa}(c\\!\uparrow\\!\kappa)}$ (40)
(by Lemma 4.4)
$\displaystyle{\sigma^{\prime}\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}}$
$\displaystyle\models{c\\!\uparrow\\!\kappa}$ (41) (by Theorem 5.5, Lemma 4.3)
$\displaystyle{\sigma^{\prime}\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}}$
$\displaystyle\models{c\\!\downarrow\\!\kappa}$ By 40, 41, Lemma 4.7
$\displaystyle{\sigma^{\prime}\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}}$
$\displaystyle\models c\quad\mbox{{i.e.}\@\leavevmode\nobreak\ $c$ is
satisfiable.}$  _Case: $c$ is satisfiable implies $c^{\prime}$ is satisfiable_
Assume $c$ is satisfiable with $\displaystyle{\sigma}$
$\displaystyle\models{c}$ by Theorem 5.6
$\displaystyle\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models c$ by Lemma 4.7
$\displaystyle\sigma\\!\cdot\\!\hat{\sigma}^{c}_{\kappa}$
$\displaystyle\models c\\!\uparrow\\!\kappa$ by Lemma 4.4
$\displaystyle\sigma$
$\displaystyle\models\hat{\sigma}^{c}_{\kappa}(c\\!\uparrow\\!\kappa)$ by
Lemma A.1 $\displaystyle\sigma$
$\displaystyle\models\mathsf{flat}(c^{\prime})\quad\mbox{{i.e.}\@ by
Lemma\leavevmode\nobreak\ \ref{lem:flatten} $c^{\prime}$ is satisfiable.}$

∎