Andrei Arusoaie

David Nowak

Vlad Rusu

Dorel Lucanu

Formal Proof of Soundness for an RL Prover

Keywords: Coq, Matching Logic, Reachability Logic, program verification procedure Coq, Matching Logic, Reachability Logic, procédure de vérification

Proving programs correct is one of the major challenges that computer scientists have been struggling with during the last decades. For this purpose, Reachability Logic (rl) was proposed as a language-parametric generalisation of Hoare Logic. Recently, based on rl, an automatic verification procedure was given and proved sound. In this paper we generalise this procedure and prove its soundness formally in the Coq proof assistant. For the formalisation we had to deal with all the minutiae that were neglected in the paper proof. The trickiest one was appropriate renaming of free variables which, we discovered, was handled in the paper proof using an insufficient assumption. We also discovered a missing case in the paper proof, and we clarified some implicit and hidden hypotheses. Last but not least, the Coq formalisation provides us with a certified program-verification procedure.

Introduction

Proving programs correct is one of the major challenges that computer scientists have been struggling with during the last decades. Many techniques have been developed in order to automate this non-trivial and tedious process. Nowadays there are many software tools used for proving program correctness, but proving that the verification tools are themselves correct is often avoided. In this paper we address this issue for our own work. More precisely, we present the formalisation in Coq of the soundness of a procedure for program verification that was proposed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF].

Floyd/Hoare Logic [START_REF] Floyd | Assigning meanings to programs[END_REF][START_REF] Antony | An Axiomatic Basis for Computer Programming[END_REF], Separation Logic [START_REF] O'hearn | The logic of bunched implications[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF], and Dynamic Logic [START_REF] Harel | Dynamic logic[END_REF] are probably the most well known logics dedicated to program verification. Recently, Matching Logic (ml) [START_REF] Roşu | Matching logic: An alternative to Hoare/Floyd logic[END_REF][START_REF] Roşu | Matching Logic: A New Program Verification Approach (NIER Track)[END_REF] and Reachability Logic (rl) [START_REF] Roşu | Towards a unified theory of operational and axiomatic semantics[END_REF][START_REF] Roşu | Checking reachability using matching logic[END_REF][START_REF] Roşu | One-path reachability logic[END_REF][START_REF] Ştefănescu | All-path reachability logic[END_REF] have been proposed as alternative approaches for dealing with this problem. ml and rl were inspired from the attempt to use rewrite-based operational semantics for program verification. Although operational semantics are considered too low level for verification, they are much easier to define and have the big advantage of being executable (and thus testable). For example, several large and complete operational semantics for real languages have been formalised with rl using the K framework [START_REF] Roşu | An overview of the K semantic framework[END_REF][START_REF] Roşu | K overview and simple case study[END_REF][START_REF] Traian Florin Şerbănuţă | The primer (version 3.3)[END_REF]: C [START_REF] Ellison | An executable formal semantics of C with applications[END_REF][START_REF] Hathhorn | Defining the undefinedness of c[END_REF], Java [START_REF] Bogdănaş | K-Java: A Complete Semantics of Java[END_REF], JavaScript [START_REF] Park | KJS: A complete formal semantics of JavaScript[END_REF], etc. ml is a first-order logic for specifying and reasoning about program configurations, e.g., code and infrastructure for executing it (heap, stack, registers, etc.). Intuitively, an ml formula ϕ is a configuration template accompanied by a constraint, and it denotes the set of configurations that match the template and satisfy the constraint. rl is a formalism which can be used for both defining operational semantics of programming language and expressing properties about program executions. An rl formula is a pair of ml formulas, denoted ϕ ⇒ ϕ , which says that all terminating executions that start from a configuration in the set denoted by ϕ, eventually reach a configuration in the set denoted by ϕ .

The state-of-the-art techniques for program verification involve defining a semantics that is thought of as being more appropriate for program reasoning than operational semantics. A wellknown example is axiomatic semantics, which is typically given in the form of a Hoare Logic proof system for deriving Hoare triples {precondition}code{postcondition}. In [START_REF] Roşu | From hoare logic to matching logic reachability[END_REF] it has been shown that such a triple can be easily encoded as an rl formula ϕ ⇒ ϕ , where ϕ denotes the configurations that contain the code to be executed and satisfy a constraint describing the precondition and ϕ denotes the final (in the sense that there is no more code to be executed) configurations that satisfy a constraint describing the postcondition. There are several advantages of rl over Hoare Logic: First, rl does not depend on a specific programming language. Second, the proof system of rl [START_REF] Ştefănescu | All-path reachability logic[END_REF] is proved sound and relatively complete for all languages, and thus, it eliminates the need for non-trivial soundness proofs for each language. Third, given an operational semantics, there is no need for an additional one which is amenable for program verification (i.e., no axiomatic semantics in the form of Hoare logic proof system is needed). Finally, rl is based on the operational semantics of a programming language, which is executable and hence enables the testing of programs prior to their verification. In contrast, axiomatic semantics are not executable, and thus, errors that could have been discovered by testing are discovered only later, after failed verification attempts.

One practical disadvantage of the rl proof system [START_REF] Ştefănescu | All-path reachability logic[END_REF] is that the proofs tend to be very low level. Moreover, some creative user input is required when applying the rules of the proof system. Those difficulties were addressed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], where a procedure for program verification based on rl was proposed and the soundness of the procedure was proved. The intent behind this procedure is to overcome the lack of strategies for applying the rules of the rl proof system, and implicitly, move forward to automation. More precisely, the procedure applies in a fixed order three inference steps that are meant to capture the rules of the rl proof system. The procedure takes as inputs sets of rl formulas representing the operational semantics of a language and the program together with its specification to be proved; if it terminates, it returns either success or failure.

The soundness theorem says that if the procedure terminates and returns success then the program satisfies its specification. Its proof depends on several assumptions which are not precisely formalised in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. In order to provide additional confidence in this soundness result, we present in this paper a formalisation of the soundness proof in Coq. The paper proof from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] raised a series of technical difficulties. One difficulty is hidden in an intermediary lemma whose proof requires intricate inductive reasoning. Then, several hypotheses and assumptions are added in an ad-hoc manner just for the proofs to hold. Also, some helper lemmas that are given inside other proofs are not precisely formulated, i.e., they need additional hypotheses. For a careful reader all these issues could raise some doubts about the validity of the paper proof. A proof in a research paper should keep a good balance between correctness and clarity. The soundness proof in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] is monolithic, i.e. the soundness does not follow from the soundness of each derivation rule, as it is commonly done in soundness proofs. Therefore, even if the procedure is recursive, the nature of the proof is not inductive; the entire execution of the procedure is needed to prove that the goals are valid. This makes the proof complex and hence the task of keeping a good balance between correctness and clarity is difficult. In order to keep the proof concise, some details are omitted but this could have hidden side effects that are not discussed by the proof.

Clearly, a proof assistant is the solution here: it has no problem dealing with every detail because it keeps track rigorously of all cases, and thus, it ensures that no corner case is overlooked; and keys lemmas and propositions still show the main steps of the reasoning process.

Contributions

We first generalise the procedure by introducing non-determinism and then encode it as an inductive relation in Coq. Then, we formally prove that our generalised procedure is sound. The soundness of the concrete procedure in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] follows.

The formalisation led us to discovering a flaw in the paper proof: it is supposed that a claim holds for a set of rl formulas, but the claim was proved only for a subset of formulas. Fortunately, this flaw does not invalidate the final result, but it makes the proof in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] incomplete. Moreover, in order to fix the proof we realised that we need an extra hypothesis in the soundness theorem. In Coq, we add both the required hypothesis and an additional case which handles the rl formulas in question and completes the proof.

Another issue that we discovered and fixed is related to renaming the free variables in rl formulas. In [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] this is imprecisely handled using an assumption saying that certain sets of variables are disjoint, and if they are not, then the free variables can always be renamed. However, why the variable renaming is sound is not established in the paper proof.

During the formalisation in Coq we were able to find and fix some other imprecisions in lemmas from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. For instance, Lemmas 7 and 8 (in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]) only make sense in the context of the proof of Theorem 1 (in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]). Here, these lemmas were reformulated to be self-contained, including all implicit or sometimes missing hypotheses. Last but not least, the Coq formalisation provides us with a certified program-verification procedure. Its use in practice depends on the availability in Coq of rl-based semantics for languages; such an effort is already underway in the K team [START_REF] Moore | Program verification by coinduction[END_REF].

Related work

The closest related work is the formalisation in Coq of rl reported in [START_REF] Ştefănescu | All-path reachability logic[END_REF]. Our initial attempt to prove the soundness of the procedure from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] consisted in reusing the mechanised proof reported in [START_REF] Ştefănescu | All-path reachability logic[END_REF]. However, the soundness of the procedure is not a direct consequence of the soundness of the rl proof system, because there is no direct correspondence Inria between the inference steps and the rules of the proof system. This is the reason why we choose to give a direct proof of the soundness of the procedure. An additional benefit of a direct proof is that, compared to the rl proof system, our procedure is closer to an implementation. Thus, by formalising directly the soundness of the procedure in Coq (vs. formalising the soundness of a proof system) we bridge the gap between theory and implementation.

Another approach which is strongly connected to rl is [START_REF] Moore | Program verification by coinduction[END_REF]. It proposes a language-independent proof method for verifying reachability properties on programs. The approach is also implemented in Coq. Although it provides tactics to increase the level of automation, the tool is not fully automatic, unlike the procedure in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. From the same authors, there are also ongoing works for translating K language definitions to Coq.

