Ran Chen

Martin Clochard

Claude Marché

A Formal Proof of a Unix Path Resolution Algorithm *

Keywords: Formal Specification, Deductive Verification, Program Verifier Why3, Unix file system, Path resolution

In the context of file systems like those of Unix, path resolution is the operation that given a character string denoting an access path, determines the target object (file, directory, etc.) designated by this path. This operation is not trivial because of the presence of symbolic links. Indeed, the presence of such links may induce infinite loops. In this report we consider a path resolution algorithm that always terminate. We propose a formal specification of path resolution and we formally prove that our algorithm terminates on any input, and is correct and complete.

The Portable Operating System Interface (POSIX) is an IEEE family of standards [5] that defines standard operating system interface and environment. Its goal is to provide software compatibility between variants of Unix and other operating systems.

In the part of the POSIX standard concerning file systems, path resolution, or more precisely pathname resolution 1 is the operation that given a pathname determines the target object (file, directory, etc.) it denotes, if any. A pathname is a character string that is made of a sequence of filenames separated by the special character "/". A pathname is absolute if it starts with "/" and relative otherwise. A filename, also called pathname component in POSIX, is a non-empty sequence of characters, containing neither "/" nor the NUL character (of ASCII code 0). The filenames "." and ".." have special meanings, respectively the current and the parent directory. When the given pathname is absolute, pathname resolution starts from the root directory, otherwise it starts from the current directory of the process that attempts resolution.

The process of pathname resolution is non trivial because of the presence of symbolic links. A symbolic link is some kind of entry allowed in directories whose contents is a pathname. Resolving a pathname containing symbolic links somehow amounts to "recursively" resolve the pathnames associated to the links. Figure 1 presents an excerpt of the real file system tree that appear in a computer with a typical Debian installation. Notice the relative symbolic link /usr/bin/latex that points to pdftex, that is /usr/bin/pdftex as an absolute path ; the absolute symbolic link /usr/bin/emacs that points to /etc/alternatives/emacs which is itself a symbolic link to /usr/bin/emacs24-x.

Notice that depending on the context, a pathname under consideration does not need to be resolved completely, e.g. when performing a mkdir command, only the prefix without the last component of the pathname must be resolved. In this report, we only consider the problem of complete resolution of a Figure 1: Excerpt of the file system tree typically found in a Debian installation. Black nodes denote directories, white nodes denote regular files, and gray nodes denote symbolic links.

pathname, thus resolution fails if the given path contains a non-existent component (e.g. when resolving /usr/bin/absent on the tree of figure 1). In practice, path resolution also fails if it attempts to access to a directory with insufficient permissions. Permissions do not pose any particular problem for a path resolution algorithm and we ignore them in this report.

The main difficulty comes from the presence of symbolic links: because of such links, the file system tree becomes some kind of a graph in which links may define cycles. A simple example would be a symbolic link that points to itself, or, on Figure 1, if the link /etc/alternatives/emacs was pointing to /usr/bin/emacs instead of /usr/bin/emacs24-x. In the presence of such cycles, the pathname resolution algorithm must be careful not to go into an infinite loop. This is the issue we address in this report. This issue is solved in practice by setting an arbitrary bound on the number of symbolic links that can be traversed during a given path resolution, in POSIX this number is required to be at least 32 2 . It means that the typical algorithm for path resolution implemented in a real OS is an incomplete one. The question of the existence of a terminating and complete algorithm is not open, such algorithms are known 3 but are not used in practice, probably because they require extra memory, and the limit of 32 is enough in practice.

The CoLiS project 4 aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts, in particular those that are used in software installation. During this project, we face the need for a formal specification of pathname resolution. We report here on the design of this formal specification and how it is used to formally prove a pathname resolution algorithm. The formalization is done using the Why3 program verifier [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF]. In Section 1 we first present how we model file systems. We then present our resolution algorithm in Section 2. We describe our formal specification in Section 3 and show how the algorithm is proved in Section 4. Section 5 presents some related work and perspectives.

The annotated code for this work is available at URL http://toccata.lri.fr/gallery/path _ 1 Simplified Model of the file system

For our development, we formalize the file system in some abstract way. Regular files play no role in the path resolution algorithm so we just ignore them. The file system is a directed graph where the vertices are directories, called dirnodes. Edges of this graph are labeled by file names. An edge from a dirnode d 1 to a dirnode d 2 labeled by f means that f is a name that belongs to directory d 1 and that points to the sub-directory d 2 .

Pathnames

A pathname (as defined by POSIX) is a sequence of file names, separated by slash characters, used to identify a file or a directory in the file system. In a pathname, "." and ".." have a special meaning, respectively to denote the current directory and the parent directory. We formalize them abstractly as follows.

type filename type pathcomponent = Down filename | Up | Here type path = list pathcomponent

The type for filenames is abstract, since for our purpose we don't need to know anything about it. A path is a list of path components, which can be either Up to denote "..", Here to denote ".", or (Down f ) to denote a normal filename f .

The file system

The graph formed by the file system is formalized using these declarations: The constant root denotes the root directory of the file system. A path resolution may start from root or from current working directory. The function lookup is a total function which looks up a filename of a directory and returns the corresponding child. A child could be four cases, namely Absent denoting 'There is no such directory', (Dir d) denoting that successfully found a sub-directory d, (AbsLink p) denoting it is a symbolic link which stores an absolute path p, and (RelLink p) denoting it is a relative symbolic link which stores an relative path. A useful simple function we need is parent to get the parent directory of some dirnode. We axiomatize the function with two axioms.The first axiom indicates that the parent directory of root is root. The second axiom indicates that if we can lookup a filename f from directory d 1 to directory d 2 , then d 1 is the parent directory of d 2 . Thus, The parent function implies the graph is almost a tree in which there is no two different father directories of one directory node. Notice that for the moment we do not require the graph is finite.

Example 1 Considering the structure of Figure 1, we have

RR n°8987

lookup root "usr" = Dir d1 lookup d1 "bin" = Dir d2 lookup d2 "emacs" = AbsLink "/etc/alternatives/emacs" lookup d2 "latex" = RelLink "pdftex" lookup d2 "foo" = Absent

Resolution Algorithms

We can give a naive path resolution algorithm now. We start to resolve a path p from some directory d.

We match the path with several cases.

• If it's an empty path, then we stay in directory d.

• If the path starts with ".." , then we go to the parent directory of d and resolve the rest of the path.

• If it starts with ".", then we stay in the current directory d and resolve the rest of the path.

• If it starts with a normal file name, then we lookup the filename in directory d:

-If it is absent, then path p resolve to nowhere. We raise an error then.

-If it is a directory d . then we resolve the remaining path from d .

-If it denotes an absolute link ps, then we recursively resolve the path ps from root to some directory d , and then resolve the remaining path of p from d . The case of a relative link is similar, except we resolve ps from current directory d.

Here is the corresponding Why3 code for this naive algorithm. We should notice that the naive algorithm above doesn't test a loop in the path. Because of the existing of the symbolic links, we may have a loop in the path which results the path cannot be resolved to anywhere and keep looping forever. Fig 2 presents some examples of the loops. /a/e is a path with a loop in it since there is a symbolic link points to itself. /c/f is also a path with a loop in it because there are two symbolic links in the path and they point to each other. From these two examples, we may suggest that we can detect a loop in the path by record the symbolic links we meet in it. But here we present another example /d/d/d/d/c in which we meet the same symbolic link (root, d) several times. But this path can be resolved successfully. From the third example above, we can now present a good algorithm to resolve a path with an 'active' parameter to detect a loop in the path. 'active' is a set of pairs made of a directory node and a file name that resolves to a symbolic link at that directory. Every time we meet a symbolic link (d, f ) in the path, we will detect the repetition of symbolic links when we resolve the link itself. Here is the Why3 code of the algorithm. The resolving function aux _ resolve keeps looking up the path component recursively. Every time we meet a symbolic link in the path, we start to record the link. Then we will resolve the link itself, and keep record the links we meet during the resolving. Once we meet a same link again, we know that the link is looping and the path could not be resolved.

