Automation of separation logic using auto2

Efficient verification of imperative programs using auto2 Bohua Zhan

arXiv:1610.06996v2 [cs.LO] 22 Oct 2017

Technical University of Munich

Abstract. Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the setup of auto2 for both stages of the proof process: verification of a functional version of the program, and refining to the imperative version using separation logic. As examples, we verify several data structures, including red-black trees, interval trees, priority queues, and union-find. We also verify several algorithms making use of these data structures. These examples show that our framework is able to verify complex algorithms efficiently and in a modular manner.

1

Introduction

Verification of imperative programs has been a well-studied area. While work on separation logic addressed the main theoretical issues, verification in practice is still a tedious process. Even if we limit to the case of sequential programs with relatively simple memory-allocation patterns, verification is still difficult when the underlying algorithm requires extensive reasoning and/or background knowledge to justify. Such reasoning can quickly go beyond the ability of automatic theorem provers. Proof assistants such as Isabelle and Coq provide an environment in which human users can guide the computer through the proof. However, such a process today often requires a lot of low-level reasoning with lists, sets, etc, as well as dealing with details of separation logic. We believe much work can still be done to provide more automation in this area, reducing the amount of time and expertise required to perform verifications, with the goal of eventually making verification of complex algorithms a routine process. The auto2 prover in Isabelle is introduced by the author in [24]. Its approach to automation in proof assistants is significantly different from the two main approaches today: tactics and the use of external automatic theorem provers (as represented by Sledgehammer in Isabelle). Compared to Sledgehammer, auto2 is highly customizable: users can set up new reasoning rules and procedures at any point in the development of a theory (for example, our entire setup for separation logic is built outside the main auto2 program). It also works directly with higher-order logic and types available in Isabelle. Compared to tactics, auto2 uses a saturation-based search mechanism, that is closer to the kind of

2

Bohua Zhan

search performed in automatic theorem provers, and from experience has been more powerful and stable than the backtracking approach usual in the tactics framework. In this paper, we apply auto2 to the verification of imperative programs. We limit ourselves to sequential programs with relatively simple memory-allocation patterns. The algorithms underlying the programs, however, require extensive reasoning and/or background knowledge to justify. The verification process can be roughly divided into two stages: verifying a functional version of the program, and refining it to an imperative version using separation logic. The main contributions of this paper are as follows. 1 – We discuss the setup of auto2 to provide automation for both stages of this process. For the verification of functional programs, this means automatically proving simple lemmas involving lists, sets, etc. For refining to the imperative program, this means handling reasoning with separation logic. – Using our setup, we verify several data structures including red-black trees, interval trees, priority queues, and union-find. We also verify algorithms including Dijkstra’s algorithm for shortest paths and a line-sweeping algorithm for detecting rectangle intersection. These examples demonstrate that using our approach, complex algorithms can be verified in a highly efficient and modular manner. We now give an outline for the rest of the paper. In Section 2, we give an overview of the auto2 prover. In Section 3, we discuss our setup of auto2 for verification of functional programs. In Section 4, we review the Imperative HOL framework in Isabelle and its separation logic, which we use to describe and verify the imperative programs. In Section 5, we discuss our setup of auto2 for reasoning with separation logic. In Section 6, we briefly describe each of the case studies, showing some statistics and comparison with existing verifications. Finally, we review related work in Section 7, and conclude in Section 8. Acknowledgements. The author would like to thank Adam Chlipala, Peter Lammich, and Tobias Nipkow for discussions and feedback during this project. For the first half of this project, the author was at MIT and was supported by NSF Award No. 1400713. During the second half, the author is at TU Munich, and is supported by DFG Koselleck grant NI 491/16-1.

2

Overview of the auto2 prover

The auto2 prover is introduced in [24]. In [25], several additional features are described, in an extended application to formalization of mathematics. In this section, we summarize the important points relevant to this paper. Auto2 uses a saturation-based proof search mechanism. At any point during the search, the prover maintains a list of items, which may be derive facts, terms 1

Code available at https://github.com/bzhan/auto2

Efficient verification of imperative programs using auto2

3

that appeared in the proof, or some other information. At the beginning, the statement to be proved is converted into contradiction form, and its assumptions form the initial state. The search finishes with success when a contradiction is derived. In addition to the list of items, the prover also maintains several additional tables, three of which will be described below. 2.1

Proof steps

Proof steps are functions that produce new items from existing ones. During the development of a theory, proof steps can be added or removed at any time. At each iteration of the proof search, auto2 applies the current list of proof steps to generate new items. Each new item is given a score and inserted into a priority queue. They are then added to main list of items at future iterations in increasing order of score. Adding new proof steps is the main way to set up new functionality for auto2. Proof steps range from simple ones that apply a single theorem, to complex functions that implement some proof procedure. Several proof steps can also work together to implement some proof strategy, communicating through their input and output items. We will see examples of all these in Section 3 and 5. 2.2

Rewrite table

