Neeraj Kumar Singh
email: nsingh@enseeiht.fr

Akshay M Fajge

Raju Halder
email: halder@iitp.ac.in

Md Imran Alam

Formal Verification and Code Generation for Solidity Smart Contracts

Keywords: Formal methods, Refinement and Proofs, Blockchain, Smart Contracts, Solidity, Code generation, Event-B

Blockchain technology has gained widespread acceptance in industries such as e-commerce, energy trading, healthcare services, and asset management. Ethereum is an open-source blockchain computing platform with contract functionality. To manage digital assets, it executes bytecode on a simple Solidity stack machine, which is difficult due to Ethereum's openness that allows both programs and anonymous users to call into the public methods of other programs. In such cases, combining trusted and untrusted code for large applications can be risky and lead to catastrophic failure. For example, TheDAO is hacked by an attacker by examining EVM semantics to transfer 50 million USD in Ether. In this chapter, we outline a framework for analysing, verifying, and implementing smart contracts while maintaining functional correctness and required safety properties in Event-B using a correct by construction approach. The refinement approach is used to reduce the complexity of smart contract verification. The Rodin tool is used to develop formal models of smart contract specifications. Furthermore, the developed Event-B models are used to generate smart contracts in Solidity using our developed tool EB2Sol. For prototype development, the development architecture and code generation rules are described in detail. Finally, we demonstrate the scalability and effectiveness of our proposed framework through a case study.

Introduction

Ethereum [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger EIP-150 REVISION[END_REF] is an open-source computing platform, also known as the Ethereum Virtual Machine (EVM), for blockchain technology with contract functionality. The blockchain technology has been adopted successfully in different business sectors, such as e-commerce, banking, finance, insurance, energy trading, healthcare services, and asset management. Manipulation of critical transactions, as well as management of digital assets, making them attractive targets for security threats and attacks, which may result in financial losses and data leakage. EVM, on the other hand, executes bytecode of smart contracts written in Solidity [START_REF]Solidity Documentation[END_REF][START_REF]Solidity Github[END_REF], a JavaScript-like language, on a simple stack machine to handle and transfer digital assets, which is extremely difficult due to Ethereum's openness, allowing both programs and anonymous users to call into the public methods of other programs. In such cases, the use of trusted and untrusted code together in a large and complex application, particularly one involving financial management or privacy data, can be dangerous. For example, TheDAO is hacked by an attacker by examining EVM semantics to transfer 50 million USD in Ether [START_REF] Zhao | The DAO attack paradoxes in propositional logic[END_REF].

Since software plays an important role in the blockchain technology, we need effective ways to evaluate smart contracts in order to certify and ensure safe transactions. The blockchain community and industrial partners are looking for better technology and methods to provide safe and secure transactions. Furthermore, smart contracts must meet safety and security standards. We believe that formal methods have the potential to develop safe and secure systems that are also certifiable with required features that can be used to verify and certify smart contracts.

This chapter contributes a framework for analysing, verifying, and implementing smart contracts while maintaining functional correctness and required safety properties through incremental refinement in Event-B [START_REF]Modeling in Event-B: System and Software Engineering[END_REF]. We use the Rodin [START_REF]Rigorous Open Development Environment for Complex Systems[END_REF] tool to develop formal models of smart contract specifications. The primary use of this formal development is to assist in the construction, clarification, and validation of the smart contract requirements. Furthermore, the developed Event-B models are used to generate smart contracts in Solidity using our developed tool EB2Sol. This developed tool covers a subset of the Event-B modelling language in order to generate a Solidity subset. In this chapter, we will go over technical details about implementation as well as design decisions made during prototype development. Finally, we use a case study to demonstrate the scalability and effectiveness of our proposed framework.

In summary, the main contributions of this chapter are :

1. a framework for using formal methods to develop smart contracts from requirements analysis to code generation; 2. smart contracts (in Solidity) are generated from the proven Event-B formal models. 3. EB2Sol is developed to generate Solidity code. [START_REF] Zhao | The DAO attack paradoxes in propositional logic[END_REF]. the proposed framework is used for developing several case studies in order to formalise the development of smart contracts.

The rest of the chapter is as follows. Section 2 reviews related work. Section 3 briefly overviews key elements of Event-B modelling language, including refinement, and Solidity smart contract. A framework for developing formal Solidity smart contract in Event-B is presented in Section 4. Section 5 outlines the translation principle and development architecture of EB2Sol. Section 6 describes a case study to demonstrate the applicability of the proposed framework, including implementation of Solidity smart contract. In Section 7, we provide an assessment and Section 8 concludes the paper with future work.

Related work

Solidity smart contracts are widely used on the Ethereum platform for blockchain technology. Following several attacks [START_REF] Atzei | A survey of attacks on ethereum smart contracts sok[END_REF][START_REF] Zhao | The DAO attack paradoxes in propositional logic[END_REF] in recent years, formal methods are now regarded as first-class citizens for mitigating potential risks through formal reasoning on defined contracts. Several approaches based on formal methods for the development of smart contracts have been proposed in recent years.

Palina et al. [START_REF] Tolmach | A survey of smart contract formal specification and verification[END_REF] provided a comprehensive overview of formal models and smart contract specifications. They also highlighted some of the identified challenges and gaps in order to guide future research in the area of formal methods for developing trustworthy smart contracts.

In [START_REF] Hildenbrandt | Kevm: A complete formal semantics of the ethereum virtual machine[END_REF], the authors proposed EVM semantics in the K Framework based on the ERC20 Standard Token for formalising and analysing smart contracts. Hirai et al. [START_REF] Hirai | Defining the ethereum virtual machine for interactive theorem provers[END_REF] defined EVM in Lem language that can be translated into many standard interactive theorem provers. In particular, they prove interesting safety properties of Ethereum smart contracts in Isabelle/HOL. The ConCert framework [START_REF] Annenkov | Extracting smart contracts tested and verified in coq[END_REF] was developed for verifying smart contracts in Coq in order to detect vulnerability.

In [START_REF] Le | Proving conditional termination for smart contracts[END_REF], the authors proposed a lazy approach to determining input conditions under which the contract terminates or not by statically proving conditional termination and non-termination of a smart contract. This is accomplished by ensuring in advance that both the current state and the contract's input satisfy the termination conditions.

Wang et al. [START_REF] Lahiri | Formal specification and verification of smart contracts for azure blockchain[END_REF] presented VERISOL, a formal verification tool for smart contracts verification based on semantic conformance of smart contracts against a state machine model with access-control policy. They discovered some previously unknown bugs in the published smart contracts, then fixed the bugs and would be able to perform model checking-based verification with VERISOL. In [START_REF] Alt | Smt-based verification of solidity smart contracts[END_REF], the authors described an SMT-based formal verification module integrated with the Solidity compiler for identifying potential bugs during the compile time, such as arithmetic overflow/underflow, unreachable code, trivial conditions, and assertion fails.

In [START_REF] Bhargavan | Formal verification of smart contracts: Short paper[END_REF], the authors presented a framework for analysing and veryfing the runtime safety properties as well as functional correctness of Ethereum contracts using the F* functional programming language. In [START_REF] Grishchenko | A semantic framework for the security analysis of ethereum smart contracts[END_REF], the authors showed small-step semantics of EVM bytecode in F*. They validated the executable code against the Ethereum test suite. Furthermore, they identified some bugs and defined several security properties to prevent them, such as call integrity and atomicity. In a similar vein, [START_REF] Zhu | Formal Verification of Solidity contracts in Event-B[END_REF] presented a mechanism for translating Solidity contracts to Event-B models by defining transfer functions covering a subset of the Solidity language. Further, the produced Event-B model can be refined at different abstraction levels to verify properties associated with Solidity contracts using Rodin [START_REF]Rigorous Open Development Environment for Complex Systems[END_REF].

A structured approach to smart contracts verification based on refinement in the Event-B modelling language proposed in [START_REF] Banach | Verification-led smart contracts[END_REF]. Our work is also in this vein, as we propose a framework based on Event-B formal methods for specifying, analysing, verifying, and implementing smart contracts through refinement by preserving the required safety properties. In addition, we have developed a prototype tool, EB2Sol, to generate Solidity smart contracts from verified Event-B models. As far as we know, this is the first tool for translating Event-B models into Solidity smart contracts.

Background

Event-B Modelling Framework

This section summarises the core components of the Event-B modelling language [START_REF] Sala | Modeling in Event-B: System and Software Engineering[END_REF], including modelling concepts. The Event-B language has two main components, which are described in Table 1: context and machine. A context describes the static structure of a system, including carrier sets s and constants c, as well as axioms A(s, c) and theorems T c (s, c) that state their properties. A machine defines a system's dynamic structure, which includes variables v, invariants I(s, c, v), theorems T m (s, c, v), variants V (s, c, v), and events evt. Terms like refines, extends, and sees are used to describe the relation between components of Event-B models. In a machine, events are used to modify state variables by providing appropriate guards.

CONTEXT MACHINE ctxt id 2 machine id 2 EXTENDS REFINES ctxt id 1 machine id 1 SETS SEES s ctxt id 2 CONSTANTS VARIABLES c v AXIOMS INVARIANTS A(s, c) I(s, c, v) THEOREMS THEOREMS T c (s, c) T m (s, c, v) END VARIANT V (s, c, v) EVENTS Event evt any x where G(s, c, v, x) then v : |BA(e)(s, c, v, x, v ) end END Table 1: Model structure Theorems A(s, c) ⇒ T c (s, c) A(s, c) ∧ I(s, c, v) ⇒ T m (s, c, v) Invariant A(s, c) ∧ I(s, c, v) ∧ G(s, c, v, x) ∧ BAP (s, c, v, x, v ) preservation ⇒ I(s, c, v ) Event A(s, c) ∧ I(s, c, v) ∧ G(s, c, v, x) feasibility ⇒ ∃v .BAP (s, c, v, x, v ) Variant A(s, c) ∧ I(s, c, v) ∧ G(s, c, v, x) ∧ BAP (s, c, v, x, v ) progress ⇒ V (s, c, v ) < V (s, c, v)
Table 2: Some of the associated proof obligations

Modelling Actions over States

An Event-B model is characterised by a set of state variables that can be modified by a set of events. An invariant I(s, c, v) expresses the required safety properties that the variable v must satisfy during event activation. An event is a state transition in a dynamic system that contains guard(s) and action(s). A guard, predicate based on state variables, is required for an event to be enabled. A action, also known as a before-after predicate, is a generalised substitution that describes how the occurrence of an event changes one or more state variables. An event evt can be defined in three ways: the first is BEGIN v : |BAP (s, c, v, v ) END, in which the action, BAP (s, c, v, v ), is not guarded and is always enabled; the second is WHEN G(s, c, v) THEN v : |BAP (s, c, v, v )) END, in which the action, BAP (s, c, v, v ), is guarded by G(s, c, v), and the guard must be satisfied to enable the action; and the final is ANY x WHERE G(s, c, v, x) THEN v : |BAP (s, c, v, x, v ) END, where the action, BAP (s, c, v, x, v ), is guarded by G(s, c, v, x) and depends on the local state variable x to describe non-deterministic events.

