Pierre Castéran
email: casteran@labri.fr

Vincent Filou
email: filou@labri.fr

Mohamed Mosbah
email: mosbah@labri.fr

Formal Proofs of Local Computation Systems 1

This paper describes the structure of a library for certifying distributed algorithms, contributed by Pierre Castéran and Vincent Filou. We formalize in the Coq proof assistant the behaviour of a subclass of local computation systems, namely the LC0 graph relabeling systems. We show how this formalization allows not only to build certified LC0 systems, but also study the limitations of their control structure.

Introduction

Local computations on graphs, and particularly graph relabeling systems, have been introduced in [START_REF] Billaud | Graph rewriting systems with priorities[END_REF] as a suitable tool for encoding distributed algorithms, for proving their correctness and for understanding their power. In this model, a network is represented by a graph whose vertices denote processors, and edges denote communication links. The local state of a processor (resp. link) is encoded by the label attached to the corresponding vertex (resp. edge). A relabeling rule is a rewriting rule which has the same underlying fixed graph for its left-hand side and its right-hand side, but with an update of the labels. According to its own state and to the states of its neighbours, each vertex may decide to realize an elementary computation step. After this step, the states of this vertex, of its neighbours and of the corresponding edges may change according to some specific computation rules.

In the Visidia [START_REF] Visidia | [END_REF] research project, we are interested in formal specification and formal proof of local computation systems. This activity consists in giving a formal semantics to these systems, develop tools for the certification of such algorithms : proof of invariants, proof of termination, and also compare the computational power of various subclasses of local computation systems or other kinds of distributed computation paradigms. The Coq proof assistant [START_REF]The Coq Proof Assistant Reference Manual[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF] has been chosen for this task.

In this paper, we focus on a particular class of computation rules: LC0 rules. An LC0-rule performs a computation on two adjacent nodes of the network. It corresponds to a rendez-vous [START_REF] Bauderon | From local computations to asynchronous message passing systems[END_REF][START_REF] Litovsky | Different local controls for graph relabelling systems[END_REF][START_REF] Litovsky | Graph relabelling systems and distributed algorithms[END_REF] between two nodes. This class of computation corresponds to the client-server model employed in most network applications. This paper describes a first modelization in Coq of LC0-relabeling systems. Section 3 presents the fundamental notions on graph Relabeling systems, illustrated by two simple examples : the distributed computation of a connected graph's spanning tree, then an election algorithm working on any tree. Section 4 shows how Coq's type system has been used to represent LC0-relabeling systems, and a brief overview of proof techniques. Section 5 presents some properties shared by all LC0 systems, which allow to prove some specifications are not realizable by such systems without some initial knowledge (section 6). Section 7 shows briefly the present structure of our Coq libraries. Finally, the directions or future work are sketched in section 8.

Related Work

The certification of distributed algorithms using a theorem prover has been the subject of a quantity of studies. Closest to our study, the work of Ching-Tsung Chou [START_REF] Chou | Mechanical verification of distributed algorithms in higher-order logic[END_REF] aims at mechanicaly proving properties of distributed algorithms using Higher-Order Logic. In this work, the author uses a notion of simulation to carry out the proof of correctness of an algorithm propagating information through a network. Qiao Heiyan has been working on a methodology for proving distributed algorithms in type theory, using the Agda theorem prover [START_REF] Haiyan | Testing and proving distributed algorithms in constructive type theory[END_REF]. The UNITY language has also been used [START_REF] Thirioux | Etude comparative de deux techniques de preuves de programmes unity[END_REF] to prove the security properties of distributed algorithm in Coq. Bezem, Bol and Groote [START_REF] Bezem | Formalizing process algebraic verifications in the calculus of constructions[END_REF] used the Coq proof assistant for proving equalities between terms of a process algebra. Leu also cite the work of Gascard and Pierre [START_REF] Gascard | Formal proof of applicatons distributed in symmetric interconnexion networks[END_REF] on formal proofs of parallel programs on symmetric interaction networks.

In [START_REF] Cansell | Logics of Specification Languages[END_REF], Cansell and Méry show how to get local computation systems from their specification through a sequence of refinements. They use for this purpose the Event-B method and the Rodin tool [START_REF]Event-B and the Rodin Platform[END_REF]. The specification is encoded by an abstract machine which computes in one big step a final state which satisfies the specification, the distributed algorithm being obtained as the last step of the refinement chain. The class of algorithms addressed in their work is exactly the same as ours. Examples of developed algorithms using this approach can be found in [START_REF] Tounsi | A Refinement Approach for Proving Distributed Algorithms : Examples of Spanning Tree Problems[END_REF]. In a few words, one could say that their approach is a kind of top-down development methodology, whilst ours tries to get properties from the language used to program local computation systems.

Graph Relabeling Systems for Encoding Distributed Algorithms

In this section, we give a few definitions of local computations, and particularly of graph relabeling systems. As usual, a network is represented by a graph whose vertices stand for processors and edges for (bidirectional) links between processors. At every time, each vertex and each edge is in some particular state and this state will be encoded by a vertex or an edge label.

According to its own state and to the states of its neighbours, each vertex may decide to realize an elementary computation step. After this step, the states of this vertex, of its neighbours and of the corresponding edges may have changed according to some specific computation rules. Let us recall that graph relabeling systems satisfy the following requirements:

(C1) they do not change the underlying graph but only the labeling of its components (edges and/or vertices), the final labeling being the result, (C2) they are local, that is, each relabeling changes only a connected subgraph of a fixed size in the underlying graph, (C3) they are locally generated, that is, the applicability condition of the relabeling only depends on the local context of the relabeled subgraph.

For such systems, the distributed aspect comes from the fact that several relabeling steps can be performed simultaneously on "far enough" subgraphs, giving the same result as a sequential realization of them, in any order. A large family of classical distributed algorithms encoded by graph relabeling systems is given in [START_REF] Bauderon | From local computations to asynchronous message passing systems[END_REF]. This approach has proved itself very well suited to obtain theoretical results on the impact of the geography of a network on algorithms [START_REF] Mazurkiewicz | Distributed enumeration[END_REF][START_REF] Godard | A characterization of families of graphs in which election is possible[END_REF][START_REF] Godard | Characterizations of classes of graphs recognizable by local computations[END_REF].

In order to make the definitions easy to read, we give in the following an example of a graph relabeling system for computing a spanning tree, and an example of a graph relabeling system to elect a node in a tree. Then, the formal definitions of local computations will be presented.

Distributed computation of a spanning tree

Let us first illustrate graph relabeling systems by considering a simple distributed algorithm which computes a spanning tree of a network. Assume that a unique given processor is in an "active" state (encoded by the label A), all other processors being in some "neutral" state (label N) and that all links are in some "passive" state, represented by the boolean f . The tree initially contains the unique active vertex. At any step of the computation, an active vertex may activate one of its neutral neighbours and mark the corresponding link which gets the label t. This computation stops as soon as all the processors have been activated. The spanning tree is then obtained by considering all the links with label t.

An elementary step in this computation may be depicted as a relabeling step by means of the relabeling rule R, given in Figure 1, which describes the corresponding label modifications (remember that labels describe processor status):

f t R : A N A A Figure 1:
The relabeling rule R Whenever an A-labeled node is linked by a f -labeled edge to an N-labeled node, then the corresponding subgraph may rewrite itself according to the rule.

A sample computation using this rule is given in Figure 2. Relabeling steps may occur concurrently on disjoint parts on the graph. When the graph is irreducible, i.e no rule can be applied, a spanning tree, consisting of t-edges labeled edges, is computed.

A A A A f f f f t t t N N A A A A A A f f t t t t t A N N N N N A A f t f f f f f f f f f f f f N N N N A A A f f f f t t N N A A A A A f f t t t t N f f N Figure 2:
Distributed computation of a Spanning Tree

Vertex Election in a Tree

The aim of an election in a graph is to choose exactly one vertex among the set of all its vertices. This vertex becomes elected and is called the leader of the graph. In our framework, this problem can be formalized in the following way. We say that a relabeling system (as will defined formally in the following section) solves the election problem for a class C of graphs if it is noetherian and if the following conditions hold :

• Any vertex of G may know if it is already elected or beaten, or still ignores this result

• Once a vertex is beaten or elected, its situation cannot change anymore,

• There is at most one elected vertex in the graph

• When no rule can be applied, all vertices are either beaten or elected Let us present a graph relabeling system allowing to elect a vertex in a tree (see Figure 3).

The alphabet for labeling the vertices is the set of natural numbers N augmented with a new element called "N". Intuitively we interpret N as "beaten", 0 as "elected", and any strictly positive integer d as "still ignoring the result". We do not label the graph's edges.

Initially, each vertex v is labeled with its degree in the graph. The set of rules we consider is the union of all replacements depicted in figure 3 for any d ∈ N.

The intuitive behaviour of our election system can be described as follows : let us associate to any state s the subgraph G s determined by the N-labeled vertices of G. In fact any computation step reduces to erasing some "pendant" edge (i.e. having at least an extremity of degree 1 w.r.t. G s ) from G s .

We prove two invariants of the system :

• in any reachable state s, any N-labeled vertex measures the degree of v with respect to G s ,

• in any reachable state s, G s is a tree.

From the invariant above, we infer that in a reachable state where no rule can be more applied (an irreducible state), there exists a unique vertex labeled 0 (hence elected) whilst other vertices of G are N-labeled (hence beaten).

N d d+1

R :

Figure 3: Rules for the election of a node in a tree

Formal Definitions of Graph Relabeling Systems

We consider only connected graphs whose vertices [resp. edges] are labeled with labels from a possibly infinite alphabet L v [resp. L e ]. We call state (or labeling) any pair s of two functions λ s :

V (G) → L v and ρ s : E(G) → L e .
Now we introduce the formal definition of a graph relabeling rule.

Definition A (graph) relabeling rule is a triple r = (G r , s r , s ′ r ) such that (G r , s r ) and (G r , s ′ r ) are two labeled graphs. The labeled graph (G r , s r ) is the left-hand side and the labeled graph (G r , s ′ r ) is the right-hand side of r.

If the graph G r is isomorphic to the graph k2 (which consists of two vertices connected by an edge), we say that the relabeling rule is of type LC0.

The intuitive notion of computation step will then correspond to the notion of relabeling step: Definition A r-relabeling step is a 5-tuple (G, s, r, ϕ, s ′ ) where r is a relabeling rule and ϕ is both an occurrence of (G r , s r ) in (G, s) and an occurrence of (G r , s ′ r ) in (G, s ′ ).

Intuitively speaking, the labeling s ′ of G is obtained from s by modifying all the labels of the elements of ϕ(G r , s r ) according to the labeling s ′ r . Such a relabeling step will be denoted by (G, s)→ r,ϕ (G, s ′ ).

This notation can be generalized to (G, s)→ R (G, s ′ ) (making abstraction of the occurrence φ and the rule r ∈ R), and to (G, s)→ * R (G, s ′ ) (reflexive and transitive closure of → R ). This last notation expresses the notion of finite computation according to the considered set R of rules.

The computation stops when the graph is labeled in such a way that no relabeling rule can be applied:

Definition A labeled graph (G, s) is said to be R-irreducible if there exists no occurrence of (G R , s R ) in (G, s) for every relabeling rule R in P .
Definition Finally, a graph relabeling system is a tuple S gathering the following information :

