Georges-Axel Jaloyan

Claire Dross

Maroua Maalej

Yannick Moy

Andrei Paskevich

Verification of Programs with Pointers in SPARK

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

SPARK [START_REF] Mccormick | Building High-Integrity Applications with SPARK[END_REF] is a subset of the Ada programming language targeted at safetyand security-critical applications. SPARK restrictions ensure that the behavior of a SPARK program is unambiguously defined, and simple enough that formal verification tools can perform an automatic diagnosis of conformance between a program specification and its implementation.

As a consequence of SPARK's focus on automation and usability, it forbids the use of programming language features that either prevent automatic proof, or make it possible only at the expense of extensive user effort in annotating the program. The lack of support for pointers in SPARK is the main example of this choice. Among the various problems related to the use of pointers in the context of formal program verification, the most difficult problem is the possibility that two names refer to overlapping memory locations, a.k.a. aliasing. Formal verification platforms that support pointer aliasing like Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF] require users to annotate programs to specify when pointers are not aliased. This can take the form of inequalities between pointers when a typed memory model is used, or the form of separation predicates between memory zones when an untyped memory model is used. In both cases, the annotation burden is acceptable for leaf functions which manipulate single-level pointers, and quickly becomes overwhelming for functions that manipulate pointer-rich data structures. In parallel to the increased cost of annotations, the benefits of automation decrease, as automatic provers have difficulties reasoning explicitly with these inequalities and separation predicates.

Programs often rely on non-aliasing in general for correctness, when such aliasing would introduce interferences between two unrelated names. We call aliasing potentially harmful when a memory location modified through one name could be read through another name, within the scope of a verification condition. Otherwise, the aliasing is benign, when the memory location is only read through both names. A reasonable approach to formal program verification is thus to detect and forbid potentially harmful aliasing of names. Although this restricted language fragment cannot include all pointer-manipulating programs, it still allows us to introduce pointers to SPARK with minimal overhead for its program verification engine.

In this work, we present the first step for the inclusion of pointers in the Ada language subset supported in SPARK. As our main contribution, we show that it is possible to borrow and adapt the ideas underlying the safe support for pointers in permission-based languages like Rust, to safely restrict the use of pointers in usual imperative languages like Ada. This adaptation is based on a possible division of work between a permission-based anti-aliasing analysis, lifetime management by typing, and the use of a formal verification platform for checking non-nullity of accessed pointers.

The rest of the paper is organized as follows. In Section 2, we give an informal description of our approach. Section 3 introduces a small formal language for which we define the formal alias analysis rules in Section 4. In Section 5, we describe the implementation of the analysis inside the open-source GNAT compiler for Ada. We survey related works in Section 6.

Informal Overview of Alias Analysis in SPARK

In Ada, the access to memory areas is given through paths that start with an identifier (a variable name) and follow through record fields, array indices, or through a special field all, which corresponds to pointer dereferencing. In this paper, we only consider record and pointer types, and discuss the treatment of arrays in Section 5.

As an example, we use the following Ada type, describing singly linked lists where each node carries a Boolean flag and a pointer to a shared integer value. Given a variable A : List, the paths A.Flag, A.Key.all, A.Next.all.Key are valid and their respective types are Boolean, Integer, and access Integer (a pointer to an Integer). The important difference between pointers and records in Ada is that-similarly to C-assignment of a record copies the values of fields, whereas assignment of a pointer only copies the address and creates an alias.

The alias analysis procedure runs after the type checking. The idea is to associate one of the four permissions-RW, R, W or NO-to each possible path (starting from the available variables) at each sequence point in the program.

The read-only permission R allows us to read any value accessible from the path: use it in a computation, or pass it as an in parameter in a procedure call. As a consequence, if a given path has the R permission, then each valid extension of this path also has it.

The write-only permission W allows us to modify memory occupied by the value: use it on the left-hand side in an assignment or pass it as an out parameter in a procedure call. For example, having a write permission for a path of type List allows us to modify the Flag field or to change the addresses stored in the pointer fields Key and Next. However, this does not necessarily give us the permission to modify memory accessible from those pointers. Indeed, to dereference a pointer, we must read the address stored in it, which requires the read permission. Thus, the W permission only propagates to path extensions that do not dereference pointers, i.e., do not contain additional all fields.

The read-write permission RW combines the properties of the R and W permissions and grants the full ownership of the path and every value accessible from it. In particular, the RW permission propagates to all valid path extensions including those that dereference pointers. The RW permission is required to pass a value as an in-out parameter in a procedure call.

Execution of program statements changes permissions. A simple example of this is procedure call: all out parameters must be assigned by the callee and get the RW permission after the call. The assignment statement is more complicated and several cases must be considered. If we assign a value that does not contain pointers (say, an integer or a pointer-free record), the whole value is copied into the left-hand side, and we only need to check that we have the appropriate permissions: W or RW for the left-hand side and R or RW for the right-hand side. However, whenever we copy a pointer, an alias is created. We want to make the left-hand side the new full owner of the value (i.e., give it the RW permission), and therefore, after the permission checks, we must revoke the permissions from the right-hand side, to avoid potentially harmful aliasing. The permission checks are also slightly different in this case, as we require the right-hand side to have the RW permission in order to move it to the left-hand side.

Let us now consider several simple programs and see how the permission checks allow us to detect potentially harmful aliasing.

Procedure P1 in Fig. 1 receives two in-out parameters A and B of type List. At the start of the procedure, all in-out parameters assume permission RW. In particular, this implies that each in-out parameter is separated from all other parameters, in the sense that no memory area can be reached from two different parameters. The first assignment copies the structure B into A. Thus, the paths A. The first assignment does not change the permissions of A and its extensions: they retain the RW permission and keep the full ownership of their respective memory areas, even if the areas themselves have changed. The paths under B, however, must relinquish (some of) their permissions. The paths B.Key.all and B.Next.all as well as all their extensions get the NO permission, that is, lose both read and write permissions. This is necessary, as the ownership over their memory areas is transferred to the corresponding paths under A. The paths B, B.Key, and B.Next lose the read permission but keep the write-only W permission. Indeed, we forbid reading from memory that can be altered through a concurrent path. However, it is allowed to "redirect" the pointers B.Key and B.Next, either by assigning those fields directly or by copying some different record into B. The field B.Flag is not aliased, nor has it aliased extensions, and thus retains the initial RW permission. This RW permission allows us to perform the assignment B.Flag := True on the next line.

The third assignment, however, is now illegal, since B.Key.all does not have the write permission anymore. What is more, at the end of the procedure the in-out parameters A and B are not separated. This is forbidden, as the caller assumes that all out and in-out parameters are separated after the call just as they were before.

Procedure P2 in Fig. 1 receives two pointers A and B, and manipulates them inside a while loop. Since the permissions are assigned statically, we must ensure that at the end of a single iteration, we did not lose the permissions necessary for the next iteration. This requirement is violated in the example: after the last assignment A := B, the path B receives permission W and the path B.all, permission NO, as B.all is now an alias of A.all. The new permissions for B and B.all are thus weaker than the original ones (RW for both), and the procedure is rejected. Should it be accepted, we would have conflicting memory modifications from two aliased paths at the beginning of the next iteration.

µSPARK Language

For the purposes of formal presentation, we introduce µSPARK, a small subset of SPARK featuring pointers, records, loops, and procedure calls. We present the syntax and semantics of µSPARK, and define the rules of alias safety.

The data types of µSPARK are as follows:

type ::= Integer | Real | Boolean scalar type | access type access type (pointer) | ident record type
Every µSPARK program starts with a list of record type declarations:

record ::= type ident is record f ield end f ield ::= ident : type
We require all field names to be distinct. The field types must not refer to the record types declared later in the list. Recursive record types are allowed: field of a record type R can contain pointers to R (written access R). We discuss the handling of array types in Section 5.

The syntax of µSPARK statements is defined by the following rules: We require all formal parameters and local variables in a procedure to have distinct names. A procedure call can only pass left-values (i.e., paths) for in-out and out parameters. The execution starts from a procedure named Main with the empty parameter list.

path ::= ident variable | path . ident record field | path .
The type system for µSPARK is rather standard and we do not show it here in full. We assume that binary operators only operate on scalar types. The null pointer can have any pointer type access τ . The dereference operator .all converts access τ to τ . Allocation p := new τ requires path p to have type access τ . In what follows, we only consider well-typed µSPARK programs.

On the semantic level, we need to distinguish the units of allocation, such as whole records, from the units of access, such as individual record fields. We use the term location to refer to the memory area occupied by an allocated value. We treat locations as elements of an abstract infinite set, and denote them with letter . We use the term address to designate either a location, denoted , or a specific component inside the location of a record, denoted .f.g, where f and g are field names (assuming that at we have a record whose field f is itself a record with a field g). A value is either a scalar, an address, a null pointer or a record, that is, a finite mapping from field names to values.

A µSPARK program is executed in the context defined by a binding Υ that maps variable names to addresses and a store Σ that maps locations to values. By a slight abuse of notation, we apply Σ to arbitrary addresses, so that Σ( .f ) is Σ( )(f ), the value of the field f of the record value stored in Σ at . Similarly, we write Σ[ .f → v] to denote an update of a single field in a record, that is,

Σ[ → Σ( )[f → v]].
We use big-step operational semantics and write Υ • Σ • s ⇓ Σ to denote that µSPARK statement s, when evaluated under binding Υ and store Σ, terminates with the state of the store Σ . We extend this notation to sequences of statements in an obvious way, as the reflexive-transitive closure of the evaluation relation on Σ. In this paper, we do not consider diverging statements.

The evaluation of expressions is effect-free and is denoted e Υ Σ . We also need to evaluate l-values to the corresponding addresses in the store, written p Υ Σ , where p is the evaluated path. Illicit operations, such as dereferencing a null pointer, cannot be evaluated and stall the execution (blocking semantics). In the formal rules below, c stands for a scalar constant and , for a binary operator:

x Υ Σ = Υ (x) p.f Υ Σ = p Υ Σ .f p.all Υ Σ = p Υ Σ c Υ Σ = c p Υ Σ = Σ( p Υ Σ ) null Υ Σ = null e 1 e 2 Υ Σ = e 1 Υ Σ e 2 Υ Σ
Allocation adds a fresh address to the store, mapping it to a default value for the corresponding type: 0 for Integer, False for Boolean, null for the access types, and for the record types, a record value where each field has the default value. Notice that since pointers are initialised to null, there is no deep allocation. We write τ to denote the default value of type τ .

The evaluation rules are given in Figure 2. In the (E-call) rule, we evaluate the procedure body in the dedicated context Υ P • Σ P . This context binds the in parameters to fresh locations containing the values of the respective expression arguments, binds the in-out and out parameters to the addresses of the respective l-value arguments, and allocates memory for the local variables. At the