The Rodin platform generates proof obligations (POs) [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF]. Event-B supports a variety of POs (see Table 2), such as invariant preservation, non-deterministic action feasibility, variant, welldefinedness, and so on. Invariant preservation ensures that each invariant is preserved by each event; non-deterministic action feasibility shows the feasibility of the event e with respect to the invariant I; variant ensures that each convergent event decreases the proposed numeric variant; and well-definedness ensures that each axiom, theorem, invariant, guard, action, and variant is well-defined.

Refinement

To model a complex system, the Event-B modelling language supports a stepwise refinement technique. The refinements allow us to gradually model a system and provide a way to strengthen invariants, introducing more detailed system behaviour. By modifying the state description, this refinement method converts an abstract model into a more concrete version. The refinement process adds new events to a list of state variables by refining each abstract event to a concrete version, or by simply refining each abstract event to a concrete version. These refinements preserve the relationship between an abstract model and its concrete model while introducing new events and variables to specify more concrete system behaviour. Gluing invariants connect the abstract and concrete state variables. Each abstract event is correctly refined by its concrete version, thanks to the generated POs. Table 3 shows some of the important POs associated to refinement, such as event simulation, guard strengthening and invariant preservation. The simulation ensures that each action in a concrete event simulates the corresponding abstract action; the guard strengthening in a refinement ensures that the concrete guards in the refining event are stronger than the abstract ones; and the invariant preservation ensures that each invariant is preserved by each refined event. These POs contain axiom A(s, c) invariant I(s, c, v), gluing invariant J(s, c, v, w), guard H(s, c, y, w), witness W (s, c, x, w, y, w ) and before-after predicate BAP (s, c, w, y, w ).

A set of new events introduced in a refinement step is referred to as hidden events because they are not visible to the environment of the system being modelled. These introduced events are beyond the environment's control. Skip is refined by new events that are not visible in the abstract model. Any number of executions of an internal action may occur between each execution of a visible action. By strengthening the guards and/or predicates, the refined model reduces the degree Event A(s, c) ∧ I(s, c, v) ∧ ∧J(s, c, v, w) ∧ H(s, c, y, w) ∧ W (s, c, x, w, y, w ) simulation ∧BAP (s, c, w, y, w ) ⇒ BAP (s, c, v, x, v ) Guard A(s, c) ∧ I(s, c, v) ∧ J(s, c, v, w) ∧ H(s, c, y, w) ∧ W (s, c, x, w, y) strengthing ⇒G(s, c, v, x) Invariant A(s, c) ∧ I(s, c, v) ∧ J(s, c, v, w) ∧ H(s, c, y, w) ∧ W (s, c, y, w, v , w )∧ preservation BAP (s, c, w, y, w ) ⇒ I(s, c, v , w ) Table 3: Refinement POs of nondeterminism. The refinement of an event e by an event f implies that the event f simulates the event e, ensuring that the set of traces of the refined model includes (up to stuttering) the traces of the resulting model.

Rodin

Rodin [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] is an open source Eclipse-based integrated development environment (IDE) for developing Event-B models. Rodin is a foundational collection of plug-ins for project management, formal development, syntactic analysis, proof assistance, and proof-based verification. Furthermore, it supports extension points for a variety of additional plugins that provide various functionalities and features related to model checking, animation, code generation, additional proof capabilities using SMTs and external theorem provers (i.e., Why3, Isabelle), UML-B, Theory plug-ins, composition and decomposition, refactoring framework, and model editors.

Applications

The Event-B method has been used successfully to design critical systems for a variety of applications, including the control system for the Meteor line 14 in Paris and the VAL shuttle for Paris CDG airport [START_REF] Behm | Météor: A Successful Application of B in a Large Project[END_REF][START_REF] Badeau | Using B as a High Level Programming Language in an Industrial Project: Roissy VAL[END_REF][START_REF] Essamé | B in Large-Scale Projects: The Canarsie Line CBTC Experience[END_REF], as well as medical devices [START_REF] Singh | Using Event-B for Critical Device Software Systems[END_REF][START_REF] Singh | Stepwise formal modelling and reasoning of insulin infusion pump requirements[END_REF][START_REF] Banach | Hemodialysis Machine in Hybrid Event-B[END_REF], autonomous systems [START_REF] Singh | Stepwise Formal Modeling and Verification of Self-Adaptive Systems with Event-B. The Automatic Rover Protection Case Study[END_REF][START_REF] Su | Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System[END_REF], security protocols [START_REF] Benaissa | Cryptographic protocols analysis in event b[END_REF][START_REF] Laibinis | A formal approach to identifying security vulnerabilities in telecommunication networks[END_REF], control-command systems [START_REF] Dupont | Event-B Hybridation: A Proof and Refinement-based Framework for Modelling Hybrid Systems[END_REF][START_REF] Banach | Core Hybrid Event-B I: Single Hybrid Event-B machines[END_REF][START_REF] Dupont | Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B[END_REF], and distributed protocols [START_REF] Stankaitis | A refinement based method for developing distributed protocols[END_REF][START_REF] Méry | Analysis of DSR Protocol in Event-B[END_REF][START_REF] Andriamiarina | Integrating proved state-based models for constructing correct distributed algorithms[END_REF][START_REF] Zoubeyr | A correct-by-construction model for asynchronously communicating systems[END_REF][START_REF] Benyagoub | Formal design of scalable conversation protocols using Event-B: Validation, experiments, and benchmarks[END_REF]. More information can be found in [START_REF] Butler | The first twenty-five years of industrial use of the b-method[END_REF].

Solidity

Solidity is a programming language designed specifically for developing smart contracts that compiled into byte-code executable by Ethereum platform's execution engine, often known as Ethereum Virtual Machine (EVM). Smart Contracts are programs that execute on a decentralized network without the intervention of a central authority. Solidity enables developers to create selfenforcing business logic via smart contracts, resulting in a trustworthy and authoritative record of transactions. The syntax of Solidity is quite similar to those of scripting languages like JavaScript, and it is heavily influenced by C++, Python. Solidity extensively utilizes programming techniques derived from other languages. It features variables, static typing, functions, libraries, and interfaces. In addition, it offers a range of control structures such as for, while, do-while, and if-else. In case of an object-oriented programming language like Java, programmers work with classes, whereas Solidity programmers deals with contracts. Each contract can define various Solidity constructs such as state variables, functions, function modifiers, events, errors, structure types, and enum types. This subsection outlines the major Solidity constructs that are relevant to our goal. More information about Solidity programming language can be found in [START_REF]Solidity Documentation[END_REF].

Solidity Types, Special Functions and Variables

Solidity is a statically typed programming language, which means that variable types are declared explicitly and thus determined at compile time. In Solidity, numerous elementary types exist that can be combined to form more sophisticated types. Solidity offers an extensive range of types, notably value types, reference types such as arrays and structures, mapping types, userdefined types and it also supports elementary type conversion. Solidity does not support undefined or null values, newly declared variables always have a default value based on their type. Table 4 summarises the most frequently used value types. In the global namespace, special variables and functions exist at all times and are primarily used to relay information about the blockchain or to perform general-purpose utility operations. Table 5 lists some of the most frequently used variables and functions from the global namespace of Solidity. Additionally, solidity supports various denomination of Ethereum cryptocurrency such as wei, gwei, and ether, as a suffix to number literals. Errors are handled in Solidity using state-reverting exceptions. This exception nullifies any state changes made during the execution of the code and notifies the caller of an error. The assert and require functions enable programmers to check for conditions and throw exceptions if they are not met. The assert function should be preferred exclusively to check for internal errors and invariants. The require function supports optional error message and should be used to ensure the existence of valid conditions that must be identified during contract execution. This includes conditions on input values or the return values of external contract calls. The revert function is another mechanism available in the global namespace for reporting errors and undoing state changes during contract code execution. Additionally, this function accepts and returns an optional message containing details about the error to the caller.

Function Modifiers

Modifiers in Solidity are analogous to the Object-Oriented Programming decorator patterns. A modifier controls how a function behaves at run-time. In the example provided in Code Snippet 1, the modifier validate(int) restricts the execution of the increment function if the parameter value of increment function is less than one. Multiple modifiers can be applied to a function or constructor by specifying them in a whitespaceseparated list and are evaluated from left to right. Modifiers are inheritable properties of contracts and may be overridden by derived contracts. The symbol ; in modifier body returns the flow of execution to the original function code. It applies to various contexts, such as providing an easyto-understand approach to express certain guards, confirming specific conditions after the function execution.

Formal framework for Solidity smart contracts

Fig. 1 depicts a modelling framework for formalising and implementing Solidity smart contracts that support the correct by construction approach. In this proposed framework, there are three main important process blocks: (1) Event-B model, (2) formal verification, and (3) Solidity implementation. The Event-B model block deals with complex modelling of smart contracts, and building a formal model of smart contracts may require several iterations. Starting from an initial model, it is gradually enhanced by adding design decisions and handling requirements. Note that the progressive safe enrichment allows to add the required safety properties and low level system requirements related to smart contracts. These refinements preserve the relationships between an abstract model and its corresponding concrete model while introducing low-level details and new properties to specify more concrete behaviour of a system. This incremental development ensures the correctness of concrete behaviour of a smart contract system in relation to the abstract model. Rodin tools are used to verify the abstract and refined Event-B models. The analysed models provide feedback to the original Event-B model, which is depicted in Fig. 1.

The second block of Fig. 1 is concerned with formal verification, which is an important step in proving and disproving the correctness of a formalized system's intended behavior under the given safety properties and assumptions. In the process of system verification, we can use an automated theorem prover to check the consistency and correctness of the generated formal model. Using mathematical operators, a formal notation can be analyzed and manipulated, and mathematical proof procedures can be used to test (and prove) the internal consistency (including data conservation) and syntactical correctness of the specifications. The formal verification ensures that the model is correctly designed, that the developed formal specification has the required properties, and that the generated models are free of errors, oversights, and bugs. The Rodin development framework can be used for project management as well as model verification via syntactical and refinement checking. Furthermore, this tool can be used to discharge the generated proof obligations. If any inconsistencies in the model are discovered during the system verification process, we can modify the model obtained in the previous step of the development process. We can iterate until we get a correct model.