There are many soundness results about proof systems for program verification (e.g., [START_REF] Marti | Formal verification of the heap manager of an operating system using separation logic[END_REF][START_REF] Appel | Program Logics for Certified Compilers[END_REF][START_REF] Weber | Towards mechanized program verification with separation logic[END_REF][START_REF] Tuch | A unified memory model for pointers[END_REF][START_REF] Schirmer | A verification environment for sequential imperative programs in isabelle/hol[END_REF] to cite only a few). Most of them are based either on Hoare Logic or Separation Logic, and thus, they are language dependent. For instance, in [START_REF] Weber | Towards mechanized program verification with separation logic[END_REF] the authors present three Hoare logics that correspond to different notions of correctness for the simple While language; for all three they prove the soundness and the relative completeness. However, compared to [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], they do not provide a language-parametric program-verification automatic procedure.

There is moreover a wide range of certified sound procedures for deciding various logical fragments, some of them formalised in Coq (e.g. [START_REF] Braibant | Deciding kleene algebras in coq[END_REF][START_REF] Besson | Fast reflexive arithmetic tactics the linear case and beyond[END_REF]), others in Isabelle/HOL (e.g., [START_REF] Chaieb | Verifying and reflecting quantifier elimination for Presburger arithmetic[END_REF]).

Outline. Section 2 provides a short overview of ml and rl, and presents the verification procedure proposed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] together with the corresponding soundness result. Section 3 describes our formalisation in Coq of the soundness of the procedure. It mainly contains the definitions and lemmas needed by the soundness result, and it also highlights the differences between the Coq proof and the one in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. We conclude in Section 4.

Background

Matching Logic & Reachability Logic

This section provides an overview of ml and rl. For both logics, we explain their syntax and semantics by means of simple examples. In addition, several notions and definitions specific to this paper are also presented. We assume the reader is familiar with First-Order Logic (hereafter, fol).

Matching Logic ml is a first-order logic variant for specifying and reasoning about structure. We here consider the version of ml from [START_REF] Roşu | Matching logic -extended abstract[END_REF]. Formally, ml formulas are defined as follows. If Σ is a many-sorted algebraic signature, Π is a set of predicate symbols, Var a set of (sorted) variables, and Cfg a sort for program configurations, then the syntax of ml formulas is:

ϕ ::= π | | p(t 1 , . . . , t n ) | ¬ϕ | ϕ ∧ ϕ | (∃V )ϕ,
where π is a Σ-term of sort Cfg with variables (also called basic pattern), p is a predicate symbol in Π, t i are Σ-terms with variables of appropriate sorts, and V a subset of Var . As usual, the other known fol connectives (∨, →, . . . ) and quantifier ∀ can be expressed using the ones above.

Let us consider a signature Σ which contains a sort AExp that includes the integer numbers (as symbols) together with the usual binary operations (e.g., _ + _, _ -_, . . . ), and a sort Cfg, which has a single constructor _, _ : AExp × AExp → Cfg (we use _ to denote the positions of the arguments). Also, let Π be the set which contains the predicate symbols _>_ and _≥_ with arguments of sort AExp, and Var a set of variables of sort AExp (e.g. x, y, z, . . . ). Then, an example of ml formula is:

ϕ x -y, z ∧ x > y ∧ z ≥ 0
Indeed, x, y and z are terms of sort AExp, x -y, z is a term of sort Cfg with variables (i.e., a basic pattern), x > y ∧ z ≥ 0 is an ml formula, and x -y, z ∧ x > y ∧ z ≥ 0 is also an ml formula.

The set of free variables that occur in an ml formula ϕ is denoted by FV(ϕ). For instance, FV((∃x, z) x, y ∧ z > 0) = {y}.

Next, we assume a (Σ, Π)-model M . The satisfaction relation |= ml of ml is akin to the satisfaction relation of fol (denoted |= fol ). For instance, (γ, ρ) |= ml (∃V )ϕ iff there is ρ : Var → M with ρ (x) = ρ(x) for all x ∈ V such that (γ, ρ ) |= ml ϕ. This is similar to fol, except that |= ml is defined over pairs (γ, ρ), where γ is an element in M of sort Cfg called a configuration, ρ : Var → M is a valuation, and ml formulas ϕ. In addition to the other fol constructs, |= ml includes the ml particular case:

(γ, ρ) |= ml π iff ρ(π) = γ.
Intuitively, a basic pattern π is satisfied by a pair (γ, ρ) if γ matches π with ρ; here, the valuation ρ can be thought of as the witness of the matching. For example, 7-3, 3 matches the basic pattern x -y, z with a valuation ρ that maps x, y, and z to 7, 3, and 3, respectively: ρ( x -y, z ) = 7 -3, 3 .

An ml formula ϕ is valid in M , written M |= ϕ, iff for all γ and ρ : Var → M we have (γ, ρ) |= ml ϕ.

Let M be a model which interprets the sort AExp as the set of integers, and the binary symbols +, -, . . . as the usual operations over integers. Similarly, M interprets the predicate symbols > and ≥ as the usual corresponding relations over integers. Also, consider the valuation ρ : Var → M with ρ(x) = 7, ρ(y) = 3, and ρ(z) = 3. Then, ( 7 -3, 3 , ρ) |= ml ϕ because ρ( x -y, z ) = 7 -3, 3 and (γ, ρ) |= ml x > y ∧ z ≥ 0 (since 7 > 3 and 3 ≥ 0 in M ).

It has been shown in [START_REF] Roşu | Checking reachability using matching logic[END_REF] that ml can be encoded in fol. If ϕ is an ml-formula then its encoding ϕ =? in fol is the formula (∃z)ϕ , where ϕ is obtained from ϕ by replacing each basic pattern occurrence π with z = π, and z is a variable which does not appear in the free variables of ϕ. Here are a few examples of formulas and their encodings:

ϕ ϕ =? (π 1 ∧ φ 1 ) ∨ (π 2 ∧ φ 2 ) (∃z)((z = π 1 ∧ φ 1 ) ∨ (z = π 2 ∧ φ 2 )) ¬π (∃z)¬(z = π) π ∨ ¬π (∃z)(z = π ∨ ¬(z = π))
The encoding of an ml formula ϕ has the following property [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]: for all ρ and ϕ, ρ |= fol ϕ =? iff there is γ such that (γ, ρ) |= ml ϕ.

Reachability Logic An rl formula (also called rule) is a pair of ml formulas, written ϕ ⇒ ϕ , which expresses reachability relationships between the two sets of configurations denoted by ϕ and ϕ . For example, the rl formula α x, y ∧ x ≥ 0 ⇒ x -y, y expresses the fact that configurations which satisfy the x -y, y (e.g. 7 -3, 3 with ρ aforesaid), can be reached from configurations which satisfy x, y ∧ x ≥ 0 (e.g., 7, 3 with the same ρ).

Inria

By FV(ϕ ⇒ ϕ ) we denote the union FV(ϕ) ∪ FV(ϕ ). Also, if S is a set of rl formulas then FV(S)

ϕ⇒ϕ ∈S FV(ϕ ⇒ ϕ ). A set S of rl formulas defines a transition system (Cfg, ⇒ S ) over configurations: we say that γ 0 ⇒ S γ 1 if there is ϕ 0 ⇒ ϕ 1 ∈ S and there is a valuation ρ : Var → M such that (γ 0 , ρ ) |= ml ϕ 0 and (γ 1 , ρ ) |= ml ϕ 1 . We often use only ⇒ S to denote the transition system (Cfg, ⇒ S ). Back to our example, the set S = {α} generates the transition 7, 3 ⇒ {α} 7 -3, 3 .

A pattern is S-derivable if there is a transition from one of its instances with S. For example, ϕ 0

x, y ∧ x ≥ 7 is {α}-derivable because there is a transition from 7, 3 (which satisfies ϕ 0 with ρ) to 7 -3, 3 .

A set S of rl formulas is total if for all ϕ, γ, and ρ, if ϕ is S-derivable and (γ, ρ) |= ml ϕ then there is γ such that γ ⇒ S γ . Note that {α} is not total because of the condition x ≥ 0 in its left hand side. To make it total, one should add to {α} another rule which handles the other possible case, namely x < 0.

The satisfaction relation |= rl of rl is defined using paths, which are (possibly infinite) sequences of transitions

γ 0 ⇒ S γ 1 ⇒ S γ 2 ⇒ S • • • . For example, 7, 3 ⇒ {α} 7 -3, 3 ⇒ {α} 7 -3 -3, 3 ⇒ {α} 7 -3 -3 -3, 3 is a finite path.
Note that α cannot be applied anymore to 7 -3 -3 -3, 3 because of the constraint x ≥ 0. If none of the rules in S can be applied then we say that the configuration (e.g. 7 -3 -3 -3, 3 ) is terminating.

Paths can be infinite too, e.g., 7, 0

⇒ {α} 7 -0, 0 ⇒ {α} • • • . A path τ is complete if it
is either finite and the last configuration in τ is terminating, or it is infinite. Both paths shown above are complete. Typically, we use τ to denote paths, i.e., τ

γ 0 ⇒ S γ 1 ⇒ S γ 2 ⇒ S • • • , and τ | i to denote the sub-path of τ starting at position i, i.e., τ | i γ i ⇒ S γ i+1 ⇒ S • • • .
We also say that τ starts from from an ml formula ϕ if there is a valuation ρ :

Var → M such that (γ 0 , ρ) |= ml ϕ. For example, 7, 0 ⇒ {α} 7 -0, 0 ⇒ {α} • • • and 7, 3 ⇒ {α} 7 -3, 3 ⇒ {α} 7 -3 -3, 3 ⇒ {α} 7 -3 -3 -3, 3 start from x, y ∧ x ≥ 0.
In this paper we are only interested in the all-path interpretation [START_REF] Ştefănescu | All-path reachability logic[END_REF] of rl formulas: a pair (τ, ρ) satisfies an rl formula ϕ ⇒ ϕ , written (τ, ρ) |= ϕ ⇒ ϕ , iff (τ, ρ) starts from ϕ (recall that τ γ 0 ⇒ S γ 1 ⇒ S γ 2 ⇒ S • • • ), and either there exists i ≥ 0 such that (γ i , ρ) |= ml ϕ , or τ is infinite; ⇒ S satisfies ϕ ⇒ ϕ , written ⇒ S |= rl ϕ ⇒ ϕ , iff (τ, ρ) |= rl ϕ ⇒ ϕ for all (τ, ρ) starting from ϕ with τ complete. We often write S |= rl ϕ ⇒ ϕ instead of ⇒ S |= rl ϕ ⇒ ϕ .

