Sylvain Dailler

Claude Marché

Yannick Moy

Lightweight Interactive Proving inside an Automatic Program Verifier *

Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts.

In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers. Adding interactive proof features in SPARK appears to be complicated by the fact that the proof toolchain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client-server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK.

Introduction

For the development of software with high safety and security requirements, deductive program verification is an approach that provides access to the highest levels of guarantees. The functional requirements are expressed using formal specification languages. The conformance of the code with such specifications can be established in a fairly automated setting using automatic program verifiers available nowadays (such as Dafny, F , KeY, KIV, OpenJML, Verifast, Viper, Why3, etc.). Such verification tools typically proceed by generating verification conditions (VC for short): mathematical formulas that need to be proven valid. Such VCs are typically discharged using automated solvers, such as the SMT solvers reasoning on Satisfiability Modulo Theories.

A major issue preventing the diffusion of deductive verification in industrial applications is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the VCs. To leverage this issue, it is important, when no SMT solver is able to solve a given VC, to provide the user with means to investigate the proof failure: is it because the code needs to be fixed, is it because the program is not sufficiently annotated (e.g. a missing loop invariant), or is it because the VC is too complex to be discharged by automatic provers (e.g. an induction is needed). Among the possible means is the generation of counterexamples [START_REF] Hauzar | Counterexamples from Proof Failures in SPARK[END_REF]. Such a feature appears to be useful in particular to fix trivial mistakes, but for complex cases, its limitations quickly show up: because of the intrinsic incompleteness of back-end solvers, or more pragmatically because solvers proof search is typically interrupted after a given time limit is reached, the counterexamples may be spurious or absent [START_REF] Hauzar | Counterexamples from Proof Failures in SPARK[END_REF]. Moreover, there is no easy mean to distinguish a true bug from insufficiently detailed specifications (although there is on-going research in that direction [START_REF] Petiot | Your Proof Fails? Testing Helps to Find the Reason[END_REF]).

This paper presents an approach that we designed in the context of the SPARK verifier for industrial development of safety-critical Ada code [START_REF] Chapman | Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK[END_REF][START_REF] Mccormick | Building High Integrity Applications with SPARK[END_REF]. The goal is to provide simplified interactions between the user and the failing VC, so as to investigate a proof task without the need to rely on an external interactive prover. A specificity of SPARK is that the underlying toolchain from the given input Ada program to the VCs makes use of the external intermediate language Why3 [START_REF] Franc ¸ois Bobot | Let's Verify This with Why3[END_REF] that itself provides access to many different automated provers (mainly Alt-Ergo, CVC4 and Z3) but also general purpose interactive theorem provers (Coq, Isabelle/HOL, PVS). Indeed, an extreme mean to investigate a proof failure is to launch an interactive theorem prover on the failing VC and to start writing a manual proof. Such a process shows up useful, mainly because writing the detailed steps, in which the user believes the proof should work, typically helps to discover missing elements in the specifications, and in such cases fixing the annotations could finally help the SMT solvers to automatically discharge the VC. Also, an ultimate situation is to finish the proof completely using the underlying interactive prover [START_REF] Berghofer | Verification of Dependable Software using SPARK and Isabelle[END_REF]. The main drawback in this process is that users should be able to use the general-purpose back-end interactive prover, forcing them to learn a completely different environment, using its own syntax for formulas, and its specific proof tactics to discharge proof tasks. Another drawback is that once the user has switched to an external proof assistant to proceed with a proof, then there is no easy mean to get back to the common environment offered by Why3 to call other automatic provers on the sub-goals generated by interactive proof tactics.

Related Work

The need for user interaction in the context of industrial use of deductive verification is not new, this issue was identified and taken into account early in the design of industrial tools. The KIV environment, used in large realistic case studies in academia and industry for more than 20 years, considered very early the importance of combining automated and interactive proving [START_REF] Ahrendt | Automated Deduction -A Basis for Applications, chapter Integrating Automated and Interactive Theorem Proving[END_REF]. Other early tools that provide some form of interactive proving are the industrial tools, largely used in railway industry, Atelier B [START_REF] Abrial | Click'n Prove: Interactive Proofs within Set Theory[END_REF] and Rodin [START_REF] Mehta | Supporting Proof in a Reactive Development Environment[END_REF]. The KeY environment, somehow a successor of KIV, is designed to build proofs interactively, with the possibility to call efficient automated provers for solving some leaves of the proof [START_REF] Hentschel | An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier[END_REF][START_REF] Hentschel | The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts[END_REF]. In the context of general purpose proof assistants, the need for adding automation to their general interactive theorem proving process is evident, for example in the environments ACL2, HOL Light, and more recently in Isabelle/HOL where the so-called Sledgehammer subtool is able to finish proofs using external SMT solvers [START_REF] Christian Blanchette | Extending Sledgehammer with SMT Solvers[END_REF].

Common Issues in Automated Program Verification

Interestingly, our analysis of the common situations where fully automatic provers fail, and switching to proof interaction is needed, is very similar to the analysis made in previous work mentioned above. Here are the main identified cases:

• quantifier instantiation: a proof should be done by an adequate instantiation of a universally quantified hypothesis, that the automatic provers cannot discover. Providing the instantiation by hand Similarly, for proving an existential goal, automated provers typically cannot guess the witness. This witness should be given by hand.

• reasoning by cases: an explicit case reasoning can help the automatic provers.

• controlling the context and the strategy of proof search: a prover would sometimes use most of its available time to try to solve the problem using a direction of thinking while a simple solution exists. Reducing the context manually can help.

• inductive reasoning: some properties require reasoning by induction over an integer, an algebraic datatype, or on an inductively defined predicate; such reasoning steps are out-of-reach of common automated solvers, whereas applying an induction rule by hand usually results in sub-goals that can be automatically discharged.

• non-linear integer arithmetic: it is typically hard for automatic provers, but a few manual proof steps can make such a proof feasible. Similarly, floating-point arithmetic is also very hard for automatic provers.

Contributions and Overview of the Paper

Our goals are shared with the above-mentioned related work. However, in the context of SPARK, there is an additional issue that does not show up in previous work. Indeed, in the previous work mentioned above, the language of formulas and proof tasks (e.g. proof sequents) is directly the language in which the user writes her input problem: for example in the context of the B method, the logic language is B set theory in which the code of the B machines is written; in KeY, the underlying Dynamic Logic incorporates pieces of Java code to verify. In the context of SPARK, we have the additional issue that a proof task generated by the Why3 VC generator is written in a language that is very different from the Ada input language. Our approach proceeds in the following steps. In Section 2, we present what we added to the Why3 intermediate tool to provide interactive proving features. Section 3 presents the use of interactive proof from SPARK, inside GNAT Programming Studio, the Ada interface development environment. Section 4 concludes and discusses remaining future work.

Adding Interactive Proving in Why3

Figure 1 presents a general overview of Why3's core architecture. The input files contain code with formal specifications, written in the dedicated language WhyML [START_REF] Filliâtre | Why3 -Where Programs Meet Provers[END_REF], which essentially consists of a set of functions or procedures annotated with contracts (pre-and post-conditions, loop invariants, etc.). The VC generator produces, from such a file, a set of proof tasks. A proof task, that we can denote as Γ G, consists in a set Γ of logical declarations of types, function symbols, predicates, and hypotheses, and finally the logical formula G representing the goal to prove. The soundness property of the VC generator expresses that if all generated proof tasks are valid logical statements, then the input program is safe: no runtime error can arise and formal contracts are satisfied. Consider the following toy example of a function written in WhyML.

let f (a:array int) (x:int) : int requires { a.length

≥ 1000 } requires { 0 ≤ x ≤ 10 } requires { forall i. 0 ≤ 4*i+1 < a.length → a[4*i+1] ≥ 0 } ensures { result ≥ 0 } = let y = 2*x+1 in a[y*y]
The function f takes as parameters an array a and an integer x. The first two pre-conditions express two simple requirements on the size of array a and an interval of possible values for x. The third precondition is a bit more complex, it expresses that for indexes that are a multiple of 4 plus 1, the values stored in a are non-negative. The function f returns an integer, denoted as the keyword result in the post-condition, with a post-condition expressing that the value at the index returned is also non-negative. The code simply returns the square of 2x + 1. For such a code, Why3 generates as the VC the formula forall a:array int, x:int. length a ≥ 1000 ∧ (0

≤ x ∧ x ≤ 10) ∧ (forall i:int. 0 ≤ ((4 * i) + 1) ∧ ((4 * i) + 1) < length a → a[(4 * i) + 1] ≥ 0) → (let y = (2 * x) + 1 in let o = y * y in (0 ≤ o ∧ o < length a) ∧ a[o] ≥ 0)
As one may guess such a formula can quickly become unreadable when code size grows, and is hardly suitable for human inspection.