The final block in our framework is related to Solidity implementation using our developed tool EB2Sol. This is the last stage of our framework proposal. From the formalised, proved, and validated formal models, it generates Solidity language code for system implementation. This phase of development includes the major executable components, concrete data structure definitions, and some auxiliary structures or functions that may be assumed in a design. However, it is also critical to rigorously review the system implementation in relation to the specified system requirements and selected design. Automatic code generation has become standard practice in developing verified code in a target language corresponding to the given specification, required configurations, and platform information without any human intervention in the new age of software development and automation of the development life-cycle.

In our proposed framework, we use our developed tool EB2Sol, an extension of EB2ALL [START_REF] Méry | Automatic code generation from Event-B models[END_REF][START_REF] Eb2all | An automatic code generation tool from Event-B[END_REF], to generate source code in Soldity language from the verified formal specification. Section 5 describes the basic architecture of this tool as well as the development process. This automation process has several advantages. For example, the automatic code generation tool produces executable software with far fewer implementation errors than a human programmer. Manually implementing the formal specification can be time-consuming and error-prone. In automatic code generation, code maintenance and successive changes are simple to handle, and the consistency between the generated code and the given formal specification is always maintained. However, there are some drawbacks to automatic code generation. For example, automatically generated codes can be difficult to understand, excessive code can be generated, and incorrect code is still a possibility.

EB2Sol: Event-B to Solidity

In this section, we describe the development architecture for our developed tool EB2Sol, which is an extension of EB2ALL [START_REF] Eb2all | An automatic code generation tool from Event-B[END_REF], developed as a new plugin for generating Solidity smart contracts from Event-B models. Fig. 2 depicts the overall architecture of the EB2Sol automatic code generation tool. The given boxes show different steps of the code generation process. The first block is associated with the Event-B model, which serves as an input to the code generation tool.

Preprocessing and generated POs

Most of the time, systems fail due to a run-time error. Overflow and underflow of bounded integers, for example, are types of run-time errors that should be checked before producing the Solidity code. There is a pre-processing step in the code generation process that allows for the introduction of a context file based on the Solidity language to provide a deterministic range for data types in order to make the Event-B model deterministic [START_REF] Sites | Clean Termination of Computer Programs[END_REF]. To obtain the deterministic model, we can use vertical refinement to refine the previous concrete model, which provides deterministic definitions of constants and variables. For this, we can introduce a Solidity context file which contains bounded integer data types. Table 6 shows a map between Event-B and Solidity types for signed and unsigned integers. Note that the Solidity context file is an Event-B context file, which is required to generate correct code. Adding a new context file may generate new set of POs that must be proved before generating the Solidity code as well as to verify the specification in order to ensure the system's consistency.

Translation of Event-B to Solidity

The main objective is to translate the Event-B model into a semantically observationally equivalent standard Solidity smart contracts. The developed translator is based on a set of transformation rules that map between the Event-B and Solidity constructs. In fact, the transformation functions allow to produce code in target language applying a set of rules when matching the inputs from the source language. We define a set of transformation functions to generate Solidity code from the Event-B model. These transformation rules are given in Table 7. All constants defined in a model's context must be replaced with their literal values. We consider Event-B formal notations available at [START_REF]Modeling in Event-B: System and Software Engineering[END_REF] and capture the Event-B grammar in a Abstract Syntax Tree (AST). This translation tool accepts conditional, arithmetic, and logical formal model expressions. Event-B model that contains machines and contexts are translated to Solidity contracts. Below we provide the translation process for dealing with context and machine models.

Event

Context models

The context of an Event-B model consists of sets, enumerated sets, constants, arrays and functions, all of which are associated with their respective type. For translation purposes, the translation tool supports all types of context components. The observational equivalence is based on the equivalence of Event-B values and the values of Solidity smart contracts. This equivalence on values is naturally extended to context instances. In Table - Constants, sets and enumerated sets of the Event-B model are translated into constants, type declaration and enumerated sets of the Solidity contracts using the translation function T decl and T axm . An Event-B enumerated sets are semantically equivalent to Solidity contracts enumerated types, thus it is simple to translate.

For the efficiency of the generated code and the correctness of the translation, the link between Event-B and Solidity contracts for integer values have been regarded significant. We recommend to use preprocessing step by introducing Solidity context file. Similarly, the Event-B constant are also directly translatable due to direct typing correspondence between Event-B integer types and Solidity language integer types. For example, if Event-B use a data type given in Table 6.

The translation for the declaration of Event-B array type and the Solidity array type is not straightforward. In Event-B, an array can be defined as a total function, whereas in Solidity, they relate to a contiguous memory zone (coded as the beginning address of the array and its size). The semantical correspondence between an array element arr(i) in Event-B and the value at the position arr[i] in Solidity, can be easily translate.

The translation for the Event-B function into Solidity function is also very complex. Only the Event-B total function is supported by the current prototype tool. Solidity function input and output arguments can be easily identified by looking at the left and right sides of the total function symbol (→) in the Event-B function specification. The Event-B function definition can be translated in a Solidity function structure.

The context model elements are declared global in the generated code. The type information for context elements is derived from the context axioms used for type definition, such as it can be used to express as integer ranges, specifically supported bit-map types, or arrays of the defined mapping functions.

Machine models

A machine model consists of variables, invariants, events. The Event-B variables can be used to generate Solidity attributes, and the Event-B invariants can be used to extract typing information. All the generated variables or attributes have default property public. Note that the Event-B machine may also contain function and array declaration that can also translate similarly to translation rule for function and array given in context model. The required typing information can be extracted from the Event-B invariants.

There are two types of variables in the Event-B specification: global variables and local variables. Global variables are produced directly from the variable declarations, and all of these variables have global scope. Local variables are derived from any clause of an event and are completely local to the corresponding event. All local variable declarations are placed as a list of input arguments of the function when the function structure is generated.

The translation tool uses a recursive method to generate Solidity contracts for each event of the Event-B specification. The translation tool always checks for the 'null' event (i.e. the guard of a false condition), never generates the source code for such event, and inserts a relevant note into the generated code for traceability. For example, if an event has a single guard with a f alse condition, the Solidity code does not produce for that event. This automatic reduction occurs to avoid the production of inaccessible run-time code.

The initialization event of Event-B machine is translated as a constructor, and all variables are initialized with default values in the constructor body which are directly derived from the action predicates of the Event-B initialization event.

Guard handling in Event-B is extremely ambiguous due to different meanings, such as local variable type definition, assignment of a value to a local variable, condition statements using negation (¬), conjunction (∧), disjunction (∨), implication (⇒), and equivalence (⇔) operators. We build a recursive technique for parsing and identifying different elements of the Event-B guard for translation purposes. For example, an implication (⇒) and equivalence (⇔) operator, the translator tool automatically rewrites the predicate in an equivalent form using conjunction (land), disjunction (∨), and negation (¬) operators, an equal relation may signify an assignment or equality comparison, and the precise meaning (and thus the resulting translation) deduced from the type and scope of implication (⇒).

Another interesting point to discuss is the definition of a functional-image relation, which can be used to represent a data array or an external function. Once the guards of an event have been classified, the guards that confer local variable type information are utilized to generate variable declarations in the function, while the remaining guards are used to generate local assignment and conditional statements. In addition, local variable type information is derived in the same way as global variables from guard information.

Event-B events are translated into functions, and event parameters are passed as function and modifier arguments. In order to effectively call each function, modifiers are added to each generated function. These associated modifiers are also defined as a function using required/assert statements derived from Event-B guard predicates.

Actions are triggered concurrently in Event-B, and any state modification in the actions is only valid in the whole event post-condition. As a result, dependency checks must be conducted to guarantee that no state variable used as an action assignee has been updated to its post-condition before to usage. As a guard statement, a similar kind of parsing is used on the Event-B action statement. At last, the event actions are directly translated in the form of assignment statements in the function body. Assignments to scalar variables, override statements acting on array-type variables, and arithmetic complicated expressions are all supported through an action translation.

Case Study

To assess the proposed methodology and developed tool EB2Sol, we use several small and large examples. For example, we developed the formal specification of arithmetic operations (increment and decrement), cardiac pacemaker and smart purchase. In this section, we apply our proposed methodology for developing smart purchase case study, and discuss its formal development, including code generation in Solidity.

Informal description of smart purchase

Purchasing goods over the internet necessitates the trust of several parties. A basic example with seller and buyer is available in [START_REF]Solidity Documentation[END_REF]. However, it becomes more complicated when a courier is included in the system, as it is challenging to detect an item's delivery to its intended recipient. Fig. 3 illustrates a process of purchasing goods. In this example, we have included a seller, courier, and buyer with the ability to return the product within a return window. The seller can execute actions such as listing an item for sale, revoking it, processing an order, and initiating settlement. On the other hand, the buyer can purchase the item, confirm delivery, and request a return. Services like pickup and pickup return are available for a courier.

Formal Development

For developing a formal model of the smart purchase, we develop a context model to express static behaviour, properties of the system, while the dynamic behaviour and properties are modelled in a machine model. Below we describe both the context and machine models.

Context model

In the context model of smart purchase, we declare a set ADDRESS to represent address type that is unique in Solidity contracts. An enumerated set P roductState is defined to encode all possible states of different processes in axm1. A new constant timeInSec is defined in axm2 to represent time duration. The next two axioms (axm3 and axm4) are used to define balance and now constants to represent initial balance and time value. The last axiom defines a constant this as an address type to indicate one's own address.

axm1 : partition(P roductState, {InStock}, {Booked}, {P acked}, {T ransite}, {ReturnReq}, {ReturnAck}, {Delivered}, {Closed}) axm2 : timeInSec ∈ N axm3 : balance ∈ N 1 axm4 : now ∈ N axm5 : this ∈ ADDRESS

Machine model