Among the tables maintained by auto2, the most important is the rewrite table. The rewrite table keeps track of the list of currently known (ground) equalities. It offers two main operations: deciding whether two terms are equivalent, and matching up to known equalities (E-matching). The latter is the basic matching function used in auto2: whenever we mention matching in the rest of the paper, it is assumed to mean E-matching using the rewrite table. We emphasize that when a new ground equality is derived, auto2 does not use it to rewrite terms in the proof state. Instead, the equality is inserted into the rewrite table, and incremental matching is performed on relevant items to discover any new matches. 2.3

Property and well-form tables

We now discuss two other important tables maintained by the prover: the property table and the well-form table. Any predicate (constant of type ’a ⇒ bool ) can be registered as a property during the development of a theory. During the proof, the property table maintains the list of properties satisfied by each term appearing in the proof. Common examples of predicates that we register as properties include sortedness on lists and various invariants satisfied by binary search trees. For any function, we may register certain conditions on its arguments as wellformedness conditions of that function. Common examples include the condition a ≥ b for the term (a - b)::nat, and i < length xs for the term xs ! i (i ’th

4

Bohua Zhan

element of the list xs ). We emphasize that registering well-formedness conditions is for the automation only, and do not imply any modification to the logic. During the proof, the well-form table maintains the list of well-formedness conditions that are known for each term appearing in the proof. The property and well-form tables allow proof steps to quickly lookup certain assumptions of a theorem. We call assumptions that can be looked-up in this way side assumptions. We will see examples of this in Section 3.1, and another important application of the well-form table in Section 3.2. 2.4

Case analysis

The need for case analysis introduces further complexities. New case analysis is produced by proof steps, usually triggered by the appearance of certain facts or terms in the proof. We follow a saturation-based approach to case analysis: the list of cases (called boxes) is maintained as a part of the proof state, and derivation in all boxes are performed in parallel. More precisely, every item (and entry in the tables) is assigned to some box, according to which additional assumptions are needed to derive that item. When a contradiction is derived in a box with additional assumption P , the fact ¬P is added to its parent box. The proof finishes only if a contradiction is derived in the initial box (with no additional assumptions). 2.5

Proof scripts

Auto2 defines its own style of proof scripts, which is similar to, but independent from Isar scripts in Isabelle. The main difference between auto2 and Isar scripts is that auto2 scripts do not contain names of tactics (all subgoals are proved using auto2), labels for intermediate goals, or names of previous theorems. Examples of auto2 scripts are given in Section 3.4. We explain the basic commands here (all commands in auto2 scripts begin with an @ sign, to distinguish them from similar Isar commands). – @have P : prove the intermediate goal P . Afterwards, make P available in the remainder of the proof block. – @case P : prove the current goal with additional assumption P . Afterwards, make ¬P available in the remainder of the proof block. – @obtain x where P(x) : here x must be a fresh variable. Prove the intermediate goal ∃x. P (x). Afterwards, create variable x and make fact P (x) available in the remainder of the proof block. – @with . . . @end : create a new proof block. That is, instead of proving the subgoal in the previous command directly using auto2, prove it using the commands between @with and @end. – @induct, @prop_induct, etc: commands for several types of induction. Each type of induction has its own syntax, specifying which variable or proposition to apply induction on. We omit the details here.


3

5

Verification of functional programs

Proofs of correctness of functional programs involve reasoning in many different domains, such as arithmetic, lists, sets, maps, etc. The proof of a single lemma may require results from more than one of these domains. The design of auto2 allows automation for each of these domains to be specified separately, as a collection of proof steps. During the proof, they work together by communicating through the common list of items and other tables maintained by the prover. In this section, we discuss our setup of auto2 for verification of functional programs. It is impossible to describe the entire setup in detail. Instead, we will give some examples, showing the range of functionality that can be supported in auto2. At the end of the section, we give an example showing the strength of the resulting automation. We emphasize that the aim here is not to implement complete proof procedures, or to compete with highly-optimized theory solvers for efficiency. Instead, we simply aim for the prover to consistently solve tasks that humans consider to be routine. Since we are in an interactive setting, we can always ask the user to provide intermediate goals for more difficult proof tasks. 3.1

Simple proof steps