e Υ Σ = v Υ • Σ • p := e ⇓ Σ[ p Υ Σ → v ] (E-assign) ∈ dom Σ Υ • Σ • p := new τ ⇓ Σ[ p Υ Σ → , → τ ] (E-alloc) e Υ Σ = True Υ • Σ • s1 ⇓ Σ Υ • Σ • if e then s1 else s2 ⇓ Σ (E-ifTrue) e Υ Σ = False Υ • Σ • s2 ⇓ Σ Υ • Σ • if e then s1 else s2 ⇓ Σ (E-ifFalse) e Υ Σ = True Υ • Σ • (s ; while e loop s end) ⇓ Σ Υ • Σ • while e loop s end ⇓ Σ (E-whileTrue) e Υ Σ = False Υ • Σ • while e loop s end ⇓ Σ (E-
Υ Σ = va 1 , . . . ΥP = [ a1 → a 1 , . . . , b1 → p b 1 Υ Σ , . . . , c1 → qc 1 Υ Σ , . . . , d1 → d 1 , . . . ] ΣP = Σ[ a 1 → va 1 , . . . , d 1 → τ d 1 , . . . ] ΥP • ΣP • s ⇓ Σ Υ • Σ • P (ea 1 , . . . , p b 1 , . . . , qc 1 , . . .) ⇓ { a 1 , . . . , d 1 , . . .} -Σ (E-call)
Fig. 2: Semantics of µSPARK (terminating statements).

end of the call, the memory allocated for the in parameters and local variables is reclaimed: the operationstands for domain anti-restriction, meaning that locations a1 , . . . , d1 , . . . are removed from Σ . As there is no possibility to take the address of a local variable, there is no risk of dangling pointers.

Access Policies, Transformers, and Alias Safety Rules

We denote paths with letters p and q. We write p q to denote that p is a strict prefix of q or, equivalently, q is a strict extension of p. In what follows, we always mean strict prefixes and extensions, unless explicitly said otherwise.

In the typing context of a given procedure, a well-typed path is said to be deep if it has an extension of an access type, otherwise it is called shallow. We extend these notions to types: a type τ is deep (resp. shallow) if and only if a τ -typed path is deep (resp. shallow). In other words, a path or a type is deep if a pointer can be reached from it, and shallow otherwise. For example, the List type in Section 2 is a deep type, and so is access Integer, whereas any scalar type or any record with scalar fields only is shallow.

An extension q of a path p is called a near extension if it has as many pointer dereferences as p, otherwise it is a far extension. For instance, given a variable

Π move ---→e check W fresh RW lift --------------→p Π Π • p := e → Π (P-assign) Π check W fresh RW lift --------------→p Π Π • p := new τ → Π (P-alloc) Π check R ----→e Π Π • s1 → Π1 Π • s2 → Π2 ∀p. Π (p) = Π1(p) ∧ Π2(p) Π • if e then s1 else s2 end → Π (P-if) Π check R ----→e Π Π • s → Π ∀π. Π (π) Π(π)
Π

• while e loop s end → Π (P-while)

procedure P ( a1 : in τa 1 ; . . . ; b1 : in-out τ b 1 ; . . .

; c1 : out τc 1 ; . . . ) is • • • begin s end is declared in the program Π check R observe ----------→e a 1 ,... check RW borrow -----------→p b 1 ,... check W borrow ----------→q c 1 ,... Π Π fresh RW lift --------→p b 1 ,... fresh RW lift --------→q c 1 ,... Π Π • P (ea 1 , . . . , p b 1 , . . . , qc 1 , . . .) → Π (P-call)
Fig. 3: Alias safety rules for statements.

A of type List, the paths A.Flag, A.Key, and A.Next are the near extensions of A, whereas A.Key.all, A.Next.all, and their extensions are far extensions, since they all create an additional pointer dereference by passing through all.

We say that sequence points are the program points before or after a given statement. For each sequence point in a given µSPARK program, we statically compute an access policy: a partial function that maps each well-typed path to one of the four permissions: RW, R, W, and NO, which form a diamond lattice: RW > R|W > NO. We denote permissions with π and access policies with Π.

Permission transformers modify policies at a given path, as well as its prefixes and extensions. Symbolically, we write Π T -→ p Π to denote that policy Π results from application of transformer T to Π at path p. We write Π T1 T2 ----→ p Π as an

abbreviation for Π T1 -→ p T2 -→ p Π (that is, for some Π , Π T1 -→ p Π T2 -→ p Π ).
We write Π T -→ p,q Π as an abbreviation for Π T -→ p T -→ q Π . Permission transformers can also apply to expressions, which consists in updating the policy for every path in the expression. This only includes paths that occur as sub-expressions: in an expression X.f.g + Y.h, only the paths X.f.g and Y.h are concerned, whereas X, X.f and Y are not. The order in which the individual paths are treated must not affect the final result.

We define the rules of alias safety for µSPARK statements in the context of a current access policy. An alias-safe statement yields an updated policy which is used to check the subsequent statement. We write Π • s → Π to denote that statement s is safe with respect to policy Π and yields the updated policy Π . We extend this notation to sequences of statements in an obvious way, as the reflexive-transitive closure of the update relation on Π. The rules for checking the alias safety of statements are given in Fig. 3. These rules use a number of permission transformers such as 'fresh', 'check', 'move', 'observe', and 'borrow', which we define and explain below.

Let us start with the (P-assign) rule. Assignments grant the full ownership over the copied value to the left-hand side. If we copy a value of a shallow type, we merely have to ensure that the right-hand side has the read permission. Whenever we copy a deep-typed value, aliases may be created, and we must check that the right-hand side is initially the sole owner of the copied value (that is, possesses the RW permission) and revoke the ownership from it.

To define the 'move' transformer that handles permissions for the right-hand side of an assignment, we need to introduce several simpler transformers. Definition 1. Permission transformer check π does not modify the access policy and only verifies that a given path p has permission π or greater. In other words,

Π check π ----→ p Π if and only if Π(p)
π and Π = Π . This transformer also applies to expressions:

Π check π ----→ e Π states that Π check π
----→ p Π (= Π) for every path p occurring in e. Definition 2. Permission transformer fresh π assigns permission π to a given path p and all its extensions. Definition 3. Permission transformer cut assigns restricted permissions to a deep path p and its extensions: the path p and its near deep extensions receive permission W, the near shallow extensions keep their current permissions, and the far extensions receive permission NO.

Going back to the procedure P1 in Fig. 1, the change of permissions on the right-hand side after the assignment A := B corresponds to the definition of 'cut'. In the case where the right-hand side of an assignment is a deep path, we also need to change permissions of the prefixes, to reflect the ownership transfer. Definition 4. Permission transformer block propagates the loss of the read permission from a given path to all its prefixes. Formally, it is defined by the following rules, where x stands for a variable and f for a field name:

Π block ---→ x Π Π[p → W] block ---→ p Π Π block ---→ p.all Π Π(p) = NO Π block ---→ p.f Π Π(p) W Π[p → W] block ---→ p Π Π block ---→ p.f Π

Definition 5. Permission transformer move applies to expressions:

if e has a shallow type, then

Π move ---→ e Π ⇔ Π check R ----→ e Π , -if e is a deep path p, then Π move ---→ e Π ⇔ Π check RW cut block -------------→ p Π , -if e is null, then Π move ---→ e Π ⇔ Π = Π.
To further illustrate the 'move' transformer, let us consider two variables P and Q of type access List and an assignment P := Q.all.Next. We assume that Q and all its extensions have full ownership (RW) before the assignment. We apply the second case in the definition of 'move' to the deep path Q.all.Next. The 'check RW' condition is verified, and the 'cut' transformer sets the permission for Q.all.Next to W and the permission for Q.all.Next.all and all its extensions to NO. Indeed, P.all becomes an alias of Q.all.Next.all and steals the full ownership for this memory area. However, we still can reassign Q.all.Next to a different address. Moreover, we still can write some new values into Q.all or Q, without compromising safety. This is enforced by the application of the 'block' transformer at the end. We cannot keep the read permission for Q or Q.all, since it implies the read access to the data under Q.all.Next.all.

Finally, we need to describe the change of permissions on the left-hand side of an assignment, in order to reflect the gain of the full ownership. The idea is that as soon as we have the full ownership for each field of a record, we can assume the full ownership of the whole record, and similarly for pointers. Definition 6. Permission transformer lift propagates the RW permission from a given path to its prefixes, wherever possible:

Π lift --→ x Π Π[p → RW] lift --→ p Π Π lift --→ p.all Π ∀q p. Π(q) = RW Π[p → RW] lift --→ p Π Π lift --→ p.f Π ∃q p. Π(q) = RW Π lift --→ p.f Π
In the (P-assign) rule, we revoke the permissions from the right-hand side of an assignment before granting the ownership to the left-hand side. This is done in order to prevent creation of circular data structures. Consider an assignment A.Next.all := A, where A has type List. According to the definition of 'move', all far extensions of the right-hand side, notably A.Next.all, receive permission NO. This makes the left-hand side fail the write permission check.

Allocations p := new τ are handled by the (P-alloc) rule. We grant the full permission on the newly allocated memory, as it cannot possibly be aliased.

In a conditional statement, the policies at the end of the two branches are merged selecting the most restrictive permission for each path. Loops require that no permissions are lost at the end of a loop iteration, compared to the entry, as explained above for procedure P2 in Fig. 1.

Procedure calls guarantee to the callee that every argument with mode in, in-out, or out has at least permission R, RW or W, respectively. To ensure the absence of potentially harmful aliasing, we revoke the necessary permissions using the 'observe' and 'borrow' transformers. Definition 7. Permission transformer borrow assigns permission NO to a given path p and all its prefixes and extensions. Definition 8. Permission transformer freeze removes the write permission from a given path p and all its prefixes and extensions. In other words, freeze assigns to each path q comparable to p the minimum permission Π(q) ∧ R. Definition 9. Permission transformer observe applies to expressions:

if e has a shallow type, then

Π observe ----→ e Π ⇔ Π = Π, -if e is a deep path p, then Π observe ----→ e Π ⇔ Π freeze ---→ p Π , -if e is null, then Π observe ----→ e Π ⇔ Π = Π.
We remove the write permission from the deep-typed in parameters using the 'observe' transformer, in order to allow aliasing between the read-only paths. As for the in-out and out parameters, we transfer the full ownership over them to the callee, which is reflected by dropping every permission on the caller's side using 'borrow'.

In the (P-call) rule, we revoke permissions right after checking them for each parameter. In this way, we cannot pass, for example, the same path as an in and in-out parameter in the same call. Indeed, the 'observe' transformer will remove the write permission, which is required by 'check RW' later in the transformer chain. At the end of the call, the callee transfers to the caller the full ownership over each in-out and out parameter.

We apply our alias safety analysis to each procedure declaration. We start with an empty access policy, denoted ∅. Then we fill the policy with the permissions for the formal parameters and the local variables and check the procedure body. At the end, we verify that every in-out and out parameter has the RW permission. Formally, this is expressed with the following rule:

∅ fresh R ----→ a1,... fresh RW -----→ b1,... fresh W cut --------→ c1,... fresh RW -----→ d1,... Π Π • s → Π Π (b 1 ) = • • • = Π (c 1 ) = • • • = RW
procedure P ( a 1 : in τ a1 ; . . . ; b 1 : in-out τ b1 ; . . . ; c 1 : out τ c1 ; . . . ) is d 1 : τ d1 ; . . . begin s end is alias-safe

We say that a µSPARK program is alias-safe if all its procedures are. By the end of the analysis, an alias-safe program has an access policy associated to each sequence point in it. We say that an access policy Π is consistent whenever it satisfies the following conditions for all valid paths π, π.f , π.all:

Π(π) = RW =⇒ Π(π.f ) = RW Π(π) = RW =⇒ Π(π.all) = RW (1)
Π(π) = R =⇒ Π(π.f ) = R Π(π) = R =⇒ Π(π.all) = R (2)
Π(π) = W =⇒ Π(π.f ) ≥ W (3)
These invariants correspond to the informal explanations given in Section 2.

Invariant [START_REF] Mccormick | Building High-Integrity Applications with SPARK[END_REF] states that the full ownership over a value propagates to all values reachable from it. Invariant (2) states that the read-only permission must also propagate to all extensions. Indeed, a modification of a reachable component can be observed from any prefix. Invariant (3) states that write permission over a record value implies a write permission over each of its fields. However, the write permission does not necessarily propagate across pointer dereference.

Lemma 1 (Policy Consistency). The alias safety rules in Fig. 3 preserve policy consistency.

When, during an execution, we arrive at a given sequence point with the set of variable bindings Υ , store Σ, and statically computed and consistent access policy Π, we say that the state of the execution respects the Concurrent Read, Exclusive Write condition (CREW), if and only if for any two distinct valid paths p and q, p Υ Σ = q Υ Σ ∧ Π(p) ≥ W =⇒ Π(q) = NO. The main result about the soundness of our approach is as follows.

Theorem 1 (Soundness). A terminating evaluation of a well-typed alias-safe µSPARK program respects the CREW condition at every sequence point.

The full proof, for a slightly different definition of µSPARK, is given in [START_REF] Jaloyan | Internship report: Safe Pointers in SPARK 2014[END_REF]. The argument proceeds by induction on the evaluation derivation, following the rules in Figure 2. The only difficult cases are assignment, where the required permission withdrawal is ensured by the 'move' transformer, and procedure call, where the chain of 'observe' and 'borrow' transformers, together with the corresponding checks, on the caller's side, ensures that the CREW condition is respected at the beginning of the callee.

For the purposes of verification, an alias-safe program can be treated with no regard for sharing. More precisely, we can safely transform access types into records with a single field that contains either null or the referenced value. Since records are copied on assignment, we obtain a program that can be verified using the standard rules of Floyd-Hoare logic or weakest-precondition calculus (as the rules have also ensured the absence of aliasing between procedure parameters).

Indeed, consider an assignment A := B where A and B are pointers. In an alias-safe program, B loses its ownership over the referenced value and cannot be used anymore without being reassigned. Then, whenever we modify that value through A.all, we do not need to update B.all in the verification condition. In other words, we can safely treat A := B as a deep copy of B.all into A.all. The only adjustment that needs to be made to the verification condition generator consists in adding checks against the null pointer dereferencement, which is not handled by our rules.

Implementation and Evaluation

The alias safety rules presented above have been implemented in the front-end shared by the Ada GNAT compiler and the SPARK proof tool. Currently, they are only enforced in the SPARK subset of Ada.

The real SPARK subset differs from µSPARK in several respects, in particular, arrays, functions, additional loop constructs, and global variables. For arrays, permission rules apply to all elements, without taking into account the exact index of an element, which may not be known statically in the general case. Functions return values and cannot perform side effects. They only take in parameters and may be called inside expressions. To avoid creating aliases between the function parameters and the returned value, the full RW permission is required on the latter at the end of the callee. The rules for loops have been extended to handle for-loops and plain loops (which have no exit condition), and also the exit (break) statements inside loops. Finally, global variables are considered as implicit parameters of subprograms that access them, with mode depending on whether the subprogram reads and/or modifies the variable.

Though our alias safety rules are constraining, we feel that they significantly improve the expressive power of the SPARK subset. To demonstrate it, let us go over some examples. One of the main uses of pointers is to serve as references to avoid copying potentially big data structures. We believe this use case is supported as long as the CREW condition is respected. We demonstrate this on a small procedure that swaps two pointers.

type Int_Ptr is access Integer; procedure Swap (X, Y: in out Int_Ptr) is T : Int_Ptr := X; --ownership of X is moved to T, X gets 'W' begin X := Y; --ownership of Y is moved to X, Y gets 'W', X gets 'RW' Y := T; --ownership of T is moved to Y, T gets 'W', Y gets 'RW' return; --when exiting Swap, X and Y should be 'RW' end Swap; --local variable T is not required to have any permission This code is accepted by our alias safety rules. We can provide it with a contract, which can then be verified by the SPARK proof tool. Another common use case for pointers in Ada is to store indefinite types (that is, the types whose size is not known statically, such as String) inside aggregate data structures like arrays or records. The usual workaround consists in storing pointers to indefinite elements instead. This usage is also supported by our alias analysis, as illustrated by an implementation of word sets6 , which is accepted and fully verified by SPARK.

The last use case that we want to consider is the implementation of recursive data structures such as lists and trees. While alias safety rules exclude cyclic structures like doubly linked lists or arbitrary graphs, they are permissive enough for many non-trivial data structures, for example, red-black trees. To insert a value in a red-black tree, the tree is first traversed top-down to find the correct leaf for the insertion, and then it is traversed again bottom-up to reestablish balancing. Doing this traversal iteratively requires storing a link to the parent node in children, which is not allowed as it would introduce an alias. Therefore, we went for a recursive implementation 7 , partially shown below. The rotating double free, and null pointer dereference. In SPARK, those checks are handled by separate analysis passes of the toolset. Even though there is still no formal description of Rust's borrow-checker, we must note a significant recent effort to provide a rigorous formal description of the foundations of Rust [START_REF] Jung | RustBelt: Securing the Foundations of the Rust Programming Language[END_REF].

Dafny associates each object with its dynamic frame, the set of pointers that it owns [START_REF] Leino | Dafny: An Automatic Program Verifier for Functional Correctness[END_REF]. This dynamic version of ownership is enforced by modeling the ownership of pointers in logic, generating verification conditions to detect violations of the single-owner model, and proving them using SMT provers. In Spec#, ownership is similarly enforced by proof, to detect violations of the socalled Boogie methodology [START_REF] Barnett | Boogie: A Modular Reusable Verifier for Object-Oriented Programs[END_REF].

In our work, we use a permission-based mechanism for detecting potentially harmful aliasing, in order to make the presence of pointers transparent for automated provers. In addition, our approach does not require additional user annotations, that are required in some of the previously mentioned techniques. We thus expect to achieve high automation and usability, which was our goal for supporting pointers in SPARK.

Conclusion

In this paper, we have presented the rules for alias safety analysis that allow to implement and verify in SPARK a wide range of programs using pointers and dynamic allocation. To the best of our knowledge, this is a novel approach to control aliasing introduced by arbitrary pointers in a programming language supported by proof. Our approach does not require additional user annotations or proof of additional verification conditions, which makes it much simpler to adopt. We provided a formalization of our rules for a subset of SPARK in order to mathematically prove the safety of our analysis.

In the future, we plan to extend our formalism and proof to non-terminating executions. For that purpose, we can provide a co-inductive definition of the bigstep semantics and perform a similar co-inductive soundness proof, as described by Leroy and Grall [START_REF] Leroy | Coinductive Big-Step Operational Semantics[END_REF].

Another long-term goal would be extending our analysis so that it could handle automatic reclamation, parallelism, initialization and lifetime checks, instead of relying on external checks.

Fig. 1 :

 1 Fig. 1: Examples of potentially harmful aliasing.

  all pointer dereference expr ::= path l-value | 42 | 3.14 | True | False | . . . scalar value | expr ( + | -| < | = | . . . ) expr binary operator | null null pointer stmt ::= path := expr assignment | path := new type allocation | if expr then stmt else stmt end conditional | while expr loop stmt end "while" loop | ident ( expr ) procedure call Following the record type declarations, a µSPARK program contains a set of mutually recursive procedure declarations: procedure ::= procedure ident ( param ) is local begin stmt end param ::= ident : ( in | in-out | out ) type local ::= ident : type

procedure

  Swap (X, Y: in out Int_Ptr) with Pre => X /= null and Y /= null, Post => X.all = Y.all'Old and Y.all = X.all'Old;

  Flag, A.Key, and A.Next are separated, respectively, from B.Flag,

	procedure P1	procedure P2
	(A,B: in out List) is	(A,B: in out access Integer) is
	begin	begin
	A := B;	while B.all > 0 loop
	B.Flag := True;	A.all := A.all + 1;
	B.Key.all := 42;	B.all := B.all -1;
	end P1;	A := B;
		end loop;
		end P2;

https://github.com/GAJaloyan/SPARKExamples/tree/master/word_set

https://github.com/GAJaloyan/SPARKExamples/blob/master/rb_tree

This work is partly supported by the Joint Laboratory ProofInUse (ANR-13-LAB3-0007) and project VECOLIB (ANR-14-CE28-0018) of the French National Research Agency (ANR).

functions, which are used by the Balance procedure (not shown here) can be implemented straightforwardly, since rotation moves pointers around without creating any cycles. The SPARK proof tool does not currently accept recursive data types, which is why we have not attempted full functional verification of this code. However, it passes alias safety analysis successfully, which will make full verification possible once the restriction on recursive types is lifted in SPARK.

Related Works

The recent adoption of permission-based typing systems by programming languages is the culmination of several decades of research in this field. Going back as early as 1987 for Girard's linear logic [START_REF] Girard | Linear logic[END_REF] and 1983 for Ada's limited types [START_REF]AdaLRM: Reference Manual for the Ada(R) Programming Language[END_REF], Baker was the first to suggest using linear types in programming languages [START_REF] Baker | Use-once' Variables and Linear Objects: Storage Management, Reflection and Multi-threading[END_REF], formalised in 1998 by Clarke et al. [START_REF] Clarke | Ownership Types for Flexible Alias Protection[END_REF]. More recent works focus on Java, such as Javari and Uno [START_REF] Tschantz | Javari: Adding Reference Immutability to Java[END_REF][START_REF] Ma | Inferring Aliasing and Encapsulation Properties for Java[END_REF].

Separation logic [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF] is an extension of Hoare-Floyd logic that allows reasoning about pointers. In general, it is difficult to integrate into automated deductive verification: in particular, it is not directly supported by SMT provers, although some recent attempts try to have it mended [START_REF] Distefano | jStar: Towards Practical Verification for Java[END_REF][START_REF] Bakst | Predicate Abstraction for Linked Data Structures[END_REF].

Permission-based programming languages generalize the issue of avoiding harmful aliasing to the more general problem of preventing harmful sharing of resources (memory, but also network connections, files, etc.).

Cyclone and Rust achieve absence of harmful aliasing by enforcing an ownership type system on the memory pointed to by objects [START_REF] Grossman | Regionbased Memory Management in Cyclone[END_REF][START_REF] Balasubramanian | System Programming in Rust: Beyond Safety[END_REF]. Furthermore, Rust has many sophisticated lifetime checks, that prevent dangling pointers,


VAN DUONG DINH Abdelwahab Bensouilah
email: ai.bensouilah@math.univ-lille1.fr

Duong Van
email: dinhvan.duong@math.univ-toulouse.fr

Mohamed Dinh

Majdoub
email: mmajdoub@iau.edu.sa

AND Mohamed Majdoub

Scattering in

Keywords: Mathematics Subject Classification. 35-xx, 35L70, 35Q55, 35B40, 35B33, 37K05, 37L50 Inhomogeneous nonlinear Schrödinger equation, Decay solutions, Virial identity, Scattering, Weighted L 2 -space, Exponential nonlinearity, Singular Moser-Trudinger inequality

Introduction and main result

This paper is concerned with the scattering theory for the following initial value problem i∂ t u + ∆u = |x| -b e α|u| 2 -1 -α|u| 2 u, u(0) = u 0 , (1.1) where u = u(t, x) is a complex-valued function in space-time R × R 2 , 0 < b < 1 and α = 2π(2 -b).

The classical nonlinear Schrödinger equation (b = 0) with pure power or exponential nonlinearities arises in various physical contexts, as for example the self trapped beams in plasma, the propagation of a laser beam, water waves at the free surface of an ideal fluid and plasma waves (see [START_REF] Lam | Self trapped laser beams in plasma[END_REF]).

From the mathematical point of view, the classical NLS equation, i.e., problem (1.1) with b = 0, has attracted considerable attention in the mathematical community and the wellposedness theory as well as the scattering has been extensively studied, see for instance [2,[START_REF] Bahouri | Scattering for the critical 2-D NLS with exponential growth[END_REF][START_REF] Cazenave | Equations de Schrödinger non linéaires en dimension deux[END_REF][START_REF] Colliander | Energy critical NLS in two space dimension[END_REF]19,22]. We refer the reader to [8,[START_REF] Tao | Nonlinear Dispersive Equations: Local and Global Analysis[END_REF] and references therein for more properties and information on nonlinear Schrödinger equations.

In particular, in [START_REF] Colliander | Energy critical NLS in two space dimension[END_REF] a notion of criticality was proposed and the authors established in both subcritical and critical regimes the existence of global solutions in the functional space

C(R, H 1 (R 2 )) ∩ L 4
loc (R, W 1,4 (R 2 )). Later on in [19], the scattering in the energy space was obtained in the subcritical case. Note that the critical case was investigated in [START_REF] Bahouri | Scattering for the critical 2-D NLS with exponential growth[END_REF] where the scattering is proved in the radial framework.

The situation in the case b > 0 is less understood. Recently, in [START_REF] Bensouilah | Energy critical NLS equation with weighted exponential nonlinearity[END_REF] the authors established the global well-posedness in the energy space for 0 < b < 1. A natural question to ask then is the long time behavior of global solutions, that is the scattering. This means that every global solution of (1.1) approaches solutions to the associated free equation

i∂ t v + ∆v = 0, (1.2)
in the energy space H 1 as t → ±∞. The main difficulty is how to obtain the interaction Morawetz inequality? Recall that the interaction Morawetz inequality is nothing but the convolution of the classical one with the mass density. This in particular leads to a priori global bound of the solution in L 4 t (L 8 x ) which is the main tool for the scattering in the energy space (see for instance [START_REF] Bahouri | Scattering for the critical 2-D NLS with exponential growth[END_REF]19,24]). Note that the interaction Morawetz inequalities were first established for the NLS with power-type nonlinearity, and the proof depends heavily on the form of nonlinearity. Of course the proof can be easily adapted to more general homogeneous nonlinearities. More precisely, for linear combination of powers it suffices that all the powers are quadratic or higher with positive coefficients. The problem with singular weight (or for non-homogeneous nonlinearity) is much more difficult and should be investigated separately. The scattering in the energy space will be investigated in a forthcoming paper, and we believe that some ideas developed in [START_REF] Bahouri | Scattering for the critical 2-D NLS with exponential growth[END_REF] will be helpful.

Remark 1.1. We stress that the two-dimensional nonlinear Klein-Gordon equation with pure exponential nonlinearity was studied in [START_REF] Ibrahim | Global solutions for a semilinear, two-dimensional Klein-Gordon equation with exponential-type nonlinearity[END_REF][START_REF] Cazenave | Semilinear Schrödinger equations[END_REF]17], and a similar trichotomy based on the energy was defined. Recently, M. Struwe [30,31] was able to construct global smooth solution for smooth initial data and prove the scattering [START_REF] Sack | Scattering for a critical nonlinear wave equation in two space dimensions[END_REF].