A machine model is developed to specify the dynamic behaviour of smart purchase including all possible operations. In this model, we introduce 8 state variables (inv1-inv8). A variable address list is defined to record all the addresses who call the smart purchase contract. The next three variables seller, buyer and courier are defined as address types belonging to address list. A transfer function is defined in inv5. The variable state represents possible product states when purchasing goods. The next variable price is used to define the product's cost and the last variable returnW indow is used to define product's return time duration. Other events are: initiateSellerto initiate seller of contract; revoketo revoke the product and reclaim the deposited ethers; conf irmP urchaseto confirm the purchase; processOrderto be called by the seller after the product has been booked; pickupto be called by the courier at the time of pickup; conf irmDeliveryto confirm delivery of the item; initiateReturnto initiate the process of product return; pickupReturnedP roductto pay the product price to the seller; F nF Settlement -Af terDeliveryto confirm the buyer's full and final settlement for the purchased item; F nF SettlementAf terReturnAcceptedto confirm full and final settlement for the purchased item when the buyer returns the purchased item; and new accountto add a new address that invokes the smart purchase contract.

In the event initiateSeller, we define three parameters and five guards. The first two guards define the local parameters msg value and msg sender. The following guard defines value and ensures that it equals msg value/3. The grd4 states that msg value is three times value, and the last guard states that seller is not equal to msg sender. These guards keep the required condition for initiating seller. In this event, two new actions are introduced, and these actions are used to initiate the seller and price variables based on the selected address msg sender and msg value, respectively.

EVENT initiateSeller ANY value, msg value, msg sender WHERE grd1: msg value ∈ N 1 grd2: msg sender ∈ address list \ {this} grd3: value ∈ N ∧ value = msg value/3 grd4: msg value = 3 * value grd5: seller = msg sender THEN act1: seller := msg sender act2: price := msg value/3 END Similarly, another event conf irmP urchase is defined to confirm the purchase, which can only be called by the buyer if the product is in stock. In this event, we define two parameters and four guards. The first two guards define the local parameters msg value and msg sender. The next guard (grd3) states that the state is InStock. The last guard shows that the msg value is three times the price. These guards keep the required condition for confirming purchase. Two new actions are introduced in this event, and these actions are used to set the state as Booked and the buyer is updated by msg sender. Other remaining events are formalised in a similar way. A complete formal development of the smart purchase case study is available at1 .

Model validation and analysis

Formal modelling and verification are carried out using the open source integrated development framework Rodin. In this section, we summarise the generated proof obligations generated by the Rodin prover. The generated proof obligations are related to well-definedness, feasibility and invariant. The generated proof obligations ensure consistency checking and it guarantees that the modelled events always preserve the given invariants. The formal development of smart purchase is presented in a single machine, but it can be developed incrementally through an abstract model and a series of refinement models. This development results in 22 proof obligations (POs), in which 19 (87%) are automatically proved and the remaining 3 (13%) are proved interactively using the Rodin prover and other associated tools, such as SMT solvers (CVC4, Z3, and veriT). By achieving the required functional behavior for the smart purchase model, we have successfully discharged all of the generated proof obligations that ensure consistency checking.

The model analysis is carried out with the help of the ProB [START_REF] Leuschel | ProB: A Model Checker for B[END_REF] model checker, which can be used to explore traces of Event-B models. The ProB tool can detect potential deadlocks and supports automated consistency checking and constraint-based checking. In this work, we use the ProB tool as a model checker to show the absence of errors (no counterexample exists) and the absence of deadlock. It is worth noting that the ProB employs all of the described safety properties during the model checking process in order to report any violations of safety properties against the formalized system behavior. We also use the ProB tool for animating the models to validate the developed smart purchase model. This validation approach entails gaining confidence that the developed models are in accordance with the requirements.

Code Generation in Solidity

In this section, we will use our developed tool EB2Sol to generate Solidity smart contracts from the formal Event-B model of smart purchase. EB2Sol is an Eclipse-based plug-in for code generation in the Solidity language for the Rodin platform. A detailed description of the automatic code generation is given in section 5.

A screen shot of the EB2Sol in the Rodin environment is shown in Fig. 4. After installing this plug-in successfully, the menu Translator/EB2Sol and a tool button on the toolbar will appear. To generate Solidity source code for any formal model, a user can select it from the EB2Sol menu or tool button, and a dialog box will appear. This dialog box displays a list of currently active projects. Any project can be chosen by the user to generate Solidity contracts, including a log file containing information about the code generation process. In our case study, we generate Solidity source code from the proven smart purchase model using the EB2Sol plug-in. Before using this tool, we refine our concrete model by introducing a new context containing Solidity type definitions (see Table 6) and removing the abstract operations and non-supported symbols via data refinement. By defining some glueing invariants, this refinement makes the smart purchase model deterministic. All new generated POs must be discharged before generating smart contracts.

Smart contract generation from an Event-B model is straightforward. The EB2Sol tool generates Solidity smart contract files from the concrete model. Constants, type definitions, variables, modifiers, and functions are all included in the generated smart contracts that are extracted from the smart purchase model. The translated constants, type definitions, and variables are taken from the generated code shown in code snippet 2. The formalised smart purchase model yields a set of functions. These functions are generated from events by analyzing various elements such as local parameters, guards, and actions. Event-B events are converted into functions, and event parameters are used as function arguments. Modifiers are added to each generated function in order to effectively call it. These associated modifiers are defined as a function as well, using required/assert statements derived from Event-B guard predicates.

The event actions are directly translated equivalent to Solidity assignment expressions. To execute a set of actions in any function, all of the given modifiers must be TRUE. If the given modifiers do not satisfy, the function body statements are skipped. The only excerpt from the generated code equivalent to the given events is given in code snippet 3.

Discussion

This chapter has presented a framework for analysing, verifying and implementing the Solidity smart contracts based on formal methods. Furthermore, the case study that we have presented demonstrated the viability of our framework. This section discusses the main benefits and limitations of our approach.

Benefits

Our proposed framework has the potential to improve blockchain system safety and quality, including assisting in the system certification process for developing smart Solidity contracts. To support the proposed framework, we use the Event-B modelling language to specify smart contracts requirements. The main advantages of this approach are that it improves the process of abstractly specifying smart contract requirements, formal development using correct by construction, and detecting potential flaws through rigorous analysis. This may enable us to analyse and validate the important properties of consistency, deadlock-freedom and safety of complex transections. The main advantages of our approach are described in the following section.

Progressive development of smart contracts

For a long time, stepwise refinement has been used to model complex systems. Our proposed framework adopted the key concepts of refinement for designing complex smart contracts. This gradual development enables us to introduce concrete details and the required safety properties associated with blockchain technology. The use of refinement reduces the complexities of design and proof efforts by increasing proof automation.

Improving smart contract error detection

Our proposed framework included modelling and verification approaches for rigorous analysis to ensure the functional behaviour of the designed smart contracts, as well as their refinement steps. We can detect inconsistencies in the given requirements and refinement relations using formal verification, where we must discharge all generated proof obligations. In addition, we may use the ProB model checker to validate the modelled contracts and ensure the absence of any counter examples.

Minimising smart contract development cost

Errors are always less expensive to identify earlier in the development phase. Our framework enables to analyse complex operations in order to define smart contracts. The use of formal reasoning in the design of complex smart contacts always results in a lower overall cost. Moreover, the use of design patterns and refinement can be applied to the development of other similar smart contracts.

Limitations

The proposed framework consists of formal modelling, verification and implementation. We used the Event-B modelling language for modelling, Rodin tools for verification, and EB2Sol for generating Solidity smart contacts. Here, we will go over some of the limitations of our approach and the tools we have chosen.

Need careful analysis in modelling and implementation

We have used Rodin tools for verification and EB2Sol code generation in our work. In fact, we must ensure the consistency of the designed smart contracts as well as the generation of the Solidity smart contracts, as we use Solidity context file to derive a deterministic model manually. All newly generated POs must be discharged before code generation. Currently, a user may need to provide a Solidity context file and refined the model, including proof process, but this can be automated in the future.

Need powerful theorem provers for smart contracts

In the current work, we discharged the generated POs using Rodin-supported proof tools. Most proofs can be discharged automatically, but human interaction is inevitable when proofs are complex. We need powerful theorem provers to automate the proof process when dealing with complex and large smart contract requirements.

No standard in the generated smart contracts

The Solidity smart contracts must be expressive and optimised in order to use the least amount of gas. Currently, the prototype tool EB2Sol does not take into account the required standard for producing Solidity smart contracts. We need to improve our developed tool so that it can meet the required standard for reducing gas consumption. Otherwise, Solidity smart contracts can be generated manually from the last deterministic model in accordance with the preferred standards.

Conclusion

In this chapter, we presented a framework for analysing, verifying and implementing Solidity smart contracts using the correct by construction approach in Event-B. The framework relies on incremental development, which allows for the abstract modelling of Solidity contracts and then further it can be refined to introduce concrete details, including the required safety and security properties. The refinement enables for the gradual modelling of complex transaction scenarios, and the required properties can be added in a step-by-step approach.

For the implementation of Solidity smart contracts, we developed the prototype tool EB2Sol, which generates source code automatically from verified and proven Event-B models. EB2Sol is a new plugin for the Rodin platform for generating Solidity contracts. Development architecture and a set of transformation functions are defined. The translation tool has been meticulously developed with safety properties preservation. The results detailed in this chapte are an architecture of the translation process, to generate Solidity code from Event-B models following syntax directed translations. Despite its limited syntax, it already covers the most of numerical applications and supports powerful static-analysis methods. The current prototype tool has covered a subset of the Event-B modelling language in order to generate Solidity subset.

We used a case study to better demonstrate the practicability of our proposed framework from abstract modelling to implementation. The selected case study is successfully developed and proven in the Rodin platform, and finally Solidity smart contracts are produced using our tool EB2Sol.

Our current approach is based on first-order logic and refinement in order to develop a safe and secure Solidity contracts that allow us to verify complex properties. Our developed tool currently supports a subset of the Event-B modelling language. Due to the richness of the Event-B modelling language, we intend to extend the current subset of Event-B modelling language for EB2Sol in order to provide modeling and reasoning flexility as well as the ability to generate Solidity contracts from any refinement level. Furthermore, we intend to expand our EB2Sol tool to cover the remaining Solidity language constructs. Another important future task will be to validate the defined translation principals for EB2Sol. We plan to develop a meta model in HOL to check the correctness of translation rules. It may aid to certify the generated Solidity smart contracts.

  pragma solidity >=0.6.0; contract ModifierExample { int public number; modifier validate(int value){ require(value>0, "value of incrementBy must be greater than 0"); _; } function increment(int incrementBy) validate(incrementBy) public{ number += incrementBy; } } Code Snippet 1: Modifier Example

Figure 1 :

 1 Figure 1: A framework for developing formal Solidity smart contracts.

Figure 2 :

 2 Figure 2: Development architecture of EB2Sol