Most of the proof steps added to auto2 applies a single theorem. In this section, we show several examples of such proof steps. They are simple enough that, using certain utility functions, one can add any of these proof steps in one line of code. Forward and backward reasoning The most basic kind of proof steps apply a theorem in the forward or backward direction. For example, the theorem sorted (x # xs) =⇒ y ∈ set xs =⇒ x ≤ y

is added as a forward proof step. This proof step looks for pairs of facts in the form sorted (x # xs) and y ∈ set xs (note this uses E-matching, same below). For every match, it produces the output x ≤ y. In contrast, the theorem sorted xs =⇒ j < length xs =⇒ i ≤ j =⇒ xs ! i ≤ xs ! j.

should be added as a backward proof step. This proof step looks for facts of the form ¬(xs ! i ≤ xs ! j) (equivalently, goal to prove xs ! i ≤ xs ! j ). For every match, it looks for the assumption sorted xs in the property table, and j < length xs in the well-form table (it is the well-formedness condition of the subterm xs ! j ). If both assumptions are found, the proof step outputs fact ¬(i ≤ j) (equivalently, goal to prove i ≤ j ). Another type of proof steps add a new fact for any term matching a certain pattern. For example, for the theorem n < length xs =⇒ xs ! n ∈ set xs,

6

Bohua Zhan

the corresponding proof step looks for terms in the form xs ! n. For every match, it looks for the assumption n < length xs in the well-form table, and output xs ! n ∈ set xs if the assumption is found. This particular setup is chosen because assumptions of the form y ∈ set xs appears frequently in practice. Rewrite rules Rewrite rules form another major class of proof steps. They add new equalities to the rewrite table, usually after matching the left side of the equality. As an example, consider the theorem for evaluation of list update: i < length xs =⇒ xs[i := x] ! j = (if i = j then x else xs ! j).

The corresponding proof step looks for terms of the form xs[i := x] ! j. For every match, it looks for the assumption i < length xs in the well-form table (this is the well-formedness condition of xs[i := x] ). If the assumption is found, the proof step outputs the equality. When the equality is pulled from the priority queue, it is added to the rewrite table. For the theorem evaluating the length of list update: length (xs[i := x]) = length xs

we add a slightly different proof step: it produces the equality whenever it finds the term xs[i := x], without waiting for length (xs[i := x]) to appear. This can be justified by observing that it is helpful to know the length of any list appearing in the proof, as it is mentioned in the assumptions of many theorems. Generating case analysis Another class of proof steps generate case analysis on seeing certain terms or facts in the proof state. For example, there is a proof step that looks for terms of the form if P then b else c, and creates case analysis on P for every match. Case analysis may also be created to check well-formedness conditions. Usually, when we register a well-formedness condition, auto2 will look for the condition in the list of items during the proof. However, sometimes it is better to be more proactive, and try to prove the condition whenever a term of the given form appears. This is achieved by creating a case analysis with the condition as the goal (or equivalently, with the negation of the condition as the assumption). 3.2

Normalization of natural number expressions

In this section, we give an example of a more complex proof step. It compares expressions on natural numbers by normalizing both sides with respect to addition and subtraction. Mathematically, the expression a−b on natural numbers is undefined if a < b. In Isabelle (and many other proof assistants), it is simply defined to be zero. This means many equalities involving subtraction on natural numbers that look obvious are in fact invalid. Examples include a − b + b = a, which in Isabelle is false if a < b.


7

This substantially complicates normalization of expressions on natural numbers involving subtraction. In general, normalization of such an expression agrees with intuition as long as the expression is well-formed, in the sense of Section 2.3. Following the terminology in [25, Section 3.3], we say a well-formed term is a term together with a list of theorems justifying its well-formedness conditions, and a well-formed conversion is a function that, given a well-formed term, returns an equality rewriting that term, together with theorems justifying wellformedness conditions on the right side of the equality. Well-formed conversions can be composed in the same way as regular conversions (rewriting procedures). In particular, we can implement normalization for expressions on natural numbers with respect to addition and subtraction as a well-formed conversion. This is in turn used to implement the following proof step. Given any two terms s, t of type nat involving addition and subtraction, look for their wellformedness conditions in the well-form table. If all well-formedness conditions for subtraction are present, normalize s and t using the well-formed conversion. If their normalizations are the same, output the equality s = t. 3.3

Difference logic on natural numbers

Difference logic is concerned with propositions of the form a ≤ b + n, where n is a constant. A collection of such inequalities can be represented as a directed graph, where nodes are terms and weighted edges represent inequalities between them. A collection of inequalities is contradictory if and only if the corresponding graph contains a negative cycle, which can be determined using the BellmanFord algorithm. In auto2, we implement difference logic for natural numbers using special items and proof steps. While less efficient than a graph-based implementation, it is sufficient for our purposes, and also interacts better with other proof steps. Each inequality on natural numbers is represented by an item of type NAT_ORDER, which contains a triple recording the terms on the two sides and the difference. The transitivity proof step looks for pairs of items of the form and , and produces the item for each match. The resolve proof step looks for items of the form , where n is less than zero, and derives a contradiction for each match. 3.4

Example

As an example, we show a snippet from the functional part of the verification of the union-find data structure. Union-find is implemented on an array l, with l ! i = i if i is the root of its component, and the parent of i if otherwise. rep_of i denotes the root of the component containing i. The compress operation is defined as: definition ufa_compress :: "nat list ⇒ nat ⇒ nat list" where [rewrite_bidir]: "ufa_compress l x = l[x := rep_of l x]" setup {* register_wellform_data ("ufa_compress l x", ["x < length l"]) *}

8

Bohua Zhan

The main properties of ufa_compress are the following: lemma ufa_compress_invar: "ufa_invar l =⇒ x < length l =⇒ l’ = ufa_compress l x =⇒ ufa_invar l’" @proof @have "∀i