Jérôme Vouillon
email: jerome.vouillon@pps.jussieu.fr

Order Theory for Big-Step Semantics

We show that tools from order theory, such as Kleene fixpoint theorem, can be used to define bigstep semantics that simultaneously account for both converging and diverging behaviors of programs. These semantics remain very concrete. In particular, values are defined syntactically: the semantics of a function abstraction is a function closure rather than some abstract continuous function.

Introduction

Many techniques are available to express formally the semantics of a calculus. Syntactic approaches are often favored, as they are very concrete and require little theory. They can be classified into two categories. Small-step semantics [START_REF] Plotkin | A structural approach to operational semantics[END_REF] are very expressive, accounting for both termination and non-termination. However, this precision can be a hinder when proving program transformations: the semantics of programs are execution traces, that needs to be transformed to validate program transformations. Big-step semantics [START_REF] Kahn | Natural semantics[END_REF] are more abstract: the semantics of a program is its final outcome. They do not account for nontermination, unless they are specified as both an inductive relation for terminating programs and a coinductive relation for non-terminating ones. Denotational approaches, on the other hand, are powerful but require a significant mathematical background: the semantics of a program is not a syntactic object, but belongs to an abstract mathematical domain; for instance, function abstractions are typically interpreted as continuous functions between domains. In the present paper, we attempt to find a middle ground: we experiment with basic denotational tools to define big step semantics that simultaneously account for finite and infinite program behaviors. This way, we can define semantics which are simple and very concrete, but also precise.

We present our technique on a kind of call-by-need calculus which would be complicated to tackle by other means (Section 2). We then discuss how to apply our framework for the semantics of other calculi (Section 3). This paper is based on a mechanised formalisation in Coq of (basic) order theory and of the call-by-need calculus (Section 4).

A Call-by-Need Calculus

As a running example, we consider a small calculus with first-class functions and pairs. We mean this calculus to be call-by-need. Our aim is to give a kind of big-step semantics to this calculus. This semantics accounts for both converging and diverging behaviors. We then illustrate how to reason on the semantics by proving a type soundness result.

Syntax

Terms T are given by the grammar below. This is the standard syntax of λ-calculus with pairs. t ::= x variable λx.t function abstraction t t function application (t, t) pair fst t first projection snd t second projection We write X for the countable set of variables x. Terms evaluate to values V , described by the following grammar.

v ::= (λx.t) ρ function closure (v, v) pair diverge divergence error error An environment ρ is a total map from variables X to values V . A variable x is unbound in an environment ρ when ρ(x) = error. The diverge and error values may occur nested inside other values: intuitively, values are computed lazily; then, when visiting a value, one may reach a position in the value where the computation diverges or fails. Laziness makes it possible to define infinite datastructures. Thus, for the moment, we consider that values v may be infinite trees (see just below for a formal definition). In other words, we interpret the grammar above in a coinductive way. Later on, we will take a different point of view, and will find it convenient to write v to denote just finite values and v to denote any value, including infinite ones.

Infinite tree. We write N * for the set of finite sequences of integers. The empty sequence is written ǫ, and w • w ′ denotes the concatenation of two sequences w and w ′ .

VAR ρ ⊢ x ; ρ(x) ABS ρ ⊢ λx.t ; (λx.t) ρ PAIR ρ ⊢ t 1 ; v 1 ρ ⊢ t 2 ; v 2 ρ ⊢ (t 1 , t 2 ) ; (v 1 , v 2 ) APP ρ ⊢ t ; (λx.t ′′ ) ρ ′ ρ ⊢ t ′ ; v ′ ρ ′ ; x → v ′ ⊢ t ′′ ; v ρ ⊢ t t ′ ; v APP-STRICT ρ ⊢ t ; diverge ρ ⊢ t t ′ ; diverge APP-ERROR ρ ⊢ t ; v v ≤ (λx.t ′′ ) ρ ′ ρ ⊢ t t ′ ; error FST ρ ⊢ t ; (v 1 , v 2 ) ρ ⊢ fst t ; v 1 FST-STRICT ρ ⊢ t ; diverge ρ ⊢ fst t ; diverge FST-ERROR ρ ⊢ t ; v v ≤ (v 1 , v 2 ) ρ ⊢ fst t ; error SND ρ ⊢ t ; (v 1 , v 2 ) ρ ⊢ snd t ; v 1 SND-STRICT ρ ⊢ t ; diverge ρ ⊢ snd t ; diverge SND-ERROR ρ ⊢ t ; v v ≤ (v 1 , v 2 ) ρ ⊢ snd t ; error Figure 1. Semantics.
We assume given a set Σ of labels together with an arity function Ar : Σ → N ∪ {∞}. A tree (T, V ) is a pair of a non-empty set of nodes T ⊆ N * and a labelling function V : T → Σ such that:

• if t • c ∈ T where c ∈ N, then t ∈ T and for all c ′ ∈ N , if c ′ < c then t • c ′ ∈ T ; • for all t ∈ T , Ar(V (t)) = d(t), where the degree of a node t ∈ T is d(t) = inf{c ∈ N | t • c ∈ T }.
We refer you to [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF][START_REF] Gapeyev | Recursive subtyping revealed: (functional pearl)[END_REF] for more details on infinite trees.

Semantics

The tentative semantics is presented using inference rules in Figure 1. The semantics ρ ⊢ t ; v is a relation between an environment ρ ∈ X → V , a term t ∈ T and the semantic value v ∈ V of the term in the environment.

As side-condition to some of the rules, we write v ≤ v ′ where v is a value and v ′ is the shape of a value to mean that value v is neither diverge nor of the shape v ′ . The inference rules read well. The value of a variable is taken from the environment. The value of a function abstraction is a closure composed of the abstraction together with the current environment. The value of a pair of two terms is the pair composed of the values of each of the terms. For value destructors (function application and pair projections), there are three cases. Consider a function application t t ′ . If the value of term t is a closure (λx.t ′′ ) ρ ′ , then the value of the application is the value of the closure body t ′′ in the environment ρ ′ ; x → v ′ derived from the closure environment ρ ′ by assigning to the function parameter x the value v ′ of the argument t ′ . If term t diverges, then so does the function application. Otherwise, the application fails. The rules for projections are similar. If the value of a term t is a pair, then the value of the projection fst t (resp. snd t) is the first element (resp. the second element) of the pair. If the term diverges, then so does the projection. Otherwise, the projection fails.

The semantics can be understood as an abstraction of callby-need that does not account for when a term is evaluated, but only expresses that terms are evaluated at most once. Hence, we avoid the imperative flavour of typical operational semantics of call-by-need, where thunks are created to delay the evaluation of terms, and are later updated in place once their value is computed. One might rightly argue that, as is, one cannot really distinguish the calculus from a callby-name calculus. The difference would really become visible if a non-deterministic construction were added (a nondeterministic choice, for instance, as in [START_REF] Kutzner | A non-deterministic callby-need lambda calculus[END_REF]). Indeed, consider an expression (λx.(x, x)) t where subexpression t may evaluate to several distinct values due to non-determinism. In a call-by-need settings, as t is evaluated at most once, the whole expression only evaluates to values of the shape (v, v). This is reflected in our calculus by the fact that a function parameter x is bound to a single value when a function application is evaluated. On the other hand, in a call-byname settings, the expression can also evaluate to values of the shape (v 1 , v 2 ), where v 1 and v 2 are two distinct values of subexpression t.

Now, what do the inference rules of Figure 1 actually mean? The standard interpretation of inference rules is as inductive rules, that is, the assertion ρ ⊢ t ; v holds if, using the inference rules, one can build a finite tree (a derivation) that justifies this assertion. An example of derivation is given in Figure 2. But we are only capturing finite behaviors this way: it is not possible to derive ρ ⊢ t ; diverge for any term t (when the environment ρ does not already contain the diverge value), as all rules that yield divergence also assume divergence as hypothesis! It is also not possible to derive that a term evaluates to any infinite value. Thus, a different interpretation of inductive rules is needed. For this, let us first come back to the definition of inference rules. Inference system. An inference system Φ over a set U is a set of pairs (A, c) ∈ P(U ) × U [START_REF] Aczel | An introduction to inductive definitions[END_REF]. The pair (A, c) is called an inference rule and is usually written:

∅ ⊢ λx.(x, x) ; (λx.(x, x)) ∅ ABS ∅ ⊢ f ; (f ) ∅ VAR ρ ⊢ x ; (f ) ∅ VAR ρ ⊢ x ; (f ) ∅ ρ ⊢ (x, x) ; ((f ) ∅ , (f ) ∅ ) PAIR ∅ ⊢ (λx.(x, x)) f ; ((f ) ∅ , (f ) ∅ ) APP where f = λx.x and ρ = x → (f ) ∅ . Figure 2. Simple derivation. ABS ∅ ⊢ ∆ ; (∆) ∅ ABS ∅ ⊢ ∆ ; (∆) ∅ VAR ρ ⊢ x ; (∆) ∅ VAR ρ ⊢ x ; (∆) ∅ . . . ρ ⊢ x x ; diverge APP ρ ⊢ x x ; diverge APP ∅ ⊢ ∆ ∆ ; diverge APP where ρ = x → (∆) ∅ .
a 1 . . . a n c
where A = {a 1 , . . . , a n }. The intuitive reading of such a rule is that the conclusion c holds if and only if all the antecedents in A hold.

Given an inference system Φ, we define the operator F Φ : P(U ) → P(U ) as

F Φ (S) = {c ∈ U | ∃A ⊆ S, (A, c) ∈ Φ}.
The set F Φ (S) is the set of conclusions that can inferred in one step from the antecedents in S. The operator F Φ is monotonic. By Knaster-Tarski [START_REF] Tarski | A lattice theoretical fixpoint theorem and its applications[END_REF] theorem, it has a least and a greatest fixpoint. The least fixpoint lfp F Φ is the inductive interpretation of the inference system Φ. The greatest fixpoint gfp F Φ is the coinductive interpretation of the inference system Φ.

There are reasoning principles associated to these fixpoints. The induction principle can be stated as follows: if X is F -closed (that is, F (X) ⊆ X), then lfp F ⊆ X. The coinduction principle can be stated as follows: if X is Fconsistent (that is, X ⊆ F (X)), then X ⊆ gfp F . Using the coinduction principle, one can prove that an element x is included in gfp X by finding an F -consistent set X such that x ∈ X. In the case of the least fixpoint, one uses the fact that lfp F = F n (∅). Thus, x ∈ lfp F if there exists n such that x ∈ F n (∅).

Concretely, with the inductive interpretation, a conclusion c holds if one can build a finite tree that derives c using the inference rules in system Φ. With the coinductive interpretation, a conclusion c holds if one can build a possibly infinite tree ending with conclusion c. The F -consistent set that proves that c holds is the set of elements of U that occur in the derivation tree. We refer you to [START_REF] Gapeyev | Recursive subtyping revealed: (functional pearl)[END_REF], for instance, for more details on coinductive reasoning.

In our case, the rules of Figure 1 define a map F on semantic relations, where a semantic relation is a relation between an environment ρ ∈ X → V , a term t ∈ T and the semantic value v ∈ V of the term in the environment. We have seen that the inductive interpretation of the rules (the least fixpoint of F ) is not large enough to encompass diverging behaviors. The coinductive interpretation seems more promising. For instance, one can derive that term ∆ ∆, where ∆ = λx.x x, diverges: indeed, the derivation in Figure 3 can be extended forever by repeating the same pattern of function application and pair evaluation. Similarly, one can show that some terms evaluate to infinite values. Figure 4 illustrates the fact that term Π Π, where Π = λx.(x x, x x), evaluates to the infinite value p such that p = (p, p). But, actually, the derivation of Figure 3 can be generalised to show that term ∆ ∆ evaluates to any value v, as shown in Figure 5. This is really not what we want! Thus, while the inductive interpretation of the inference rules is too small, the coinductive interpretation appears to be too large. It seems that we need to find a fixpoint in-between.