T

  decl : Datatype and Constant declaration translation function T st : State variables translation function T axm : Axioms translation function T pred : Predicate translation function T thm : Theorem translation function T evt : Events translation function T grd : Event's guards translation function T act : Event's actions translation function T exp : Expressions translation function

Figure 3 :

 3 Figure 3: Smart Purchase Example

inv1:

  address list ⊆ ADDRESS inv2 : seller ∈ address list inv3 : buyer ∈ address list inv4 : courier ∈ address list inv5 : transf er ∈ ADDRESS → N inv6 : state ∈ P roductState inv7 : price ∈ N inv8 : returnW indow ∈ N In this machine, we introduce 12 events, including INITIALISATION event. The INITIALI-SATION event is used to set the initial value for each declared variable. EVENT INITIALISATION BEGIN act1: address list := {this} act2: seller := this act3: buyer := this act4: courier := this act5: transf er := ∅ act6: state := InStock act7: price := 0 act8: returnW indow := timeInSec END

  EVENT confirmPurchase ANY msg value, msg sender WHERE grd1: msg value ∈ N 1 grd2: msg sender ∈ address list \ {this} grd3: state = InStock grd4: msg value = 3 * price THEN act1: state := Booked act2: buyer := msg sender END

Figure 4 :

 4 Figure 4: EB2Sol plug-in in the Rodin IDE

3 :

 3 uint256 value = msg.value/3; require((msg.value==3 * value)&&(seller!=msg.sender)); Generated modifiers and functions

Table 4 :

 4 Solidity Value Types

Table 5 :

 5 Frequently Used Special Variables and Functions

Table 6 :

 6 Signed and Unsigned Integers

	Event-B type Formal Range	Solidity type
	tl int8	-2 7 ..2 7 -1	int8
	tl int16	-2 15 ..2 15 -1	int16
	tl int24	-2 23 ..2 23 -1	int24
	. . .	. . .	. . .
	tl int256	-2 255 ..2 255 -1	int256
	tl uint8	0..2 8 -1	uint8
	tl uint16	0..2 16 -1	uint16
	tl uint24	0..2 24 -1	uint24
	. . .	. . .	. . .
	tl int256	0..2 256 -1	uint256

Table 7 :

 7 Transformation function A set of supported symbols of EB2Sol tool is given in Table-8. This table shows a subset of Event-B syntax to equivalent Solidity smart contracts.

