Formal Reasoning about Efficient Data Structures: A Case Study in ACL2

Formal Reasoning about Efficient Data Structures: A Case Study in ACL2 Jos´e Luis Ruiz-Reina, Jos´e Antonio Alonso-Jim´enez, Mar´ıa Jos´e Hidalgo, and Francisco Jes´us Mart´ın-Mateos Computational Logic Group Dept. of Computer Science and Artificial Intelligence, University of Seville E.T.S.I. Inform´atica, Avda. Reina Mercedes, s/n. 41012 Sevilla, Spain http://www.cs.us.es/{~jruiz,~jalonso,~mjoseh,~fmartin} Abstract. We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms are represented as directed acyclic graphs (dags) and these graphs are stored in a single-threaded object (stobj). The use of stobjs allows destructive operations on data (thus improving the performance of the algorithm), while maintaining the applicative semantics of ACL2. We intend to show how ACL2 provides an environment where execution of algorithms with efficient data structures and formal reasoning about them can be carried out. 1 Introduction The ACL2 system includes a programming language, a logic for formal reasoning about the properties of the functions defined in the language, and a theorem prover supporting mechanized reasoning in the logic. The ACL2 programming language is an extension of an applicative subset of Common Lisp and the logic is a first-order logic with equality, without quantifiers (all the formulas are implicitly universally quantified). Since the programming language is applicative, logical arguments about the correctness and termination of algorithms are made as they are in ordinary mathematics, without the complications incured by consideration of state. Notwithstanding, it is possible to declare some objects in the language as single-threaded objects (in the sequel, stobjs) and perform destructive updates on them. When an object is declared to be single-threaded, ACL2 enforces certain syntactic restrictions on its use, ensuring that in every moment only one copy of the object is needed. With these restrictions, the destructive updates are consistent with the applicative semantics of ACL2. Using stobjs we can combine efficient imperative implementations with the semantic of functional languages to reason about these implementations. This work has been supported by project TIC2000-1368-C03-02 (Ministry of Science and Technology, Spain) and FEDER funds. In this paper we present a case study where we use ACL2 to implement and verify a unification algorithm. A standard approach in the implementation of unification is to represent terms as directed acyclic graphs (dags in the following), allowing some amount of structure sharing; in this way, it is not needed to build new terms during the unification process, but merely update (destructively) the graph, thus improving the performance of the algorithm. In our implementation, the dags will be stored using a stobj. To achieve the formal proof, we follow the well-known methodology of compositional reasoning. As a first step, we reason about unification at a very abstract level, without entering in details related to the control of the algorithm or the data structures used. By stepwise-refinement, we finally obtain the proof of the desired properties of our concrete unification algorithm. Another interesting point in this case study is the use of a new feature in ACL2 (the mbe feature) that associates an “executable body” with a (possibly different) “logical body”. This association will be allowed by the system after proving that on the intended domain of the function, the executable body and the logical body are equal. We describe this new feature of ACL2, and explain how it can be used to improve the execution efficiency of the verified unification algorithm. Although we will not give an introduction to ACL2, we will comment the relevant questions in passing, when needed. An excellent introduction to ACL2 is [5]. A detailed description of the system can be found in the manual, available in [6]. We will assume the reader familiar with Common Lisp. Due to the lack of space, we will not give here details about the proofs obtained and some function definitions will be omitted. We urge the interested reader to consult [11], where the complete development (with a detailed description) is available. 2DagUnification We briefly review some basic concepts about (syntactic) unification, a fundamental process upon which many methods of automated deduction are based. A complete description of the theory of unification can be found in [2]. An equation is a pair of first-order terms, denoted as t1≈t2,andasystem of equations is a finite set of equations. A substitution σis a solution of t1≈t2 if σ(t1)=σ(t2) and it is a solution of a system of equations Sif it is a solution of every equation in S. Given two substitutions σand δ,wesaythatσis more general than δif there exists a substitution γsuch that δ=γ◦σ,where◦denotes functional composition. We say that a solution of Sis a most general solution if it is more general than any other solution of S.Twotermst1and t2are unifiable if there exists a solution (called unifier) of the system {t1≈t2}.Amost general unifier (mgu in the sequel) of t1and t2is a most general solution of that system. Aunification algorithm is an algorithm that decides whether two given terms are unifiable, and in that case it returns a most general unifier. Essentially, the unification algorithm we have implemented is based on the relation ⇒ugiven by the set of transformation rules presented in Figure 1 (known Delete: {t≈t}∪R;U⇒uR;U Occur-check: {x≈t}∪R;U⇒u⊥if x∈V(t)andx=t Eliminate: {x≈t}∪R;U⇒uθ(R); {x≈t}∪θ(U) if x∈X,x/∈V(t)andθ={x→ t} Decompose: {f(s1, ..., sn)≈f(t1, ..., tn)}∪R;U⇒u{s1≈t1, ..., sn≈tn}∪R;U Clash: {f(s1, ..., sn)≈g(t1, ..., tm)}∪R;U⇒u⊥if n=mor f=g Orient: {t≈x}∪R;U⇒u{x≈t}∪R;Uif x∈X,t/∈X Fig. 1. Martelli–Montanari transformation system as the Martelli-Montanari transformation system). This system acts on pairs of systems of equations of the form S;U. Intuitively, the system Scan be seen as a set of pairs of terms to be unified, and the system Uas a (partially) computed unifier1(we say that the pair S;Uis a unification problem). The symbol ⊥ represents unification failure. Starting with the pair of systems S;∅,theserules can be (non-deterministically) applied iteratively, until either a pair of systems of the form ∅;Uor ⊥is obtained. It can be proved that this process must terminate and that Shas a solution if and only if ⊥is not derived; in that case Uis a most general solution of S. Thus, a unification algorithm can be designed choosing an strategy to apply the rules, starting with the pair of systems {t1≈t2};∅,where t1and t2are two given input terms. In [10] we had defined and verified a unification algorithm based on this set of transformation rules, as part of an ACL2 library with formal proofs of the lattice-theoretic properties of first-order terms. In that library, terms are represented in prefix notation, using lists (except variables, which are represented by atomic objects). For example, the term f(x, g(y),h(x)) is represented by the list (fx(gy)(hx)). Substitutions are represented as association lists, and systems of equations as lists of dotted pairs of terms. In the sequel, this representation of terms and substitutions in prefix form, using lists, will be referred to as prefix representation or prefix notation. Using the prefix representation, a unification algorithm may be inefficient in some situations. Consider, for example, the following standard parameterized unification problem, which we will call Un: p(xn,...,x 2,x 1)≈p(f(xn−1,x n−1),...,f(x1,x 1),f(x0,x 0)) A mgu of this problem is {x1→ f(x0,x 0),x 2→ f(f(x0,x 0),f(x0,x 0)),...}, which maps each variable xito a complete binary tree of height i.Thismgu can be obtained by repeatedly applying the Eliminate rule of ⇒u.Ifweusethe prefix representation of terms, it will be necessary to reconstruct the instantiated system of equations, each time the rule is applied. 1We will identify a system of equations of the form {x1≈t1,...,x n≈tn},where the xiare variables, with the substitution {x1→ t1,...,x n→ tn}.Ifnoneofthexi appear in any of the tj, we say that the system is in solved form.Notethatevery system in solved form is a mgu of itself. The standard approach to deal with this problem is to use term dags where variables are shared. For example, the following graph represents the equation f(h(z),g(h(x),h(u))) ≈f(x, g(h(u),v)). Nodes are labeled with function and variable symbols, and outgoing edges connect every node with dags representing its immediate subterms. We can naturally identify the root node of a term dag with the whole term. Note also that there is a certain amount of structure sharing, at least for the repeated variables2: ff gg hhh v To implement a unification algorithm with this term representation, the main idea is never to build new terms but only create pointers. In particular, the Eliminate rule can be implemented adding a pointer linking the variable with the term to which this variable is bound; in that way no reconstruction of the term is required in the application of a substitution. In the graph above, these pointers are represented by dashed arrows. The binding for a variable can be determined by following the pointers traversing the graph depth first, from left to right. In this case, the substitution represented is {x→ h(z),u → h(z),v → h(h(z))}, which is a mgu of f(h(z),g(h(x),h(u))) and f(x, g(h(u),v)). 3 An ACL2 Implementation The implementation described here is based on the Pascal implementation given in section 4.8 of [1]. The main difference is that instead of a record with pointers, we use a single-threaded object. This stobj is a structure called terms-dag with only one field: an array called dag (whose size can be modified dynamically). This array is used to store the unification problem in dag form: (defstobj terms-dag (dag :type (array t (0)) :resizable t)) The effect of this ACL2 event is to introduce the stobj terms-dag and its associated recognizers, creator, accessors, updaters, and length and resize functions of the array field. In particular, given an index i(a natural number) corresponding to a cell of the dag array, the expressions (dagi iterms-dag) and (update-dagi ivterms-dag) access and update (with value v) respectively the i-th cell of the dag array. These operations are done in constant time and the 2It should be remarked that this is simply one possible representation in which only variables are shared; this is not the most compact representation, but the one that serves as the basis of the verified unification algorithm. update is destructive. Nevertheless, from the logical point of view, the array can be thought as a list, with an applicative semantic (that is, as if in every update a new object were created) . This is possible due to the fact that in ACL2, the use of stobjs is syntactically restricted, ensuring that in every moment only one copy of the object is needed. Roughly speaking, these syntactic restrictions enforce that the only references to the stobj are done via its name (terms-dag,inthis case). See [4, 6] for further information about stobjs in ACL2 and the restrictions on its use. Each node in the graph is represented by a cell in the dag array of the stobj. Thus, a node in the graph can be identified with an array index. Each cell stores the label and the successors of one node, in the following way: –If node irepresents an unbound variable x,then(dagi iterms-dag) contains a dotted pair of the form (x.t). –If node irepresents a bound variable, then (dagi iterms-dag) contains an index npointing to the root node of the term to which the variable is bound. –If node iis the root node of a non-variable term f(t1,...,t n), then (dagi i terms-dag) isadottedpairoftheform(f.l),wherelis the list of the indices corresponding to the root nodes of t1,...,t n. In this way, we can store a unification problem using the terms-dag stobj. For example, if we store the term equ(f(h(z),g(h(x),h(u))),f(x, g(h(u),v))) the significant cells of the dag array are: 6 8 1 (EQU . (1 9)) 0 (F . (2 4)) 7 (H . (8)) 8 (U . T) 9 (F . (10 11)) 32 (H . (3)) (Z . T) 10 4 (G . (5 7)) (X . T) 6 (H . (6)) 5 1311 (G . (12 14)) (H . (13)) 12 (V . T) 14 We can naturally identify an array index with the term whose root node is stored in the corresponding array cell. Taking advantage of this idea, we can define a function (called dag-transform-mm-st, figure 2) that applies one step of the transformation relation ⇒uto a unification problem stored in terms-dag. Let us precise about the behavior of dag-transform-mm-st. In addition to the stobj, this function receives as input a (non-empty) system of equations S to be unified and a partially computed substitution U. The key point here is that Sand Uonly contain indices pointing to the terms stored in terms-dag. In particular, Sis a list of pairs of indices, and Uis a list of pairs of the form (x.n)where xis a variable symbol and nis the index of the node for which the variable is bound (we say that Sis an indices system and Uan indices substitution). Depending on the pair of terms pointed to by the first equation of S3, one of the rules of ⇒uis applied. The function returns a multivalue with the following components, obtained as a result of the application of one step of transformation: the resulting indices system of equations to be solved, the 3Note that the indices of the selected equation are dereferenced using the function dag-deref-st, which follows a chain of instantiations until it reaches an unbound variable or non-variable node. (defun dag-transform-mm-st (S U terms-dag) (declare (xargs :stobjs terms-dag)) (let* ((ecu (car S)) (t1 (dag-deref-st (car ecu) terms-dag)) (t2 (dag-deref-st (cdr ecu) terms-dag)) (R (cdr S)) (p1 (dagi t1 terms-dag)) (p2 (dagi t2 terms-dag))) (cond ((= t1 t2) (mv R U t terms-dag)) ((dag-variable-p p1) (if (occur-check-st t t1 t2 terms-dag) (mv nil nil nil terms-dag) (let ((terms-dag (update-dagi t1 t2 terms-dag))) (mv R (cons (cons (dag-symbol p1) t2) U) t terms-dag)))) ((dag-variable-p p2) (mv (cons (cons t2 t1) R) U t terms-dag)) ((not (eql (dag-symbol p1) (dag-symbol p2))) (mv nil nil nil terms-dag)) (t (mv-let (pair-args bool) (pair-args (dag-args p1) (dag-args p2)) (if bool (mv (append pair-args R) U t terms-dag) (mv nil nil nil terms-dag))))))) Fig. 2. One step of transformation resulting indices substitution, a boolean (if ⊥is obtained, this value is nil)and the stobj terms-dag. Note that only when Eliminate is applied, the stobj is updated, causing the corresponding variable to point to the corresponding term. With dag-transform-mm-st as its main component, we can define the unification algorithm. In short, this function, called dag-mgu, receives as input two terms in prefix form; after storing these terms as directed acyclic graphs in the stobj (previously resizing the dag array properly), it iteratively applies the function dag-transform-mm-st until either non-unifiability is detected or there are no more equations to be solved. In this last case, the returned substitution (in prefix form) is built from the final contents of dag, following the pointers of the instantiated variables. The following are two examples obtained with dag-mgu. Note that the function returns two values: the first one is a boolean indicating whether the terms are unifiable or not, and, in case of unifiability, the second is the mgu. ACL2 !>(dag-mgu ’(f (h z) (g (h x) (h u))) ’(f x (g (h u) v))) (T ((V . (H (H Z))) (U . (H Z)) (X . (H Z)))) ACL2 !>(dag-mgu ’(f y x) ’(f (k x) y)) (NIL NIL) It is worth pointing out that the syntactic requirements needed to ensure the single-threadedness of the ACL2 functions that use stobjs are naturally met in this algorithm. See [11] for the definitions of all the auxiliary functions used. Since the ACL2 language is a subset of Common Lisp (and we have verified guards4), the defined algorithm can be compiled and executed in every compliant Common Lisp, with the appropriate ACL2 files loaded. 4 The Formal Properties of the Unification Algorithm Once defined the function dag-mgu, we use the ACL2 logic and its theorem prover to formally establish that it computes the most general unifier of two terms if and only if the terms are unifiable: (defthm dag-mgu-completeness (implies (and (term-p t1) (term-p t2) (equal (instance t1 sigma) (instance t2 sigma))) (first (dag-mgu t1 t2)))) (defthm dag-mgu-soundness (implies (and (term-p t1) (term-p t2) (first (dag-mgu t1 t2))) (equal (instance t1 (second (dag-mgu t1 t2))) (instance t2 (second (dag-mgu t1 t2)))))) (defthm dag-mgu-most-general-solution (implies (and (term-p t1) (term-p t2) (equal (instance t1 sigma) (instance t2 sigma))) (subs-subst (second (dag-mgu t1 t2)) sigma))) The function instance defines the application of a substitution to a term, and the predicate subs-subst defines the relation “more general than” between substitutions. The predicate term-p recognizes those ACL2 objects that represent first-order terms in prefix notation. Note that the basic theory used to state the properties is built on the terms represented in prefix notation. For a detailed description of this theory, see [10]. Also the input and the output of the function dag-mgu are terms and substitutions in prefix notation. But it has to be emphasized that internally, the main process is carried out on term dags. The first theorem, dag-mgu-completeness, establishes that the algorithm returns t(as its first value) if the input terms are unifiable5.Thetheoremdag- -mgu-soundness establishes that in that case it returns (as its second value) a unifier of both terms. Finally, the theorem dag-mgu-most-general-solution establishes that the returned substitution is more general than any other unifier of both terms. These three proved theorems constitute a formal proof of the correctness of the algorithm. 4The notion of guard of a function will be explained in section 6. 5Note that the variable sigma, although implicitly universally quantified, can be seen as existentially quantified, since it only appears in the hypothesis of the theorem. 5 Comments about the Proof In this section, we give an overview of the proof process. To emphasize the “compositional reasoning” methodology followed, we have structured it in subsections. First we begin with the subsections describing properties of the algorithm at a more abstract level. These abstract properties can be gradually concretized to finally obtain the theorems shown in the previous section. 5.1 Reasoning about the Reduction ⇒u One step of transformation of ⇒uis determined by the rule applied and the equation selected. To formalize this intuitive idea in ACL2, we define ⇒uby means of operators. In this context, an operator is a dotted pair of the form (name .i)where name is one of the rule names in figure 1 and iis a natural number, corresponding to the i-th equation of the system. Thus, the transformation ⇒ucan be seen as applying one operator to a unification problem. This operator can be applied whenever the conditions of the particular rule applied are met. For example, the operator (eliminate . 3) can be applied to a unification problem if its third equation is of the form x≈tand xdoes not occur in t. The following two functions formalize this idea in ACL2: •(unif-legal-pr upl op), checking the conditions needed to apply a given operator op to a unification problem upl (in prefix notation). •(unif-reduce-one-step-pr upl op), returning the transformed unification problem (in prefix notation) after applying op to upl. With this operator-based representation we proved in ACL2 the main properties of ⇒u. That is: a) the set of solutions of a unification problem is preserved in each step, b) if the second system of a unification problem is in solved form, then the transformed unification problem has its second system in solved form, and c) the transformation relation is terminating. These properties are more naturally proved with terms represented in prefix form, and this allows us to reuse part of the theory developed in [10] for the verification of the applicative unification algorithm. Having proved the main properties of one-step transformations, we can easily extend these properties to finite sequences of transformations. In particular we prove that if {t1≈t2};∅∗ ⇒u∅;σ,thenσis a mgu of t1and t2,andif{t1≈ t2};∅∗ ⇒u⊥,thent1and t2are not unifiable. Note that in our formalization, a sequence of transformation can be identified with a list of (legal) operators. It is remarkable that these results do not deal with control or data structures issues: to prove the correctness of a concrete unification algorithm, it suffices to show that the actions of the algorithm can be simulated by a finite sequence of transformations w.r.t. ⇒u. That is the main advantage of rule-based specifications: they allow to prove the essential properties of the procedure without the burden of technical implementation issues. 5.2 Dags and Well-Formedness Conditions In order to translate the main properties of ⇒uto our implemented algorithm, we have to relate the information stored in the terms-dag stobj with the terms in prefix notation it may represent. In general, not every possible contents of the dag array represent first-order terms. The main reason is that the graph could contain cycles, and in that case, no first-order term is represented by the cells of the array. This means that we have to define predicates to recognize the properties needed to ensure that the array contents represent a first-order term; the main of those properties is acyclicness, ensuring that the graph stored in the dag array is actually a dag. Some other well-formedness properties are also needed (for instance the sharing of variables). Another important reason why these well-formedness conditions are needed has to do with the restrictions imposed by the ACL2 logic in its principle of definition: new function definitions are admitted as axioms in the logic only if there exists a measure in which the arguments of each recursive call decrease with respect to a well-founded relation, ensuring in this way that the function terminates on all inputs (and consequently no inconsistencies are introduced by new function definitions). For example, a function implementing “occur-check” (looking for the occurrence of a given variable in a term) may not terminate if the graph stored in the array contains cycles. The same happens with dereferencing or even with the function that iteratively applies dag-transform-mm-st.Thus, these functions require an explicit check to verify that the stobj does indeed represent an acyclic graph, ensuring their termination. We will comment more about this point in section 6. For these reasons, we have developed a library of results about directed acyclic graphs. For example, this library contains the definition of the function dag-p; this function checks that a given graph (stored following the conventions described in section 3) does not contain cycles. It is implemented as a standard depth-first search algorithm, looking for cycles in the graph. The following theorems establish that a graph gverifies the dag-p condition if and only if does not contain cycles: (defthm dag-p-soundeness (implies (not (dag-p g)) (cycle-p (one-cyclic-path g) g))) (defthm dag-p-completeness (implies (cycle-p p g) (not (dag-p g)))) Some other general definitions and results about dags are part of this library. See [11] for details. Having dag-p as its main auxiliary function, we can define a function checking the well-formedness conditions of a unification problem given in dag form: (well-formed-upl dag-upl) is true if and only if dag-upl is a three-element list such that its first element is an indices system, the second The intuitive idea that algorithms employing more complex data structures or more sophisticated control structures require more effort in verification is supported by the table of subsection 5.5. These data contrast with the effort needed in the verification of the same algorithm using a prefix representation of terms [10]. In that work, we needed 19 definitions and 129 theorems, and in this case we needed 177 definitions and 703 theorems. Anyway, this additional verification effort has resulted in the development of a number of ACL2 files that could be used in other formalizations (for example, the theory about directed acyclic graphs). As for related works, unification algorithms have been the center of several formalizations. In particular, formal proofs of the correctness of a unification algorithm have been given in LCF [8], Coq [9] and ALF [3]. Although these works are related to ours, the logic used is quite different and, more important, their main concern is not efficiency or the data structures used. Other related work is done by Mehta and Nipkow [7], who have recently developed in Isabelle/HOL a general framework for reasoning about programs that use pointers. As a non-trivial case study, they present a proof of the correctness of the Schorr–Waite graph marking algorithm. This work is more general than ours, since all the reasoning about pointers that we do is especifically devoted to the results needed by the algorithm. Moreover, the logics used are different: in [7], a Hoare logic for pointer programs is embedded in Isabelle/HOL, whereas we are using the ACL2 logic for reasoning about ACL2 functions that can be directly executed in any compliant Common Lisp. Nevertheless, some of the techniques used in [7] are similar to ours: for example, what they call abstraction (mapping low level structures in the heap to higher level concepts) is similar to what we do when we first reason about the main properties of the algorithm using the prefix representation of terms (a higher level representation) and then we translate them to the algorithm that uses dags (a lower level representation). As for further work, we already pointed out at the end of subsection 6 that we can introduce some technical improvements in order to make the verified algorithm run in quadratic time. We also plan to verify this improved algorithm. Finally, note that although our main concern is an efficient and formally verified algorithm, we do not prove theorems about the efficiency of the algorithm. Although reasoning about complexity of algorithms in the ACL2 logic is (in principle) possible, we think that it could be much more difficult than reasoning about the correctness of the algorithm, mainly due to the need of formalizing the “big-O notation” (and its asymptotic character) in the ACL2 logic. Acknowledgments Part of this work was done during a visit of the first author to the Computer Science Department of the University of Texas at Austin. We would like to thank the ACL2 group in Austin, especially to J Moore and Matt Kaufmann, for their support, and for introducing mbe in ACL2. References 1. Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge University Press, 1998. 2. Baader, F. and Snyder, W. Unification theory. Handbook of Automated Reasoning, Elsevier Science Publishers, 2001. 3. Bove, A. Programming in Martin-Lf Type Theory: Unification - A non-trivial Example. Licentiate Thesis, Department of Computer Science, Chalmers University of Technology, 1999. 4. Boyer R.S. and Moore J S. Single-threaded objects in ACL2. In Practical Aspects of Declarative Languages, LNCS 2257, pages 9–27, Springer–Verlag, 2002. 5. Kaufmann, M., Manolios, P. and Moore, J S. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000. 6. Kaufmann, M. and Moore, J S. ACL2 Version 2.7, 2002. Homepage: http://www.cs.utexas.edu/users/moore/acl2/ 7. Mehta, F. and Nipkow, T. Proving Pointer Programs in Higher-Order Logic . to be presented at CADE-19, 2003. 8. Paulson, L. Verifying the unification algorithm in LCF. Science of Computer Programming, 5, 1985. 9. Rouyer, J. Dveloppement de l’algorithme d’unification dans le calcul des constructions avec types inductifs. Tech. Rep. 1795, INRIA Lorraine, 1992 (in french). 10. Ruiz–Reina, J.L., Alonso, J.A., Hidalgo, M.J. and Mart´ ın, F.J. Atheory about first–order terms in ACL2 In Third ACL2 Workshop, Grenoble, 2002. 11. Ruiz–Reina, J.L., Alonso, J.A., Hidalgo, M.J. and Mart´ ın, F.J. A verified dag unification algorithm in ACL2, 2002. Available at http://www.cs.us.es/~jruiz/unificacion-dag