ρ ≤ ρ ′ (λx.t) ρ ≤ (λx.t) ρ ′ v 1 ≤ v ′ 1 v 2 ≤ v ′ 2 (v 1 , v 2 ) ≤ (v ′ 1 , v ′ 2 ) diverge ≤ v for all x, ρ(x) ≤ ρ ′ (x) ρ ≤ ρ ′
More precisely, the issue we have is that the calculus should be deterministic: to each environment ρ and term t should be associated exactly one value v. This is not the case with the fixpoints we have considered so far. But remark that operator F returns a function when given as input a function.

FACT 1. Operator F is a self-map on the graph of functions in (X → V ) → T → V .
In other words, the operator F preserves determinism. This gives us some confidence that it has a deterministic fixpoint. By the way, this is also a strong hint that we have the right set of rules, with no missing nor overlapping rules.

Thus, we want a fixpoint of operator F that is a function. But how to find such a fixpoint? The solution comes from order theory: we need to find a suitable domain of functions in which operator F has a least fixpoint. To find this fixpoint, the idea is to consider approximate derivations, that corresponds intuitively to giving up the computation of parts of a value at some points, returning the diverge value instead. Approximate derivations are partial derivations where all assertions ρ ⊢ t ; v are justified (like for a normal finite derivation), except possibly for some assertions of the shape ρ ⊢ t ; diverge. An example is given in Figure 6, where the rightmost assertion at the top is not justified. Then, a correct derivation should be the limit of a suitable set of approximate derivations. For instance, the partial derivation in Figure 6 shows that the resulting value is a pair of pairs. By considering larger partial derivations, one can get a more precise approximation of the value. This approach rules out the derivation in Figure 5, where value v is coming out of this air, from infinity: if one gives up the computation at any point, one does not get any value as a result but diverge.

We will progressively make these ideas precise. As a first step, we define the approximation relation between finite values by the inductive rules in Figure 7: an approximation of a value is built by replacing some of its subvalues by the diverge value. Intuitively, it is then enough to work with finite values, as we will be able to approximate infinite values as precisely as wanted using only finite values (in a sense that will be made precise later). Hence, from now on, we write v to denote only finite values, and v to denote any value, including infinite ones. The inference rules of Figure 1 are reinterpreted accordingly. As we use heavily orders and more generally preorders below, we remind their definitions.

Preorder. A preorder ≤ on a set A is a binary relation on this set which is both reflexive (for all x in A, we have x ≤ x) and transitive (for all x, y, z in A, if x ≤ y and y ≤ z, then x ≤ z). A set A with a preorder ≤ defined on it is called a preordered set. We denote it by (A, ≤), or just A when there is no confusion.

An order is a preorder that is also antisymmetric (that is, if for all x, y in A, x ≤ y and y ≤ x implies x = y). A set A with an order ≤ defined on it is called an ordered set.

A preorder induces an equivalence relation ≡ on A (x ≡ y iff x ≤ y and y ≤ x), and an order on the quotient set A/≡. However, it is often more convenient (in particular, when undertaking mechanised proofs) to work directly with the initial preordered set rather than with the quotient set.

We expect that the more precise the input of the semantic function, the more precise its output. We should thus consider only monotonic semantic functions. Then, function F should also be monotonic, for a suitable order on semantic functions: given more precise subcomputation results, the function F should produce more precise computation results. Formally, we adopt the following definitions. Monotonic map. A monotonic map f : A → B between two preordered sets A and B is a map that preserves the preorder, that is, for all

x 1 , x 2 in A, if x 1 ≤ x 2 , then f (x 1 ) ≤ f (x 2 ). We write A → m B for the set of monotonic maps from A to B.
Pointwise order on functions. Given a set A and a preordered set B, one can define a canonical preorder on functions in A → B by:

f ≤ g iff ∀x ∈ A, f (x) ≤ g(x).
Monotonic functions A → m B between two preordered sets A and B can be ordered canonically in the same way.

Then, we have the expected result. FACT 2. Function F is a monotonic self-map on functions We are onto something. But, remember we have defined F for finite values only. The next step is to define infinite values and extend F to deal with them. We want infinite values to be limits of a set of finite values. We need to make a number of definition to precise this notion of limit. In particular, for preorders, the natural notion of limit is the supremum.

(X → V ) → m T → V . ABS ∅ ⊢ ∆ ; (∆) ∅ ABS ∅ ⊢ ∆ ; (∆) ∅ VAR ρ ⊢ x ; (∆) ∅ VAR ρ ⊢ x ; (∆) ∅ . . . ρ ⊢ x x ; v APP ρ ⊢ x x ; v APP ∅ ⊢ ∆ ∆ ; v APP where ρ = x → (∆) ∅ . Figure 5. Incorrect derivation. VAR ρ ⊢ x ; (Π) ∅ VAR ρ ⊢ x ; (Π) ∅ ρ ⊢ (x x, x x) ; diverge ρ ⊢ x x ; diverge APP ρ ⊢ (x x, x x) ; (diverge, diverge) PAIR ρ ⊢ x x ; (diverge, diverge) APP ρ ⊢ (x x, x x) ; ((diverge, diverge), (diverge, diverge)) PAIR where ρ = x → (Π) ∅ .
Least element and supremum. A least element x of a subset s of a preordered set A is an element of s which is smaller than all other elements in s. The supremum x of a subset s of a preordered set A, if it exists, is the least element of A that is greater or equal to all elements of subset s. Suprema and least elements are each unique up to equivalence.

Directed subset. A subset s of a preordered set A is a directed subset of A if it is nonempty and every pair of its elements has an upper bound : for all x and y in s, there exists z in s such that x ≤ z and y ≤ z. Directed sets are a generalisation of chains (that is, totally ordered subsets of a preordered set). Intuitively, if a directed subset s has a limit (its supremum), then given two elements of s, it is always possible to find an element of s that provides a better approximation of the limit.

Directed complete preordered set (DCPO). A directed complete preordered set is a preordered set such that each of its directed subsets has a supremum. Note that DCP O normally stands for directed complete (partial) order. We use a more general definition in the present paper.

We now define the set of possibly infinite values as a completion of the set of values V , so that infinite values v be the limits of finite values that approximate them. The idea is similar to the way real numbers can be constructed as a completion of the rational numbers. We first define the objects that we want to converge. In the case of real numbers, these are Cauchy sequences. Here, we consider directed sets of values. Then, we specify how their expected limits should be related. In other words, we define an equivalence relation between Cauchy sequences or, here, a preorder on directed set. Finally, the completed set is obtained by quotienting by the equivalence relation. It appears that we can reason directly on the preorder. We thus skip this last step.

Preorder completion. The preorder completion A of a preordered set A is the set of directed subsets of A, with the following preorder:

s ≤ t iff ∀x ∈ s, ∃y ∈ t, x ≤ y.
Intuitively, for any approximation x in s, there should exist a more precise approximation y in t. The set A is a DCPO.

A supremum of a directed set d of elements of A is their union: sup d = s∈d s. The function i : x → {x} is a monotonic injection of A into A (in the relaxed sense that, if i(x) ≡ i(y), then x ≡ y). Thus, one can consider A as if it was a subset of A.

This completion is equivalent to the standard ideal completion, where an ideal is a downward closed directed subset. Indeed, any directed subset s is equivalent to its downward closure {x ∈ A | ∃y ∈ s, x ≤ y}.

We thus define the set of possibly infinite values as being V , the completion of the set of finite values V . We should now extend the definition of function F to also deal with infinite values. There is a canonical way to do it and get a continuous function (that is, a morphism between DCPO).

Continuous function.

A function f between two preordered sets A and B is continuous if it preserves suprema of directed set, that is, if for any directed subset s of A, if x ∈ A is a supremum of s, then f (x) is a supremum of f (s). We write A → c B for the set of continuous functions from A to B. A continuous function is monotonic.

A monotonic function f : A → m B can be extended in a unique way, up to equivalence, into a continuous function ↑f : A → c B such that, for all x ∈ A, we have ↑f ({x}) ≡ {f (x)} (this equation states that ↑f coincides with f for all elements of set A). This function can be defined by:

↑f (X) = {f (x) | x ∈ X}.
Thus, we consider the continuous function ↑F . We need to show that it has a fixpoint. We rely on the following theorem.

Kleene fixpoint theorem. A complete preordered set (CPO) is a directed complete preordered set with a least element ⊥.

Every continuous self-map f on a CPO has a least fixpoint lfp f (such that f (lfp f ) ≡ lfp), which is a supremum of the iterates {⊥, f (⊥), f (f (⊥)), . . . , f n (⊥), . . .}.
The set (X → V ) → m T → V is a CPO, with least element the set {λρ.λt.diverge}. Hence, applying the theorem to ↑F , we get a least fixpoint, which is the semantics of the calculus. Or is it? The fixpoint lfp ↑F is in (X → V ) → m T → V . But we would like the semantics to be in (X → V ) → m T → V ! How far are we from that? As we show now, the two sets can be related in an appropriate fashion, so that lfp ↑F can indeed be considered as a semantics.

For that, we need to understand how preorder completion commutes with arrows. As we will show, the set A → B, where A is a set and B is a preordered set, can be seen as a refinement of the set A → B, in the sense that the second set is equivalent to a partition of the first set. The sets A → m B and A → c B, where A and B are both preordered sets, are related in a similar fashion. The relations between these pairs of sets will be materialised by pairs of functions. Then, by combining appropriately the fixpoint lfp ↑F with these functions, we get a semantics of the expected type. We need to introduce a number of definitions to state this precisely.

Galois connection. A Galois connection [START_REF] Erné | A Primer on Galois Connections[END_REF] between two preordered sets A and B is a pair of functions f : A → B and g : B → A such that for all x in A and y in B we have f (x) ≤ y if and only if x ≤ g(y). In this situation, function f is called the lower adjoint of function g and function g is called the upper adjoint of function f . If (f, g) is a Galois connection, then function f is continuous and function g is monotonic. Besides, given function f , function g is unique up to equivalence, as g(y) is a supremum of {x ∈ A | f (x) ≤ y} for all y in B.

Preorder equivalence. Two preordered sets A and B are equivalent, written A ≈ B, if there exists a pair of functions f : A → m B and g : B → m A such that for all x in A, g(f (x)) ≡ x and for all y in B, f (g(y)) ≡ y. In other words, two preordered sets are equivalent when their associated quotient ordered sets are isomorphic.

If two preordered sets A and B are equivalent, as witnessed by two functions f : A → m B and g : B → m A, then (f, g) is a Galois connection. Conversely, given two preordered sets A and B and two functions f : A → B and g : B → A, if both (f, g) and (g, f ) are Galois connections, then A and B are equivalent.

Reflection. A reflection [START_REF] Erné | A Primer on Galois Connections[END_REF][START_REF] Melton | Lagois connections -a counterpart to Galois connections[END_REF] between two preordered sets A and B is a Galois connection (f, g) between A and B such that for all y in B, f (g(y)) ≡ y.

The existence of a reflection between two preordered sets A and B makes it possible to consider set A as a refinement of set B, in the sense that B is equivalent to a partition of A. More precisely, a Galois connection (f, g) between two preordered sets A and B induces an equivalence relation ∼ on A compatible with the preorder:

x 1 ∼ x 2 iff f (x 1 ) ≡ f (x 2 )
. Then, the Galois connection (f, g) is a reflection when the preordered sets A/∼ and B are equivalent.

Given a set A and a preordered set B, we thus want to define a reflection (G * , G * ) between sets A → B to A → B. Though these two functions depend on sets A and B, we do not index them, as the involved sets will always be clear from the context. The function G * should basically be the identity for functions in A → B. By using the appropriate injection functions, a function f ∈ A → B corresponds to {f } in A → B and λx.{f (x)} in A → B. We should therefore have

G * ({f })(x) = {f (x)}.
Function G * should also be continuous for (G * , G * ) to be a Galois connection. Thus, we should have, for all s ∈ A → B and all x ∈ A,