Proof Tasks and Transformations

The core of Why3 comes as a software library, written in the OCaml language and with a documented API, that proposes in particular data-types for terms, formulas and proof tasks, and a large collection of functions to operate on them. A central notion is the notion of transformation: an OCaml function that takes a proof task as input and returns a set of proof tasks. All implemented transformations are expected to be sound, in the sense that if all the resulting proof tasks are valid, then the original task is valid too.

A simple example of such a transformation is splitting, which basically transforms a task of the form

Γ G 1 ∧ G 2 ∧ • • • ∧ G k into the set of tasks Γ G i for 1 ≤ i ≤ k.
The VC generator is designed so as to produce a single proof task for each procedure or function of the input code, as in the example above. To ease the visibility and understanding of the resulting formula, a generalized splitting transformation is typically applied, so as to decompose such a VC into a set of simpler VCs for specific properties to check, e.g. checking if an array index is in bounds, checking the preservation of a loop invariant, checking the pre-condition of a sub-procedure called, etc. Figure 2 presents a screenshot of Why3's graphical interface (Why3IDE) when given our toy program as input. The left part of that window is the proof task tree. The current selected line is for the proof task after applying the transformation named split_vc which implements the generalized splitting transformation mentioned above.

Indeed the role of transformations is two-fold. The first role is to simplify the given task (such as the splitting above). In such a case a transformation is applied on user's request inside the graphical interface. The second role is to preprocess a task before sending it to an external prover: typically an external prover does not support all features of Why3's logic, such as polymorphic types, algebraic data types and the corresponding pattern-matching, recursive or inductive definition of predicates, etc. Hence, when the user wants to invoke an external prover on a given task, Why3 transparently applies some transformations to make the proof task fit into the logic of the target prover, before using an appropriate printer suitable for the back-end prover input syntax (e.g. SMT-LIB). On Figure 2 it can be seen that the provers Alt-Ergo, CVC4 and Z3 were invoked but none of them were able to discharge the expected postcondition. It is likely that the combination of non-linear arithmetic and the need for finding an appropriate instantiation for the hypothesis H is the reason why they fail. Mixing quantifiers and arithmetic makes very difficult goals to prove for all categories of automatic provers: SMT solvers quantifier handling is based on triggers, that do not interact well with arithmetic, while TPTP provers have a more powerful handling of quantifiers but do not support arithmetic. This corresponds to the limitation of automatic provers that we called quantifier instantiation in Section 1.2.

On top of the core architecture of Figure 1, Why3 features two major components: the proof session manager and the graphical interface. Adding support for interactive proving in this global architecture requires extensions that we detail in the subsections below: extensions of the GUI, extension of the transformation setting of the core architecture, and extensions in the proof session manager. A feature, that has important consequences on our approach presented below for adding interactive proving in Why3, is the genericity of transformations handling. The Why3 library is designed so that an additional user-written transformation can be dynamically loaded at run-time, using a mechanism of registration with a name.

Extending User Interface

As shown in Figure 2, the graphical interface is naturally where proof tasks are displayed and where the user can decide which transformations to apply and which prover to call. Below the top-right part of the window, where the current proof task is displayed, and above the bottom-right part where different kinds of messages are displayed, we added a kind of command-line input field where the user can input arbitrary character text to form a command. If we consider our toy example, one possibility to progress towards proving the goal is to replace y*y by the term 4*(x*x+x)+1. To achieve that, the user can directly input the text Both subgoals are proved by Alt-Ergo. Similarly, the transformation "instantiate H x*x+x" generates one subgoal where an additional hypothesis is present (the instance of H for the given particular value for i) and is also proved by Alt-Ergo. As can be seen, applying any of these two transformations is enough to finish the proof automatically.

Even if this mechanism using a textual interface may seem old-fashioned, it permits a lot of genericity. We'll see below how it simplifies the communication with a front-end such as SPARK. It also permits a lot of extra features that show themselves important in practice, such as searching in the proof context.

Adding Parameters to Proof Transformations

A central design choice towards the introduction of interactive proofs is to reuse the existing infrastructure of transformations. Basically, since that infrastructure already allows the user to select among a given set of transformations to apply on a given proof task, we just have to extend this set, after extending the concept of transformations so that they can take parameters, like the two transformations used above: replace is a transformation that takes two terms as input. instantiate takes a hypothesis name and a term. We faced two main issues for this extension. First, the transformations can take various objects as parameters: a term, a formula, a name, a string, etc. It means that at the level of the API, we need a typing mechanism in order to declare what are the right types of objects to pass as parameters. Second, at the level of the interface, the data submitted by the user are just textual, so we need a generic infrastructure to parse them and turn them into objects of the right kind.

At the level of the API, in order to handle the large variability of the kinds of transformation parameters, we were able to use the advanced concept of GADT (Generalized Abstract Data Types). An excerpt of the new declaration of transformation type in the API is as follows (the real one has 20 constructors): To implement a transformation like instantiate above, we first have to program it with an OCaml function, say inst, of type prsymbol → term → task list, and then register it under the proper name as follows wrap_and_register "instantiate" (Tprsymbol (Tterm Ttrans_l)) inst Not only will it make the transformation available for use in the interface, but it will automatically proceed with the parsing, name resolution and typing of the textual arguments, as given by the type (Tprsymbol (Tterm Ttrans_l)). This mechanism based on GADTs is powerful enough to handle optional parameters. For example, the replace transformation is declared with type (Tterm (Tterm (Topt ("in", Tprsymbol Ttrans_l))))

which means that a third optional argument is allowed, of type prsymbol and introduced by the keyword in to say that the replacement should be done in the hypothesis of the given name instead of the goal, e.g. "replace (length a) 1000 in H". Notice the large genericity of this mechanism, in particular the keyword used for introducing the optional argument. The genericity also comes from the wrap_and_register function which is defined once and for all and does all the hard job of parsing and typing arguments. In particular, the resolution of variable names given as arguments had to be carefully made consistent with the printing of the task, which can rename variables.

Here is a quick summary of the major transformations with parameters that we added in Why3. They are supposed to cover the major needs for interaction as already listed in Section 1.2.

• case analysis on a formula (case P), on algebraic data (destruct_alg t), decomposition on propositional structure of a hypothesis (destruct H). For example, the transformation "case P" where P is an arbitrary formula would be transforming a task Γ G into the two tasks Γ, P G and Γ, ¬P G.

• introduction of an auxiliary hypothesis (cut P, assert P) or term (pose x t)

• induction on integers, on inductive predicates

• instantiation as seen above (instantiate H t 1 , . . . ,t k ), including existential case (exists t), or via direct application of a hypothesis to a goal (apply H)

• various rewriting and computation transformations: rewrite H (in H ), replace t 1 t 2 (in H), subst x, subst_all, etc.

• context handling: remove H 1 , . . . , H k , clear_but ...

• unfolding a definition: unfold f

• import an extra theory: use_th T

Extending The Proof Session Mechanism

A proof session is essentially a record of all the proof tasks generated from a given input file, and also a record of all transformations applied to these tasks. It is indeed an internal representation of the proof task tree displayed on the left part of Figure 2. Such a session can be stored on disk, and can be reloaded to a former state by the user. A crucial feature of the session manager is to manage the changes if the input file is modified (e.g. more annotations are added): the manager implements a clever and sound merging operation to discover which parts of the proof session can be reused, which tasks are modified, and which external proofs should be replayed [START_REF] Franc ¸ois Bobot | Preserving User Proofs Across Specification Changes[END_REF]. The Why3 session files do not store any internal representation to avoid any problem when the Why3 tools themselves evolve. Accordingly, we decided that the arguments of transformations should be stored under their textual form too. This definitely avoids potential problems with changes in internal representations, but still some problems with renaming could occur. For example, an automatically introduced name for any hypothesis, say H1, could perfectly be renamed into H2, e.g. if an extra annotation is added in the source code. It is thus perfectly normal that from time to time, while reloading a proof session, a transformation with argument does not apply anymore. In order to avoid the loss of any sub-proof tree, we implemented the new notion of detached nodes in the proof task tree. These nodes are a record of the state of the previous session, but without any corresponding proof task. We then implemented a mechanism to copy and paste fragments of proof trees from one node to another. This copy-paste mechanism showed itself very useful in practice for maintaining interactive proofs.

Examples

