Jean-Christophe Filliâtre

Léon Gondelman

Andrei Paskevich

Keywords:

In the context of deductive program verification, ghost code is a part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in the program outcome. In particular, ghost data cannot participate in regular computations and ghost code cannot mutate regular data or diverge. The idea exists in the folklore since the early notion of auxiliary variables and is implemented in many state-of-the-art program verification tools. However, ghost code deserves rigorous definition and treatment, and few formalizations exist.

In this article, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Introduction

A common technique in deductive program verification consists in introducing data and computations, traditionally named ghost code, that only serve to facilitate specification. Ghost code can be safely erased from a program without affecting its final result. Consequently, a ghost expression cannot be used in a regular (non-ghost) computation, it cannot modify a regular mutable value, and it cannot raise exceptions that would escape into regular code. However, a ghost expression can use regular values and its result can be used in program annotations: preconditions, postconditions, loop invariants, assertions, etc. A classical use case for ghost code is to equip a data structure with ghost fields containing auxiliary data for specification purposes. Another example is ghost step counters to prove the time complexity of an algorithm.

When it comes to computing verification conditions, for instance using a weakest precondition calculus, there is no need to make a distinction between ghost and regular code. At this moment, ghost code is just a computation that supplies auxiliary values to use in specification and to simplify proofs. This computation, however, is not necessary for the program itself and thus should be removed when we compile the annotated source code. Therefore we need a way to ensure, by static analysis, that ghost code does not interfere with the rest of the program.

Despite that the concept of ghost code exists since the early days of deductive program verification, and is supported in most state-of-the-art tools [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF][START_REF] Cohen | VCC: A practical system for verifying concurrent C[END_REF][START_REF] Jacobs | The VeriFast program verifier[END_REF][START_REF] Filliâtre | Why3 -where programs meet provers[END_REF], it deserves a proper formal treatment. In particular, a sound non-interference analysis must ensure that every ghost sub-expression terminates. Otherwise, one could supply such a sub-expression with an arbitrary postcondition and thus be able to prove anything about the program under consideration. Another non-obvious observation is that structural equality cannot be applied naively on data with ghost components. Indeed, two values could differ only in their ghost parts and consequently the comparison would yield a different result after the ghost code erasure.

There is a number of design choices that show up when conceiving a language with ghost code. First, how explicit should we be in our annotations? For example, should every ghost variable be annotated as such, or can we infer its status by looking at the values assigned to it? Second, how much can be shared between ghost and regular code? For instance, can a ghost value be passed to a function that does not specifically expect a ghost argument? Similarly, can we store a ghost value in a data structure that is not specifically designed to hold ghost data, e.g. an array or a tuple? Generally speaking, we should decide where ghost code can appear and what can appear in ghost code.

In this article, we show that, using a tailored type system with effects, we can design a language with ghost code that is both expressive and concise. As a proof of concept, we describe a simple ML-style programming language with mutable state, recursive functions, and ghost code. Notably, our type system allows the same data types and functions to be used in both regular and ghost code. We give a formal proof of the soundness of ghost code erasure, using a bisimulation argument. A type system based on the same concepts is implemented in the verification tool Why3 [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF]. The language presented is this paper is deliberately simplified. The more exciting features, listed in Section 5 and implemented in Why3, only contribute to more complex effect tracking in the type system, which is mostly orthogonal to the problem of ghost code non-interference. This paper is organized as follows. Sec. 2 illustrates the use of ghost code on an example. Sec. 3 introduces an ML-like language with ghost code. Sec. 4 defines the operation of ghost code erasure and proves its soundness. Sec. 5 describes the actual implementation in Why3. We conclude with related work in Sec. [START_REF] Hatcliff | Behavioral interface specification languages[END_REF] and perspectives in Sec. 7.

A Tiny Program Featuring Ghost Code

Consider the following program fibo that computes F n , the n-th Fibonacci number, using an auxiliary function aux: let rec aux a b n = if n = 0 then a else aux b (a+b) (n-1)

let fibo n = aux 0 1 n
To prove the correctness of this program using deductive verification, we supply a suitable specification. Let us assume a specification language with contracts [START_REF] Hatcliff | Behavioral interface specification languages[END_REF],

where requires introduces a precondition and ensures introduces a postcondition.

A possible specification would be the following:

let rec aux (a b n: int) : int requires { 0 ≤ n } requires { ∃k. 0 ≤ k ∧ a = F k ∧ b = F k+1 } ensures { ∃k. 0 ≤ k ∧ a = F k ∧ b = F k+1 ∧ result = F k+n } = if n = 0 then a else aux b (a+b) (n-1) let fibo (n: int) : int requires { 0 ≤ n } ensures { result = F n } = aux 0 1 n
Even if acceptable, this specification has several drawbacks: first, some information is duplicated between the pre-and the postcondition; second, it uses existential quantifiers, which makes the specification less readable and the proof less amenable for automation.

One way to simplify the specification is to turn quantifiers into something more constructive, where the existence of k is materialized by an extra argument to function aux, as follows:

let rec aux (k: int) (a b n: int) : int requires { 0 ≤ k ∧ 0 ≤ n } requires { a = F k ∧ b = F k+1 } ensures { result = F k+n } = if n = 0 then a else aux (k+1) b (a+b) (n-1)
When performing the recursive call to aux, we provide the suitable value for this extra argument. Similarly, we provide the initial value for k when calling aux in fibo:

let fibo (n: int) : int requires { 0 ≤ n } ensures { result = F n } = aux 0 0 1 n
Such an extra computation, used only for the purpose of specification, is precisely what we call ghost code (here in blue). The point is that we can erase ghost code, once the verification is completed, to recover the original program. On this example, it is easy to check that ghost computations have no impact on the program outcome.

Generally speaking, we need a way to check/enforce non-interference of ghost code with regular computations. The purpose of this article is to introduce a type system to do this.

This example also illustrates a desirable feature of ghost code, that is, the ability to reuse the same data types and operations in both regular and ghost code. Here, we reuse type int, numeric constants, and addition. Generally speaking, we may want to do this with arbitrary user-defined types and operations. We will show that our type system is sufficiently flexible to permit such reuse.

GhostML

We introduce GhostML, a minimal ML-like language with ghost code. It features global references (that is, mutable variables), recursive functions, as well as integer and Boolean primitive types.

Syntax

The syntax of GhostML types and expressions is given in Fig. 1 and2, respectively. Types are either primitive data types or function types. A function type is an arrow τ β 1 =⇒ τ 2 , where τ 1 is the type of the argument and τ 2 is the type of the result. The superscript β attached to t 1 indicates the ghost status of the parameter: denotes a ghost parameter and ⊥ a regular one (here and below, "regular" stands for "non-ghost"). The latent effect of the function, denoted , is a Boolean value which indicates possible non-termination or modification of a regular reference. This latent effect is realised whenever the function is applied. Terms are either values or compound expressions like application, conditional, reference access, and modification. All the language constructions are standard ML, except for the keyword ghost which turns a term into ghost code. We write x β , y β , f β , g β and r β , s β to denote respectively variables and references, that is, we distinguish references and variables syntactically. Unlike variables, references are not valid expressions, they can only be used in a term via assignment and dereference. We assume a fixed finite set of global references. Every variable, function parameter, and reference is annotated with its ghost status β. Consider the following example:

τ ::= types | κ primitive type | τ β =⇒ τ functional type κ ::= primitive types | int | bool | unit primitive types β ∈ {⊥, } ghost status ∈ {⊥, } effect
t ::= terms | v value | t v application | let x β = t in t local binding | if v then t else t conditional | r β := v assignment | !r β dereference | ghost t ghost code v ::= values | x β variable | c constant | λx β : τ. t anonymous function | rec f β : τ β =⇒ τ.
let upd = λx ⊥ : int. s := x ⊥ in upd !r ⊥
Here, ghost function upd takes one regular parameter x ⊥ and assigns it to a ghost reference s . Then upd is applied to the contents of a regular reference r ⊥ . In practice, some ghost status annotations (e.g., those of locally defined variables) can be inferred using the typing rules, and do not need to be supplied by the user.

Note that compound terms follow a variant of A-normal form [START_REF] Flanagan | The essence of compiling with continuations[END_REF]. That is, in application, conditional, and reference assignment, one of the sub-expressions must be a value. This does not reduce expressiveness, since a term such as (t 1 t 2 ) can be rewritten as let x β = t 2 in t 1 x β , where β is the ghost status of the first formal parameter of t 1 .

MiniML Syntax. The syntax of traditional MiniML can be obtained by omitting all ghost indicators β (on references, variables, parameters, and types) and excluding the ghost construct. Equivalently, we could define MiniML as the subset of GhostML where all ghost indicators β are ⊥ and where terms of the form ghost t do not appear.

Semantics

In Fig. 3, we give a small-step operational semantics to GhostML which corresponds to a deterministic call-by-value reduction strategy. An execution state is a pair µ • t of a term t and a store µ, which maps global references to constants. Each reduction rule defines a state transition during one step of execution. The contextual reduction rules (E-Context-App) and (E-Context-Let) identify the subterm to be reduced (called the redex) whereas other rules apply to redex itself. In the rules, we omit the store µ when it is not changed during the reduction step.