Before stating our main result, let us recall that solutions of (1.1) satisfy the conservation of mass and Hamiltonian

M(u(t)) := u(t) L 2 , (1.3)
H(u(t)) := |∇u(t, x)| 2 + 1 α e α|u(t,x)| 2 -1 -α|u(t, x)| 2 - α 2 2 |u(t, x)| 4 dx |x| b . (1.4)
Our main result is the following.

Theorem 1.2. Let u 0 ∈ Σ be such that H(u 0 ) < 2 (1+b)(2-b) .
Then the corresponding global solution u of (1.1) satisfies u ∈ L 4 (R, C 1/2 ) and there exist u ± 0 ∈ Σ such that

lim t→±∞ e -it∆ u(t) -u ± 0 Σ = 0.
Let us make some comments. First, we see that illustrates the interaction between the wave function u and the potential |x| -b . More precisely, a sufficient condition for scattering is when the energy of the wave is less than a fixed amount depending on the sole parameter b that characterizes the weight function involved in the Hamiltonian of (1.1). Finally, a natural question that one could raise is the following: is the value 2 (1+b)(2-b) critical for scattering, in the sense that if the energy of the wave exceeds the latter quantity, would one get scattering?

Remark 1.3. For all 0 < b < 1, 8 9 ≤ 2 (1+b)(2-b) < 1.
The proof of Theorem 1.2 follows a standard strategy for the classical NLS equation. We first derive a decaying property for global solutions by using the pseudo-conformation law. We then show two types of global bounds for the solution u and its weighted variant (x + 2it∇)u. More precisely, we will show that