Formal Specification of Path Resolution

Our goal is now to express the informal property "from some directory d 1 we can resolve a path p to some other directory d 2 ". Because resolution does not always succeed, we cannot formalize this property as a logical function that, from d 1 and p, returns d 2 . This is because in the logic of Why3, all logical functions are total. Instead, we formalize this property as a ternary predicate, that we denote as d 1 , p d 2 . We define this predicate inductively, that is we define it as the smallest predicate satisfying the rules below.

d, ε d (ResolveNil)

d 1 (f ) = Dir d 2 d 2 , p d 3 d 1 , f /p d 3 (ResolveDir) d 1 (f ) = AbsLink ps root, ps d 2 d 2 , p d 3 d 1 , f /p d 3 (ResolveAbsLink) d 1 (f ) = RelLink ps d 1 , ps d 2 d 2 , p d 3 d 1 , f /p d 3 (ResolveRelLink)
resolve _ to d1 p d2 → resolve _ to d1 (Cons Here p) d2

Example 2 Here are some examples of valid resolution. First we pretend that resolving the path /usr/bin from root results in d 2 , that is root, usr/bin d 2 . The proof of this fact is

root(usr) = d 1 d 1 (bin) = d 2 d 2 , ε d 2 d 1 , bin d 2 root, usr/bin d 2
Now from d 2 we pretend that resolving the path ./latex to d 3 which is

d 2 , ./latex d 3 . The proof is d 2 (latex) = RelLink(pdftex) d 2 (pdftex) = d 3 d 3 , ε d 3 d 2 , pdftex d 3 d 3 , ε d 3 d 2 , latex d 3 d 2 , ./latex d 3
Suppose the parent directory of some directory node d 1 is root, and we pretend that resolving the path ../etc/alternatives/emacs from d 1 results in d 4 .

The proof of d 1 , ../etc/alternatives/emacs d 4 is

parent d 1 = root root(etc) = d 2 d 2 (alternatives) = d 3 Π 1 d 2 , alternatives/emacs d 4
root, etc/alternatives/emacs

d 4 d 1 , ../etc/alternatives/emacs d 4
where Π 1 is the proof

d 3 (emacs) = AbsLink(/usr/bin/emacs24-x) Π 2 d 4 , ε d 4 d 3 , emacs d 4
where Π 2 is the proof

root(usr) = d 5 d 5 (bin) = d 6 d 6 (emacs24-x) = d 4 d 4 , ε d 4 d 6 , emacs24-x d 4 d 5 , bin/emacs24-x d 4
root, usr/bin/emacs24-x d 4

Comparison with POSIX specification of resolution

If we compare our formal specification of path resolution to the informal one of POSIX5 , we can notice a slight divergence, lying on the way symbolic links must be handled: "If a symbolic link is encountered during pathname resolution, [...] the system shall prefix the remaining pathname, if any, with the contents of the symbolic link". On other words, in our rules ResolveAbsLink and ResolveRelLink, we should not have two premises but only one to resolve the concatenation of the link and the remaining pathname.

Our definition is indeed simpler because it does not use concatenation, and in particular it will make the proofs easier. To show that there is no difference with POSIX informal specification, we now define another predicate closer to POSIX specification and prove the equivalence between this specification and the one above. The predicate d 1 , p P OSIX d 2 can be presented as an inductive predicate in Why3 code below. We want to prove that the predicate above is equivalent to the first one, as stated by the following theorem. To prove this theorem we have to state a few auxiliary lemmas. The first lemmas below are related to the first resolution predicate. We use the operator ++ to denote the concatenation of paths.

Lemma 4 for all dirnodes d 1 , d 2 , d 3 and paths p, q, if d 1 , p d 2 and d 2 , q d 3 then d 1 , p ++ q d 3 .
The proof is done by induction on the hypothesis d 1 , p 1 d 2 . Within Why3 such a lemma can be stated directly as follows.

lemma resolve _ to _ append : forall d1 d2 d3 p q. resolve _ to d1 p d2 → resolve _ to d2 q d3 → resolve _ to d1 (p ++ q) d3 and the proof is done using the Why3 transformation induction _ pr and the 6 resulting goals are proved by automatic provers. From now on we do not mention the Why3 code of our lemmas. See appendix for the detailed code and the detailed proofs.

We state the converse property using two lemmas. We denote by operator :: the list cons.

Lemma 5 for all dirnodes d 1 , d The proof is done by induction on hypothesis d 1 , p 1

P OSIX d 2 .
Finally, the proof of Theorem 3 is done by considering each direction of the equivalence separately, and reasoning by induction on the predicate in hypothesis in both cases.

Inria

Resolution Indexed with Explicit Height

For the purpose the proving our resolution algorithm, we will need to explicitly refer to the height of the proof of some judgment d 1 , p d 2 . For that purpose we introduce another predicate with an extra argument corresponding to that height. Moreover, we want to express that some path p can not be resolved, we express that by saying that it can be resolved with an infinite height. We denote d 1 , p d 2 , h to mean "resolving path p from node d 1 results in node d 2 with a proof of height h", and d 1 , p ∞ means we cannot resolve path p from node d 1 . That predicate is also defined inductively with the rules below.

∀d 1 . ¬(d, p d 1 ) d, p ∞ (ResolveHeightAbsent) d, ε d, 0 (ResolveHeightNil)

Technical Lemmas

We need some technical lemmas to prove the algorithm. First, we need to state that proof height of a resolved path is greater or equal than 0. The proof can be done by induction on the hypothesis d 1 , p d 2 , and looking at all the 7 cases of rules applied to establish d 1 , p d 2 . That lemma can be turned into Why3 and as expected, the proof is done using the transformation induction _ pr. The 7 resulting goals are proved automatically by Alt-Ergo.

A second lemma works the other way around: every time we resolve a path to some directory we can always resolve with some height. The proof proceeds by induction also. The proof in Why3 has 6 cases and all of them are proved automatically by Alt-Ergo and CVC4.

Determinism of Resolution

An important property we need is the uniqueness of the result of resolution, if it exists. The following lemma states this property. The last lemma is saying that we can always find a proof height (possibly infinite) for any path resolving from any directory. Up to now, we did not specify that the filesystem has finitely many nodes. Potentially, resolution could not terminate even if there is no loop: imagine a link l 1 pointing to another link l 2 itself pointing to l 3 etc.

To prove termination, we thus need to add more constraints in our model of the filesystem, as follows. In other words, there exists some finite set alllinks of pairs (dirnode,filename) such that all links in the file system belong to alllinks.

To achieve the proof of termination, we just need to state a variant, that is a quantity that decreases at each recursive call. A proper variant in this case is as follows: either the active set increases, or it remains unchanged and the length of the path p decreases. Instead of saying that the active set increases, we say that the complement set alllinksactive decreases. This requires to add a precondition stating that the active set is always a subset of alllinks. Such a precondition acts as an invariant maintained for all the recursive calls. From the variant above, given as a pair of an integer and a list, Why3 implicitly considers that the associated well-founded ordering is the lexicographic composition of the natural ordering on non-negative integers and the sub-list ordering on lists. The proof of termination is then obtained by automatic provers.

Correctness

The correctness of the algorithm is stated using the following post-condition. The proof works very easily, because the recursive calls of the algorithm recursively construct the needed premises to build the inductive proof of d, p result . Notice that for this proof it is important to use our first variant of the resolution predicate, and not the POSIX one.

Completeness

The completeness is stated using the following post-condition stated when the function raise the exception The hard part of the proof is to prove this completeness property. We need to add more invariants on the active set, again under the form of preconditions to be satisfied by the recursive calls.

The invariants on the active set are as follows: for all (d 1 , f ) ∈ active and for any ps, if

d 1 (f ) = AbsLink ps then • ∀d 2 . root, ps d 2 → ∃d . d, p d • ∀d 2 , h 1 , d , h. root, ps d 2 , h 1 → d, p d , h → h ≤ h 1
Both assertions say something about an arbitrary pair (d 1 , f ) in the active set. If the filename f in dirnode d 1 denotes an absolute link to some path ps, then:

• The first assertion states that if ps is resolvable from root (to some d 2 ) then p is resolvable from d (to some d ).

• The second assertion states that if ps is resolvable from root with some finite height h 1 and if p is resolvable from d with some finite height h then h is smaller than h 1 .

In other words, these two assertions together mean that if you resolve any pair in the active set, then the input path p is resolvable also, with a proof that as a smaller height. This is the key property that allows us to prevent cycles in the proofs of path resolution, as we will see below. Still another way to express this is to say that the resolution of the current path p is a part of the resolution of all the paths that appear in the active set.

We also need two similar invariants about relative links: for all (d 1 , f ) ∈ active and for any ps, if

d 1 (f ) = RelLink ps then • ∀d 2 . d 1 , ps d 2 → ∃d .d, p d • ∀d 2 , h 1 , d , h. d 1 , ps d 2 , h 1 → d, p d , h → h ≤ h 1
The code is thus annotated as follows. The assertion in the first line of the body of aux _ resolve is added to help the provers to instantiate the lemma 13.

The proof of the exceptional post-condition must be done in the case of each occurrence of raise Error in the code. The first case, when the considered filename does not exists, is easy: no rules for construct a proof of resolution can apply. The two other cases concern the symbolic links. Let's consider the first case, for an absolute link (the other case is similar). By contradiction, if we assume that it is possible to resolve d, p to some d , then this proof has some finite height h. But then since (d, f ) is in the active set and points to AbsLink ps, the first part of the invariant says that root, ps is resolvable. Moreover, the second part of the invariant says that the height of that resolution is some h 1 ≥ h. By applying the rule ResolveAbsLink we can then build a proof of resolution of d, p of height h = 1 + min(h 1 , h ) where h the height of the proof of resolution of the remaining path pr. Hence h ≥ h 1 + 1, but by uniqueness of resolution h must be equal to h, contradicting h 1 ≥ h.

Proof results

The table of Figure 3 summarizes the provers' results on all the verification conditions of our development. The total number of VCs is 198. We run all provers on all VCs with a time limit of 10 seconds. The first column gives the number of VCs successfully proved by the given prover. The other columns give respectively the minimum, average and maximum time the prover took to solve the VCs it proved. The last column gives the number of VCs that are proved only by the given prover. This number is 0 for Z3, meaning that Z3 is not really needed, but all the other provers are needed to make a complete proof of our development.

Notice that we needed one Coq proof to solve one VC in the part where we prove the equivalence between our definition of resolution and the one closer to POSIX informal definition. This Coq proof is not complex at all (see appendix), but surprisingly is no solved by any of our provers.

In the appendix we give the details of each verification conditions and which transformations and provers we used to discharge them.

Conclusions

We designed a formal specification of the intended meaning of pathname resolution in a Unix file system. We considered an algorithm that is not limited in the number of traversed symbolic links, and we formally proved that this algorithm is terminating, correct and complete. The main difficulty of this work is to design an adequate definition of the meaning of path resolution under the form of a ternary predicate d 1 , p d 2 , and also, in order to achieve the formal verification of the algorithm, to design an adequate variant of this predicate, indexed with an explicit height of the derivation. This idea of using the height of the derivation is a new lesson we learned during this work. In particular, such a concept have not be used so far in the formal verification of other algorithms for graph traversal. It seems that similar approaches exist in formal reasoning about semantics of programmation languages, for example the technique so-called step-indexing [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF].

The path resolution algorithm is indeed some kind of graph traversal, and its formal proof could be compared with those of standard graph algorithms. There is a collection of such graph algorithms proved using Why3 due to Chen and Lévy6 [START_REF] Chen | Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe[END_REF]. It seems that the presence of symbolic links in the Unix filesystem adds a significant difficulty to reason about graph traversal, which required the use our technique of indexing with height.

There exists an increasing amount of work on formal reasoning about Unix, file systems and shell scripts. Gardner, Ntzik and Wright proposed a framework based on an ad-hoc separation logic to reason about Unix commands that modify the file system [START_REF] Gardner | Local reasoning for the POSIX file system[END_REF]. Our own work is conducted within the CoLiS project which aims at reasoning about shell scripts for package installation. In CoLiS, a full formalization of the file system, including owners, groups, permissions and such is in progress. In this context, a subset of the POSIX shell is already formalized using Why3 [START_REF] Jeannerod | Le coquillage dans le CoLiS-mateur: formalisation d'un langage de programmation de type Shell[END_REF].

B Detailed Proof Results

The tables from Figure 4, 5, 6, 7, 8 and 9 give the details of each verification conditions and which transformations and provers we used to discharge them. The script for the only proof for which need Coq (in Figure 4) is the following. There is no great difficulty, indeed, it is unclear why no automatic prover is able to discharge it.

  function lookup dirnode filename : child function parent dirnode : dirnode axiom parent _ root: parent root = root axiom parent _ non _ root: forall d1 f d2. lookup d1 f = Dir d2 → parent d2 = d1

Inria

Figure 2 :

 2 Figure 2: Toy examples of partial path resolution.

  type lnk = (dirnode,filename) exception Error let rec aux _ resolve (d: dirnode) (p:path) (active:set lnk) : dirnode = match p with | Nil → d | Cons Up pr → let d' = parent d in aux _ resolve d' pr active | Cons Here pr → aux _ resolve d pr active | Cons (Down f) pr → match lookup d f with | Absent → raise Error | Dir d' → aux _ resolve d' pr active | AbsLink ps → if mem (d,f) active then raise Error else begin let actadd = add (d,f) active in let d' = aux _ resolve root ps actadd in aux _ resolve d' pr active end | RelLink ps → if mem (d, f) active then raise Error else begin let actadd = add (d, f) active in let d' = aux _ resolve d ps actadd in aux _ resolve d' pr active end end end

  inductive resolve _ to _ POSIX dirnode path dirnode = | ResolveNilPOSIX : forall d. resolve _ to _ POSIX d Nil d | ResolveDirPOSIX : forall d1 f d2 p d3. lookup d1 f = Dir d2 → resolve _ to _ POSIX d2 p d3 → resolve _ to _ POSIX d1 (Cons (Down f) p) d3 | ResolveAbsLinkPOSIX : forall d1 f ps pr d2. lookup d1 f = AbsLink ps → resolve _ to _ POSIX root (ps ++ pr) d2 → resolve _ to _ POSIX d1 (Cons (Down f) pr) d2 | ResolveRelLinkPOSIX : forall d1 f ps pr d2. lookup d1 f = RelLink ps → resolve _ to _ POSIX d1 (ps ++ pr) d2 → resolve _ to _ POSIX d1 (Cons (Down f) pr) d2 | ResolveUpPOSIX: forall d1 d2 d3 p. parent d1 = d2 → resolve _ to _ POSIX d2 p d3 → resolve _ to _ POSIX d1 (Cons Up p) d3 | ResolveHerePOSIX: forall d1 p d2. resolve _ to _ POSIX d1 p d2 → resolve _ to _ POSIX d1 (Cons Here p) d2

Lemma 10

 10 For any directory node d 1 and d 2 , and any path p, if d 1 , p d 2 then there exists h such that d 1 , p d 2 , h.