ghost t 1 → t 1 (E-Ghost) 1 ≤ m < arity(c 0 ) c 0 c 1 . . . c m → λx ⊥ : κ. c 0 c 1 . . . c m x ⊥ (E-Op-λ) m = arity(c 0 ) δ(c 0 , c 1 , . . . , c m ) is defined c 0 c 1 . . . c m → δ(c 0 , c 1 , . . . , c m ) (E-Op-δ) (λx β : τ. t 1 ) v → t 1 [x β ← v] (E-App-λ) v 0 = rec f β : τ β =⇒ τ. λx β : τ. t 1 (v 0 v) → t 1 [x β ← v, f β ← v 0 ] (E-App-Rec) let x β = v in t 1 → t 1 [x β ← v] (E-Let) if true then t 1 else t 2 → t 1 (E-If-True) if false then t 1 else t 2 → t 2 (E-If-False) µ(r β ) = c µ • !r β → µ • c (E-Deref) µ • (r β := c) → [r β → c]µ • () (E-Assign) µ • t 1 → µ • t 1 µ • (t 1 v) → µ • (t 1 v) (E-Context-App) µ • t 1 → µ • t 1 µ • (let x β = t 1 in t 2 ) → µ • (let x β = t 1 in t 2 ) (E-Context-Let)
Rule (E-Ghost) expresses that, from the point of view of operational semantics, there is no difference between regular and ghost code. Other rules are standard. For instance, rules (E-Op-λ) and (E-Op-δ) evaluate the application of a constant c 0 to constants c 1 . . . c m . Such an application either is partial (1 ≤ m < arity(c 0 )), and then turns into a function λx ⊥ : κ. c 0 c 1 . . . c m x ⊥ , or is total (m = arity(c 0 )), and then some oracle function δ gives the result δ(c 0 , c 1 , . . . , c m ). For instance, δ(not, true) = false, δ(+, 47, -5) = 42, etc.

As usual, → denotes the reflexive, transitive closure of →. We say that a closed term t evaluates to value v in a store µ if there is a µ such that µ • t → µ • v. Note that, since t is closed, and the reduction rules do not free variables, v is either a constant or a function, and not a variable. Finally, the divergence of a term t in a store µ is defined co-inductively as follows:

µ • t → µ • t µ • t → ∞ µ • t → ∞ (E-Div)
MiniML Semantics. Since ghost statuses do not play any role in the semantics of GhostML, dropping them (or, equivalently, marking all β as ⊥) and removing the rule (E-Ghost) results in a standard call-by-value small-step operational semantics for MiniML. For the sake of clarity, we use a subscript m when writing MiniML reduction steps: µ • t → m µ • t .

Type System

The purpose of the type system is to ensure that "well-typed terms do not go wrong". In our case, "do not go wrong" means not only that well-typed terms verify the classical type soundness property, but also that ghost code does not interfere with regular code. More precisely, non-interference means that ghost code never modifies regular references and that it always terminates. For that purpose, we introduce a type system with effects, where the typing judgement is

Γ • Σ t : τ • β • .
Here, τ is the type of term t. Boolean values β and indicate, respectively, the ghost status of t and its regular side effects. Typing environment Γ binds variables to types. Store typing Σ binds each global reference r β to the primitive type of the stored value. We restrict types of stored values to primitive types in order to avoid a possible non-termination via Landin's knot (that is, recursion encoded using a reference containing a function), which would be undetected in our type system.

Typing rules are given in Fig. 4. To account for non-interference, each rule whose conclusion is a judgement Γ • Σ t : τ • β • comes with the implicit side condition

β =⇒ ¬ ∧ ¬ + (τ ) (1)
where + (τ ) is defined recursively on τ as follows:

+ (κ) ⊥ + (τ β 2 =⇒ τ 1 ) ∨ + (τ 1 )
In other words, side condition (1) stands for the type system invariant to ensure that, whenever t is ghost, it must terminate and must not modify regular references. Note that a weaker form of the invariant β =⇒ ¬ is acceptable, but we strengthen it with ¬ + (τ ) to reject functions whose latent effect would violate the non-interference once the function is applied.

Let us explain some rules in detail. The rule (T-Const) states that any constant c is regular, pure, and terminating (i.e., β = ⊥ and = ⊥). Moreover, we assume that if c is some constant operation, then its formal parameters are all regular. The type of each constant is given by some oracle function Typeof(c). For instance,

Typeof(+) = int ⊥ ⊥ =⇒ int ⊥ ⊥ =⇒ int. Typeof(c) = τ Γ • Σ c : τ • ⊥ • ⊥ (T-Const) Γ(x β ) = τ Γ • Σ x β : τ • β • ⊥ (T-Var) Σ(r β ) = κ Γ • Σ !r β : κ • β • ⊥ (T-Deref) Γ • Σ t 1 : τ • β • ⊥ Γ • Σ (ghost t 1 ) : τ • • ⊥ (T-Ghost) [x β → τ ]Γ • Σ t 1 : τ 1 • β 1 • Γ • Σ (λx β : τ. t 1 ) : τ β =⇒ τ 1 • β 1 • ⊥ (T-λ) 0 = CheckTermination(rec f β 1 : τ 0 . λx β : τ 2 . t 1 ) τ 0 = (τ β (T-App ) Γ • Σ v : κ • β • ⊥ Σ(r β ) = κ β ≥ β Γ • Σ (r β := v) : unit • β • ¬β (T-Assign)
Fig. [START_REF] Jacobs | The VeriFast program verifier[END_REF] Typing rules.

The rule (T-λ) shows that the ghost status of an abstraction is the ghost status of its body. Note also that effects of the body become latent, while function itself has no effects.

The rule (T-Rec) gives the typing for recursive functions. Recall that ghost code must always terminate, and that termination is in general undecidable. The easiest solution therefore would be to enforce that no recursive function is ever used in ghost code, that is, to assign recursive functions a latent non-termination effect. In practice, however, we want to accept recursive functions whose termination can be established by static analysis. To do so, we assume the existence of an oracle function CheckTermination which, given a recursive definition, returns ⊥ if it can prove the function terminating, and otherwise. By terminating, we mean that any call terminates, whatever the store and the argument. A typical example of such an oracle would be the generation of verification conditions from user-provided variants (as in our forthcoming example on page 21). Note that the oracle is not taking non-interference into account, so it does not have to distinguish between ghost and regular code. The rule (T-Rec) imposes that the latent effect of the recursive function ( 1) is no smaller than the effect computed by the oracle, that is 1 ≥ 0 . Similarly, if the body of the recursive function is ghost ( β 0 = ), then the recursive function must be ghost as well (

β 1 = ), that is β 1 ≥ β 0 .
The rule (T-If) shows how ghost code is propagated through conditional expressions: if at least one of the branches or the Boolean condition is ghost code, then the conditional itself becomes ghost. Note, however, that the side condition (1) will reject conditionals where one part is ghost and another part has some effect, as in if true then r ⊥ := 42 else ghost ().

The rule (T-Ghost) turns any term t into ghost code, provided that t is pure and terminating. Thus, terms like ghost (r ⊥ := 42) are ill-typed, since their evaluation would interfere with the evaluation of regular code.

The side condition β ≥ β of the rule (T-Assign) ensures that regular references cannot be assigned ghost code. (Boolean values are ordered as usual, with > ⊥.) Additionally, the rule conclusion ensures that is if and only if the assigned reference is regular (β = ⊥), i.e., ghost reference assignments are not part of regular effects.

The most subtle rules are those for local binding and application. Rule (T-Let ) states that, whatever the ghost status of a term t 1 is, as long as t 1 is pure and terminating, we can bind a ghost variable x to t 1 . Notice that the resulting letexpression is not necessarily ghost: the type system knows that the value stored in x is ghost and will ensure the non-interference of subsequent uses of x . Similarly, by rule (T-App ) a function that expects a ghost parameter can be applied to both ghost and regular values. Once again, the result may be regular.

Consider the following example1 where we trace an update of a regular reference r ⊥ by using a ghost function succ :

let succ = λy : int. (y + 1) in let x ⊥ = !r ⊥ in let trace = succ x ⊥ in r ⊥ := x ⊥ + 1
With the rule (T-App ), we can apply succ to the current value of r ⊥ , even if we store it in the regular variable x ⊥ . Then, thanks to rule (T-Let ) we are able to "contain" ghost computation (succ x ⊥ ) in trace which may be used in subsequent computations without interfering with regular code.

Rule (T-Let ⊥ ) is somewhat dual to (T-Let ): when binding a regular variable x ⊥ to a ghost term, the type system expands the ghost status to the whole letexpression, "contaminating" it. Similarly, rule (T-App ⊥ ) allows us to pass a ghost value to a function expecting a regular parameter, in which case the application itself becomes ghost.

Let us look again at the previous example. We can notice that since successor function succ is ghost, we cannot use it in regular code and thus cannot replace r ⊥ := x ⊥ + 1 by r ⊥ := succ x ⊥ . Given that the successor function is pure and terminating, it is more natural to define it as regular code and then reuse it in ghost computations. The rule (T-Let ⊥ ) allows us to improve the code in this way:

let succ ⊥ = λy ⊥ : int. (y ⊥ + 1) in let x ⊥ = !r ⊥ in let trace = succ ⊥ x ⊥ in r ⊥ := succ ⊥ x ⊥
To sum up, while rules (T-Let ) and (T-App ) stop the expansion of ghost code thanks to the explicit ghost status of bound variables, the purpose of rules (T-Let ⊥ ) and (T-App ⊥ ) is to allow ghost code to use regular variables and functions. This was one of motivations for this work.

Finally, it is worth pointing out that there is no sub-typing in our system. That is, in the rules for application, the formal parameter and the actual argument must have exactly the same type τ 2 . In particular, all latent effects and ghost statuses in function types must be the same. For instance, a function expecting an argument of type int ⊥ =⇒ int cannot be applied to an argument of type int =⇒ int.

Type System of MiniML. Similarly to operational semantics, if we drop all ghost statuses (or, equivalently, if we consider them marked as ⊥) and get rid of typing rule (T-Ghost), we get a standard typing system with effects for MiniML with simple types. For clarity, we add a subscript m when we write typing judgements for MiniML terms: Γ • Σ m t : τ • .

Type Soundness

The type system of GhostML enjoys the standard soundness property. Any welltyped program either diverges or evaluates to a value. This property is well established in the literature for ML with references [START_REF] Wright | A syntactic approach to type soundness[END_REF][START_REF] Pierce | Types and Programming Languages[END_REF], and we can easily adapt the proof in our case. Due to lack of space, we only give the main statements.

As usual, we decompose type soundness into preservation and progress lemmas. First, we define well-typedness of a store with respect to a store typing. Definition 1 A store µ is well-typed with respect to a store typing Σ, written Σ µ, if dom(µ) ⊆ dom(Σ) and µ(r β ) has type Σ(r β ) for every r β ∈ dom(µ).

To prove preservation, we need the following substitution lemma:

Lemma 1 (Substitution Lemma) Let [x β 0 → τ 0 ]Γ•Σ t : τ •β 1 • and Γ•Σ v : τ 0 •β 2 • ⊥ be two derivable judgements such that + (τ ) ∨ = and β 0 = ⊥ implies β 2 = ⊥. Then, Γ • Σ t[x β 0 ← v] : τ • β 3 • is derivable with i) β 0 = ⊥ ⇒ β 1 ∨ β 2 ≥ β 3 ii) β 0 = ⇒ β 1 ≥ β 3
Proof By induction on the derivation of the statement