u S 1 (R) < ∞, (x + 2it∇)u S 0 (R) < ∞, (1.5)
where

u S 1 (R) := u L ∞ (R,H 1 ) + u L 4 (R,W 1,4 ) , u S 0 (R) := u L ∞ (R,L 2 ) + u L 4 (R,L 4 ) .
The proof of these global bounds relies on the decaying property, the singular Moser-Trudinger inequality and the Log estimate. The main difficulty comes from the singular weight |x| -b which does not belong to any Lebesgue space. To overcome this problem, we will take the advantage of Lorentz spaces. Note that |x| -b ∈ L 2 b ,∞ (R 2 ), where L p,∞ is the Lorentz space.

Once these global bounds are established, the scattering in weighted L 2 space Σ follows easily.

This paper is organized as follows. In Section 2, we recall some useful tools needed in our problem. The pseudo-conformal law is derived in Section 3. The decaying property of global solutions in Lebesgue spaces is showed in Section 4. Sections 5 and 6 are devoted to the proofs of global bounds (1.5). We shall give the proof of our main result in Theorem 1.2 in Section 7.

Useful Tools

In this section, we collect some known and useful tools.

Proposition 2.1 (Moser-Trudinger inequality [1]).

Let α ∈ [0, 4π). A constant c α exists such that exp(α|u| 2 ) -1 L 1 (R 2 ) ≤ c α u 2 L 2 (R 2 ) , (2.1
)

for all u in H 1 (R 2 ) such that ∇u L 2 (R 2 ) ≤ 1. Moreover, if α ≥ 4π, then (2.1) is false.
Remark 2.2. We point out that α = 4π becomes admissible in (2.1) if we require u H 1 (R 2 ) ≤ 1 rather than ∇u L 2 (R 2 ) ≤ 1. Precisely, we have

sup u H 1 ≤1 exp(4π|u| 2 ) -1 L 1 (R 2 ) < ∞, (2.2)
and this is false for α > 4π. See [25] for more details.

Theorem 2.3. [START_REF] Bergh | Interpolation Spaces[END_REF] Let 0 < b < 2 and 0 < α < 2π(2 -b). Then, there exists a positive

constant C = C(b, α) such that R 2 e α|u(x)| 2 -1 |x| b dx C R 2 |u(x)| 2 |x| b dx, (2.3
)

for all u ∈ H 1 (R 2 ) with ∇u L 2 (R 2 ) 1.
We point out that

α = 2π(2 -b) becomes admissible in (2.3) if we require u H 1 (R 2 ) ≤ 1 instead of ∇u L 2 (R 2 ) ≤ 1.
More precisely, we have Theorem 2.4.

[27] Let 0 < b < 2. We have

sup u H 1 (R 2 ) 1 R 2 e α|u(x)| 2 -1 |x| b dx < ∞ if and only if α ≤ 2π(2 -b). (2.4)
The following lemma will be very useful.

Lemma 2.5. Let 0 < b < 2 and γ ≥ 2. Then, there exists a positive constant C = C(b, γ) > 0

such that R 2 |u(x)| γ |x| b dx ≤ C u γ H 1 (R 2 ) , (2.5
)

for all u ∈ H 1 (R 2 ).
Proof. Note that

|x| -b L r (B) < ∞ if b < 2 r , |x| -b L r (B c ) < ∞ if b > 2 r , (2.6)
where

B = B(0, 1) is the unit ball in R 2 and B c = R 2 \B. Write R 2 |x| -b |u(x)| γ dx = B |x| -b |u(x)| γ dx + B c |x| -b |u(x)| γ dx.
We have from the Sobolev embedding

H 1 (R 2 ) ⊂ L q (R 2 ) for any q ∈ [2, ∞) that B c |x| -b |u(x)| γ dx ≤ u γ L γ (R 2 ) u γ H 1 (R 2 ) .
The first term is estimated as follows. Since 0 < b < 2, there exists ε > 0 small such that b < 2 1+ε . We apply (2.6) with r = 1 + ε and get

B |x| -b |u(x)| γ dx ≤ |x| -b L 1+ε (B) |u| γ L 1+ε ε (R 2 ) u γ L (1+ε)γ ε (R 2 ) u γ H 1 (R 2 ) .
Combining the two terms, we prove the desired estimate.

Remark 2.6. The inequality (2.5) fails for b 2. Indeed, let u ∈ D(R 2 ) (the space of smooth compactly supported functions) be a radial function such that u(x)

≡ 1 for |x| 1. Then, u ∈ H 1 (R 2 ) and R 2 |u(x)| γ |x| b dx 2π 1 0 rdr r b = +∞.
We also recall the so-called Gagliardo-Nirenberg inequalities and Sobolev embedding.

Proposition 2.7 (Gagliardo-Nirenberg inequalities [START_REF] Gagliardo | Proprieta di alcune classi di funzioni in piu variabili[END_REF]23]).

We have

u L m+1 u 1-θ L q+1 ∇u θ L p , (2.7)
where

θ = pN (m -q) (m + 1)[N (p -q -1) + p(q + 1)] , 0 ≤ q < σ -1, q < m < σ, σ = (p-1)N +p N -p if p < N ∞ if p ≥ N
In particular, for N = 2, we obtain

u L q u 2/q L 2 ∇u 1-2/q L 2 , 2 ≤ q < ∞. (2.8)
Proposition 2.8 (Sobolev embeddings).

We have

W s,p (R N ) → L q (R N ), 1 ≤ p < ∞, 0 ≤ s < N p , 1 p - s N ≤ 1 q ≤ 1 p .
(2.9)

W 1,p (R N ) → C 1-N p (R N ), p > N.
(2.10)

The following estimate is an L ∞ logarithmic inequality which enables us to establish the link between e 4π|u| 2 -1 L 1 T (L 2 (R 2 )) and dispersion properties of solutions of the linear Schrödinger equation.

Proposition 2.9 (Log estimate [START_REF] Ibrahim | Double logarithmic inequality with a sharp constant[END_REF]).

Let 0 < β < 1. For any λ > 1 2πβ and any 0 < µ ≤ 1, a constant C λ > 0 exists such that, for any function u ∈ H 1 (R 2 ) ∩ C β (R 2 ), we have u 2 L ∞ ≤ λ u 2 µ log C λ + 8 β µ -β u C β u µ , (2.11)
where

u 2 µ := ∇u 2 L 2 + µ 2 u 2 L 2 .
(2.12)

Recall that C β (R 2 ) denotes the space of β-Hölder continuous functions endowed with the norm

u C β (R 2 ) := u L ∞ (R 2 ) + sup x =y |u(x) -u(y)| |x -y| β .
We refer to [START_REF] Ibrahim | Double logarithmic inequality with a sharp constant[END_REF] for the proof of this proposition and more details. We just point out that the condition λ > 1 2πβ in (2.11) is optimal.

We also recall the so-called Strichartz estimates. We say that (q, r) is an L 2 -admissible

pair if 0 ≤ 2 q = 1 - 2 r < 1.
(2.13)

In particular, note that ( 2 1-2σ , 1 σ ) is an admissible pair for any 0 < σ < 1/2 and