Lemma 13 Inria 4

 134 For any directory node d, and any path p, exists h that d, p h Proof of the Path Resolution Algorithm 4.1 Termination

  constant alllinks : set lnk ( * finite set * ) axiom alllinks _ in : forall d f ps. lookup d f = AbsLink ps ∨ lookup d f = RelLink ps → mem (d,f) alllinks

  let rec aux _ resolve (d: dirnode) (p:path) (active:set lnk) : dirnode requires { subset active alllinks } variant { cardinal alllinks -cardinal active, p } = ...

  let rec aux _ resolve (d: dirnode) (p:path) (active:set lnk) : dirnode ensures { resolve _ to d p result }

  _ resolve (d: dirnode) (p:path) (active:set lnk) : dirnode raises { Error → forall d'. not resolve _ to d p d' }

  resolve _ to _ POSIX d1 (Cons (Down fn) pr) d2 | ResolveUpPOSIX: forall d1 d2 d3 p. parent d1 = d2 -> resolve _ to _ POSIX d2 p d3 -> resolve _ to _ POSIX d1 (Cons Up p) d3 | ResolveHerePOSIX: forall d1 p d2. resolve _ to _ POSIX d1 p d2 -> resolve _ to _ POSIX d1 (Cons Here p) d2 lemma resolve _ to _ POSIX _ append: forall d1 d2 p1. resolve _ to _ POSIX d1 p1 d2 -> forall p2 d3. resolve _ to _ POSIX d2 p2 d3 -> resolve _ to _ POSIX d1 (p1 ++ p2) d3 lemma resolve _ to _ equivalence: forall d1 d2 p. resolve _ to _ POSIX d1 p d2 <-> resolve _ to d1 p d2 end ( ** {2 Determinism of Path Resolution} * ) theory Determinism use import int.Int use import FileSystem lemma resolve _ unique : forall d1 p d2. resolve _ to d1 p d2 -> forall d3. resolve _ to d1 p d3 -> d2 = d3 lemma resolve _ with _ height _ unique: forall d p h1. resolve _ with _ height d p h1 -> forall h2. resolve _ with _ height d p h2 -> h1 = h2 by match h1, h2 with | None, None -> true | _ , None | None, _ -> false | Some( _ ,u), Some( _ ,v) -> u = v end lemma resolve _ with _ height _ exists : forall d p. exists h. resolve _ with _ height d p h end ( ** {2 Path Resolution Algorithm} * ) module Resolution use import int.Int use import FileSystem use Determinism ( ** obvious technical lemmas, but needed to help provers * ) lemma resolve _ height _ absLink: forall d x p r h ps d' h'. resolve _ with _ height d (Cons (Down x) p) (Some(r, h)) -> lookup d x = AbsLink ps -> resolve _ with _ height root ps (Some(d', h')) -> h' <= h lemma resolve _ height _ relLink: forall d x p r h ps d' h'. resolve _ with _ height d (Cons (Down x) p) (Some(r, h)) -> lookup d x = RelLink ps -> resolve _ with _ height d ps (Some(d', h')) -> h' <= h use import set.Fset use import map.Map

  Theorem 3 For any directory node d 1 , d 2 , and any path p,

	d 1 , p	P OSIX	d 2	if and only if	d 1 , p	d 2

  Lemma 6 for all paths p 1 , p 2 and all dirnodes d 1 , d 3 , if d 1 , p 1 ++ p 2 d 3 then there exists d 2 such that d 1 , p 1 d 2 and d 2 , p 2 d 3 . This lemma is proved by structural induction on p 1 , using the previous lemma. The next lemma concerns the POSIX variant of resolution predicate. It is similar to lemma 4. For any directory node d 1 , d 2 and d 3 , and any path p 1 , p 2 , if d 1 , p 1

	Lemma 7 P OSIX	d 2 and
	d 2 , p 2	P OSIX	d 3 then d 1 , p 1 ++ p 2	P OSIX	d 3

3 , any path component c and any path p, if d1, c :: p d 3 then there exists d 2 such that d 1 1, c :: N il d 2 and d 2 , p 2 d 3 .

This lemma is also proved by induction on hypothesis d1, c :: p d 3 .

  Lemma 8 For any directory node d 1 and d 2 , and any path p, and any height h if d 1 , p d 2 , h then h ≥ 0 The proof can be done by induction on the hypothesis d 1 , p d 2 , and looking at all the 7 cases of rules applied to establish d 1 , p d 2 . We also need lemmas that relate the predicate resolves _ to to the predicate with height resolve _ with _ height. if there is a resolution with explicit height d 1 , p d 2 , h with any finite height h, then there is a resolution d 1 , p d 2 . For any directory nodes d 1 and d 2 , any path p, and any height h if d 1 , p d 2 , h then d 1 , p d 2 .

	Lemma 9

  Lemma 11 For any directory node d 1 , d 2 and d 3 , and any path p, if d 1 , p d 2 and d 1 , p d 3 then d 2 = d 3 A similar lemma goes for the same as former one that same resolving with height will result to a same proof height. Lemma 12 For any directory node d, and any path p, and any h 1 and h 2 , if d, p h 1 and d, p h 2 then h 1 = h 2

http://pubs.opengroup.org/onlinepubs/9699919799/basedefs/V1 _ chap04.html#tag _ 04 _ 13 RR n°8987

RR n°8987

parent d 1 = d 2 d 2 , p d 3 d 1 , ../p d 3 (ResolveUp) d 1 , p d 2 d 1 , ./p d 2 (ResolveHere) The first rule means that resolving the empty path from some node d results to d itself. The second rule means that if from node d 1 the filename f denotes a directory node d 2 , and if from d 2 the path p resolves to some node d 3 , then we know from node d 1 we can resolve the path f /p to node d 3 . The third rule indicates that if from some node d 1 we look up filename f then meet an absolute link which stores a path ps, we resolve this link from root to some node d 2 and from d 2 we can resolve path p to d 3 , then from node d 1 we can resolve path f /p to node d 3 . The fourth rule is similar to the third one, except when we look up the first filename we meet a relative link and we resolve this link from current directory which is d 1 itself. The fifth rule means if d 2 is the parent directory of some node d 1 , and from d 2 we can resolve path p to some node d 3 , then the path ../p can be resolved from d 1 to d 3 . The last rule denotes if from some node d 1 we can resolve path p to node d 2 then we can resolve the path ./p from d 1 to d 2 . The predicate d 1 , p d 2 can be formalised in the Why3 logic using an inductive definition, as follows, that corresponds closely to the rules above.inductive resolve _ to dirnode path dirnode = | ResolveNil : forall d. resolve _ to d Nil d | ResolveDir : forall d1 f d2 p d3. lookup d1 f = Dir d2 → resolve _ to d2 p d3 → resolve _ to d1 (Cons (Down f) p) d3 | ResolveAbsLink : forall d1 f ps pr d2 d3. lookup d1 f = AbsLink ps → resolve _ to root ps d2 → resolve _ to d2 pr d3 → resolve _ to d1 (Cons (Down f) pr) d3 | ResolveRelLink : forall d1 f ps pr d2 d3. lookup d1 f = RelLink ps → resolve _ to d1 ps d2 → resolve _ to d2 pr d3 → resolve _ to d1 (Cons (Down f) pr) d3 | ResolveUp: forall d1 d2 d3 p. parent d1 = d2 → resolve _ to d2 p d3 → resolve _ to d1 (Cons Up p) d3 | ResolveHere: forall d1 p d2.Inria

http://pubs.opengroup.org/onlinepubs/9699919799/basedefs/V1 _ chap04.html#tag _ 04 _ 13 RR n°8987

d 1 (f ) = Dir d 2 d 2 , p d 3 , h d 1 , f/p d 3 , h + 1 (ResolveHeightDir) d 1 (f ) = AbsLink ps root, ps d 2 , h 1 d 2 , p d 3 , h 2 d 1 , f/p d 3 , max(h 1 , h 2 ) + 1 (ResolveHeightAbsLink) d 1 (f ) = RelLink ps d 1 , ps d 2 , h 1 d 2 , p d 3 , h 2 d 1 , f/p d 3 , max(h 1 , h 2 ) + 1 (ResolveHeightRelLink) parent d 1 = d 2 d 2 , p d 3 ,h d 1 , ../p d 3 , (h + 1) (ResolveHeightUp) d 1 , p d 2 , h d 1 , ./p d 2 , (h + 1)

pauillac.inria.fr/~levy/why3/ Inria

rue Honoré d'Estienne d'Orves Bâtiment Alan Turing Campus de l'École Polytechnique 91120 Palaiseau Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