Table 8 :

 8 Event-B to Solidity

	-B	Solidity	Comment
	const x ∈ N ∧ cons x=120	int256 constant const x = 120	Constant declaration
	x ∈ Z	int256 x	Signed integer variable declaration
	x ∈ N	uint256 x	Unsigned integer variable declaration
	x ∈ tl int16	int16 x;	Signed integer variable declaration
	b ∈ BOOL	bool b;	Boolean variable declaration
	x ∈ n..m → Z	int [m+1] x;	Array declaration
	x = y	if(x==y) { . . . }	Conditional statement
	x = y	if(x!=y) { . . . }	Conditional statement
	x < y	if(x<y) { . . . }	Conditional statement
	x ≤ y	if(x<=y) { . . . }	Conditional statement
	x > y	if(x>y) { . . . }	Conditional statement
	x ≥ y	if(x>=y) { . . . }	Conditional statement
	(x>y) ∧ (x≥z)	if ((x>y) && (x>=z) { . . . }	Conditional statement
	(x>y) ∨ (x≥z)	if ((x>y) (x>=z) { . . . }	Conditional statement
	¬x<y	if(!(x<y)){ . . . }	Logical not
	X⇒Y	if(!X Y){ . . . }	Logical Implication
	X⇔Y	if((!X Y) && (!Y X)){ . . . }	Logical Equivalence
	x := y + z	x = y + z;	Arithmetic assignment
	x := y -z	x = y -z;	Arithmetic assignment
	x := y * z	x = y * z;	Arithmetic assignment
	x := y ÷ z	x = y / z;	Arithmetic assignment
	x := a(y)	x = a[y];	Array assignment
	x := y	x = y;	Scalar action
	a := a -{x →y}	a[x] = y;	Array action
	a := a -{x →y} -{i →j}	a[x]=y; a[i]=j;	Array action
	fun ∈ N × N → N	function fun name(uint256 arg1,
		uint256 arg2) public returns(arg)	Function definition
		{ . . . }

Table 9 :

 9 9, the observational equivalence between Event-B sets and Solidity smart contracts types is given. Equivalence between Event-B and Solidity smart contracts

	Event-B types	Solidity language
	Enumerated sets	Enumerated types
	Basic integer sets	Predefined integer types
	Event-B array types Solidity array type
	Function	Solidity function structure

http://singh.perso.enseeiht.fr/BAC-2021/SmartPurchaseModel.pdf


Karim Gizatullin
email: karimgizatullin@gmail.com

Alexander Trokhimovskiy

Anna Fedorova

Jean-Loup Bertaux

Monique Spite

Alexander Lomakin

Andrey Patrakeev

Franck Montmessin

Oleg Korablev

Near-infrared high-resolution solar spectrum from ACS NIR onboard TGO

Spectrometer

The ACS NIR is a near-infrared spectrometer, extension of SPICAM-IR instrument family [START_REF] Korablev | Spicam ir acousto-optic spectrometer experiment on mars express[END_REF], the main concept of which relies on the combination of an acousto-optic tunable filter (AOTF) and an echelle diffraction grating [START_REF] Trokhimovskiy | Near-infrared echelle-aotf spectrometer acs-nir for the exomars trace gas orbiter[END_REF]. This combination gives resolving power λ ∆λ ≈ 25, 000 in spectral range of 0.73 -1.65µm that corresponds to the echelle diffraction orders from 48 through 105. This is the first instrument that can measure with such high resolution in near-infrared range outside the atmosphere. Here we present results that were obtained in June 2016 during Mid Cruise Checkout TGO Payload (MCC) observations of Sun.

Observations

In case of direct spectrum measurements, all specifics of the optical scheme should be taken into account. For ACS NIR, current instrument model includes the shape of AOTF function, blaze function, diffraction order overlapping, spectral variations, stray light and flat field correction for the detector.

A detailed spectrally resolved solar spectrum is important for line-by-line radiative transfer modeling in the near-IR. But it is still not well known due to the difficulties in ground-based measurements because of strong water vapor absorption in this spectral range. There are theoretical calculations of high-resolution spectrum in near-IR and the CAVIAR [START_REF] Menang | A high-resolution nearinfrared extraterrestrial solar spectrum derived from ground-based fourier transform spectrometer measurements[END_REF][START_REF] Elsey | Can measurements of the near-infrared solar spectral irradiance be reconciled? a new ground-based assessment between 4,000 and 10,000 cm-1[END_REF] solar spectrum derived using the Langley technique applied to observations of ground-based high-resolution Fourier transform spectrometer (FTS) in atmospheric windows from 2000 to 10,000 cm -1 (1 -5µm). ACS NIR can provide more precise information in area 1 -1.65µm. An attempt to identify new, previously unobserved solar lines would be also shown.

Acknowledgements

ExoMars is the space mission of ESA and Roscosmos. The ACS experiment is led by IKI Space Research Institute in Moscow. The project acknowledges funding by Roscosmos and CNES. Science operations of ACS are funded by Roscosmos and ESA. K.G., A.T., A.F., O.K., A.L., J-L.B. acknowledge support from the Ministry of Education and Science of the Russian Federation, Grant 14.W03.31.0017.


Nguyen Tien-Cuonga

COMA Véroniquec, CAMELEYRE Anne-Archard Dominiqueb

Kim Anh D'

Fillaudeau Luca

IN-SITU PHYSICAL ANAL YSIS OF CELLULOSE FIBRE SUSPENSIONS DU RING ENZYMATIC HYDROLYSIS

INTRODUCTION

Lignocellulose biomass is one of the most abundant renewable resources and certainly one of the least expansive. lt was considered as a glucose source for obtain energetic or chemical molecules by bioconversion. This enzymatic conversion was sa complicate therefor a better scientific understanding and, ultimately, good technical control of these critical biocatalytic reactions, which involve complex matrices at high solid contents, is currently a major challenge if biorefining operations are ta become commonplace. Amongst the main parameters ta be studied, the rheological behaviour of the hydrolysis suspension and the fibre particle size, stand out as a major determinants of process efficiency and determine equipment ta be used and the strategies applied. Rheological behaviour of fibre suspensions is usually described by an apparent yield stress, a shear viscosity (Hershei-Buckley or Bingham models) and elasticity. During biological hydrolysis, the apparent viscosity of suspensions decreases in parallel with a decrease of particle size [START_REF] Nguyen | ln situ rheometry of concentrated cellulose fibre suspensions and relationships with enzymatic hydrolysis[END_REF]. This study focuses on the characterisation of cellulose suspensions (Microcrystalline cellulose, Whatman paper and extruded paper pulp) during enzymatic hydrolysis using in-situ and ex-situ physical analysis. The complex relationships between fibre structure, degradation, chemical composition and rheological behaviour was scrutinised.

METHODS

1. Experimental setup

The experimental set-up consists of a tank and an impeller system connected ta a viscometer working at imposed speed (Viscotester HaakeVT550,Thermo Fisher Scientific,. This allows on-line torque measurements. The rotational speed ranged between 0.5 and 800 rpm and torque between 1 and 30mN.m. The bioreactor was a homemade glass tank {diameter: 130mm, Hmax: 244mm, V: 2.0L) fitted with a water jacket. Suspension homogeneity was maintained with a shaft equipped with double impeller. The first impeller consists in a 3 inclined blades (diameter: 73.5mm, angle: 45°, h=38mm) located at 75mm height from the bottom ta ensure mixing. The second impeller is a close bottom mixer including 2 large blades {diameter: 120mm, h=22mm) ta avoid substrate decantation. Temperature was controlled by circulation (cryostat Haake DC30 and 1<20) through the water jacket. The viscometer and the cryostat were controlled by software from HaakeRheoWin Job Manager (Thermo Fisher Scientific) which also ensured data recording (temperature, torque, mixing rate). A focused bearn reflectance sensor was located in bulk in arder ta measure the distribution of particle chords.

ln-situ and ex-situ rheometry

Power consumption curve was identified and modelled with the semi-empirical madel (Churchill, 1983) including laminar and transition regions. lt was considered as the reference curve:

(( ](; )n

Jy,;

Np = :e + (Np 0 )n with n=0.834, Kp=98.1, Np 0 =0.25. The in-situ viscosity of suspension was determined using the torque and mixing rate measurements and considering the Metzner & Otto concept (1957) andRieger andNovak's approach (1973). Ex-situ viscous and elastic modules were measured by rheometer (MARS Ill, Thermo Scientific, 3.1 o• 8 < C < 0.2 N.m) under oscillation with parallel striated plate (D: 60mm, gap: 1 mm, frequency range: 0.05 to 20Hz, 20°C).

ln-situ and ex-situ granulometry

ln-situ particle size characterization was realised by chard length measurement of particles using a solidstate laser light source (FBRM G400, Mettler-Toledo, range: 0.1 to 1 OOO~o~m).

Ex-situ particle size distribution was determined through laser diffraction analyses (Mastersizer 2000 Hydra, Malvern Instruments, red À=632.8nm and blue À=470.0nm lights, range: 0.02 to 20001Jm).

Enzyme, substrate and operation conditions

Three cellulose matrices were studied in arder to investigate different fibre morphologies and particle size distributions (Table 1 ): microcrystalline cellulose (ACROS Organics), a dried and milled Whatman paper (Whatman International Ltd., Maidstone, England) and paper-pulp (Tembec Co., Saint-Gaudens, France, type FPP31) after extrusion. The Tembec paper-pulp was made from coniferous wood and contained 26.1% dry matter (75.1% cellulose, 19.1% hemicellulose, 2.2% Klason lignin and ash). An enzyme cocktail (ACCELLERASE® Genecor) containing exoglucanases, endoglucanases (2800 CMC U/g ie.

57±2.8 FPU/ml cited by [START_REF] Alvira | Effect of endoxylanase and alpha-L-arabinofuranosidase supplementation on the enzymatic hydrolysis of steam exploded wheat straw[END_REF], hemicellulases and 13glucosidases (775 pNPG Ulg) was used. lts optimal temperature and pH were sooc (range 50 to 65°C) and pH 4.8 (range 4 to 5). A dosage rate of 0.1 -0.5 ml per gram of cellulose. Enzymatic hydrolysis was carried out at 40°C due to energy saving and the microbiological step du ring the fermentation process considering a simultaneous saccharification and fermentation (SSF) operation. The pH of the medium was adjusted to 4.8 using a solution of 85% orthophosphoric acid. To avoid contamination, 201JL of a solution of chloramphenicol (5 g/L) was added. Then enzymes were added when the suspension reached homogeneity and the torque values were stable. Hydrolysis was investigated over 24h at a mixing rate of 100 rpm and using the selected concentrations: 1%, 3%dm at different enzyme/substrate ratios: 0.1 and 0.5 mUg cellulose. Samples were taken manually by a 6mm diameter flexible connected to a 50ml syringe. Each sample was about 15ml, sufficient to perform analyses on 8 sub-samples. Glucose concentration was checked in the supernatant along enzymatic hydrolysis (Analyser YSI madel 27A; Yellow Springs Instruments, Yellow Springs, Ohio, range 0-2.5g/L ± 2%, sample volume=251JL).

RESUL TS AND DISCUSSIONS

1. ln-situ and ex-situ rheometry

Under the action of enzymes, the cellulose chains were eut giving simple products such as glucose (ultimate monomer). The glucose concentration (i.e bioconversion percentage) was increased with the time of hydrolysis (between 1 and 24 hours) to reach a final value that was very different for the three substrates (Table 2). For the lowest enzyme/substrate ratio, the enzymatic attack strongly depends on fibre structures and substrate compositions; by consequence the bioconversion rate of MCC was higher than PP and WP. On the contrary, this dependance was limited when the ratio enzyme/substrate increased. For MCC and PP, at the ratio 0.5 mllg cellulose, their bioconversion rates reached 61% and 72% respectively which were superior to the results reported by [START_REF] Dasari | The effect of particle size on hydrolysis reaction rates and rheological properties in cellulosic slurries[END_REF][START_REF] Pereira | Sugarcane bagasse enzymatic hydrolysis: rheological data as criteria for impeller selection[END_REF]Szijarto et al., 2011 (bioconversion The changes in the physical appearance of the slurry are associated to the biochemical changes of fibres.

A sharp decrease of viscosity was observed with WP and PP during hydrolysis whereas with MCC its viscosity remain stable having value of water viscosity (=0.6mPa.s) (Fig 1-A). Under 100 rpm, it was the same observed phenomena for WP, 0.62 to 0.006 Pa.s and PP, 0.574 to 0.007 Pa.s. However, this reduction is faster for WP than for PP. lt takes 3h for one reduction of 100 times with WP comparing 10h with PP. This evolution of viscosity is supported by the literature over a wide range of matrices, particle sizes and enzyme/cellulose ratios [START_REF] Geddes | Optimizing cellulase usage for improved mixing and rheological properties of acid-pretreated sugarcane bagasse[END_REF][START_REF] Nguyen | ln situ rheometry of concentrated cellulose fibre suspensions and relationships with enzymatic hydrolysis[END_REF]Pereira et al., 2010;[START_REF] Um | Optimization of Ethanol Production from Concentrated Substrate[END_REF][START_REF] Wiman | Rheological Characterization of Dilute Acid Pretreated Softwood[END_REF]. The ex-situ rheometry results showed a typical viscoelastic behaviour being confirmed bath in the initial step and during hydrolysis for WP and PP (for MCC, it is impossible to realise this measurement because of substrate decantation). The elastic behaviour was predominately comparing with viscous module; however these two modules decreased regular during hydrolysis (fig 1-B).

Evolution of particle size during enzymatic hydrolysis

During hydrolysis, as the fibres were degraded, their morphology (shape, area, length ... ) significantly changed [START_REF] Nguyen | Production of fermentescible sugar from paper-pulp: Looking for a dynamique and multiscale integrated models based on physical parameters[END_REF]. The large particles were hydrolysed; their mean diameter decreased for ali substrates (Fig 2 -B). This led to the reduction of viscosity suspension. The hydrolysis effect was mainly observed on coarse particles. The fine population increases and translates to a smaller diameter. The same result was reported by [START_REF] Nguyen | ln situ rheometry of concentrated cellulose fibre suspensions and relationships with enzymatic hydrolysis[END_REF][START_REF] Um | Optimization of Ethanol Production from Concentrated Substrate[END_REF][START_REF] Wiman | Rheological Characterization of Dilute Acid Pretreated Softwood[END_REF]. However, coherence of in-situ and ex-situ data need to be explored to strengthen our understanding of particle deconstructing. . . ... This study focussing on the rheometry of lignocellulosic suspensions explored enzymatic hydrolysis based on physical parameters. A method for following viscosity and particle size on-line was proposed and used to characterise the cellulose suspensions. Du ring enzymatic hydrolysis, the change in viscosity was found due to enzymatic actions and modifications of fibre properties. The decrease of fibre mean diameter could lead to the decrease of suspension viscosity and the effect of enzymatic attack.

• ... ..• •• • • t!• •• •• lE!! ! • ..: • •••• 300 70 • B 250 60 • Ê • • • 50 Ê a 2oo • • ..

Fig. 1 .

 1 Fig. 1. Evolution of in-situ viscosity (A) and ex-situ viscous and elastic modules (8) during enzymatic hydrolysis (Suspension at 3%dm and 0.1 mL enzyme/g cellulose).

Fig. 2 .

 2 Fig. 2. Evolution of volume cumulative distribution as a function of particle diameter or chard (A) and mean chard (number weighted) and mean diameter (volume weighted) as a function of bioconversion rate (B) (Suspension of PP 3%dm, 0.5mL enzyme/g cellulose) 4. CONCLUSION

Table 1 :

 1 Substrate properties (MCC: microcrystalline cellulose. WP: Whatman paper and PP: extruded

		paper pulp)
		MCC	WP	pp
	Dry matter (%)	99	99	26
	Cellulose(%)	100	90	75
	D[4,3] (IJm)	70	250	190
	p (g/L)	1623 ± 28 1200 ± 2	1346 ± 2
	Crystallinity (%)	79.0	88.6	64.5

  rates between 3.6% and 45%).

		Table 2. Bioconversion percentage at 24h of hydrolysis
	Substrate	Concentration (%dm) Ratio enzyme/substrate Bioconversion rate(%)
	MCC	1%	0.1 ml/g cellulose	34.8
	MCC	1%	0.5 ml/g cellulose	61.2
	pp pp	1% 3%	0.1 mllg cellulose 0.5 ml/g cellulose	17.3 72.1
	WP	1%	0.1 ml/g cellulose	12.8


Sarrah Boukthir

Loren Dejoies

Asma Zouari

Anaïs Collet

Sophie Potrel

Gabriel Auger

Prof Vincent Cattoir
email: vincent.cattoir@chu-rennes.fr.

In vitro activity of eravacycline

Keywords: 34 References Enterococcus, VRE, Eravacycline, Tigecycline, Tetracycline resistance

and mechanisms of resistance in enterococci

Introduction

Enterococci, in particular E. faecalis and E. faecium, are opportunistic pathogens that are increasingly responsible for hospital-acquired infections and acquisition of multidrug resistance (MDR) is an important issue for therapeutic management [START_REF] Kristich | Enterococcal Infection-Treatment and Antibiotic Resistance[END_REF]. Numerous clinical isolates, with regionally varying incidence, have especially acquired resistance to vancomycin (vancomycin-resistant enterococci [VRE]) [START_REF] Cattoir | Antibiotic resistance in Enterococcus faecium clinical isolates[END_REF]. For the treatment of VRE infections, only a few therapy options remain available such as linezolid, daptomycin or tigecycline (TGC) [START_REF] Kristich | Enterococcal Infection-Treatment and Antibiotic Resistance[END_REF].

As a member of the tetracycline family, TGC (a semi-synthetic derivative of minocycline) acts by inhibiting bacterial protein biosynthesis by binding to the 30S subunit of the ribosome. Resistance to classical tetracyclines is mainly due to ribosomal protection and/or active efflux pump. Different classes of ribosomal protection proteins exist, the most common ones being encoded by tet(M), tet(O) and tet(S) genes. Several efflux pump-encoding genes have been described both in Grampositives [e.g. tet(K) and tet(L)] and Gram-negatives [e.g. tet(A) and tet(B)] [START_REF] Zhanel | Review of Eravacycline, a Novel Fluorocycline Antibacterial Agent[END_REF]. All these genes are usually located on plasmids and are then transferable. In enterococci, the most frequent genes implicated in tetracycline resistance are tet(L), tet(M), tet(O) and tet(S) while ribosomal protection is the most common acquired mechanism of resistance [START_REF] Grossman | Tetracycline Antibiotics and Resistance[END_REF][START_REF] Thaker | The tetracycline resistome[END_REF]. Interestingly, TGC is not or only poorly affected by these classical tetracycline resistance determinants and the mechanism of TGC decreased susceptibility in enterococci is associated with alterations of the S10 protein of the ribosomal 30S subunit encoded by the rpsJ gene or the overexpression of tet(M) and tet(L) genes [START_REF] Cattoir | Genomic analysis of reduced susceptibility to tigecycline in Enterococcus faecium[END_REF][START_REF] Bender | Update on prevalence and mechanisms of resistance to linezolid, tigecycline and daptomycin in enterococci in Europe: Towards a common nomenclature[END_REF][START_REF] Dabul | Molecular basis for the emergence of a new hospital endemic tigecycline-resistant Enterococcus faecalis ST103 lineage[END_REF][START_REF] Bender | A Nosocomial Cluster of Tigecycline-and Vancomycin-Resistant Enterococcus faecium Isolates and the Impact of rpsJ and tet(M) Mutations on Tigecycline Resistance[END_REF]. Even though enterococcal clinical isolates resistant to TGC have been mainly reported sporadically, some hospital outbreaks due to TGC-resistant epidemic clones have been described in Brazil [START_REF] Dabul | Molecular basis for the emergence of a new hospital endemic tigecycline-resistant Enterococcus faecalis ST103 lineage[END_REF] and Germany [START_REF] Bender | A Nosocomial Cluster of Tigecycline-and Vancomycin-Resistant Enterococcus faecium Isolates and the Impact of rpsJ and tet(M) Mutations on Tigecycline Resistance[END_REF], highlighting their potential risk of spread.

Novel compounds of the tetracycline family, including eravacycline (ERC) have been recently developed. ERC, formerly known as TP-434, is a fully synthetic fluorocycline developed to escape the resistance mechanisms of the tetracycline class as efflux pumps and ribosomal protection mechanisms. Its possible oral use makes it more advantageous than tigecycline. Intravenous administration is also possible, in this case the serum concentrations obtained are higher than those obtained with tigecycline. In addition, the MIC to the ERC of the different strains tested are significantly lower than those of TGC, making ERC a promising antibiotic [START_REF] Grossman | Target-and resistance-based mechanistic studies with TP-434, a novel fluorocycline antibiotic[END_REF][START_REF] Clark | Fluorocyclines. 2. Optimization of the C-9 side-chain for antibacterial activity and oral efficacy[END_REF][START_REF] Xiao | Fluorocyclines. 1. 7-fluoro-9-pyrrolidinoacetamido-6-demethyl-6-deoxytetracycline: a potent, broad spectrum antibacterial agent[END_REF]. This molecule acts like the other tetracyclines by reversibly binding to the ribosomal 30S subunit and preventing the bacterial protein synthesis [START_REF] Zhanel | Review of Eravacycline, a Novel Fluorocycline Antibacterial Agent[END_REF]. It has excellent activity in vitro and in vivo on both Gram-positive and Gram-negative bacteria and anaerobes, including MDR strains such as VRE [START_REF] Monogue | Antibacterial Efficacy of Eravacycline In Vivo against Gram-Positive and Gram-Negative Organisms[END_REF][START_REF] Zhanel | In vitro activity of eravacycline against 2213 Gram-negative and 2424 Gram-positive bacterial pathogens isolated in Canadian hospital laboratories: CANWARD surveillance study 2014-2015[END_REF][START_REF] Snydman | Evaluation of the In Vitro Activity of Eravacycline against a Broad Spectrum of Recent Clinical Anaerobic Isolates[END_REF]. Its use is recommended by the FDA in August 2018 for complicated abdominal infections [START_REF] Solomkin | Eravacycline: a new treatment option for complicated intra-abdominal infections in the age of multidrug resistance[END_REF].Some ERCresistant clinical isolates of enterobacteria, A. baumannii and S. aureus have been reported in the literature [START_REF] Zhang | Eravacycline activity against clinical S. aureus isolates from China: in vitro activity, MLST profiles and heteroresistance[END_REF][START_REF] Zheng | Overexpression of OqxAB and MacAB efflux pumps contributes to eravacycline resistance and heteroresistance in clinical isolates of Klebsiella pneumoniae[END_REF][START_REF] Shi | Mechanism of eravacycline resistance in Acinetobacter baumannii mediated by a deletion mutation in the sensor kinase adeS, leading to elevated expression of the efflux pump AdeABC[END_REF], but no ERC-resistant enterococci have been described so far.

The aim of the work was first to study the in vitro activity of ERC against clinical isolates enterococci including VRE and to compare it to other tetracyclines. Secondly, an analysis of the associated resistance mechanisms was performed.

Materials and Methods

Bacterial isolates

A panel of 60 non-duplicate strains of enterococci was studied consisting of: 54 epidemiologicallyunrelated clinical isolates (46 E. faecium and 8 E. faecalis) including 42 VRE (33 vanA positive and 9 vanB positive), 3 in vitro mutants resistant to TGC (E. faecium AusTig, HMtig1 and HMtig2 [START_REF] Cattoir | Genomic analysis of reduced susceptibility to tigecycline in Enterococcus faecium[END_REF]) and 3 reference strains (E. faecium Aus0004 [START_REF] Lam | Comparative analysis of the first complete Enterococcus faecium genome[END_REF] and HM1070 [START_REF] Bozdogan | Effects of Genes Encoding Resistance to Streptogramins A and B on the Activity of Quinupristin-Dalfopristin against Enterococcus faecium[END_REF], E. faecalis ATCC 29212). All the clinical TGC-resistant isolates received at the National Reference Centre for Enterococci (university hospital of Rennes, France) from all French hospitals between 1 st January 2017 and 31 st December 2018 were included (as positive controls) as well as TGC-susceptible epidemiologically-unrelated strains (as negative controls). They were isolated from rectal swabs (n=39), urines (n=7), blood cultures (n=4) and surgical samples (n=4). All the strains were identified by MALDI-TOF mass spectrometry (Microflex; Bruker Daltonics, Bremen, Germany).

Antimicrobial susceptibility testing

The MICs of the different tetracyclines tested (ERC, TGC, doxycycline [DOX], minocycline [MIN] and tetracycline [TET]) were determined by broth microdilution (BMD) method according to Clinical and Laboratory Standards Institute (CLSI) guidelines [START_REF] Humphries | CLSI Methods Development and Standardization Working Group Best Practices for Evaluation of Antimicrobial Susceptibility Tests[END_REF], except for ERC (MIC test strips supplied by Liofilchem; Roseto degli Abruzzi, Italy). For BMD, the serialdilution of antibiotics (all prepared extemporaneously) were from 32 to 0.03 mg/L and the MH medium used (Becton Dickinson, Spark, MD, USA) was adjusted to provide 20 to 25 mg/L of calcium and 10 to 12.5 mg/L of magnesium. The MIC is defined as the lowest concentration of antimicrobial agent that inhibited the growth at 35±2°C after 24 h of incubation in aerobic conditions. Results were determined and interpreted according to European Committee on Antimicrobial Susceptibility Testing (EUCAST) clinical breakpoints for TGC (sensitive (S) ≤ 0.25 mg/L; resistance (R) > 0.25 mg/L) and ERC (S ≤ 0.125 mg/L; R > 0.125 mg/L) (www.eucast.org). Enterococcus faecalis ATCC 29212 and Staphylococcus aureus ATCC 29213 served as quality control strains for each tested batch.

Gene resistance screening

Genomic DNA of TGC-and ERC-resistant strains was extracted using the InstaGene kit (Bio-Rad, Hercules, CA). The tet(L), tet(M), tet(O) and tet(S) genes were screened, and rpsJ gene was amplified by performing specific real-time PCR assays (primers and probes previously described by Cattoir et al. [START_REF] Cattoir | Genomic analysis of reduced susceptibility to tigecycline in Enterococcus faecium[END_REF]). All rpsJ PCR-amplified products were sequenced in both directions by the Sanger method using the same primers . RpsJ deduced-amino-acid sequences obtained thanks to the alignment tool of CLC Genomics Workbench (Qiagen) were compared with those of reference strains E. faecium DO (GenBank accession no. NC_017960) and E. faecalis V583 (GenBank accession no. NC_004668) by using the BLASTX program (https://blast.ncbi.nlm.nih.gov/Blast.cgi). The screening for vancomycin resistance genes was also done by qPCR as previously described [START_REF] Sassi | Emergence of optrA-mediated linezolid resistance in enterococci from France, 2006-16[END_REF].

Results

In vitro activity of tetracyclines against enterococci

Of the different tetracyclines tested, ERC showed the lowest MIC 90 (0.08 mg/L) as compared to the other tetracyclines (Table 1). MIC 50 was higher for E. faecalis strains (between 1 and 5-fold-dilutions apart) compared to E. faecium strains. MIC 90 were higher for E. faecium isolates for ERC (0.08 mg/L) and TGC (0.5 mg/L) with one and two-fold-dilutions difference respectively. MIC 90 was identical between the two species for the other tetracyclines.

In E. faecium strains, MIC 50 and MIC 90 values were identical for ERC and TGC regardless of the susceptibility to vancomycin whereas for the other molecules a higher value of at least one folddilution was observed in VRE strains (Table 1). Focusing on VRE strains, a significant difference was observed between strains carrying the vanA and vanB genes (Table 1). Indeed, MIC 90 values of ERC and TGC were 0.19 mg/L and 1 mg/L for VRE vanA(+) versus 0.016 mg/L and 0.06 mg/L for vanB(+), respectively.

Since a critical concentration is only available for TGC and ERC, only results for these molecules were interpreted for susceptibility and resistance. Among the strains studied, 8 E. faecium and 1 E. faecalis were categorized as resistant to TGC with MICs ranging from 0.5 to 8 mg/L, MICs of classical tetracyclines being variable (Table 2). Four of the TGC-R (TGC MICs ≥1mg/L) strains were also resistant to ERC with MICs between 0.19 and 1.5 mg/L, and also exhibited high MICs for all the classical tetracyclines (Table 2).

Mechanisms of resistance to TGC and/or ERC

To decipher the mechanisms of resistance to TGC and ERC, tet genes were screened in resistant strains. Most of the strains possessed one or two tet resistance genes: tet(L) (n=1), tet(M) (n=2), tet(L) + tet(M) (n=3) and tet(M) + tet(S) (n=2) (Table 2). None tet(O) was detected. None of these resistance genes were been found in the E. faecalis isolate and in vitro mutants HMtig1 and HMtig2, which was expected since the parental strain HM1070 is susceptible to tetracyclines [START_REF] Cattoir | Genomic analysis of reduced susceptibility to tigecycline in Enterococcus faecium[END_REF].

Note that all the ERC-R isolates (n=4) carried the tet(M) gene, two of them also carried the tet(L) gene and the other also tet(S) gene (Table 2). All strains resistant to ERC were strains of E. faecium resistant to vancomycin (vanA positive).

The amino acid sequence of the S10 protein (encoded by rpsJ) was also determined in ERC-and/or TGC-resistant strains. Two types of modifications were observed, substitutions (most frequently) and deletions, all between amino acids 52 and 60 (Table 2). All strains resistant to ERC and TGC (n=4) displayed one non-synonymous substitution: I 52 M (n=1), H 56 N (n=2) and K 57 R (n=1). Three of these strains additionally had a deletion of two (delR53_A54, n=1) or four amino acids (delI52_T55, n=2).

Concerning the TGC-resistant/ERC-susceptible strains (n=5), all E. faecium strains had a protein S10 substitution: D 60 Y (n=4) and K 57 E (n=1). The E. faecalis strain did not show any rpsJ mutation.

The more strains accumulated tet genes and S10 protein modification, the higher their tetracycline MICs were. All ERC-R strains had two tet resistance genes and one S10 protein alteration. E. faecium strains TGC-R and ERC-S had one tet resistance gene and/or a mutation on rpsJ gene.

Discussion

ERC has shown good in vitro activity against a wide panel of bacteria in many studies [START_REF] Zhanel | In vitro activity of eravacycline against 2213 Gram-negative and 2424 Gram-positive bacterial pathogens isolated in Canadian hospital laboratories: CANWARD surveillance study 2014-2015[END_REF][START_REF] Snydman | Evaluation of the In Vitro Activity of Eravacycline against a Broad Spectrum of Recent Clinical Anaerobic Isolates[END_REF], we find similar results with a low MIC 90 at 0.08 mg/L against enterococci including VRE. In this study, we report for the first time four ERC-resistant clinical enterococcal isolates, which is in line with resistance previously reported in Gram-negative (overexpression of efflux pumps and tetracyclineinactivating enzyme) [START_REF] Zheng | Overexpression of OqxAB and MacAB efflux pumps contributes to eravacycline resistance and heteroresistance in clinical isolates of Klebsiella pneumoniae[END_REF][START_REF] Shi | Mechanism of eravacycline resistance in Acinetobacter baumannii mediated by a deletion mutation in the sensor kinase adeS, leading to elevated expression of the efflux pump AdeABC[END_REF][START_REF] Wang | Novel Plasmid-Mediated tet(X5) Gene Conferring Resistance to Tigecycline, Eravacycline, and Omadacycline in a Clinical Acinetobacter baumannii Isolate[END_REF] and other Gram-positive (efflux pumps and ribosomal protection) [START_REF] Zhang | Eravacycline activity against clinical S. aureus isolates from China: in vitro activity, MLST profiles and heteroresistance[END_REF] bacteria.

Analysis of these four strains showed that the occurrence of ERC resistance resulted from an accumulation of several resistance mechanisms. Indeed, these strains exhibited high MICs for all the tetracyclines studied, suggesting a high-level resistance to this class of antibiotics. Moreover, for each of them, two tet resistance genes were simultaneously found, i.e. tet(M) + tet(L) or tet(M) + tet(S).

These acquired resistance genes were associated with alterations in the S10 protein in all cases. All these elements suggest that resistance to ERC in enterococci would require the presence of at least two tet genes associated with an rpsJ mutation. The ERC was initially developed to deal with classical acquired resistance mechanisms (active efflux and ribosomal protection) and numerous studies have shown its effectiveness against strains carrying them, including the very common Tn916-likeassociated tet(M) gene [START_REF] Zhanel | Review of Eravacycline, a Novel Fluorocycline Antibacterial Agent[END_REF][START_REF] Grossman | Target-and resistance-based mechanistic studies with TP-434, a novel fluorocycline antibiotic[END_REF][START_REF] Clark | Fluorocyclines. 2. Optimization of the C-9 side-chain for antibacterial activity and oral efficacy[END_REF][START_REF] Xiao | Fluorocyclines. 1. 7-fluoro-9-pyrrolidinoacetamido-6-demethyl-6-deoxytetracycline: a potent, broad spectrum antibacterial agent[END_REF][START_REF] Thabit | Assessment of in vivo efficacy of eravacycline against Enterobacteriaceae exhibiting various resistance mechanisms: a dose-ranging study and pharmacokinetic/pharmacodynamic analysis[END_REF]. All ERC-R enterococcal isolates studied were strains of E. faecium vanA(+) suggesting plasmid acquisition of previously reported tet genes as described by others [START_REF] Fiedler | Tigecycline resistance in clinical isolates of Enterococcus faecium is mediated by an upregulation of plasmid-encoded tetracycline determinants tet(L) and tet(M)[END_REF]; different expression of the tet genes (plasmid versus. chromosome) depending on the strain studied could explain the absence of an in vitro ERC-R mutant.

All ERC-resistant isolates were also highly resistant to TGC with high MICs (≥1 mg/L) suggesting the evolutionary potential of these enterococcal strains and the risk of therapeutic failure by ERC in case of infections caused by strains highly resistant to TGC. No significant difference was observed between the ERC and TGC MIC 90 of VRE and vancomycin-susceptible strains, which may be surprising since MIC 90 reflect acquired resistance, it could be explained by the low number of vancomycinsusceptible strains tested (8 vs. 43).

Focusing on the S10 protein, the location of the rpsJ changes seems to be important and responsible for different resistance levels. Indeed, alterations located between amino acids 57 and 60 seem to be responsible for resistance to TGC as described above [START_REF] Cattoir | Genomic analysis of reduced susceptibility to tigecycline in Enterococcus faecium[END_REF][START_REF] Beabout | The ribosomal S10 protein is a general target for decreased tigecycline susceptibility[END_REF] and not to ERC. The alterations of the amino acids between positions 54 and 57 would lead to resistance to both TGC and ERC, which has not yet been described to our knowledge and remains to be demonstrated experimentally. Changes in these amino acids are probably significant enough to affect the conformation of the 16S rRNA and therefore prevent both TGC and ERC from binding to the ribosome. For the TGC-resistant/ERCsusceptible strains, a single tet gene and a single rpsJ mutation (non-synonymous substitution) were found. Based on our results, deletions of rpsJ in enterococci seem to be necessary to confer ERC resistance.

One strain of TGC-resistant E. faecalis was found in our panel. Neither the presence of a tet gene nor a rpsJ modification were identified suggesting that the involvement of other mechanisms such as another tet gene or chromosomal mutation, or less likely a Tet(X)-mediated enzymatic inactivation [START_REF] Grossman | Tetracycline Antibiotics and Resistance[END_REF].

Conclusion

It seems difficult to predict the evolution of tetracycline resistance, in particular through the evolution of rpsJ gene mutations in vivo in exposed patients, demonstrating the non-negligible risk of selection of tetracycline-resistant mutants [START_REF] Niebel | Deletions in a ribosomal protein-coding gene are associated with tigecycline resistance in Enterococcus faecium[END_REF]. Although having an excellent in vitro activity, ERC does not escape the resistance mechanisms already reported as TGC.

  ***************:** *********** ***************:** *********** ***************:** *********** ****************** *********** a ERC, eravacycline; TGC, tigecycline; DOX, doxycline; MIN, minocycline; TET, tetracycline. MIC of ERC and TGC are indicated in bold for resistant strains. b rpsJ sequences were aligned against those of susceptible reference strains E. faecium DO and E. faecalis V583. Nonsynonymous substitutions are indicated by a colon and deletion by a space for each amino acid (the absence of modification is represented by an asterisk). None synonymous substitution was observed. c non-functional truncated tet(M) gene.

d

  Strains categorized as susceptible to TGC but with elevated MIC.

Table 1 .

 1 In vitro activity (MICs in mg/L) of tetracyclines against enterococci MIC 90 and MIC range of each tetracyclines tested are represented for all the isolates studied in the first line and then considering bacterial species and vancomycin-susceptibility.

	Strains	Eravacycline	Tigecycline		Doxycycline		Minocycline		Tetracycline
		MI	MI	MIC	MI	MI	MIC	MI	MI	MIC	MI	MI	MIC	MI	MI	MIC
		C 50	C 90	ran	C 50	C 90	ran	C 50	C 90	ran	C 50	C 90	ran	C 50	C 90	ran
				ge			ge			ge			ge			ge
	All	0.0	0.0	0.0	≤0.	0.5 ≤0.	4	32 ≤0.	8	16 ≤0.	32 >3	≤0.
	(n=60)	16	8	04-	03		03-			03-			03-		2	03-
				1.5			8			>32			32			>32
	E.	0.0	0.0	0.0	≤0.	0.5 ≤0.	4	32 ≤0.	0.5 16 ≤0.	16 >3	0.0
	faecium	16	8	04-	03		03-			03-			03-		2	6-
	(n=51)			1.5			8			>32			32			>32
		0.0	0.0	0.0	≤0.	0.5 ≤0.	0.1	4	≤0.	0.1	8	≤0.	0.2	32 0.1
	vancom	16	8	08-	03		03-	25		03-	25		03-	5		25-
	ycin-			0.0			0.5			>32			32			>32
	suscepti			8
	ble
	(n=8)
		0.0	0.0	0.0	≤0.	0.5 ≤0.	8	32 ≤0.	8	16 ≤0.	32 >3	0.0
	vancom	16	8	04-	03		03-			03-			03-		2	6-
	ycin-			1.5			8			>32			32			>32
	resistan
	t (n=43)
		0.0	0.1	0.0	≤0.	1	≤0.	8	32 ≤0.	8	16 ≤0.	32 >3	0.0
	vanA	16	9	04-	03		03-			03-			03-		2	6-
	(n=32)			1.5			8			>32			32			>32
		0.0	0.0	0.0	≤0.	0.0	≤0.	0.1	16 ≤0.	16 16 ≤0.	0.2	32 0.0
	vanB	12	16	08-	03	6	03-	25		03-			03-	5		6-

Table 2 .

 2 Characteristics of eravacycline-and/or tigecycline-resistant isolates and reference strains

Acknowledgments

The authors warmly thank all the microbiologists who sent clinical isolates to the NRC-Enterococci.

Declarations

Funding This work was supported by 'Santé Publique France', the French national public health agency.

Competing Interests: No

Ethical Approval; Not required