Let ϕ ⇒ ϕ be the rl formula:

x, y ∧x ≥ y∧y > 0 ⇒ (∃x ) x , y ∧mod (x , x, y),

where mod is a predicate symbol with interpretation: M mod (r, x, y) holds iff r is the remainder after division of x by y. The path τ 7, 3 ⇒ {α} 7-3, 3 ⇒ {α} 7-3-3, 3 ⇒ {α} 7-3-3-3, 3 is complete and starts from x, y ∧ x ≥ y ∧ y > 0 with a valuation ρ : Var → M , which maps x and y to 7 and 3, respectively. However, (τ, ρ) |= ϕ ⇒ ϕ because ( 7 -3 -3 -3, 3 , ρ) |= ml ϕ (since, in M , -2 is not the remainder after division of 7 by 3).

However, if x ≥ y, the remainder after division of x by y can be obtained by repeated subtraction of y from the initial x if y > 0. Thus, let us consider a version of α:

α x, y ∧ x ≥ y ∧ y > 0 ⇒ x -y, y
The finite path τ 7, 3 ⇒ {α } 7 -3, 3 ⇒ {α } 7 -3 -3, 3 is complete and starts from x, y ∧ x ≥ y ∧ y > 0 with the same valuation ρ as above. Also, there is a configuration 7 -3 -3, 3 in τ such that ( 7 -3 -3, 3 , ρ) |= ml ϕ . More precisely, ( 7 -3 -3, 3 , ρ) |= ml (∃x ) x , y ∧ mod (x , x, y) iff there is a valuation ρ : Var → M such that ρ (y) = ρ(y) and ( 7 -3 -3, 3 , ρ ) |= ml x , y ∧ mod (x , x, y); if we take ρ such that ρ (v) = ρ(v) for all v ∈ Var \ {x } and ρ (x ) = 1, then ρ ( x , y ) = 1, 3 and M mod (1, 7, 3) holds, which implies ( 7 -3 -3, 3 , ρ ) |= ml x , y ∧ mod (x , x, y). Therefore, we obtain (τ , ρ) |= rl ϕ ⇒ ϕ .

RR n°471

Language definitions In the example above, we have shown that the path τ , whose transitions are given by {α }, satisfies the rl formula ϕ ⇒ ϕ with a valuation ρ. The system S = {α } can be seen as the operational semantics of a language whose programs are pairs of (arithmetic) expressions. Formally, we consider language definitions ((Σ, Π, Cfg), M , S), where, for our simple language, Σ is the signature containing the sorts Cfg and AExp (together with the corresponding operation symbols), Π is the set of predicates including _>_ and _≥_, M is a (Σ, Π) model, and

S = {α }.
This notion of language definition is general, in the sense that it captures real language definitions, such as those defined in the K framework, e.g., C [START_REF] Ellison | An executable formal semantics of C with applications[END_REF][START_REF] Hathhorn | Defining the undefinedness of c[END_REF], Java [START_REF] Bogdănaş | K-Java: A Complete Semantics of Java[END_REF], JavaScript [START_REF] Park | KJS: A complete formal semantics of JavaScript[END_REF], etc.

Derivatives of an ml (and rl) formula A notion introduced in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] is that of derivative of an ml (and rl) formula. If ϕ is an ml formula and S is a set of rl formulas, then the derivative of ϕ with S is defined as follows:

∆ S (ϕ) {(∃FV(ϕ l , ϕ r ))(ϕ l ∧ ϕ) =? ∧ ϕ r | ϕ l ⇒ ϕ r ∈ S}. If ϕ ⇒ ϕ is an rl formula then ∆ S (ϕ ⇒ ϕ ) {ϕ 1 ⇒ ϕ | ϕ 1 ∈ ∆ S (ϕ)}.
Intuitively, the derivative of an ml formula ϕ encodes the concrete successors by ⇒ S of configurations matching ϕ. Derivatives can be computed for sets of rl formulas G too:

∆ S (G) ϕ⇒ϕ ∈G ∆ S (ϕ ⇒ ϕ ). Let again α x, y ∧ x ≥ y ∧ y > 0 ⇒ x -y, y and ϕ u, v ∧ u ≥ v ∧ v > 0.
Then ∆ {α } (ϕ) has only one element:

(∃x, y)(( x, y ∧ x ≥ y ∧ y > 0) ∧ ( u, v ∧ u ≥ v ∧ v > 0)) =?
∧ x -y, y , which, by the definition of the encoding, becomes:

(∃x, y)( x, y = u, v ) ∧ x ≥ y ∧ y > 0 ∧ u ≥ v ∧ v > 0 ∧ x -y, y .
This can be further simplified to ϕ u -v, v ∧ u ≥ v ∧ v > 0 using the fact that x, y = u, v implies x = u and y = v. The ml formula ϕ specifies the configurations obtained from those satisfying ϕ after applying α ; for example, the configuration 7 -3, 3 (which satisfies ϕ with a valuation ρ s.t. ρ(u) = 7, ρ(v) = 3) is a successor of 7, 3 (that satisfies ϕ with the same ρ), i.e., 7, 3 ⇒ {α } 7 -3, 3 .

Remark 1 Note that in the example above the free variables in ϕ are disjoint from those in α , i.e, {u, v} ∩ {x, y} = ∅. If these sets are not disjoint, then there is no guarantee that the derivative encodes the set of all concrete successors of configurations that match ϕ. For instance, let ϕ u, x ∧u ≥ x∧x > 0 (i.e., ϕ is ϕ where variable v was replaced by x). When computing the derivative of ϕ with {α }, the variable x ∈ FV(ϕ ) is bound:

(∃x, y)( x, y = u, x ) ∧ x ≥ y ∧ y > 0 ∧ u ≥ x ∧ x > 0 ∧ x -y, y .
Again, this formula can be simplified to ϕ u -u, u ∧ u > 0, using the fact that x, y = u, x implies x = u and y = x. Here, there is no valuation ρ such that ( 7 -3, 3 , ρ ) |= ϕ , and thus, not all successors by ⇒ {α } of 7, 3 are matched by the derivative.

Inria

Therefore, when computing ∆ S (ϕ), it is important that the free variables of ϕ and those of S are in disjoint sets.

The issue described in Remark 1 is also an issue in the verification procedure proposed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]: the procedure computes derivatives ∆ S (ϕ) without checking (as it should) that FV(S) and FV(ϕ) are disjoint. This is discussed in detail in the next section.

A procedure for verifying Reachability Logic properties

A procedure for verifying rl formulas (Figure 1), called prove, was introduced in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. The intent behind prove is to overcome the lack of strategies for applying the rules of the rl proof system from [START_REF] Ştefănescu | All-path reachability logic[END_REF], and implicitly, to move forward towards automatisation.

In a nutshell, the procedure uses symbolic execution (i.e., run programs with symbolic values instead of concrete ones, and collect the constraints over symbolic values) combined with circular reasoning. Intuitively, given an rl formula ϕ ⇒ ϕ , one can symbolically execute ϕ and check whether every leaf node of the obtained symbolic execution tree implies ϕ . The procedure uses derivatives to compute symbolic execution paths. An obvious problem of this approach is that the symbolic execution tree can be infinite due to loops or recursion. To overcome this problem rl allows the use of helper formulas called circularities, which generalise the notion of invariant.

Instead of proving a single formula, prove attempts to prove a set of formulas (goals). The procedure checks first whether a helper formula can be used (e.g., an rl formula specifying a loop) to discharge the current goal, rather than performing symbolic execution blindly. A goal can be used in the proof of a different goal or in its own proof, provided that at least one symbolic step has been performed from it.

Note that a proof by simple induction on the inferences steps of the procedure does not work because of its circular nature, that is, it uses goals to prove other goals (line 4 in Figure 1). This is sound only if a symbolic step from the current goal has been performed. If this condition is not met then every goal can be proved using itself! For this reason, the soundness theorem assumes a successful execution starting with ∆ S (G 0 ) instead of G 0 .

The procedure takes as input three sets of rl formulas: the operational semantics S, a set of goals G 0 , and a recursive argument G whose initial value is ∆ S (G 0 ); and it returns either success or failure. At each recursive call, a goal from G is either eliminated and/or replaced by other goals. If ϕ ⇒ ϕ ∈ G is the current goal then it is processed as follows: if M |= ϕ → ϕ then the goal is eliminated from G; else, the procedure checks whether there is a circularity available in G 0 which is used to generate a new goal that replaces the current one; if no circularity is found, but ϕ is S-derivable, then ϕ ⇒ ϕ is replaced by a set of goals consisting in its symbolic successors; otherwise, prove returns failure. The procedure succeeds when all the goals in ∆ S (G 0 ) together with those generated during the execution are eliminated. If the procedure does not terminate or it returns failure then it means that G 0 does not contain enough information to prove the goals. This is similar to proving invariants for loops in imperative programs, which requires users to provide strong-enough invariants.

Below, we show the soundness result and a sketch of the proof that was given in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. We illustrate by this the fact it is not a simple proof by induction on the recursive calls: even if they terminate, the calls do not induce a well-founded order over formulas ensuring a formula holds whenever the "smaller" formulas hold as well. Indeed, a formula may coinductively use itself in its own proof.