* Work partly supported by the Joint Laboratory ProofInUse (ANR-13-LAB3-0007, http://www.spark-2014.org/ proofinuse) and by the CoLiS project (ANR-15-CE25-0001, https://www.irif.fr/~treinen/colis/) of the French national research organization

A Complete Annotated Code

The full annotated code is given below.


J Buhot

C Toulouse

Y Gallais

A Sacuto

R De Sousa

D Wang

L Bellaiche

M Bibes

A Barthélémy

A Forget

D Colson

M Cazayous

M-A Measson
email: marie-aude.measson@univ-paris-diderot.fr

Driving spin excitations by hydrostatic pressure in BiFeO 3

Keywords: numbers: 77.80.Bh, 75.50.Ee, 75.25.+z, 78.30.Hv

Optical spectroscopy has been combined with computational and theoretical techniques to show how the spin dynamics in the model multiferroic BiFeO3 responds to the application of hydrostatic pressure and its corresponding series of structural phase transitions from R3c to the Pnma phases. As pressure increases, multiple spin excitations associated with non-collinear cycloidal magnetism collapse into two excitations, which show jump discontinuities at some of the ensuing crystal phase transitions. Effective Hamiltonian approach provides information on the electrical polarization and structural changes of the oxygen octahedra through the successive structural phases. The extracted parameters are then used in a Ginzburg-Landau model to reproduce the evolution with pressure of the spin waves excitations observed at low energy and we demonstrate that the structural phases and the magnetic anisotropy drive and control the spin excitations.

Multiferroic insulators have non-collinear magnetic order that drives ferroelectricity, and ferroelectric order that controls magnetism. This demonstrated crosscorrelation between electric and magnetic effects shows great promise for the development of magnonic devices whose goal is to use magnetic excitations as a low energy substitute of conventional electronics [1][2][START_REF] Demokritov | Magnonics: From fundamentals to applications[END_REF]. The spin-lattice interaction plays a decisive role in mediating the combined ferroic properties of multiferroic materials. When induced by epitaxial mismatch or chemical substitutions, strain provides a handle for the complex interplay between magnetic and electronic properties and their coupling to structural distortions [START_REF] Bai | [END_REF][5][6]. At present, the mechanisms linking spin excitation to structural deformation remain hardly accessible, whereas their fine control is highly desirable to build these new technologies.

Bismuth ferrite (BiFeO 3 ) plays an important role in multiferroics research as it is one of the few materials that has coexisting ferroelectricity and magnetism at room temperature [7] with an unusual combination of properties such as large above band gap voltages [8], photovoltaic effect [9] and conductive domain walls [10]. At ambient pressure, it becomes ferroelectric below 1100 K, with one of the largest known electrical polarization (that is, P = 100 µC/cm 2 ). Below 640 K, it exhibits an antiferromagnetic-like spiral of the cycloidal type with wavevector Q 0 = 2π/64nm [11]. This spiral transforms into a canted homogenous antiferromagnetic state under epitaxial strain [START_REF] Bai | [END_REF]6] or chemical doping [5]. Hydrostatic pressure is known to induce dramatic changes in BiFeO 3 's ferroelectricity and crystal structure. The large electric polarization either disappears or becomes weak above ≈ 5 GPa, and a total of six structural phase transitions have been observed up to 50 GPa [12,13].

In this Letter, we combine an advanced high-pressure technique ideally suited to probe simultaneously spin and phonon excitations with Landau-Ginzburg and effective Hamiltonian calculations to elucidate the coupling between spin excitations and structure in the prototypical multiferroic BiFeO 3 . We determine how pressureinduced structural transitions drive the magnetic order from a non-collinear to an homogeneous magnetic state.

We performed Raman spectroscopy measurements on single crystals of bulk BiFeO 3 under hydrostatic pressure up to 12 GPa in a membrane diamond anvil cell. We have developped an original optical experimental setup in order to track low energy excitations down to 7 cm -1 under extreme conditions (See Supplemental Material). We have thus been able to follow simultaneously the phonon modes and the magnetic excitations under a broad range of hydrostatic pressure. tations measured at low pressure. The frequency and the optical selection rules of the phonons modes are characteristic of the rhombohedral (R3c) phase [14]. The series of narrow peaks (with linewidth ∼ 1 cm -1 ) in Fig. 1 a) are the fingerprint of the cycloidal spin excitations at zero wavevector [15]. The spin excitations in BiFeO 3 can be decomposed into cyclon (φ n ) and extra-cyclon (ψ n ) modes, corresponding to oscillations in and out of the cycloid plane, respectively (Fig. 1 b) [15][16][17]. The first spin wave excitation peak at 7 cm -1 has not been assigned because it can either be attributed to the Φ + 0 mode or can result from small domains in the sample with weak magnetization [18].

As indicated by the change in the phonon modes (See Fig 2 a and Supplemental Material), we observe four structural transitions occurring at about 3.5, 5.5, 7.75 and 11 GPa, from a rhombohedral (R3c) to an orthorhombic (Pnma) phase through three orthorhombic structures (O 1 , O 2 , O 3 ), in agreement with previous high energy Raman scattering and X-ray studies [12]. Thanks to our observation of the new phonon modes occurring below 100 cm -1 , all structural transitions can be tracked, especially the transitions between the O 2 and O 3 phases. To support the structural description of BiFeO 3 under pressure, we performed a theoretical study of the crystalline structure using the effective Hamiltonian approach developed in Refs. [19,20]. As shown in Fig. 2 b), at low pressure the crystalline structure is rhombohedral and belongs to the R3c space group; when the pressure increases, we find several transitions towards orthorhombic structures with complex oxygen octahedra tilts belonging to the space groups Pna2 1 and Pca2 1 . These complex structures belong to the family of nanotwin phases predicted in Ref. [20] that have energies close to those of the R3c and Pnma states. Finally, at the highest pressures, theory predicts a transition to the orthorhombic structure belonging to the Pnma space group. One can thus notice that all but one of the measured structural phases are reproduced in the calculations. This missing phase is likely another intermediate and stable nanotwin configuration that may have a slightly higher enthalpy in the present effective Hamiltonian calculations. This theoretical study also provides information on the electrical polarization and structural changes of the oxygen octahedra through the successive FIG. 3: a) Low energy part of some of the Raman spectra showing the behaviour of the magnetic excitations under pressure. b) Energy of the spin wave excitations in BiFeO3 from 0 to 12 GPa reported as a function of pressure. Lines are fits using our theoretical model (See text) and some structural parameters obtained from computations. Vertical dash lines mark the four structural transitions.

structural phases. These extracted parameters will be shown to be crucial to reproduce the evolution with pressure of the spin waves excitations observed at low energy.

Figure 3 a) shows the low-energy part of the Raman spectra obtained at different pressures, and Fig. 3 b) depicts the corresponding spin excitation energies as a function of the applied pressure. At low pressure, below the first structural transition at 3.5 GPa, we observe that some spin excitations harden while other soften with a clear tendency for the three lowest energy modes to merge towards 12 cm -1 . Otherwise, the width of these peaks remains constant under pressure which indicates good hydrostaticity. Above 3.5 GPa, the crystal structure enters the first orthorhombic phase and only two spin excitations are observed, signaling the sudden disappearance of the spin cycloid at the first structural transition. The presence of two spin excitations in the O 1 phase shows that in this pressure range, BiFeO 3 's magnetic order is a simple two-sublattice antiferromagnet. The spin excitations harden as the pressure increases. A jump discontinuity is observed at the O 1 -to-O 2 phase transition whereas the hardening is continuous through the O 2 -to-O 3 phase transition.

In order to describe these results we propose a modified model for the coupling between magnetism and ferroelec-tricity in BiFeO 3 [19,21]