G * (s)(x) ≡ G * (sup{{f } | f ∈ s})(x) ≡ (sup{G * ({f }) | f ∈ s})(x) ≡ sup{G * ({f })(x) | f ∈ s} ≡ sup{{f (x)} | f ∈ s} ≡ {f (x) | f ∈ s}.
We thus take

G * (s)(x) = {f (x) | f ∈ s}. 6 2012/3/19
Given the characterisation of G * in function of G * for Galois connections, one can show that one must have

G * (f ) ≡ {g ∈ A → B | ∀x, {g(x)} ≤ f (x)}.
This can be taken as a definition of G * (f ) by replacing the equivalence by an equality. We have the expected result.

THEOREM 3. The pair (G * , G * ) is a reflection.

It is instructive to understand why we do not have a preorder equivalence but only a reflection. For that, consider the sequence of functions f i from natural numbers to values defined by

f i (j) = error if i ≤ j diverge otherwise
and the function f defined by f (j) = error for all j ∈ N. Then, we have

sup{f i | i ∈ N} ≡ f in N → V , but sup{{f i } | i ∈ N} ≡ {f i | i ∈ N} ≡ {f } in N → V .
What happens is that existing suprema, when they are not also greatest elements, are not preserved by completion; instead, new suprema are added just below. Note that, however, we have G * (G * ({f i | i ∈ N})) ≡ {f }, and thus, G * ({f i | i ∈ N}) ≡ G * ({f }): the sets {f i | i ∈ N} and {f } cannot be distinguished when considered as functions in N → V . This kind of situation does indeed happen with our semantic function, with any sequence of terms that take longer and longer to yield a result. This example also suggests that one could get an equivalence by restricting appropriately the sets of functions considered so that it contains no problematic sequence of functions such as functions f i above. This idea is developed in Section 3.2.

We similarly relate the sets A → m B and A → c B by the pair of functions (H * , H * ) defined by

H * (f )(x) = {f (x) | f ∈ f , x ∈ x} H * (g) = {f ∈ A → m B | ∀x, {f (x)} ≤ g({x})}.
The two functions are well-defined and suitably related. We can finally define the semantics of a term t ∈ T in an environment ρ ∈ X → V , as a value in V :

t ρ = (G * • H * (lfp ↑F ) • G * )( ρ)(t).
There is a slight rough point with this definition. Indeed, while functions G * and H * are both continuous (as lower adjoints of a Galois connection), function G * is only monotonic. When computing t ρ , we therefore need to approximate G * ( ρ) ∈ X → V , not directly ρ ∈ X → V . In other words, a kind of uniform convergence is required: we need to provide a directed set of functions in X → V as approximations, rather than providing for each variable x in X a directed set of values. For these reasons, we find it useful to also state the semantics of a term t ∈ T in an environment ρ ∈ X → V :

t ρ = (G * • H * (lfp ↑F ))(ρ)(t).
To provide better insight on the semantics, it is interesting to unravel the definitions. We consider an environment ρ ∈ X → V and a term t ∈ T . We compute

(G * • H * (lfp ↑F ))(ρ)(t) ∈ V . Function F is a self-map on the preordered set Σ = (X → V ) → m T → V .
This set has a least element ⊥ Σ = λρ.λt.diverge. Then, function ↑F is a self-map on the CPO Σ and ⊥ Σ = {⊥ Σ } is a least element of this CPO. The semantic function is defined using Kleene fixpoint theorem as the following least fixpoint of ↑F :

lfp ↑F = sup{(↑F ) n (⊥ Σ ) | n ∈ N}.
We have, by definition, (↑F )(X) = {F (x) | x ∈ X}. Hence, (↑F ) n (⊥ Σ ) = {{F n (⊥ Σ )}}. Then, by definition of sup for a completed preorder,

lfp ↑F = sup{{F n (⊥ Σ )} | n ∈ N} = {F n (⊥ Σ ) | n ∈ N}.
Then, we have, by definition of H * ,

H * (lfp ↑F )(ρ) = H * ({F n (⊥ Σ ) | n ∈ N})(ρ) = {F n (⊥ Σ )(ρ) | n ∈ N, ρ ∈ ρ}.
Finally, by definition of G * ,

t ρ = (G * • H * (lfp ↑F ))(ρ)(t) = G * ({F n (⊥ Σ )(ρ) | n ∈ N, ρ ∈ ρ})(t) = {F n (⊥ Σ )(ρ)(t) | n ∈ N, ρ ∈ ρ}.
The expression F n (⊥ Σ ) is the set of assertions ρ ⊢ t ; v that can be deduced by building approximate derivations of height n. So, the value of term t in environment ρ is the limit of the values derived from more and more precise derivation trees, and for better and better approximations ρ of environment ρ. This is what we expected.

To summarize this section, we define the semantics through inductive rules only involving finite values. We prove that these rules define a monotonic operator F that maps a preordered set of functions onto itself (Facts 1 and 2). These are the only proofs that have to be adapted for other calculi. They indicate, in particular, that there is no missing nor overlapping rules. Such an operator can automatically be extended to work on the CPO obtained by completion of the preordered set of functions. There, it has a least fixpoint, which we consider as the semantics of the calculus. Though this fixpoint is not a function mapping environments and terms to values, it can be considered as such, in a canonical way, by a suitable use of reflections. Values

Γ ⊢ t : τ 1 × τ 2 Γ ⊢ fst t : τ 1 Γ ⊢ t : τ 1 × τ 2 Γ ⊢ snd t : τ 2
ρ : Γ Γ; x : τ 1 ⊢ t : τ 2 (λx.t) ρ : τ 1 τ 2 v 1 : τ 1 v 2 : τ 2 (v 1 , v 2 ) : τ 1 × τ 2 diverge : τ Environments ρ : ∅ ρ : Γ ρ(x) : τ ρ : Γ; x : τ Figure 9.
Typing rules for values.

Type Soundness

We illustrate how to reason on the semantics by proving a type soundness result. We use simple infinite types: types are defined coinductively by the grammar below.

τ ::= τ → τ function type τ × τ pair type
The use of infinite types ensures that interesting programs can be typed while having a very short grammar of types and few typing rules. In particular, the fixpoint operator

Y = λf.(λx.f (x x)) (λx.f (x x))
is well typed, with type (τ → τ ) → τ for any type τ . The typing relation Γ ⊢ t : τ , where environments Γ are sequence of bindings x : τ , is defined using inductive rules in Figure 8. These typing rules are standard.

In order to prove type soundness, we define a typing relation for values. We first define inductively the type of finite values (Figure 9). We want to extend this definition to all values by continuity. Given a type τ , the predicate v : τ can be seen as a function from finite values V to Booleans.

The CPO of Booleans. The set Bool = {true, false} of Booleans, ordered such that true ≤ false, is a CPO. Besides, this set Bool and its completion Bool are equivalent: the function that maps Boolean b to the set {b} and the function that maps set s ∈ Bool to its greatest element (which always exists) are both monotonic and inverse of one-another.

A predicate on a set A is a function in A → Bool. Given a preordered set A, a monotonic predicate P on A, that is a function in A → m Bool, can be extended into a continuous predicate P = sup •(↑P ) on A. By unfolding definitions, one can see that P (s) holds when P (x) holds for all x in s.

Hence, if typing rules v : τ are monotonic with respect to values v, we can extend them to infinite values. FACT 5. The typing rules for values define, for each type, a monotonic predicate on finite values. The same holds for the typing rules for environments.

We can therefore adopt the following definitions to type values v ∈ V and environments ρ ∈ X → V :

• v : τ when, for all v ∈ v, we have v : τ ;

• ρ : Γ when, for all ρ ∈ ρ, we have ρ : Γ.

The soundness theorem can now be stated as follows.

THEOREM 6 (Type Soundness). If Γ ⊢ t : τ then, for all ρ ∈ X → V such that ρ : Γ, we have t ρ : τ .

The result can also be stated for environments ρ ∈ X → V . This is an immediate consequence of the theorem. COROLLARY 7. If Γ ⊢ t : τ then, for all ρ ∈ X → V such that ρ : Γ (that is, G * ( ρ) : Γ), we have t ρ : τ .

To prove the theorem, we need a way to reason about the semantics. The characterisation of the least fixpoint given by Kleene theorem provides such a reasoning principle.

Induction principles. The standard reasoning principle can be stated as follows. An admissible predicate is a continuous map from a CPO A to the CPO of Booleans. Let f be a continuous self-map on a CPO A. Suppose that an admissible predicate P on A is such that:

• P (⊥);

• for all x in A, we have P (x) implies P (f (x)).

Then P (lfp f ) holds.

When the CPO is the completion A of a preordered set A, a variant of this induction principle allows to reason only on A rather than on A. Let f be a monotonic self-map on a preordered set A with a least element ⊥. Suppose that a monotonic predicate P on A is such that:

• P (⊥);

• for all x in A, we have P (x) implies P (f (x)).

Then P (lfp ↑f ) holds.

This variant relies on equality (↑f ) n ({⊥}) = {f n (⊥)}, from which one can deduce lfp ↑f = {f n (⊥) | n ∈ N}.

Thus, we distinguish the values v ∈ V of the calculus from the semantic values s ∈ S. We have the following grammars.

v ::= (λx.t) ρ function closure (v, v) pair s ::= v regular value diverge divergence error error
Semantic values are ordered as follow: s 1 ≤ s 2 when s 1 = diverge. This is a so-called flat CPO. An interesting property of flat CPOs is that they are equivalent to their completion: S ≈ S. This is because all suprema are reached. The canonical injection function maps set S to set S; the converse mapping is provided by the supremum function. Note that Booleans are another instance of flat CPOs.

The semantics is a relation ρ ⊢ t ; s between an environment ρ ∈ X → V , a term t ∈ T and a semantic value s ∈ S. We define it by the inference rules in Figure 10. One can check that the operator F specified by these rules is a monotonic self-map on

(X → V ) → T → S.
As previously, we extend F into a self-map ↑F on CPO:

(X → V ) → T → S.
The semantics is the least fixpoint lfp ↑F of this operator.

To use it, one should compose it with appropriate reflections. We thus adopt the following definition:

t ρ = sup(G * (G * (lfp ↑F )(ρ))(t)).
This gives us a function with signature

(X → V ) → T → S,
which is exactly the expected signature of a semantics.

Note that we could have left implicit either the rules for divergence, or the rule for errors. Then, the inference rules would define a partial operator F ′ . When the divergence rules are omitted, this operator can be extended into the total operator F by

F (σ)(ρ)(t) = F ′ (σ)(ρ)(t) when defined diverge otherwise.
One can then proceed as previously to define the semantics.

Maps with Finite Support

We have shown in Section 2.2 that the DCPOs A → B and A → B, where A is a set and B is a preordered set, are not equivalent in general. One can show, however, that the equivalence holds when the set A is finite. Another interesting case is when one restricts oneself to functions with finite support. Let A be a set and B be a preordered set with a distinguished maximal element m (that is, for all y in B, if m ≤ y, then m ≡ y). We say that a function g ∈ A → B has finite support when g(x) = m for all x in A but a finite number of them. We write A → f B for the set of such functions. One can then show that A → f B and A → f B are equivalent, with witness the pair of functions (G * , G * ). defined previously, restricted to these sets. As a consequence of the equivalence, both these functions are continuous.

It is quite usual to consider environments to be functions from variables X to values V with finite support (taking error as distinguished element). This solves the issue we encountered in Section 2.2 where we saw that environments had to be approximated in X → V rather than in X → V for lack of continuity. The price to pay is a more complex definition of environments.

Non-Determinism

As we mentioned in Section 2.2, it would be interesting to extend our running example with a non-deterministic choice. Indeed, we explained that this operator makes it possible to distinguish call-by-need from call-by-name. But then, clearly, the semantics is not going to be a function returning a single value anymore.

The usual approach to deal with non-determinism is to use powerdomains (the order-theoretic counterparts to powersets), such as Plotkin powerdomains [START_REF] Plotkin | A powerdomain construction[END_REF]. Then, the semantic is a function returning an element in a powerdomain of values. But powerdomains are complex beasts, and thus we loose some of the simplicity of our approach.