[x β 0 → τ 0 ]Γ • Σ t : τ • β 1 • .
The statement is almost a standard version of substitution lemma for variables. The only difference is the conditions we impose on ghost statuses in hypotheses and conclusion. The intuition is that we use this lemma to prove preservation theorem in the cases for let-expression let x β = v in t, or for application (t v). In both cases, by assumption, the corresponding redex will be a well-typed, so we will know that the side condition (1) holds for the union of effects and ghost statuses of t and v. However, we do not have this information explicitly in the lemma, so we need to strengthen its statement. We detail the proof for some interesting cases.

Case (T-Var): t = z β with ([x β 0 → τ 0 ]Γ)(z β ) = τ 0 .
There are two subcases to consider, depending on whether z β is equal x β 0 or not. If z β = x β 0 , then β 1 = β 3 , so the result follows, whatever β 0 is.

If β = x β 0 , then t[x β 0 ← v] = v with β 0 = β 1 and β 2 = β 3 . So, if β 0 = ⊥, we have β 1 ∨ β 2 = β 2 ≥ β 2 = β 3 ; if β 0 = , then = β 1 ≥ β 3 which holds for any β 3 . Case (T-Assign): t = r β 1 := v . The typing of t is Γ • Σ v : κ • β • ⊥ Σ(r β 1 ) = κ β 1 ≥ β Γ • Σ r β 1 := v : unit • β 1 • ¬β 1 (T-Assign)
where Γ = Γ , x β 0 : τ 0 . Sub-Case β 0 = : by induction hypothesis on the typing subderivation for v , we get Γ

• Σ v [x β 0 ← v] : κ • β 3 • ⊥ with β ≥ β 3 . Since β 1 ≥ β by hypothesis, we have by transitivity β 1 ≥ β 3 . Thus the typing judgement Γ • Σ (r β 1 := v )[x β 0 ← v] : unit • β 1 • ¬β 1 is derivable. Γ • Σ v [x β 0 ← v] : bool • β 30 • ⊥ with β 10 ≥ β 30 Γ • Σ t 1 [x β 0 ← v] : τ • β 31 • 1 with β 11 ≥ β 31 Γ • Σ t 2 [x β 0 ← v] : τ • β 32 • 2 with β 12 ≥ β 32
Thus, the typing judgement

Γ • Σ (if v then t 1 else t 2 )[x β 0 ← v] : τ • β 30 ∨ β 31 ∨ β 32 • 1 ∨ 2 is derivable with β 1 ≥ β 3 = β 30 ∨ β 31 ∨ β 32 .
Sub-Case β 0 = ⊥: if + ∨ 1 ∨ 2 = , then we may assume that β 2 = ⊥ and the subcase is proved in the same way; if + ∨ 1 ∨ 2 = ⊥, then by induction hypotheses on the typing subderivations, we obtain

Γ • Σ v [x β 0 ← v] : bool • β 30 • ⊥ with β 10 ∨ β 2 ≥ β 30 Γ • Σ t 1 [x β 0 ← v] : τ • β 31 • 1 with β 11 ∨ β 2 ≥ β 31 Γ • Σ t 2 [x β 0 ← v] : τ • β 32 • 2 with β 12 ∨ β 2 ≥ β 32
Thus, the typing judgement

Γ • Σ (if v then t 1 else t 2 )[x β 0 ← v] : τ • β 30 ∨ β 31 ∨ β 32 • 1 ∨ 2 is derivable with β 1 ∨ β 2 ≥ β 3 = β 30 ∨ β 31 ∨ β 32 .
The other cases are proved similarly (with standard auxiliary weakening and permutation lemmas in the cases for λ-abstractions and let-in expressions).

Lemma 2 (Preservation)

If Γ • Σ t : τ • β • and Σ µ, then µ • t → µ • t implies that Γ • Σ t : τ • β • and Σ µ , where β ≥ β and ≥ .
Proof By induction on the derivation of Γ • Σ t : τ • β • , using lemmas above. The only difference with respect to the standard statement is that ghost statuses and effect indicators can decrease during evaluation. At each step of the induction, we assume that the desired result holds for all subderivations and proceed by case analysis on the last rule used in the derivation. The four cases where t is a value cannot happen.

Case (T-If): t = if v then t 1 else t 2 with typing judgement Γ • Σ v : bool • β 0 • ⊥ Γ • Σ t 1 : τ • β 1 • 1 Γ • Σ t 2 : τ • β 2 • 2 Γ • Σ if v then t 1 else t 2 : τ • β 0 ∨ β 1 ∨ β 2 • 1 ∨ 2
There are two rules by which µ • t → µ • t can be derived: (E-If-True) and

(E-If-False).

Subcase

(E-If-True): µ • t → µ • t 1 .
As can be seen in the typing subderivation of t 1 above, the desired property holds, since

β 0 ∨ β 1 ∨ β 2 ≥ β 1 and 1 ∨ 2 ≥ 1 .
Subcase (E-If-False): µ • t → µ • t 2 . Identical to the previous subcase.

Case (T-Let ⊥ ): t = let x ⊥ = t 2 in t 1 . The typing judgement is [x ⊥ → τ 2 ]Γ • Σ t 1 : τ 1 • β 1 • 1 Γ • Σ t 2 : τ 2 • β 2 • 2 Γ • Σ let x ⊥ = t 2 in t 1 : τ 1 • β 1 ∨ β 2 • 1 ∨ 2
There are two rules by which µ • t → µ • t can be derived: (E-Context-Let) and

(E-Let).

Subcase (E-Let):

t 2 = v 2 and µ•let x ⊥ = v 2 in t 1 → µ•t 1 [x ⊥ ← v 2 ]. By substitution lemma 1, we have Γ • Σ t 1 [x ⊥ ← v 2 ] : τ 1 • β 3 • 1 where β 1 ∨ β 2 ≥ β 3 . Subcase (E-Context-Let): µ • let x ⊥ = t 2 in t 1 → µ • let x ⊥ = t 2 in t 1 with subderivation µ • t 2 → µ • t 2 . The typing judgement for t is [x ⊥ → τ 2 ]Γ • Σ t 1 : τ 1 • β 1 • 1 Γ • Σ t 2 : τ 2 • β 2 • 2 Γ • Σ let x ⊥ = t 2 in t 1 : τ 1 • β 1 ∨ β 2 • 1 ∨ 2 By induction hypothesis on Γ • Σ t 2 : τ 2 • β 2 • 2 we have Γ • Σ t 2 : τ 2 • β 2 • 2 with 2 ≥ 2 β 2 ≥ β 2 . So we can derive [x ⊥ → τ 2 ]Γ • Σ t 1 : τ 1 • β 1 • 1 Γ • Σ t 2 : τ 2 • β 2 • 2 Γ • Σ let x ⊥ = t 2 in t 1 : τ 1 • β 1 ∨ β 2 • 1 ∨ 2 with ( 1 ∨ 2 ) ≥ ( 1 ∨ 2 ) and (β 1 ∨ β 2 ) ≥ (β 1 ∨ β 2 ).
Case (T-Let ): t = let x = t 2 in t 1 . There are two rules by which µ • t → µ • t can be derived: (E-Let) and (E-Context-Let).

Subcase (E-Let):

t 2 = v 2 and µ • let x = v 2 in t 1 → µ • t 1 [x ← v 2 ]
The result follows from the substitution lemma 1.

Subcase