We evaluated the new interactive proof features of Why3 on prior examples where some VCs could not be discharged except using the Coq proof assistant. Bobot et al. paper [START_REF] Franc ¸ois Bobot | Let's Verify This with Why3[END_REF] illustrated the use of Why3 on the three challenges of the VerifyThis competition in 2012. On each of these case studies, at least one Coq proof was required. We have reconsidered the first challenge (Longest Repeated Substring) and were able to replace all three Coq proofs with interactive proofs. Interestingly, only very few transformations were needed, because we quickly arrived at simpler subgoals that are discharged by automatic solvers.

Another illustrative example is the proof of Dijkstra's shortest path algorithm on graphs: again, we were able to replace Coq proofs with interactive transformations and automatic solvers. We noticed that not only does it simplify the proofs, they are now easier to maintain in case of a change in Why3 implementation or standard library.

We still have to evaluate to what extent the interaction using transformations with argument is easy to use for regular users. Moreover, we need more practice in order to see if this mechanism is of effective help for debugging proofs, as explained in the introduction.

Adding Interactive Proving in SPARK

Although the SPARK verifier, called GNATprove, is based on Why3 for generating VCs and proving them, there is a large gap between the SPARK and WhyML programming languages. Therefore, the interactive proof features of Why3 cannot be used directly by SPARK users. The same issue arose in the past with the counterexample generation features of Why3, which required translation back to SPARK for use inside GNATprove [START_REF] Hauzar | Counterexamples from Proof Failures in SPARK[END_REF]. That issue also involved interactions with users inside different IDEs, Why3IDE for Why3 users and GNAT Programming Studio for SPARK users, but that interaction was one-way only: the counterexamples output by provers were translated back to either Why3 or SPARK syntax and displayed in their respective IDE. Here, we need a two-way interaction where users can input commands (possibly with elements of the code as parameters) and Why3 returns a modified set of proof tasks.

We start by presenting a simple SPARK program that cannot be proved with automatic provers in Section 3.1. Then we describe in Section 3.2 the client-server architecture that we have adopted for twoway communication between the IDE for SPARK programs and Why3. We detail in Section 3.3 how we translate back and forth between user-level names in SPARK and internal names in Why3. Finally, we explain in Section 3.4 how to complete the proof of our example.

Unprovable Code Example

The code in Figure 4 is a simplified version of an excerpt from a bounded string library. This code contains a post-condition that cannot be proved today by any prover available with SPARK (Alt-Ergo, CVC4, Z3). The reason for this unproved property is characteristic of the kind of problems faced by users of a technology like SPARK. It is in the class of problems called quantifier instantiation already presented in Section 2.

The code in Figure 4 computes the location of a sub-list of integers within a list of integers, when the sub-list is contained in the list. Lists are implemented here as SPARK arrays starting at index 1 and ranging over positive indexes. The post-condition of function Location introduced by Post states the following properties: the result of the function ranges from 0 to the length of the list; a positive result is used when the sub-list is contained in the list, and value 0 is used as result otherwise. For the sake of sages attached to program lines. Between these two instants, GPS called GNATprove; GNATprove translated the SPARK program into an equivalent WhyML program w.r.t. axiomatic semantics for generation of VCs; an internal program using Why3 API successively generated VCs by calling Why3 VC generator and dispatched VCs to provers; this internal program collected the output of provers and returned the overall results to GNATprove; GNATprove generated and adapted results for GPS, that displayed these results to the user.

All this work occurred transparently for the user, who never had to see the generated WhyML code in Why3IDE, or to launch Why3 commands in a terminal. A less-than-ideal process for completing the proof of the post-condition would consist in asking the user to open the session file generated by Why3 in Why3IDE to complete the proof using the interactive proof feature described in Section 2. While this would work, this is not a suitable solution in an industrial context. Indeed, asking users to interact directly with a generated artifact in a different language (the Why3 file) is akin to asking them to debug their programs at assembly level. While this is possible and sometimes useful, it is best left to rare occasions when this is really needed, and instead interaction should be done as much as possible at source code level. Most modern IDEs like GPS provide client-server interfaces with various tools such as debuggers or, in the context of formal verification, with proof assistants such as Emacs Proof-General support for Coq, Isabelle, Lego, HOL, etc. We have adopted a client-server architecture to allow two-way communications between the interactive proof module (acting as a server) and the client IDE, which can be Why3IDE or GPS here. The server handles requests from the user (through the IDE), such as proof transformations (see Section 2.3) and direct calls to provers. After the requested action terminates, the server informs the IDE of changes to the proof task tree.

Client-Server Architecture

For the integration in GPS, we developed both a wrapper in OCaml for the underlying service to act as the server, and a plugin in Python to communicate with the server from GPS. The server takes the session file as initial argument, gets its input in JSON format on standard input, calls Why3 core services, updates the session file accordingly, and returns its output in JSON format on the standard output. The plugin modifies GPS interface to add a console window for command-line interaction, a window to display VCs and a window to display the proof task tree. The plugin translates requests made by the user on the command-line interface into JSON requests that are sent to the server, and translates back the server notifications into updates of the graphical user interface (adding nodes in the proof task tree, changing the VC, etc.). For example, as seen in Figure 5, GPS first starts the server, then the server returns the initial proof task tree which is printed by GPS. When the user clicks a node, GPS asks for the corresponding proof task which the server returns and GPS then prints it for the user. This goes on until the Figure 6: Example of interactive proof in GPS user exits manual proof which GPS interprets by sending the exit request: Why3 interactive server ends its execution. The death of the process is detected by GPS which goes back to its normal interface. A schematic of the interactions between the IDE and the server is depicted in Figure 5. With very little effort, we transformed a generic IDE such as GPS into an elementary proof assistant.

As seen on Figure 6, the user interface in GPS is similar to the one in Why3IDE presented in Figure 2. The same windows are present but they are not located at the same place. From left to right, we can see the SPARK code window, the proof task window and the proof task tree window. The command-line console is displayed as a bottom panel sharing its window with other panels for Messages (tool output) and Locations (tool messages). The user can type commands for applying transformations and calling provers inside the command-line console, similar to what we saw for Why3IDE.

One can observe that the VC from Figure 6 is much more complex than the simple VC we generated with Why3 in Figure 2. This is mainly a consequence of the complexity of the WhyML code generated from SPARK. Simple data structures and control flow in SPARK are modeled with much more complex data structures and control flow in WhyML to encode the semantic features of SPARK. This complexity gets exposed in the VC generated by Why3 VC generator, as it combines the complexity of data structures and control flow. This inherent complexity cannot be eliminated and must be dealt with to present SPARK users with understandable VCs.

Printing of Proof Tasks and Parsing of Transformation Arguments

In order for users to be able to relate the proof task to their code, it is necessary to use the names of source SPARK entities in the proof task instead of the generated Why3 names. This is achieved by creating a mapping from Why3 names to their source SPARK name during the generation of Why3 code from SPARK. This mapping is embedded in the WhyML code using labels, a generic mechanism in Why3 to attach strings to terms. For example, in the following code snippet the label "name:Not_y" is attached to the identifier y: let f (a:array int) (x:int) : int ensures {result = 20} = let y "name:Not_y" = 2*x+1 in y*y Labels on terms are preserved by VC generation and transformations. For example, the label "name :Not_y" remains attached to the constants derived from y in the final VC obtained after VC generation and transformations. Thus, when printing a proof task, the name of an identifier can be replaced by the name found in the attached label when there is one. Thus we get the following proof task where the source SPARK name Not_y is used instead of the generated Why3 name y: Different Why3 names with the same name label are currently distinguished by appending a unique number to the source SPARK name. The consecutive problem of interpreting the names of SPARK entities as Why3 names occurs when the user types a command with arguments referring to the names of SPARK entities. Why3 uses here the inverse map from distinguished SPARK names to Why3 names associated to a given proof task to translate automatically the arguments of transformations.

Application to the Unprovable Code Example

With the interactive proof interface in GPS, we complete the proof of the post-condition of Location from Section 3.1. For the sake of simplicity, we only describe the proof part of the then branch in this subsection, shown in the screenshot in Figure 6. The root of the proof task tree is green, showing that the initial VC was fully proved.

The interactive proof proceeds by deriving a contradiction from the loop invariant property in the last iteration of the loop and the condition of the then branch Contains (Within, Fragment). This requires unfolding the definition of Contains and finding suitable instances of quantified properties. In this case, the proof task tree is linear and a complete proof script is the following: instantiate contains__def_axiom Within,Fragment rewrite Hinst in H16 destruct H16 destruct H destruct H instantiate H18 k