Theorem 1 (Theorem 1 in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]) Let prove be the procedure given in Figure 1. Assume that S is total. Let G 0 be such that for each ϕ c ⇒ϕ c ∈ G 0 , ϕ c is S-derivable and satisfies FV(ϕ c ) ⊆ FV(ϕ c ). If prove(S, G 0 , ∆ S (G 0 )) returns success then S|= rl G 0 .

procedure prove(S, G0, G)

1: if G = ∅ then return success 2: else choose ϕ ⇒ ϕ ∈ G 3: if M |=ml ϕ → ϕ then return prove(S, G0, G \ {ϕ ⇒ ϕ }) 4: else if there is ϕc ⇒ ϕ c ∈ G0 s. t. M |=ml ϕ → ϕ c then 5: return prove(S, G0, G \ {ϕ ⇒ ϕ } ∪ ∆ ϕc⇒ϕ c (ϕ ⇒ ϕ )) 6: else if ϕ is S-derivable then 7: return prove(S, G0, G \ {ϕ ⇒ ϕ } ∪ ∆S (ϕ ⇒ ϕ ))
8: else return failure. Proof sketch At each step of the procedure, the set G of goals evolves from ∆ S (G 0 ) to ∅ (if prove terminates successfully). Let F G 0 i G i , where i represents the i th call of prove. The first call is made for G 1 ∆ S (G 0 ). In order to prove that S |= G 0 one has to prove that S |= rl ϕ ⇒ ϕ for all goals ϕ ⇒ ϕ ∈ G 0 , that is, (τ, ρ) |= ϕ ⇒ ϕ for all (τ, ρ) starting from ϕ with τ complete.

We consider an arbitrary τ γ 0 ⇒ S γ 1 ⇒ S • • • such that τ starts from ϕ with a valuation ρ : Var → M . If τ is infinite then, by definition, (τ, ρ) |= ϕ ⇒ ϕ . There remains to show that (τ, ρ) |= ϕ ⇒ ϕ when the path is finite, i.e., τ

γ 0 ⇒ S γ 1 ⇒ S • • • ⇒ S γ n .
This case is proved using an intermediate lemma, which states the property for all goals in F, including the ones in G 0 : Lemma 1 (Lemma 8 in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]) For all τ , for all ρ, for all ϕ ⇒ ϕ ∈ F, if τ is finite and complete, and (τ, ρ) starts from ϕ then (τ, ρ) |= ϕ ⇒ ϕ .

The lemma works on the following assumption (from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]):

(a 1 ) "In what follows we consider only ml formulas ϕ with the following property: If ϕ does not occur as a member of a rule in S and ϕ l ⇒ ϕ r ∈ S then FV(ϕ) ∩ FV(ϕ l , ϕ r ) = ∅. This is not a real restriction since the free variables in rules can always be renamed."

It also uses two additional results (from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]):

(1) For all ϕ ⇒ ϕ ∈ F either M |= ϕ → ϕ or ϕ is S-derivable.

(2) For all γ 0 , γ 1 , ϕ, and ρ such that γ ⇒ {α} γ and (γ, ρ)

|= ml ϕ there is ϕ ∆ {α} (ϕ) such that (γ , ρ) |= ml ϕ .
The proof of the lemma is by induction on the number of transitions (n

) in τ γ 0 ⇒ S γ 1 ⇒ S • • • ⇒ S γ n . Since τ is finite, proving (τ, ρ) |= ϕ ⇒ ϕ reduces to finding γ i such that (γ i , ρ) |= ml ϕ .
In the base case n = 0 and τ γ 0 . Since ϕ ⇒ ϕ ∈ F the auxiliary result (1) ensures that M |= ϕ → ϕ or ϕ is S-derivable. From (τ, ρ) starts from ϕ we obtain that (γ 0 , ρ) |= ϕ. If M |= ϕ → ϕ , then we have γ 0 such that (γ 0 , ρ) |= ϕ . If ϕ is S-derivable, then we obtain a contradiction in our hypotheses: on the one hand, γ 0 is terminating because τ is complete, and on the other hand γ 0 is not terminating because there is γ 1 such that γ 0 ⇒ S γ 1 which is implied by the totality of S and (γ 0 , ρ) |= ϕ.

Inria

In the inductive case, we have n > 0 and τ γ 0 ⇒ S γ 1 ⇒ S • • • ⇒ S γ n . Note that n > 0 implies the fact that τ contains at least the first transition γ 0 ⇒ S γ 1 , i.e., there is α ∈ S such that γ 0 ⇒ {α} γ 1 .

Since ϕ ⇒ ϕ ∈ F( i≥0 G i ) then ϕ ⇒ ϕ was eliminated at some point, i.e, there is i such that ϕ ⇒ ϕ ∈ G i \ G i+1 ; We distinguish the three situations (corresponding to the inference steps of the procedure):

• M |= ϕ → ϕ . Trivial: (γ 0 , ρ) |= ϕ implies (γ 0 , ρ) |= ϕ . • there is ϕ c ⇒ ϕ c ∈ G 0 s. t. M |= ml ϕ → (∃FV(ϕ c ))ϕ c .
From (γ 0 , ρ) |= ϕ and M |= ml ϕ → (∃FV(ϕ c ))ϕ c we get (γ 0 , ρ) |= (∃FV(ϕ c ))ϕ c , i.e, there is ρ such that ρ (x) = ρ(x) for all x ∈ FV(ϕ c ) and (γ 0 , ρ ) |= ml ϕ c . Then, by applying (2) to (γ 0 , ρ ) |= ml ϕ c and γ 0 ⇒ S γ 1 there is

ϕ 1 ∆ {α} (ϕ c ) and (γ 1 , ρ ) |= ml ϕ 1 .
Next, the inductive hypothesis is applied twice.

First, the inductive hypothesis is applied for τ | 1 , which starts from ϕ 1 , and ϕ 1 ⇒ ϕ c ∈ ∆ S (ϕ c ⇒ ϕ c ) ⊆ F, and thus, there is γ j which satisfies ϕ c with ρ ; Then, using the assumption (a 1 ) from above, one can prove (γ j , ρ) |= ml ∆ ϕc⇒ϕ c (ϕ).

Second, we apply the inductive hypothesis for τ | j , which starts from ∆ ϕc⇒ϕ c (ϕ), and ∆ ϕc⇒ϕ c (ϕ ⇒ ϕ ) ∈ F, and thus, there is γ i such that (γ i , ρ) |= ml ϕ .

• ϕ is S-derivable. By applying (2) for (γ 0 , ρ) |= ml ϕ c and γ 0 ⇒ S γ 1 , there is ϕ 1 ∆ {α} (ϕ) and (γ 1 , ρ) |= ml ϕ 1 . In this case we apply the inductive hypothesis for τ | 1 , which starts from ϕ 1 ∆ {α} (ϕ), and for

ϕ 1 ⇒ ϕ ∈ ∆ S (G 0 ) ⊆ F, to obtain γ i such that (γ i , ρ) |= ml ϕ .
Remark 2 Computing ∆ ϕc⇒ϕ c (ϕ) (in the second case of the inductive step) requires that sets FV(ϕ) and FV(ϕ c , ϕ c ) are disjoint (cf. Remark 1). However, in the proof, there is no guarantee that this condition is met. Note that assumption (a 1 ) is insufficient in this case because it takes into account only rules in S (i.e., if ϕ l ⇒ ϕ r ∈ S then FV(ϕ) ∩ FV(ϕ l , ϕ r ) = ∅), but here ϕ c ⇒ ϕ c is from G 0 . In fact, (a 1 ) is relevant only when applying the additional result (2), since the rule α is from S. Although the assumption (a 1 ) states that the free variables in rules can always be renamed, in the proof from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] this is not handled explicitly.

A formal proof of soundness in Coq

In this section we generalise the procedure by introducing non-determinism and then encode it as an inductive relation in Coq. In spite of this generalisation, the formal proof of soundness follows the same pattern as the paper proof in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. Using Coq, we were able to find a flaw in the paper proof: the claim that all the goals in F are eliminated by one of the inference steps of the procedure (made in the proof of Lemma 1) does not hold. More precisely, the claim holds only for goals from F \ G 0 because the procedure is called with G 1 ∆ S (G 0 ), that is, it operates only with goals from G 1 , G 2 , . . .. This flaw does not invalidate the final result, but it makes the proof incomplete: an additional case is needed to prove the conclusion of Lemma 1 for the goals in G 0 . Note that, in the proof of Theorem 1, the goals (of interest) for which we apply Lemma 1 are exactly those from G 0 ⊆ F. During the formalisation, we also realised that we need an extra hypothesis in the soundness theorem to fix the proof.

Unlike in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], in the Coq proof we explicitly handle the renaming of variables in rl formulas. Also, we reformulate several lemmas from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] (Lemmas 5, 7, and 8) such that they are self contained, and we update their proofs accordingly.

In Section 3.1 we introduce a set of axioms that capture only those constructs of ml needed in our proof, and in Section 3.2 we define rl, derivatives, and related notions. In Section 3.3 we present the procedure as a set of inference rules, and then, its encoding in Coq. We precisely show how the assumptions from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] regarding variable renamings and well-formedness of rl formulas are dealt with. In Sections 3.4 and 3.5 we show the formalisation of the main lemmas and we emphasise the differences with respect to [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. Finally, in Section 3.6 we present a complete formulation of the soundness theorem and its proof.

ml in Coq

A definition of ml such as in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] would require us to formalise many things (algebraic specifications, FOL,...), which are irrelevant in our proof. Instead, we introduce a set of axioms that capture only what is needed by the proof: variables, ml implication (→), the existential quantifier (∃), a model M , a way to identify concrete program states in the model, and the rl satisfaction relation.