An alternative due to Cary and Sarkar [START_REF] Crary | Foundational certified code in the twelf metalogical framework[END_REF] is to use oracles: the semantics is made deterministic by threading an oracle, a sequence of Boolean Ω = (ω n ) n∈N , through the computation. The semantic relation ρ ⊢ Ω t ; v, can then associate a single value to a triple of an oracle, an environment and a term. Whenever a Boolean is needed (for instance, to choose an alternative for a non-deterministic choice), one can take the first element ω 0 of the sequence; it remains the oracle (ω ′ n ) n∈N such that ω ′ n = ω n+1 . An oracle can also be split into two independent oracles (ω 1 n ) n∈N and (ω 2 n ) n∈N with ω 1 n = ω 2n and ω 2 n = ω 2n+1 . This is useful when several computations are performed independently. This would be the case for the evaluations of the function argument and the function body in rule APP of Figure 1.

Mechanised Formalisation

Our results regarding the call-by-need calculus of Section 2 have been formalised in Coq [START_REF]The Coq Development Team: The Coq Proof Assistant Reference Manual -Version V8.2[END_REF]. Our packaging of mathematical structures (preorders, DCPOs and CPOs, and the corresponding morphisms) follows the techniques established by Garillot, Gonthier, Mahboubi and Rideau [START_REF] Garillot | Packaging mathematical structures[END_REF][START_REF] Gonthier | Type design patterns for computer mathematics[END_REF].

We take Coq propositions Prop for the CPO of Booleans. We have the following hierarchy of structures:

• a preorder is a set A with a reflexive transitive relation sub : A → A → Prop;

• a DCPO is a preorder with a function sup of signature directed_set A → A, which associates to each directed set its supremum (a directed set directed_set A is a characteristic function, that is a function in A → Prop, with suitable properties);

• a CPO is a DCPO with a least element bottom.

The fact that sup is defined as a function rather than a relation makes it possible to have an explicit definition of the least fixpoint lfp f of a function f, as the function sup applied to the directed set containing the iterates f n (bottom). However, due to the constructive nature of Coq, the supremum function sup cannot be defined for concrete CPOs such as the set S of semantic values of Section 3.1: it is not possible to associate in a constructive way a suitable element of S to the characteristic function f : S → Prop corresponding to each directed set. For the same reason, one can establish that S and S are equivalent preorders (in the sense that there exists suitable functional relations between the two), but it is not possible to provide an explicit function that map an element of S to an element of S.

The operator F is directly specified in Coq as a function from semantic functions to semantic functions. We use pattern matching, which helps keep the definition short by sharing some cases. Such a definition directly shows that operator F maps functions to functions (Fact 1). Then, one only needs to show that F is appropriately monotonic (Fact 2) to complete the definition of the semantics of the calculus. Establishing type soundness is similarly short and simple.

The mechanised formalisation of complex semantics was one of the main motivations for this work. We found that working with a proof assistant was also very helpful for finding the right definitions.

Related Work

The works by Gunter and Remy [START_REF] Gunter | A proof-theoretic assessment of runtime type errors[END_REF] and Stoughton [START_REF] Stoughton | An operational semantics framework supporting the incremental construction of derivation trees[END_REF] are most related to ours. They describe the incremental construction of derivation trees, which is similar to our presentation of approximate derivations. We go beyond these works by working at a more abstract level, making an explicit connection with order theory and dealing with more complex domains of values.

Leroy and Grall [START_REF] Leroy | Coinductive big-step operational semantics[END_REF] present a trace-based big-step semantics for a call-by-value calculus. They use separately an inductive definition for converging behaviors and a coinductive definition for divergence. It would be interesting to compare this approach with ours in which both cases would be handled simultaneously. The complexity should be inbetween the two calculi we have studied here: one has to deal with finite values V and environments X → V but infinite semantic values (traces) S.

An alternative to our order-theoretic approach is the mixed induction and coinduction approach, advocated in particular by Danielsson and Altenkirch [START_REF] Danielsson | Subtyping, declaratively: an exercise in mixed induction and coinduction[END_REF], where rules are partitioned into inductive and coinductive rules. With this approach, inference rules are separated in two sets: those interpreted in a inductive fashion, and those interpreted in a coinductive fashion. This yields two operators F ind and F coind . These operators are then combined into a single operator F (X, Y ) = F ind (X) ∪ F coind (Y ). Then, the semantics of the rules is gfp(λY. lfp(λX.F (X, Y ))).

In order to reason on this semantics, one has to combine coinduction with induction. Concretely, derivation trees are allowed to be infinite, but only finitely many inductive rules may ever appear on top of one another without any coinductive rule in-between. In our case, rules for divergence should be interpreted in a coinductive way; the rule APP for function application ought to be split in two, depending on whether the function body evaluates to diverge or not. We feel that having to combine inductive and coinductive reasoning is complex. For instance, the proof that the semantics of the calculus is deterministic would not be immediate at all with this approach: it would be a rather complex proof involving both induction and coinduction.

A similar approach, proposed by Cousot and Cousot [START_REF] Cousot | Inductive definitions, semantics and abstract interpretations[END_REF][START_REF] Cousot | Bi-inductive structural semantics[END_REF], is to partition instead the universe U , relying on the following set isomorphism: P(U 1 ∪ U 2 ) ≈ P(U 1 ) × P(U 2 ). Then, one can order P(U 1 ) by inclusion and use the converse order for P(U 2 ). This works well for a call-by-value semantics, where one can separate converging behaviors from diverging behaviors, but it is not clear how this framework can be extended to cover our call-by-need calculus.

We use order theory to define an operational semantics. A fruitful research topic has been to start instead from an operational semantics and build order-theoretic concepts upon this semantics. This includes defining types as sets of terms that are downward-closed and closed under limits, as in MacQueen, Plotking and Sethi [START_REF] Macqueen | An ideal model for recursive polymorphic types[END_REF], Abadi, Pierce and Plotkin [START_REF] Abadi | Faithful ideal models for recursive polymorphic types[END_REF], Birkedal and Harper [START_REF] Birkedal | Constructing interpretations of recursives types in an operational setting[END_REF], or Vouillon and Melliès [START_REF] Vouillon | Semantic types: a fresh look at the ideal model for types[END_REF]. It is also possible to define syntactic logical relations as in Crary and Harper [START_REF] Crary | Syntactic logical relations for polymorphic and recursive types[END_REF]. As shown by Mason, Smith and Talcott [START_REF] Mason | From operational semantics to domain theory[END_REF][START_REF] Smith | The coverage of operational semantics[END_REF], many notions from domain theory can be defined in this context.

There have been several formalisations of domain theory in Coq. Bertot and Komendantsky [START_REF] Bertot | Fixed point semantics and partial recursion in Coq[END_REF] use a choice axiom to prove Kleen fixpoint theorem. They are able to extract possibly non-deterministic programs. During extraction, the least fixpoint operator is replaced by a fixpoint function of the target language. Paulin-Mohring [START_REF] Paulin-Mohring | From Semantics and Computer Science: Essays in Honor of Gilles Kahn, chap. A constructive denotational semantics for Kahn networks in Coq[END_REF] develop a constructive formalisation, taking advantage of the possibility to define coinductive datastructures in Coq. Benton, Birkedal, Kennedy and Varming [START_REF] Benton | Formalizing domains, ultrametric spaces and semantics of programming languages[END_REF][START_REF] Benton | Some domain theory and denotational semantics in Coq[END_REF] extend this work up to and including the inverse-limit construction of solutions to mixedvariance recursive domain equations, and the existence of invariant relations on those solutions. Our work is different from these works as we use syntactic values as a domain: for instance, the semantics of an abstraction is syntactically a closure, not a continuous function from values to values. We have a non-constructive definition of CPOs. But it should be possible to specify our semantics in a constructive way, as they are defined as the supremum of a chain.

Conclusion

We have presented a way to specify big-step semantics that account simultaneously for finite and infinite behaviors, based on order theory. We were able to specify semantics with little proof obligations. Basically, one only has to prove that the inference rules define a monotonic self-map on a suitable set of functions, which is easy. It is noteworthy that we do not have to establish any continuity property (as is often the case for order-theoretic developments); indeed, this is typically a lot more complicated. Also, we only work with very concrete objects defined using inductive grammars and with finite derivations involving these objects; in particular, it is possible to reason inductively on these objects and derivations, as well as on the semantics itself. A bit more work is required than with the standard way of defining bigstep semantics, but we gain a lot in precision.

Figure 3 .

 3 Figure 3. Derivation for a diverging term.

Figure 4 .

 4 Figure 4. Term evaluating to an infinite value.

Figure 7 .

 7 Figure 7. Order on finite values and environments.

Figure 6 .

 6 Figure 6. Truncated derivation.

THEOREM 4 .

 4 The pair (H * , H * ) is a reflection.

Figure 8 .

 8 Figure 8. Typing rules for terms.

2012/3/19

2012/3/19

2012/3/19

2012/3/19

2012/3/19 Γ(x) = τ Γ ⊢ x : τ Γ; x : τ 1 ⊢ t : τ 2 Γ ⊢ λx.t : τ 1 → τ 2 Γ ⊢ t 1 : τ 1 → τ 2 Γ ⊢ t 2 : τ 1 Γ ⊢ t 1 t 2 : τ 2 Γ ⊢ t 1 : τ 1 Γ ⊢ t 2 : τ 2 Γ ⊢ (t 1 , t 2 ) : τ 1 × τ 2

2012/3/19

2012/3/19

2012/3/19

2012/3/19

2012/3/19

2012/3/19

Core rules

We use this theorem to prove soundness. We consider the following predicate P (σ) that states that semantic relation σ

We want to apply the induction principle on P . Hence, we check its premises. FACT 8. The predicate P is monotonic. Besides, we have P (⊥ Σ ), where ⊥ Σ = λρ.λt.diverge, and, for all σ ∈ Σ, if P (σ) then P (F (σ)).

The first two propositions are immediate. Regarding the last proposition, we show P (F (σ)) by case on the derivation of assumption Γ ⊢ t : τ , applying the hypothesis P (σ) on immediate subderivations. All cases are easy.

Hence, we have P (lfp ↑F ): the semantics satisfies the soundness property. We are not quite done yet, however: the statement of Theorem 6 is not an immediate consequence of this result. Let us now conclude the proof. We assume Γ ⊢ t : τ . Let ρ ∈ X → V such that ρ : Γ. We now need to prove that t ρ : τ . Note that t ρ = {σ(t)(ρ) | σ ∈ lfp ↑F, ρ ∈ ρ}. Hence, it is sufficient to prove that for all σ ∈ lfp ↑F and all ρ ∈ ρ we have σ(t)(ρ) : τ . Let σ ∈ lfp ↑F and ρ ∈ ρ. We have ρ : Γ, hence ρ : Γ. On the other hand, P (lfp ↑F ), hence P (σ) holds for all σ ∈ lfp ↑F . This is exactly what we need to conclude.

Soundness is thus fairly easy to establish. We do not have to work directly with possibly infinite values nor infinite derivations. Instead, the proof is based on an inductive principle, which we are able to apply without proving any admissibility result, and that involves only finite values and derivations. Only a bit of fiddling is needed at the end to relate the soundness statement resulting from this principle with a direct statement of type soundness.

Considering Other Calculi

We discuss how our technique can be applied to specify the semantics of other calculi.

Deterministic Call-by-Value Calculi

We define the semantics of a call-by-value calculus. This is simpler as there are only finite values. We keep the same syntax for terms (Section 2.1). In a call-by-value settings, errors and divergence cannot occur nested inside a value.


Jérôme Vouillon
email: jerome.vouillon@pps.jussieu.fr

Reasoning on Assembly Code using Linear Logic

published or not. The documents may come

Introduction

We present a logic for reasoning on assembly code. The core of this logic is intuitionistic linear logic [START_REF] Girard | Linear logic and lazy computation[END_REF]. The multiplicative conjunction P ⊗ Q of linear logic corresponds to the separating conjunction P * Q of separation logic [START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]: it asserts that subformulas P and Q hold for disjoint parts of the heap. Likewise, the multiplicative unit 1 correspond to formula emp that asserts that the heap is empty. These constructions make it possible to reason in a modular way about the heap.