The intuition of the proof is that we need to explain to the tool how to combine the hypotheses coming from the loop invariant and the definition of Contains. The first two transformations (instantiate, rewrite) are used to make the axiomatic definition of Contains, applied to the right arguments, appear as a hypothesis in the context. The three calls to the destruct transformation are used to destruct the head connective of the hypothesis that appeared. They transform Γ, H : (A ∧ ∃k.P(k)) G into Γ, H : A, k : int, H 1 : P(k) G. The objective is to use k as an instance for the loop invariant property (to make the contradiction appear). This is exactly what transformation "instantiate H18 k" does. The quantification disappears and SMT solvers can now solve the goal. This completes the proof of the then branch of the post-condition of Location. The else branch is handled similarly, which completes the proof of the program.

Conclusions and Future Work

We brought interactive proving features to the SPARK verification environment for Ada. This was done by conservatively extending the intermediate Why3 tool by allowing to pass arguments to proof task transformations. The design is generic enough to allow simple addition of new transformations via Why3's API. The proof session mechanism and the graphical interface have been extended to allow simple user interaction and facilities for proof maintenance. A few program examples were re-proved, showing that former external interactive proofs using Coq can be substituted with light interactive proofs in our new setting. The user interface of Why3 was redesigned under the form of a generic client-server architecture, allowing to bring interactive proving features to the SPARK front-end inside the regular GPS graphical interface.

Future Work will go into several directions. First, we certainly want to enlarge the set of transformations with arguments, to cover more needs for interactive proofs. The needed transformations will be identified from practice. Notice that others are already reusing our API to implement new transformations, for example for doing proofs by reflection for complex non-linear goals [START_REF] Melquiond | A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms[END_REF]. Second, we plan to reuse the client-server architecture to provide an alternative interface for Why3, this time within a web browser. We also plan to bring the interactive proof feature to the Frama-C front-end for C code, by augmenting the existing Jessie plug-in of Frama-C that uses Why3 internally. A third longer-term work is to allow for more customization of the printing of tasks and the parsing of transformation arguments: from SPARK, we would like the terms in proof tasks expressed in a more Ada-like syntax, in particular for arrays. For this we will need to design in Why3's generic API a possibility to register printers and parsers. A fourth even longer-term issue is the question of trust in the implemented transformations. Since we implement more and more complex OCaml code for that purpose, a general need for verifying the soundness of the transformations shows up. It is likely that we will need to design a language of proof terms or proof certificates to achieve this long-term goal.

Figure 1 :

 1 Figure 1: Why3 general architecture

Figure 2 :

 2 Figure 2: Failed proof attempts shown in Why3IDE

Figure 3 :

 3 Figure 3: Completed proof using two possible transformations with arguments

  replace y*y 4*(x*x+x)+1 in the input field and hit the return key. An alternative possible transformation would be to instantiate the hypothesis H with x*x+x, which can be done with the input instantiate H x*x+x

Figure 3

 3 Figure3displays the GUI after trying both transformations. As seen on left, the transformation replace y*y 4*(x*x+x)+1 generated two subgoals: first proving the formula after the replacement, second proving that y*y=4*(x*x+x)+1. Both subgoals are proved by Alt-Ergo. Similarly, the transformation "instantiate H x*x+x" generates one subgoal where an additional hypothesis is present (the instance of H for the given particular value for i) and is also proved by Alt-Ergo. As can be seen, applying any of these two transformations is enough to finish the proof automatically.Even if this mechanism using a textual interface may seem old-fashioned, it permits a lot of genericity. We'll see below how it simplifies the communication with a front-end such as SPARK. It also permits a lot of extra features that show themselves important in practice, such as searching in the proof context.

  type _ trans_typ = | Ttrans_l : (task -> task list) trans_typ (** transformation with no argument, and many resulting tasks *) | Tstring : 'a trans_typ -> (string -> 'a) trans_typ (** transformation with a string as argument *) | Tprsymbol : 'a trans_typ -> (Decl.prsymbol -> 'a) trans_typ (** transformation with a Why3 proposition symbol as argument *) | Tterm : 'a trans_typ -> (Term.term -> 'a) trans_typ (** transformation with a Why3 term as argument *) | Topt : string * ('a -> 'c) trans_typ -> ('a option -> 'c) trans_typ (** transformation with an optional argument. The first string is the keyword introducing that optional argument*)

Figure 5 :

 5 Figure 5: Schematic of the interactions between IDE and server

  constant x : int constant Not_y : int = (2 * x) + 1 goal VC f : (Not_y * Not_y) = 20

