Using the Theorem Prover Isabelle-91 to Verify a Simple Proof of

Compiler Correctness

Boleslaw Ciesielski and Mitchell Wand^{∗} College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA December, 1991

Contents

1 Introduction 2 2 The original proof 2

2.1 The source language and its semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 The compiler and the abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 The compiler correctness proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 The Theorem-Prover Isabelle 8 3.1 A short introduction to Isabelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Lambda calculus as an Object Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Tactics and Tacticals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

4 The theory of the language L_{add} and its semantics 16 5 The proof of the correctness criterion 21 6 Conclusions 31

∗Work supported by the National Science Foundation under grant number CCR-9014603. This paper should be cited as Northeastern University College of Computer Science Technical Report NU-CCS-91-20, December, 1991

1 Introduction

The issue of compiler correctness is of prime importance in program verification theory since the correctness of every ready to run application (as opposed to an algorithm or even a source language program) depends on the compiler being correct. As with every other program the correctness has to be expressed relative to some specification. For compilers, the specification is the semantics of the source language and the semantics of the target language. The compiler is correct if for every source program its semantics is equivalent to the semantics of its translation, for some notion of equivalency. It seems that the most successful approach uses the same theory for expressing both semantics and the compiler itself. In that case the correctness criterion is much easier to formulate. In particular denotational semantics is well suited for this purpose.

Our goal is to develop some techniques for machine verification of compiler correctness proofs. As the first trial we picked up a very simple functional language with addition expressions and procedures. The compiler for this language derived from its denotational semantics has already been developed by Clinger and Wand and is in the style of [1], complete with the abstract machine specification and the correctness proof. This proof is presented in section 2.

Section 3 deals with the actual machine implementation of the proof. Among various theorem provers or checkers available, the Isabelle-91 system [3, 6, 7] was chosen. Isabelle has many features which were quite essential for our research. First, it is a generic theorem prover with user definable object logics. So far we don’t know exactly what the object logic for compiler correctness proofs should be, and it is very likely that more complex source languages will require different proof techniques. One of the most important features of Isabelle is its capability to define tactics which can automate frequently repeated proof steps. Of course tactics can do much more, in fact tactics can actually search for the proof. The latter capability was only used to a limited extent in the presented example due to the lack of experience in proof searching techniques. We also found Isabelle’s mechanisms for dealing with conversions between concrete and abstract syntax very valuable. Due to that the actual definitions of theories and the proofs themselves are much more readable which is very important as proofs and terms tend to grow quickly.

Isabelle is written in the functional programming language ML and using Isabelle often requires writing ML functions. Hence, some knowledge of ML is expected from the reader. Although familiarity with Isabelle is not necessary, it would be very helpful.

2 The original proof

As was stated above the actual proof has been already known, although not in a machine verifiable form. It is presented here to demonstrate the differences to Isabelle’s implementation. Actually, the original proof contains a derivation of the abstract machine performed simultaneously with the compiler derivation. In our experiment we use more straightforward approach. The compiler and the machine are defined in advance and the goal is to prove the correctness criterion.

2.1 The source language and its semantics

The source language L_{add} is given by the following grammar:

Exp ::= Ide  identifier
| (Exp + Exp)  addition
| (Exp Exp)  application
| λ Ide . Exp  abstraction.

To define the denotational semantics for L_{add} the following domains are needed:

Cmd = …  command continuations
v : Val = Int +(Val → Cont → Cmd)  values (integers or procedures)
κ : Cont = Val → Cmd  expression continuations
ρ : Env = Ide → Val  environments.

In addition let error : Cmd be the constant denoting the command continuation returned in the case of an error. The standard continuation semantics is given by the semantics function E : Exp → Env → Cont → Cmd. It is defined by the following equations:

E[[I]] = λρκ.κ(ρ[[I]])  (1)
E[[(e_{1} + e_{2})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.E[[e_{2}]]ρ(λv_{2}. sum v_{1}v_{2}κ))  (2)
E[[(e_{1} e_{2})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.E[[e_{2}]]ρ(λv_{2}. apply v_{1}v_{2}κ))  (3)
E[[λI.e]] = λρκ.κ (in_{R}(λvκ′.E[[e]](ρ[v/I])(λv′. return κ′v′)))  (4)

where

sum = λv_{1}v_{2}κ.(v_{1} = in_{L}(n_{1})) ∧ (v_{2} = in_{L}(n_{2})) ⟶ κ (in_{L}(n_{1} + n_{2})), error  (5)
apply = λv_{1}v_{2}κ.(v_{1} = in_{R}(p)) ⟶ pv_{2}κ, error  (6)
return = λκv.κv  (7)

2.2 The compiler and the abstract machine

Some additional domains are needed in order to define the compiler. The environment has to be split into the symbol table and the display. Expressions are evaluated on the stack which is just a sequence of values. There is also a domain for compiled code (a program).

l : LexAddr = …  lexical addresses
Γ : Stab = Ide → LexAddr symbol table
u : Display = LexAddr → Val  display
ζ : Stack  = Val ∗  stack
π : Prog  = Display → Stack → Cont → Cmd  compiled code

The composition of a symbol table and a display is of type Ide → Val and corresponds to the environment in the denotational semantics. We need a way of updating both components that preserves this correspondence. Here we assume the existence of two predefined combinators ext_{C} : Ide → Stab → Stab and ext_{R} : Val → Display → Display with the following property:

(ext_{R} vu) ∘ (ext_{C} IΓ) = (u ∘ Γ)[v/I]  (8)

for any v : Val, I : Ide, u : Display, Γ : Stab.

As can be seen from the definition of Prog the abstract machine has three registers in addition to the program counter: a display, a local stack, and a continuation. Each instruction of the abstract machine has the form of a combinator which, given a display, a stack and a continuation, returns the command continuation. The instructions may have arguments (fields) and most of them have the program to be executed later (the sequel) as one of the arguments. Let’s assume u : Display, ζ : Stack, κ : Cont, π : Prog, l : LexAddr, v : Val. The machine is defined as follows:

(fetch lπ)uζκ = πu((u l) :: ζ)κ  (9)
(add π)u(in_{L}(n_{2}) :: in_{L}(n_{1}) :: ζ)κ = πu((in_{L}(n_{1} + n_{2})) :: ζ)κ  (10)
(close π′π)uζκ = πu((in_{R}(closure uπ)) :: ζ)κ  (11)
(jsr π)u(v :: in_{R}(closure u′π′) :: ζ)κ = π′(ext_{R} vu′)⟨⟩(cont πuζκ)  (12)
(rts)u(v :: ζ)(cont π′u′ζ′κ′) = π′u′(v :: ζ′)κ′  (13)

The fetch instruction retrieves the value of the identifier and pushes it on the stack. The add instruction replaces the top two values on the stack (which must be integers) by their sum.

The procedure calling scheme involves two record constructors closure and cont. For the correctness proof we will have to assume that

closure uπ = λvκ.π(ext_{R} vu)⟨⟩κ  (14)
cont πuζκ = λz.πu(z :: ζ)κ  (15)

but as far as the machine is concerned these constructors may remain uninterpreted. The close instruction pushes the closure record on the local stack.

The jsr instruction should be executed when the evaluated argument is on the top of the stack and the closure is the next element. The display is updated reflecting the parameter value and the code for the procedure is executed. In addition a continuation is constructed to save the current state of the machine.

The rts instruction is executed with the value to be returned on top of the stack. It restores the saved state from the continuation record and pushes the returned value on the caller’s stack.

Now the compiler may be defined. The compiler is a three argument operator C : Exp → Stab → Prog → Prog. It takes a source expression, a symbol table and a piece of machine code to be executed later. As a result the combined code is returned. In the following definition assume that Γ : Stab, π : Prog.

C[[I]]Γπ = fetch(Γ[[I]])π  (16)
C[[(e_{1} + e_{2})]]Γπ = C[[e_{1}]]Γ(C[[e_{2}]]Γ(add π))  (17)
C[[(e_{1} e_{2})]]Γπ = C[[e_{1}]]Γ(C[[e_{2}]]Γ(jsr π))  (18)
C[[λI.e]]Γπ = close(C[[e]](ext_{C} IΓ) rts)π  (19)

2.3 The compiler correctness proof

The correctness criterion used here was proposed in [1]. It states that the effect of executing a code obtained from the compilation of an expression should be to place the value of the expression (as defined by the denotational semantics) on the top of the stack. The following theorem formulates the correctness criterion in our notation.

Theorem 1 For all source expressions e and for all Γ : Stab, π : Prog, u : Display, ζ : Stack, κ : Cont :

(C[[e]]Γπ)uζκ = E[[e]](u ∘ Γ)(λz.πu(z :: ζ)κ).  (20)

Proof: The proof is performed by induction on the structure of the source expression. The above equation is our induction hypothesis.

1. e ≡ I

(C[[I]]Γπ)uζκ = fetch(Γ[[I]])πuζκ  by (16)
= πu((u ∘ Γ)[[I]] :: ζ)κ  by (9)
= E[[I]](u ∘ Γ)(λz.πu(z :: ζ)κ)  by (1)

2. e ≡ (e_{1} + e_{2})

(C[[(e_{1} + e_{2})]]Γπ)uζκ = C[[e_{1}]]Γ(C[[e_{2}]]Γ(add π))uζκ by (17)
= E[[e_{1}]](u ∘ Γ)(λx.C[[e_{2}]]Γ(add π)u(x :: ζ)κ) by (20) for e_{1}
= E[[e_{1}]](u ∘ Γ)(λx.E[[e_{2}]](u ∘ Γ)
(λy.(add π)u(y :: x :: ζ)κ)) by (20) for e_{2}
= E[[e_{1}]](u ∘ Γ)(λx.E[[e_{2}]](u ∘ Γ)
(λy.πu((x + y) :: ζ)κ)) by (10)
= E[[e_{1}]](u ∘ Γ)(λx.E[[e_{2}]](u ∘ Γ)
(λy. sum xy(λz.πu(z :: ζ)κ)) by (5)
= E[[(e_{1} + e_{2})]](u ∘ Γ)(λz.πu(z :: ζ)κ) by (2)

The applications of (5) and (10) in the above derivation require some explanation. Both sum and add operate only on integer arguments but we don’t really know what is returned as a value of e_{1} and e_{2}. However we assume that the execution of a program trying to execute add on non-integer arguments yields the same constant error which is passed to continuation in the definition of sum. Therefore the correctness criterion holds also in that case. This may seem a little informal and we will have to be more precise when formalizing the proof for Isabelle.

3. e ≡ (e_{1} e_{2})

(C[[(e_{1} e_{2})]]Γπ)uζκ = C[[e_{1}]]Γ(C[[e_{2}]]Γ(jsr π))uζκ by (18)
= E[[e_{1}]](u ∘ Γ)(λx.C[[e_{2}]]Γ(jsr π)u(x :: ζ)κ) by (20) for e_{1}
= E[[e_{1}]](u ∘ Γ)(λx.E[[e_{2}]](u ∘ Γ)
(λy.(jsr π)u(y :: x :: ζ)κ)) by (20) for e_{2}

Now (12) could be applied but it requires a closure record below the top of the stack. Here we have to be more precise than in case 2 because the closure record contains fields which will be needed later. Lets try expanding the right hand side:

E[[(e_{1} e_{2})]](u ∘ Γ)(λz.πu(z :: ζ)κ) = E[[e_{1}]](u ∘ Γ)(λx.E[[e_{2}]](u ∘ Γ)(λy. apply xy(λz.πu(z :: ζ)κ))

Hence it is sufficient to prove that

(jsr π)u(y :: x :: ζ)κ = apply xy(λz.πu(z :: ζ)κ)

for any x, y : Val. Again when x is not a procedure closure we assume that the abstract machine stops and returns error so by (6) the above equation holds. Otherwise x must be of the form in_{R}(closure u′π′) and

(jsr π)u(y :: x :: ζ)κ = (jsr π)u(y :: (in_{R}(closure u′π′)) :: ζ)κ
= π′(ext_{R} yu′)⟨⟩(cont πuζκ)  by (12)
= (closure u′π′)y(cont πuζκ)  by (14)
= apply xy(cont πuζκ)  by (6)
= apply xy(λz.πu(z :: ζ)κ)  by (15)

4. e ≡ λI.e′

(C[[λI.e′]]Γπ)uζκ = (close(C[[e′]](ext_{C} IΓ) rts)π)uζκ by (19)

= πu(in_{R}(closure u(C[[e′]](ext_{C} IΓ) rts)) :: ζ)κ by (11)
= πu(in_{R}(λvκ′′.(C[[e′]](ext_{C} IΓ) rts)(ext_{R} vu)⟨⟩κ′′) :: ζ)κ by (14)
= πu(in_{R}(λvκ′′.E[[e′]]((ext_{R} vu) ∘ (ext_{C} IΓ))
(λz. rts(ext_{R} vu)(z :: ⟨⟩)κ′′)) :: ζ)κ by (20)
= πu(in_{R}(λvκ′′.E[[e′]]((u ∘ Γ)[v/I])
(λz. rts(ext_{R} vu)(z :: ⟨⟩)κ′′)) :: ζ)κ by (8)

By expanding the right hand side we obtain

E[[λI.e′]](u ∘ Γ)(λz.πu(z :: ζ)κ) = πu(in_{R}(λvκ′′.E[[e′]]((u ∘ Γ)[v/I])(return κ′′)) :: ζ)κ by (4)
= πu(in_{R}(λvκ′′.E[[e′]]((u ∘ Γ)[v/I])(λz.κ′′z)) :: ζ)κ  by (7)

so it is sufficient to prove that

rts(ext_{R} vu)(z :: ⟨⟩)κ′′ = κ′′z

for any v, z : Val, u : Display, κ′′ : Cont. The return continuation κ′′ has to be of the form cont π′u′ζ′κ′ so

rts(ext_{R} vu)(z :: ⟨⟩)κ′′ = rts(ext_{R} vu)(z :: ⟨⟩)(cont π′u′ζ′κ′)
= π′u′(z :: ζ′)κ′  by (13)
= (cont π′u′ζ′κ′)z  by (15)
= κ′′z

QED.

3 The Theorem-Prover Isabelle

3.1 A short introduction to Isabelle

Isabelle-91 is a general theorem prover developed by Larry Paulson and Tobias Nipkow [3, 6, 7]. It was intended to allow complex proof checking and/or searching in various types of logics. Hence the user may define his own logic, complete with the concrete and abstract syntax, axioms and rules. User-defined logics are called object logics. A version of intuitionistic higher-order logic, called the meta-logic, is used to describe the object logic and proofs within object logic. For example, axioms and rules of the object logic as well as the state of the proof are all expressed as suitable meta-logic formulae.

The typical proof state is of the form Γ ⊢ [ϕ_{1}; …; ϕ_{n}] ⟹ ϕ where Γ contains meta-level assumptions, ϕ is the original goal of the proof and ϕ_{1}, …, ϕ_{n} are the current subgoals which remain to be proved. The starting proof state is Γ ⊢ ϕ ⟹ ϕ, so initially there is only one subgoal, which is equal to the main goal. By applying object-level derivation rules to the current proof state, the set of subgoals is transformed into another one which is hopefully easier to prove. Hence, most of the time we apply the rules backwards, building the proof in a top down fashion. The built-in tactic resolve_tac implements this basic proof step. Its arguments are the list of rules to be applied and a subgoal number. Isabelle also allows forward application of rules but this feature is not used in our example. Also all free variables in our main goal are fixed during the proof, so the main goal remains the same all the time. The proof is successful if one reaches the state Γ ⊢ ϕ i.e. when there are no remaining subgoals.

Before one starts proving anything one needs to define an object logic within which proofs are performed. The theory pure_thy is the pure meta-logic used by Isabelle. Other theories are defined either as extensions to existing theories or as compositions of existing theories. Isabelle supports a large class of possible object logics, much more complex than is needed in this example. Several object logics (like First-Order Logic, Constructive Type Theory) are predefined in the Isabelle distribution but we do not use any of these.

Since our proof relies mainly on term rewriting and uses very little logical reasoning we decided to build our own logic from scratch. It is much simpler than any other logic supplied with Isabelle. We tried to do as much as possible within the Isabelle’s meta-logic rather than at the object level. Although it simplified many things and also improved efficiency we are not sure how well this approach will fit more complex proofs.

3.2 Lambda calculus as an Object Logic

Since the correctness of our compiler is expressed relative to the denotational semantics of the source language it seems natural to start with the simply-typed lambda calculus as the object logic. However, it has to be extended by constants and rules defining the semantics, abstract machine and compiler which are dependent on the source language. Hence we decided to define basic lambda calculus as a separate theory (object logic) in Isabelle to provide a common basis for other examples.

We first describe informally what we need to define object logic and then we present the definitions in actual Isabelle’s syntax. Some new types have to be defined, corresponding to the syntactic categories (nonterminals) in the object logic. Isabelle-91 has an order-sorted polymorphic type system [4, 5] which is more or less like ML type system except that there is an additional level of sorts involved. Sorts classify types and every type is of some sort. Sorts are partially ordered by the relation < (with the intuitive meaning of set inclusion). The purpose of sorts is to restrict the class of types that type variables range over. Each type variable ranges over some sort and may be instantiated only by types of that sort.

The following example of how order-sorted polymorphism may be used in practice is given in [7]. In Standard ML the equality operator = is polymorphic but can be applied only to objects of so called equality types. For instance, one cannot compare functions since function types are never equality types. Using order-sorted polymorphism we can model this by having a sort any of all types and sort eq of equality types. Of course eq < any. The equality type system can be described as follows:

SORTS eq < any

TYPES

bool : eq
int : eq
list : (eq) eq
list : (any) any
∗ : (any, any) any
∗ : (eq, eq) eq
→ : (any, any) any
ref : (any) eq

CONSTS = : α_{eq} → α_{eq} → bool

Arities of type constructors are written (s_{1}, …, s_{n})s in order to avoid confusion with functions types like t_{1} → t_{2}. Type variables are subscripted to indicate the subset of types they range over: α_{eq} ranges over all types of sort eq. From the above signature it follows that int, int list and int ∗ bool are all of sort eq, int → int ref is of sort any and not of sort eq, whereas (int → int) ref is again of sort eq (and hence also of sort any).

In Isabelle’s meta-logic there are two predefined sorts (they are part of pure_thy). Sort any is the sort of all types. Every other sort is supposed to be a subset of any. Sort logic is the sort of all syntactic categories of the object logic, such as terms, formulae, contexts, and object level types (if they exist in the object logic). Meta-level abstraction and quantification are possible over types of the sort logic. All types we are going to define will be of that sort although some of them will be also of the sort term.

We define term as a subsort of logic (i.e. term < logic). The sort term will be the sort of all the types of terms in our theory (like values, stacks, continuations, environments). Since those types are dependent on the particular language we are going to describe, none of them is defined in the basic lambda calculus theory; they will be defined later in the theory extensions. However, these types will be closed under the formation of function types. Therefore we define the polymorphic type constructor arrow. This constructor takes two types of the sort term and returns a new type also of the sort term. Thus the introduction of the sort term ensures that the function types may only be constructed from the lambda calculus types and not from formulae, for instance.

We define the type of the object logic formulae, traditionally called o (of sort logic, but not of sort term). For our logic there will be only one form of object formula: the equation.

Isabelle uses Standard ML as a command language so all definitions and proofs have the form of ML programs that are executed in an environment containing Isabelle’s types and primitives. The expression

val lambda_thy = extend_theory pure_thy "LAMBDA"
                          ([("term", ["logic"])],
                           [],
                           [(["o"], ([], "logic")),
                            (["arrow"], (["term", "term"], "term"))],
                           [(["norm"], "'a => 'a")],
                           Some (lambda_sext))
                          lambda_rules;

defines a theory with the name LAMBDA as the extension of pure_thy. The pure theory is extended by several new elements: a new sort term, the type constructors o and arrow (basic types are just nullary type constructors), the syntax extensions lambda_ext, and the rules lambda_rules. Of course the data structures lambda_sext and lambda_rules have to be defined earlier but we need to have new sorts and types first to talk about other elements. In practice, as can be seen from the above definition, all parts of the logic specification are just data structures passed as arguments to the built-in function extend_theory, so there is no circularity involved. The new constant norm, not mentioned above, is required by Isabelle’s built-in simplification module and its meaning is not relevant to the further discussion.

The syntax extension describes the concrete and abstract syntax of the object logic. Without going into too much detail about the particular conventions we may say that the syntax is described by a context free priority grammar [7] with additional information about types and constants used for abstract syntax representation. One may also specify print and/or parse translation functions which are useful when the abstract syntax differs significantly from the concrete syntax. In our case the definition of the syntax extension is as follows:

val lambda_mixfix =
[
    Infixl("=", "['a, 'a] => o", 50),
    Infixl("*", "[('a, 'b)arrow, 'a] => 'b", 70),
    Binder("lambda ", "'a", "'b", "('a, 'b)arrow", "lambda", 60, 60),
    Mixfix("(_)", "o => prop", "Trueprop", [0], 5),
    Infixl("<->", "[o, o] => o", 45)
];
val lambda_sext = Sext{mixfix = lambda_mixfix,
                       parse_translation = [],
                       print_translation = []};

There are five productions added by the theory LAMBDA (in addition to those in the pure Isabelle). The = sign is our only formula constructor. Its type is "['a, 'a] = > o" which means that it takes two objects of the type 'a (where 'a is a type variable) and returns an object of type o i.e. an object level formula. In Isabelle a type variable without a sort subscript by default ranges over the most recently declared sort in the arguments of extend_theory. In our case the type variables 'a and 'b range over the sort term (since this is the only new sort) so the equality is defined properly only for lambda calculus terms of the same type. The * is the concrete syntax operator for object level application. Its type is "[('a, 'b)arrow, 'a] => 'b" which is what we expect. The definition of the abstraction operator lambda is less obvious since Isabelle uses higher-order abstract syntax for binding operators (like abstraction or quantifiers). Moreover, bound variables are replaced by de Bruijn indices which requires additional actions during parsing and printing. Hence the special production constructor Binder is used, which defines automatically proper parse and print translations. The fourth production defines an implicit (i.e. without any concrete syntax) conversion from object level formulae to meta level formulae (of the predefined type prop). The symbol <-> defined in the last production is the object-level equivalence relation and is used only by the normalization module. The numbers at the end of each production are the priorities of the productions and nonterminals. Shortly, application has greater priority than abstraction and equality has the lowest priority. Finally no parse or print translations have to be defined since they are already provided by Binder.

The axioms and rules of theory LAMBDA are basically the rules of the untyped lambda calculus.

val lambda_rules =
[
    ("refl",         "M = M"),
    ("sym",          "M = N ==> N = M"),
    ("trans",        "[| M = N; N = P |] ==> M = P"),

("normr",        "x = norm(x)"),
("norml",        "norm(x) = x"),
("congr",        "[| M = M'; N = N' |] ==> M * N = M' * N'"),
("xi",
         "(!! a . M(a) = N(a)) ==> (lambda x . M(x)) = (lambda x . N(x))"),
("beta",         "(lambda x . M(x)) * N = M(N)"),
("eta",          "lambda x . M * x = M"),
("ext",          "(!!x . M * x = N * x) ==> M = N"),
("eqvrefl",      "p <-> p"),
("eqvtrans",     "[| p <-> q;  q <-> r |] ==> p <-> r"),
("red1",         "[| P <-> Q;  P |] ==> Q"),
("red2",         "[| P <-> Q;  Q |] ==> P"),
("eqvcong",      "[| x1 = x2;  y1 = y2 |] ==> (x1 = y1) <-> (x2 = y2)"),
("subst",        "M = N ==> P(M) ==> P(N)")
];

There are no type inference rules because all the typing information is handled by Isabelle at the meta-level. Accordingly there is no judgement of the form A ⊢ e : t. The rules normr, norml, eqvrefl, eqvtrans, red1, red2, eqvcong and subst are used only by the simplification module and do not occur in interactive proofs.

Once the theory is defined, the rules are accessible through Isabelle’s function get_axiom. For easier access the rules are bound to ML identifiers. For instance, after executing

val beta = get_axiom lambda_thy "beta";

the rule beta is accessible by the ML identifier with the same name.

3.3 Tactics and Tacticals

Now it’s time to define some tactics which implement frequently repeated proof steps. Isabelle provides built-in operators (called tacticals) which are useful for combining primitive tactics into more powerful ones. Here we describe informally the meaning of those tacticals which are used in our example. For a more precise definition see [7].

1. tac1 ORELSE tac2

Tries to execute tac1 and if it fails executes tac2

2. tac1 THEN tac2

Executes tac1 and then executes tac2 in the resulting proof state.

3. REPEAT tac

Repeats execution of tac until it fails.

4. SOMEGOAL tacfun

Here tacfun is a function which given a subgoal number returns a tactic. tacfun is applied to every subgoal number and the resulting tactic is executed. The process stops when the tactic succeeds for some goal. The order of trials is from the last subgoal to the first.

5. TRYALL tacfun

Applies tacfun to every subgoal number (from last to first) and executes the resulting tactic.

The most fundamental proof step is the term normalization relative to a given set of rewrite rules. The hard work is done by the Isabelle’s built-in simplification module which can be generated by applying the functor SimpFun. Therefore first thing to do is to define the structure Simp_data which is passed to SimpFun

val lambda_congr_rules = [congr, xi];
structure Simp_data: SIMP_DATA =
struct
fun auto_tac i = resolve_tac [refl] i
val case_splits = []
fun dest_red (_$ (c $ ta $ tb)) = (c, ta, tb)
fun mk_rew_rules th = [schemify th]
val norm_thms = [(normr, norml)]
val red1 = red1
val red2 = red2
val refl_thms = [refl, eqvrefl]
val subst_thms = [(subst, "P")]
val trans_thms = [trans, eqvtrans]
end;

This structure contains rules and functions which the user has to provide and which are used by the normalization module. The rules state the necessary properties of equality and the <-> relation mentioned above. The most important function is mk_rew_rules. This function given a theorem returns a list of rewrite rules (in our case equalities) derived from this theorem. Since our only theorems are just equalities, all we have to do is to replace meta-level quantifiers by schematic variables which may be instantiated in the course of rewriting. The auxiliary function schemify is used for that purpose.

fun schemify th =
    let val {maxidx, ...} = rep_thm th in
        forall_elim_vars (maxidx + 1) th
    end;

After applying SimpFun to the above structure

structure Simp = SimpFun (Simp_data);
open Simp;

the structure Simp is created, which is the normalization module:

structure Simp :
sig
type simpset
val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
val ASM_SIMP_TAC : simpset -> int -> tactic
val CASE_TAC : simpset -> int -> tactic
val SIMP_CASE2_TAC : simpset -> int -> tactic
val SIMP_CASE_TAC : simpset -> int -> tactic
val SIMP_TAC : simpset -> int -> tactic
val SIMP_THM : simpset -> thm -> thm
val addcongs : simpset * thm list -> simpset
val addrews : simpset * thm list -> simpset
val delcongs : simpset * thm list -> simpset
val delrews : simpset * thm list -> simpset
val empty_ss : simpset
val extract_free_congs : unit -> thm list
val mk_congs : theory -> string list -> thm list
val mk_typed_congs : theory -> (string * string) list -> thm list
val print_ss : simpset -> unit

    val tracing : bool ref
  end

Several of the features provided by Simp are of particular interest to us. The type simpset together with the functions addcongs, addrews, delcongs and delrews defines sets of theorems and is used to represent the sets of simplification (congruence or rewrite) rules (which may be different for different invocations of SIMP_TAC). The tactic SIMP_TAC is the normalization tactic which works with unconditional rewrite rules. It has two parameters, the first being the set of simplification rules and the second being the subgoal number.

It often happens that the normalization tactic affects only the relatively small subterms since the context has been already normalized and is the same as the corresponding context on the other side of the equation. To improve readability as well as efficiency we want to avoid such situations. The current proof state should reflect only those parts of the goal that are not yet proved to be equal. To achieve this, we extend the tactic SIMP_TAC provided by Simp to decompose lambda calculus terms using congruence rules. This also makes normalization easier to use in interactive proof searching.

We do not know in advance what either the congruence or the rewrite rules will be but we assume that for a given object-logic the set of the congruence rules is fixed whereas the set of rewrite rules may be different for each invocation of the normalization tactic. Thus we provide a curried function mk_normalize which can be used to produce a version of normalization tactic specialized for the given logic yet accepting the set of rewrite rules as a parameter. The rules beta, eta and eqvcong are always included in the set of simplification rules.

The idea behind the decomposition tactic is to apply congruence rules as long as the number of subgoals which are not solvable immediately (by reflexivity) does not increase. This means that congruence rules with one premise (like ξ) may be always applied safely i.e. without the risk that the new subgoal will be unsolvable. For the other rules it doesn’t hold however. If the current subgoal is MN = M′N′ and we apply the application congruence rule we will get two subgoals M = M′ and N = N′ which are not always provable even if the original goal was. Our tactic tries to detect such situations by applying congruence rules only if one of the resulting subgoals is solvable immediately by reflexivity.

The tactic returned by mk_normalize first partitions the list of congruence rules according to the number of premises (1 or more). The basic decomposition step (decompose_step) is an alternative of two tactics. The first tactic tries to apply a single premise congruence rule to one of the subgoals. The second tactic tries to apply a multiple premises congruence rule but rejects those resulting states in which the reflexivity rule cannot be applied afterwards. This works well assuming that there are no trivial subgoals to begin with. Hence the decomposition tactic decompose_tac first removes all trivial equations and then applies decomposition step repeatedly as long as possible. Our normalization tactic first calls SIMP_TAC from the normalization module with the assumptions (rewrite rules) added to the set of simplification rules. Then the decomposition tactic is called to remove identical contexts.

val defsimpset = (empty_ss addcongs [eqvcong]) addrews [beta, eta];
fun mk_normalize congr_rules assumptions i =
    let val (congr1, congr2) = partition (fn t => length (prems_of t) = 1) congr_rules;
        val decompose_step =
               (SOMEGOAL (resolve_tac congr1))
            ORELSE
               ((SOMEGOAL (resolve_tac congr2))
                THEN
                (SOMEGOAL (resolve_tac [refl])));
        val decompose_tac =
            (REPEAT (SOMEGOAL (resolve_tac [refl])))
            THEN
            (REPEAT decompose_step)
        val simps = defsimpset addcongs congr_rules
    in
        (SIMP_TAC (simps addrews assumptions) i)
        THEN
        decompose_tac
    end;

4 The theory of the language L_{add} and its semantics

The theory LAMBDA from the previous section could only be used for reasoning in pure lambda calculus. Now we extend it by additional constants, types and rules to obtain a theory within which theorems about L_{add} can be stated and proved. The definition starts with domains, corresponding to those defined in Section 2.

infixr ==>  --> ;
fun typ1 ==> typ2 = typ1 ^" => " ^typ2;
fun typ1 --> typ2 = "(" ^typ1 ^", " ^typ2 ^")arrow";
val Ide    = "ident";
val Expr   = "exp";
val Cmd    = "cmd";
val Int    = "int";

val LexAddr= "LexAddr";
val Stack  = "stack";
val Val    = "val";
val Cont   = Val --> Cmd;
val Proc   = Val --> Cont --> Cmd;
val Env    = Ide --> Val;
val Stab   = Ide --> LexAddr;
val Display= LexAddr --> Val;
val Prog   = Display --> Stack --> Cont --> Cmd;

In the logic definition all types are specified as type expressions in their concrete syntax. However, Isabelle does not allow the definition of type names in concrete syntax. To overcome this, strings containing type expressions are bound to ML identifiers. They may be combined using to constructors ==> and --> which correspond directly to the concrete syntax constructors: => (meta-level function type) and arrow (object-level function type). Although this may not seem very elegant, it is the easiest way (known to us) to overcome Isabelle’s lack of type name definitions.

The theory LADD of the language L_{add} is obtained as an extension of LAMBDA:

val ladd_thy = extend_theory lambda_thy "LADD"
                            ([],
                             [],
                             [(["exp"], ([], "logic")),
                              (["cmd", "int", "LexAddr", "stack", "ident", "val"],
                                     ([], "term"))],
                             [(["Ide"],           "ident => exp"),
                              (["Add", "App"],    "[exp, exp] => exp"),
                              (["Abs"],           "[ident, exp] => exp"),
                              (["E"],             Expr ==> Env --> Cont -->Cmd),
                              (["C"],             Expr ==> Stab ==> Prog ==> Prog),
                              (["sum", "apply"],  Val --> Val --> Cont --> Cmd),
                              (["return"],        Cont --> Cont),
                              (["plus"],          Int ==> Int ==> Int),
                              (["push"],          Val ==> Stack ==> Stack),
                              (["closure"],       Display ==> Prog ==> Proc),
                              (["int_val"],       Int ==> Val),
                              (["proc_val"],      Proc ==> Val),
                              (["extend"],        Ide ==> Val ==> Env ==> Env),
                              (["fetch"],         LexAddr ==> Prog ==> Prog),
                              (["close"],         Prog ==> Prog ==> Prog),

                          (["add", "jsr"],    Prog ==> Prog),
                          (["rts"],           Prog),
                          (["empty_stack"],   Stack),
                          (["cont"], Prog ==> Display ==> Stack ==> Cont ==> Cont),
                          (["extr"],          Val ==> Display ==> Display),
                          (["extc"],          Ide ==> Stab ==> Stab),
                          (["error"],         Cmd),
                          (["IH"],            "exp => o")],
                         None)

[
("E_Ide",   "E(Ide(I)) = lambda ro k . k * (ro * I)"),
("E_Add",   "E(Add(e1, e2)) = lambda ro k . E(e1) * ro * (lambda v1 .     \
\                    E(e2) * ro * (lambda v2 . sum * v1 * v2 * k))"),
("E_App",   "E(App(e1, e2)) = lambda ro k . E(e1) * ro * (lambda v1 .     \
\                    E(e2) * ro * (lambda v2 . apply * v1 * v2 * k))"),
("E_Abs",   "E(Abs(I, e)) = lambda ro k . k * proc_val(lambda v k' .      \
\                    E(e) * extend(I, v, ro) * (lambda v . return * k' * v))"),
("sumii",   "sum * int_val(n1) * int_val(n2) =                            \
\                    lambda k . k * int_val(plus(v1, v2))"),
("sump1",   "sum * proc_val(p1) * v2  = lambda k . error"),
("sump2",   "sum * v1 * proc_val(p2)  = lambda k . error"),
("applyp",  "apply * proc_val(p) * v      = lambda k . p * v * k"),
("applyi",  "apply * int_val(n) * v       = lambda k . error"),
("return",  "return = lambda k v . k * v"),
("C_Ide",   "C(Ide(I), G, pi) = fetch(G * I, pi)"),
("C_Add",   "C(Add(e1, e2), G, pi) = C(e1, G, C(e2, G, add(pi)))"),
("C_App",   "C(App(e1, e2), G, pi) = C(e1, G, C(e2, G, jsr(pi)))"),
("C_Abs",   "C(Abs(I, e), G, pi) = close(C(e, extc(I, G), rts), pi)"),
("addii",   "add(pi) * u * push(int_val(n2), push(int_val(n1), zeta)) =   \
\                       pi * u * push(int_val(plus(n1, n2)), zeta)"),
("addp1",   "add(pi) * u * push(proc_val(p2), push(v1, zeta)) =           \
\                       lambda k . error"),

("addp2",   "add(pi) * u * push(v2, push(proc_val(p1), zeta)) =           \
\                       lambda k . error"),
("fetch",   "fetch(l, pi) =                                               \
\                       lambda u zeta k . pi * u * (push(u*l, zeta)) * k"),
("close",   "close(pi', pi) =                                             \
\      lambda u zeta k . pi * u  * push(proc_val(closure(u, pi')), zeta) * k"),
("jsrp",    "jsr(pi) * u *                                                \
\                  push(v, push(proc_val(closure(u', pi')), zeta)) * k =      \
\                     pi' * extr(v, u') * empty_stack * cont(pi, u, zeta, k)"),
("jsri",    "jsr(pi) * u * push(v, push(int_val(n), zeta)) * k = error"),
("rts",     "rts * u * push(n, zeta) * cont(pi', u', zeta', k') =         \
\                       pi' * u' * push(n, zeta') * k'"),
("cont",    "cont(pi, u, zeta, k) =                                       \
\                       lambda z . pi * u * push(z, zeta) * k"),
("closure", "closure(u, pi) =                                             \
\                       lambda v k . pi * extr(v, u) * empty_stack * k"),
("contE",   "(!! pi u zeta k . P(cont(pi, u, zeta, k))) ==> P(k')"),
("closureE","(!! u pi . P(closure(u, pi))) ==> P(v)"),
("val_ind",  "[| !!n . P(int_val(n));  !!p . P(proc_val(p)) |] ==> P(v)"),
("push",    "[| a = b;  x = y |] ==> push(a, x) = push(b, y)"),
("proc",    "p = p' ==> proc_val(p) = proc_val(p')"),
("extend",  "lambda id . extr(v, u) * (extc(I, G) * id) =                 \
\                       extend(I, v, (lambda x . u * (G * x)))"),
("IH",      "Trueprop(IH(e)) ==                                           \
\                  (!! G pi . C(e, G, pi) =                                   \
\                      lambda u zeta k . E(e) * (lambda x . u * (G * x)) *    \
\                               (lambda z . pi * u * push(z, zeta) * k))"),
("IND",     "[| !! I . P(Ide(I));                                         \
\                   !! e1 e2 . [| P(e1); P(e2) |] ==> P(Add(e1, e2));         \
\                   !! e1 e2 . [| P(e1); P(e2) |] ==> P(App(e1, e2));         \
\                   !! I e . P(e) ==> P(Abs(I, e)) |]                         \

\                       ==> P(e)")
];

No new sorts are added this time but there are few new types. The type exp is the type of expressions (programs) from the source language L_{add} so it is of the sort logic rather than term. All other new types (cmd, int, LexAddr, stack, ident, val) corresponding to the semantic domains are of the sort term since they are the types of the lambda calculus terms.

Most of the constant definitions are straightforward and do not require explanations. Combinators are parameterized by meta-level abstraction. Once applied to arguments they become lambda calculus terms and may be further applied at the object level. The constructors proc_val and int_val are used to express the fact that val is a disjoint union of int and proc. This is similar to ML’s datatype constructor and allows us to overcome the lack of recursive types. The predicate IH whose domain are source expressions is the induction hypothesis.

The rules of the theory LADD give interpretation to some constants and define denotational semantics, compiler and the abstract machine. Most of them are direct translations of the equations from section 2.

The rules push and proc are additional congruence rules. Actually, equality is congruent with everything but only those congruence rules which are used in the proof are defined. The rules defining the combinators sum and apply as well as the machine instructions add and jsr use pattern matching to specify their behavior for different types of values (integers or procedures). The rules contE and closureE specify respectively that a continuation has to be of the form cont(pi, u, zeta, k) and a procedure value has to be of the form closure(u, pi). The rule val_ind is the (trivial) induction rule for values. It says that to prove that a given predicate holds for all values it is sufficient to prove that it holds for both integers and procedures. The rule IH is the definition of the induction hypothesis. The constant Trueprop which appears in this rule is needed for syntactic reasons and may be ignored. The last rule, named IND, is the induction principle for source expressions.

To complete the definition of the theory LADD, a specialized versions of the normalization tactic is defined:

val ladd_congr_rules = [push, proc] @ lambda_congr_rules;
val normalize = mk_normalize ladd_congr_rules;
fun norm assumptions i = by (normalize assumptions i);

Here normalize is the proper tactic returned by mk_normalize as described above and norm is its command version. Commands have side effects — they change the state of the proof. The built-in generic command by just invokes the specified tactic.

5 The proof of the correctness criterion

The proof we are going to machine check is sufficiently complex to justify the introduction of some lemmas. The obvious choices are the four cases of the induction. In each case the main goal is the correctness criterion instantiated for the particular form of the source expression. This is an object level formula — an equation. The proof is performed essentially by normalizing both sides of the equation, with some other steps inserted as needed. Normalization uses rewrite rules which are either axioms from the theory definition, previously proved lemmas or induction hypotheses.

1. Identifier.

We have to prove that (20) holds for all identifiers. There are no assumptions in that case. The Isabelle’s command goal specifies a goal to be proved and enters the initial proof state. In the following presentation the lines beginning with - (which is the ML’s prompt) denote the actual user’s input. The remaining lines belong to the output printed by Isabelle or ML itself. After stating the goal IH(Ide(I))

- goal ladd_thy "IH(Ide(I))";

the state ⊢ IH(Ide(I)) ⟹ IH(Ide(I)) is entered. Isabelle responds:

Level 0
IH(Ide(I))
 1. IH(Ide(I))
val it = [] : thm list

indicating that the main goal is IH(Ide(I)) and there is one current subgoal which is also equal to IH(Ide(I)). Normally goal returns a list of assumptions which is empty in this case so we don’t even have to save it. The first thing we have to do is to expand the definition of IH using the appropriate rule. The Isabelle’s tactic rewrite_goals_tac rewrites all subgoals using a list of meta-level rewrite rules

- by (rewrite_goals_tac [IH]);
Level 1
IH(Ide(I))
 1. !!G pi.
       C(Ide(I),G,pi) =
       lambda u zeta k.
          E(Ide(I)) * (lambda x. u * (G * x)) *
          (lambda z. pi * u * push(z,zeta) * k)
val it = () : unit

All that must be done now is the normalization of both sides of the equation using the proper definitions of C, E, and fetch (which appears after expanding C). Isabelle responds that there are no remaining subgoals so the proof of that lemma is completed:

- norm [C_Ide, E_Ide, fetch] 1;
Level 2
IH(Ide(I))
No subgoals!
val it = () : unit

Finally the proved lemma is bound to an ML identifier since it will be needed later

- val IH_Ide = result();
val IH_Ide = Thm # : thm

2. Addition.

This case is more complex since the induction hypothesis must be used to prove the goal. The list of premises (meta-level assumptions) returned by goal has to be bound to an ML identifier and saved for later use.

- val prems = goal ladd_thy "[| IH(e1);  IH(e2) |] ==> IH(Add(e1, e2))";
Level 0
IH(Add(e1,e2))
 1. IH(Add(e1,e2))
val prems = [#,#] : thm list
- by (rewrite_goals_tac [IH]);
Level 1
IH(Add(e1,e2))
 1. !!G pi.
       C(Add(e1,e2),G,pi) =
       lambda u zeta k.
          E(Add(e1,e2)) * (lambda x. u * (G * x)) *
          (lambda z. pi * u * push(z,zeta) * k)
val it = () : unit

Similarly as above we first expand the definitions of C and E using proper rules.

- norm [C_Add, E_Add] 1;
Level 2

IH(Add(e1,e2))
 1. !!G pi.
       C(e1,G,C(e2,G,add(pi))) =
       lambda u zeta k.
          E(e1) * (lambda x. u * (G * x)) *
          (lambda v1.
              E(e2) * (lambda x. u * (G * x)) *
              (lambda v2.
                  sum * v1 * v2 * (lambda z. pi * u * push(z,zeta) * k)))
val it = () : unit

Now it is time to apply the induction hypothesis to both e1 and e2. To do this we have to expand the definition of IH in both premises using the built-in function rewrite_rule. After the expansion the assumptions become rewrite rules which can be used with the normalization tactic.

- norm (map (rewrite_rule [IH]) prems) 1;
Level 3
IH(Add(e1,e2))
 1. !!G pi a aa ab ac ad.
       add(pi) * a * push(ad,push(ac,aa)) * ab =
       sum * ac * ad * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

Notice how the common context has been stripped off by the decomposition tactic. Also bound variables have been renamed because of substitution. The rules describing the action of the add instruction can only be applied for specific types of values on the stack. Hence various cases have to be considered, corresponding to the three rules we have available. By applying the val_ind rule the current goal can be split into the two subgoals depending on the type of the value on the top of the stack. However simple resolution with the rule val_ind is not appropriate in this case, since it can result in a large (possibly infinite) number of unifiers. We use another built-in tactic res_inst_tac which allows to instantiate free variables in a rule before the resolution. In our case the free variable v from val_ind has to be instantiated as the term ad from the current subgoal, which is the value on the top of the stack.

- by (res_inst_tac [("v", "ad")] val_ind 1);
Level 4
IH(Add(e1,e2))
 1. !!G pi a aa ab ac ad n.

       add(pi) * a * push(int_val(n),push(ac,aa)) * ab =
       sum * ac * int_val(n) * (lambda z. pi * a * push(z,aa) * ab)
 2. !!G pi a aa ab ac ad p.
       add(pi) * a * push(proc_val(p),push(ac,aa)) * ab =
       sum * ac * proc_val(p) * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

Subgoal 1 has to be split further depending on the type of the value below the top of the stack. This time we instantiate v as ac, which is the value below the top of the stack. After applying val_ind we get

- by (res_inst_tac [("v", "ac")] val_ind 1);
Level 5
IH(Add(e1,e2))
 1. !!G pi a aa ab ac ad n na.
       add(pi) * a * push(int_val(n),push(int_val(na),aa)) * ab =
       sum * int_val(na) * int_val(n) * (lambda z. pi * a * push(z,aa) * ab)
 2. !!G pi a aa ab ac ad n p.
       add(pi) * a * push(int_val(n),push(proc_val(p),aa)) * ab =
       sum * proc_val(p) * int_val(n) * (lambda z. pi * a * push(z,aa) * ab)
 3. !!G pi a aa ab ac ad p.
       add(pi) * a * push(proc_val(p),push(ac,aa)) * ab =
       sum * ac * proc_val(p) * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

Now each subgoal corresponds to one of the add (or sum) rules. As soon as the goal is split into the proper cases the rest of the proof is easy. After normalizing with the rules addii and sumii the first subgoal is solved and disappears (the remaining subgoals are renumbered).

- norm [addii, sumii] 1;
Level 6
IH(Add(e1,e2))
 1. !!G pi a aa ab ac ad n p.
       add(pi) * a * push(int_val(n),push(proc_val(p),aa)) * ab =
       sum * proc_val(p) * int_val(n) * (lambda z. pi * a * push(z,aa) * ab)
 2. !!G pi a aa ab ac ad p.
       add(pi) * a * push(proc_val(p),push(ac,aa)) * ab =
       sum * ac * proc_val(p) * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

This step has to be repeated two more times using the rules addp2 and sump1 to solve the first subgoal and the rules addp1 and sump2 to solve the second subgoal.

- norm [addp2, sump1] 1;
Level 7
IH(Add(e1,e2))
 1. !!G pi a aa ab ac ad p.
       add(pi) * a * push(proc_val(p),push(ac,aa)) * ab =
       sum * ac * proc_val(p) * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit
- norm [addp1, sump2] 1;
Level 8
IH(Add(e1,e2))
No subgoals!
val it = () : unit
- val IH_Add = result();
val IH_Add = Thm # : thm

3. Application.

In this case the first steps should be of no surprise to the reader. We expand the definition of IH, expand the definitions of C and E and apply the induction hypothesis (with IH also expanded).

- val prems = goal ladd_thy "[| IH(e1);  IH(e2) |] ==> IH(App(e1, e2))";
Level 0
IH(App(e1,e2))
 1. IH(App(e1,e2))
val prems = [#,#] : thm list
- by (rewrite_goals_tac [IH]);
Level 1
IH(App(e1,e2))
 1. !!G pi.
       C(App(e1,e2),G,pi) =
       lambda u zeta k.
          E(App(e1,e2)) * (lambda x. u * (G * x)) *
          (lambda z. pi * u * push(z,zeta) * k)
val it = () : unit
- norm [C_App, E_App] 1;
Level 2

IH(App(e1,e2))
 1. !!G pi.
       C(e1,G,C(e2,G,jsr(pi))) =
       lambda u zeta k.
          E(e1) * (lambda x. u * (G * x)) *
          (lambda v1.
              E(e2) * (lambda x. u * (G * x)) *
              (lambda v2.
                  apply * v1 * v2 * (lambda z. pi * u * push(z,zeta) * k)))
val it = () : unit
- norm (map (rewrite_rule [IH]) prems) 1;
Level 3
IH(App(e1,e2))
 1. !!G pi a aa ab ac ad.
       jsr(pi) * a * push(ad,push(ac,aa)) * ab =
       apply * ac * ad * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

To proceed further we have to consider two cases depending on the type of the value below the top of the stack. Again, we apply the rule val_ind with the proper instantiation of the free variable.

- by (res_inst_tac [("v", "ac")] val_ind 1);
Level 4
IH(App(e1,e2))
 1. !!G pi a aa ab ac ad n.
       jsr(pi) * a * push(ad,push(int_val(n),aa)) * ab =
       apply * int_val(n) * ad * (lambda z. pi * a * push(z,aa) * ab)
 2. !!G pi a aa ab ac ad p.
       jsr(pi) * a * push(ad,push(proc_val(p),aa)) * ab =
       apply * proc_val(p) * ad * (lambda z. pi * a * push(z,aa) * ab)

The first subgoal corresponds to an erroneous situation (one cannot apply integers) and can be solved using the rules jsri and applyi.

- norm [jsri, applyi] 1;
Level 5
IH(App(e1,e2))
 1. !!G pi a aa ab ac ad p.

       jsr(pi) * a * push(ad,push(proc_val(p),aa)) * ab =
       apply * proc_val(p) * ad * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

To solve the remaining subgoal the rule jsrp has to be applied. This rule requires that the value below the top of the stack is a closure record. Here is where the rule closureE comes into action. Every procedure is a closure so using this rule we can narrow further reasoning to closure records. This time we instantiate the free variable v from closureE to the procedure p from the current subgoal.

- by (res_inst_tac [("v", "p")] closureE 1);
Level 6
IH(App(e1,e2))
 1. !!G pi a aa ab ac ad p u pia.
       jsr(pi) * a * push(ad,push(proc_val(closure(u,pia)),aa)) * ab =
       apply * proc_val(closure(u,pia)) * ad *
       (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit

To complete the proof of this case we have to apply the rules jsrp and applyp and to further normalize using the rules closure and cont. This cannot be done in a single step, since we don’t want closure to be interpreted as a lambda calculus term in the place where it is supposed to be used as a data structure by jsr.

- norm [jsrp, applyp] 1;
Level 7
IH(App(e1,e2))
 1. !!G pi a aa ab ac ad p u pia.
       pia * extr(ad,u) * empty_stack * cont(pi,a,aa,ab) =
       closure(u,pia) * ad * (lambda z. pi * a * push(z,aa) * ab)
val it = () : unit
- norm [closure, cont] 1;
Level 8
IH(App(e1,e2))
No subgoals!
val it = () : unit
- val IH_App = result();
val IH_App = Thm # : thm

4. Abstraction.

Abstraction is even easier since we don’t have to deal with the issues of the types of values on the stack. As always, we start with expanding the definition of IH. Then as many rules as possible are applied in a single step. This includes the definitions of C and E, the induction hypothesis as well as the definitions of the instruction close and auxiliary combinators.

- val prems = goal ladd_thy "IH(e) ==> IH(Abs(I, e))";
Level 0
IH(Abs(I,e))
 1. IH(Abs(I,e))
val prems = [#] : thm list
- by (rewrite_goals_tac [IH]);
Level 1
IH(Abs(I,e))
 1. !!G pi.
       C(Abs(I,e),G,pi) =
       lambda u zeta k.
          E(Abs(I,e)) * (lambda x. u * (G * x)) *
          (lambda z. pi * u * push(z,zeta) * k)
val it = () : unit
- norm ([C_Abs, E_Abs, close, closure, extend] @ (map (rewrite_rule [IH]) prems)) 1;
Level 2
IH(Abs(I,e))
 1. !!G pi a aa ab ac.
       lambda z. rts * extr(ab,a) * push(z,empty_stack) * ac = return * ac
val it = () : unit

The variable ac above is of the type Cont and stands for continuation. A continuation has to have the form of a continuation record. The rule contE allows us to make use of this fact. The application of contE (with the proper instantiation) yields:

- by (res_inst_tac [("k'", "ac")] contE 1);
Level 3
IH(Abs(I,e))
 1. !!G pi a aa ab ac pia u zeta k.
       lambda z. rts * extr(ab,a) * push(z,empty_stack) * cont(pia,u,zeta,k) =
       return * cont(pia,u,zeta,k)
val it = () : unit

To solve the remaining subgoal we normalize relative to the rules rts, cont and return. Again, we have to do this in two steps to avoid interpreting cont as a lambda calculus term.

     - norm [rts, return] 1;
     Level 4
     IH(Abs(I,e))
      1. !!G pi a aa ab ac pia u zeta k.
            lambda z. pia * u * push(z,zeta) * k = cont(pia,u,zeta,k)
     val it = () : unit
     - norm [cont] 1;
     Level 5
     IH(Abs(I,e))
     No subgoals!
     val it = () : unit
     - val IH_Abs = result();
     val IH_Abs = Thm # : thm

To complete the proof we have to combine all the lemmas we have proved so far using the induction principle IND. This is a somewhat different kind of proof since it is performed on the meta-logic level and has little to do (if at all) with our lambda calculus logics. We want to prove that IH(e) holds for all e. After stating the goal and applying (backwards) the induction rule we have four subgoals which correspond to the four cases of the induction proof (and our four lemmas!).

- goal ladd_thy "IH(e)";
Level 0
IH(e)
 1. IH(e)
val it = [] : thm list
- by (resolve_tac [IND] 1);
Level 1
IH(e)
 1. !!I. IH(Ide(I))
 2. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(Add(e1,e2))
 3. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(App(e1,e2))
 4. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit

The first subgoal is solvable by resolution with the lemma IH_Ide.

- by (resolve_tac [IH_Ide] 1);
Level 2
IH(e)
 1. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(Add(e1,e2))
 2. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(App(e1,e2))
 3. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit

The addition case is slightly more complex since there are two assumptions. After applying the lemma IH_Add we have two trivial subgoals which have to be resolved by another built-in tactic

assume_tac.
- by (resolve_tac [IH_Add] 1);
Level 3
IH(e)
 1. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(e1)
 2. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(e2)
 3. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(App(e1,e2))
 4. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit
- by (assume_tac 1);
Level 4
IH(e)
 1. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(e2)
 2. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(App(e1,e2))
 3. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit
- by (assume_tac 1);
Level 5
IH(e)
 1. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(App(e1,e2))
 2. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit

The application lemma IH_App is used exactly in the same way

- by (resolve_tac [IH_App] 1);
Level 6
IH(e)

 1. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(e1)
 2. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(e2)
 3. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit
- by (assume_tac 1);
Level 7
IH(e)
 1. !!e1 e2. [| IH(e1); IH(e2) |] ==> IH(e2)
 2. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit
- by (assume_tac 1);
Level 8
IH(e)
 1. !!I e. IH(e) ==> IH(Abs(I,e))
val it = () : unit

The abstraction case is a little simpler since there is only one assumption.

- by (resolve_tac [IH_Abs] 1);
Level 9
IH(e)
 1. !!I e. IH(e) ==> IH(e)
val it = () : unit
- by (assume_tac 1);
Level 10
IH(e)
No subgoals!
val it = () : unit
- val IH_e = result();
val IH_e = Thm # : thm

This completes the compiler correctness proof implemented using Isabelle.

6 Conclusions

We showed how to use a fairly sophisticated theorem prover to implement a fairly simple proof of compiler correctness. There are a few considerations about the usefulness of the presented approach. First of all, the completion of the machine version of the proof took quite a long time, although the proof has been already known. There is a large overhead in preparing such proofs. Many things about Isabelle’s theory, usage and even internals have to be learned to successfully define an object logic and to perform proofs within it. We believe however, that this startup overhead is not so much of an issue as examples become larger and more complex. Moreover, many techniques can be used with little change for other denotational proofs.

Another question is how much of the proof has to be known in advance before one wants to use Isabelle to machine check it. Ideally, Isabelle should provide enough help to actually find the proof using itself. Although this is not the case yet, some of the aspects are addressed even in the above example. Comparing the informal and formal versions of the proof we can see that Isabelle’s version, although not simpler, often contains fewer steps thanks to the use of the normalization module. The other obvious benefit is that the user is freed from hand rewriting of sometimes long terms which occur during the proof.

Many aspects of our approach should be improved. For instance the proof in the current version contains the names of the variables generated automatically by Isabelle. They are used for instantiation when the tactic res_inst_tac is invoked. These names are implementation dependent and we should avoid referring to them in the proof source.

The fact that all logical reasoning is performed in meta-logic rather than at the object level may seem controversial. It is possible that this approach will be difficult to apply in more complex proofs. This is an area of possible future research.

It remains also an open question how this approach fits other machine/compiler models, particularly the Higher Order Assembly Language (HOAL) [2, 8]. We don’t know whether or not dealing with free variables will cause any significant problems.

References

[1] Clinger, W. “The Scheme 311 Compiler: An Exercise in Denotational Semantics,” Conf. Rec. 1984 ACM Symposium on Lisp and Functional Programming (August, 1984), 356–364.

[2] Kelsey, R., and Hudak, P. “Realistic Compilation by Program Transformation,” Conf. Rec. 16th Ann. ACM Symp. on Principles of Programming Languages (1989), 281–292.

[3] Nipkow, T. “Term Rewriting and Beyond — Theorem Proving in Isabelle,” Formal Aspects of Computing (1989) 1:320-338.

[4] Nipkow, T., Snelting, G. “Type Classes and Overloading Resolution via Order-Sorted Unification,” Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture, (1991) LNCS 523, 1-14

[5] Nipkow, T. “Order-Sorted Polymorphism in Isabelle,” Proc. 2nd Workshop on Logical Frameworks, Edinburgh, May 1991, 307-321 [6] Paulson, L.C., “The Foundation of a Generic Theorem Prover,” J. of Automated Reasoning 5

(1989) 363–397.

[7] Paulson, L.C, Nipkow, T. “Isabelle Tutorial and User’s Manual,” Isabelle-91 distribution.

[8] Wand, M. “On the Correctness of Procedure Representations in Higher-Order Assembly Language” Proc. MFPS ’91 (S. Brookes, ed.) Springer Lecture Notes in Computer Science, to appear.