H = 1 2 i,δ JS i • S i+δ + [C (u i × δ) + D (ω i -ω i+δ )] •S i × S i+δ -K i (u i • S i ) 2 , (1)
with the sum running over all sites i of the pseudo cubic lattice formed by the Fe 3+ ions, with δ being the unit vector linking each site to its six nearest neighbours. The vector S i describes the Fe 3+ spin at site i, while the vectors u i and ω i represent structural distortions around this site. More precisely and as schematized in Fig. 4, u i is the local mode describing the electric dipole moment at site i (the ionic contribution to the electrical polarization, P , is proportional to u i ), and ω i is a pseudovector describing oxygen octahedra tilting at site i (the direction of ω i is the axis about which the oxygen octahedron of site i tilts, while its magnitude is the value of the angle associated with such tilt [22]. All interaction energies in Eq. ( 1) are expected to be pressure dependent. The exchange interaction J > 0 is known to scale inversely proportional to the tenth power of the distance between the Fe spins [23], and to increase linearly with pressure in each structural phase [12]. The pressure dependence of the other model parameters is not known. The parameter C is the spin-current interaction responsible for cycloidal order in BiFeO 3 , and the parameter D leads to spin canting and weak ferromagnetism [ 19,[START_REF] Sousa | Proc. SPIE 8813, Spintronics VI[END_REF]. Both C and D arise from the Dzyaloshinskii-Moriya interaction, with C, D ∝ η SO J, with η SO being the spin-orbit energy splitting of the heaviest lattice ion, Bi 3+ . Finally, the last term of Eq. ( 1) models single ion anisotropy, with the anisotropy axis pointing along the local mode vector u i , with K ∝ η 2 SO as shown in a microscopic calculation [21].

At ambient pressure and room temperature, BiFeO 3 has the R3c structure with the same local mode, u, at all sites i, pointing along [111] and giving rise to P . In addition, the oxygen octahedra adopts an antiferrodistortive order, with ω i = ω AF D /2 in one sublattice and ω i+δ = -ω AF D /2 in the other, with ω AF D also pointing along [111]. This structural configuration combined with Eq. (1) gives rise to the magnetic cycloidal order shown in Fig. 1 b). When the effective anisotropy

K eff = Ku 2 - D 2 ω 2 AF D 12J (2)
is positive, the ground state of Eq. ( 1) is an anharmonic cycloid, with spin excitations splitting into waves of even (+) and odd (-) symmetry with respect to space inversion along the cycloid wavevector Q (See Supplemental Material). This splitting is found to be essential to describe the modes [START_REF] Talbayev | [END_REF][26][27]; for example, at ambient pressure, the φ ± 1 modes are split by 5.5 cm -1 [27]. From our model calculations, we expect the evolution with pressure of the splitted modes to track the pressure dependence of J, u, and ω AF D (See Supplemental Material).

Our effective Hamiltonian calculations predict that u decreases with increasing pressure and ω AF D remains nearly constant in each phase (Fig. 4), as consistent with the known fact that (small) pressure typically reduces ferroelectricity [28]. In Fig. 3 b), the pressure trend of the spin excitations is well reproduced by our simple two parameters model. Only one of them depends on pressure (See Supplemental Material).

With pressures above about 3.5 GPa, a structural phase transition has occured, and only two spin excitations with frequencies to be denoted by ω high and ω low are observed. Equation (1) predicts a transition to a (canted) homogeneous antiferromagnet when

π 2 8 < J|K eff | (Cu) 2 ∝ 1 J - ω 2 AF D u 2 , (3)
so we infer that either J decreases or ω AF D /u increases during the transition R3c → O 1 . Both behaviours are consistent with our effective Hamiltonian calculations.

Obviously if P becomes zero right at the O 1 phase boundary, a transition towards an homogeneous antiferromagnetic state would appear associated with a single spin waves peak. This scenario is inconsistent with the measurements and the structural calculations. Indeed, u is not zero in the nanotwin phases as evidenced in Fig. 4 a). We combine the two theoretical models to reproduce the spin wave excitations in the orthorhombic phases. Equation ( 1) is able to explain the observed magnon data provided that two conditions are satisfied: K < 0 and θ = 0, where θ is the angle between u and ω AF D shown in Fig. 4. Only under these two conditions do we get ω high > √ 2 ω low with ω low > 0 as observed experimentally in the homogeneous magnetic phases.

Turning again to our effective Hamiltonian calculations, we see that θ becomes nonzero only after the transition R3c → Pna2 1 ; and that θ has a jump discontinuity in the transition Pna2 1 → Pca2 1 (Fig. 4). We do not define θ for the non-polar phase Pnma. Using the effective Hamiltonian calculations of θ for Pna2 In the Pnma phase, we observe two modes at 25 cm -1 and ∼ 40 cm -1 (Fig 3 a)). The first one has quite large spectral weight (10 times larger than all other magnon peaks), and does not seem to change frequency with increasing pressure. The second peak is quite similar to the magnon peaks in other phases. It may be that these first and second peaks are related to the so-called X5 + and R5 + antipolar modes known to occur in the nonpolar Pnma phase [29,30]. Future work is needed to verify such hypothesis because the model of Eqs. ( 1)-( 3) is presently developed to understand results of the polar R3c, O 1 , O 2 and O 3 phases.

In summary, via the combination of original Raman scattering experiment and computational and theoretical techniques, we report the magnetic excitations of BiFeO 3 as a function of pressure up to 12 GPa, showing for the first time that the material undergoes a series of magnetic phase transitions linked to structural changes. As pressure increases above 3.5 GPa , the non-collinear cycloidal magnetism tranforms into a canted homogeneous antiferromagnet. At the ensuing crystal phase transitions at 5.5, 7.75 and 11 GPa, the two remaining spin excitations show jump discontinuities. Effective Hamiltonian approach provides information on the electrical polarization and structural changes of the oxygen octahedra through the successive structural phases. The extracted parameters are then used in a Ginzburg-Landau model to reproduce the evolution with pressure of the spin waves excitations observed at low energy in all the structural phases. We demonstrate that the structural phases and the magnetic anisotropy drive and control the spin excitations. Pressure reveals several hytherto unexplored regimes in the prototypical multiferroic BiFeO 3 and can help stabilize unstable structural distortions leading to promising novel metastable phases. The control of the crystallographic lattice by ultrafast optical excitations may result in high-speed magnonic thanks to the simultaneous coherent driving of both lattice and magnetic excitations between different ferroelectric and magnetic phases.

Figure 1 aFIG. 1 :

 11 Figure 1 a) shows the phonon modes and the spin exci-

FIG. 2 :

 2 FIG. 2: a) Evolution of the energies of selected phonon modes in the 40-200 cm -1 range. Several modes appear or disappear at the structural transitions. b) Effective Hamiltonian simulations of the structure : the plotted lines corresponds to the enthalpies of four different structures as a function of pressure, relative to the enthalpy of the R3c phase. As pressure increases we observe the sequence of phase transitions R3c → Pna21 → Pca21 → Pnma.

FIG. 4 :

 4 FIG.4: a) Calculated average local mode u (directly proportional to P) for each phase as a function of pressure. Inset: schematic representation of the local mode u, the polarization P and the antiferrodistortive vector ωAF D describing the tilting of BiFeO3's oxygen octahedra in the pseudo-cubic structure of BiFeO3. The Dzyaloshinskii-Moryia interaction vector points along ωAF D . b) Calculated antiferrodistortive vector ωAF D (left scale) and the θ angle between u and ωAF D (right scale) as a function of pressure.

1 and Pca2 1

 1 to model magnons in the O 1 and O 2 -O 3 phases, respectively, we are able to reproduce the pressure dependence of the two spin wave excitations in the O 1 , O 2 and O 3 (Fig. 3 b)). Therefore, the jumps observed at the R3c → Pna2 1 (O 1 ) and the Pna2 1 (O 1 ) → Pca2 1 (O 2 ) structural transitions are directly linked to θ.

Acknowledgements C.T., J.B., M.-A. M. and M.C. would like to acknowledge support from the French National Research Agency (ANR) through DYMMOS and PRINCESS projects and the General Directorate for Armament (DGA). J.B. and M.-A. M. thank P. Munsch and G. Le Marchand for highpressure technical support (IMPMC, UPMC, Paris 6). R.d.S. acknowledges support from the Natural Sciences and Engineering Research Council of Canada, through its Discovery program. D.W. and L.B. thank the financial support of NSF grant DMR-1066158.


Pierre Castelli
email: pierre.castelli@ac-nice.fr