Variables (Var), program configurations (State), models (Model), and valuations (Valuation) are all parameters. From the ml syntax we only keep ¬, ∧ (both used to express →), and ∃, together with the corresponding axioms about the satisfaction relation |= ml . To avoid ambiguities, we distinguish the logical connectives and quantifiers of ml (¬, ∧, ∃, . . . ) from those of Coq by using a bold font for the latter (¬ ¬ ¬, ∧ ∧ ∧, ∃ ∃ ∃, . . . ):

Model : Type State : Type Var : Type MLFormula : Type Valuation : Type := Var → Model |=ml : State → Valuation → MLFormula → Prop ¬ : MLFormula → MLFormula ∧ : MLFormula → MLFormula → MLFormula ∃ : list Var → MLFormula → MLFormula |= ¬ : ∀ ∀ ∀γ ρ ϕ . (γ, ρ) |= ml ¬ϕ ↔ ↔ ↔ ¬ ¬ ¬(γ, ρ) |= ml ϕ |= ∧ : ∀ ∀ ∀γ ρ ϕ ϕ . (γ, ρ) |= ml ϕ ∧ ϕ ↔ ↔ ↔ (γ, ρ) |= ml ϕ ∧ ∧ ∧ (γ, ρ) |= ml ϕ |= ∃ : ∀ ∀ ∀ϕ γ ρ V . (γ, ρ) |= ml (∃V )ϕ ↔ ↔ ↔ ∃ ∃ ∃ρ . ∀ ∀ ∀v . v ∈ V → → → ρ (v) = ρ(v) ∧ ∧ ∧ (γ, ρ ) |= ϕ
The ml implication (→) is defined using ¬ and ∧:

ϕ → ϕ ¬(ϕ ∧ ¬ϕ ) Also, the validity of an ml formula is defined as follows:

M |= ml ϕ ∀ ∀ ∀γ ρ . (γ, ρ) |= ϕ
To collect the free variables of an ml formula we use a function FV, which takes a formula ϕ as an argument and returns the list of free variables occurring in ϕ. Because we do not instantiate the above axioms FV is a parameter:

FV : MLFormula → list Var
In the proofs of our lemmas we often have to build new valuations from existing ones. For that we use the following function:

Inria : Valuation → Valuation → list Var → Valuation
Intuitively, (ρ, ρ , V ) returns a new valuation which is equal to ρ in all variables except for those in V , where (ρ, ρ , V ) is equal to ρ . We capture this intuition in the following simple lemmas:

∈ : ∀ ∀ ∀x ρ ρ V . x ∈ V → → → (ρ, ρ , V )(x) = ρ(x) ∈ : ∀ ∀ ∀x ρ ρ V . x ∈ V → → → (ρ, ρ , V )(x) = ρ (x)
If an ml formula ϕ is satisfied by a pair (γ, ρ), and none of its free variables are in V , then for any ρ , the pair (γ, (ρ, ρ , V )) also satisfies ϕ, because on those variables (ρ, ρ , V ) has the same effect as ρ. Conversely, if ϕ is satisfied by a pair (γ, ρ ), and all its free variables are included in V , then for any ρ, the pair (γ, (ρ, ρ , V )) also satisfies ϕ. Since the full definition of |= ml is abstract here, these properties are given as axioms:

|= ⊆ : ∀ ∀ ∀ϕ γ ρ ρ V . (∀ ∀ ∀x . x ∈ FV(ϕ) → → → x ∈ V ) ∧ ∧ ∧ (γ, ρ) |= ml ϕ → → → (γ, (ρ, ρ , V )) |= ml ϕ |= ⊆ : ∀ ∀ ∀ϕ γ ρ ρ V . FV(ϕ) ⊆ V ∧ ∧ ∧ (γ, ρ ) |= ml ϕ → → → (γ, (ρ, ρ , V )) |= ml ϕ
Another property which depends on |= ml is the one about the encoding of ml formulas into fol: for all ρ and ϕ, ρ |= fol ϕ =? iff there is γ such that (γ, ρ) |= ml ϕ. Here we do not define fol, but we use the fact that any fol formula is also an ml formula. Hence, the encoding will transform an ordinary ml formula into an ml formula without patterns, and the property above is axiomatised as:

|= =? : ∀ ∀ ∀γ ρ ϕ . (γ , ρ) |= ml ϕ =? ↔ ↔ ↔ (∃ ∃ ∃γ)(γ, ρ) |= ml ϕ

rl and derivatives

By definition, an rl formula is simply a pair of ml formulas:

RLFormula MLFormula * MLFormula
For clarity, in Coq we use the notation ϕ ⇒ ϕ instead of the pair notation (ϕ, ϕ ). In [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] the following assumption is made: for any rl formula ϕ ⇒ ϕ the condition FV(ϕ ) ⊆ FV(ϕ) holds. Here, we introduce the notion of well-formed rl formula:

wf (ϕ ⇒ ϕ ) FV(ϕ ) ⊆ FV(ϕ)
A set of rl formulas S defines a transition system over states:

γ ⇒ S γ ∃ ∃ ∃ϕ ϕ ρ . ϕ ⇒ ϕ ∈ S ∧ ∧ ∧ (γ, ρ) |= ml ϕ ∧ ∧ ∧ (γ , ρ) |= ml ϕ
In the rest of the paper we assume a given set of rl formulas S. The satisfaction relation |= rl of rl is defined over execution paths τ , which could be either finite or infinite. Because of that, we formalise them as functions from nat to option State (where option State is the extension of State with an extra element None). The i th element of a path τ is τ (i) and can be either a state γ i or None. The subpath of τ which starts at position i is denoted τ | i . Also, a path is well-formed, written wfPath(τ ), if every two consecutive states (say γ i and γ i+1 ) are in the transition relation given by S (γ i ⇒ S γ i+1 ), and for all i and j such that i < j, if τ (i) = None then τ (j) = None.

A path τ is infinite, written infinite(τ ), if for all i, τ (i) = None. A configuration γ is terminating, denoted as terminating(γ), if there is no γ such that γ ⇒ S γ . A well-formed path τ is complete and has n transitions, written complete(τ, n) if τ is finite and terminating(τ (n)). Also, a well-formed path τ is complete, denoted by complete(τ ), if infinite(τ ) or complete(τ, n) for some natural number n. Note that, if the path τ is complete and well-formed then for all i (if τ is finite then i ≤ n) the subpath τ | i is also complete and well-formed. This statement is assumed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] but in Coq we prove it explicitly. Finally, we say that (τ, ρ) startsFrom ϕ if (τ (0), ρ) |= ml ϕ.

The satisfaction relation of rl is defined for complete paths τ : (τ, ρ) |= rl ϕ ⇒ ϕ iff (τ, ρ) startsFrom ϕ and, either there is i ≥ 0 such that (τ (i), ρ) |= ml ϕ or infinite(τ ). Also, ⇒ S |= rl ϕ ⇒ ϕ iff (τ, ρ) |= rl ϕ ⇒ ϕ for all pairs (τ, ρ) starting from ϕ with τ complete. Here are the exact definitions:

(τ, ρ) |= rl ϕ ⇒ ϕ (τ, ρ) startsFrom ϕ ∧ ∧ ∧ ((∃ ∃ ∃ i n γ . i ≤ n ∧ ∧ ∧ complete(τ, n) ∧ ∧ ∧ τ (i) = γ ∧ ∧ ∧ (γ , ρ) |= ml ϕ ) ∨ ∨ ∨ infinite(τ )) ⇒ S |= rl ϕ ⇒ ϕ ∀ ∀ ∀τ ρ . wfPath(τ ) ∧ ∧ ∧ complete(τ ) ∧ ∧ ∧ (τ, ρ) startsFrom ϕ ∧ ∧ ∧ (τ, ρ) |= rl ϕ ⇒ ϕ ⇒ S |= rl G ∀ ∀ ∀ ϕ ⇒ ϕ . ϕ ⇒ ϕ ∈ G → → →⇒ S |= rl ϕ ⇒ ϕ
An ml formula ϕ is S-derivable if there are γ, ρ, and γ such that (γ, ρ) |= ml ϕ and γ ⇒ S γ . The S-derivability of an ml formula must not be confused with the notion of S-derivative, i.e, the derivative with S of an ml formula (Section 2.1). To compute the S-derivative of an ml formula in Coq, we use the following function:

∆ ϕ l ⇒ϕr (ϕ) (∃FV(ϕ l ))(ϕ l ∧ ϕ) =? ∧ ϕ r .
Note that, unlike in the definition of derivatives from Section 2.1, here we quantify only the variables of ϕ l because wf(ϕ l ⇒ ϕ r ), i.e., FV(ϕ r ) ⊆ FV(ϕ l ). We use a similar notation for rl formulas:

∆ ϕ l ⇒ϕr (ϕ ⇒ ϕ ) (∃FV(ϕ l ))(ϕ l ∧ ϕ) =? ∧ ϕ r ⇒ ϕ .
∆ S (ϕ ⇒ ϕ ) returns the list of S-derivatives of ϕ ⇒ ϕ , and it is defined using ∆ ϕ l ⇒ϕr (ϕ ⇒ ϕ ) for every rule in ϕ l ⇒ ϕ r ∈ S.

Next, we introduce two relations ≈ and ∼, where the former is over rl formulas, and the latter is over pairs of ml formulas and valuations.

The relation ≈ is used to handle the renaming of free variables in rl formulas that is required when computing derivatives. More precisely, instead of computing ∆ ϕ l ⇒ϕr (ϕ ⇒ ϕ ) we compute ∆ ϕ l ⇒ϕ r (ϕ ⇒ ϕ ), where ϕ l ⇒ ϕ r is ϕ l ⇒ ϕ r with renamed free variables such that FV(ϕ l ) ∩ FV(ϕ) = ∅. This disjointness condition is essential for computing derivatives: if this condition is not met, then there is no guarantee that the derivative above encodes the successors of configurations matching ϕ (cf. Remark 1). The rl formula ϕ l ⇒ ϕ r is a renamed version of ϕ l ⇒ ϕ r and we express that using ≈:

ϕ l ⇒ ϕ r ≈ ϕ l ⇒ ϕ r .
If two rl formulas are related by ≈ then they denote the same set of transitions between configurations, but with different valuations. For instance, the transition from 7, 3 to 7 -3, 3 is given by both ϕ 0 ⇒ ϕ 0

x, y ⇒ x -y, y and

ϕ 1 ⇒ ϕ 1 u, v ⇒ u -v, v
with different valuations: a valuation ρ such that ρ(x) = 7 and ρ(y) = 3 for the former, and a valuation ρ such that ρ (u) = 7 and ρ (v) = 3 for the latter. Thus, 7, 3 satisfies ϕ 0 with ρ and ϕ 1 with ρ ,while 7 -3, 3 satisfies ϕ 0 with ρ and ϕ 1 with ρ .

To express the fact that two rl formulas in relation ≈ denote the same transitions between configuration, but with different valuations, we use the relation ∼:

Inria (ϕ, ρ) ∼ (ϕ , ρ ) ∀ ∀ ∀ γ . (γ, ρ) |= ml ϕ → → → (γ, ρ ) |= ml ϕ ,
and the following property:

≈ ∼ : ∀ ∀ ∀ ϕ 0 ϕ 0 ϕ 1 ϕ 1 . ϕ 0 ⇒ ϕ 0 ≈ ϕ 1 ⇒ ϕ 1 → ∀ ∀ ∀ ρ . ∃ ρ . (ϕ 0 , ρ) ∼ (ϕ 1 , ρ ) ∧ ∧ ∧ (ϕ 0 , ρ) ∼ (ϕ 1 , ρ )

The procedure as a relation

The inference steps that the procedure in Figure 1 performs are summarised below; for the moment, let us ignore the fact that prove operates with sets of goals:

M |= ml ϕ → ϕ S |= rl ϕ ⇒ ϕ [impl] ϕ c ⇒ ϕ c ∈ G 0 M |= ml ϕ → ϕ c S |= rl ∆ {ϕc⇒ϕ c } (ϕ ⇒ ϕ ) S |= rl ϕ ⇒ ϕ [circ] ϕ is S-derivable S |= rl ∆ S (ϕ ⇒ ϕ ) S |= rl ϕ ⇒ ϕ [symb]
The set G 0 is the initial set of goals and ϕ c (∃FV(ϕ c ))ϕ c . The connection with the procedure is straightforward: [impl] says that if the current goal ϕ ⇒ ϕ can be proved by checking the implication M |= ml ϕ → ϕ then S |= rl ϕ ⇒ ϕ (see line 3 of the procedure); [circ] captures the case when a circularity can be applied (lines 4 and 5); [symb] corresponds to the case when the current goal is discharged to its symbolic successors (lines 6 and 7). Thus, the procedure can be thought of as a strategy which applies the above rules in a fixed order:

[impl], [circ], [symb].
The procedure shown in Figure 1 might not terminate. Because all Coq functions are terminating, the procedure cannot be encoded as a Coq function. Also, the procedure operates with a set of goals instead of a single goal. In our formalisation, we adapt the inference steps above to work with lists of goals, since in Coq it is more convenient to work with lists rather than sets. One could claim that working with lists might restrict the generality of the procedure, but our encoding does not rely on list-specific features. Another aspect that we have to deal with within our Coq formalisation concerns the renaming of free variables in rl formulas when computing derivatives. Thus, the inference steps [circ] and [symb] have to be changed such that they compute derivatives with conveniently renamed rl formulas.

In Coq, we introduce non-determinism by encoding the procedure as an inductive relation:

ϕ ⇒ ϕ ∈ G M |= ml ϕ → ϕ step(G, G \ {ϕ ⇒ ϕ }) [impl] ϕ ⇒ ϕ ∈ G ϕ c ⇒ ϕ c ∈ G 0 ϕ c ⇒ ϕ c ≈ ϕ c ⇒ ϕ c M |= ml ϕ → ϕ c FV(ϕ c ) ∩ FV(ϕ) = ∅ step(G, G \ {ϕ ⇒ ϕ } ∪ {∆ ϕ c ⇒ϕ c (ϕ ⇒ ϕ )}) [circ] ϕ ⇒ ϕ ∈ G ϕ is S-derivable S ≈ S FV(ϕ) ∩ FV(S ) = ∅ step(G, G \ {ϕ ⇒ ϕ } ∪ ∆ S (ϕ ⇒ ϕ )) [symb]
Here, FV(S ) denotes the list of free variables that occur in all the rl formulas in S . By abuse of notation we write ϕ ⇒ ϕ ∈ G to denote the fact that ϕ ⇒ ϕ is in list G. Intuitively, step relates two lists of goals G and G , where G contains the current goal ϕ ⇒ ϕ , and G contains the remaining goals from G \ {ϕ ⇒ ϕ } and possibly the new goals generated by [circ] and [step]. At each step, only a single goal is removed from G, but zero, one, or more goals can be added. Note that, like in the original procedure (Figure 1) which uses sets, it does not matter which goal is chosen from the list G, we only require that ϕ ⇒ ϕ ∈ G. Also, note that derivatives are always computed using equivalent (w.r.t. ≈) rl formulas whose variables are conveniently renamed.

A successful execution of the non-deterministic version of the procedure is defined using steps:

steps(∅) [base] step(G, G ) steps(G ) steps(G) [steps]
Intuitively, given a set of initial goals G, step is applied multiple times until the goals in G, together with the intermediary ones generated by [circ] and [symb], are all eliminated by [impl].

In [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], for a successful run of the procedure the set F G 0 ∪ i G i is defined, where G 0 is the initial set of goals, G 1 = ∆ S (G 0 ), and G i (i > 1) are the sets of goals generated by each recursive call. In Coq, we define the following relation (which says when a goal g is in F):

g ∈ G 0 g ∈ F [in-G 0 ] step(G, G ) g ∈ G\G G ⊆ F g ∈ F [in-step]
A goal g ∈ F if it is either in G 0 , or there is step where g was eliminated (i.e., step(G, G ) with g ∈ G\G ) and the remaining goals, including the ones introduced by this step, are also in F.

To ensure that this definition is consistent with the one in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], we prove the following technical lemma:

Lemma 2 For all lists of goals G, if steps(G) then G ⊆ F.

Proof We give the proof for the sake of completeness. It goes by induction on steps(G).

The [base] case is trivial because G = ∅ ⊆ F. If [steps] was applied, then we have step(G, G ), steps(G ), and, the inductive hypothesis G ⊆ F. We choose an arbitrary g ∈ G. If g was eliminated by step(G, G ) then g ∈ G \ G , Inria and we get g ∈ F by applying [in-step]. Otherwise, if g was not eliminated by step(G, G ), we trivially show that g ∈ G using the definition of step. Then, we use the inductive hypothesis G ⊆ F, and thus, g ∈ F. Since g was arbitrarily chosen then G ⊆ F.

In particular, if G ∆ S (G 0 ) in Lemma 2 then ∆ S (G 0 ) ⊆ F. We note that steps and F encapsulate the entire execution of the procedure. They also address the monolithic nature of the proof.

Helper lemmas

In this section we present and prove two lemmas that correspond to the additional results (1) and (2) shown in Section 2.2. These lemmas have been also proved in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], but here we reformulate them more precisely.

The first lemma states that every goal which is generated by a successful execution is either eliminated by [impl], or its left hand side is S-derivable. In [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] this lemma is given inside the proof of another lemma, and inherently, it depends on several hypotheses of that lemma. Here, we disentangle the required hypotheses and we formulate it as a stand-alone lemma:

Lemma 3 For all rl formulas ϕ ⇒ ϕ ∈ F, if S is total, all goals in G 0 are S-derivable, and there are γ and ρ such that (γ, ρ) |= ml ϕ then M |= ml ϕ → ϕ or ϕ is S-derivable.

Proof. If ϕ ⇒ ϕ ∈ F then either ϕ ⇒ ϕ ∈ G 0 (cf. [in-G 0 ]
), or there is a step where ϕ ⇒ ϕ is eliminated, i.e, step(G, G ) with ϕ ⇒ ϕ ∈ G\G , and G ⊆ F (cf. [in-step]):

• ϕ ⇒ ϕ ∈ G 0 : trivial, because all goals in G 0 are S-derivable.

• In this case, ϕ ⇒ ϕ was eliminated when applying one of the rules [impl], [circ], or

[symb]:

[impl ] : Trivial: M |= ml ϕ → ϕ .

[circ ]: There is ϕ c ⇒ ϕ c ∈ G 0 such that M |= ml ϕ → ϕ c . We have to show that there are γ 0 , γ 1 , and ρ such that (γ 0 , ρ ) |= ml ϕ and γ 0 ⇒ S γ 1 . Let us choose γ 0 γ and ρ ρ. We easily obtain (γ, ρ) |= ml ϕ from the hypothesis. In order to get a transition from γ we use the fact that S is total: first, M |= ml ϕ → ϕ c implies (γ, ρ) |= ϕ c , that is, there is a valuation ρ such that ρ (x) = ρ(x) for all x ∈ FV(ϕ c ) and (γ, ρ ) |= ϕ c (cf. |= ∃ ); second, from (γ, ρ ) |= ϕ c , ϕ c is S-derivable (because ϕ c ⇒ ϕ c ∈ G 0 ), and S total we obtain γ such that γ ⇒ S γ .

[symb ]: Trivial: ϕ is S-derivable.

The second lemma states that for every transition γ ⇒ S γ which starts from ϕ there is a symbolic successor ϕ of ϕ such that γ is an instance of ϕ . The lemma can be generalised to paths, that is, one can prove that for a concrete execution path there is a symbolic one which covers it. There are two important conditions required by this lemma: all rules from S have distinct free variables from variables in ϕ and all formulas from S and G 0 are well-formed. In [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] these conditions hold thanks to assumption (a 1 ). Here, we add these conditions as hypotheses:

Lemma 4 For all transitions γ ⇒ S γ , for all valuations ρ, and for all formulas ϕ, if (γ, ρ) |= ml ϕ, f ∈ S ∪ G 0 implies wf(f ), and FV(S) ∩ FV(ϕ) = ∅, then there are α ∈ S and ϕ ∆ α (ϕ) such that (γ , ρ) |= ml ϕ .

Proof The proof is constructive in the sense that we explicitly provide α and ϕ . The transition γ ⇒ S γ implies that there is a rule ϕ l ⇒ ϕ r ∈ S and a valuation ρ such that (γ, ρ ) |= ϕ l and (γ , ρ ) |= ϕ r .

Let us choose α ϕ l ⇒ ϕ r ∈ S and ϕ ∆ ϕ l ⇒ϕr (ϕ). For the chosen ϕ we have to prove (γ , ρ ) |= ml ϕ , that is, (γ , ρ ) |= ml (∃FV(ϕ l ))(ϕ l ∧ ϕ r ) =? ∧ ϕ r . This is equivalent (cf. |= ∃ ) to showing that there is a valuation ρ : Var → M such that ρ (x) = ρ (x) for all x ∈ FV(ϕ l ) and (γ , ρ ) |= ml (ϕ l ∧ ϕ r ) =? ∧ ϕ r . Let ρ (ρ, ρ , FV(ϕ l )). By ∈ we have ρ (x) = (ρ, ρ , FV(ϕ l ))(x) = ρ (x) for all x ∈ FV(ϕ l ). There remains to show that (γ , ρ ) |= ml (ϕ l ∧ ϕ r ) =? ∧ ϕ r , that is (cf. |= ∧ ), (γ , (ρ, ρ , FV(ϕ l ))) |= ml (ϕ l ∧ ϕ r ) =? and (γ , (ρ, ρ , FV(ϕ l ))) |= ml ϕ r .

The first part is equivalent to showing that there is γ 0 such that (γ 0 , (ρ, ρ , FV(ϕ l ))) |= ml ϕ l ∧ ϕ r (cf. |= =? ). Let γ 0 γ. On one hand, from (γ, ρ ) |= ml ϕ l we obtain (γ 0 , (ρ, ρ , FV(ϕ l ))) |= ml ϕ l (cf. |= ⊆ ), and on the other hand, from (γ, ρ) |= ml ϕ we obtain (γ 0 , (ρ, ρ , FV(ϕ l ))) |= ml ϕ (cf. |= ⊆ ). Then, using |= ∧ we obtain (γ 0 , (ρ, ρ , FV(ϕ l ))) |= ml ϕ l ∧ ϕ r .

Next, since ϕ l ⇒ ϕ r ∈ S then wf(ϕ l ⇒ ϕ r ), i.e, FV(ϕ r ) ⊆ FV(ϕ l ). Therefore, using |= ⊆ and the fact that (γ , ρ ) |= ml ϕ r we obtain (γ , (ρ, ρ , FV(ϕ l ))) |= ml ϕ r .

The soundness for finite paths

The proof of the soundness theorem (sketched in Section 2.2) depends on an intermediate technical lemma (Lemma 1). In this section we reformulate the lemma by adding all the hypotheses needed by its proof so that it does not rely on hidden assumptions. Briefly, assuming a successful execution steps(∆ S (G 0 )), the lemma states that for all complete finite paths τ , and for all formulas ϕ ⇒ ϕ ∈ F such that τ starts from ϕ with a valuation ρ, (τ, ρ) satisfies ϕ ⇒ ϕ . The lemma can be thought of as a version of soundness for finite paths, which involves all the goals in F, not only those from G 0 . Its proof is by induction on the number of the transitions from the path τ .

With respect to [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], there are several significant differences. First, the proof takes into account the fact that derivatives are computed with renamed rl formulas. Second, we find and fix the flaw from the proof in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], where a false assumption about the goals in F is made: given a successful execution of the procedure starting with ∆ S (G 0 ), all the goals in F are eliminated by a step of the procedure. This cannot be true, since F includes G 0 , but the procedure only processes goals starting with ∆ S (G 0 ). The assumption does not invalidate the result from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], but it makes the proof incomplete. In fact, the goals in G 0 , which are of interest in the soundness theorem, are not handled. This flaw was detected only when formalising the proof in Coq. To fix it, we add a new hypothesis: the free variables that occur in rules in S and those that occur in rules in G 0 constitute disjoint sets (i.e., FV(S) ∩ FV(G 0 ) = ∅).

In the following, we formulate the lemma, and we emphasise the main changes that occur in this proof (w.r.t. to the one in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]) using gray font.

Lemma 5 For all finite and complete paths τ , for all valuations ρ, and for all formulas ϕ ⇒ ϕ ∈ F, if (τ, ρ) startsFrom ϕ, G 0 = ∅, wfPath(τ ), steps(∆ S (G 0 )), S is total, the left hand sides of goals in G 0 are S-derivable, all formulas in S ∪ G 0 are well formed, and FV(S) ∩ FV(G 0 ) = ∅, then (τ, ρ) |= rl ϕ ⇒ ϕ .

Proof Let n be the the number of transitions in τ . The proof is by well-founded induction on n: Inria the derivative is computed using a renaming of the circularity. Also, here we do not rely on assumption (a 1 ) (Section 2.2).

By the definition of derivatives, we have to show (γ j , ρ) |= ml (∃(FV(ϕ c ))(ϕ c ∧ ϕ) =? ∧ ϕ c (note that ϕ c ⇒ ϕ c ≈ ϕ c ⇒ ϕ c and FV(ϕ c ) ∩ FV(ϕ c ) = ∅). This reduces to showing that there is a valuation ρ such that ρ (x) = ρ(x) for all x ∈ FV(ϕ c ) and

(γ j , ρ ) |= ml (ϕ c ∧ ϕ) =? ∧ ϕ c (cf. |= ∃ ).
Before providing ρ , we apply ≈ ∼ for ϕ c ⇒ ϕ c ≈ ϕ c ⇒ ϕ c and ρ to obtain a valuation ρ * : Var → M such that (ϕ c , ρ ) ∼ (ϕ c , ρ * ) and (ϕ c , ρ ) ∼ (ϕ c , ρ * ).

Next, we consider ρ = (ρ, ρ * , FV(ϕ c )). The condition (ρ, ρ * , FV(ϕ c ))(x) = ρ(x) for all x ∈ FV(ϕ c ) is directly obtained using ∈ . Therefore, there remains to prove (γ j , (ρ, ρ * , FV(ϕ c ))) |= ml (ϕ c ∧ ϕ) =? ∧ ϕ c , that is, (γ j , (ρ, ρ * , FV(ϕ c ))) |= ml (ϕ c ∧ ϕ) =? and (γ j , (ρ, ρ * , FV(ϕ c ))) |= ml ϕ c (cf. |= ∧ ). The latter can be proved using |= ⊆ in combination with FV(ϕ c ) ⊆ FV(ϕ c ) (because ϕ c ⇒ ϕ c ) is wellformed), and then using (ϕ c , ρ ) ∼ (ϕ c , ρ * ) and the fact that (γ j , ρ ) |= ml ϕ c . For the former, (γ j , (ρ, ρ * , FV(ϕ c ))) |= ml (ϕ c ∧ ϕ) =? , we use |= =? and we equivalently prove that there is γ = γ 0 such that (γ 0 , (ρ, ρ * , FV(ϕ c ))) |= ml ϕ c ∧ ϕ: first, (γ 0 , (ρ, ρ * , FV(ϕ c ))) |= ml ϕ c is obtained using |= ⊆ , (ϕ c , ρ ) ∼ (ϕ c , ρ * ), and (γ 0 , ρ ) |= ml ϕ c ; second, (γ, (ρ, ρ * , FV(ϕ c ))) |= ml ϕ is given directly by |= ⊆ and the fact that (γ 0 , ρ) |= ml ϕ.

Now, (γ

j , ρ) |= ml ∆ ϕ c ⇒ϕ c (ϕ) implies (τ | j , ρ) startsFrom ∆ ϕ c ⇒ϕ c (ϕ). Moreover, ∆ ϕ c ⇒ϕ c (ϕ ⇒ ϕ ) ∈ G ⊆ F because it has been just added to G by [circ]. Thus, we apply the inductive hypothesis for (τ | j , ρ) (the length of τ | j is n -j < n) and ∆ ϕ c ⇒ϕ c (ϕ ⇒ ϕ ) to obtain (τ | j , ρ) |= ∆ ϕ c ⇒ϕ c (ϕ ⇒ ϕ ), i.e, there is γ i such that (γ i , ρ) |= ml ϕ .
[symb ] The path τ contains at least the first transition γ 0 ⇒ S γ 1 because n > 0.

In [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], the next step in the proof is to apply Lemma 4 for γ 0 ⇒ S γ 1 and (γ 0 , ρ) |= ml ϕ. Here, we show first that γ 0 ⇒ S γ 1 . By definition, the transition γ 0 ⇒ S γ 1 implies that there is a rule ϕ l ⇒ ϕ r ∈ S and a valuation ρ such that (γ 0 , ρ ) |= ml ϕ l and (γ 1 , ρ ) |= ml ϕ r . Since S ≈ S then for any ϕ l ⇒ ϕ r ∈ S there is ϕ l ⇒ ϕ r ∈ S such that ϕ l ⇒ ϕ r ≈ ϕ l ⇒ ϕ r . This implies that there is ρ such that (ϕ l , ρ ) ∼ (ϕ l , ρ ) and (ϕ r , ρ ) ∼ (ϕ r , ρ ) (cf. ≈ ∼ ). By the definition of ∼, we obtain (γ 0 , ρ ) |= ml ϕ l and (γ 1 , ρ ) |= ml ϕ r ; thus, γ 0 ⇒ ϕ l ⇒ϕ r γ 1 , i.e, γ 0 ⇒ S γ 1 .