• Two alphabets for labeling vertices and edges (respectively L v and L e ),

• A set R of relabeling rules,

• A class C of graphs, the system is assumed to work on,

• A function I which associates to each graph G in C a set I G of initial states

We will use the abbreviation (G, s)→ * S (G, s ′ ) for (G, s)→ * R (G, s ′ ). We will say that s ′ is reachable from s. If i ∈ I G and (G, i)→ * R (G, s ′ ), we will simply say that s ′ is reachable.

In this paper, we consider only rules of type LC0; in fact there are other types (see [START_REF] Bauderon | From local computations to asynchronous message passing systems[END_REF][START_REF] Litovsky | Graph relabelling systems and distributed algorithms[END_REF]) considered in our future developments, mainly LC1 and LC2. Both of them are defined when G r is isomorphic to a star graph (called also a ball of radius one). Roughly speaking, in an LC1 computation step, the label attached to the center of the star is modified according to some rules depending on the labels of the star, labels of the leaves are not modified. In an LC2 computation step, labels attached to the center and to the leaves of the star may be modified according to some rules depending on the labels of the star.

Types for Representing Graph Relabeling Systems

We show how the rich type system of Coq [START_REF]The Coq Proof Assistant Reference Manual[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF] allow us to represent graph relabeling systems and their specification, and some proofs about the LC0 class.

Labeled Graphs

Non-oriented graphs are encoded with the help of the FSets library, contributed by Pierre Letouzey for Coq's standard library. Let us call Pregraph any pair G of a finite set of vertices V (G) and a finite sets of edges E(G).

The FSets library is compatible with Coq's setoid feature, thus we consider as equivalent any pair of edges (v, v ′ ) and (v ′ , v). Some predicates defined on PreGraph define the set of graphs (pregraphs which satisfy the proposition) (E(G) ⊆ V (G) × V (G)), of simple graphs (self-loop free), acyclic, connected graphs, etc.

We do not provide a type for representing directly labeled graphs. For simplicity's sake, we define some types for labelings as follows :

• We consider two non empty types L v (for vertices' labels) and L v (for edges' labels). In the spanning-tree example of section 3.1, we use an inductive type AN with two constructors A and N for vertex-labeling and the pre-built type bool for edge-labeling. Notice that any type with decidable equality is well suited for labels.

• A state s is any pair of a vertex-labeling λ s and an edge-labeling ρ s , where λ s is finite map from the type of vertices to L v (similarly for ρ s ). In general we consider only states where the functions λ s and ρ s are total (we say that "s covers G ".)

• Finally, a labeled graph is any pair (G, s) where s is a state for G.

In our Coq development, we denote by " state L v L e " the type of states using the alphabets L v and L e .

Graph Relabeling Relations

A Graph relabeling relation for a graph G is any binary relation → between states,such that if s covers G and s → s ′ , then s ′ covers G. Notice that this condition corresponds to the C1 requirement of section 3. Graph relabeling relations inhabit the dependent type " GR L v L e G "1 for graph relabelings operating on G. Notice that G is in last position, so we cannot define types for labeling knowing already the graph G. The task of building a distributed algorithm using graph relabeling amounts to choose two types is building some term of type L v and L e , then build a term S inhabiting the dependent product " ∀ G, GR L v L e G ".

Let us consider for instance an algorithm S of spanning-tree computation. Its correctness can be expressed as follows :

Let G be any simple, connected graph; for any initial state i,

• any rewriting sequence starting from i terminates, and

• any irreducible state s reachable from i determines a spanning tree of G

The graph G is the parameter of S. The predicate " to be a simple, connected graph" characterizes the class of graphs it is supposed to work on. Notice that this "specification" is still informal ; we must make precise the notion of initial state, and the verb "determines". For the latter, the meaning is simply "get a function r from labeled graphs to graphs, such that if s is any irreducible, reachable state w.r.t. S(G), then r(G, s) is a spanning tree of G."

LC0 Systems

We present a formal representation of a LC0 System; throughout this section, the non empty types L v and L e are fixed; we will use the notation Σ as an abbreviation for the type " state L v L e ".

LC0 Rules

As said in section 3.3, LC0 relabeling rules can be represented as a relabeling relation on the graph k2. Such a relation can be represented as a binary relation R on the product type

L v × L e × L v .
To be more precise, we encode any LC0 set of rules as a 6-ary predicate whose arguments as are follows: By convention, we name the vertices of k2 as c (for "center") and v (for "voisin", french translation of "neighbour").

Embedding into a Graph Relabeling Relation

Let R be a set of LC0-rules over the types L v and L e . It is easy to embed R into a relabeling relation over any graph G : Let s and s ′ be two states covering G; (G, s)→ R (G, s ′ ) if there exists two adjacent vertices c and v of G, such that

• the proposition R(λ s (c), λ s (v), ρ s (c, v), λ s ′ (c), λ s ′ (v), ρ s ′ (c, v)) holds,

and

• s and s ′ coincide everywhere except on the vertices c,v and the edge (c, v)

Graph Classes and Initial States

A LC0 relabeling system is supposed to perform some computations on some class C of graphs, starting from some initial state. In section 4.2 we presented a graph class as any predicate P defined on graphs.

In additon to its sets of rules, a graph relabeling system must determine a set of possible initial states for any graph G which belongs to C.

A Type for LC0 Systems

Putting all this information together, we can define a type LC0 for LC0systems as a dependent structure containing the following fields :

• Two non empty types L v and L e ,

• A graph class C : PreGraph→Prop,

• A family of sets of initial states I : PreGraph→(Σ→Prop)

• A LC0-set of rules R : L v →L e →L v →L v →L e →L v →Prop.

Proof Techniques for LC0 Systems

Let S be a LC0-system described as above. There are a few kinds of statement one may have to prove about S.

Invariants

An invariant of S is any relation I on states such that (G, i)→ * R (G, s) implies I i s for any graph G of the considered class C, any initial state i ∈ I G .

Let us consider for instance the invariants of the spanning tree algorithm: For writing these invariants, we need an auxiliary definition : Let G be a graph, and s be some state, then G A (s) is the subgraph of G containing all the vertices of G such that λ s (v) = A and the edges of G such that ρ s (e) = t.

Thus the invariants we prove are the following ones :

edge inv: For each edge of e of G, if at least one of e's extremities is labeled by N in the state s, then ρ s (e) = f,

tree inv: G A (s)

is a tree,

ExA: There exists at least some vertex v of G such that λ s (v) = A.

Proof techniques for invariants are quite usual : we prove that they are satisfied by any initial state, and preserved by the relation → R . The proof of this preservation is helped by specialized inversion tactics, which infer from some hypothesis (G, s) → R (G, s ′ ) the equalities of section 4.3.2.

Termination

The usual proof technique for termination can be very simplified when dealing with LC0-systems. If we associate to any label l of L v and L e some value µ(l) in a well-founded domain (D, <) , and if + is an associative, commutative and monotone operation on D, then it is enough to check the inequality µ(x ′ ) + µ(y ′ ) + µ(z ′ ) < µ(x) + µ(y) + µ(z), whenever R x y z x ′ y ′ z ′ holds. For instance, if we associate 1 to the label N, and 0 to any other label, the proof of termination of the spanning-tree computation is simply a proof of 0 < 1.

Properties Shared by all LC0 Systems

It is important to consider generic properties of the LC0 class of local computation systems. This is made possible by Coq's type system, which allows to quantify on the types for labeling, on the function which builds initial states, and the sets of LC0-rules.

First, LC0-systems are consistent w.r.t. the theoretical model by Godard and Métivier [START_REF] Godard | A characterization of classes of graphs recognizable by local computations with initial knowledge[END_REF] : If two labeled graphs (G, s) and (G ′ , s ′ ) are isomorphic, then any LC0-system S has the same behaviour on both labeled graphs.

Other properties implement a common scheme : from some computation on a labeled graph (G, s), build a computation for another appropriate labeled graph (G 1 , s 1 ) (with respect to the same relabeling system).

Extending a Computation to a Bigger Graph

The first case (lemma LC0:extends_computation), deals with the case where (G, s) is a labeled subgraph of (G 1 , s 1 ) (intuitively (G 1 , s 1 ) is obtained from (G, s) by adding some labeled vertices and edges). Then for any computation (G, s) → R (G, s ′ ) there exists a computation (G

1 , s 1 ) → R (G 1 , s ′ 1 ) where (G, s ′ ) is a labeled subgraph of (G 1 , s ′ 1 )
. In other words, the LC0system S can "ignore" the extra edges and vertices and perform the same computations in G and G 1 .

This property is used in Section 6.1 for proving that no LC0-system can be used to compute the degree of the underlying graph's vertices.

Notice that this property is clearly false for LC1 and LC2-systems, since their rules' guards explore the neighbourhood of any vertex. It is then possible to consider some LC1 or LC2-guard which becomes false if some new neighbour is added to some vertex.

Composing Computations

Let (G, s) be a labeled graph. Let us consider two disjoint labeled-subgraphs of G : (G 1 , s 1 ) and (G 2 , s 2 ), and two computations (

G 1 , s 1 ) → R (G 1 , s ′ 1 ) and (G 2 , s 2 ) → R (G 2 , s ′
2 ). Then we can build a computation (G, s) → R (G, s ′ ) where (G 1 , s ′ 1 ) and (G 2 , s ′ 2 ) are labeled subgraphs of (G, s ′ ). This property is used in the proof of 6.2. When we extend this property to LC1 or LC2 systems, we will have to consider some stronger constraints than "G 1 and G 2 are disjoint" : if we allow some edge (v 1 , v 2 ) to link G 1 and G 2 , any state change in v 1 can affect rule guards in G 2 . Thus G 1 and G 2 will have to be "distant enough".

Computational Power of LC0 Systems

LC0 algorithms form only a subfamily of local computation systems. It is thus interesting to consider the limitations of this class of algorithms. In this section, we present two examples of specifications, which cannot be realized by any LC0-system under some "reasonable" conditions (a term that will be explicited below).

Computing the Vertices' Degree

Let us consider for instance the following statement :

No LC0 algorithm can compute the degree of the underlying graph's vertices

We have to make this statement more precise in order to prove it : There exists no types L v and L e , no function f : L v →option N, no set of LC0-rules, no "reasonable" family of set of initial states I, such that for any graph G, :

• for any reachable state s, any vertex v of G, if f (λ s (v)) = Some d, then the degree of v in G is d,

• for any initial state i, there exists some state s reachable from i, such that f (λ s (v)) = Some d, for some d.

It remains to make more precise which sets of initial states we have to consider. We say that a family I of type " PreGraph→(Σ→Prop) " is extendable if for any pair of graphs G and G 1 such that G is a subgraph of G 1 , then any state i in I G can be extended in a state i 1 ∈ I G ′ .