W 1, 1 σ (R 2 ) → C 1-2σ (R 2 ).
Proposition 2.10 (Strichartz estimates [8]).

Let I ⊂ R be a time interval and let t 0 ∈ I. Then, for any admissible pairs (q, r) and (q, r),

we have v L q (I,W 1,r (R 2 )) v(t 0 ) H 1 (R 2 ) + i∂ t v + ∆v L q (I,W 1,r (R 2 )) .
(2.14)

The following continuity argument (or bootstrap argument) will be useful for our purpose.

Theorem 2.11 (Continuity argument).

Let X : [0, T ] → R be a nonnegative continuous function, such that, for every 0 t T ,

X(t) a + bX(t) θ ,
where a, b > 0 and θ > 1 are constants such that 1) and X(0)

a < 1 - 1 θ 1 (θb) 1/(θ-
1 (θb) 1/(θ-1) .
Then, for every 0 t T , we have

X(t) θ θ -1 a.
Proof. We sketch the proof for reader's convenience. The function f : x -→ bx θ -x + a is decreasing on [0, (θb) 1/(1-θ) ] and increasing on [(θb) 1/(1-θ) , ∞). The assumptions on a and

X(0) imply that f ((θb) 1/(1-θ) ) < 0. As f (X(t)) 0, f (0) > 0 and X(0) 1 (θb) 1/(θ-1)
, we deduce the desired result.

Pseudo-conformal law

In this section, we show a decaying property of global solutions to (1.1). Note that the conservation laws of mass and Hamiltonian give the boundedness of the L 2 and the H 1 norms but are insufficient to provide a decay estimate in (more general) Lebesgue spaces. To obtain such a decay we will take advantage of the pseudo-conformal law.

More precisely, we define the following quantities

V(t) := |x| 2 |u(t, x)| 2 dx, (3.1)
M(t) := 2 I (ū(t, x)x • ∇u(t, x)) dx, (3.2)
K(t) := (x + 2it∇)u(t) 2 L 2 + 4t 2 α e α|u(t,x)| 2 -1 -α|u(t, x)| 2 - α 2 2 |u(t, x)| 4 dx |x| b , (3.3) G(t) := 4(2 -b) α e α|u(t,x)| 2 -1 -α|u(t, x)| 2 - α 2 |u(t, x)| 4 dx |x| b - 8 α e α|u(t,x)| 2 (α|u(t, x)| 2 -1) + 1 - α 2 2 |u(t, x)| 4 dx |x| b =: g(|u(t, x)| 2 ) dx |x| b , (3.4)
where Then

g(τ ) = 4(2 -b) α e ατ -1 -ατ - α 2 2 τ 2 - 8 α e ατ (ατ -1) + 1 - α 2 2 τ 2 . ( 3
dV(t) dt = 2M(t), (3.6)
d 2 V(t) dt 2 = 8H(u 0 ) -G(t), (3.7
)

dK(t) dt = tG(t), (3.8)
G(t) ≤ 0, ∀ t ∈ R. (3.9)
Proof. A straightforward computation gives (3.6). Let N (x, u) := |x| -b e α|u| 2 -1 -α|u| 2 u. Following [START_REF] Azzam | Doubly Critical Semilinear Schrödinger Equations[END_REF] for instance, we find that

d 2 V(t) dt 2 = 8 |∇u| 2 dx + 4 x • {N (x, u), u} p dx,
where {f, g} p = R f ∇ḡ -g∇ f is the momentum bracket. Now compute the momentum bracket {N (x, u), u} p . Expand N (x, u) in a formal series

N (x, u) = |x| -b ∞ k=2 α k k! |u| 2k u.
Using the fact

{|x| -b |u| β u, u} p = - β β + 2 ∇(|x| -b |u| β+2 ) - 2 β + 2 ∇(|x| -b )|u| β+2 , one gets {N (x, u), u} p = ∞ k=2 α k k! {|x| -b |u| 2k u, u} p = - ∞ k=2 k α k (k + 1)! ∇(|x| -b |u| 2k+2 ) - ∞ k=2 α k (k + 1)! ∇(|x| -b )|u| 2k+2 .
An integration by parts leads

x • {N (x, u), u} p = 2 ∞ k=2 k α k (k + 1)! |u| 2k+2 dx |x| b + b ∞ k=2 α k (k + 1)! |u| 2k+2 dx |x| b = 2 α e α|u| 2 (α|u| 2 -1) + 1 - α 2 2 |u| 4 dx |x| b + b α e α|u| 2 -1 -α|u| 2 - α 2 2 |u| 4 dx |x| b ,
where we have used

∞ k=2 k α k (k + 1)! |u| 2k+2 = 1 α e α|u| 2 (α|u| 2 -1) + 1 - α 2 2 |u| 4 , ∞ k=2 α k (k + 1)! |u| 2k+2 = 1 α e α|u| 2 -1 -α|u| 2 - α 2 2 |u| 4 .
Therefore,

d 2 V(t) dt 2 = 8 ∇u(t) 2 L 2 + 8 α e α|u| 2 (α|u| 2 -1) + 1 - α 2 2 |u| 4 dx |x| b + 4b α e α|u| 2 -1 -α|u| 2 - α 2 2 |u| 4 dx |x| b .
Using the conservation law (1.4), we conclude the proof of (3.7). To prove (3.8), we first remark that

K(t) = V(t) -t dV(t) dt + 4t 2 H(u 0 ). Hence dK(t) dt = -t d 2 V(t)
dt 2 + 8tH(u 0 ), and the conclusion follows. Finally, for the sign of G, a simple computation shows that (for all τ ≥ 0)

g (τ ) = -8(αxe αx -e αx + 1) -4b(e αx -αx -1) ≤ 0.
Since g(0) = 0, we get (3.9).

As a consequence of Proposition 3.1, we have Corollary 3.2. Let u 0 ∈ Σ and u the corresponding global solution to (1.1). Then

(x + 2it∇)u(t) 2 L 2 + 4t 2 α e α|u(t,x)| 2 -1 -α|u(t, x)| 2 - α 2 2 |u(t, x)| 4 dx |x| b = xu 0 2 L 2 + t 0 τ G(τ ) dτ.

Decay estimate

Theorem 4.1. Let u 0 ∈ Σ and u the corresponding global solution to (1.1). Then, for all t = 0 and 2 ≤ q < ∞,

u(t) L q ≤ C q u 0 Σ |t| -(1-2 q ) ,
where C q > 0 is a constant depending only on q.

Proof. Set v(t, x) := e -i |x| 2 4t u(t, x). We see that

(x + 2it∇)u(t) 2 L 2 = 4t 2 ∇v(t) 2 L 2 . Hence, by Corollary 3.2, 4t 2 H(v(t)) = xu 0 2 L 2 + t 0 τ G(τ ) dτ.
Using (3.9), we get

4t 2 ∇v(t) 2 L 2 ≤ xu 0 2 L 2 , or equivalently ∇v(t) L 2 |t| -1 .
The conservation of mass, the fact that |u| = |v| and the Gagliardo-Nirenberg inequality (2.8), yield, for all 2 ≤ q < ∞,

u(t) L q = v(t) L q |t| -(1-2 q ) .
The proof is complete.

A natural and useful consequence from the previous theorem is the following bound estimate.

Corollary 4.2. Let u 0 ∈ Σ and u the corresponding global solution to

(1.1). Let 1 ≤ p < ∞, 2 ≤ q < ∞ be such that p 1 - 2 q > 1. (4.1)
Then, for all T > 0, we have

u L p ([T,∞);L q ) T 1 p + 2 q -1 p 1 -2 q -1 1/p < ∞.
). Let 1 ≤ p < ∞, 2 ≤ q < ∞ and 0 < T < S < ∞. Then u L p ([T,S];L q ) ≤ C,
where C > 0 depends only on p, q, T, S, u 0 Σ .

Another important consequence that will be used to obtain global bounds asserts that one can decompose any time interval (T, ∞) with T > 0 into a finite number of intervals on which the L p t (L q x ) norm is sufficiently small for every (p, q) satisfying (4.1). More precisely, we have

L =1 I = [T, ∞)
and

u L p (I ;L q ) ≤ ε, ∀ = 1, 2, • • • , L. (4.2)
Proof. From Corollary 4.2, one can choose S > T sufficiently large (not depending on u) such that u L p ([S,∞);L q ) ≤ ε. Define

T = T + S -T m , = 0, 1, • • • , m,
where m ≥ 1 to be chosen later. Using Hölder's inequality in time, we obtain that

u L p (T ,T +1 ];L q ) ≤ S -T m 1 2p u L 2p ([T,S];L q ) S -T m 1 2p
≤ ε, for m ≥ 1 sufficiently large and for all = 0, 1, • • • , m -1. This finishes the proof of Corollary 4.4.

Global bounds 1

In this section, we give the proof of the first global bound in (1.5). For a time slab I ⊂ R, we define S 1 (I) via

u S 1 (I) = u L ∞ (I,H 1 ) + u L 4 (I,W 1,4 ) .
By the Strichartz estimates, we have

u S 1 (I) u(T ) H 1 + i∂ t u + ∆u L 2 1+2δ (I,W 1, 1 1-δ ) , (5.1)
for any 0 < δ < 1/2 and T ∈ I. Note that . By Hölder's inequality,

A L 1 1-δ ∇u L 2 1-δ u 2 L 4 δ e α|u| 2 -1 |x| b L 2 1-2δ .
The term e α|u| 2 -1

|x| b L 2 1-2δ
can be estimated using Lorentz spaces. Indeed, by (A.1), we get

e α|u| 2 -1 |x| b L 2 1-2δ e α|u| 2 -1 1-θ L 1 e α|u| 2 -1 θ L ∞ |x| -b L 2 b ,∞ e α|u| 2 -1 θ L ∞ ,
where θ := δ + 1+b 2 . Note that we can choose 0 < δ < 1-b 2 so that θ ∈ (0, 1). Here we have used the Moser-Trudinger inequality (2.1) to obtain that e α|u| 2 -

1 L 1 1 since ∇u 2 L 2 < H(u 0 ) < 2 (1+b)(2-b) < 1. Hence A L 2 1+2δ (I,L 1 1-δ ) ∇u L 2 1-δ u 2 L 4 δ e α|u| 2 -1 θ L ∞ L 2 1+2δ (I) + ∇u L 2 1-δ u 2 L 4 δ e α|u| 2 -1 θ L ∞ L 2 1+2δ (J)
, where I = {t ∈ I/ u(t) L ∞ ≤ 1} and J = {t ∈ I/ u(t) L ∞ ≥ 1}. The first term in the right hand side can be easily estimated as follows

∇u L 2 1-δ u 2 L 4 δ e α|u| 2 -1 θ L ∞ L 2 1+2δ (I) ∇u L 2 δ (I,L 2 1-δ ) u 2 L 4 1+δ (I,L 4
δ ) u S 1 (I) u 2 L 4 1+δ (I,L 4 δ ) , (5.2)
where the following interpolation inequality is used

∇u L 2 δ (I,L 2 1-δ ) ≤ ∇u 1-2δ L ∞ (I,L 2 ) ∇u 2δ L 4 (I,L 4 ) . (5.3)
Let us turn to the second term. For t ∈ J, we obtain using (2.11) with

β = 1 2 -δ 2 that e α|u| 2 -1 θ L ∞ 1 + u C 1 2 -δ 2 u µ αθλ u 2 µ ,
for some 0 < µ < 1 and λ > 1 π(1-δ) to be chosen later. Since