(E-Context-Let): µ • let x = t 2 in t 1 → µ • let x = t 2 in t 1 with subderivation µ • t 2 → µ • t 2 . The typing judgement for t is [x → τ 2 ]Γ • Σ t 1 : τ 1 • β 1 • 1 Γ • Σ t 2 : τ 2 • β 2 • ⊥ Γ • Σ let x = t 2 in t 1 : τ 1 • β 1 • 1 By induction hypothesis on Γ • Σ t 2 : τ 2 • β 2 • ⊥ we have Γ • Σ t 2 : τ 2 • β 2 • ⊥ with β 2 ≥ β 2 . So we can derive [x → τ 2 ]Γ • Σ t 1 : τ 1 • β 1 • 1 Γ • Σ t 2 : τ 2 • β 2 • ⊥ Γ • Σ let x = t 2 in t 1 : τ 1 • β 1 • 1 Case (T-App ⊥ ): t = t 1 v 2 with Γ • Σ t 1 : τ ⊥ 2 1 =⇒ τ 1 • β 1 • 2 . Similar to the case (T-Let ⊥ ). Case (T-App ): t = t 1 v 2 with Γ • Σ t 1 : τ 2 1 =⇒ τ 1 • β 1 • 2 . Similar to the case (T-Let ). Case (T-Deref): t = !r β with µ • !r β → µ • µ(r β ).
We have the following typing for t:

Σ(r β ) = κ Γ • Σ !r β : κ • β • ⊥ (T-Deref)
By hypothesis, Σ µ, so µ(r β ) has type κ. Moreover, µ(r β ) is necessarily a constant. Therefore we can conclude by deriving the typing judgement for µ(r β ):

Typeof(µ(r β )) = κ Γ • Σ µ(r β ) : κ • ⊥ • ⊥ (T-Const) Case (T-Assign): t = r β := v. The typing rule for t is Γ • Σ v : κ • β • ⊥ Σ(r β ) = κ β ≥ β Γ • Σ r β := v : unit • β • ¬β
The only rule that allows us to derive µ

• t → µ • t is (E-Assign). That is v is necessarily a constant and the derivation is µ • r β := c → µ[r β → c] • (). It remains then to check that Σ µ[r β → c],
which is true, since we have µ\{r β } = µ \{r β } and c = µ (r β ) has type κ = Σ(r β ).

Case (T-Ghost): t = ghost t 1 with Γ • Σ t 1 : τ • β • ⊥.
The result follows immediately.

Lemma 3 (Progress

) If ∅ • Σ t : τ • β • , then
• Σ t : τ • β • ⊥ and Σ µ, then µ • t → µ • t implies µ ⊥ = µ ⊥ .
Proof By induction on the derivation of µ

• t → µ • t . Case (E-Assign): t = r β := c with µ • r β := c → µ[r β → c] • ().
By hypothesis, = ⊥, so in the typing of t, β = :

Γ • Σ v : κ • β • ⊥ Σ(r β ) = κ β ≥ β Γ • Σ (r β := v) : unit • β • ¬β
that is r β is necessarily a ghost reference, so the regular part of the store remains the same.

Case (E-Context-App): µ • t 1 v → µ • t 1 v.
As t is well-typed by hypothesis, t 1 is well-typed too with the typing

Γ • Σ t 1 : τ β 2 =⇒ τ 2 • β • 1
for some β , β that depend on typing rule for t (either

(T-App ⊥ ) or (T-App )).
In both cases, by hypothesis, we have ⊥ = 1 ∨ 2 . As 1 = ⊥, we can apply the induction hypothesis on the sub-derivation µ

• t 1 → µ • t 1 , which gives the desired result µ ⊥ = µ ⊥ Case (E-Context-Let).
Identical to the previous case.

Other cases are trivial since the store is not modified by reduction.

Lemma 5 (Program Termination)

If ∅ • Σ t : τ • β • ⊥, Σ µ,
then evaluation of t in store µ terminates, that is, there is a value v and a store µ such that µ

• t → µ • v.
Proof Let us assume first that the reduction of t does not involve any call to a recursive function. Since the set of global references is finite and each global reference r i stores a value of a primitive type κ i (whatever its ghost status), the program t can be translated into a simply-typed λ-term, using the state monad

M τ κ 1 × • • • × κ n → τ × κ 1 × • • • × κ n .
The result follows by normalization of simply-typed λ-calculus. Now, let us assume we have an infinite reduction from t involving calls to recursive functions. Since t has effect ⊥, it only calls recursive functions for which the oracle (presumed to be sound) says they terminate. Thus we can replace any finite subreduction corresponding to a recursive function call by (λx.x) v where v is the result value. We still have an infinite reduction, which contradicts the first part of the proof.

A consequence of the previous lemmas and the side condition (1) is that ghost code does not modify the regular store and is terminating.

From GhostML to MiniML

This section describes an erasure operation that turns a GhostML term into a Min-iML term. The goal is to show that ghost code can be erased from a regular program without observable difference in the program outcome.

The erasure is written either E β (.), when parameterized by some ghost status β, and simply E(.) otherwise. First, we define erasure on types and terms. The main idea is to preserve the structure of regular terms and types, and to replace any ghost code by a value of type unit.

Definition 2 (τ -erasure) Let τ be some GhostML type. The erasure E β (τ ) of type τ with respect to β is defined by induction on the structure of τ as follows:

E (τ ) unit E ⊥ (τ β 2 2 =⇒ τ 1 ) E β 2 (τ 2 ) =⇒ E ⊥ (τ 1 ) E ⊥ (κ) κ
In other words, the structure of regular types is preserved and all ghost types are turned into type unit. Now we can define erasure on terms.

Definition 3 (t-Erasure)

Let t be such that Γ • Σ t : τ • β • holds. The erasure E β (t) is defined by induction on the structure of t as follows:

E (t) () E ⊥ (c) c E ⊥ (x ⊥ ) x E ⊥ (λx β : τ. t 1 ) λx : E β (τ ). E ⊥ (t 1 ) E ⊥ (rec f ⊥ : τ β 2 2 =⇒ τ 1 . t 1 ) rec f : E ⊥ (τ β 2 2 =⇒ τ 1 ). E ⊥ (t 1 ) E ⊥ (r ⊥ := v) r := E ⊥ (v) E ⊥ (!r ⊥ ) !r E ⊥ (if v then t 1 else t 2 ) if E ⊥ (v) then E ⊥ (t 1 ) else E ⊥ (t 2 ) E ⊥ (t 1 v) E ⊥ (t 1 ) E β (v)
where t 1 has type τ 2

β 1 =⇒ τ 1 E ⊥ (let x β = t 1 in t 2 ) let x = E β (t 1 ) in E ⊥ (t 2 )
Note that ghosts variables and ghost references do not occur anymore in E ⊥ (t). Note also that a regular function (recursive or not) with a ghost parameter remains a function, but with an argument of type unit. Similarly, a let-expression that binds a ghost variable inside a regular code remains a let, but now binds a variable to (). More generally, E ⊥ (t) is a value if and only if t is a value. Leaving unit values and arguments in the outcome of erasure may seem unnecessary. However, because of latent effects, full erasure of ghost code is not possible. Consider for instance the function λx ⊥ : int. λy : int. r ⊥ := x where r is a regular reference. Then a partial application of this function to a single argument should not trigger the modification of r. Our solution is to keep a second argument y of type unit. These reductions facilitate the proofs of forthcoming theorems. Notice that the program after erasure is semantically equivalent to the original one, with only extra administrative reduction steps (a term coined by Plotkin [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF]) that do not impact the program complexity and can be eliminated at compile time.

Well-typedness Preservation

We prove that erasure preserves well-typedness of terms. To do so, we first define the erasure of a typing context and of a store typing by a straightforward induction on their size: Definition 4 (Γ-erasure and Σ-erasure)

E(∅) ∅ E(∅) ∅ E(Γ, x : τ ) E(Γ), x : unit E(Σ, r : κ) E(Σ) E(Γ, x ⊥ : τ ) E(Γ), x : E ⊥ (τ ) E(Σ, r ⊥ : κ) E(Σ), r : κ With these definitions, we have immediately that E([x → τ ]Γ) = [x → unit]E(Γ) and E([x ⊥ → τ ]Γ) = [x → E ⊥ (τ )]E(Γ)
. Now we can prove well-typedness preservation under erasure:

Theorem 1 (Well-typedness Preservation) If Γ • Σ t : τ • ⊥ • holds, then E(Γ) • E(Σ) m E ⊥ (t) : E ⊥ (τ ) • holds.
Proof By induction on the typing derivation, with case analysis on the last applied rule.

Case (T-λ): [x β → τ ]Γ • Σ t 1 : τ 1 • ⊥ • Γ • Σ (λx β : τ. t 1 ) : τ β =⇒ τ 1 • ⊥ • ⊥ By induction hypothesis, we have [x → E β (τ )]E(Γ)•E(Σ) m E ⊥ (t 1 ) : E ⊥ (τ 1 )• . There- fore, we conclude that E(Γ) • E(Σ) m λx : E β (τ ). E ⊥ (t) : E β (τ ) =⇒ E ⊥ (τ 1 ) • ⊥. Case (T-App ⊥ ): Γ • Σ t : τ ⊥ 2 1 =⇒ τ 1 • β 1 • 2 Γ • Σ v : τ 2 • β 2 • ⊥ Γ • Σ (t v) : τ 1 • β 1 ∨ β 2 • 1 ∨ 2 By hypothesis β 1 ∨ β 2 = ⊥.
By induction hypotheses on the rule premises,