* Work partly supported by the Joint Laboratory ProofInUse (ANR-13-LAB3-0007, https://www.adacore.com/ proofinuse) of the French national research organization

simplicity, we do not state the complete post-condition of Location (that would make precise that the resulting index is the location of the match), but this could be done easily.

This post-condition relies on the definition in function Contains of what it means for a sub-list Fragment to be contained in a list Within. This function is only used in specifications, which is enforced by marking it as Ghost. It is defined as an expression function, quantifying with for some (Ada existential quantification) over a range of scalar values the property that the sub-list Fragment is equal to a moving slice of the list Within (K .. (K -1 + Fragment'Length)). This last expression is the slice of array Within from index K to index (K -1 + Fragment'Length).

For the sake of simplicity, function Location naively iterates over each possible location for a match and tests for equality of the corresponding slice with the argument sub-list. The loop invariant repeats the post-condition and specializes it for the K th iteration of the loop, so that the loop invariant is itself provable and can be used to prove the post-condition.

When running GNATprove on this code, it proves automatically the absence of runtime errors (no integer overflows, no array access out of bounds, no other runtime check failures), as well as the loop invariant in function Location, but it does not prove the post-condition of that function.

The user interaction is simple here. The user requests that this program is verified by GNATprove inside GPS (GNAT Programming Studio), and a few seconds later receives the output of the tool as mes-


Matthias Függer
email: mfuegger@lsv.fr

Thomas Nowak
email: thomas.nowak@lri.fr

Fast Multidimensional Asymptotic and Approximate Consensus

Keywords: 2012 ACM Subject Classification Theory of computation → Distributed algorithms asymptotic consensus, approximate consensus, multidimensional data, dynamic networks, Byzantine processes Digital Object Identifier 10.4230/LIPIcs.DISC.2018.27 Fast Multidimensional Asymptotic and Approximate Consensus

We study the problems of asymptotic and approximate consensus in which agents have to get their values arbitrarily close to each others' inside the convex hull of initial values, either without or with an explicit decision by the agents. In particular, we are concerned with the case of multidimensional data, i.e., the agents' values are d-dimensional vectors. We introduce two new algorithms for dynamic networks, subsuming classical failure models like asynchronous message passing systems with Byzantine agents. The algorithms are the first to have a contraction rate and time complexity independent of the dimension d. In particular, we improve the time complexity from the previously fastest approximate consensus algorithm in asynchronous message passing systems with Byzantine faults by Mendes et al. [Distrib. Comput. 28]

where ∆ is the initial and ε is the terminal diameter of the set of vectors of correct agents.

Introduction

The problem of one-dimensional asymptotic consensus requires a system of agents, starting from potentially different initial real values, to repeatedly set their local output variables such that all outputs converge to a common value within the convex hull of the inputs. This problem has been studied in distributed control theory both from a theoretical perspective [START_REF] Chazelle | The total s-energy of a multiagent system[END_REF][START_REF] Moreau | Stability of multiagent systems with time-dependent communication links[END_REF][START_REF] Cao | Reaching a consensus in a dynamically changing environment: convergence rates, measurement delays, and asynchronous events[END_REF][START_REF] Angeli | Stability of leaderless discrete-time multi-agent systems[END_REF] and in the context of robot gathering on a line [START_REF] Bouzid | Optimal Byzantine-resilient convergence in uni-dimensional robot networks[END_REF] and clock synchronization [START_REF] Olfati | Consensus problems in networks of agents with switching topology and time-delays[END_REF][START_REF] Li | Global clock synchronization in sensor networks[END_REF].

Extensions of the problem to multidimensional values naturally arise in the context of robot gathering on a plane or three-dimensional space [START_REF] Cieliebak | Solving the robots gathering problem[END_REF], as subroutines in formation forming [START_REF] Chazelle | The total s-energy of a multiagent system[END_REF], and distributed optimization [START_REF] Boyd | Convex optimization[END_REF], among others.

The related problem of approximate consensus, also called approximate agreement, requires the agents to eventually decide, i.e., to only set their output variables once. Additionally all output variables must be within a predefined ε > 0 distance of each other and lie within the convex hull of the inputs. There is a large body of work on approximate consensus in distributed computing devoted to solvability and optimality of time complexity [START_REF] Dolev | Reaching approximate agreement in the presence of faults[END_REF][START_REF] Fekete | Asymptotically optimal algorithms for approximate agreement[END_REF] and applications in clock synchronization; see e.g. [24,23].

Both problems were studied under different assumptions on the underlying communication between agents and their computational strength, including fully connected asynchronous message passing with Byzantine agents [24,[START_REF] Dolev | Reaching approximate agreement in the presence of faults[END_REF] and communication in rounds by message passing in dynamic communication networks [START_REF] Moreau | Stability of multiagent systems with time-dependent communication links[END_REF][START_REF] Chazelle | The total s-energy of a multiagent system[END_REF]. In [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF][START_REF] Charron-Bost | Fast, robust, quantizable approximate consensus[END_REF] Charron-Bost et al. analyzed solvability of asymptotic consensus and approximate consensus in dynamic networks with round-wise message passing defined by network models: a network model is a set of directed communication graphs, each of which specifies successful reception of broadcast messages; see Section 2.1 for a formal definition. Solving asymptotic consensus in such a model requires to fulfill the specification of asymptotic consensus in any sequence of communication graphs from the model. Charron-Bost et al. showed that in these highly dynamic networks, asymptotic consensus and approximate consensus are solvable in a network model if and only if each of its graphs contains a spanning rooted tree. An interesting class of network models are those that contain only non-split communication graphs, i.e., communication graphs where each pair of nodes has a common incoming neighbor. Several classical fault-models were shown to be instances of non-split models [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF], among them asynchronous message passing systems with omissions.

Recently the multidimensional version of approximate consensus received attention. Mendes et al. [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF] were the first to present algorithms that solve approximate consensus in Byzantine message passing systems for d-dimensional real vectors. Their algorithms, Mendes-Herlihy and Vaidya-Garg, are based on the repeated construction of so called safe areas of received vectors to constraint influence of values sent by Byzantine agents, followed by an update step, ensuring that the new output values are in the safe area. They showed that the diameter of output values contracts by at least 1/2 in each dimension every d rounds in the Mendes-Herlihy algorithm, and the diameter of the output values contracts by at least 1 -1/n every round in the Vaidya-Garg algorithm, where n is the number of agents. The latter bound assumes f = 0 Byzantine failures and slightly worsens for f > 0.

In terms of contraction rates as introduced in [START_REF] Függer | Tight bounds for asymptotic and approximate consensus[END_REF] (see Section 2.3 for a definition) of the respective non-terminating algorithms for asymptotic consensus, they thus obtain upper bounds of d 1/2 and 1 -1/n. Note that the Mendes-Herlihy algorithm has a contraction rate depending only on d but requires an a priori common coordinate system, and the algorithm's outcome depends on the choice of this coordinate system. By contrast the Vaidya-Garg algorithm is coordinate-free, i.e., its outcome is invariant under coordinate transformations such as translation and rotation, but it has a contraction rate depending on n.

Charron-Bost et al. [START_REF] Charron-Bost | Multidimensional asymptotic consensus in dynamic networks[END_REF] analyzed convergence of the Centroid algorithm where agents repeatedly update their position to the centroid of the convex hull of received vectors. The algorithm is coordinate-free and has a contraction rate of d/(d + 1), independent of n. Local time complexity of determining the centroid was shown to be #P-complete [START_REF] Rademacher | Approximating the centroid is hard[END_REF] while polynomial in n for fixed d.

The contraction rate of the Centroid algorithm is always smaller or equal to that of the Mendes-Herlihy algorithm, though both contraction rates converge to 1 at the same speed with the dimension d going to infinity. More precisely,

lim d→∞ 1 -d 1 2 1 -d d+1 = log 2 , which implies 1 -d 1 2 = Θ 1 -d d+1 .

Contribution

In this work we present two new algorithms that are coordinate-free: the MidExtremes and the ApproachExtreme algorithm, and study their behavior in dynamic networks. Both algorithms are coordinate-free, operate in rounds, and are shown to solve asymptotic agreement in non-split network models. Terminating variants of them are shown to solve approximate agreement in non-split network models.

As a main result we prove that their contraction rate is independent of network size n and dimension d of the initial values. For MidExtremes we obtain an upper bound on the contraction rate of 7/8 and for ApproachExtreme of 31/32. Due to the fact that classical failure models like asynchronous message passing with Byzantine agents possess corresponding network models, our results directly yield improved algorithms for the latter failure models: In particular, we improve the time complexity from the previously fastest approximate consensus algorithm in asynchronous message passing systems with Byzantine faults, the Mendes-Herlihy algorithm, from Ω d log d∆ ε to O log ∆ ε , where ∆ is the initial and ε is the terminal diameter of the set of vectors of correct agents. Note that our algorithms share the benefit of being coordinate-free with the Vaidya-Garg algorithm presented in the same work.

Table 1 summarizes our results and the algorithms discussed above for asymptotic and approximate consensus. The table compares the new algorithms MidExtremes and ApproachExtreme to the Centroid, Mendes-Herlihy (MH), and Vaidya-Garg (VG) algorithms with respect to their local time complexity per agent and round and an upper bound on their contraction rate in non-split network models. A lower bound of 1/2 on the contraction rate is due to Függer et al. [START_REF] Függer | Tight bounds for asymptotic and approximate consensus[END_REF]. The Mendes-Herlihy algorithm has a smaller contraction rate than the MidExtremes algorithm whenever d 10; the Centroid algorithm whenever d 14. The Centroid algorithm is hence the currently fastest known algorithm for dimensions 3 d 14. For dimensions d = 1 and d = 2, the componentwise MidPoint algorithm has an optimal contraction rate of 1/2 [START_REF] Charron-Bost | Multidimensional asymptotic consensus in dynamic networks[END_REF]. Note that the MidExtremes algorithm is equivalent to the componentwise MidPoint algorithm for dimension d = 1. For d 15, the MidExtremes algorithm is the currently fastest known algorithm.

We finally note that all our results hold for the class of inner product spaces and are not restricted to the finite-dimensional Euclidean spaces R d , in contrast to previous work. For example, this includes the set of square-integrable functions on a real interval. However, finite value representation and means to calculate the norm have to be guaranteed. Further, local TIME becomes n 2 , respectively, n norm calculations.

Model and Problem

We fix some vector space V with an inner product •, • : V × V → R and the norm x = x, x . The prototypical finite-dimensional example is V = R d with the usual inner product and the Euclidean norm. The diameter of set A ⊆ V is denoted by diam(A) = sup

x,y∈A x -y .

For an n-tuple x = (x 1 , . . . , x n ) ∈ V n of vectors in V , we write diam(x) by slight abuse of notation to denote diam {x 1 , . . . , x n } .

Dynamic Network Model

We consider a distributed system of n agents that communicate in rounds via message passing, like in the Heard-Of model [START_REF] Charron-Bost | The Heard-Of model: computing in distributed systems with benign faults[END_REF]. In each round, each agent i, broadcasts a message based on its local state, receives some messages, and then updates its local state based on the received messages and its local state. Rounds are communication closed: agents only receive messages sent in the same round.

In each round t 0, messages are delivered according to the directed communication graph G t for round t: the message broadcast by i in round t is received by j if and only if the directed edge (i, j) is in G t . Agents always receive their own messages, i.e., (i, i) ∈ G t . A communication pattern is an infinite sequence G 1 , G 2 , . . . of communication graphs. A (deterministic) algorithm specifies, for each agent i, the local state space of i, the set of initial states of i, the sending function for which message to broadcast, and the state transition function. For asymptotic consensus, each agent i's local state necessarily contains a variable y i ∈ V , which initially holds i's input value and is then used as its output variable. We require that there is an initial state with initial value v for all vectors v ∈ V . A configuration is an n-tuple of local states. It is called initial if all local states are initial. The execution of an algorithm from initial configuration C 0 induced by communication pattern

G 1 , G 2 , . . . is the unique sequence C 0 , G 1 , C 1 , G 2 , C 2 , .
. . alternating between configurations and communication graphs where C t is the configuration obtained by delivering messages in round t according to communication graph G t , and applying the sending and local transition functions to the local states in C t-1 according to the algorithm. For a fixed execution and a local variable z of the algorithm, we denote by z i (t) its value at i at the end of round t, i.e., in configuration C t . In particular, y i (t) is the value of y i in C t . We write y(t) = y 1 (t), . . . , y n (t) for the collection of the y i (t).

A specific class of algorithms for asymptotic consensus are the so-called convex combination, or averaging, algorithm, which only ever update the value of y i inside the convex hull of y j it received from other agents j in the current round. Many algorithms in the literature belong to this class, as do ours.

Following [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF], we study the behavior of algorithms for communication patterns from a network model, i.e., a non-empty set of communication patterns: a communication pattern is from network model N if all its communication graphs are in N . We will later on show that such an analysis also allows to prove new performance bounds for more classical fault-models like asynchronous message passing systems with Byzantine agents.

An interesting class of network models are so called non-split models, i.e., those that contain only non-split communication graphs: a communication graph is non-split if every pair of nodes has a common in-neighbor. Charron-Bost et al. [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF] showed that asymptotic and approximate consensus is solvable efficiently in these network models in the case of one dimensional values. They further showed that: (i) In the weakest (i.e., largest) network model in which asymptotic and approximate consensus are solvable, the network model of all communication graphs that contain a rooted spanning tree, one can simulate non-split communication graphs. (ii) Classical failure models like link failures as considered in [22] and asynchronous message passing systems with crash failures have non-split interpretations. Indeed we will make use of such a reduction from non-split network models to asynchronous message passing systems with Byzantine failures in Section 3.2.

Problem Formulation

An algorithm solves the asymptotic consensus problem in a network model N if the following holds for every execution with a communication pattern from N :

Convergence. For every agent i, the sequence y i (t) t 0 converges. Agreement. If y i (t) and y j (t) converge, then they have a common limit.

Validity. If y i (t) converges, then its limit is in the convex hull of the initial values y 1 (0), . . . , y n (0).

For the deciding version, the approximate consensus problem (see, e.g., [START_REF] Lynch | Distributed Algorithms[END_REF]), we augment the local state of i with a variable d i initialized to ⊥. Agent i is allowed to set d i to some value v = ⊥ only once, in which case we say that i decides v. In addition to the initial values y i (0), agents initially receive the error tolerance ε and an upper bound ∆ on the maximum distance of initial values. An algorithm solves approximate consensus in N if for all ε > 0 and all ∆, each execution with a communication pattern in N with initial diameter at most ∆ satisfies:

Termination. Each agent eventually decides. ε-Agreement. If agents i and j decide d i and d j , respectively, then

d i -d j ε. Validity. If agent i decides d i , then d i is in the convex hull of initial values y 1 (0), . . . , y n (0).

Performance Metrics

A direct natural performance metric to assess the speed of convergence of agent outputs y along an execution is the round-by-round convergence rate

c(t) = diam y(t) diam y(t -1)
for a given round t 1 in the respective execution. The round-by-round convergence rate is the supremum over all executions and rounds. While a uniform upper bound of β < 1 on the round-by-round convergence rate establishes convergence of the outputs, this measure fails in establishing convergence and comparing speeds of convergence for several algorithms considered in literature that set their output values every k > 1 rounds, or that do not converge during an initial phase.

The convergence rate, defined by lim sup

t→∞ t diam y(t) ,
allows a comparison in this case by measuring eventual amortized convergence speed. For example, an algorithm that eventually contracts by a factor β < 1 every k 1 rounds has a convergence rate of k √ β. As a performance measure for general asymptotic consensus algorithms, where agents do not necessarily set their outputs y to within the convex hull of previously received vales, [START_REF] Függer | Tight bounds for asymptotic and approximate consensus[END_REF] considered the contraction rate, measuring contraction of reachable output limits rather D I S C 2 0 1 8

27:6

Fast Multidimensional Asymptotic and Approximate Consensus than output values: Following [START_REF] Függer | Tight bounds for asymptotic and approximate consensus[END_REF], the valency of a configuration C, denoted by Y * (C), is defined as the set of limits of the values y i in executions that include configuration C. If the execution is clear from the context, we abbreviate Y * (t) = Y * (C t ). The contraction rate of an execution is then defined as lim sup

t→∞ t diam Y * (t) .
The contraction rate of an algorithm in a network model is the supremum of the contraction rates of its executions. For convex combination algorithms, the contraction rate is always upper-bounded by its convergence rate, that is, lim sup

t→∞ t diam Y * (t) lim sup t→∞ t diam y(t) ,
since the set of reachable limits Y * (t) at round t is contained in the set of output values {y 1 (t), . . . , y n (t)} at round t for these algorithms.

Clearly, an algorithm that guarantees a round-by-round convergence rate of c(t) β also guarantees a convergence rate of at most β. Since both of our algorithms are convex combination algorithms, all our upper bounds on the round-by-round convergence rates are also upper bounds for the contraction rates.

The convergence time of a given execution measures the time from which on all values are guaranteed to be in an ε of each other. Formally, it is the function defined as

T (ε) = min t 0 | ∀τ t : diam y(τ ) ε .
In an execution that satisfies c(t) β for all t 1, we have the bound T (ε) log 1/β ∆ ε on the convergence time, where ∆ = diam y(0) is the diameter of the set of initial values.

Algorithms

In this section, we introduce two new algorithms for solving asymptotic and approximate consensus in arbitrary inner product spaces with constant contraction rates. We present our algorithms and prove their correctness and bounds on their performance in non-split networks models. While we believe that this framework is the one in which our arguments are clearest, our results can be extended to a number of other models whose underlying communication graphs turn out to be, in fact, non-split. The following is a selection of these models:

Rooted network models: This is the largest class of network models in which asymptotic and approximate consensus are solvable [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF]. A network model is rooted if all its communication graphs include a directed rooted spanning tree, though not necessarily the same in all graphs. Although not every such communication graph is non-split, Charron-Bost et al. [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF] showed that the cumulative communication graph over n -1 rounds in a rooted network model is always non-split. In such network models, one can use amortized versions [START_REF] Charron-Bost | Fast, robust, quantizable approximate consensus[END_REF] of the algorithms, which operate in macro-rounds of n -1 rounds each. If an algorithm has a contraction rate β in non-split network models, then its amortized version has contraction rate n-1 √ β in rooted network models. The amortized versions of our algorithms thus have contraction rates independent of the dimension of the data. Omission faults: In the omission fault model studied by Santoro and Widmayer [22], the adversary can delete up to t messages from a fully connected communication graph each round. If t n -1, then all communication graphs are non-split. If t 2n -3, then all communication graphs are rooted [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF]. Our algorithms are hence applicable in both these cases and have contraction rates independent of the dimension. Asynchronous message passing with crash faults: Building asynchronous rounds atop of asynchronous message passing by waiting for n -f messages in each round, the resulting communication graphs are non-split as long as the number f of possible crashes is strictly smaller than n/2. We hence get a constant contraction rate using our algorithms also in this model. For f n/2, a partition argument shows that neither asymptotic nor approximate consensus are solvable. Asynchronous message passing with Byzantine faults: Mendes et al. [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF] showed that approximate consensus is solvable in asynchronous message passing systems with f Byzantine faults if and only if n > (d + 2)f where d is the dimension of the data. The algorithms they presented construct a round structure whose communication graphs turn out to be non-split. Since the construction is not straightforward, we postpone the discussion of our algorithms in this model to Section 3.2.

Non-split Network Models

We now present our two new algorithms, MidExtremes and ApproachExtreme. Both operate in the following simple round structure: broadcast the current value y i and then update it to a new value depending on the set Rcv i of values y j received from agents j in the current round. Both of them only need to calculate distances between values and form the midpoint between two values. In particular, we do not need to make any assumption on the dimension of the space of possible values for implementing the algorithms. We only need a distance and an affine structure, for calculating the midpoint. Our correctness proofs, however, rely on the fact that the distance function is a norm induced by an inner product.

Note that, although we present algorithms for asymptotic consensus, combined with our upper bounds on the convergence time, one can easily deduce versions for approximate consensus by having the agents decide after the upper bound. Our upper bounds only depend on the precision parameter ε and (an upper bound on) the initial diameter ∆. While upper bounds on the initial diameter cannot be deduced during execution in general non-split network models, it can be done in specific models, like asynchronous message passing with Byzantine faults [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF]. Otherwise, we need to assume an a priori known bound on the initial diameter to solve approximate consensus.

The algorithm MidExtremes, which is shown in Algorithm 1, updates its value y i to the midpoint of a pair of extremal points of Rcv i that realizes its diameter. In the worst case, it thus has to compare the distances of Θ(n 2 ) pairs of values. For the specific case of Euclidean spaces V = R d stored in a component-wise representation, this amounts to O(n 2 d) local scalar operations for each agent in each round.

It turns out that we can show a round-by-round convergence rate of the MidExtremes algorithm independent of the dimension or the number of agents, namely 7/8. For the specific case of values from the real line V = R, it reduces to the MidPoint algorithm [START_REF] Charron-Bost | Fast, robust, quantizable approximate consensus[END_REF], whose contraction rate of 1/2 is known to be optimal [START_REF] Függer | Tight bounds for asymptotic and approximate consensus[END_REF].

Theorem 1. In any non-split network model with values from any inner product space, the MidExtremes algorithm guarantees a round-by-round convergence rate of c(t)

7/8 for all rounds t 1. Its convergence time is at most

T (ε) = log √ 8/7 ∆ ε
where ∆ is the diameter of the set of initial values.

D I S C

y i ← a + b 2
In the particular case of values from the real line, it guarantees a round-by-round convergence rate of c(t) 1/2 and a convergence time of

T (ε) = log 2 ∆ ε .
The second algorithm we present is called ApproachExtreme and shown in Algorithm 2. It updates its value y i to the midpoint of the current value of y i and the value in Rcv i that is the farthest from it. While having the benefit of only having to compare O(n) distances, and hence doing O(nd) local scalar operations for each agent in each round in the case of V = R d with component-wise representation, the ApproachExtreme algorithm also only has to measure distances from its current value to other agents' values; never the distance of two other agents' values. This can be helpful for agents embedded into the vector space V that can measure the distance from itself to another agent, but not necessarily the distance between two other agents.

Algorithm 2 Asymptotic consensus algorithm ApproachExtreme for agent i Initialization:

1: y i is the initial value in V In round t 1 do:

2: broadcast y i 3: Rcv i ← set of received values 4: b ← arg max b∈Rcvi y i -b 5: y i ← y i + b 2
The ApproachExtreme algorithm admits an upper bound of 31/32 on its round-byround convergence rate, which is worse than the 7/8 of the MidExtremes algorithm. For the case of the real line V = R, we can show a round-by-round convergence rate of 3/4, however.

Theorem 2. In any non-split network model with values from any inner product space, the ApproachExtreme algorithm guarantees a round-by-round convergence rate of c(t)

31 32 for all rounds t 1. Its convergence time is at most

T (ε) = log √ 32/31 ∆ ε
where ∆ is the diameter of the set of initial values.

In the particular case of values from the real line, it guarantees a round-by-round convergence rate of c(t) 3/4 and a convergence time of

T (ε) = log 4/3 ∆ ε .

Asynchronous Byzantine Message Passing

We now show how to adapt algorithm MidExtremes to the case of asynchronous message passing systems with at most f Byzantine agents. The algorithm proceeds in the same asynchronous round structure and safe area calculation used by Mendes et al. [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF] whenever approximate consensus is solvable, i.e., when n > (d + 2)f . Plugging in the MidExtremes algorithm, we achieve a round-by-round convergence rate and round complexity independent of the dimension d.

More specifically, our algorithm has a round complexity of O log ∆ ε , which leads to a message complexity of O n 2 log ∆ ε where ∆ is the maximum Euclidean distance of initial vectors of correct agents. In contrast, the Mendes-Herlihy algorithm has a worst-case round complexity of Ω d log d∆ ε and a worst-case message complexity of Ω n 2 d log d∆ ε . We are thus able to get rid of all terms depending on the dimension d.

After an initial round estimating the initial diameter of the system, the Mendes-Herlihy algorithm has each agent i repeat the following steps in each coordinate k ∈ {1, 2, . . . , d} for Θ log d∆ ε rounds:

1. Collect a multiset V i of agents' vectors such that every intersection V i ∩ V j has at least n -f elements via reliable broadcast and the witness technique [START_REF] Abraham | Optimal resilience asynchronous approximate agreement[END_REF]. 2. Calculate the safe area S i as the intersection of the convex hulls of all sub-multisets of V i of size |V i | -f . The safe area is guaranteed to be a subset of the convex hull of vectors of correct agents. Helly's theorem [START_REF] Danzer | Helly's theorem and its relatives[END_REF] can be used to show that every intersection S i ∩ S j of safe areas is nonempty. 3. Update the vector y i to be in the safe area S i and have its k th coordinate equal to the midpoint of the set of k th coordinates in S i .

The fact that safe areas have nonempty pairwise intersections guarantees that the diameter in the k th coordinate

δ k (t) = max i,j correct y (k) i (t) -y (k) j (t)
at the end of round t fulfills δ k (t) δ k (t -1)/2 if round t considers coordinate k. The choice of the number of rounds for each coordinate guarantees that we have δ k (t) ε/ √ d after the last round for coordinate k. This in turn makes sure that the Euclidean diameter of the set of vectors of correct agents after all of the Θ d log d∆ ε rounds is at most ε. The article of Mendes et al. [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF] describes a second algorithm, the Vaidya-Garg algorithm, which replaces steps 2 and 3 by updating y i to the non-weighted average of arbitrarily chosen points in the safe areas of all sub-multisets of V i of size n -f . Another difference to the Mendes-Herlihy algorithm is that it repeats the steps not several times for every dimension, but for Θ n f +1 log d∆ ε rounds in total. The Vaidya-Garg algorithm comes with the advantage of not having to do the calculations to find a midpoint for the k th coordinate while remaining inside the safe area, but also comes with the cost of a convergence rate and a round complexity that depends on the number of agents.

The algorithm we propose has the same structure as the Mendes-Herlihy algorithm, with the following differences: (i) like the Vaidya-Garg algorithm it is missing the loop over all coordinates one-by-one, and (ii) we replace step 3 by updating vector y i to the midpoint of two points that realize the Euclidean diameter of the safe area S i . According to our results in Section 4.1, the Euclidean diameter This means that we have δ(T ) ε after

δ(t) = max i,j correct
T (ε) = log √ 8/7
∆ ε rounds.

Performance Bounds

We next show upper bounds on the round-by-round convergence rate for algorithms MidExtremes (Theorem 1) and ApproachExtreme (Theorem 2) in non-split network models.

Bounds for MidExtremes

For dimension 1, MidExtremes is equivalent to the MidPoint Algorithm. We hence already know that c(t) 1 2 from [START_REF] Charron-Bost | Fast, robust, quantizable approximate consensus[END_REF], proving the case of the real line in Theorem 1. For the case of higher dimensions we will show that c(t) 7 8 holds. The proof idea is as follows: For a round t 1, we consider two agents i, j whose distance realizes diam(y(t)). By the algorithm we know that both agents set their y i (t) and y j (t) according to y i (t) = m = (a + b)/2 and y j (t) = m = (a + b )/2, where a, b are the extreme points received by agents i in round t and a , b are the extreme points received by agents j in the same round. All four points must lie within a common subspace of dimension 3, and form the vertices of a tetrahedron as depicted in Figure 1.

Further, any three points among a, b, a , b must lie within a 2 dimensional subspace, forming a triangle. Lemma 3 states the distance from the midpoint of two of its vertices to the opposite vertex, say c, and an upper bound in case the two edges incident to c are upper bounded in length.

27:11

In particular, if a -c γ and b -c γ, then

m -c 2 γ 2 - 1 4 a -b 2 .
Proof. We begin by calculating

a -c 2 = (a -m) + (m -c) 2 = a -m 2 + m -c 2 + 2 a -m, m -c (1) and b -c 2 = (b -m) + (m -c) 2 = b -m 2 + m -c 2 + 2 b -m, m -c . ( 2
)
Adding ( 1) and ( 2), while noting a -

m 2 = b -m 2 = 1 4 a -b 2 and a -m = (a -b)/2 = -(b -m), gives a -c 2 + b -c 2 = 1 2 a -b 2 + 2 m -c 2 .
Rearranging the terms in the last equation concludes the proof.

We are now in the position to prove Lemma 4 that is central for Theorem 1. The lemma provides an upper bound on the distance d between m and m for the tetrahedron in Figure 1 given that all its sides are upper bounded by some γ 0 and the sum of the lengths of edge a, b and a , b , i.e., a -b + a -b , is lower bounded by γ. At the heart of the proof of Lemma 4 is an application of Lemma 3 for the three hatched triangles in Figure 1.

m -b 2 γ 2 - 1 4 a -b 2 . ( 5
)
Now, again using Lemma 3 with the points a , b , m and the bounds of ( 4) and ( 5), we get

m -m 2 γ 2 - 1 4 a -b 2 + a -b 2 .
Using the second inequality in (3) then shows

m -m 2 γ 2 - 1 4 a -b 2 + γ -a -b 2 . ( 6
)
Setting ξ = a -b , we get

m -m 2 max 0 ξ γ γ 2 - 1 4 ξ 2 + (γ -ξ) 2 .
D I S C 2 0 1 8

27:12

Fast Multidimensional Asymptotic and Approximate Consensus

Differentiating the function f (ξ) = γ 2 -1 4 ξ 2 + (γ -ξ) 2 reveals that its maximum is attained for -(2ξ -γ) = 0, i.e., ξ = γ/2, which gives

m -m 2 γ 2 - γ 2 8 = 7 8 γ 2 .
Taking the square root now concludes the proof.

We can now prove Theorem 1. For the proof we consider the tetrahedron with vertices a, b, a , b as discussed before; see Figure 1. Recalling that the vertices a, b are vectors received by an agent i and a , b vectors received by an agent j in the same round, we may infer from the non-split property that all communication graphs must fulfill that both i and j must have received a common vector from an agent. Together with the algorithm's rule of picking a, b and a , b as extreme points, we obtain the constraints required by Lemma 4. Invoking this lemma we finally obtain an upper bound on the distance d between m and m , and by this an upper bound on the round-by-round convergence rate of the MidExtremes algorithm.

Proof of Theorem 1. Let i and j be two agents. Let a, b ∈ Rcv i (t) such that y i (t) = (a+b)/2 and a , b ∈ Rcv j (t) such that y j (t) = (a + b )/2. Define γ ij = diam {a, b, a , b } . Since a, b, a , b are the vectors of some agents in round t -1, we have γ ij diam y(t -1) .

Further, from the non-split property, there is an agent k whose vector c = y k (t -1) has been received by both i and j, i.e., c ∈ Rcv i (t) ∩ Rcv j (t). By the choice of the extreme We can hence apply Lemma 4 to obtain

y i (t) -y j (t) 7 8 γ ij 7 8 diam y(t -1) .
Taking the maximum over all pairs of agents i and j now shows diam y(t) 7/8 diam y(t-1) , which concludes the proof.

Bounds for ApproachExtreme

We start by showing the one-dimensional case of Theorem 2, i.e., V = R, in Section 4.2.1. Section 4.2.2 then covers the multidimensional case.

One-dimensional Case

For the proof we use the notion of -safety as introduced by Charron-Bost et al. [START_REF] Charron-Bost | Fast, robust, quantizable approximate consensus[END_REF]. A convex combination algorithm is -safe if

M i (t) + (1 -)m i (t) y i (t) (1 -)M i (t) + m i (t) (7)
where M i (t) = max Rcv i (t) and m i (t) = min Rcv i (t) .

Multidimensional Case

For the proof of Theorem 2 with higher dimensional values, we consider two agents i, j whose distance realizes diam(y(t)). From the ApproachExtreme y i (t) = m = (a + y i (t -1))/2 and y j (t) = m = (a + y j (t -1))/2 where a and a maximize the distance to y i (t -1) and y j (t -1), respectively, among the received values.

To show an upper bound on the distance d between the new agent positions m and m in the multidimensional case, we need the following variant of Lemma 4 in which we relax the upper bound on γ by a factor of two, but thereby weaken the bound on d .

Analogous to the proof of Theorem 1, the proof is by applying Lemma 5 to the three hatched triangles in Figure 1. The proof of the lemma is essentially the same as that of Lemma 4, with the following differences: Equation ( 6 We can hence apply Lemma 5 to obtain y i (t) -y j (t) 31 32 γ ij 31 32 diam y(t -1) .

Taking the maximum over all pairs of agents i and j now shows diam y(t) 31/32 • diam y(t -1) , which concludes the proof.

Conclusion

We presented two new algorithms for asymptotic and approximate consensus with values in arbitrary inner product spaces. This includes not only the Euclidean spaces R d , but also spaces of infinite dimension. Our algorithms are the first to have constant contraction rates, independent of the dimension and the number of agents.

We have presented our algorithms in the framework of non-split network models and have then shown how to apply them in several other distributed computing models. In particular, we improved the round complexity of the algorithms by Mendes et al. [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF] for asynchronous message passing with Byzantine faults from Ω d log d∆ ε to O log ∆ ε , eliminating all terms that depend on the dimension d.

The exact value of the optimal contraction rate for asymptotic and approximate consensus is known to be 1/2 in dimensions one and two [START_REF] Függer | Tight bounds for asymptotic and approximate consensus[END_REF][START_REF] Charron-Bost | Multidimensional asymptotic consensus in dynamic networks[END_REF], but the question is still open for higher dimensions. Our results are a step towards the solution of the problem as they show the optimum in all dimensions to lie between 1/2 and 7/8 ≈ 0.9354 . . .

Fast

  y i (t) -y j (t)Multidimensional Asymptotic and Approximate Consensus of the set of vectors of correct agents at the end of round t satisfies δ(t) 7 8 δ(t -1) .

Lemma 3 .Figure 1

 31 Figure 1 Tetrahedron formed by extreme points a and b of agent i and extreme points a and b of agent j. The distance between the new agent positions m and m is d .

Lemma 4 . 3 ) 4 a -b 2 . ( 4 )

 43424 Let a, b, a , b ∈ V and γ 0 such that diam {a, b, a , b } γ a -b + a -b . (Then, setting m = (a + b)/2 and m = (a + b )/2, we have Applying Lemma 3 with the points a, b, a yields m -a 2 γ 2 -1 Another invocation with the points a, b, b gives

  points a, b by agent i, we must have a -c a -b ; otherwise a, b would not realize the diameter of Rcv i (t). Analogously, by the choice of the extreme points a , b by agent j, it must hold that a -c a -b . From the triangular inequality, we then obtain a -a a -c + c -a a -b + a -b . Analogous arguments for the other pairs of points in {a, b, a , b } yield diam {a, b, a , b } = γ ij a -b + a -b .

Lemma 5 .

 5 Let a, b, a , b ∈ V and γ 0 such that diam {a, b, a , b } γ 2 a -b + 2 a -b . Then, setting m = (a + b)/2 and m = (a + b )/2, we have m -m 31 32 γ .

) is replaced by m -m 2 γ 2 - 1 4 a -b 2 + γ 2 -a -b 2 , 2 . 2 ,

 42222 which changes the function f to f (ξ) = γ 2 -1 4 ξ 2 + ( γ 2 -ξ)2 . The maximum of this function f is achieved for ξ = γ/4, which means thatm -m 2 f (γ/4) = γ 2 -We are now in the position to prove Theorem 2. multidimensional case. Let i and j be two agents. Let a = y i (t -1) and a = y j (t -1). Further, let b ∈ Rcv i (t) such that y i (t) = (a + b)/2 and b ∈ Rcv j (t) such that y j (t) = (a + b )/2. Define γ ij = diam {a, b, a , b } . Since a, b, a , b are the vectors of some agents in round t -1, we have γ ij diam y(t -1) .From the non-split property, there is an agent k whose vector c = y k (t -1) has been received by both i and j, i.e., c ∈ Rcv i (t) ∩ Rcv j (t). By the choice of the extreme point b by agent i, we must have a -c a -b ; otherwise b would not maximize the distance to a. Analogously, by the choice of the extreme points b by agent j, it must hold that a -c a -b . Note, however, that the roles of a and b are not symmetric and that, contrary to the proof of Theorem 1, we can haveb -c > a -b or b -c > a -b .From the triangular inequality and the two established inequalities, we then obtaina -a a -c + a -c a -b + a -b , a -b a -c + c -a + a -b a -b + 2 a -b ,and b -b b -a + a -c + c -a + a -b 2 a -b + 2 a -b . Analogously, a -b 2 a -b + a -b . Together this implies diam {a, b, a , b } = γ ij 2 a -b + 2 a -b .

Table 1

 1 Comparison of local time complexity and contraction rates in non-split network models. Entries marked with an * are new results in this paper.

		MidExtremes ApproachExtreme Centroid	MH	VG
	contraction rate	7 8	*	31 32	*	d d+1	d 1 2	1 -1 n
	local TIME	O(n 2 d)	O(nd)	#P-hard O(nd) O(nd)
	coordinate-free	yes	yes		yes	no	yes

2 0 1 8 27:8 Fast Multidimensional Asymptotic and Approximate Consensus Algorithm 1

  Asymptotic consensus algorithm MidExtremes for agent i

	Initialization:
	1: y i is the initial value in V
	In round t 1 do:
	2: broadcast y i
	3: Rcv i ← set of received values
	4: (a, b) ← arg max	a -b
	(a,b)∈Rcv 2 i

5:

Nicola Santoro and Peter Widmayer. Time is not a healer. In B. Monien and R. Cori, editors, 6th Symposium on Theoretical Aspects of Computer Science, volume 349 of LNCS, pages 304-313. Springer, Heidelberg, 1989.

Fred B Schneider. Understanding protocols for Byzantine clock synchronization. Technical report, Cornell University, 1987.

Jennifer Lundelius Welch and Nancy Lynch. A new fault-tolerant algorithm for clock synchronization. Information and computation, 77(1):1-36, 1988.

Funding This research was partially supported by the CNRS project PEPS DEMO and the Institut Farman.