u 2 µ = ∇u 2 L 2 + µ 2 u 2 L 2 < H(u 0 ) + µ 2 M(u 0 ) =: K 2 (µ), we bound e α|u| 2 -1 θ L ∞ 1 + u C 1 2 -δ 2 K(µ) αθλK 2 (µ) . Since K 2 (µ) → H(u 0 ) < 2 (1+b)(2-b) as µ → 0, we can choose 0 < µ < 1 sufficiently small so that K 2 (µ) < 2 (1+b)(2-b) . Moreover, as θK 2 (µ) 1-δ → 1+b 2 K 2 (µ) < 1 2-b as δ → 0, we choose 0 < δ < 1-b 2 sufficiently small such that θK 2 (µ) 1-δ < 1 2-b . At final, we choose 1 π(1-δ) < λ < 2 αθK 2 (µ) so that αθλK 2 (µ) < 2. It follows that e α|u| 2 -1 θ L ∞ (1 + u C 1 2 -δ 2 ) 2 u 2 C 1 2 -δ 2
, where we have used the fact that u(t)

C 1 2 -δ 2 ≥ u(t) L ∞ ≥ 1 for all t ∈ J. Therefore, ∇u L 2 1-δ u 2 L 4 δ e α|u| 2 -1 θ L ∞ L 2 1+2δ (J) ∇u L 2 1-δ u 2 L 4 δ u 2 C 1 2 -δ 2 L 2 1+2δ (I) ∇u L 2 δ (I,L 2 1-δ ) u 2 L 2 δ (I,L 4 δ ) u 2 L 4 1-δ (I,C 1 2 -δ 2 ) u 2 L 2 δ (I,L 4 δ ) u 3 S 1 (I) .
(5.4)

The last estimate follows from (5.3) and the fact

u L 4 1-δ (I,C 1 2 -δ 2 ) u L 4 1-δ (I,W 1, 4 1+δ ) u δ L ∞ (I,H 1 ) u 1-δ L 4 (I,W 1,4 )
u S 1 (I) .

Combining inequalities (5.2) and (5.4), we end up with . Taking 1 1-δ < p, q < ∞ such that 1 p + 1 q = 1-δ and applying Hölder's inequality, we get