Pierre-Emmanuel Jabin
email: pjabin@umd.edu

Stéphane Junca
email: stephane.junca@unice.fr

Pierre-Emmanuel Jabin

P-E Jabin

Fractional spaces and conservation laws

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In this short note we first prove a remark on the optimal smoothing effect in Sobolev spaces given by Lions, Perthame and Tadmor [LPT] for strictly convex flux with a power-law type of degeneracy. Then we improve this result in fractional BV spaces: BV s . The smoothing effect in BV s with the optimal s yields to the optimal Sobolev regularity in W s,p with the same exponent s and the optimal p . This BV s regularity also gives traces property of the entropy solution ( [START_REF] Bianchini | On the structure of L ∞ -entropy solutions to scalar conservation laws in one-space dimension[END_REF][START_REF] De Lellis | Structure of entropy solutions for multidimensional scalar conservation laws[END_REF][START_REF] De Lellis | The rectifiability of entropy measures in one space dimension[END_REF][START_REF] Yu | Existence of strong traces for generalized solutions of multidimensional scalar conservation laws[END_REF][START_REF] Yu | Existence of strong traces for quasi-solutions of multidimensional conservation laws[END_REF]). We do not use the Lax-Oleinik formula ( [E]) as suggested in [LPT] and used in [START_REF] Bourdarias | Fractional BV spaces and applications to scalar conservation laws[END_REF][START_REF] Castelli | Smoothing effect in BV -Φ for scalar conservation laws[END_REF] but the one-sided Lipschitz condition on the velocity of the entropy solution (2) below. In all the paper, the following one-dimensional scalar conservation law are considered:

   ∂ u ∂t + ∂ ∂ x ( f (u)) = 0 on R×]0, +∞[ u(x, 0) = u 0 (x) on R , (1)
where the flux f is strictly convex and f ∈ C 1 , that is to say that the velocity a(u) = f (u) is strictly increasing. Lax ([La]) and Oleinik ([O]) obtained the optimal smoothing effect in BV for an uniformly convex flux: inf f > 0. The BV regularity is known to be lost if the second derivative of the flux vanishes at only one point [START_REF] Cheng | The space BV is not enough for hyperbolic conservation laws[END_REF]). Nevertheless we can obtain BV s regularity with 0 < s < 1. BV s spaces are essentially fractional BV spaces with similar properties as for example BV = BV 1 . First applications of such fractional BV spaces for a 2 × 2 system are already obtained in [BGJP].

We do not speak about SBV regularity ([AGV2, AD, B]) since this related to an uniform convex flux and the BV smoothing effect. On the other hand there are many other studies of the regularizing effect ([AGV1, BM, Cc, Ja]) which can be interpreted in the framework of fractional BV spaces but are beyond the scope of this short note.

The paper is organized as follow. In Section 2 a one-sided Lipschitz condition is recalled and linked with the degeneracy of the flux. Then, the smoothing effect is stated in W s,p and BV s . Section 3 gives a very simple proof of the smoothing effect in BV s and some consequences as the optimal W s,p regularity. We also present in the final Section 4 an alternative proof of the optimal Sobolev regularity in W s,1 .

One-sided condition and degeneracy of the flux

The proof uses the following generalized one-sided Oleinik inequality due to Dafermos ( [D]) (see also [START_REF] Cheng | A regularity theorem for a nonconvex scalar conservation law[END_REF]) under convex condition on the flux and for almost all x < y:

a(u(y,t)) -a(u(x,t)) ≤ y -x t (2)
There is a geometric interpretation of Inequality (2). If there is no shock issued from (x, 0) and (y, 0) in the (x,t) plane then u is constant on the two characteristics issued from (x, 0) and (y, 0) and the constant difference of the velocities is less than the constant velocity needed to meet the characteristics at time t. Inequality (2) is usually interpreted as an entropy condition: the jump of velocity can only be negative when y → x. A complete argument can be given with the generalized characteristics of Dafermos ([D]).

Since any strictly C 1 convex flux can be approached in C 1 by a sequence of C 2 uniformly convex flux, inequality (2) is still valid for entropy solutions almost everywhere. If the flux is uniformly convex then m |u -v| ≤ |a(u)a(v)| for a positive constant m and Inequality (2) yields to the one-sided Oleinik condition: u(y,t)u(x,t) ≤ y-x mt which can be rewritten with (v) + = max(v, 0) for almost all (x, y) ∈ R 2 and t > 0:

(u(y,t)u(x,t)) + ≤ (yx) + mt For a non uniformly convex flux, the previous one-sided Lipschitz condition becomes a one-sided Hölder condition: Inequality (5) at the end of this section. Before, a precise definition of a nonlinear flux is needed.

A power-law type of nonlinear degeneracy is considered as in [BGJ]. The following condition is enough for a strictly convex flux with some regularity and powerlaw flux for instances.

Definition 1. Let f ∈ C 1 (K, R), where K is a closed interval of R. We say that the degeneracy of f on K is at least q > 0 if the continuous derivative a(u) = f (u) satisfies : inf (u,v)∈(K×K) D K |a(u) -a(v)| |u -v| q > 0, (3)
where

D K = {(u, v) ∈ (K × K) | u = v}.
The lowest real number q, if there exists, is called the degeneracy of f on K and denoted p.

Inequality 3 is equivalent to:

∃m > 0, ∀(u, v) ∈ K 2 , |a(u) -a(v)| ≥ m |u -v| q . (4)
In particular, (4) implies that a : K→ R is strictly monotonic, since a is injective and continuous.

Example 1. If f (u) = |u| 1+p , p ≥ 1, then p is the degeneracy of f on any interval which contains 0.

Remark 1. 1) Suppose that for all u, v ∈ K, |a(u)a(v)| ≥ m |u -v| q and that a is differentiable at u 0 . Then q ≥ 1, since ∞ > a(u)-a(u 0 )

u-u 0 ≥ m |u -u 0 | q-1 . 2) If f is smooth on K, then f has a degeneracy p which is a positive integer. ([BGJ])
Replacing f (u) byf (-u) if necessary, we will assume subsequently that a(u) = f (u) is strictly increasing, so f is strictly convex. Now, one-sided condition (2) on the velocity is interpreted as the following onesided Hölder condition for almost all x, y:

(u(y,t) -u(x,t)) + ≤ K [(y -x) + ] s t s , (5)
where

s = 1 p , K = m -s , (v) + = max(v, 0) since m(u -v) p = m((u -v) + ) p ≤ a(u) - a(v) for u ≥ v.
Again, the exponent s naturally appears to estimate the positive variation of the entropy solution u . Now, we can state the smoothing effect for entropy solutions.

Theorem 1. Let u 0 belongs to L ∞ (R) function, K be the convex hull of u 0 (R), f a C 1 strictly convex flux with degeneracy p on K. Then the associated entropy solution of the conservation law (1) have got the following regularity in space for all positive time t and for all ε > 0:

u(.,t) ∈ W s-ε,1/s loc (R) ∩ BV s loc (R).
The regularity in W s-ε,1 loc (R) was conjectured in [LPT] and proved in [Ja]. The regularity in BV s was first proved in [BGJ] . The regularity in W s-ε,1/s loc is the consequence of the BV s loc regularity. The optimality in Sobolev spaces can be found in [DW] and in the fractional BV spaces in [START_REF] Castelli | Oscillating waves and the maximal smoothing effect for onedimensional nonlinear conservation laws[END_REF].

The main originality of this note is hence to give new and simpler proofs for this smoothing effect. Our proofs are based on the key BV estimate of the velocity a(u) for positive time given by (2). This is obviously a nonlinear regularity estimate on the entropy solution u which can easily be translated into more traditional regularity estimates.

The spaces BV s are in particular well adapted for this, leading to a very simple proof in the next section. From this BV s regularity it is straightforward to deduce fractional Sobolev regularity as well. But of course one can also prove directly the Sobolev regularity; we give an example of such a proof in the last Section.

BV s smoothing effect

We can define BV s + as W s,1 + and try to adapt the previous proof from Section 4.3. Unfortunately, the equality:

L ∞ ∩ BV s + = BV s for 0 < s < 1 is an open problem.
It is only known for s = 1 and, fortunately, it is enough to get the optimal BV s regularity.

BV s spaces

We recall briefly the definition and the main properties of fractional BV spaces. Definition 2. Let I be an non-empty interval of R and let S (I) be the set of subdivisions of I:

S (I) = {(x 0 , x 1 , ..., x n ), n ≥ 1, x i ∈ I, x 0 < x 1 < ... < x n }. For 0 < s ≤ 1 set TV s u[I] = sup S (I) n ∑ i=1 |u(x i ) -u(x i-1 )| 1 s , then BV s (I) := {u, TV s u[I] < ∞}.
For s = 1 we recover the space BV of functions of bounded variation. Functions in BV s have always left and right traces, like in BV ( [MO]). The exponent s is related to the fractional Sobolev derivative: BV s ⊂ W s-ε,1/s for all ε > 0 ( [BGJ]). The space BV s is also called the space of functions of bounded p -variation, with p = 1 s .

3.2

The short proof of the BV s smoothing

Set TV + u := sup n ∈ N * x 0 < x 1 < ... < x n n ∑ i=1 (u(x i ) -u(x i-1
)) + and BV + := {u, TV + u < ∞} then a(u(.,t)) ∈ BV + from inequality (2). According to the Maximum principle a(u(x,t)) ∈ L ∞ as the initial data u 0 . Since BV + ∩ L ∞ = BV , then a(u(.,t)) ∈ BV . Moreover, the velocity a() has at most a power law degeneracy:

|a(u) -a(v)| ≥ m |u -v| p , thus u ∈ BV s , where s = 1
p . This proof is very short and shortens the proof given in [BGJ]. Moreover, it gives more information about the singularity of u. For instance if the flux is a convex power law f (u) = |u| 1+p and the convex hull K of u 0 (R)does not contain the singular point 0 then the entropy solution associated to the initial date u 0 belongs to BV . That means that the BV s regularity is due to bigger oscillations around the state u = 0. Notice that since there is only a finite number of oscillations with any given positive strength thus the oscillations near state u = 0 has to be smaller and smaller and with infinitely many oscillations as optimal examples given in [START_REF] Castelli | Oscillating waves and the maximal smoothing effect for onedimensional nonlinear conservation laws[END_REF][START_REF] De Lellis | On the optimality of velocity averaging lemmas[END_REF].

4 Optimal smoothing effect in Sobolev spaces W s,1

The best smoothing effect in Sobolev spaces W s,1 was suggested in [LPT] with the Lax-Oleinik formula, bounded in [DW] and proved in [Ja] with a kinetic formulation and a BV assumption on the velocity. In this short note an another proof is proposed.

We recall a classical result for W 1,1 + and BV + . Then a similar result in W s,1 + is proved and used to get the maximal smoothing effect for conservation laws.

Usual results in

W 1,1 W 1,1 + (R) is the set of functions u such that the semi-norm |u| + 1 = R (∂ x u) + dx is finite, where (v) + = max(v, 0). Lemma 1. W 1,1 + (R) ∩ L 1 (R) ⊂ BV (R). Notice that W 1,1 + (R) ∩ L 1 (R) is bigger than W 1,1 (R): for instance consider the BV function u(x) = x χ [0,1](x)
where χ I is the indicator function of the set I.

The lemma follows from the equality R |∂ x u| dx = 2 |u| + 1 , which is valid for any smooth compactly supported function, since |x| = 2 x +x and then R |∂

x u| dx = 2 R (∂ x u) + dx -R ∂ x u dx = 2 R (∂ x u) + dx.
The space BV is better fitted through the control of the positive variation since

BV + (R) ∩ L ∞ (R) = BV (R)
where BV + (R) is the space of function u such that

TV + u = sup n∈N,x 0 <x 1 <•••<x n n ∑ i=1 (u(x i ) -u(x i-1 )) + < ∞.
4.2 The W s,1 + (R) case

The usual Sobolev semi-norm in W s,1 (R) for s ∈]0, 1[ is :

|u| s = R R |u(x) -u(y)| |x -y| 1+s dx dy = |u(x + h) -u(x)| |h| 1+s dx dh.
The Sobolev semi-norm in W s,1 + for s ∈]0, 1[ is :

|u| + s = R h>0 [u(x + h) -u(x)] + |h| 1+s dx dh.
The definition of the set W s,1 + (R) is:

Definition 3. u ∈ W s,1 + (R) if x>y [u(x) -u(y)] +
|x -y| 1+s dx dy < +∞.

Proposition 1. For all 0 < s < 1, L 1 (R) ∩W s,1 + (R) = W s,1 (R).

For s < 1 the estimates for the "one-sided" semi-norm is almost enough to stay in the associated Sobolev space. This is not true for s = 1 (Lemma 1). Proposition 1 is also valid locally:

L 1 loc (R) ∩W s,1 +,loc (R) = W s,1 loc (R).
Proof. The bound of the Sobolev semi-norm 2 I = |u(x)-u(y)| |x-y| 1+s dx dy < +∞ is obtained thanks to the integral I = x>y |u(x)-u(y)| |x-y| 1+s dx dy, which is a priori singular. Consider for ε > 0 the well-defined integrals :

I + ε = x>y [u(x) -u(y)] + ε + |x -y| 1+s dx dy I - ε = x>y [u(x) -u(y)] - ε + |x -y| 1+s dx dy , I ε = x>y |u(x) -u(y)| ε + |x -y| 1+s dx dy = I + ε + I - ε J ε = x>y u(x) -u(y) ε + |x -y| 1+s dx dy = I + ε -I - ε . Since J ε = u(x) x>y 1 ε + |x -y| 1+s dy dx -u(y) x>y 1 ε + |x -y| 1+s dx dy = u(x) x>y 1 ε + |x -y| 1+s dy dx -u(x) x<y 1 ε + |x -y| 1+s dy dx = u(x) h>0 1 ε + |h| 1+s dh dx -u(x) h<0 1 ε + |h| 1+s dh dx = 0 , it follows that I + ε = I - ε and then I ε = 2 I + ε ≤ 2 I + 0 < +∞.
The monotone convergence theorem yields lim ε→0 I ε = I = 2 I + 0 , so that u ∈ W s,1 (R).

Optimal smoothing effect in fractional Sobolev spaces

Thanks to Proposition (1), it suffices to get a W σ ,1 + estimate to have the W σ ,1 regularity ∀ σ < s. The information is propagated with a finite speed for conservation laws so we work only locally with local Sobolev semi-norm as in [Ju].

The well known embedding from Holder spaces to Sobolev spaces: W s,∞ loc ⊂ W σ ,1 loc , ∀σ < s, is simply extended to W s,∞ +,loc : Lemma 2. W s,∞ +,loc ⊂ W σ ,1 +,loc , ∀σ < s, Proof. Assume that (u(x + h)u(x)) + ≤ Ch s for h > 0.

Let h 0 and A be some positive constants to estimate the W σ ,1 +,loc semi-norm on the interval ]-A, A + h 0 [:

|u| + σ ,loc = |x|<A h 0 >h>0 [u(x + h) -u(x)] + h 1+σ dx dh ≤ |x|<A h 0 >h>0 C h s-σ -1 dx dh |u| + σ ,loc ≤ 2AC h 0 >h>0
h s-σ -1 dh which is finite if and only if σ < s .

Finally, the one-sided Holder condition for an entropy solution is already given by Inequality (5) and the Sobolev regularity follows since an entropy solution is bounded in L ∞ as its initial data and W σ ,1 +,loc ∩ L ∞ ⊂ W σ ,1 loc .

Acknowledgements We thanks the support of the project SlowDyn (team leader Bruno Lombard): an interdisciplinary CNRS project based on the LMA (CNRS, UPR 7051, Marseille). P-E

Jabin acknowledge the support of NSF Grants DMS 1312142 and 1614537 and by NSF Grant RNMS (Ki-Net) 1107444.