Intuitively, any initial state for a graph G can be built incrementally. This is a the case of randomly built initial states, or initial states which attribute a constant label to each vertex [resp. edge]. The proof is done by contradiction. Suppose that some LC0-system allows to compute the degree of any vertex of any graph, with an extendable family I of sets of initial states. Let us consider the graphs G and G 1 as in figure 4. Then there exists some computation starting from some initial state i ∈ I G , reaching some state s, where f (λ s (0) = Some(deg G (0)). Then there exists some initial state i 1 for G 1 which extends i, and, by the property 5, some state s 1 which extends s and is reachable from i 1 . The following equalities show that our hypotheses lead to a contradiction.

Some 2 = Some(deg G 1 (0)) = λ s 1 (0) = λ s (0) = Some(deg G 1 (0)) = Some 1 6.1.1 Important Remark
Notice that the statement we proved deals with a local knowledge of the each vertex's degree at any time of the computation. Let us consider the following change of our specification :

• for any irreducible reachable state s, any vertex v of G, if f (λ s (v)) = Some d, then the degree of v in G is d,

• for any initial state i, there exists some state s reachable from i, such that f (λ s (v)) = Some d, for some d.

We can easily build a LC0-algorithm for computing the degree of each vertex.

• Vertices are labeled by a natural number (initially 0), and edges by booleans (initially f ),

• The unique rule applies to any edge labeled by f , increments its extremities, and relabels this edge with t.

Notice that this example doesn't contradict at all the result shown in section 6.1. There is a big difference between a local knowledge of a vertex's degree, and using a global knowledge about irreducibility of all the graph's state.

Initial States for an Election Algorithm

In section 3.2, we presented a LC0 election algorithm. Its correction relies on the fact that its initial states encode every vertex's degree in the graph.

A very natural question is : "is this initial knowledge necessary" ? A partial answer is given if we determine some properties of the function I which associates to any tree T the set of initial states allowed for starting the computation.

Let I be a family of set of initial states allowing to build a configuration like in section 5.2, where s, [resp. s 1 , s 2 ] are initial states taken in I G [resp.

I G 1 , I G 2 .
Let us assume that some LC0 election algorithm S works for, say, trees, using such a family I. Consider the graph P 4 , decomposed in two disjoints Figure 5: A graph with two disjoint subgraphs subgraphs isomorphic to P 2 linked by an edge (fig 5). Applying the property in section 5.2, we can easily reach a state where two vertices are elected, which contradicts the election specification.

Among the families I we can consider for that purpose, we can cite :

• Any state defined over the types L v and L e can be an initial state

• There are some constants l v : L v and l e : L e such that every vertex [resp. edge] is labeled l v [resp. l e ].

• Any state where no vertex is elected or beaten yet.

About the Development in Coq

The libraries on graph relabeling systems work with the version 8.2 of the Coq proof assistant, and can be downloaded at www.labri.fr/∼casteran/Penda. These libraries are still in development, and some definitions, theorem statements and specialized tactics will be subject to change. Some proofs are very long and will be shortened too. The present (March 2009) representation of unordered edges led to very long proofs. It will be replaced in the next release by another representation relying on reflection.

We present briefly the structure of this library, which will be quite stable, and will be extended to wider classes of local computation systems. The library is divided in four parts :

Library Prelude

This part contains some additional definitions and lemmas, extending Coq's standard library.

We mainly extend Letouzey's FSets and FMaps libraries . The module AccP is a slight extension to Wellfounded, dealing with relations of the form P a ∧ R a b ∧ P b.

Finally, Monoids defines the structure of [commutative] monoid on a setoid.

Library Graphs

In our development, we consider unoriented finite graphs, represented with finite sets of vertices and edges. Usual notions such as pathes, cycles, connexity are also defined. Since mechanizing graph theory is not the main purpose of our work, we often use in our proofs of algorithms some folklore lemmas which will be proven when there are more time or people to do it. At present the module Graph_Admitted contains only two lemmas, used in the proof of the election algorithm:

• Acyclic_leaf : Any non empty, acyclic graph G has at least a vertex of degree 0 or 1,

• remove_leaf_tree : Let G be a tree, x and y two adjacent vertices of G, where x is a leaf of G. Then removing the edge (x, y) from G results in a tree.

The module GraphLabeling defines the notion of labeled graph.

Library GRS (Graph Relabeling Systems

The sublibrary GRS contain general definitions about Graph Relabeling relationsé: invariants, termination, etc. A specialized module LC0 is devoted to the LC0 class of graph relabeling systems, and contains specialized tactics, as well as the proofs of the theorems presented in section 5.

Library Examples

The Examples directory contains some cases studies. Two of them are examples of algorithm certification through invariant proofs.

Spanning Tree Computation

The module SpanningTree_Specification contains a formal specification of any graph relabeling system in which any irreducible states allows to get a spanning tree of the input graph.

The module SpanningTree_LC0 contains a certified implementation of this specification, which works on any simple and connected input graph.

Vertex Election

The module Election_Specification contains a formal specification of any election algorithm. It is the formal translation of the informal presentation of section 3.2.

The correction of the algorithm of election in a tree is in the module Election_Tree_LC0.

Limitations of LC0 Rules

The module No_Degree_LC0 contains the formal proof presented in section 6.1 and No_Election_LC0 the proof presented in section 6.2.

Conclusion and Future Work

This works shows how to design a framework for reasoning on a wide class of local computation systems. Such a framework allows two kinds of activities :

• Formal proofs of particular distributed algorithms,

• Proofs of properties of entire classes of such systems, allowing expressive power comparison, including some proofs of the impossibility to realize a given specification within a given class of systems. This work will be continued in the following directions :

• Automation of parts of the proofs, including termination [START_REF] Contéjean | Mechanically proving termination using polynomial interpretations[END_REF], proof by reflection,

• Extension to more classes of local computation systems, more generally to other formalisms for distributed algorithmics,

• Use of the Why [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF] technology for generating proof obligations,

• Taking into account algorithm composition, probabilistic algorithms, etc.

  λ s (c) old label of the center c λ s (v) old label of the neighbour v ρ s (c, v) old label of the edge (c, v) λ s ′ (c) new label for the center c λ s ′ (v) new label for the neighbour v ρ s ′ (c, v)) new label for the edge (c, v) In other terms, we describe a kind of before/after relation describing the state change on k2. Let us take for instance the spanning tree rule : It is represented by an inductive predicate : Inductive R : AN → AN → bool → AN → AN → bool → Prop := R_intro : R A N false A A true.

Figure 4 :

 4 Figure 4: The degree of 0 in G is not equal to the degree of 0 in G 1

defined in the module GRS/GraphRelabeling

Acknowledgement We thank Yves Bertot, Dominique Cansell, Pierre Letouzey, Dominique Méry, Yves Métivier and Xavier Urbain for the helpful discussions and for many ideas used in this work.

* partly supported by ANR A3PAT ANR-05-BLAN-0146 and RIMEL ANR-06-SETIN-015 † partly supported by ANR A3PAT ANR-05-BLAN-0146 and RIMEL ANR-06-SETIN-015


Solène M Laville

Aymeric Couturier

Oriane Lambert

Marie Metzger

Nicolas Mansencal

Christian Jacquelinet

Maurice Laville

Luc Frimat

Denis Fouque

Christian Combe

Bruce M Robinson

Bénédicte Stengel

Sophie Liabeuf
email: liabeuf.sophie@chu-amiens.fr

Ziad A Massy
email: ziad.massy@aphp.fr

Christian Herpe

Maurice Jacquelinet

Ziad A Laville

Christophe Massy

Bruce M Pascal

Bénédicte Robinson

Céline Stengel

Karine Lange

Sophie Legrand

Marie Liabeuf

Elodie Metzger

Speyer

Ckd-Rein Investigators The

Thierry Hannedouche

Bruno Moulin

Sébastien Mailliez

Gaétan Le- Brun

Eric Magnant

Gabriel Choukroun

Benjamin Deroure

Adeline Lacraz

Guy Lambrey

Jean-Philippe Bourdenx

Marie Essig

Thierry Lobbedez

Raymond Azar

Hacène Sekhri

Mustafa Smati

Mohamed Jamali

Alexandre Klein

Michel De- Lahousse

Séverine Martin

Isabelle Landru

Eric Thervet

Philippe Lang

Xavier Belenfant

Pablo Urena

Carlos Vela

Dominique Chauveau

Viktor Panescu

Christian Noel

François Glowacki

Maxime Hoffmann

Maryvonne Hourmant

Dominique Besnier

An- Gelo Testa

François Kuentz

Philippe Zaoui

Charles Chazot

Laurent Juillard

Stéphane Burtey

Adrien Keller

Nassim Kamar

Urea levels and cardiovascular disease in patients with chronic kidney disease

Keywords: cardiovascular disease, chronic kidney disease, urea, uraemic toxin

What is already known about this subject?

• Chronic kidney disease (CKD) is now considered as a major worldwide public health problem and the death rate due to cardiovascular disease (CVD) is significantly higher in patients with CKD than in the general population. However, conventional cardiovascular (CV) risk factors do not appear to fully account for this elevated risk of CVD. • For many years, urea was considered to be a relatively inert, nontoxic molecule. But several studies have shown that urea is a direct and indirect uraemic toxin. Although the mechanisms of urea's direct toxicity still require further investigation, in vitro and in vivo studies have shown that uraemia modulates the smooth muscle cell's phenotype, induces the expression of pro-apoptotic family genes. Other studies have shown that urea has an indirect toxic effect via protein carbamylation, which interferes with the proteins' molecular and cellular functions and is associated with CKD progression after adjustment for conventional risk factors. However, it is still not clear whether serum urea levels are related to CV outcomes in patients with moderate-to-advanced CKD.

What this study adds?

• Among 2507 patients with CKD not receiving maintenance dialysis attending nephrology outpatient facilities, we showed that patients with moderately elevated serum urea were at high risk of developing adverse CV outcomes. The association was independent of CV risk factors including estimated glomerular filtration rate.

What impact this may have on practice or policy?

• Considering the toxic effect of elevated serum urea levels in the management of patients with moderate to advanced chronic renal failure is important, given the actual body of evidence. Given the dietary origin of a proportion of the urea in the circulation, nutritional therapy could be used to counter an elevation in urea levels. Interventional studies of various diets and their impacts on CV outcomes (and especially non-atheromatous events) in non-dialysed patients with CKD are warranted.

A B S T R AC T

Background. Elevated serum urea levels are common in moderate-to-advanced chronic kidney disease (CKD). Several studies have shown that urea is a direct and indirect uraemic toxin, especially with regard to cardiovascular disease. We sought to determine whether serum urea levels are associated with adverse cardiovascular events and death before renal replacement therapy (RRT) in patients with CKD. Methods. CKD-REIN is a prospective cohort of CKD nephrology outpatients not receiving maintenance dialysis. The 2507 patients included in the analysis were divided into three groups according to the baseline serum urea level (T1 <10.5, T2 10.5-15.1 and T3 ≥15.1 mmol/L). Cox proportional hazard models were used to estimate hazard ratios (HRs) for first atheromatous or non-atheromatous cardiovascular (CV) events and all-cause mortality before RRT. The models were adjusted for baseline comorbidities, laboratory data and medications.

Findings. Of the 2507 included patients {median [interquartile range (IQR)] age: 69 [61-77]; mean (standard deviation) estimated glomerular filtration rate (eGFR) 33.5 (11.6) mL/min/1.73 m2}, 54% had a history of cardiovascular disease. After multiple adjustments for CV risk factors (including eGFR), patients in T3 had a higher risk of atheromatous and non-atheromatous CV events than patient in T1 (n events = 451, HR [95% CI]: 1.93 [1.39; 2.69]). The adjusted HRs for death before RRT (n events = 407) were 1.31 [0.97; 1.76] and 1 .73 [1.22; 2.45] for patients T2 and those in T3, respectively. Interpretation. Our data suggested that urea is a predictor of CV outcomes beyond CV risk factors including eGFR.

INTRODUCTION

Chronic kidney disease (CKD) is now considered as a major worldwide public health problem [START_REF] Levey | Chronic kidney disease as a global public health problem: approaches and initiatives -a position statement from kidney disease improving global outcomes[END_REF]. It directly affects the overall burden of morbidity and mortality and its increasing prevalence is being driven primarily by population ageing and increases in the prevalence of diabetes, hypertension and obesity [START_REF] Jha | Chronic kidney disease: global dimension and perspectives[END_REF]. Although the death rate due to cardiovascular disease (CVD) is significantly higher in patients with CKD than in the general population [START_REF] Go | Chronic kidney disease and the risks of death, cardiovascular events, and hospitalization[END_REF][START_REF] Vanholder | Chronic kidney disease as cause of cardiovascular morbidity and mortality[END_REF], the underlying pathophysiological mechanisms are not fully understood. Indeed, conventional cardiovascular (CV) risk factors do not appear to fully account for this elevated risk of CVD.

Urea is a product of protein metabolism that is often used as a proxy for CKD severity and dialysis adequacy in clinical settings. For many years, urea was considered to be a relatively inert, nontoxic molecule. However, several studies have shown that urea is a direct and indirect uraemic toxin [START_REF] Massy | Reconsidering the lack of urea toxicity in dialysis patients[END_REF]. Although the mechanisms of urea's direct toxicity still require further investigation, in vitro and in vivo studies have shown that uraemia modulates the smooth muscle cell's phenotype and induces the expression of pro-apoptotic BCL-2 family genes; this might explain the elevated apoptosis rate observed in the arterial wall in uraemic patients [START_REF] Trécherel | Upregulation of BAD, a proapoptotic protein of the BCL2 family, in vascular smooth muscle cells exposed to uremic conditions[END_REF][START_REF] Shroff | Dialysis accelerates medial vascular calcification in part by triggering smooth muscle cell apoptosis[END_REF]. Furthermore, a high urea concentration in endothelial cell progenitor cultures has been associated with increased senescence and free radical formation [START_REF] D' Apolito | Urea-induced ROS accelerate senescence in endothelial progenitor cells[END_REF]. In a study of nephrectomized mice, inhibition of the urea transporter was associated with reductions in hypertension and cardiac fibrosis and an improvement in cardiac function [START_REF] Kuma | Inhibition of urea transporter ameliorates uremic cardiomyopathy in chronic kidney disease[END_REF].

Other studies have shown that urea has an indirect toxic effect via protein carbamylation [START_REF] Kalim | Protein carbamylation in kidney disease: pathogenesis and clinical implications[END_REF], which interferes with the proteins' molecular and cellular functions. Protein carbamylation is associated with CKD progression after adjustment for conventional risk factors [START_REF] Kalim | Protein carbamylation and chronic kidney disease progression in the chronic renal insufficiency cohort study[END_REF]. Furthermore, the exacerbation of vascular calcification by carbamylation [START_REF] Mori | Protein carbamylation exacerbates vascular calcification[END_REF], or atherosclerosis with lipoprotein carbamylation might explain the high incidence of CVD and mortality in CKD [START_REF] Apostolov | Chronic uremia stimulates LDL carbamylation and atherosclerosis[END_REF].

Thus, urea might contribute to the elevated CV risk in patients with CKD. However, no clinical studies we are aware of have reported an association between the occurrence of CV events (whether fatal or nonfatal) and serum urea levels in pre-dialysis patients with CKD. Thus, the objective of the present study was to determine whether serum urea levels are associated with adverse outcomes such as CV events (both atheromatous and non-atheromatous) and death before renal replacement therapy (RRT) in patients with CKD after adjustment for the estimated glomerular filtration rate (eGFR).

MATERIALS AND METHODS

Study design and participants

CKD-REIN is a prospective cohort study conducted by 40 nationally representative nephrology outpatient facilities in France. Details of the study protocol have been published [START_REF] Stengel | Risk profile, quality of life and care of patients with moderate and advanced CKD: The French CKD-REIN Cohort Study[END_REF]. Briefly, the main inclusion criteria are ≥18 years, a confirmed diagnosis of moderate or advanced CKD, an eGFR <60 mL/min/1.73 m2 and the absence of dialysis or transplantation. Between July 2013 and April 2016, 3033 patients were enrolled during a routine nephrology outpatient appointment and are actively followed up for 5 years at most. The recruitment of outpatients ensured that the study participants did not present with acute illness (such as acute kidney injury or digestive tract haemorrhage) on inclusion. Furthermore, all patients were receiving stable background therapy. The study protocol was approved by the institutional review board at the French National Institute of Health and Medical Research (INSERM; reference: IRB00003888) and was registered at ClinicalTrials.gov (NCT03381950).

For the purposes of the present analysis, we excluded patients with missing data for the serum urea level at baseline or who had an aberrant serum urea value (i.e. <2.5 or >100 mmol/L). To limit the effects of nonrenal factors on serum urea levels, patients who were on corticosteroids or had a history of metastatic cancer were excluded. Patients who had an eGFR <15 mL/min/1.73 m2 at baseline were also excluded, considering that they had reached the stage of kidney failure (Figure 1). A total of 2507 patients were analysed here.

Study data

Trained clinical research associates (CRAs) collected data from patient interviews and medical records at baseline and then annually. The patients' characteristics (age, sex and smoking status) were recorded and the patients were screened for a history of hypertension, diabetes, CVD or acute kidney injury (definitions in Supplementary data, Table S1). Blood pressure was measured, as were height and weight to calculate body mass index (BMI). All patients were prescribed a set of standard blood and urine tests (recommended by French health authorities for routine CKD care), with sample to be taken at their usual medical laboratory. Data on the serum creatinine, serum urea level, blood haemoglobin, serum albumin and albumin-or protein-to-creatinine ratio (Supplementary data, Table S1) were recorded. The GFR was estimated using the Chronic Kidney Disease Epidemiology Collaboration (CKD-EPI) creatinine equation and the isotope dilution mass spectrometry-traceable creatinine concentration determined in a Jaffe assay (in 38% of participants) or an enzymatic assay (in 57%; the assay type was unknown for 5%) [START_REF] Levey | A new equation to estimate glomerular filtration rate[END_REF].

Patients were asked to bring all their drug prescriptions for the preceding 3 months to the enrolment visit. The CRAs used an electronic case report form [linked to the international Anatomical Therapeutic and Chemical (ATC) thesaurus] to enter standardized ATC codes.

Longitudinal clinical data (nephrology consultations, hospital admissions, laboratory test results, medications and any transition to dialysis or transplantation) were collected every year from medical records and patient interviews.

Study outcomes

CV events were assessed carefully according to the Cardiovascular and Stroke Endpoint Definitions for Clinical Trials [START_REF] Hicks | Cardiovascular and stroke endpoint definitions for clinical trials[END_REF].

The primary endpoint was the occurrence of a first fatal or nonfatal atheromatous or non-atheromatous CVD. Fatal or nonfatal atheromatous CVD was defined as a composite of (i) death (fatal myocardial infarction or stroke), (ii) hospitalization for myocardial infarction, silent ischaemia, unstable angina, intrastent thrombosis, stroke or transient ischaemic attack, peripheral artery disease, percutaneous coronary intervention or coronary artery bypass graft, vascular surgery, or amputation and, (iii) revascularization for coronary or peripheral artery disease. Fatal or nonfatal non-atheromatous CVD was defined as a composite of (i) sudden cardiac death or death from heart failure, haemorrhagic stroke, or other CV causes, (ii) death associated with a CV procedure, such as noncoronary or peripheral vascular procedure, (iii) hospitalization for haemorrhagic stroke, heart failure, cardiac rhythm/conduction disorders, pulmonary embolism or deep vein thrombosis, valvular heart disease and, (iv) cardiac procedures such as valve prosthesis, cardioversion, implantation of a pacemaker and implantable cardioverter defibrillator.

The secondary outcomes included first major CV events (any CV death, myocardial infarction, stroke and hospitalization for heart failure) and all-cause death. Deaths before RRT were identified from medical records or reported by family members at the annual follow-up visit.

All the considered events occurred before RRT. RRT was defined in the present study as kidney dysfunction requiring initiation of chronic dialysis or preemptive transplantation (as identified from medical records or by linking to the French National Kidney Failure Registry) [START_REF] Couchoud | Rapport annuel 2017 -Réseau Epidémiologie[END_REF].

CV events were available for the first 3 years of follow-up at the time of analysis and so data were censored on the date of the patient's third annual follow-up visit, the date of the last followup before the third annual visit, the date of RRT or the date of death from a non-CV cause. Each death occurring during the 5-year follow-up period was used in the all-cause mortality model and the data were censored at the date of RRT or the date of the last follow-up.

Statistical analysis

The participants' serum urea levels were divided into tertiles (T1 <10.5, T2 10.5-15.1, T3 ≥15.1 mmol/L). The baseline characteristics were described for the overall population (n = 2507) and the subgroups (serum urea tertiles) and reported as the median [interquartile range (IQR)] or the mean [standard deviation (SD)] for continuous data (depending on the distribution) and as the frequency (percentage) for qualitative variables. An analysis of variance (ANOVA) or the Kruskal-Wallis test was used to compare continuous variables, depending on the data distribution and homoscedasticity. Incidence rates and 95% confidence intervals (CIs) for each event were computed as a function of the serum urea levels. For each outcome studied, we used cause-specific Cox models to estimate crude and adjusted hazard ratios (HRs) [95% CI] associated with the serum urea level (in tertiles). HRs were adjusted for relevant demographic variables and baseline comorbidities (preselected in a review of the literature for each outcome). Risks associated with serum urea were adjusted for age at baseline, sex, smoking status, baseline eGFR, urine albumin-or protein-to-creatinine ratio, BMI, diabetes, systolic blood pressure, history of CVD, anaemia, serum albumin, high-sensitivity C-reactive protein and prescriptions of diuretics, statins and antiplatelet agents at baseline. The risk of death before RRT was further adjusted for a history of acute kidney injury and prescription of a proton pump inhibitor at baseline. Each model's validity (according to the proportional hazard assumption) was checked by testing the Schoenfeld residuals.

We used penalized splines in fully adjusted Cox models to represent the functional relationship between serum urea and the CVD risk. As a sensitivity analysis, we built a cause-specific Cox model for each type of CVD outcome, i.e. an analysis of (i) fatal and nonfatal atheromatous CVD events and (ii) fatal and nonfatal non-atheromatous CVD events.

Missing covariate data were managed by multivariate imputation by chained equations (MICE) [START_REF] Van Buuren | mice: Multivariate Imputation by Chained Equations in R[END_REF]. The assumption whereby data were missing at random was plausible. By using the MICE package in R statistical software (version 4.0.3) [START_REF] Core | R: A Language and Environment for Statistical Computing[END_REF], we created 50 datasets (20 iterations). All covariates present in the Cox models and baseline serum bicarbonate were included in the imputation model. Fitted Cox models were generated for each dataset and pooled regression coefficients were obtained using Rubin's rules. All statistical analyses were performed with R software.

RESULT S

Characteristics of the patients at baseline

Of the 3033 patients, 2507 patients were analysed (Table 1). The median age was 69 years [61-77] and the mean (SD) eGFR was 33.5 (11.6) mL/min/1.73 m2; 54% of the patients had a history of CVD, 45% had diabetes and 38% had anaemia. The mean (SD) serum urea was 8.3 (1.5) for T1, 12.6 (1.3) for T2 and 20.3 (5.1) mmol/L for T3. We observed significant difference in eGFR levels and the albumin-or protein-tocreatinine ratio at baseline between the three groups. A strong negative correlation was found between serum urea and eGFR (r = -0.64). The BMI was significantly higher in patients in T3. Compared with patients in T1, patients in the other tertiles were more likely to have a history of CVD, diabetes, anaemia, diuretic use and/or acute kidney injury. Lower serum bicarbonates levels were found in patients in T3. The proportion of patients with heart failure at baseline was significantly higher in T3 (19%) than in T1 (9%) and T2 (16%) (P < 0.001, not shown).

Fatal and nonfatal atheromatous or non-atheromatous cardiovascular events

Of the 2507 patients, 451 experienced a first atheromatous or non-atheromatous CV event (fatal or nonfatal) over a median [IQR] follow-up period of 3.0 [2.2-3.1] years, leading to a crude incidence rate [95% CI] of 7.1 [6.4; 7.7] per 100 person-years (PY). The incidence rate was highest in patients in the third urea tertile (Supplementary data, Table S2, Figure 2). After multiple adjustments, the risk of fatal and nonfatal atheromatous or non-atheromatous CV events was found to be significantly higher for patients in T3 than in patients in T1 (HR [95% CI]: 1.93 [1.39; 2.69]; Figure 2, Supplementary data, Table S3). A nonsignificant trend towards a higher risk was also noted for patients in T2 (HR [95% CI]: 1.24 [0.93; 1.66]). Penalized spline regression showed that serum urea was linearly related to the CVD risk (Figure 3). The interaction between serum urea and heart failure was tested and turned out not to be significant (P = .15), as well as the interaction between serum urea and eGFR (P = .69).

A sensitivity analysis failed to show an association between the baseline serum urea level and atheromatous CV events (fatal or nonfatal) (Supplementary data, Table S4). In contrast, a significantly higher risk of non-atheromatous CV events S5).

Major CV events

Over the first 3 years of follow-up, 275 patients first experienced a major CV event. The crude incidence rate was FIGURE 3: Hazard ratio for fatal atheromatous or non-atheromatous cardiovascular events, according to the baseline serum urea level (mmol/L). The continuous line represents predictions with penalized splines in Cox models (95% confidence intervals). Ticks on the x-axis represent the distribution of the baseline serum urea level. Hazard ratios are adjusted for age at baseline, sex, smoking status, baseline estimated glomerular filtration rate, urine albumin-or protein-to-creatinine ratio, body mass index, diabetes, systolic blood pressure, history of cardiovascular disease, anaemia, serum albumin, high-sensitivity C-reactive protein and prescriptions of diuretics, statins and antiplatelet agents at baseline. FIGURE 4: Adjusted HRs for major cardiovascular events, according to the baseline serum urea level. HR, hazard ratio; CI, confidence interval. Adjusted for age at baseline, sex, smoking status, baseline estimated glomerular filtration rate, urine albumin-or protein-to-creatinine ratio, body mass index, diabetes, systolic blood pressure, history of cardiovascular disease, anaemia, serum albumin, high-sensitivity C-reactive protein and prescriptions of diuretics, statins and antiplatelet agents at baseline of diuretics, prescription of statins and prescription of antiplatelet agents at baseline.

FIGURE 5:

Adjusted HRs for death before renal replacement therapy according to the baseline serum urea level. HR, hazard ratio; CI, confidence interval. Adjusted for age at baseline, sex, smoking status, baseline estimated glomerular filtration rate, urine albumin-or protein-to-creatinine ratio, body mass index, diabetes, systolic blood pressure, history of cardiovascular disease, anaemia, serum albumin, high-sensitivity C-reactive protein, history of acute kidney injury, diuretic prescription, proton pump inhibitor prescription and prescriptions of statins and antiplatelet agents at baseline. [START_REF] Vanholder | Chronic kidney disease as cause of cardiovascular morbidity and mortality[END_REF].1 [3.6; 4.6] per 100 PY. The incidence rate was 3.5 times higher in patients in T3 than in patients in T1 (Supplementary data, Table S2, Figure 4). The adjusted HR [95% CI] for major CV events associated with the baseline serum urea level was 1.13 [0.77; 1.67] for patients in T2 and 1.94 [1.27; 2.98] for patients in T3 (Figure 4, Supplementary data, Table S6).

Death before RRT

Over a median follow-up period of 4.8 [3.3; 5.1] years in the CKD-REIN cohort, 407 patients died before RRT, leading to an incidence rate of 4.0 [3.6; 4.3] per 100 person-years (Supplementary data, Table S2, Figure 5). The adjusted HRs [95% CI] for death before RRT were 1.31 [0.97; 1.76] and 1.73 [1.22; 2.45] for patients in T2 and T3, respectively (Figure 5, Supplementary data, Table S7).

DISCUSSION

Our analysis of a large prospective cohort of CKD patients not receiving maintenance dialysis attending nephrology outpatient facilities showed that higher serum urea levels were associated with a higher incidence of adverse CV outcomes and a higher all-cause mortality rate. Our findings are in line with the current body of epidemiological evidence on kidney function biomarkers and the risk of CVD, and suggest that urea should be taken into account when seeking to predict and prevent CV disease in patients with CKD.

Several serum biomarkers [such as serum creatinine or urea, or blood urea nitrogen (BUN), which reflects only the nitrogen content of urea], are routinely used in clinical settings to evaluate kidney function. Urea is the main metabolite derived from dietary proteins and tissue protein turnover. The compound is almost exclusively excreted by the kidneys in the urine, after filtration in the glomerulus and a certain degree of reabsorption from the filtrate. Although several nonrenal factors affect the serum urea concentration [START_REF] Luke | Uremia and the BUN[END_REF], reduced urinary elimination of urea (due to CKD) is the main factor that increases serum urea levels. Volume depletion by diuretics or a decrease in the effective circulating volume induced by heart failure might contribute to the elevation of urea levels in our CKD patients. However, the fact that bicarbonate levels were significantly lower in T3 than in T1 (Table 1) tends to rule out volume depletion by diuretics. In contrast, the difference between the tertiles in the prevalence of heart failure suggests that the elevated urea levels could be due (at least in part) to a decrease in the effective circulating volume caused by heart failure.

Under normal conditions, the serum urea level ranges from 2.2 to 7.2 mmol/L (or 13-43 mg/dL) [START_REF] Vanholder | Urea and chronic kidney disease: the comeback of the century? (in uraemia research)[END_REF]. Patients in the first urea tertile in our study can be considered as having a normal level, those in the second tertile have a slightly elevated level and those in the third tertile have a moderately elevated level. During the course of the CKD, serum urea levels can easily reach or exceed 10 times the upper normal limit-especially when kidney failure occurs [START_REF] Vanholder | Urea and chronic kidney disease: the comeback of the century? (in uraemia research)[END_REF]. Until recently, urea was considered to be a biologically inert marker. However, studies of animal models of CKD have shown that the accumulation of urea is toxic [START_REF] Vanholder | Urea and chronic kidney disease: the comeback of the century? (in uraemia research)[END_REF].

CKD is a common disease and its prevalence will continue to increase in the coming years [START_REF] Jha | Chronic kidney disease: global dimension and perspectives[END_REF]. CVD is one of the leading contributors to morbidity and mortality in patients with CKD [START_REF] Thompson | Cause of death in patients with reduced kidney function[END_REF]. The limited effectiveness of most conventional risk factor modification strategies in patients with CKD may suggest that various metabolic pathways underlie the development of CVD in this population [START_REF] Gregg | Management of traditional cardiovascular risk factors in CKD: what are the data?[END_REF]. The results of animal studies suggest that several direct and indirect pathophysiological mechanisms underlie the relationship between urea levels and CV adverse events in CKD [START_REF] Massy | Reconsidering the lack of urea toxicity in dialysis patients[END_REF]. Uraemic conditions lead to the overexpression of proapoptotic genes in animal tissues and in cultured human vascular smooth muscle cells [START_REF] Trécherel | Upregulation of BAD, a proapoptotic protein of the BCL2 family, in vascular smooth muscle cells exposed to uremic conditions[END_REF]. Moreover, the urea levels found in the serum of CKD patients directly increase levels of reactive oxygen species (ROS) and oxidative stress in several types of cells [START_REF] D' Apolito | Urea-induced ROS generation causes insulin resistance in mice with chronic renal failure[END_REF][START_REF] Koppe | Urea impairs β cell glycolysis and insulin secretion in chronic kidney disease[END_REF][START_REF] D' Apolito | Urea-induced ROS cause endothelial dysfunction in chronic renal failure[END_REF]. Interestingly, endothelial progenitor cell number and function decrease with advancing CKD [START_REF] Krenning | Endothelial progenitor cell dysfunction in patients with progressive chronic kidney disease[END_REF], which might be due to the acceleration of senescence in endothelial progenitor cells by urea-induced ROS [START_REF] D' Apolito | Urea-induced ROS accelerate senescence in endothelial progenitor cells[END_REF]. In fact, these endothelial progenitor cells have a key role in the repair and maintenance of the vascular system [START_REF] Werner | Endothelial progenitor cells in health and atherosclerotic disease[END_REF]. Furthermore, there is a growing body of evidence on indirect toxic effects of urea via post-translational modifications of proteins; the resulting biochemical alterations might have an impact on CV outcomes [START_REF] Massy | Reconsidering the lack of urea toxicity in dialysis patients[END_REF][START_REF] Vanholder | Urea and chronic kidney disease: the comeback of the century? (in uraemia research)[END_REF]. Indeed, urea's dissociation products (e.g. cyanate) irreversibly carbamylate proteins [START_REF] Kraus | Carbamoylation of amino acids and proteins in uremia[END_REF] and so change the latter's physical properties and molecular and cellular functions. CKD is associated with elevated protein carbamylation [START_REF] Kalim | Protein carbamylation in kidney disease: pathogenesis and clinical implications[END_REF]. Low-density lipoproteins are sensitive to carbamylation; this damage can cause endothelial cell death and smooth muscle cell proliferation in vitro [START_REF] Ok | Carbamylated low-density lipoprotein induces death of endothelial cells: a link to atherosclerosis in patients with kidney disease[END_REF] and other molecular alterations leading to vascular damage in vivo [START_REF] Massy | Reconsidering the lack of urea toxicity in dialysis patients[END_REF]. In the 4D study, protein carbamylation was associated with heart failure and death in diabetic patients with end-stage renal disease [START_REF] Drechsler | Protein carbamylation is associated with heart failure and mortality in diabetic patients with end-stage renal disease[END_REF]. Several comparative studies in patients with CKD have suggested that BUN is a strong predictor of allcause mortality in patients with heart failure and in those with acute coronary syndrome [START_REF] Aronson | Elevated blood urea nitrogen level as a predictor of mortality in patients admitted for decompensated heart failure[END_REF][START_REF] Kirtane | Serum blood urea nitrogen as an independent marker of subsequent mortality among patients with acute coronary syndromes and normal to mildly reduced glomerular filtration rates[END_REF][START_REF] Cauthen | Relation of blood urea nitrogen to long-term mortality in patients with heart failure[END_REF]. Although the mechanisms underlying these associations have yet to be characterized, these data suggest that carbamylation has an important role in CV outcomes in patients with CKD.

Interestingly, in our study, the highest serum urea level was associated with both CV events and death before RRT in the CKD-REIN cohort and these associations persisted after adjustment for the current eGFR-suggesting that more attention should be paid to the prevention of CVD in patients with high serum urea levels. We found that the risk of atheromatous CVD was not significant but that the association between high serum urea levels and non-atheromatous CVD was strong and significant. Our hypothesis is that urea might have limited effects (directly, or indirectly via carbamylation) on atheromatous CVD, relative to traditional risk factors. Urea is the most potent uraemic toxin for inducing the expression of the pro-apoptotic BCL2 family protein BAD in human smooth muscle cells. However, the induction of BAD by urea alone did not induce apoptosis but sensitized cells to the pro-apoptotic effect of oxidized cholesterol-a physiologically relevant inducer of this form of programmed death [START_REF] Trécherel | Upregulation of BAD, a proapoptotic protein of the BCL2 family, in vascular smooth muscle cells exposed to uremic conditions[END_REF]. Moreover, urea might have a significant impact on nonatherosclerotic events, such as cardiac fibrosis. Indeed, it has been shown that the inhibition of urea transporters reduces cardiac fibrosis and improves heart function [START_REF] Kuma | Inhibition of urea transporter ameliorates uremic cardiomyopathy in chronic kidney disease[END_REF].

Given the dietary origin of a proportion of the urea in the circulation, nutritional therapy could be used to counter an elevation in urea levels. Indeed, Di Iorio et al. have shown that serum urea levels were lower in patients on a Mediterranean diet and on a very low protein diet supplemented with ketoanalogues, relative to patients with an unrestricted diet [START_REF] Iorio | Nutritional therapy reduces protein carbamylation through urea lowering in chronic kidney disease[END_REF]. Interventional studies of various diets and their impacts on cardiovascular outcomes (and especially non-atheromatous events) in non-dialysed patients with CKD are warranted.

The present study had several strengths. Firstly, and to the best of our knowledge, the present prospective study is the first to have investigated the association between urea levels and CVD in non-dialysed patients with CKD. Secondly, we studied a large number of patients, which increased the study's statistical power and enabled extensive adjustment for confounders (including the eGFR). Thirdly, all the CV events were carefully adjudicated according to standardized definitions [START_REF] Hicks | Cardiovascular and stroke endpoint definitions for clinical trials[END_REF]. Our study also had limitations. Firstly, the observational design means that we cannot rule out the possibility of residual confounding and we did not explore time-varying risk associations between serum urea and outcomes. However, our study could be considered to be a hypothesis-generating study. Secondly, we did not assess the protein intake at the time of the blood test, nor the time at which this blood test was taken; these variables might have affected the baseline serum urea levels. Thirdly, elevated urea could be a marker for occult heart failure. Lastly, urea is one of many uraemic toxins and so these other toxins (not assayed here) might have influenced the study outcomes. However, urea is a useful biomarker because it is measured in routine clinical practice-in contrast to various other uraemic toxins, which require specific assays.

C ONCLUSION

The present prospective, epidemiological study is the first to our knowledge to show that serum urea levels are associated with CVD and mortality in non-dialysed patients with CKD, independently of renal function. Indeed, our analysis of a large cohort of patients with CKD demonstrated that individuals with elevated serum urea levels had a higher risk of CV outcomes and death.

FIGURE 1 :

 1 FIGURE 1: Study flowchart. eGFR, estimated glomerular filtration rate.

Table 1 . The baseline characteristics of the study population

 1

			Baseline serum urea (mmol/L)
		Total	T1 <10.5	T2 10.5-15.1	T3 ≥ 15.1		Imputed data
		(N = 2507)	(N = 829)	(N = 835)	(N = 843)	P-value	(N = 2507)
	Serum urea (mmol/L)	13.8 (5.9)	8.3 (1.5)	12.6 (1.3)	20.3 (5.1)		0%
	Age at baseline (years)	69 [61-77]	68 [60-76]	69 [61-77]	69 [61-77]	0.13	0%
	Men, n ( % )	6 6	6 5	6 6	6 7	0 . 7 1	0
	Smoking, n (%)					0.03	0.8
	Never-smoker, n (%)	40.6	44.5	39.6	37.7
	Current smoker, n (%)	12.6	11.7	11.8	14.4
	Former smoker, n (%)	46.8	43.8	48.5	47.9
	eGFR at baseline (mL/min/1.73 m2)	33.5 (11.6)	43.5 (9.9)	32.6 (8.9)	24.5 (7.0)	<0.001	0%
	Albumin-or protein-to-creatinine ratio					<0.001	8.0
	A1 (normal to mildly increased), n (%)	28.6	42.1	27.0	16.9
	A2 (moderately increased), n (%)	31.8	31.8	33.7	29.7
	A3 (severely increased), n (%)	39.6	26.1	39.2	53.4
	Body mass index (kg/m2)	28.8 (5.8)	28.3 (5.2)	28.7 (5.9)	29.5 (6.3)	<0.001	2.0%
	Diabetes, n (%)	44.8	36.8	43.9	53.6	<0.001	0.2
	Systolic blood pressure (mmHg)	142 (20)	142 (20)	142 (21)	143 (20)	0.32	2.3%
	History of cardiovascular disease, n (%)	53.9	47.3	54.6	59.6	<0.001	1.3
	Anaemia, n (%)	38.3	21.1	35.8	57.8	<0.001	0.3
	Serum bicarbonate (mmol/L)	25.0 (3.4)	25.8 (3.1)	24.9 (3.3)	24.1 (3.6)	<0.001	6.9%
	Serum albumin (g/L)	40.4 (4.5)	40.6 (4.4)	40.5 (4.2)	39.9 (4.9)	0.009	15.2%
	High-sensitivity C-reactive protein (mg/L)	2.5 [1.1-5.9]	2.2 [1.1-5.0]	2.5 [1.1-5.4]	2.9 [1.2-7.1]	<0.001	17.6%
	History of acute kidney injury, n (%)	22.5	20.0	20.9	26.6	0.004	7.7
	Diuretic prescription at baseline, n (%)	54.0	39.9	51.1	70.7	<0.001	0.3
	PPI prescription at baseline, n (%)	31.4	27.9	33.9	32.4	0.02	0.3
	RASi prescription at baseline, n (%)	76.9	72.3	80.2	78.0	<0.001	0.3
	Statin prescription at baseline, n (%)	58.9	51.4	61.0	64.1	<0.001	0.%
	Antiplatelet prescription at baseline, n (%)	42.1	37.6	43.1	45.6	0.003	0.3
	FIGURE 2: Adjusted HRs for fatal and nonfatal atheromatous or
	non-atheromatous cardiovascular events, according to the baseline
	serum urea level. HR, hazard ratio; CI, confidence interval. Adjusted
	for age at baseline, sex, smoking status, baseline estimated
	glomerular filtration rate, urine albumin-or protein-to-creatinine
	ratio, body mass index, diabetes, systolic blood pressure, history of
	cardiovascular disease, anaemia, serum albumin, high-sensitivity
	C-reactive protein and prescriptions of diuretics, statins and
	antiplatelet agents at baseline.
	(fatal or nonfatal) was observed in patients in T3 (HR [95%
	CI]: 2.13 [1.40; 3.24]), and a trend towards a greater risk was
	observed in patients in T2 (HR [95% CI], 1.28 [0.88; 1.88]);
	Supplementary data, Table

eGFR, estimated glomerular filtration rate, based on the CKD-EPI equation; RASi, renin-angiotensin system inhibitor; PPI, proton pump inhibitor; T, tertile. Data are quoted as the frequency (%), mean (standard deviation) or the median [interquartile range]. An ANOVA or a Kruskal-Wallis or Chi-squared test was used to compare groups.

  Downloaded from https://academic.oup.com/ndt/advance-article/doi/10.1093/ndt/gfac045/6537416 by Universite de Picardie -Service commun de documentation, laville.solene on 07 June 2022

	Serum urea	Events	Incidence rate
	(mmol/L)	(N)	(95%CI)
	< 10.5	51	2.1 (1.5; 2.7)
	10.5 to 15.1	74	3.2 (2.5; 4.0)
	≥ 15.1	150	7.6 (6.4; 8.8)
			0.4	1	1.5	2	2.5	3
					HR (95% CI)
	Urea and cardiovascular disease				5

S.M. Laville et al. Downloaded from https://academic.oup.com/ndt/advance-article/doi/10.1093/ndt/gfac045/6537416 by Universite de Picardie -Service commun de documentation, laville.solene on 07 June 2022

Urea and cardiovascular disease

S.M. Laville et al. Downloaded from https://academic.oup.com/ndt/advance-article/doi/10.1093/ndt/gfac045/6537416 by Universite de Picardie -Service commun de documentation, laville.solene on 07 June 2022

S.M. Laville et al. Downloaded from https://academic.oup.com/ndt/advance-article/doi/10.1093/ndt/gfac045/6537416 by Universite de Picardie -Service commun de documentation, laville.solene on 07 June 2022

Downloaded from https://academic.oup.com/ndt/advance-article/doi/10.1093/ndt/gfac045/6537416 by Universite de Picardie -Service commun de documentation, laville.solene on 07 June 2022

S.M. Laville et al. Downloaded from https://academic.oup.com/ndt/advance-article/doi/10.1093/ndt/gfac045/6537416 by Universite de Picardie -Service commun de documentation, laville.solene on 07 June 2022

SUPPLEMENTARY DATA

Supplementary data are available at ndt online.

ACKNOWLED GEMENT S

We thank the CKD-REIN study coordination staff for their efforts in setting up the cohort: Elodie Speyer, Céline Lange, Reine Ketchemin, Natalia Alencar de Pinho and all the clinical research associates. The authors thank Thao Nguyen Khoa for dosing high-sensitivity C-reactive protein.

C ONFLICT OF INTEREST STATEMENT

S.M.L., S.L., O.L. and N.M. have nothing to declare. D.F. reports grants and lecture fees form Sanofi, Fresenius Kabi, Astra-Zeneca and Lilly. Z.A.M. reports grants for CKD-REIN and other research projects from Amgen, Baxter, Fresenius Medical Care, GlaxoSmithKline, Merck Sharp and Dohme-Chibret, Sanofi-Genzyme, Lilly, Otsuka and the French government, as well as fees and grants to charities from Amgen, Daichii, and Sanofi-Genzyme. These sources of funding are not necessarily related to the content of the present manuscript. B.S. reports grants for the CKD-REIN cohort study from Amgen, Baxter, Fresenius Medical Care, GlaxoSmithKline, Merck Sharp and Dohme-Chibret, Sanofi Genzyme, Lilly, Otsuka and Vifor Fresenius, as well as speaker from Lilly and MSD, unrelated to the content of this manuscript.

AU THORIZATIONS

All legal authorizations were obtained, including those from the Comité consultatif sur le traitement de l'information en matière de recherche dans le domaine de la santé (CCTIRS N°12.360), the Commission nationale de l'informatique et des libertés (CNIL N°DR-2012-469) and the Kremlin-Bicêtre Comité de protection des personnes (CPP N°IDRCB 2012-A00902-41). The CKD-REIN sample collection is registered in the management application by the COnservation D'Eléments du COrps Humain biological resource center (CODECOCH N°-2012-1624). The Institut national de la santé et de la recherche médical (INSERM) institutional review board approved the study protocol (IRB00003888), which was registered at ClinicalTrials.gov (NCT03381950).

APPENDIX

The CKD-REIN study collaborators: The CKD-REIN Study Group steering committee and coordinators include: Carole Ayav, Serge Briançon, Dorothée Cannet, Christian Combe, Denis Fouque, Luc Frimat, Yves-Edouard


U Thupakula

V Perrin

A Palacio-Morales

L Cario

M Aprili

P Simon

F Massee

Coherent and incoherent tunneling into YSR states revealed by atomic scale shot-noise spectroscopy

The pair breaking potential of individual magnetic impurities in s-wave superconductors generates localized states inside the superconducting gap commonly referred to as Yu-Shiba-Rusinov (YSR) states whose isolated nature makes them ideal building blocks for artificial structures that may host Majorana fermions. One of the challenges in this endeavor is to understand their intrinsic lifetime, /Λ, which is expected to be limited by the inelastic coupling with the continuum thus leading to decoherence. Here we use shot-noise scanning tunneling microscopy to reveal that electron tunnelling into superconducting 2H-NbSe2 mediated by YSR states is ordered as function of time, as evidenced by a reduction of the noise. Moreover, our data show the concomitant transfer of charges e and 2e, indicating that incoherent single particle and coherent Andreev processes operate simultaneously. From the quantitative agreement between experiment and theory we obtain Λ = 1 µeV kBT demonstrating that shot-noise can probe energy-and time scales inaccessible by conventional spectroscopy whose resolution is thermally limited.

INTRODUCTION

For a single impurity spin in a superconductor, a bound state appears inside the gap [START_REF] Yu | Bound state in superconductors with paramagnetic impurities[END_REF][2][START_REF] Rusinov | Superconductivity near a paramagnetic impurity[END_REF] with its particle-and hole components located in energy symmetrically around zero [START_REF] Balatsky | Impurityinduced states in conventional and unconventional superconductors[END_REF]. The amplitudes of the two components are usually different [START_REF] Yazdani | Probing the local effects of magnetic impurities on superconductivity[END_REF][START_REF] Ji | Highresolution scanning tunneling spectroscopy of magnetic impurity induced bound states in the superconducting gap of Pb thin films[END_REF][START_REF] Heinrich | Single magnetic adsorbates on s-wave superconductors[END_REF] and reflect the coherence factors of the electron and hole excitations. Whereas the spatial extent of the YSR states is typically on the order of a few atoms [START_REF] Yazdani | Probing the local effects of magnetic impurities on superconductivity[END_REF], they have been shown to range up to tens of nanometers for two dimensional superconductors [START_REF] Ménard | Coherent long-range magnetic bound states in a superconductor[END_REF]. Since the YSR states are inside the superconducting gap, one of the key questions, particularly with an eye on building more complicated structures such as chains and islands [START_REF] Nadj-Perge | Observation of Majorana fermions in ferromagnetic atomic chains on a superconductor[END_REF][START_REF] Ruby | End states and subgap Structure in proximity-coupled chains of magnetic adatoms[END_REF][START_REF] Pawlak | Probing atomic structure and Majorana wavefunctions in mono-atomic Fe chains on superconducting Pb surface[END_REF][START_REF] Kim | Toward tailoring Majorana bound states in artificially constructed magnetic atom chains on elemental superconductors[END_REF] is how electrons move between the YSR states and the condensate. Not only is a full understanding of the nature of the impurity and its intrinsic lifetime important for theoretical modelling, the dynamics of charge transfer through it can in principle also be used to directly distinguish conventional YSR states from Majorana bound states [START_REF] Perrin | Identifying Majorana bound states by tunneling shot-noise tomography[END_REF].

The high spatial-and energy resolution make the scanning tunnelling microscope (STM) an ideal experimental tool to investigate the tunnelling process into individual impurities. Previous studies using the time averaged current and theoretical modelling showed tantalizing signatures of a transition from single-electron dominated tunnelling to multi-particle Andreev processes [START_REF] Ruby | Tunneling processes into localized subgap states in superconductors[END_REF][START_REF] Huang | Tunnelling dynamics between superconducting bound states at the atomic limit[END_REF]. Direct evidence for such a transition, and more specifically for Andreev processes to occur with a standard metallic probe, however, is lacking. Moreover, direct tunnelling into the magnetic impurity can complicate the interpretation of the data, since the impurity state may be affected by the presence of the tip [START_REF] Heinrich | Tuning the magnetic anisotropy of single molecules[END_REF][START_REF] Ormaza | Controlled spin switching in a metallocene molecular junction[END_REF][START_REF] Malavolti | Tunable spin-superconductor coupling of spin 1/2 vanadyl phthalocyanine molecules[END_REF][START_REF] Kezilebieke | Observation of coexistence of Yu-Shiba-Rusinov states and spin-flip excitations[END_REF], or multiple tunnelling paths and relaxation processes may occur [START_REF] Figgins | Differential conductance and quantum interference in Kondo systems[END_REF][START_REF] Bryant | Controlled complete suppression of single-atom inelastic spin and orbital cotunneling[END_REF][START_REF] Farinacci | Interfering tunneling paths through magnetic molecules on superconductors: asymmetries of Kondo and Yu-Shiba-Rusinov resonances[END_REF] which are difficult to incorporate in theory. Although experimentally challenging, atomic scale shot-noise measurements can in principle resolve all these issues. This is because shot-noise (S shot ), which is current noise originating from the discreetness of the charge carriers, is sensitive to both the charge of the carriers, q, as well as the nature of the tunnelling process [START_REF] Ya | Shot noise in mesoscopic conductors[END_REF]. To evaluate the shot-noise, we consider the effective Fano factor, F * = S shot /2e|I| = qF/e, where I is the time averaged current, e the electron charge and F the Fano factor. For uncorrelated elastic quasi-particle tunnelling between a metallic tip and the bulk superconductor, the electrons follow Poissonian statistics [START_REF] Ronen | Charge of a quasiparticle in a superconductor[END_REF] giving F * = F = 1 (EQP in Fig. 1a). Single electron tunnelling via the YSR states, on the other hand, is a resonant process and only possible through inelastic quasi-particle relaxation (IQP in Fig. 1a). Therefore the electron flow will become ordered, thereby reducing the current noise from Poissonian to sub-Poissonian, i.e. F * < 1 (IQP in Fig. 1a), as observed in quantum dots [START_REF] Choi | Counting statistics in an InAs nanowire quantum dot with a vertically coupled charge detector[END_REF]. Alternatively, Andreev reflection through the YSR state transfers a charge of q = 2e, giving F * > 1 (AR in Fig. 1a), enabling them to be easily distinguished from either forms of single electron tunnelling [START_REF] Ronen | Charge of a quasiparticle in a superconductor[END_REF][START_REF] Jehl | Detection of doubled shot noise in short normal-metal/ superconductor junctions[END_REF][START_REF] Bastiaans | Imaging doubled shot noise in a Josephson scanning tunneling microscope[END_REF].

RESULTS

Noise at the atomic scale is measured using our homebuilt scanning tunnelling microscope with cryogenic circuitry operating in the MHz regime [START_REF] Massee | Atomic scale shot-noise using cryogenic MHz circuitry[END_REF]. The circuitry, which is explained in more detail in the Supplementary Information, converts the current noise into voltage noise at the input of a cryogenic amplifier and can operate simultaneously with conventional low frequency (DC) mea- a Schematic depiction of the various tunnelling processes into 2H-NbSe2: direct elastic quasi-particle tunnelling into the bulk (EQP, red) inelastic quasi-particle tunnelling through the YSR state (IQP, purple) and Andreev reflection assisted by the YSR (AR, green). Whereas direct tunnelling of electrons generates Poissonian noise (F * = 1), inelastic tunneling through the YSR state orders the electron flow, reducing the noise (F * < 1). The energy relaxation time sets the intrinsic lifetime of the YSR. Andreev reflection on the other hand involves a charge of q = 2e, leading to F * > 1. The coloured spheres for the three scenarios on the right illustrate the passage of electrons as function of time: random, ordered, or in pairs. b Differential conductance on a fully gapped 2H-NbSe2 surface, V = 3 mV, I = 3 nA. c Current noise power recorded simultaneously with b, the black line shows a fit for F * = 1, that takes into account the measured RJ (V ) and uses a single set of fitting parameters for all voltages. The inset highlights the effect of the strongly varying dynamical resistance on the measured voltage noise which is accurately captured by the fit. See Supplementary Information section 1 for more details.

surements. Although in most circumstances the junction resistance, R J , is sufficiently large to be safely ignored, for the relatively low junction resistances used in this work it will start acting as a voltage divider resulting in a reduction of the measured voltage noise. Importantly, for a highly non-linear I(V ) characteristic, such as that of clean 2H-NbSe 2 (Fig. 1b), the dynamical resistance, R J (V ) = dV /dI, needs to be considered instead of the setup resistance. Fig. 1c shows this effect vividly: instead of a simple linear current dependence of the measured noise power, it decreases at the onset of the coherence peak (∼ ±0.9 mV ) below that obtained at zero voltage. As evidenced by the fit in Fig. 1c, this non-linear behavior is purely an effect of the non-linearity of the junction, R J (V ), which reduces the contribution of the thermal noise more than that of the shot-noise increases; F * = 1 for all voltages as expected for quasi-particle tunnelling following Poissonian statistics [START_REF] Ronen | Charge of a quasiparticle in a superconductor[END_REF] (EQP in Fig. 1a).

Having a detailed understanding of the noise data recorded on clean 2H-NbSe 2 , we next move to the electronic transport into YSR states in 2H-NbSe 2 . The precise spatial extent of the in-gap resonances, as well as the particle-hole asymmetry of the core, can vary from impurity to impurity as it depends on the impurity type and its location in the crystal structure [START_REF] Ménard | Coherent long-range magnetic bound states in a superconductor[END_REF][START_REF] Senkpiel | Robustness of Yu-Shiba-Rusinov resonances in the presence of a complex superconducting order parameter[END_REF][START_REF] Liebhaber | Yu-Shiba-Rusinov states in the chargedensity modulated superconductor NbSe2[END_REF]. Two YSR states with opposite particle-hole asymmetry and different spatial extent are shown in Fig. 2. Interestingly, also the ratio of the YSR-and coherence peaks is very different for the two cores. As we are interested in the tunnelling process through the YSR states, to facilitate comparison we choose setup parameters that give roughly the same YSR-current, i.e. the YSR peaks in differential conductance in Figs. 2c andh have approximately the same height. Consequently, since the noise is proportional to the current, the simultaneously recorded current noise has a similar magnitude for the two cores, despite the rather different conditions outside the gap, see Figs. 2d,i. To evaluate the in-gap noise, we fit the normal state (|V | > 1.2 mV) noise data using the measured R J (V ) and F * = 1, then extend the fit inside the gap giving the black line in Figs. 2d,I. Unlike for the noise taken on clean 2H-NbSe 2 (Fig. 1c), the noise on the YSR cores evidently does not follow F * = 1: for the dominant resonance, i.e. positive bias for Figs. 2c,d and negative bias for Figs. 2h, i, the noise is reduced (F * < 1), whereas for the weak resonance, i.e. negative bias for Figs. 2c,d and positive bias for Figs. 2h,i, it is enhanced (F * > 1). Although the deviations in absolute numbers are relatively small, they are larger than the experimental error bars due to our high signal-to-noise ratio and accurate fitting procedure (see Supplementary Information section 1), and correspond to changes in F * of the order of 10% (Figs. 2e,j). Importantly, the observation of F * > 1 strongly suggests Andreev processes to be present, as it cannot occur for single electron tunnelling into a one-level system. Furthermore, the particle-hole asymmetry of the noise also suggests a contribution from single electron tunneling, meaning both processes operate simultaneously.

To make a more quantitative analysis of the noise, and in order to avoid possible mechanical [START_REF] Heinrich | Tuning the magnetic anisotropy of single molecules[END_REF][START_REF] Ormaza | Controlled spin switching in a metallocene molecular junction[END_REF][START_REF] Malavolti | Tunable spin-superconductor coupling of spin 1/2 vanadyl phthalocyanine molecules[END_REF][START_REF] Kezilebieke | Observation of coexistence of Yu-Shiba-Rusinov states and spin-flip excitations[END_REF], multi- paths related [START_REF] Figgins | Differential conductance and quantum interference in Kondo systems[END_REF][START_REF] Bryant | Controlled complete suppression of single-atom inelastic spin and orbital cotunneling[END_REF][START_REF] Farinacci | Interfering tunneling paths through magnetic molecules on superconductors: asymmetries of Kondo and Yu-Shiba-Rusinov resonances[END_REF], or spin-dependent [START_REF] Pradhan | Shot noise as a probe of spincorrelated transport through single atoms[END_REF] complications from direct tunnelling into the impurity, we shift our attention to the YSR tails. Since the particlehole asymmetry of the tails oscillates as function of distance from the core [START_REF] Ménard | Coherent long-range magnetic bound states in a superconductor[END_REF], we can probe locations where the particle-hole asymmetry is nearly perfectly mirrored while all other experimental parameters remain identical. Fig. 3 shows two such locations, both situated a distance of several atoms from the core (crosses in Fig. 3b), ensuring that direct tunnelling into the impurity is negligible. Fig. 3c shows the noise recorded simultaneously with the tunnelling spectra of Fig. 3a. As was the case for the spectra taken on the core, the noise is reduced (F * < 1) for the dominant resonance, and enhanced (F * > 1) for the weaker resonance. To analyse the deviation from F * = 1 in more detail, we extract F * for each voltage in Fig. 3d which shows that F * is roughly equally enhanced as it is suppressed, and converges to Poissonian as soon as the current becomes dominated by the quasi-particles at the coherence peaks. To confirm that the noise deviates from F * = 1, we additionally measured the current dependence of the noise at fixed voltage in-and outside the gap, see Fig. 3e.

To gain more insight into our experimental data, we calculate the tunnelling current and current noise using a standard description of a classical YSR impurity (see Supplementary Information section 2 for more details), considering both single electron tunnelling and Andreev processes [START_REF] Ruby | Tunneling processes into localized subgap states in superconductors[END_REF]. The main input parameters of the theory are the coherence factors of the electron and hole excitations of the YSR, u and v, the superconducting gap, ∆, the YSR energy, E 0 , the normal state conductance, G N , and the intrinsic lifetime, τ = /Λ. Of these, ∆, E 0 and G N can be directly obtained from the differential conductance spectra (e.g Fig. 3a). Furthermore, u and v, can be extracted from the normal state conductance (G N ) dependence of the YSR conductance (G Y SR), see Figs. 4a,c. Here, we fit the single electron tunnelling dominated linear part at low conductance [START_REF] Ruby | Tunneling processes into localized subgap states in superconductors[END_REF][START_REF] Huang | Tunnelling dynamics between superconducting bound states at the atomic limit[END_REF] to determine u and v, see also Supplementary Information section 2. This enables us to calculate the noise with as only adjustable parameter the intrinsic lifetime, /Λ, which is masked in experiment by thermal broadening. Figs. 4b, d compare the experimental noise data for energies where the tunnelling current is carried exclusively by the YSR states (i.e. |V | < 0.8 mV) with theoretical curves for several values of Λ, showing quantitative agreement for Λ ∼ 1µeV, i.e. τ ∼ 0.7 ns, for both measured particle-hole asymmetries. We stress that for increasing values of Λ, meaning shorter relaxation times, single electron tunnelling becomes less resonant (i.e. less ordered in time) and increasingly dominates the tunnelling process. Indeed, for Λ = 10 µeV, the calculated noise is already nearly Poissonian (F * = 1) for all voltages (see Figs. 4b,d), putting a strong lower limit on the relaxation time extracted from the noise data. For comparison, calculations using only Andreev reflection (AR) or only inelastic single electron processes (IQP) fail to reproduce the data for any Λ, as the former always has F * > 1 for both polarities and the latter F * < 1.

DISCUSSION

The persistent enhancement of the noise for the smaller of the two YSR resonances in both experiment and theory directly proves the presence of Andreev processes, whereas the reduction in noise of the strong resonance results from a finite lifetime of the YSR. The fact that we obtain qualitative agreement between theory and experiment for u and v extracted from the linear part of Figs. 4a,c, while all experimental noise data was recorded in the non-linear part of Figs. 4a,c highlights the robustness of our results. We stress that although qualitatively still in agreement, the theoretical curves for the data taken on the cores (Figs. 4d,h) slightly deviate quantitatively (see Supplementary Information Fig. S7), suggesting that tip and/or current induced effects may indeed play a role on the YSR core which is currently not included in the theory. Despite the less accurate fit, the noise recorded for both cores agrees best to the theory curves that use a lifetime similar to that obtained on the YSR tails. This implies that for roughly equal YSR currents, which at sub-gap voltages constitute the only contribution to the current, the YSR lifetime in 2H-NbSe 2 is independent of the particular details of the magnetic impurity and the measurement location. Fur-thermore, the sub-nanosecond value at 0.7 K we extract from the noise data is similar to that reported for Mn atoms on a Pb(111) surface [START_REF] Ruby | Tunneling processes into localized subgap states in superconductors[END_REF], and not incompatible with the electron-phonon relaxation time in 2H-NbSe 2 [START_REF] Anikin | Ultrafast dynamics in the high-symmetry and in the charge density wave phase of 2H-NbSe2[END_REF]. Importantly, the energy scale of relaxation we obtain (Λ = 1 µeV) is much smaller than the electron temperature, meaning that shot-noise allows to determine the YSR lifetime even if the width of the resonance in the tunnelling spectra is dominated by thermal broadening, or the current not thermally saturated as used previously [START_REF] Ruby | Tunneling processes into localized subgap states in superconductors[END_REF]. More generally, we show that local measurements of fluctuations in the tunnelling current provide direct evidence of the coherent transfer of charges equal to 2e through YSR states into the bulk, and enable one to probe energy-and time scales inaccessible to conventional spectroscopy. Although experimentally challenging, this work shows the feasibility of using atomic scale shot-noise to elucidate the transport dynamics through individual impurity resonances, which could in future studies be used to e.g. distinguish trivial from non-trivial states.

Figure 1 .

 1 Figure 1. Noise schematic and fully gapped 2H-NbSe2.a Schematic depiction of the various tunnelling processes into 2H-NbSe2: direct elastic quasi-particle tunnelling into the bulk (EQP, red) inelastic quasi-particle tunnelling through the YSR state (IQP, purple) and Andreev reflection assisted by the YSR (AR, green). Whereas direct tunnelling of electrons generates Poissonian noise (F * = 1), inelastic tunneling through the YSR state orders the electron flow, reducing the noise (F * < 1). The energy relaxation time sets the intrinsic lifetime of the YSR. Andreev reflection on the other hand involves a charge of q = 2e, leading to F * > 1. The coloured spheres for the three scenarios on the right illustrate the passage of electrons as function of time: random, ordered, or in pairs. b Differential conductance on a fully gapped 2H-NbSe2 surface, V = 3 mV, I = 3 nA. c Current noise power recorded simultaneously with b, the black line shows a fit for F * = 1, that takes into account the measured RJ (V ) and uses a single set of fitting parameters for all voltages. The inset highlights the effect of the strongly varying dynamical resistance on the measured voltage noise which is accurately captured by the fit. See Supplementary Information section 1 for more details.

Figure 2 .

 2 Figure 2. YSR cores in 2H-NbSe2. a Atomically resolved constant current image of the Se surface of 2H-NbSe2, V = 4.2 mV, I = 100 pA. b In-gap current recorded simultaneously with a showing a spatially extended YSR states generated by a sub-surface impurity. c Tunnelling spectrum taken at the core of the YSR and d simultaneously recorded current noise, V = 3 mV, I = 3 nA. The black line in d indicates F * = 1: the noise from the YSR deviates at both positive and negative sample bias (arrows), as can be clearly seen in the effective Fano factor, F * , in e. Outside the gap, F * converges to 1. f -j The same as a-e for a more compact, but relatively strong, YSR located elsewhere on the same sample. V = 4 mV, I = 100 pA for f, g; V = 6 mV, I = 400 pA for h-j.

Figure 3 .

 3 Figure 3. Noise on the YSR tails. a Differential conductance G = dI/dV on two tail locations with opposite particle-hole asymmetry, V = 4.2 mV, I = 1.5 nA. We define G ± = G(±E0) with E0 the YSR resonance energy. The inset shows the corresponding currents on the same energy scale, dashed lines indicate where the current is dominated by the YSR and is sufficiently large for noise measurements. The YSR state is the same as that in Fig. 2f-j. The location of the spectra (red and blue crosses), as well as that of the YSR core (black cross) is marked in the constant current image in b (V = 4 mV, I = 100 pA). c Current noise recorded simultaneously with a, the black lines indicate F * = 1. d Effective Fano factor, F * , extracted from c showing clearly that the noise deviates from F * = 1 where the current is dominated by the YSR. The points corresponding to I<10 pA have been omitted for clarity; since the fluctuations in the noise are the same for all voltages, the associated error in F * becomes relatively large for such small currents. e Current dependence of the noise at fixed voltage taken at the blue cross in d.

Figure 4 .

 4 Figure 4. Experiment vs theory. a YSR peak conductance (GY SR) as function of normal state conductance (GN ) for the location of the blue spectrum of Fig. 3a, reproduced here in the inset, see Supplementary Information section 2 for more details. A linear fit of the data taken at small conductance is used to extract u and v. b Sub-gap F * (symbols) for the blue spectrum of Fig. 3d and theoretical curves for three different values of Λ. Pure Andreev reflection (AR, Λ = 0 µeV ) and pure inelastic quasi particle tunnelling (IQP, Λ = 1 µeV ) are shown for comparison. c, d Same as a, b for the red data of Fig. 3.

We thank A. Mesaros and M. Civelli for insightful discussions. We would like to acknowledge funding from H2020 Marie Sk lodowska-Curie Actions (grant number 659247) and the ANR (ANR-16-ACHN-0018-01 and ANR-19-CE47-0006).