E(Γ) • E(Σ) m E ⊥ (t) : E ⊥ (τ 2 ) 1 =⇒ E ⊥ (τ 1 ) • 2 E(Γ) • E(Σ) m E ⊥ (v) : E ⊥ (τ 2 ) • ⊥. Thus, E(Γ) • E(Σ) m E ⊥ (t) E ⊥ (v) : E ⊥ (τ 1 ) • 1 ∨ 2 . Case (T-App ): Γ • Σ t : τ 2 1 =⇒ τ 1 • β 1 • 2 Γ • Σ v : τ 2 • β 2 • ⊥ Γ • Σ (t v) : τ 1 • β 1 • 1 ∨ 2 By hypothesis β 1 = ⊥. Thus, E ⊥ (t v) = E ⊥ (t) (). By induction hypothesis, E(Γ) • E(Σ) m E ⊥ (t) : unit 1 =⇒ E ⊥ (τ 1 ) • 2 As E(Γ) • E(Σ) m () : unit • ⊥, we conclude that E(Γ) • E(Σ) m E ⊥ (t) () : E ⊥ (τ 1 ) • 1 ∨ 2 . Case (T-Assign): Γ • Σ v : κ • β • ⊥ Σ(r β ) = κ β ≥ β Γ • Σ r β := v : unit • β • ¬β
By hypothesis β = ⊥, and by premise side condition β ≥ β , so β = ⊥ as well. By induction hypothesis on the rule premise, we obtain

E(Γ) • E(Σ) m E ⊥ (v) : κ • ⊥. Also, Σ(r ⊥ ) = κ, so (E(Σ))(r) = κ. Therefore we conclude with E(Γ) • E(Σ) m E ⊥ (v) : κ • ⊥ (E(Σ))(r) = κ E(Γ) • E(Σ) m r := E ⊥ (v) : unit •
Other cases are easily proved in a similar way.

Correctness of Erasure

Finally, we prove correctness of erasure, that is, evaluation is preserved by erasure. To turn this into a formal statement, we first define the erasure of a store µ by a straightforward induction on the store size:

Definition 5 (µ-erasure) E(∅) ∅ E(µ {r → c}) E(µ) E(µ {r ⊥ → c}) E(µ) {r → c}
Notice that E(µ) removes ghost annotations, and thus is not the same that µ ⊥ . The correctness of erasure means that, for any evaluation µ

• t → µ • v in GhostML, we have E(µ) • E ⊥ (t) → m E(µ ) • E ⊥ (v)
in MiniML and that, for any diverging evaluation

µ • t → ∞ in GhostML, we have E(µ) • E ⊥ (t) → m ∞ in MiniML.
We prove these two statements using a bisimulation argument. First, we need the substitution lemma below, which states that substitution and erasure commute.

Lemma 6 (Substitution Under Erasure) Let t be a GhostML term and v a GhostML value such that

[x β → τ ]Γ • Σ t : τ 0 • ⊥ • and Γ • Σ v : τ • β • ⊥, with β ≥ β , hold.
Then the following holds:

E ⊥ (t)[x ← E β (v)] = E ⊥ (t[x β ← v]).
Proof Straightforward induction on the structure of t.

Note that if Σ µ then E(Σ) m E(µ). To prove erasure correctness for terminating programs, we use the following forward simulation argument:

Lemma 7 (Forward Simulation of GhostML) If ∅ • Σ t : τ • ⊥ •
and, for some store µ such that Σ µ, we have µ • t → µ • t , then the following holds in MiniML:

E(µ) • E ⊥ (t) → 0|1 m E(µ ) • E ⊥ (t ).
Proof By induction on the derivation →.

Case (E-App-λ): (λx β : τ 2 . t) v → t[x β ← v]. If β = , then Γ • Σ λx : τ 2 . t : τ 2 1 =⇒ τ 1 • ⊥ • ⊥ Γ • Σ v : τ 2 • β 1 • ⊥ Γ • Σ (λx : τ 2 . t v) : τ 1 • ⊥ • 1
Therefore, by substitution under erasure (Lemma 6), we get

E ⊥ ((λx : τ 2 . t) v) = (λx : unit. E ⊥ (t)) ()) → m E ⊥ (t)[x ← ()] = E ⊥ (t[x ← v]). If β = ⊥, then we have Γ • Σ λx ⊥ : τ 2 . t : τ ⊥ 2 1 =⇒ τ 1 • ⊥ • ⊥ Γ • Σ v : τ 2 • ⊥ • ⊥ Γ • Σ (λx ⊥ : τ 2 . t v) : τ 1 • ⊥ • 1
Again, by substitution under erasure (Lemma 6), we get

E ⊥ ((λx ⊥ : τ 2 . t) v) → m E ⊥ (t)[x ← E ⊥ (v)] = E ⊥ (t[x ⊥ ← v]).
Therefore, by forward simulation in GhostML (Lemma 7), we have

E(µ) • E ⊥ (t) → 0 m E(µ) • E ⊥ (let x = v in t 1 ) → m E(µ) • E ⊥ (t 1 )[x ← ()].
Finally, by store preservation (Lemma 4), µ ⊥ = µ ⊥ . Therefore, E(µ) = E(µ ), which allows us to conclude.

Case 2: t is let x ⊥ = t 2 in t 1 . We have by hypothesis that t 1 is regular code. Then we also have that t 2 is regular too. If t 2 is a value, the result follows immediately. If t 2 is not a value, then the result follows from the results of GhostML soundness (safety and anti-monotony of statuses), using the induction hypothesis on t 2 , since t-erasure preserves the structure of regular terms.

Other cases are proved in a similar way.

Finally, we establish non-termination preservation:

Theorem 3 (Non-termination Preservation) If judgement ∅ • Σ t : τ • ⊥ • holds and µ • t → ∞, for some store µ such that Σ µ, then E ⊥ (t) also diverges, that is, E(µ) • E ⊥ (t) → m ∞.
Proof By co-induction, it suffices to prove that there exist t and µ such that the typing judgement ∅ • Σ t : τ • ⊥ • and Σ µ , and

E(µ) • E ⊥ (t) → 1 m E(µ ) • E ⊥ (t ) ∧ µ • t → ∞.
Observe that, since t diverges, t is not a value. Thus E ⊥ (t) is not a value either. By well-typedness preservation (Theorem 1), E ⊥ (t) is well-typed, with

∅ • E(Σ) m E ⊥ (t) : E ⊥ (τ ) • .
We have E(Σ) m E(µ), since Σ µ. Therefore, by progress in MiniML, there exist some term q and some store ν such that E(µ) • E ⊥ (t) → m ν • q. By simulation (Lemma 8), µ • t → ≥1 µ • t with q = E ⊥ (t ) and ν = E(µ ). The reduction being deterministic, t diverges and we have the following reductions:

µ • t → ≥1 µ • t → ∞ ⇓ ⇓ E(µ) • E ⊥ (t) → 1 m ν • q
By preservation (Lemma 2), Γ • Σ t : τ • ⊥ • , with ≥ , and Σ µ . Now, by co-induction hypothesis, ν • q → m ∞ and thus E(µ) • E ⊥ (t) → m ∞.

Implementation

Our method to handle ghost code is implemented in the verification tool Why32 . With respect to GhostML, the language and the type system of Why3 have the following extensions:

Type Polymorphism. The type system of Why3 is first-order and features ML-style type polymorphism. Our approach to associate ghost status with variables and expressions, and not with types, makes this extension straightforward.

Local References. Another obvious extension of GhostML is the support of nonglobal references. As long as such a reference cannot be an alias for another one, the needed alterations to the type system of GhostML are minimal. In a system where aliases are admitted, the type system and, possibly, the verification condition generator must be adapted to detect modifications made by a ghost code in locations accessible from regular code. In Why3, aliases are tracked statically [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF], and thus non-interference is ensured purely by type checking.

Structures with Ghost Fields. Why3 supports algebraic data types (in particular, records), whose fields may be regular or ghost. Pattern matching on such structures requires certain precautions. Any variable bound in the ghost part of a pattern must be ghost. Moreover, pattern matching over a ghost expression that has at least two branches must make the whole expression ghost, whatever the right-hand sides of the branches are, just as in the case of a conditional over a ghost Boolean expression. That said, ghost code can use the same data types as regular code. A ghost variable may be a record with regular, mutable fields, which can be accessed and modified in ghost code. Similarly, Why3 has a unique type of arrays and admits both regular and ghost arrays.

Exceptions. Adding exceptions is rather straightforward, since in Why3 exceptions are introduced only at the top level. Indeed, it suffices to add a new effect indicator, that is the set of exceptions possibly raised by a program expression. We can use the same exceptions in ghost and regular code, provided that the ghost status of an expression that raises an exception is propagated upwards until the exception is caught.

Provable Termination. As in GhostML, Why3 allows the use of recursive functions in ghost code. Loops can be used in ghost code as well. The system requires that such constructs are supplied with a "variant" clause, so that verification conditions for termination are generated.