A L 2 1+2δ (I,L 1 1-δ ) u S 1 (I) u 2 L 4 1+δ (I,L 4
δ ) + u 2 L 2 δ (I,L 4
B L 1 1-δ |x| -b-1 |u| e α|u| 2 -1 L 1 1-δ u L q e α|u| 2 -1 |x| b+1 L p .
Clearly,

e α|u| 2 -1 |x| b+1 p L p e α(p-1) u 2 L ∞ e α|u| 2 -1 |x| p(b+1) dx. Since 1 1-δ < 2 b+1 for 0 < δ < 1-b 2 , we choose 1 1-δ < p < 2 b+1 .
Hence we can apply the singular Moser-Trudinger inequality for the term e α|u| 2 -1 |x| p(b+1) dx to obtain

B L 2 1+2δ (I,L 1 1-δ ) u L q e α p-1 p u 2 L ∞ L 2 1+2δ (I) + u L q e α p-1 p u 2 L ∞ L 2 1+2δ (J)
.

Note that the choice of p leads to q > 2 1-b-2δ . Therefore,

B L 2 1+2δ (I,L 1 1-δ ) u L 2 1+2δ (I,L q ) + u L γ (I,L q ) e α p-1 p u 2 L ∞ L ρ (J)
,

where 2 1+2δ < γ, ρ < ∞ such that 1 γ + 1 ρ = 1+2δ 2 . Let t ∈ J. An application of the Log estimate (2.11) with β = 1 2 gives e α p-1 p u 2 L ∞ 1 + u C 1 2 u µ α p-1 p λ u 2 µ ,
for some 0 < µ < 1 and λ > 1 π to be chosen shortly. Since u 2 µ < K 2 (µ), it follows that e

α p-1 p u 2 L ∞ 1 + u C 1 2 K(µ) α p-1 p λK 2 (µ) . Choose 0 < µ < 1 sufficiently small such that K 2 (µ) < 2 (1+b)(2-b) < 1. Since 1 1-δ < 2(2-b) 2(2-b)-1 for 0 < δ < 1 2(2-b) , we choose 1 1-δ < p < 2(2-b) 2(2-b)-1 . In particular p 2(2-b)(p-1) > 1 > K 2 (µ). At final, we choose 1 π < λ < p α(p-1)K 2 (µ) so that α p-1 p λK 2 (µ) < 1. We thus get e α p-1 p u 2 L ∞ 1 + u C 1 2 u W 1,4 ,
where we have used

u(t) W 1,4 u(t) C 1 2 ≥ u(t) L ∞ ≥ 1 for all t ∈ J. Therefore, choosing 2 1+2δ < ρ < 4, one gets e α p-1 p u 2 L ∞ L ρ (J) u 4 ρ L 4 (I,W 1,4 ) .
This finally leads to

B L 2 1+2δ (I,L 1 1-δ ) u L 2 1+2δ (I,L q ) + u L γ (I,L q ) u 4 ρ S 1 (I) .
Note also that this choice of p leads to 0

< δ < 1 2(2-b) and q > 2(2-b) 1-2δ(2-b) . Arguing similarly for N (x, u) L 2 1+2δ (I,L 1 1-δ ) , we conclude that u S 1 (I) u(T ) H 1 + u S 1 (I) u 2 L 4 1+δ (I,L 4
δ ) + u 2 L 2 δ (I,L 4
δ ) u 3 S 1 (I) + u L 2 1+2δ (I,L q ) + u L γ (I,L q ) u 4 ρ S 1 (I) , (5.6)
where 0

< δ < min 1-b 2 , 1 2(2-b) , γ > 2 1+2δ and q > max 1 1-b-2δ , 2(2-b) 1-2δ(2-b) . Since 0 < δ < min 1-b 2 , 1 2(2-b)
and γ > 2 1+2δ , it is easy to check that the condition (4.1) is satisfied for

(p, q) ∈ 4 1 + δ , 4 δ , 2 δ , 4 δ , 2 1 + 2δ
, q , (γ, q) (5.7)

provided that q satisfies an additional condition q > 4 1-2δ . We thus obtain by Corollary 4.2 that u L p ((a,∞),L q ) < ∞ for all a > 0 and (p, q) in (5.7).

Let v(t, x) := e -i |x| 2 4t u(t, x). It is easy to see that |v| = |u|, |(x+2it∇)N (x, u)| = 2|t||∇N (x, v)| and 2|t||∇v| = |w|. We thus bound

|(x + 2is∇)N (x, u)| |x| -b (2|s||∇v|)|u| 2 e α|u| 2 -1 + |x| -b-1 (2|s||u| 3 ) e α|u| 2 -1 := C + D,
where we have used the fact that for all x ≥ 0, e x -1 -x ≤ x(e x -1). It follows from the pseudo-conformal law that w(T ) L 2 ≤ xu 0 L 2 . Thus, Strichartz estimate yields

w S 0 (I) xu 0 L 2 + (x + 2is∇)N (x, u) L 2 1+2δ (I,L 1 1-δ ) xu 0 L 2 + 2|s||∇N (x, v)| L 2 1+2δ (I,L 1 1-δ )
.

As above, one gets

C L 2 1+2δ (I,L 1 1-δ ) w S 0 (I) u 2 L 4 1+δ (I,L 4
δ ) + u 2 L 2 δ (I,L 4
δ ) w S 0 (I) u 2 S 1 (I)
and

D L 2 1+2δ (I,L 1 1-δ ) |s||u| 3 L 2 1+2δ (I,L q ) + |s||u| 3 L γ (I,L q ) u 4 ρ S 1 (I) , where 0 < δ < min 1-b 2 , 1 2(2-b) , γ > 2 1+2δ and q > max 1 1-b-2δ , 2(2-b) 1-2δ(2-b) .
The last inequality can be written as

D L 2 1+2δ (I,L 1 1-δ ) |s| 1 3 |u| 3 L 6 1+2δ (I,L 3q ) + |s| 1 3 |u| 3 L 3γ (I,L 3q ) u 4 ρ S 1 (I) .
As in Corollary 4.2, we note that for all a > 0, the norm |s|

1 3 u L m ((a,∞),L n ) < ∞ provided that 1 ≤ m < ∞, 2 ≤ n < ∞ satisfying m 2 3 - 2 n > 1. (6.1)
Since γ > 2 1+2δ , the condition (6.1) is fulfilled for (m, n) = 6 1+2δ , 3q , (3γ, 3q) provided that q > 4 3-2δ . Under the conditions

0 < δ < min 1 -b 2 , 1 2(2 -b) , γ > 2 1 + 2δ , q > max 1 1 -b -2δ , 2(2 -b) 1 -2δ(2 -b) , 4 3 -2δ
, we argue as above to obtain w S 0 ((T,∞)) < ∞ for some T > 0. By the same argument, we prove as well that w S 0 ((-∞,-S)) < ∞ for some S > 0. It remains to show that w ∈ S 0 ([-S, T ]). The proof of the latter claim follows the same argument as in [START_REF] Azzam | Doubly Critical Semilinear Schrödinger Equations[END_REF]. To see this, set H(t) = x + 2it∇. We are going to prove that Hu S 0 ([-S,T ]) < ∞. Divide [-S, T ] into a finite number of intervals J k = [t k , t k+1 ] such that |J k | ≤ ε, where ε > 0 is to be chosen later.

The Duhamel formula reads

H(t)u(t) = e i(t-t k )∆ H(t k )u(t k ) -i t t k e i(t-s)∆ H(s)N (x, u) ds.
By Strichartz estimates,

Hu S 0 (J k ) H(t k )u(t k ) L 2 + H(s)N (x, u) L 2 1+2δ (J k ,L 1 1-δ ) H(t k )u(t k ) L 2 + 2|s||∇N (x, v)| L 2 1+2δ (J k ,L 1 1-δ )
.

Note that in the following all constants involved in are independent of k. Using the fact that, for all x ≥ 0 and all η > 0, x(e x -1) ≤ e (1+η)x -1 η , and that |v| = |u|, we bound

2|s||∇N (x, v)| η |x| -b (2|s||∇v|) e α(1+η)|u| 2 -1 + |x| -b-1 (2|s||u|) e α(1+η)|u| 2 -1 .
The first term in the right hand side is estimated as follows. By Hölder's inequality,

2|s||∇v| e α(1+η)|u| 2 -1 |x| b L 1 1-δ 2|s||∇v| L 2 1-δ e α(1+η)|u| 2 -1 |x| b L 2 1-δ . Hence 2|s||∇v| e α(1+η)|u| 2 -1 |x| b L 2 1+2δ (J k ,L 1 1-δ ) 2|s||∇v| L 2 δ (J k ,L 2 1-δ ) e α(1+η)|u| 2 -1 |x| b L 2 1+δ (J k ,L 2 1-δ )
.

By (5.3), 2|s||∇v| L 2 δ (J k ,L 2 1-δ ) = Hu L 2 δ (J k ,L 2 1-δ ) Hu S 0 (J k ) . Write e α(1+η)|u| 2 -1 |x| b 2 1-δ L 2 1-δ e α(1+η) u 2 L ∞ -1 1+δ 1-δ e α(1+η)|u| 2 -1 |x| 2b 1-δ dx.
Since 2b 1-δ → 2b < 2 as δ → 0 and 1 H(u 0 ) > 1, one can choose 0 < δ < 1 2 and η > 0 sufficiently small such that 2b 1-δ < 2 and 0 < η < 1 H(u 0 ) -1. This guarantees that ∇(

√ 1 + η u) L 2 ≤ √ 1 + η H(u 0 ) < 1.
Hence we can apply the singular Moser-Trudinger inequality for the

term e α(1+η)|u| 2 -1 |x| 2b 1-δ dx. Thus e α(1+η)|u| 2 -1 |x| b L 2 1+δ (J k ,L 2 1-δ ) e α(1+η) u 2 L ∞ -1 1+δ 2 L 1 (I k ) + e α(1+η) u 2 L ∞ -1 1+δ 2 L 1 (J k ) ,
where

I k := {t ∈ J k / u(t) L ∞ ≤ 1} and J k := {t ∈ J k / u(t) L ∞ ≥ 1}. Let t ∈ I k . We have e α(1+η) u 2 L ∞ -1 α,η 1. Thus e α(1+η) u 2 L ∞ -1 L 1 (I k ) |J k |.
Let t ∈ J k . An application of the Log estimate (2.11) gives

e α(1+η)|u| 2 -1 L ∞ 1 + u C 1 2 K(µ) α(1+η)λK 2 (µ)
, where K 2 (µ) = H(u 0 ) + µ 2 M(u 0 ), 0 < µ < 1 and λ > 1 π . Choose 4 b+1 < σ < 4. We next choose 0 < µ < 1 sufficiently small such that K 2 (µ) < σ 2(2-b) . This is possible since

K 2 (µ) → H(u 0 ) < 2 (1+b)(2-b) < σ 2(2-b) . Choose η > 0 sufficiently small such that 1 + η < σ 2(2-b)K 2 (µ) . Thus 1 < σ 2(2-b)(1+η)K 2 (µ) . One can thus choose 1 π < λ < σ α(1+η)K 2 (µ) so that α(1 + η)λK 2 (µ) < σ.
As above, one comes to

e α(1+η) u 2 L ∞ -1 L 1 (J k ) |J k | 1-σ 4 u σ L 4 (J k ,W 1,4 ) .
Therefore,

e α(1+η)|u| 2 -1 |x| b L 2 1+δ (J k ,L 2 1-δ ) |J k | 1+δ 2 + |J k | (1-σ 4 ) 1+δ 2 u (1+δ)σ 2 S 1 (J k ) . Conclusion 2|s||∇v| e α(1+η)|u| 2 -1 |x| b L 2 1+2δ (J k ,L 1 1-δ ) Hu S 0 (J k ) |J k | 1+δ 2 + |J k | (1-σ 4 ) 1+δ 2 u (1+δ)σ 2 S 1 (J k ) .
For the second term, we estimate

|s||u| e α(1+η)|u| 2 -1 |x| b+1 L 2 1+2δ (J k ,L 1 1-δ ) |s||u| L γ (J k ,L q ) e α(1+η)|u| 2 -1 |x| b+1 L ρ (J k ,L p )
,

where 1 p + 1 q = 1 -δ and 1 γ + 1 ρ = 1+2δ 2 . Write e α(1+η)|u| 2 -1 |x| b+1 p L p e α(1+η) u 2 L ∞ -1 p-1 e α(1+δ)|u| 2 -1 |x| p(b+1) dx.
Since 1 1-δ → 1 < 2 b+1 and 1 H(u 0 ) > 1, one can choose 0 < δ < 1 2 and η > 0 sufficiently small such that 1 1-δ < 2 b+1 and 0 < η < 1 H(u 0 ) -1. This guarantees that ∇(

√ 1 + η u) L 2 ≤ √ 1 + η H(u 0 ) < 1. Choose
α(1+η)|u| 2 -1 |x| b+1 L ρ (J k ,L p ) e α(1+η) u 2 L ∞ -1 p-1 p L ρ (I k ) + e α(1+η) u 2 L ∞ -1 p-1 p L ρ (J k ) . Let t ∈ I k . Since e α(1+η) u 2 L ∞ -1 p-1 p ρ α,η,p,ρ 1, we get e α(1+η) u 2 L ∞ -1 p-1 p ρ L ρ (I k ) |J k |. Let t ∈ J k . An application of the Log estimate (2.11) with β = 1 2 gives e α(1+η)|u| 2 -1 p-1 p ρ L ∞ 1 + u C 1 2 K(µ) α(1+η) p-1 p ρλK 2 (µ)
, for some 0 < µ < 1 and λ > 1 π . Choose 0 < µ < 1 sufficiently small such that K 2 (µ) < 1.

Since

1 1-δ → 1 < 2(2-b) 2(2-b)-1 as δ → 0, one can choose 0 < δ < 1 2 sufficiently small such that 1 1-δ < 2(2-b) 2(2-b)-1 . Choose 1 1-δ < p < 2(2-b) 2(2-b)-1 . In particular p 2(2-b)(p-1) > 1 > K 2 (µ). Choose 0 < η < 1 such that 1 + η < p 2(2-b)(p-1)K 2 (µ) . At final, we choose 1 π < λ < p α(1+η)(p-1)K 2 (µ) .
Therefore, choosing 2 1+2δ < ρ < 4, one gets

e α(1+η)|u| 2 -1 p-1 p ρ L ∞ 1 + u C 1 2 4 . Using the fact that 1 ≤ u(t) L ∞ ≤ u(t) C 1 2 ≤ u(t) W 1,4 for all t ∈ J k , one gets e α(1+η)|u| 2 -1 p-1 p ρ L ∞ u 4 W 1,4 .
We come to

e α(1+η) u 2 L ∞ -1 p-1 p ρ L ρ (J k ) u 4 L 4 (J k ,W 1,4 ) . Thus e α(1+η)|u| 2 -1 |x| b+1 L ρ (J k ,L p ) |J k | + u 4 S 1 (J k ) 1 ρ .
By the sobolev embedding, one has

|s||u| L γ (J k ,L q ) u L ∞ (J k ,H 1 ) s L γ (J k ) |J k | γ+1 γ ,
where we have used the conservation laws and the fact that s

L γ (J k ) = t γ+1 k+1 -t γ+1 k γ+1 1 γ (t k+1 -t k ) γ+1 γ = |J k | γ+1 γ . Therefore, |s||u| e α(1+η)|u| 2 -1 |x| b+1 L 2 1+2δ (J k ,L 1 1-δ ) |J k | γ+1 γ |J k | + u 4 S 1 (J k ) 1 ρ .
Collecting the above estimates, we obtain

Hu S 0 (J k ) H(t k )u(t k ) L 2 + Hu S 0 (J k ) |J k | 1+δ 2 + |J k | (1-σ 4 ) 1+δ 2 u (1+δ)σ 2 S 1 (J k ) + |J k | γ+1 γ |J k | + u 4 S 1 (J k ) 1 ρ H(t k )u(t k ) L 2 + Hu S 0 (J k ) ε 1+δ 2 + ε (1-σ 4 ) 1+δ 2 u (1+δ)σ 2 S 1 (J k ) + ε γ+1 γ ε + u 4 S 1 (J k ) 1 ρ .
Since u S 1 (R) < ∞, we can choose ε > 0 small enough depending on S, T and u Summing over all subintervals J k , we prove Hu S 0 ([-S,T ]) < ∞. The proof is complete. .

Arguing as in the proof of (5.6), we obtain e -it 2 ∆ u(t 2 ) -e -it 1 ∆ u(t + u L γ ((t 1 ,t 2 ),L q ) u 4 ρ S 1 ((t 1 ,t 2 )) ,

where 0 < δ < min 1-b 2 , 1 2(2-b) , γ > 2 1+2δ and q > max . By adding an additional condition q > 4 1-2δ , we learn from Corollary 4.2 that u L p ((a,∞),L q ) < ∞ for all a > 0 and (p, q) in (5.7). In particular, u → 0 as t 1 → +∞. Since u S 1 (R) < ∞, we infer that the right hand side of (7.1) tends to zero as t 1 , t 2 → +∞ provided that 0 < δ < min 1-b 2 , 1 2(2-b) , γ > 2 1+2δ and q > max

For

  instance, it was noticed in [11] that the interaction Morawetz inequality for the NLS with singular nonlinearity N (x, u) = |x| -b |u| α u may not hold due to the lack of momentum conservation law. This is why we restrict ourselves to initial data belonging to the weighted L 2 -space Σ := H 1 ∩ L 2 (|x| 2 dx). Note that the scattering in Σ for the NLS with N (x, u) = |x| -b |u| α u was considered by the second author in [10].

2(

  1+b)(2-b) → 1 as b → 0. Thus our result extends the one in [19] for initial data in Σ. Second, the condition H(u) < 2 (1+b)(2-b)

. 5 )

 5 Proposition 3.1. Let u 0 ∈ Σ and u the corresponding global solution to (1.1).

For

  bounded time intervals, the local theory allows us to remove the assumption (4.1) to obtain Corollary 4.3. Let u 0 ∈ Σ and u the corresponding global solution to (1.1

Corollary 4 . 4 .

 44 Let u 0 ∈ Σ and u the corresponding global solution to (1.1). Let 1 ≤ p < ∞, 2 ≤ q < ∞, ε > 0 and T > 0. Assume that the condition (4.1) is fulfilled. Then there exists L ≥ 1 not depending on u and time intervals I 1 , I 2 , • • • , I L such that

2 1+2σ , 1 1 -Theorem 5 . 1 .

 151 δ is the conjugate pair of the Schrödinger admissible pair 2 1-2σ , 1 σ . Let u 0 ∈ Σ be such that H(u 0 ) < 2 (1+b)(2-b) . Then the corresponding global solution u to (1.1) satisfies u ∈ S 1 (R).

Proof.

  It suffices to estimate the nonlinear term in some dual Strichartz norm as in (5.1). We have|∇N (x, u)| |x| -b |∇u||u| 2 e α|u| 2 -1 + |x| -b-1 |u| e α|u| 2 -1 -α|u| 2 := A + B. Let 0 < δ < 12 to be chosen adequately, and let I be a time slab. Let us first estimate the norm A

S 1 (

 1 R) to get Hu S 0 (J k ) ≤ C H(t k )u(t k ) L 2 + C,for some constant C > 0 independent of S and T . By induction, we obtain for each k, Hu S 0 (J k ) ≤ C H(-S)u(-S) L 2 + C.

1 1 -

 1 b-2δ , 2(2-b) 1-2δ(2-b)

  t 1 ,t 2 ),L q )

1 1 -

 1 b-2δ , 2(2-b) 1-2δ(2-b) ,4 1-2δ

7 .

 7 Scattering in weighted L 2 spaceIn this section, we give the proof of our main result in Theorem 1.2.Proof of Theorem 1.2. Let u 0 ∈ Σ and u the corresponding global solution to (1.1). By Duhamel formula, we havee -it∆ u(t) = u 0 -i Let 0 < t 1 < t 2 < +∞. It follows from Strichartz estimates that e -it 2 ∆ u(t 2 ) -e -it 1 ∆ u(t 1 ) H 1 =

				t
				e -is∆ N (x, u)ds.
				0
	t 2	e -is∆ N (x, u)ds
	t 1			H 1
	N (x, u)	L	2 1+2δ ((t 1 ,t 2 ),L	1 1-δ )	+ ∇N (x, u)	L	2 1+2δ ((t 1 ,t 2 ),L	1 1-δ )

  1 ) H 1 u S 1 ((t 1 ,t 2 )) u 2

	L	4 1+δ ((t 1 ,t 2 ),L	4 δ )	+ u 2 L	2 δ ((t 1 ,t 2 ),L	4 δ )	u 3 S