A major difference with separation logic is that the assertions we consider pure are the assertions that hold for empty portions of the heap, rather than assertions that are independent of the machine state. These assertions can be characterised using the of course modality of linear logic: a proposition P is pure when P !P . The contraction rule !P !P ⊗!P and the weakening rule !P 1 show that pure assertions can be duplicated or ignored, at will. Note that we use the separating conjunction ⊗ here, rather than the additive conjunction & (corresponding to conjunction ∧ in separation logic). We believe this is an advantage of this choice of pure assertions: one does not have to juggle with two distinct conjunction operators. In practice, we hardly use the additive conjunction.

In order to reason about machine states, we define a suitable model of the logic. The objects w of this model are basically pairs of a machine state and a domain (a set of locations). The domain specifies which part of the heap we are currently focused on. We define a Kripke semantics [START_REF] Kripke | Semantical considerations on modal logic[END_REF], hence we call these objects worlds. We write w P to states that a world w satisfies an assertion P . The model differs from usual models of program logics in that we consider whole machine states rather than heap portions. The use of a Kripke semantics allows to enforce that two equivalent machine states (that differs only on parts of the heap that are outside the set of locations in focus) cannot be distinguished by the logic: we define a preorder between states and the semantics of the logic should satisfy a persistence property: if w w and w P then w P . As the machine state is a component of our worlds, we can define a modality d to reason on program execution: the formula d P asserts that we can make progress from current state and that we reach after one step a state satisfying formula P . Hoare triples can be encoded using this modality: the assertion {P }c{Q} holds when:

∀ς.

([c ; ς] ⊗ P d ([ς] ⊗ Q)),
where assertion [ς] states that the current sequence of instructions is ς. (A slightly more complex interpretation of Hoare triples can also be adopted in order to validate the frame rule.)

The logic has greatest fixed points νx. F (x) for monotone operators F . This makes it possible to define safety as the greatest fixed point of operator d : we define safe syn = νx. d x. A program is safe if and only progress can be made while remaining safe. Besides, safe is the greatest post-fixed point of operator d , satisfying the rule below. P d P P safe Indeed, given some initial world w, suppose we can find a proposition P such that P d P . Then, we have a proof of progress and preservation: it is always possible to take another step, and after this step, the program still satisfies P . The greatest fixed point construction can also be used to enforce stronger program invariants: programs that satisfy νx. (P & d x) are safe programs with invariant P .

Finally, in order to deal with first class code pointers, we define an indexed model [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF][START_REF] Ahmed | A stratified semantics of general references embeddable in higher-order logic[END_REF][START_REF] Ahmed | Semantics of Types for Mutable State[END_REF][START_REF] Appel | A very modal model of a modern, major, general type system[END_REF]. With such a model, one can define fixed points for operators that are not monotone, but rather contractive. One also has a modality 2 that satisfies Gödel-Löb rule:

2P P P This rule can be read as an induction principle: 1 is the least prefixed point of 2 ( P stands for 1 P ). In indexed models, the relation is also used to enforce preservation properties: if a state satisfies a property, then we want the property to remain satisfied in the future if the part of the state we are considering remains unchanged.