Example. Let us illustrate the use of ghost code in Why3 on a simple example. Fig. 5 contains an implementation of a mutable queue data type, in Baker's style. A queue is a pair of two immutable singly-linked lists, which serve to amortize push and pop operations. Our implementation additionally stores the pure logical view of the queue as a list, in the third, ghost field of the record. Notice that we use the same list type both for regular and ghost data. We illustrate propagation in function push (lines 27-30), where a local variable v is used to hold some intermediate value, to be stored later in the ghost field of the structure. Despite the fact that variable v is not declared ghost, and the fact that function append is a regular function, Why3 infers that v is ghost. Indeed, the ghost value q.view contaminates the result of append. It would therefore generate an error if we tried to store v in a non-ghost field of an existing regular structure. Since the expression append q.view (Cons x Nil) is ghost, it must not diverge. Thus Why3 requires function append to be terminating. This is ensured by the variant clause on line 8. In function pop (lines 34-52), the regular function rev_append is used both in regular code (line 42) and ghost code (line 39).

The online gallery of verified Why3 programs contains several other examples of use of ghost code3 , in particular, ghost function parameters and ghost functions to supply automatic induction proofs (also known as lemma functions).

Related Work

The idea to use ghost code in a program to ease specification exists since the early days (late sixties) of deductive program verification, when so-called auxiliary variables became a useful technique in the context of concurrent programming. According to Jones [START_REF] Jones | Reflections on the Work of C[END_REF] and Reynolds [START_REF] Reynolds | The craft of programming[END_REF], the notion of auxiliary variable was first introduced by Lucas in 1968 [START_REF] Lucas | Two constructive realizations of the block concept and their equivalence[END_REF]. Since then, numerous authors have adapted this technique in various domains.

It is worth noting that some authors, in particular, Reynolds [START_REF] Reynolds | The craft of programming[END_REF] and Kleymann [START_REF] Kleymann | Hoare logic and auxiliary variables[END_REF], make a clear distinction between non-operational variables used in program annotations and specification-purpose variables that can appear in the program itself. The latter notion has gradually evolved into the wider idea that ghost code can be arbitrary code, provided it does not interfere with regular code. For example, Zhang et al. [START_REF] Zhang | A structural approach to prophecy variables[END_REF] discuss the use of auxiliary code in the context of concurrent program verification. They present a simple WHILE language with parallelism and auxiliary code, and prove that the latter does not interfere with the rest of the program. In their case, non-interference is ensured by the stratified syntax of the language. For instance, loops can contain auxiliary code, but auxiliary code cannot contain loops, which ensures termination. They also define auxiliary code erasure and prove that a program with ghost code has no less behaviors than its regular part. Schmaltz [START_REF] Schmaltz | Towards the Pervasive Formal Verification of Multi-Core Operating Systems and Hypervisors Implemented in C[END_REF] proposes a rigorous description of ghost code for a large fragment of C with parallelism, in the context of the VCC verification tool [START_REF] Cohen | VCC: A practical system for verifying concurrent C[END_REF]. VCC includes ghost data types, ghost fields in regular structures, ghost parameters in regular functions, and ghost variables. In particular, ghost code is used to manipulate ownership information. A notable difference w.r.t. our work is that VCC does not perform any kind of inference of ghost code. Another difference is that VCC assumes that ghost code terminates, and the presence of constructions such as ghost(goto l) makes it difficult to reason about ghost code termination.

Another example of a modern deductive verification tool implementing ghost code is the program verifier Dafny [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF]. In Dafny, "the concept of ghost versus non-ghost declarations is an integral part of the Dafny language: each function, method, variable, and parameter can be declared as either ghost or non-ghost." [START_REF] Leino | Co-induction simply: Automatic co-inductive proofs in a program verifier[END_REF]. In addition, a class can contain both ghost fields and regular fields. Dafny ensures termination of ghost code. Ghost code can update ghost fields, but is not allowed to allocate memory or update non-ghost fields. Consequently, ghost code cannot obtain full reuse of libraries that allocate and mutate classes or arrays. However, on the fragment of Dafny's language corresponding to GhostML, Dafny provides a semantics of ghost code similar to what is presented here.

The property of non-interference of ghost code is a special case of information flow non-interference [START_REF] Denning | Certification of programs for secure information flow[END_REF]. Indeed, one can see ghost code as high-security information and regular code as low-security information, and non-interference precisely means that high-security information does not leak into low-security computations. Information flow properties can be checked using a type system [START_REF] Pottier | Information flow inference for free[END_REF] and proofs in that domain typically involve a bisimulation technique (though not necessarily through an erasure operation). Notice that applying an information flow type system to solve our problem is not straightforward, since termination of ghost code is a crucial requirement. For instance, the type system described by Simonet and Pottier [START_REF] Pottier | Information flow inference for ML[END_REF] simply assumes termination of secret code. To the best of our knowledge, this connection between information flow and ghost code has not been made before, and mainstream deductive verification tools employ syntactical criteria of non-interference instead of type-based ones. In this paper, we develop such a type-based approach, specifically tailored for program verification.

Erasure of ghost code is similar to the mechanism of program extraction in the Coq proof assistant [START_REF] Paulin-Mohring | Extracting Fω's programs from proofs in the Calculus of Constructions[END_REF][START_REF] Paulin-Mohring | Extraction de programmes dans le Calcul des Constructions[END_REF]. Indeed, the purpose of such a mechanism is to remove from the program what is computationally irrelevant. For instance, in a proof of ∃x. P (x), that is a witness t and a proof of P (t), only t is kept in the extracted program. To do this, the Coq extraction is guided by sorts, namely Set for programs and Prop for proofs, and non-interference is ensured by Coq type-checking. Coq users must choose between Set and Prop beforehand. For instance, the type nat of natural numbers has sort Set and therefore natural numbers are never removed during extraction, even when they are only used for the purpose of specification and/or proof. In our approach, the same type of natural numbers can be used for both regular and ghost code and is kept only when relevant.

Conclusion and Perspectives

In this paper, we described an ML-like language with ghost code. Non-interference between ghost code and regular code is ensured using a type system with effects. We formally proved the soundness of this type system, that is, ghost code can be erased without observable difference. Our type system results in a highly expressive language, where the same data types and functions can be reused in both ghost and regular code.

We see two primary directions of future work on ghost code and Why3. First, ghost code, especially ghost fields, plays an important role in program refinement. Indeed, ghost fields that give sufficient information to specify a data type are naturally shared between the interface and the implementation of this data type. In this way, the glue invariant becomes nothing more than the data type invariant linking regular and ghost fields together. Our intention is to design and implement in Why3 a module system with refinement that makes extensive use of ghost code and data. Second, since ghost code does not have to be executable, it should be possible to use in ghost code various constructs which, up to now, may only appear in specifications, such as quantifiers, inductive predicates, non-deterministic choice, or infinitely parallel computations (cf. the aggregate forall statement in Dafny).

Fig. 1

 1 Fig. 1 Types and effects.

Fig. 2

 2 Fig. 2 Syntax of terms.

Fig. 3

 3 Fig. 3 Semantics.

11 = match l1 with 12 | Nil → l2 13 | 18 = match l1 with 19 | Nil → l2 20 |Fig. 5

 1112131819205 Fig. 5 Queue implementation in Why3.

  either t is a value or, for any store µ such that Σ µ, there exists a reduction step µ • t → µ • t .Proof Straightforward induction on the typing derivation of t. Let µ ⊥ denote the regular part of store µ, that is the restriction of µ to regular references. Then, If ∅

	Additionally, we have the following results for effectless programs.
	Lemma 4 (Store Preservation)

1 =⇒ τ 1 ) [f β 1 → τ 0 ]Γ • Σ (λx β : τ 2 . t 1 ) : τ 0 • β 0 • ⊥ β 1 ≥ β 0 1 ≥ 0 Γ • Σ (rec f β 1 : τ 0 . λx β : τ 2 . t 1 ) : τ 0 • β 1 • ⊥ (T-Rec) Γ • Σ v : bool • β 0 • ⊥ Γ • Σ t 1 : τ • β 1 • 1 Γ • Σ t 2 : τ • β 2 • 2 Γ • Σ (if v then t 1 else t 2 ) : τ • β 0 ∨ β 1 ∨ β 2 • 1 ∨ 2 (T-If) Γ • Σ t 1 : τ 1 • β 1 • 1 [x ⊥ → τ 1 ]Γ • Σ t 2 : τ 2 • β 2 • 2 Γ • Σ (let x ⊥ = t 1 in t 2 ) : τ 2 • β 1 ∨ β 2 • 1 ∨ 2 (T-Let ⊥ ) Γ • Σ t 1 : τ 1 • β 1 • ⊥ [x → τ 1 ]Γ • Σ t 2 : τ 2 • β 2 • 2 Γ • Σ (let x = t 1 in t 2 ) : τ 2 • β 2 • 2 (T-Let ) Γ • Σ t 1 : τ ⊥ 2 1 =⇒ τ 1 • β 1 • 2 Γ • Σ v : τ 2 • β 2 • ⊥ Γ • Σ (t 1 v) : τ 1 • β 1 ∨ β 2 • 1 ∨ 2 (T-App ⊥ ) Γ • Σ t 1 : τ 2 1 =⇒ τ 1 • β 1 • 2 Γ • Σ v : τ 2 • β 2 • ⊥ Γ • Σ (t 1 v) : τ 1 • β 1 • 1 ∨ 2

For the sake of readability, we slightly relax the constraints of the A-normal form and accept arbitrary terms in the reference assignment.