1 ((t 1 ,t 2 )) + u L 2 1+2δ ((t 1 ,t 2 ),L q )

  . This shows that e -it∆ u(t) is a Cauchy sequence in H 1 as t → +∞. There thus exists u + 0 ∈ H 1 such that e -it∆ u(t) → u + 0 as t → +∞. It remains to show that this scattering state u + 0 belongs to Σ. Since x + 2it∇ commutes with i∂ t + ∆u, the Duhamel formula gives (x + 2it∇)u(t) = e it∆ xu 0 -i Using the fact that x + 2it∇ = e it∆ xe -it∆ , we write xe -it∆ u(t) = xu 0 -i By Strichartz estimates, we have xe -it 2 ∆ u(t 2 ) -xe -it 1 ∆ u(t 1 ) L 2 =

	t
	e i(t-s)∆ (x + 2is∇)N (x, u)ds.
	0
	t
	e -is∆ (x + 2is∇)N (x, u)ds.
	0
	t 2
	t 1

e -is∆ (x + 2is∇)N (x, u)ds

L 2 (x + 2is∇)N (x, u) L 2 1+2δ ((t 1 ,t 2 ),L 1 1-δ ) 2|s||∇N (x, v)| L 2 1+2δ ((t 1 ,t 2 ),L 1 1-δ ) ,

Acknowledgments

V. D. D. would like to express his deep thanks to his wife-Uyen Cong for her encouragement and support. M. M. would like to thank K. Nakanishi for enlightening discussions concerning the interaction Morawetz inequalities. The authors would like to thank the reviewer for his/her helpful comments and suggestions.

Now let 0 < δ < min 1-b 2 , 1 2(2-b) , γ > 2 1+2δ and q > max < ∞. We have

Bounding u(T ) H 1 by a constant C(H(u 0 ) + M(u 0 ))) depending only on the mass and energy of the initial data, one infers

Using Corollary 4.4, one can pick ε > 0 small (to be determined later) and a finite number

≤ ε.

Thus, by (5.6) and since 4 ρ > 1, we get

A continuity argument allows us to pick ε > 0 sufficiently small depending only on C(H(u 0 )+ M(u 0 ))+A such that u S 1 (I ) ≤ C(H(u 0 ), M(u 0 ), A). Since the number of intervals is finite and the conclusion can be made for all I 's, we get u S 1 ((T,∞)) < ∞. A similar argument applies for negative times, and we get u S 1 ((-∞,-S)) < ∞ for some S > 0. We conclude the proof by the local theory.

Global bounds 2

In this section, we prove the second global bound in (1.5). For a time slab I ⊂ R, we define S 0 (I) by

. Let u the corresponding global solution to (1.1) and set w(t) := (x + 2it∇)u(t). Then it holds that w ∈ S 0 (R).

Proof. Let T > 0 and set I = (T, ∞). Since x + 2it∇ commutes with i∂ t + ∆, the Duhamel formula implies

where v(t, x) := e -i |x| 2 4t u(t, x). Estimating as in the proof of Theorem 6.1, we get

w S 0 (I) u 2 S 1 (I)

where

and u

are finite for any a > 0. Moreover, adding an additional condition q > 4 3-2δ , the condition (6.1) is satisfied for (m, n) = 6 1+2δ , 3q , (3γ, 3q) . Thus the norms |s|

and |s|

are both finite for any a > 0. In particular, |s|

→ 0 as t 1 → +∞. Since u S 1 (R) < ∞ and w S 0 (R) < ∞, the right hand side of (7.2) tends to zero as t 1 , t 2 → +∞.

This implies that xe -it∆ u(t) is a Cauchy sequence in L 2 as t → +∞. We thus have xu + 0 ∈ L 2 and so u + 0 ∈ Σ. Moreover, we have

Repeating the above argument, we prove that e -it∆ u(t) -u + 0 Σ → 0 as t → +∞.

This completes the proof for positive times, the one for negative times is similar.

Appendix A. Lorentz spaces

We recall some basic facts about the Lorentz spaces which are relevant to our study. We refer the reader to [6, 13, 20, 14, 28] and references therein for more properties and information on Lorentz spaces.

Definition A.1. Let u : R N → R be a measurable function. The distribution function of u is given by

Here, the notation |E| stands for the N -dimensional Lebesgue measure of E. The (unidimensional) decreasing rearrangement of u, denoted by u * , is defined by

It is clear that d u and u * are non-negative non-increasing functions. The Lorentz spaces L p,q (R N ) are defined as follows.

Definition A.2. Let 0 < p < ∞ and 0 < q ≤ ∞. Then

We have L p,p = L p and by convention L ∞,∞ = L ∞ . Another way to define the Lorentz space L p,q is via real interpolation theory as follows (see [START_REF] Bennet | Interpollation of Operators[END_REF])

One of the difficulties in our problem is the singular weight |x| -b in the nonlinearity. Since this weight does not belong to any Lebesgue space we have to treat it differently. Fortunately, |x| -b belongs to the Lorentz space L 2 b ,∞ (R 2 ) which plays an important role in our proof.

The following lemma will be useful.

Lemma A.3. Let 1 < p < ∞, 1 < p 1 < ∞ and 1 ≤ p 2 ≤ ∞ be such that

Then

where θ = 1 -1 p 1 .


Jean-Jacques Hamm a réuni sous le titre Approches de Stendhal la plupart des contributions qu'il a publiées entre 1985 et 2012 dans des revues spécialisées, remaniées pour l'occasionet dont certaines sont inédites. Les textes sélectionnés ont été regroupés sous quatre rubriques : une première partie chronologique, « OEuvres », rassemble des études sur la création stendhalienne dans une perspective diachronique et fait voir ce qui, des premiers balbutiements en 1797, des « ratages » (p. 20) de l'auteur en herbe, conduit à l'oeuvre proprement dite : ou comment Henri Beyle est devenu Stendhal, en faisant l'« apprentissage d'une liberté » (p. 147), à travers des constantes nommées « indices » ou « invariants textuels » (p. 12). Ces premiers textes lacunaires ou incomplets de Stendhal permettent à l'auteur de l'ouvrage de dégager, dès le seuil, les premiers éléments d'une poétique de l'inachevé qui a fait la matière d'un livre fondamental et sa signature (Le texte stendhalien : achèvement et inachèvement, Sherbrooke, 1986). Jean-Jacques Hamm échappe ainsi à une perspective purement téléologique et revient d'ailleurs, à la fin de cette première section, sur l'inachèvement pour proposer de « repenser l'inachèvement » à nouveaux frais, en une sorte de bilan sur la question après les synthèses proposées, depuis la parution de son livre, par Michel Crouzet et Philippe Jousset. L'inachèvement n'est pas considéré comme un échec et « les raisons des inachèvements changent à mesure que l'auteur vieillit » (p. 149). Cette première partie s'intéresse à Stendhal « en tout genre », au fur et à mesure des choix génériques de Stendhal qui suivent la courbe de sa vie : théâtre, journal de voyage, essai sur l'amour, autobiographie, roman (La Chartreuse de Parme), texte hybride et singulier des Privilèges. La deuxième partie, thématiqueet qui n'échappe pas à une certaine dispersion-, s'intéresse à des objets aussi divers que la religion, la chasse, les « bois et forêts », le rapport entre économie politique et roman ou encore le bon usage de la biographie pour éclairer le texte stendhalien (« texte et auteur »), en une sorte de « retour à l'auteur » qui n'est pas étranger aux questions que se pose la critique à ce moment-là (l'article date de 2010), après des années de formalisme auquel Jean-Jacques Hamm n'a pas été tout à fait insensible en son temps. L' « auteur » est, dans cet esprit, une construction textuelle, et même si les réticences sont grandes à « remonter le courant vers Beyle » (p. 251), il se dégage de ce très bel article plus subjectif que les autres sans doute, une figure très touchante de ce sujet-Beyle considéré « au delà de ses masques » comme « un homme engagé dans un combat secret, un homme aussi profondément marqué de solitude » (ibid.). Ces remarques sont toujours fondées sur un examen très attentif du texte stendhalien et partent toujours de l'oeuvre pour éclairer la biographie (et non l'inverse) parce que « la biographie peut difficilement accéder à ce que l'auteur cache ». C'est ainsi que la « démarche archéologique » est privilégiée, au détriment de la « causalité psychologique » et que l'inachèvement, revisité une nouvelle fois à l'aulne de ces principes, est une « manière d'être » (p. 252), « un habitus stendhalien » (p. 254). Depuis la typologie un peu sèche des premiers textes sur le sujetmais nécessaire pour cerner la notion et conforme à l'esprit du temps -, l'inachèvement devient une sorte d'anthropologie et il est la mesure à laquelle s'estime et se mesure le parcours de Jean-Jacques Hamm. Enfin, une troisième partie, intitulée « Écriture » s'intéresse aux pas de côtés de l'écriture stendhalienne, que ce soit le masque, l'écart, le déplacement (« jeux et enjeux de l'épigraphe chez Stendhal »), la « dénégation », la « réticence » ou la « langue sacrée » qui réserve son texte aux initiés choisis, à ces Happy few sur lesquels tant de lignes ont été écrites.

Le recueil se clôt sur un article inédit qui sert en quelque sorte de conclusion à l'ensemble (« Une autre lecture. Concordances et répétitions ») : d'une part, Jean-Jacques Hamm trace des pistes, des « perspectives ouvertes » sur un sujet actuel, en considérant l'intérêt et les limites de la statistique des textes littéraires, d'autre part, en une sorte de bilan

sur son parcours de chercheur, il réfléchit sur sa propre pratique des outils informatiques appliqués à la littérature (il est l'auteur d'une table de Concordances des Romans et Nouvelles en quinze tomes, parus de 1991 à 2005 chez Georg Olms Verlag).

Ce volume de synthèse retrace donc l'itinéraire d'un chercheur dont le questionnement est sans cesse en éveil et qui n'hésite pas à revenir sur certaines propositions autrefois énoncées et à les nuancer, à les moduler. Mais la démarche reste essentiellement orientée vers une poétique diachronique des textes, genre et statut confondus, dans le sillage de Gérard Genette et de Jean-Pierre Richard (pour l'aspect thématique de son travail) : il s'agit de « dégager des invariants textuels ou un ensemble de figures dominantes exemplaires » (p. 12). Malgré ce credo textualiste annoncé dès l'introduction, qui occulte largement le contexte particulier dans lequel a vécu l'auteur, certaines échappées plus récentes, ouvrent le propos sur un Stendhal plus humain et plus incarné. Jean-Jacques Hamm affirme, lui aussi, comme Gérard Genette 1 , que, chez Stendhal, tout est à lire, l'oeuvre étant « comme un continent, un archipel de textes, un vaste chantier où l'auteur se mesure à différentes matières, à différents genres, sans jamais choisir la clôture définitive d'une identité unique » (p. 11). Le corpus de cet ouvrage reprend donc l'ensemble de la production stendhalienne, et c'est l' « oeuvre » dans son entier, par-delà les distinctions de genre et d'époque que croise l'auteur de ce recueil qui a le mérite de reconstituer un cheminement (le sien propre mais aussi celui de Stendhal) en constante évolution. Même si l'ensemble n'échappe pas à certaines redites, inévitables dans ce genre de florilège, il donne une bonne idée de la variété des sujets qu'a traités Jean-Jacques Hamm tout au long de sa carrière et de son long compagnonnage avec un auteur qu'il connaît parfaitement. On a donc là un livre très stimulant et construit de manière critique, n'hésitant pas à revenir sur des idées jadis énoncées, en un « entretien infini » (p. 11) avec l'auteur d'élection.

Catherine Mariette

Litt&Arts UMR 5316 Université Grenoble-Alpes/CNRS 1 Gérard Genette écrivait déjà en 1969 que « le texte stendhalien, marges et bretelles comprises est un » (« Stendhal », dans Figures II, Paris, Seuil, 1969, p 169).