Then, since (γ 0 , ρ) |= ml ϕ and γ 0 ⇒ S γ 1 , by Lemma 4 there are α ∈ S and ϕ 1 ∆ α (ϕ) such that (γ 1 , ρ) |= ml ϕ 1 . Note that Lemma 4 requires that ϕ ⇒ ϕ is well-formed (from the inductive hypothesis), FV(ϕ) ∩ FV(S ) = ∅ (again, from the inductive hypothesis), and all formulas in S are well-formed (because those in S are well-formed). The next step in the proof is to apply the inductive hypothesis for τ | 1 (which is well-formed and complete of length n -1) and ϕ 1 ⇒ ϕ . On the one hand, we have (γ 1 , ρ) |= ml ϕ 1 and thus, τ | 1 startsFrom ϕ 1 . On the other hand, since ϕ 1 ∆ α (ϕ) ∈ ∆ S (ϕ) then the rl formula ϕ 1 ⇒ ϕ ∈ ∆ S (G 0 ) ⊆ G ⊆ F because ∆ S (G 0 ) has been just added to G by [symb]. By the inductive hypothesis we obtain (τ | 1 , ρ) |= ml ϕ 1 ⇒ ϕ , i.e, there is γ i such that (γ i , ρ) |= ml ϕ.

Inria

The soundness theorem

In this section we show the formalisation of the soundness theorem and its proof. Several assumptions from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] are here transformed in hypotheses: all formulas in S and G 0 are well formed and for all the goals ϕ ⇒ ϕ in G 0 ϕ is S-derivable. Moreover, we add the additional hypothesis required by lemma 5: FV(S) ∩ FV(G 0 ) = ∅.

Theorem 2 If S is total, all formulas in S ∪ G 0 are well-formed, the left hand sides of goals in G 0 are S-derivable, FV(S) ∩ FV(G 0 ) = ∅, and steps(∆ S (G 0 )) then ⇒ S |= rl G 0 .

Proof. We arbitrarily choose ϕ ⇒ ϕ ∈ G 0 . S |= rl ϕ ⇒ ϕ iff for all complete paths τ and all valuations ρ : Var → M with (τ, ρ) startsFrom ϕ we have (τ, ρ) |= rl ϕ ⇒ ϕ . If τ is infinite, then, by definition, (τ, ρ) |= rl ϕ ⇒ ϕ . If τ is finite of length n, then, by lemma 5 (note that ϕ ⇒ ϕ ∈ G 0 ⊆ F and G 0 = ∅), (τ, ρ) |= rl ϕ ⇒ ϕ . Since ϕ ⇒ ϕ was arbitrarily chosen from G 0 , we have S |= G 0 .

Overview of the formal proof The formal proof of the soundness of the procedure was developed using version 8.4pl5 of the Coq proof assistant. The code can be found at: https: //fmse.info.uaic.ro/imgs/soundness-proof.tar.gz. The archive also contains additional information about the code organisation and instructions for compilation. The Coq code is spread over several files. The main file is called sound.v and it contains the definitions for step and steps; it also includes several helper lemmas and, at the end of the file, the main lemmas and the soundness theorem shown in Section 3. The axioms that we use for ml (shown in Section 3.1) can be found in ml.v. The definition of rl, derivatives, and the other related notions from Section 3.2 are located in rl.v and derivatives.v.

Conclusions

In this paper we present the Coq formalisation of the soundness of a procedure for program verification that was proposed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. The procedure is formalised as an inductive relation, and, unlike in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], it explicitly handles the renaming of the free variables in rl formulas when computing derivatives. We precisely formulate the intermediary lemmas and the soundness theorem, and then we prove them in Coq. During the development of the proof in Coq we discovered (and fixed) some flaws in the proof from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF].

Alternative proofs for the soundness of the procedure from [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF] can be found in [START_REF] Arusoaie | Verifying Reachability-Logic Properties on Rewriting-Logic Specifications[END_REF] and [START_REF] Arusoaie | A Generic Framework for Symbolic Execution[END_REF]. However, those are less suitable to be encoded in Coq: the proof in [START_REF] Arusoaie | Verifying Reachability-Logic Properties on Rewriting-Logic Specifications[END_REF] is more intuitive (it uses a digraph for visualisation) but not that precise, while the one in [START_REF] Arusoaie | A Generic Framework for Symbolic Execution[END_REF] uses coinduction; however, Coq's support for coinduction is not as good as the one for induction (e.g., no coinduction principle is generated automatically).

Future work In terms of future work there are several directions to follow. The first one consists in extracting a certified OCaml program from our inductive relation, and then use it for verification within the K framework. This requires rl-based semantics of languages in OCaml, which could be extracted from corresponding semantics in Coq, an effort already underway in the K team, who are developing a Coq backend [START_REF] Moore | Program verification by coinduction[END_REF] for K.

Another future work is related to a computational definition of derivatives, based on rewriting, which is also proposed in [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. It is there shown equivalent to the current (logical) definition of derivatives. A step further would be to formalise that proof of equivalence as well, thereby obtaining a more efficient certified program-verification procedure.

Figure 1 :

 1 Figure 1: rl verification procedure. ϕ c denotes (∃FV(ϕ c ))ϕ c .

RR n°471

Case n = 0. Here, τ γ 0 and complete(τ, 0). We use Lemma 3 for ϕ ⇒ ϕ ∈ F and (γ 0 , ρ) |= ml ϕ (implied by (τ, ρ) startsFrom ϕ) to split the proof in two cases: M |= ml ϕ → ϕ or ϕ is S-derivable:

• If M |= ml ϕ → ϕ and (γ 0 , ρ) |= ml ϕ then (γ 0 , ρ) |= ml ϕ . Finally, (τ, ρ) |= rl ϕ ⇒ ϕ is obtained directly using the definition of |= rl with i = 0, n = 0, and γ = γ 0 .

• If ϕ is S-derivable then, by the definition of totality of S and (γ 0 , ρ) |= ml ϕ there is γ such that γ ⇒ S γ . On the other hand, complete(τ, 0) implies terminating(γ 0 ), which, by definition, means that there is no γ such that γ ⇒ S γ . Thus, we obtain a contradiction.

Case n > 0. Let τ γ 0 ⇒ S • • • ⇒ S γ n and complete(τ, n). The inductive hypothesis holds for all complete paths of length strictly less than n, that are well-formed and start from the left hand side of a goal in F. We have to show that (τ, ρ) |= rl ϕ ⇒ ϕ , that is, (τ, ρ) startsFrom ϕ and there is γ i such that (γ i , ρ) |= ml ϕ . The first part is given already in the hypothesis of the lemma, so it remains to find γ i such that

• This case was overlooked in the paper proof [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF]. Assume ϕ ⇒ ϕ ∈ G 0 . Since τ has length n > 0 then there is at least one transition γ 0 ⇒ S γ 1 in τ . Using Lemma 4 and (γ 0 , ρ) |= ml ϕ, there are α ∈ S and ϕ 1 ∆ α (ϕ) such that (γ 1 , ρ) |= ml ϕ 1 . Note that Lemma 4 requires that ϕ ⇒ ϕ is well-formed and FV(ϕ) ∩ FV(S) = ∅, all formulas in S are well-formed, and all the free variables occurring in them are different from those in ϕ. All these can be trivially proved using the hypotheses of the lemma. First, from ϕ ⇒ ϕ ∈ G 0 , and FV(S) ∩ FV(G 0 ) = ∅ we get FV(ϕ) ∩ FV(S) = ∅. Second, if τ is complete and well-formed then τ | 1 is also complete and well-formed. Finally, since τ has length n(> 0) then τ | 1 has length n -1.

The next step in the proof is to apply the inductive hypothesis for τ | 1 and ϕ 1 ⇒ ϕ . For this, we show that τ | 1 startsFrom ϕ 1 and ϕ 1 ⇒ ϕ ∈ F. First, the fact that τ | 1 startsFrom ϕ 1 is implied by (γ 1 , ρ) |= ml ϕ 1 . Second, since ϕ 1 ∆ α (ϕ) ∈ ∆ S (ϕ) and ϕ ⇒ ϕ ∈ G 0 then the rl formula ϕ 1 ⇒ ϕ ∈ ∆ S (G 0 ) ⊆ F (cf. Lemma 2 with G ∆ S (G 0 )). Now, by the inductive hypothesis, (τ | 1 , ρ) |= ml ϕ 1 ⇒ ϕ , i.e., there is γ i such that (γ i , ρ) |= ml ϕ .

• If step(G, G ), ϕ ⇒ ϕ ∈ G \ G , and G ⊆ F, then ϕ ⇒ ϕ was eliminated when applying one of the rules [impl], [circ], or [step]:

[impl ] : ϕ ⇒ ϕ ∈ G and M |= ϕ → ϕ . Trivial: from (γ 0 , ρ) |= ml ϕ and M |= ϕ → ϕ we have (γ 0 , ρ) |= ml ϕ .

[circ ] : there are

The inductive hypothesis applied for (τ | 1 , ρ ) (the length of τ | 1 is n -1 < n) and ϕ 1 ⇒ ϕ c , implies (τ | 1 , ρ ) |= rl ϕ 1 ⇒ ϕ c , that is, there is γ j such that (γ j , ρ ) |= ml ϕ c . The next step in our proof is to show that (γ j , ρ) |= ml ∆ ϕ c ⇒ϕ c (ϕ). With respect to [START_REF] Lucanu | Verifying reachability-logic properties on rewriting-logic specifications[END_REF], this part of the proof follows the same pattern, but it takes into account that