Sub-Case β 0 = ⊥, β 1 = : by induction hypothesis on the typing subderivation for v , we get Γ• Σ v [x β 0 ← v] : κ • β 3 • ⊥ with = β 1 ∨ β 2 ≥ β 3 .Thus the side condition ≥ β 3 is trivially verified and the typing judgement Γ • Σ (rβ 1 := v )[x β 0 ← v] : unit • β 1 • ¬β 1 is derivable.Sub-Case β 0 = ⊥, β 1 = ⊥: Since = , we can assume that β 2 = ⊥. Since β = ⊥ as well, the induction hypothesis on the typing subderivation of v givesΓ • Σ v [x β 0 ← v] : κ • β 3 • ⊥ where β 3 = ⊥ since ⊥ = β ∨ β 2 ≥ β 3 .Thus the side condition ⊥ ≥ β 3 is trivially verified and the judgement Γ • Σ (rβ 1 := v )[x β 0 ← v] : unit • β 1 • ¬β 1 is derivable. Case (T-If): t = if v then t 1 else t 2 . The typing of t is Γ • Σ v : bool • β 10 • ⊥ Γ • Σ t 1 : τ • β 11 • 1 Γ • Σ t 2 : τ • β 12 • 2 Γ • Σ if v then t 1 else t 2 : τ • β 10 ∨ β 11 ∨ β 12 • 1 ∨ 2where Γ = Γ , x β 0 : τ 0 .Sub-Case β 0 = : by induction hypotheses on the subderivations, we obtain the following typing judgements:

Why3 is freely available from http://why3.lri.fr/.

http://toccata.lri.fr/gallery/ghost.en.html

Acknowledgments. We are grateful to Sylvain Conchon, Rustan Leino, and François Pottier for comments and discussions regarding earlier versions of this paper.