To illustrate the logic, we show how it can be used to verify a destructive list-append function written in CPS. This example was initially suggested by Reynolds [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. We use the assembly code version of Ni and Shao [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF].

We first present the core logic (Section 2). A simple machine is specified for illustration purposes (Section 3). The logic is extended with rules for reasoning on the heap and on program execution (Section 4). We build an indexed model, which makes it possible to deal with first class code pointers (Section 5). Finally, we show how the logic can be used to prove program soundness (Section 6).

The Logic

Syntax and Rules

The syntax of the core logic is given in Figure 1. It is an extension of intuitionistic linear logic [START_REF] Girard | Linear logic and lazy computation[END_REF] with the greatest fixed Intuitionistic linear logic [START_REF] Bradfield | Modal mu-calculi[END_REF] (penultimate construction). The logic can be specified in a proof assistant using a shallow embedding. It is then very natural to lift arbitrary propositions from the meta-logic, such as equality predicates x = y, that do not involve the world (last construction). So far, we only have purely logical constructions. The logic will be extended in later sections with assertions and operators to deal specifically with programs. We list these additional constructions in Figure 2.

P P P Q Q R P R P ⊗ Q Q ⊗ P P ⊗ (Q ⊗ R) (P ⊗ Q) ⊗ R P P Q Q P ⊗ Q P ⊗ Q P ⊗ 1 P P ⊗ Q R P Q R P P ⊕ Q Q P ⊕ Q P R Q R P ⊕ Q R 0 P P P ⊗ 1 P Q R P ⊗ Q R P & Q P P & Q Q R P R Q R P & Q P !P P !P !!P P Q !P !Q !P ⊗!Q !(P ⊗ Q) 1 !1 !P !P ⊗!P !P 1 P Q x not free in P P ∀x:A. Q a ∈ A ∀x:A. P P [a/x] Q P x not free in P ∃x:A. Q P a ∈ A P [a/x] ∃x:A. P Greatest fixed points Q P [Q/x] Q
The greatest fixed point operator νx. P only makes sense for monotonic formulas P , that is, formulas such that P ρ;x →S ⊆ P ρ;x →S whenever S ⊆ S (where P ρ is the semantics of formula P , defined in Section 2.2). This can be enforced syntactically be demanding that all occurrences of variable x be in positive position in P , that is, one should always go through the right hand side of an implication an even number of times to reach each occurrence of variable x. When formalising the logic in a proof assistant, it may me more convenient to let the user write propositions νx. P for arbitrary propositions P and rather add a side-condition ensuring monotonicity to the unfolding rule νx. P P [νx. P/x].

The inference rules of the logic are given in Figure 3. We use symmetric sequents P Q rather than the asymmetric sequents P1, . . . , Pn Q of the traditional presentation of intuitionistic linear logic. Indeed, we find this presentation more convenient for mechanised proofs. Symmetric sequents define a preorder between propositions and we can use rewriting tactics that take advantage of this. The traditional presentation satisfies a cut elimination result, but this is not a property we are interested in. We write P for 1 P .

In linear logic, there are two choices to define pure propositions, that do not refer to the heap. One can either state that they are independent of the heap, or that they hold only on empty heap portions. The first choice is taken in separation logic. We prefer the second choice. Indeed, the pure proposition can then be characterised in a simple way, as the propositions P such that P !P . Besides, they can be combined with other propositions using the ⊗ operator. One can thus avoid the use of the & operator most of the time.

w w (1)

w w =⇒ w w =⇒ w w (2) w ≈ w1 • w2 =⇒ w ≈ w2 • w1 (3) w ≈ w1 • w =⇒ w ≈ w2 • w3 =⇒ ∃w , w ≈ w1 • w2 ∧ w ≈ w • w3 (4) ∃u, w ≈ u • w (5) u ≈ u • u (6) w ≈ u • w =⇒ w w (7) u w =⇒ w ∈ U (8) w ≈ w1 • w2 =⇒ w w =⇒ ∃w 1 , ∃w 2 , w ≈ w 1 • w 2 ∧ w1 w 1 ∧ w2 w 2 (9)

Models

To reason about machine states, we define models of the logic above. This can be done in a generic way by defining an abstract notion of separation algebras, as initiated by Calcagno, O'Hearn and Yang [START_REF] Calcagno | Local action and abstract separation logic[END_REF]. We use, though, a fairly different definition, in part because we define a Kripke model.

A separation algebra is a quadruple (W, , •, U ) composed of a set of worlds W , an accessibility relation

∈ W × W , a join relation • ∈ W × W × W
and a set of units U ⊆ W . This quadruple should satisfy the conditions listed in Figure 4. We write w for worlds in W and u for units in U . Free variables in these conditions should be considered universally quantified. The accessibility relation is used to define the Kripke semantics. It is a preorder, that is, it is reflexive (1) and transitive (2). The join relation and the set of units give us a model of linear logic. Following, Dockins, Hobor and Andrew [START_REF] Dockins | A fresh look at separation algebras and share accounting[END_REF], the join relation • is defined as a 3-place relation, rather than a partially defined binary function. We write w ≈ w1 • w2 for (w, w1, w2) ∈ • to suggest that world w is in some way a combination of worlds w1 and w2. The operation can be partial: there is no guarantee that there exists a world w such that w ≈ w1 • w2; the notation also emphasises that the operation may not be functional: there may be several such worlds w. The join relation is commutative (3) and associative (4). Each element has a unit (5). Each unit is a unit for itself (6). Finally, the accessibility and join relations interact in different ways. When a world is combined with a unit, one gets a related world (7). (This condition is used to validate rule P ⊗ 1 P .) The accessibility relation preserves units (8) and joins (9).

Given a separation algebra, we can define the semantic of the logic as a function _ _ that maps propositions P and environments ρ to so-called persistent sets of worlds (Figure 5). An environment is a sequence of bindings x → v. We say that a set of worlds W ⊆ W is persistent when it is upward closed with respect to the accessibility relation, that is, when for all worlds w ∈ W, if w w then w ∈ W. The following operator extracts the persistent worlds in a set of worlds W:

persist W {w ∈ W | ∀w ∈ W, w w ⇒ w ∈ W}.
Though we do not formalise it here, we assume that environments are suitably kinded. In particular, they should be such that the sets x ρ are indeed persistent. With this assumption, one can prove that the semantics is well-defined.

The semantics of most constructions is straightforward. There are two noteworthy points. The semantics of the linear implication P1 P2, must be explicitly restricted to persistent worlds.

Indeed, the usual definition {w | ∀w1∀w2, w2 ≈ w • w1 ⇒ w1 ∈ P1 ρ ⇒ w2 ∈ P2 ρ} is not persistent in general. This is standard for a Kripke semantics. We have the equality !P ρ = P & 1 ρ, which can be found in some other models of linear logic [START_REF] Lafont | The undecidability of second order multiplicative linear logic[END_REF]. In other words, a proposition is made pure by restricting it to units.

A consequence of persistency is that the logic cannot distinguish equivalent worlds, that is worlds w and w such that both w w and w w. This is crucial for us, as it will make it possible to reason locally on heap portions, while considering worlds that contain whole machine states.

The semantics of sequents is defined as follows:

P Q ρ P ρ ⊆ Q ρ.
One can show that all the rules of Figure 3 are sound with this definition.

Building Separation Algebras

It is convenient to build complex separation algebras by combining simpler algebras. We propose several such constructions.

Trivial algebra. We associate to a preordered set (W, ) the separation algebra (W, , •, U ) by taking U = W , and w ≈ w1 • w2 when w = w1 = w2. With this algebra, the two conjunctions ⊗ and & coincide, the assertion 1 holds for all worlds, and proposition !P is equivalent to proposition P .

Discrete algebra. We associate to a set W the trivial separation algebra associated to the preordered set (W, =). Algebra of subsets. Given a set A, we can define a separation algebra (W, , •, U ) where

• W = P(A),
• w w when w = w ,

• w ≈ w1 • w2 when w = w1 ∪ w2 and w1 ∩ w2 = ∅,

• U = {∅}.
Product of two algebras. Given two separation algebras (W1, 1 , •1, U1) and (W2, 2, •2, U2), we can define a product separation algebra (W, , •, U ) where

• W = W1 × W2, • (w1, w2) (w 1 , w 2 ) when w1 1 w 1 and w2 2 w 2 , • (w1, w2) ≈ (w 1 , w 2 ) •(w 1 , w 2 ) when w1 ≈ w 1 •1 w 1 and w2 ≈ w 2 •2 w 2 , • U = U1 × U2.

A Machine

In order to illustrate our logic, we specify a machine that interpret assembly code. The machine is that of Ni and Shao [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF], except that we leave memory management functions free and alloc out of the definition of the machine. Instead, we later assume that they can be implemented and give axioms to type them. We assume given a set of registers. We write r for registers and i for machine words. The syntax of machine code is given in Figure 6. An instruction sequence ς is a sequence of commands c followed by a jump. A machine state is a quadruple s = (µ, ρ, κ, ς) composed of a memory heap µ, a register file ρ, a code heap κ and an instruction sequence ς. A memory heap is a partial function from words to words. A register file is a total function from registers to words. A code heap is a partial function from words to instruction sequences.

The operational semantics is defined in two steps. The semantics of commands c is given in Figure 7. It specifies how the memory heap µ and the registers file ρ are modified by the command. Commands c ::= add r, r, r add registers addi r, r, i add register and word mov r, r move between registers movi r, i move word into register ld r, r(i) load st r(i), r store bgt r, r, i branch when greater than bgti r, i, i branch when greater than word Instruction sequences

1 ρ U P1 ⊗ P2 ρ {w ∈ W | ∃w1, w2 ∈ W, w ≈ w1 • w2 ∧ w1 ∈ P1 ρ ∧ w2 ∈ P2 ρ} P1 P2 ρ persist{w ∈ W | ∀w1, w2 ∈ W, w2 ≈ w • w1 ⇒ w1 ∈ P1 ρ ⇒ w2 ∈ P2 ρ} 0 ρ ∅ P1 ⊕ P2 ρ P1 ρ ∪ P2 ρ ρ W P1 & P2 ρ P1 ρ ∩ P2 ρ !P ρ P ρ ∩ U ∀x:A. P ρ a∈A P ρ;x →a ∃x:A. P ρ a∈A P ρ;x →a νx. P ρ {W ⊆ W |W persistent ∧ W ⊆ P ρ;x →W } x ρ ρ(x) p ρ U if p ρ holds ∅ otherwise
ς ::= c ; ς sequence jd i jump jmp r computed jump

Command c

Outcome (µ , ρ )

add r d , rs, rt (µ, ρ(r d ):=ρ(rs) + ρ(rt)) addi r d , rs, i (µ, ρ(r d ):=ρ(rs) + i) mov r d , rs (µ, ρ(r d ):=ρ(rs)) movi r d , i (µ, ρ(r d ):=i) ld r d , rs(i) (µ, ρ(r d ):=µ(ρ(rs) + i)) st r d (i), rs (µ(ρ(r d ) + i):=ρ(rs), ρ) Figure 7. Command semantics (µ, ρ) c → (µ , ρ ). Sequence ς Next state (µ , ρ , κ , ς ) jd l (µ, ρ, κ, κ(l)) jmp rs (µ, ρ, κ, κ(ρ(r))) bgt rs, rt, l ; ς (µ, ρ, κ, ς ) when ρ(rs) ≤ ρ(rt); (µ, ρ, κ, κ(l)) when ρ(rs) > ρ(rt) bgti rs, i, l ; ς (µ, ρ, κ, ς ) when ρ(rs) ≤ i; (µ, ρ, κ, κ(l)) when ρ(rs) > i c ; ς (µ , ρ , κ, ς ) when (µ, ρ) c → (µ , ρ ) Figure 8. Semantics (µ, ρ, κ, ς) → (µ , ρ , κ , ς ).
Given a partial function f , we write f (x):=v to denote, when f (x) is defined, the function that maps x to v and otherwise behaves as function f ; the expression f (x):=v is undefined when f (x) is undefined. Then, we define in Figure 8 the step relation → between a machine state and the next. Note that it is illegal to access or modify unallocated parts of the memory heap, or to jump to a non-existing code label. The execution gets stuck in all these cases.

Machine Logic

The Heap

We are going to define assertions for specifying the state of the machine. We handle in a uniform way the register file, the memory heap and the current instruction sequence. For that, we define locations l as either a register, a machine word, or the keyword pc.

l ::= r | i | pc
Then, to a machine state s = (µ, ρ, κ, ς), we associate an abstract heap h = heap(s), a partial dependent function from locations l to values v ∈ type(l), which maps a register r to its value ρ(r), a memory location i to its contents µ(i) if any, and the keyword pc to the current instruction sequence ς. We write code(s) for the code heap κ in machine state s. Note that the machine state s is isomorphic to the pair (code(s), heap(s)).

We define worlds w as pairs of a machine state s and a set of locations d. We define a separation algebra on worlds in a modular way by combining separation algebras on code heaps, on abstract heaps and on set of locations. For the sake of clarity, we state afterwards explicitely the resulting relations. Given a set of locations d, we define an equivalence relation between heaps:

h ≡ d h when ∀l ∈ d, h(l) = h(l ).
By the trivial algebra construction, this gives us a family of preordered separation algebra (H, ≡ d , •H , UH ) on heaps. On the other hand, we have a canonical separation algebra (D, =, •D, UD) on sets of locations. We take a kind of dependent product of these two separation algebras:

• W = H × D; • (h, d) (h , d ) when h ≡ d h and d = d ; • (h, d) ≈ (h1, d1) •(h1, d1) when h ≈ h1 •H h1 and d ≈ d1 •D d2; • U = UH × UD.
One can show that this defines a separation algebra. Finally, the separation algebra on worlds is the product of this algebra and of the discrete algebra on code heaps κ. This modular definition can be restated directly as follows. The accessibility relation is an equivalence relation. Two worlds (s1, d1) and (s2, d2) are equivalent when they share the same code (code(s1) = code(s2)), they are focused on the same set of locations (d1 = d2), and the corresponding heap portion is shared (heap(s1) ≡ d 1 heap(s2)). Two worlds (s1, d1) and (s2, d2) can be joined when they share the same machine state (s1 = s2) and are focused on disjoint set of locations (d1 ∩ d2 = ∅). The resulting world (s1, d1 ∪ d2) is composed of the common machine state and the union of the locations. Units are worlds (s, ∅) with an empty set of locations.

l → v ⊗ l → v 0 code(i, ς) !code(i, ς ) code(i, ς) ⊗ code(i, ς ) ς = ς
We now define two assertions to specify the heaps. The first one holds when we are focused on a single location l and that location contains value v. The second one states that code location i contains instruction sequence ς.

l → v ρ {w ∈ W | heap(w)(l) = v ∧ dom(w) = {l}} code(i, ς) ρ {u ∈ U | code(u)(i) = ς}
The inference rules corresponding to these two assertions are given in Figure 9. Disjoint heap portions cannot have a location l in common. The assertion code(i, ς) is pure. There cannot be two distinct instruction sequences at the same location. It is convenient to define abbreviations for some common uses of the first assertion. We write l → _ for ∃x:type(l). l → x and [ς] for pc → ς.

"Next" Modality and Safety

In order to reason on program execution, we define a modal operator d , which we call the "next" modality. The assertion d P holds when either the current execution has terminated successfully, or it is possible to perform a step and the world reached satisfies P .

We have already defined the step relation → for machine states. It can naturally be lifted to worlds: (s, d) → (s , d ) when s → s and d = d . We also define a success predicate that indicates whether the machine is in a successful termination state. We take success(w) = ∅ for the moment, as our machine does not have a notion of success. We will have to adopt a different definition later on when considering indexed models (Section 5). This predicate can also be useful with other machines, for instance when a value is reached during the evaluation of a lambda term.

The step relation and the success predicate should satisfy three conditions. The success predicate should be persistent (10). The step relation should be deterministic (11) and compatible with the accessibility relation (12). success(w) =⇒ w w =⇒ success(w ) (10)

w → w =⇒ w → w =⇒ w = w (11) w1 ≈ u • w2 =⇒ w2 → w 2 =⇒ ∃w 1 , ∃u , w 1 ≈ u • w 2 ∧ w1 → w 1 ∧ u u (12)
One can define the product of two separations algebras (W1, 1 , •1, U1) and (W2, 2, •2, U2) with associated step relations →1 and →2, and success predicates success1 and success2: we define (w1, w2) → (w 1 , w 2 ) when w1 →1 w 1 and w2 →1 w 2 and success(w1, w2) when either success1(w1) or success2(w2). The disjunction might look surprising, but it ensures that the pair (w1, w2) is safe when worlds w1 and w2 are safe. One can check that the relation and the predicate satisfy conditions (10), ( 11) and ( 12). This construction is used to build indexed models (Section 5).

P Q d P d Q d P & d Q d (P & Q) !P ⊗ d Q d (!P ⊗ Q)
Figure 10. Inference rule for "next" modality.

We then define the semantics of the "next" modality as follows:

d P ρ persist{w ∈ W | success(w) ∨ ∃w ∈ W, w → w ∧ w ∈ P ρ}.
Remark that we have to explicitly restrict ourselves to persistent worlds. This means that d P holds when we are able to perform a step and reach a world satisfying P not just starting from w but also from any world accessible from w (and in particular, from any equivalent world).

As the machine state is part of the world, it is straightforward to define the modality. That should also be possible with a standard presentation where the world only contains the constant part of the machine and a heap portion, by defining a Galois connection between set of worlds and set of machine states. But that would be much less natural.

There are three inference rules associated to the "next" modality (Figure 10). The first two are standard for modalities. The last one comes from conditions (10) and ( 12). It can be read as a constancy rule. If a pure property !P holds, then it will still holds after taking a step. In particular, if one assume that Q d R then one can derive

!P ⊗ Q d (!P ⊗ R). If one interpret Hoare triples {Q}c{R} as ∀ς. ([c ; ς] ⊗ Q d ([ς] ⊗ R)),
as in the introduction, this corresponds precisely to the constancy rule of Hoare logic:

{Q}c{R} {!P ⊗ Q}c{!P ⊗ R}
We consider that a machine state is safe when after any number of steps, either a success state is reached, or a further step can be performed. We therefore adopt the following definition of the safety predicate.

safe syn = νx. d x
This definition is actually a bit more restrictive than the standard definition of safety, due to our definition of the "next" modality: the machine state is allowed to change in an unobservable way between each step.

It is also possible to define stronger notions of safety, where an invariant property P remains satisfied at each step, by refining the above definition to:

safeP syn = νx. (P & d x).

Instruction Types

The instruction types can be specified as axioms, listed in Figure 11. The axioms corresponding to instructions add, addi and bgt have been omitted, as they are similar to other instructions. All these axioms are sound in our assembly code model. The type of commands c which do not change the flow of control follows the scheme:

[c ; ς] ⊗ R ⊗ P d ([ς] ⊗ R ⊗ Q). 5 2013/1/29 [ld r d , rs(i) ; ς] ⊗ P ⊗ rs → l ⊗ r d → _ ⊗ l + i → v d ([ς] ⊗ P ⊗ rs → l ⊗ r d → v ⊗ l + i → v) [ld r, r(i) ; ς] ⊗ P ⊗ r → l ⊗ l + i → v d ([ς] ⊗ P ⊗ r → v ⊗ l + i → v) [st r d (i), rs ; ς] ⊗ P ⊗ rs → v ⊗ r d → l ⊗ l + i → _ d ([ς] ⊗ P ⊗ rs → v ⊗ r d → l ⊗ l + i → v) [mov r d , rs ; ς] ⊗ P ⊗ rs → v ⊗ r d → _ d ([ς] ⊗ P ⊗ rs → v ⊗ r d → v) [movi r, i ; ς] ⊗ P ⊗ r → _ d ([ς] ⊗ P ⊗ r → i) [jmp r] ⊗ P ⊗ r → i ⊗ code(i, ς) d ([ς] ⊗ P ⊗ r → i) [jd i] ⊗ P ⊗ code(i, ς) d ([ς] ⊗ P ) [bgti r, i, l ; ς] ⊗ P ⊗ r → v ⊗ code(l, ς ) d (([ς] ⊗ P ⊗ r → v ⊗ v ≤ i ) ⊕ ([ς ] ⊗ P ⊗ r → v ⊗ v > i )) ∃∆. (([alloc r, n ; ς] ⊗ P ⊗ freespace ⊗ r → _) ⊕ ∆) d (∆ ⊕ ([ς] ⊗ P ⊗ freespace ⊗ ∃i. r → i ⊗ mem_block(i, n))) ∃∆. (([free r, n ; ς] ⊗ P ⊗ freespace ⊗ ∃i. r → i ⊗ mem_block(i, n)) ⊕ ∆) d (∆ ⊕ ([ς] ⊗ P ⊗ freespace ⊗ r → _)) Figure 11. Instruction types.
This corresponds to a refined interpretation of Hoare triple {P }c{Q}, which validate the frame rule:

{P }c{Q} {P ⊗ R}c{Q ⊗ R}
The types of jump instructions are similar, except that the initial and subsequent sequences of instruction are unrelated. For the conditional branch instruction bgti, the two possible following states are specified by a disjunction.

In order to type memory allocation and release, we will assume the existence of sequences of instructions alloc and free. The type of these operations is given in Figure 11. An abstract datastructure, specified by an assertion freespace contains available free space. These operations respectively extract memory blocks from this space, and put them back. We specify memory blocks at address i of length n using the following inductive definition:

mem_block(i, 0) = 1 mem_block(i, n + 1) = i → _ ⊗ mem_block(i + 1, n)
It takes several steps for these operations to terminate. An existentially quantified assertion ∆ specifies the machine state at each intermediate step.

An Example

We illustrate the logic by proving the soundness of a function that appends destructively the elements of a list to another list, in reversed order. A list is either the machine word 0, or a pointer to two contiguous memory locations. The first location contains the first element of the list, and the second contains a pointer to the remainder of the list.

list(nil, i) = i = 0 list(v :: ls, i) = ∃j. i = 0 ⊗ i → v ⊗ i + 1 → j ⊗ list(ls, j)
We consider the following rev_append function. It takes as arguments two lists x and y . If the list x is empty, then list y is returned.

Otherwise, the first cell of list x is put at the beginning of list y (by setting its tail to y ), and the function is called recursively with the tail z of the first list and the second list, now in variable x . This corresponds to the following piece of assembly code.

revapp: bgti r0, 0, else mov r0, r1 jd cont else: ld r2, r0(1) st r0(1), r1 mov r1, r0 mov r0, r2 jd revapp

The whole program can be described by an assertion Π of the following shape:

Π = code(i1, ς1) ⊗ . . . ⊗ code(in, ςn).
The type of the piece of assembly code above can be specified by defining an assertion:

Σ = ς ([ς] ⊗ Pς ).
where ς ranges over all subsequences of instructions and Pς specifies the precondition required for executing sequence ς. The entry point of the function is given precondition:

Prevapp =∃x. ∃y. ∃ls. ∃lt.

P ⊗ r0 → x ⊗ r1 → y ⊗ r2 → _ ⊗ list(ls, x) ⊗ list(lt, y) ⊗ l = rev ls ++ lt .
We assume given a specification l of the resulting list and an assertion P describing the part of the heap which is not modified by the function. The two lists are respectively in registers r0 and r1. Registers r2 is a temporary register that the function is allowed to use. We state that the returned list should be the first list reversed and appended to the second list. We have:

[ςrevapp ] ⊗ Prevapp Σ.

When the function terminates, it jumps to location cont . The precondition for the sequence of instructions at this location is the following:

Pcont = ∃y. P ⊗ r0 → y ⊗ r1 → _ ⊗ r2 → _ ⊗ list(l, y).
Register r0 contains the resulting list, which satisfies the specification given by l. The part of the heap specified by assertion P and the two registers r1 and r2 are available.

We further assume that the program continuation is well-typed, that is, that we can find a proposition ∆ such that:

[ςcont ] ⊗ Pcont ∆ Π ⊗ ∆ d ∆.
We can now perform the soundness proof. First, we prove for each sequence of instructions ς in the function above that:

Π ⊗ ([ς] ⊗ Pς ) d (Σ ⊕ ([ςcont ] ⊗ Pcont )),
that is, if we are executing this sequence, we can take a step and either we arrive in Σ or we exit the function. From this, we deduce:

Π ⊗ Σ d (Σ ⊕ ([ςcont ] ⊗ Pcont )).
Then, by combining this with the continuation soundness assumption, we get:

Π ⊗ (Σ ⊕ ∆) d (Σ ⊕ ∆).
Then, by constancy, we have:

Π ⊗ (Σ ⊕ ∆) d (Π ⊗ (Σ ⊕ ∆).
Finally, by definition of safety, we have:

Π ⊗ (Σ ⊕ ∆) safe.
In particular,

Π ⊗ [ςrevapp ] ⊗ Prevapp safe,
that is, if we are at the beginning of the function (the current sequence of instructions is ςrevapp ) and the heap satisfies the precondition Prevapp , the program will execute safely.

This soundness proof can be done entirely using the given inference rules: there is no need to unfold definitions at any point. We prove safety, but it would be possible to prove stronger invariants by making appropriate assumptions on Σ and ∆. This proof scheme applies when the control flow is rather static: loops, simple functions. On the other hand, to deal with first class functions, we need a last ingredient...

Indexed Models

We now present how to build indexed models. The idea is to consider truncated execution traces. This is implemented by associating to each world an integer that is decremented at each step. Then it becomes possible to reason by induction of the length of these traces. As described in [START_REF] Appel | A very modal model of a modern, major, general type system[END_REF], we do not have to deal explicitly with indices in the logic. Instead, the logic is extended with, first, a modal operator 2, called the "later" modality, and an associated induction principle, and second, a fixed point operator µx. P for so-called contractive operators.

A Modality

We first define indexed models in an abstract way. They are characterised by the existence of a relation ≺ that satisfies the following conditions. The relation is stable with respect to the accessibility relation (13). It is more precise than the accessibility relation ( 14). It preserves joins (15). The step relation is compatible with the re-lation (16). Last, the relation is well-founded (17).

w w =⇒ w ≺ w =⇒ w ≺ w (13) w ≺ w =⇒ w w (14) w ≈ w1 • w2 =⇒ w ≺ w =⇒ ∃w 1 , ∃w 2 , w ≈ w 1 • w 2 ∧ w1 ≺ w 1 ∧ w2 ≺ w 2 (15) w1 ≈ u • w2 =⇒ w2 → w 2 =⇒ ∃w 1 , ∃u , w 1 ≈ u • w 2 ∧ w1 → w 1 ∧ u ≺ u (16)
There is no infinite chain: w1 ≺ w1 ≺ . . . ≺ wn ≺ . . .

The relation ≺ is transitive, by ( 13) and ( 14). Conditions ( 16) and ( 14) imply the compatibility of the step relation with the accessibility relation ( 12). An assertion w ≺ w intuitively means that world w is a world strictly in the future with respect to world w (16) but otherwise satisfies the same properties ( 14).

We can define a simple separation algebra satisfying all these conditions by taking the trivial separation algebra corresponding to the preordered set (N, ≥) and adopting the following definitions:

• w → w when w = w + 1;

• success(w) when w = 0;

• w ≺ w when w > w .

Furthermore, given two separations algebras (W1, 1, •1, U1) and (W2, 2, •2, U2) with associated step relations and success predicates, the second also having a suitable relation ≺2, one can define a suitable relation ≺ on the product separation algebra (as defined in Section 4.2) by (w1, w2) ≺ (w 1 , w 2 ) when w1 w 1 and w2 ≺ w 2 .

Our model for assembly code can thus be turned into an indexed model by considering worlds W × N and lifting appropriately the definitions:

• (w, n) (w , n ) when w w and n ≥ n ;

• (w, n) ≈ (w1, n1) •(w2, n2) when w ≈ w1 • w2 and n = n1 = n2;

• the units are U × N;

• (w, n) → (w , n ) when w → w and n = n + 1;

• success(w, n) when n = 0;

• (w, n) ≺ (w , n ) when w w and n > n .

The semantics of the "later" modality associated to relation ≺ is defined in a standard way:

2P ρ {w ∈ W | ∀w ∈ W, w ≺ w ⇒ w ∈ P ρ}.
In particular, this is the same definition as in [START_REF] Appel | A very modal model of a modern, major, general type system[END_REF]. The set is indeed persistent, by condition (13).

The inference rules corresponding to this modality are listed in Figure 12. The first rule is standard for modalities. The second rule is a consequence of condition (14). Then, there are four distributivity rules. The last two rules are especially interesting. The penultimate rule is Gödel-Löb rule, adapted to linear logic by inserting the "of course" modality in the hypothesis. This is the induction principle corresponding to condition (17). The standard Gödel-Löb rule, given in the introduction, also holds, but is weaker. The following derived rule is useful when we have a pure invariant !P and want to prove that it implies so proposition Q:

!P ⊗!2Q Q !P Q .
The last rule is a stronger version of the constancy rule in Figure 10, consequence of condition (16). Basically, it is sufficient for prop-

P Q 2P 2Q P 2P 2P ⊗ 2Q 2(P ⊗ Q) 2P & 2Q 2(P & Q) ∀x:A. 2P 2∀x:A. P !2P 2!P !2P P 1 P !2P ⊗ d Q d (!P ⊗ Q)
µx. P P [µx. P/x] P [µx. P/x] µx. P Figure 12. Later modality and associated fixed point.

erty P to hold in the future for property P to hold after one step. We have the following derived rule, that nicely connects the modalities:

!2(P Q) d P d Q.
We use this rule to type code pointers.

Fixed Points

We are interested in having fixed points for so-called contractive propositions. We first define contractiveness. Then, we specify additional conditions on models neede to prove the existence of fixed points. Finally, we define a fixed point operator for contractive propositions.

In order to specify contractiveness, we first need to define the equivalence between two propositions:

P ⇔ Q syn = !(P Q)⊗!(Q P ).
Then, a proposition P is contractive with respect to a variable x when the following sequent holds:

∀y. ∀z. !2(y ⇔ z) (P [y/x] ⇔ P [z/x])
Intuitively, this holds when all occurences of variable y can be replaced by variable z in P [y/x], by doing it as many time as necessary ("of course" modality), but only in the future (2 modality).

A simple syntactic criterion that implies this property is that any occurrence of variable x in proposition P should be guarded by a 2 modality. In order to have fixed points, we need to make a further assumption on models. To each world w, one should be able to associate its level |w| ∈ N. Levels should satisfy three conditions: levels decrease when following relation (18); they decrease strictly when following relation ≺ (19); joining worlds preserves levels (20).

If w w , then |w| ≥ |w |. (18) If w ≺ w , then |w| > |w |. (19) If w ≈ w1 • w2, then |w| = |w1|. (20)
Then, to define the semantics of the fixed point construction µx. P in some environment ρ, we iteratively define a sequence Wn of sets of worlds:

W0 = ∅ Wn+1 = P ρ;x →Wn
Finally, we define:

µx. P ρ = {w ∈ W | w ∈ W |w|+1 }
When P is contractive, this defines a persistent set of worlds that validates fixed point folding and unfolding (last two rules in Figure 12). We do not give a reasoning principle for this fixed point operator. The existence of a fixed point is enough for our needs. The contractiveness property can either be a well-formedness condition of the syntax of propositions, or a side-condition of these rules. In the second case, the definition above does not yield a persistent set of worlds in general. This should be forced by using the persist operator.

Using the Logic

Typing Programs

We follow the same approach for specifying assembly code as Ni and Shao [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF] The formalisation and proof techniques follows the work of Tan and Appel [START_REF] Tan | A Compositional Logic for Control Flow and its Application to Foundational Proof-Carrying Code[END_REF][START_REF] Tan | A compositional logic for control flow[END_REF][START_REF] Appel | A very modal model of a modern, major, general type system[END_REF] We define typing judgements Γ |= {P } ς for instruction sequences, Γ |= κ : Γ for code heaps, and Γ |= {P } s for whole programs. The code is typed in a modular way. A code heap specification Γ = i1 : P1 ; . . . ; in : Pn defines the interface of a code heap. It states that the piece of code at location ij has precondition Pj. We adopt the following semantics for specifications:

Γ syn = ∃ς1. . . . ∃ςn. code(i1, ς1) ⊗ . . . ⊗ code(in, ςn)⊗ !2((([ς1] ⊗ P1) ⊕ . . . ⊕ ([ςn] ⊗ Pn)) safe)
That is, each location ij contains an instruction sequence ςj, and whenever (! modality) in the future (2 modality) we reach one of these sequences and the associated precondition Pj is satisfied, the program executes safely thereafter. The semantics of the typing judgment for instruction sequences Γ |= {P } ς is:

Γ |= {P } ς syn = Γ ([ς] ⊗ P ) safe,
that is, if the remainder of the program follows specification Γ, when the program reaches the code sequence ς and precondition P is satisfied, it executes safely thereafter. The semantics of the typing judgment for code heaps Γ |= κ : Γ is defined, assuming dom(κ) = dom(Γ ), by:

Γ |= κ : Γ syn = Γ Σ κ,Γ safe where Σ κ,Γ syn = i∈dom(κ) ([κ(i)] ⊗ Γ (i)),
that is, if the remainder of the program follows specification Γ, when the program reaches any of the code sequence κ(i) and the corresponding precondition Γ (i) is satisfied, it executes safely thereafter.

Finally, the semantics of the typing judgment for machine states Γ |= {P } s is just a soundness statement: ∃d, ∀n ∈ N, (((µ, ρ, κ, ς), d), n) safe.

The rules for these judgements are given in Figure 13. They can be easily proved in the logic. Regarding instruction sequence judgements, there is a consequence rule, elimination rules for existentials and meta propositions, a rule for single command executions, a rule to extract a code pointer from the specification Γ, and three rules for flow control instructions. We have omitted rules for alloc and free. Code heaps are typed in a modular way: there is one rule for typing a heap composed of a single instruction sequence, and a rule for combining code heaps. In this second rule, import interfaces Γ1 and Γ2 are allowed to overlap. Finally, the last rule states the soundess of a machine state.

The semantics of code pointers correspond to a specification with a single location: added to the precondition. To type jump instructions, we rely on rule !2(P Q)

codeptr(i, P ) syn = ∃ς. (code(i, ς)⊗!2(([ς] ⊗ P ) safe)). P Q Γ |= {Q} ς Γ |= {P } ς Γ |= {P } ς x not free in Γ Γ |= {∃x:A. P } ς p implies Γ |= {P } ς Γ |= {P ⊗ p } ς Γ |= {Q} ς [ς] ⊗ P d ([ς ] ⊗ Q) Γ |= {P } ς (i : Q) ∈ Γ Γ |= {P ⊗ codeptr(i, Q)} ς Γ |= {P } ς P ⊗ r → i ⊗ codeptr(i, Q) Q Γ |= {P ⊗ r → i ⊗ codeptr(i, Q)} jmp r (i : P ) ∈ Γ Γ |= {P } jd i (j : Q) ∈ Γ P ⊗ r → v ⊗ v > i Q Γ |= {P ⊗ r → v ⊗ v ≤ i } ς Γ |= {P ⊗ r → v} bgti r, i, j ; ς Γ |= {P } ς Γ |= (i : ς) : (i : P ) Γ1 |= κ1 : Γ 1 Γ2 |= κ2 : Γ 2 Γ1 ; Γ2 |= κ1 ; κ2 : Γ 1 ; Γ 2 Γ |= κ : Γ Γ |= {P } ς ∃d,
d P d Q. Indeed, by instantiating P and Q, we get:

!2([ς] ⊗ P ) safe) d ([ς] ⊗ P ) safe,
that is, if we have a code pointer to some instruction sequence ς with precondition P , the program jumps to the sequence ς (which takes one step), and the precondition is satisfied, then the program executes safely thereafter. We explain the last rule of Figure 13. The specification of the code heap of a state (µ, ρ, κ, ς) is:

Πκ syn = i∈dom(κ) code(i, κ(i)).
From the two first premises,

Γ (Σκ,Γ ⊕ ([ς] ⊗ P )) safe.
We write Σ = Σκ,Γ ⊕ ([ς] ⊗ P ). We can derive Πκ⊗!2(Σ safe) Γ .

Hence, Πκ⊗!2(Σ safe) Σ safe.

By Gödel-Löb rule, we get Πκ Σ safe.

In particular, the program entry point is safe if its precondition holds:

Πκ ([ς] ⊗ P ) safe. The third premise tell us that there exists a set of locations d and a natural number n such that:

(((µ, ρ, κ, ς), d), n) P.
We also have:

(((µ, ρ, κ, ς), d), n) Πκ (((µ, ρ, κ, ς), d), n) [ς].
By combining these, we finally get soudness:

(((µ, ρ, κ, ς), d), n) safe.

An Example

We have proved the soundness of the destructive list append function written in CPS from Ni and Shao [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF] given in Figure 14. This function corresponds to the following piece of code due to Reynolds [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. The structure of our proof follows closely the proof by Ni and Shao. It is about 250 lines of Coq, compared to about 1700 lines for their proof. The reason is that we are able to work entirely in the logic rather that expanding definitions and reasoning at a lower level. We do not explain the proof here. We refer you to [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF] for details. However, we find it interesting to give the append function precondition (Figure 15), as this gives an idea of what the logic can express.

Function append allocates and frees memory blocks and thus must have access to freespace. Registers r0 and r1 contains respectively the two lists x and y, which satisfy respectively some specifications ls and lt. Register r2 contains a pointer rk to the continuation closure. We assert that the continuation will be applied to the concatenation of the two lists (last assertion).

The continuation closure is a pair of two memory locations at address i. The first location contains a pointer cnt to the code of the continuation. The second contains a pointer env to the continuation environment. The environment pointer should satisfy a predicate envtype. Assertion envtype(env) typically specify the part of the memory heap that contains the environment. The code pointer assertion states that the continuation precondition should be satisfied in order to jump to the code at location cnt.

The precondition of the continuation states that it expects a pointer env to the environment in registers r0 and the resulting list z in register r1. The resulting list should satisfy the specification given by ls.

Proving Preservation Results

In Section 6.1, we have presented a way to prove program soundness. We show here how one can prove a stronger result: that a whole program satisfies some invariant I such that Π ⊗ I d I, where Π specify that the program is loaded into memory. This gives us a partial-correctness result: invariant I remains satisfied after any number of step.

The idea is to replace safe by some indeterminate invariant I in the semantics of specification Γ and code pointers:

codeptr I (i, P ) syn = ∃ς. (code(i, ς)⊗!2(([ς] ⊗ P ) I))
The semantics of the typing judgment for instruction sequences

Γ |= {P } ς becomes Γ |= {P } ς syn = Γ ∃∆. !2(∆(I) I) (([ς] ⊗ P ) ⊕ ∆(I)) d I
The existentially quantified predicate ∆ stands for the type of all subsequences of instructions in sequence ς: we assume that the invariant is satisfied whenever we arrive in the future to any instruction in the sequence with the associated precondition satisfied; then we prove that if we are on any of these instruction and the corresponding precondition is satisfied, then we can take a step and then satisfy the invariant.

By typing the whole program, one finally get an equation of the shape:

Π⊗!2(F (I) I) F (I)

d I
where F specifies the preconditions of all subsequences of instructions occurring in the program. There are two ways to continue from here. The first solution is to take I = safe. Then, as d safe safe, we have:

Π⊗!2(F (safe) safe) F (safe) safe.

From this, we can conclude as in Section 6.1. The other solution is to take I = µx. F (x). Operator F should indeed be contractive, as I only occurs inside a 2 modality in specifications and code pointers. Then, the hypothesis 2(F (I) I) always holds, and we get:

Π F (I) d I.
As I is a fixed point of F , this can be rewritten into:

Π ⊗ I d I,
that is, I is an invariant of the program.

From this, we can prove soundness. As Π is pure, we can derive by constancy:

Π ⊗ I d (Π ⊗ I).
Finally, as safe is the greatest fixed point of d , Π ⊗ I safe.

Related Work

Separation logic [START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] is the main starting point for this work. We use the same constructions (singleton heap, empty heap and separating conjunctions) to reason about the heap. However, as Spalding and Jia [START_REF] Spalding | Asserting memory shape using linear logic[END_REF], we use intuitionistic linear logic rather than the logic of bunched implications and we characterise pure propositions using the "of course" modality .

The assembly code machine and our main example are taken from the work by Ni and Shao on certifying programs with embedded code pointers [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF]. We are able to use similar judgments, such as judgment Γ |= {P } ς, to reason on programs. However, our judgments are syntactic sugar for logical assertions, rather than primitive constructs. Another difference if that we give an axiomatisation of our logic, which makes it possible to prove the soundness of programs without having to unfold any definition. This results in much smaller proofs, even with hardly any automation.

The 2 modality and the associated fixed point operator were introduced by Appel, Melliès, Richards and Vouillon [START_REF] Appel | A very modal model of a modern, major, general type system[END_REF].

We additionally have a d modality to reason in a direct way on program execution. We similarly start from a logic with very atomic constructions from which we define high-level constructions as syntactic sugar. Our models are simpler as we do not deal with memory references.

Following Calcagno, O'Hearn and Yang [START_REF] Calcagno | Local action and abstract separation logic[END_REF], we define separation algebras to specify in an abstract way families of models for our logic. Our notion of separation algebra is significantly different as, first, we do not attempt to reason on concurrent programs and second, we adopt a Kripke semantics. Dockins, Hobor and Appel [START_REF] Dockins | A fresh look at separation algebras and share accounting[END_REF][START_REF] Hobor | A logical mix of approximation and separation[END_REF] have extended separation algebras to deal with indexed models. They also propose modular constructions for these separation algebras. Overall, we put weaker conditions on algebras.

Conclusion and Future Work

We have presented a logic, and associated models, for reasoning on assembly code. A novelty is the "next" modality d that makes it possible to reason on program execution. Our definitions are modular and flexible. For instance, indexing can be leaved out. Given a machine whose state can be split into a heap and a constant part, it is straightforward to define a corresponding separation algebra (following Section 4.1).

Most of the results in this paper have been machine-checked in Coq. Modularity is currently achieved through the module system of Coq, which shows its limits. We plan to adopt the packaging techniques of Garillot, Gonthier, Mahboubi and Rideau [START_REF] Garillot | Packaging mathematical structures[END_REF].

Figure 4 .

 4 Figure 4. Properties of separation algebras.

Figure 5 .

 5 Figure 5. Semantics of the logic.

Figure 6 .

 6 Figure 6. Syntax of machine code.

Figure 9 .

 9 Figure 9. Heap assertions.

  let rec revapp (x ,y ) = if x = nil then y else let z = [x +1] in [x +1] := y ; revapp (z ,x )

Figure 14 .Figure 15 .

 1415 Figure 14. Destructive list append function in CPS.

  let rec append(x,y,r) = if x = nil then r(y) else let a = [x] and b = [x+1] and k(z) = let w = cons(a,z) in r(w) in append(b,y,k)

  Figure 13. Derived rules for judgments Γ |= {P } ς, Γ |= κ : Γ and Γ |= {P } s.

		∀n ∈ N, (((µ, ρ, κ, ς), d), n) P
		Γ |= {P }(µ, ρ, κ, ς)
	append: bgti r0, 0, else	else: alloc r3 2	k: ld r2, r0(0)
	ld r31, r2(0)	st r3(0), r0	ld r3, r0(1)
	ld r0, r2(1)	st r3(1), r2	free r0, 2
	free r2, 2	ld r0, r0(1)	st r2(1), r1
	jmp r31	alloc r2, 2	mov r1, r2
		st r2(1) r3	ld r31, r3(0)
		movi r3, k	ld r0, r3(1)
		st r2(0), r3	free r3, 2
		jd append	jmp r31

2013/1/29

2013/1/29

2013/1/29

2013/1/29

2013/1/29

Note that when (i : P ) ∈ Γ, we have Γ codeptr(i, P ). This is how a code pointer can be extracted from the specification and 82013/1/29

2013/1/29

2013/1/29

Though we have only very simple tactics so far, proofs are reasonably short. Still, more powerful tactics, for instance following the recent work by Gonthier, Ziliani, Nanevski and Dreyer [START_REF] Gonthier | How to make ad hoc proof automation less ad hoc[END_REF], would further help.