This work is partly supported by the Bware (ANR-12-INSE-0010, http://bware.lri.fr/) project of the French national research agency (ANR). This is an extended version of a conference paper [1].

As t 2 is an effectless term, we have by store preservation (Lemma 4), µ ⊥ = µ ⊥ . Thus we have E(µ) = E(µ ). Therefore,

By induction hypothesis on sub-derivation µ • t 2 → µ • t 2 , we get

The result trivially holds when this reduction has 0 steps. Otherwise, we have

Other cases are proved in a similar way.

We are now able to prove the first part of the main theorem:

for some value v and some store µ

Proof By induction on the length of the evaluation µ

then the result trivially holds since t = v and µ = µ. Now, assume that µ • t → 1 µ • t → n µ • v for some intermediate store µ . By preservation (Lemma 2), Γ•Σ t : τ •⊥• and Σ µ for some , such that ≥ . By induction hypothesis on t , we obtain E(µ

Now we prove the second part of the erasure correctness (non-termination preservation), using the following simulation argument. Lemma 8 (Forward Simulation of MiniML) If ∅ • Σ t : τ • ⊥ • holds, then, for any store µ such that Σ µ, if E(µ) • E ⊥ (t) → m ν • q for some term q and some store ν, then µ • t → ≥1 µ • t where E ⊥ (t ) = q and E(µ ) = ν.

Proof By induction on the term t.

Case 1: t is let x = t 2 in t 1 . If t 2 is not a value, then by the GhostML progress property (Lemma 3), it can be reduced. By hypothesis, t is well-typed, with a typing judgement for t 2 being ∅ • Σ t 2 : τ • β • ⊥. By program termination (Lemma 5), we have µ • t 2 → µ • v for some v and µ . Consequently,


Stéphane Durand
email: stephane.durand@inria.fr

Bruno Gaujal
email: bruno.gaujal@inria.fr

Average complexity of the Best Response Algorithm in Potential Games *

Keywords: Potential Games, Best Response, Average Complexity

Introduction

Potential games have been introduced in [START_REF] Rosenthal | A class of games possessing pure-strategy nash equilibria[END_REF] and have proven very useful, especially in the context of routing games, first mentioned in [START_REF] Beckman | Studies in the Economics of Transportation[END_REF] and exhaustively studied ever since, in the transportation as well as computer science litterature, see for example [START_REF] Gallager | A minimum delay routing algorithm using distributed computation[END_REF][START_REF] Orda | Competitive routing in multeuser communication networks[END_REF][START_REF] Wardrop | Some theoretical aspects of road traffic research. part ii[END_REF] and for distributed optimization (see for example [START_REF] Roughgarden | Selfish Routing and the Price of Anarchy[END_REF]).

The Best Response Algorithm (BRA) is probably the most popular algorithm that converges to a pure Nash equilibrium (NE) in potential games [START_REF] Monderer | Potential games. Games and economic behavior[END_REF]. However, its efficiency (speed of convergence) has attracted surprisingly little attention.

In this paper, we analyze the performance of BRA used over a potential game with N players, each with A possible actions, and we provide answers to the following questions.

1. How many steps does the Best Response Algorithm take before it stops in a Nash Equilibrium ?

2. A related question is how many comparisons are done during the execution of BRA ?

In a nutshell, the answers to these questions are respectively, 1. less than log(N ) + e γ on average (γ is the Euler constant) ;

2. e γ AN on average.

These numbers say that BRA is a very efficient distributed algorithm to compute NE. Our analysis is based on two ingredients, one is the construction of an approximation of the behavior of BRA, where each state is examined at most once and the second is the use of a continuousstate space-discrete-time Markov chain to analyze the average complexity.

Best Response Algorithm and Potential games

We consider a game with a finite number N of players and a finite strategy space for each player, each of size A, and the corresponding utility functions. G def = G(N , A, u) will be a tuple consisting of -a finite set of players N = {1, . . . , N } ; -a finite set A k of actions (or pure strategies) for each player k ∈ N ; The set of actions profiles or states of the game is

A def = k A k ;
-the players' payoff functions u k : A → R. * Supported by ANR LabEx Persyval-Lab

We define the classical best response correspondence br k (x) as the set of all actions that maximizes the payoff for player k under profile x :

br k (x) def = argmax α∈A k u k (α; x -k ) .
(

A Nash equilibrium (NE) is a fixed point of the correspondence, i.e. a profile x * such that x * k ∈ br k (x * ) for every player k.

Iteratively playing a best response may not converge in general. We consider here the specific class of potential games for which convergence is ensured.

Définition 1 (Potential games)

A game is a potential game [START_REF] Monderer | Potential games. Games and economic behavior[END_REF] if it admits a function (called the potential) Φ : A → R such that for any player k and any unilateral deviation of k

from action profile x to x , u k (x) -u k (x ) = Φ(x) -Φ(x ).
We consider a general version of Best Response Algorithm (BRA) where the next player is selected according to a revision sequence (R t ) t∈N . We assume that this sequence of players is weakly fair : each players appears infinitely often in the sequence. The revision sequence can be deterministic (for example, Round-Robbin) or random (for example, the next player is chosen according to a probability distribution ρ (the revision law) : ∀k ∈ N , P(selected player = k) = ρ k ). In that case, we assume that the probability of choosing any player k is strictly positive (∀k ∈ N , ρ k > 0). This insures that the revision sequence is weakly fair almost surely.

Algorithm 1: Best Response Algorithm (BRA) Input : Game utilities (u i (•)), Initial state (x(0)), Infinite revision sequence R = (R t ) t∈N of players. foreach player k ∈ K do stop k := f alse repeat Pick next player k := R t+1 Select new action α k := br k (x(t)) stop k := 1 {α k =x k (t)} ; x k (t + 1) := α k ; until stop 1 ∧ stop 2 ∧ • • • ∧ stop N ;
A famous result first proved in [START_REF] Monderer | Potential games. Games and economic behavior[END_REF] states that for any potential game G, Algorithm 1 converges in finite time (a.s.) to a Nash Equilibrium of G.

Complexity

In this section, we analyse the time complexity of BRA. More precisely, we consider three measures (related to each other). The most important quantity is T BRA , the number of iterations (or the number of times that the function br was called) before BRA reaches a Nash equilibrium. A related measure is the total number of comparisons used (denoted C BRA ). One should expect that C BRA ≈ (A-1)T BRA . Finally, another interesting quantity is the number of different states visited by BRA. This is the same (up to one) as the number of moves (denoted M BRA ) taken by BRA before convergence to a NE. Of course, M BRA T BRA . The proofs of the propositions 1 and 2 are not provided due to lack of space. They are available in a research report [START_REF] Durand | Efficiency of the best response algorithm in potential games[END_REF].

In the worst case, for random weakly fair revision sequences R, T BRA is unbounded because the revision sequence R can be arbitrarily bad : one player might appear too few times to guarantee convergence in any bounded time. Indeed, the weak fairness assumption is too weak to prevent unbounded gaps between the turns of one player). Even when this is not the case, for example when R is a round-robin sequence, the time for convergence can still be very large, as shown in the following proposition.

Proposition 1 In the worst case, under round robin revisions, T

BRA = N A N -1 .
The worst case complexity does not say much about the typical behavior of BRA. In the following we will analyze its average complexity when the revision sequence is round-robin. Other revision sequences behave similarly (up to a multiplicative factor).

Randomization

In the following we will randomize over the potential game over which BRA is used. Since the behavior of BRA only depends on the potential function, we randomize directly over the potential Φ. The natural randomization is to consider all possible total orderings of the set {Φ(x), x ∈ A} (there are (A N )! of them) and pick one uniformly. This is equivalent to pick iid potentials in all states, uniformly distributed in [0, 1].

Markovian Analysis

We will be analysing the intersection-free approximation of the behavior of BRA (where no state is visited twice) whose behavior is asymptotically the same as BRA.

Let y be the potential of the current state x : (y def = Φ(x)). If k -1 players have already played best response without changing the profile, then the evolution at the next step of BRA is as follows. The k-th player computes its best response. This player has a def = A -1 new actions whose potential must be compared with the current potential (y). With probability y a none of the new actions beat the current choice. The state remains at y and it is the turn of the k + 1-st player to try its best response. With probability 1 -y a , one of the new actions is the best response. The current state moves to a new state with a larger potential and the number of players for which the new state is a best response is set back to 1. More precisely, with probability 1 -z a the potential moves from y to a value larger than z.

This says that the couple (Y (t), K(t)) is a Markov chain, where Y (t) is the potential at step t, in [0, 1] and K(t) is the current number of players whose best response did not change the current state (in {1, 2, . . . , N }). Its transitions are :

P (Y (t + 1), K(t + 1)) = (y, k + 1) (Y (t), K(t)) = (y, k) = y a ,
and, if z > y,

P (Y (t + 1), K(t + 1)) ∈ ([z, 1], 1) (Y (t), K(t)) = (y, k) = 1 -z a .
Now, let M (y, k) be the average number of moves of BRA before convergence when the current potential equals y and k players have played without changing their action, at potential y.

The quantity M (y, k) satisfies the forward heat equation of the Markov chain : Solving these equations leads to the following proposition.

M (y, k) = y a M (y, k + 1) +
= e γ (A -1)(N -1) + o(A).
The average number of steps is ET BRA = e γ (N -1) + o(1).

Numerical experiments

The following figures correspond to simulations on games, all with A = 30. The number of players N ranges from 0 to 250. These games have potentials chosen uniformly in [0, 1]. For each value of N , algorithm BRA is run 5000 times. the errorbars correspond to confidence interval at 95%. As one can see in Figure 1a the average number of moves for BRA with Round-Robin approaches log N + 1.09, while Theorem 2 predicts that it should be of the form log N + Cte, with Cte e γ ≈ 1.7. As predicted by Theorem 2, Figure 1b shows that the number of comparisons is e γ (A -1)N , with a very tight confidence interval. This provides numerical evidence that the variance is small (and the distribution is not spread).

1 y 1 y

 11 au a-1 (M (u, 1) + 1)du. Let us also consider the average number of comparisons made by BRA under the intersectionfree assumption. Let C(y, k) be the average number of comparisons starting in a state with potential y and k players have played without changing their action. The forward equation for C(y, k) is : C(y, k) = y a (C(y, k + 1) + a) + au a-1 (C(u, 1) + a)du, with the boundary conditions C(1, 1) = a(N -1) and C(y, N ) = 0.

  Average number of moves. The best fit function is log(N ) + 1Average number of steps before reaching the NE.The predicted value is (e γ -1)N .

FIG. 1 -

 1 FIG.1-Simulation results for Round-Robin BRA

Proposition 2

 2 The average number of moves in BRA before convergence can be bounded : EM BRA log(N ) + e γ + O(1/N ), and this bound is tight, up to an additive constant.The average number of comparisons made during an execution of BRA is asymptotycally EC BRA


Stéphane Durand

Bruno Gaujal

Average complexity of the Best Response Algorithm in Potential Games *

Introduction

The computation of Nash Equilibria (NE) in games has been investigated of many papers. The most general result is in [START_REF] Goldberg | The complexity of computing a nash equilibrium[END_REF] and says that the problem of computing NE is PPAD complete. Potential games have been introduced in [START_REF] Rosenthal | A class of games possessing pure-strategy nash equilibria[END_REF] and have proven very useful, especially in the context of routing games, first mentioned in [START_REF] Beckman | Studies in the Economics of Transportation[END_REF] and exhaustively studied ever since, in the transportation as well as computer science litterature, see for example [START_REF] Orda | Competitive routing in multeuser communication networks[END_REF]. For potential games, efficient polynomial time algorithms exist in symmetric cases (see [START_REF] Fabrikant | The complexity of pure nash equilibria[END_REF]). However, the same paper shows that the computation of NE for general potential games is PLS complete. The Best Response Algorithm (BRA) is probably the most popular algorithm that converges to a pure Nash equilibrium (NE) in potential games [START_REF] Monderer | Potential games. Games and economic behavior[END_REF]. However, its complexity has attracted surprisingly little attention.

In this paper, we analyze the performance of BRA over a potential game with N players, each with A possible actions. We show that on average, the Best Response Algorithm takes log(N)+e γ (γ is the Euler constant) effectives steps and makes e γ AN comparisons before finding a NE. These numbers say that BRA is very efficient on average to compute NE, even if this is a PLS complete problem. Our analysis is based on two ingredients, one is the construction of an approximation of the behavior of BRA, where each state is examined at most once and the second is the use of a continuous space discrete time Markov chain to analyze the average complexity.

Best Response Algorithm and Potential games

We consider a game with a finite number N of players and a finite strategy space for each player, each of size A, and the corresponding utility func- * . Supported by ANR LabEx Persyval-Lab tions. The game G def = G(N , A, u) will be a tuple consisting of -a finite set of players N = {1, . . . , N} ; -a finite set A k of actions (or pure strategies) for each player k ∈ N ; The set of action profiles or states of the game is

A def = k A k ;
-the players' payoff functions u k : A → R.

We define the classical best response correspondence br k (x) as the set of all actions that maximizes the payoff for player k under profile x :

br k (x) def = argmax α∈A k u k (α; x -k ) . (1)
A Nash equilibrium (NE) is a fixed point of the correspondence, i.e. a profile x * such that x * k ∈ br k (x * ) for every player k.

Definition 1 (Potential games)

A game is a potential game [START_REF] Monderer | Potential games. Games and economic behavior[END_REF] if it admits a function (called the potential) Φ : A → R such that for any player k and any unilateral deviation of k from action α to α ,

u k (α, x -k )-u k (α , x -k ) = Φ(α, x -k )-Φ(α , x -k ).
We consider a version of Best Response Algorithm (BRA) where the next player is selected according to a round robin pattern. Other patterns can also be considered using the same approach and can be shown to have a similar behavior.

foreach player k ∈ K do stop k := false repeat Pick next player k := R t+1 Select new action α k := br k (x(t)) stop k := 1 {α k =x k (t)} ; x k (t + 1) := α k ; until stop 1 ∧ stop 2 ∧ • • • ∧ stop N ;
A famous result first proved in [START_REF] Monderer | Potential games. Games and economic behavior[END_REF] states that for any potential game G, Algorithm 1 converges in finite time to a Nash Equilibrium of G.

Complexity

Let us consider three complexity measures (related to each other) : T BRA is the number of iterations (or the number of times that the function br was called) before BRA reaches a Nash equilibrium. The total number of comparisons is denoted C BRA . One should expect that C BRA ≈ (A -1)T BRA . Finally, the number of different states visited by BRA is denoted M BRA . Of course, M BRA T BRA . The proofs of Theorems 1 and 2 are not provided due to lack of space. They are available in a research report [START_REF] Durand | Efficiency of the best response algorithm in potential games[END_REF].

Theorem 1 In the worst case, under round robin revisions, T BRA = NA N-1 .

Randomization

In the following we will analyze the average complexity of BRA.

We randomize over all the potential games over which BRA is used. Since the behavior of BRA only depends on the potential function, we randomize directly over the potential Φ. The natural randomization is to consider all possible total orderings of the set {Φ(x), x ∈ A} (there are (A N )! of them) and pick one uniformly. This is equivalent to pick iid potentials in all states, uniformly distributed in [0, 1].

Markovian Analysis

We will be analyzing the intersection-free approximation of the behavior of BRA (where no state is visited twice) whose behavior is asymptotically the same as BRA. Let y be the potential of the current state x : (y def = Φ(x)). If k -1 players have already played best response without changing the state, then the evolution at the next step of BRA is as follows. The k-th player computes its best response. This player has a def = A -1 new actions whose potential must be compared with the current potential (y). With probability y a none of the new actions beat the current choice. The state remains at y and it is the turn of the k+1-st player to try its best response. With probability 1 -y a , one of the new actions is the best response. The current state moves to a new state with a larger potential and the number of players for which the new state is a best response is set back to 1. This says that the couple (Y t , K t ) is a Markov chain, where Y t is the potential at step t, in [0, 1] and K t is the current number of players whose best response did not change the current state (in {1, 2, . . . , N}). Its transitions are :

P (Y, K) t+1 = (y, k + 1) (Y, K) t = (y, k) = y a , and, if z > y, P (Y, K) t+1 ∈ ([z, 1], 1) (Y, K) t = (y, k) = 1 -z a .

Bibliographie

Algorithm 1 :

 1 Best Response Algorithm (BRA) Input : Game utilities (u i (•)), Initial state (x(0)), Infinite seq. of players R = (1, 2, . . . , N, 1, . . . ).

1 yTheorem 2

 12 Let C(y, k) be the average number of comparisons required to reach a NE, starting in a state with potential y where k players have played without changing their action. The forward equation for C(y, k) is :C(y, k) =y a (C(y, k + 1) + a) + au a-1 (C(u, 1) + a)du,with the boundary conditions C(1, 1) = a(N -1) and C(y, N) = 0. Solving these equations leads to the following proposition (quantities M BRA and T BRA are analyzed similarly). The average number of moves in BRA verifies EM BRA log(N) + e γ + O(1/N). The average number of comparisons verifies EC BRA e γ (A -1)N + o(AN) and the average number of steps verifies ET BRA e γ N + o(N).