Emmanuelle Anceaume

Antonella Del Pozzo

Romaric Ludinard

Maria Potop-Butucaru

Sara Tucci-Piergiovanni

Sara Tucci

Maria Potop

Blockchain Abstract Data Type -Full version

Keywords: Blockchain, Abstract Data Type, Consistency Criteria

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

Introduction

The paper proposes a new data type to formally model blockchains and their behavior. We aim at providing consistency criteria to capture the correct behavior of current blockchain proposals in a unified framework. It is already known that some blockchain implementations solve eventual consistency of an append-only queue using Consensus [START_REF] Anta | Formalizing and implementing distributed ledger objects[END_REF][START_REF] Androulaki | Hyperledger Fabric: A Distributed Operating System for Permissioned Blockchains[END_REF]. The question 1 is about the consistency criterion of blockchains as Bitcoin [START_REF] Nakamoto | Bitcoin: A Peer-to-Peer Electronic Cash System[END_REF] and Ethereum [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger[END_REF] that technically do not solve Consensus, and their relation with Consensus in general.

We advocate that the key point to capture blockchain behaviors is to define consistency criteria allowing mutable operations to create forks and restricting the values read, i.e. modeling the data structure as an append-only tree and not as an append-only queue. This way we can easily define semantics equivalent to eventually consistent append-only queue but as well as weaker semantics. More in detail, we define a semantic equivalent to eventually consistent append-only queue by restricting any two reads to return two chains such that one is the prefix of the other. We call this consistency property Strong Prefix (already introduced in [START_REF] Girault | Monotonic prefix consistency in distributed systems[END_REF]). Additionally, we define a weaker semantics restricting any two reads to return chains that have a divergent prefix for a finite interval of the history. We call this consistency property Eventual Prefix. Note that our consistency criteria specifically defined for blockchain systems have a similarity flavor with fork-consistency defined in [START_REF] Mazieres | Building secure file systems out of byzantine storage[END_REF], which concern a different area, i.e., the data integrity in the network file system domain.

Another peculiarity of blockchains lies in the notion of validity of blocks, i.e. the blockchain must contain only blocks that satisfy a given predicate. Let us note that validity can be achieved through proof-of-work (Dwork and Naor [START_REF] Dwork | Pricing via processing or combatting junk mail[END_REF]) or other agreement mechanisms. We advocate that to abstract away implementation-specific validation mechanisms, the validation process must be encapsulated in an oracle model separated from the process of updating the data structure. Because the oracle is the only generator of valid blocks and only valid blocks can be appended to the tree, it follows that, it is the oracle that grants the access to the data structure and it might also own a synchronization power to control the size of forks, i.e., the number of blocks that point back to the same block of the tree. In this respect we define oracle models such that, depending on the model, the size k of forks can be equal to 1 (i.e., strongest oracle model), strictly greater than 1, or unbounded (i.e., weakest oracle model).

The blockchain is thus abstracted by an oracle-based construction in which the update and consistency of the tree data structure depends on the validation and synchronization power of the oracle.

The main contribution of the paper is a formal unified framework providing blockchain consistency criteria that can be combined with oracle models in a proper hierachy of abstract data types [START_REF] Perrin | Causal consistency: beyond memory[END_REF] independent of the underlying communication and failure models. Thanks to the establishment of the formal framework the following implementability results are shown.

• The strongest oracle, guaranteeing no fork, has Consensus number ∞ in the Consensus hierarchy of concurrent objects [START_REF] Herlihy | Wait-free synchronization[END_REF] (Theorem 5.2). Note that similarly to [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF][START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF][START_REF] Cachin | Secure and efficient asynchronous broadcast protocols[END_REF] we extend the validity property of Consensus to fit the blockchain setting.

• The weakest oracle, which validates a potentially unbounded number of blocks to be appended to a given block, is not stronger than Generalized Agreement Lattice [START_REF] Falerio | Generalized lattice agreement[END_REF].

• The impossibility to guarantee Strong Prefix in a message-passing system if forks of size k > 1 are allowed (Theorem 5.6). This means that Strong Prefix needs the strongest oracle to be implemented, which is at least as strong as Consensus.

• A necessary condition (Theorem 5.5) for Eventual Prefix in a message-passing system is that each update sent by a correct process must be eventually received by every correct process. Moreover, the result implies that it is impossible to implement Eventual Prefix if even a single update is dropped at some correct process while it has been received at all the other correct processes.

The proposed framework along with the above-mentioned results helps in classifying existing blockchains in terms of their consistency and implementability. We used the framework to classify several blockchain proposals. We showed that Bitcoin [START_REF] Nakamoto | Bitcoin: A Peer-to-Peer Electronic Cash System[END_REF] and Ethereum [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger[END_REF] have a validation mechanism that maps to our weakest oracle and then they only implement Eventual prefix, while other proposals map to our strongest oracle, falling in the class of those that guarantee Strong Prefix (e.g. Hyperledger Fabric [START_REF] Androulaki | Hyperledger Fabric: A Distributed Operating System for Permissioned Blockchains[END_REF], PeerCensus [START_REF] Decker | Bitcoin meets strong consistency[END_REF], ByzCoin [START_REF] Kokoris-Kogias | Enhancing bitcoin security and performance with strong consistency via collective signing[END_REF], see Section 5.3 for further details).

Related work

In [START_REF] Oswald | The Bitcoin Backbone Protocol: Analysis and Applications[END_REF] the authors extract Bitcoin backbone and define invariants that this protocol has to satisfy in order to verify with high probability an eventual consistent prefix. This line of work has been continued by [START_REF] Pass | Fruitchains: A fair blockchain[END_REF]. However, to the best of our knowledge, no other previous attempt proposed a consistency unified framework and hierarchy capturing both Consensus-based and proof-of-work based blockchains. In [START_REF] Abraham | The blockchain consensus layer and BFT[END_REF], the authors present a study about the relationships between Byzantine fault tolerant consensus and blockchains. In order to abstract out the proof-of-work mechanism the authors propose a specific oracle, in the same spirit of our oracle abstraction, but more specific than ours, since it makes a direct reference to proofof-work properties. In parallel and independently of our work, [START_REF] Anta | Formalizing and implementing distributed ledger objects[END_REF] proposes a formalization of distributed ledgers modeled as an ordered list of records. The authors propose in their formalization three consistency criteria: eventual consistency, sequential consistency and linearizability. Interestingly, they show that a distributed ledger that provides eventual consistency can be used to solve the consensus problem. These findings confirm our results about the necessity of Consensus to solve Strong Prefix. On the other hand, the proposed formalization does not propose weaker consistency semantics more suitable for proof-of-work blockchains as BitCoin. The work achieved in [START_REF] Anta | Formalizing and implementing distributed ledger objects[END_REF] is complementary to the one presented in [START_REF] Anceaume | Bitcoin a distributed shared register[END_REF], where the authors study the consistency of blockchain by modeling it as a register. Finally, [START_REF] Girault | Monotonic prefix consistency in distributed systems[END_REF] presents an implementation of the Monotonic Prefix Consistency (MPC) criterion and showed that no criterion stronger than MPC can be implemented in a partition-prone message-passing system.

Preliminaries on shared object specifications based on Abstract Data Types

The basic idea underlying the use of abstract data types is to specify shared objects using two complementary facets [START_REF] Perrin | Distributed Systems, Concurrency and Consistency[END_REF]: a sequential specification that describes the semantics of the object, and a consistency criterion over concurrent histories, i.e. the set of admissible executions in a concurrent environment. In this work we are interested in consistency criteria achievable in a distributed environment in which processes are sequential and communicate through message-passing.

Abstract Data Type (ADT)

The model used to specify an abstract data type is a form of transducer, as Mealy's machines, accepting an infinite but countable number of states. The values that can be taken by the data type are encoded in the abstract state, taken from a set Z. We refer by ξ 0 ∈ Z the initial state of the ADT. It is possible to access the object using the symbols of an input alphabet A. Unlike the methods of a class, the input symbols of the abstract data type do not have arguments. Indeed, as one authorizes a potentially infinite set of operations, the call of the same operation with different arguments is encoded by different symbols. An operation can have two types of effects. First, it can have a side-effect that changes the abstract state according to the transition system formalized by a transition function τ . Second, operations can return values taken from an output alphabet B, which depends on the state in which they are called and an output function δ. For example, the pop operation in a stack removes the element at the top of the stack and returns that element (its output). In the following, an abstract data type refers to a 6-tuple T = A, B, Z, ξ 0 , τ, δ . The formal specification of abstract data types is as follows.

Definition 3.1. (Abstract Data Type T ) An abstract data type is a 6-tuple T = A, B, Z, ξ 0 , τ, δ where:

• A and B are countable sets called input alphabet and output alphabet;

• Z is a countable set of abstract states and ξ 0 is the initial abstract state;

• τ : Z × A → Z is the transition function; • δ : Z × A → B is the output function.
Definition 3.2. (Operation) Let T = A, B, Z, ξ 0 , τ, δ be an abstract data type. An operation of T is an element of Σ = A ∪ (A × B). We refer to a couple (α, β) ∈ A × B as α/β. We extend the transition function τ over the operations and apply τ on the operations input alphabet:

τ T :      Z × Σ → Z (ξ, α) → τ (ξ, α) if α ∈ A (ξ, α/β) → τ (ξ, α) if α/β ∈ A × B

Sequential specification of an ADT

An abstract data type, by its transition system, defines the sequential specification of an object. The sequential specification of an object describes its behavior when its operations are applied sequentially. That is, if we consider a path that traverses its system of transitions, then the word formed by the subsequent labels on the path is part of the sequential specification of the abstract data type, i.e. it is a sequential history. A sequential history of an ADT T refers to a sequence (σ i ) i≥0 (finite or not) of operations leading the state of T to evolve according to its specification. More formally,

Definition 3.3. (Sequential specification L(T )) A finite or infinite sequence σ = (σ i ) i∈D ∈ Σ ∞ , D = N or D = {0, .
. . , |σ| -1} is a sequential history of an abstract data type T if there exists a sequence of the same length (ξ i+1 ) i∈D ∈ Z ∞ (ξ 0 has already been defined has the initial state) of states of T such that, for any i ∈ D,

• ξ i ∈ δ -1 T (σ i ), i.e.
, the output alphabet of σ i is compatible with ξ i ;

• τ T (ξ i , σ i ) = ξ i+1 , i.e.
, the execution of the operation σ i is such that the state changes from ξ i to ξ i+1 .

The sequential specification of T is the set of all its possible sequential histories L(T ).

Concurrent histories of an ADT

Concurrent histories are defined considering a partial order relation among events executed by different processes. A set of processes V invoking operations of an ADT defines a concurrent history. Operations are not executed instantaneously, i.e., given an operation o ∈ Σ = A ∪ (A × B), we denote by e inv (o) the invocation event of operation o and by e rsp (o) the corresponding response event. In addition, we denote by e rsp (o) : x the returned value associated to the response event e rsp (o). In the following E represents the set of events and Λ is the function which associates events to the operations in Σ. Given two events (e, e ) ∈ E 2 we say that e → e in the process order if they are produced by the same process, e = e and e happens before e . Given two events e, e ∈ E, we say that e precedes e in operation order, denoted by e ≺ e , if e is the invocation of an operation occurred at time t and e is the response of another operation occurred at time t with t < t . Finally, for any couple of events (e, e ) ∈ E 2 with e = e , we say that e precedes e in program order, denoted by e e , if e → e or e ≺ e . These asymmetric event structures allow us to define a concurrent history H of an ADT T = A, B, Z, ξ 0 , τ, δ as a 6-tuple H = Σ, E, Λ, →, ≺, , formally defined as follows.

Definition 3.4. (Concurrent history H) The execution of a program that uses an abstract data type T = A, B, Z, ξ 0 , τ, δ defines a concurrent history H = Σ, E, Λ, →, ≺,

, where

• Σ = A ∪ (A × B) is a countable set of operations;
• E is a countable set of events that contains all the ADT operations invocations and all ADT operation response events;

• Λ : E → Σ is a function which associates events to the operations in Σ;

• →: is the process order, irreflexive order over the events of E. Two events (e, e ) ∈ E 2 are ordered by → if they are produced by the same process, e = e and e happens before e , that is denoted as e → e . If e and e are the invocation and response events of the same operation, then trivially e → e .

• ≺: is the operation order, irreflexive order over the events of E. For each couple (e, e ) ∈ E 2 , if e is the invocation of an operation occurred at time t and e is the response of another operation occurred at time t with t < t then e ≺ e ;

• : is the program order, irreflexive order over E, for each couple (e, e ) ∈ E 2 with e = e if e → e or e ≺ e then e e .

Consistency criterion

A consistency criterion characterizes which concurrent histories are admissible for a given abstract data type. It can be viewed as a function that associates a concurrent specification to abstract data types. Specifically, Definition 3.5. (Consistency criterion C) A consistency criterion is a function

C : T → P(H)
where T is the set of abstract data types, H is a set of histories and P(H) is the sets of parts of H.

Given a consistency criterion C, an algorithm A T implementing the ADT T is C-consistent with respect to criterion C if all the operations terminate and all the admissible executions are C-consistent, i.e., they belong to the set of histories C(T ).

BlockTree and Token oracle ADTs

In this section we present the BlockTree and the token Oracle ADTs along with consistency criteria.

BlockTree ADT

We formalize the data structure implemented by blockchain-like systems as a directed rooted tree bt = (V bt , E bt ) called BlockTree. Each vertex of the BlockTree is a block and any edge points backward to the root, called genesis block. By convention, the root of the BlockTree is denoted by b 0 . Two operations are provided: the append(b ) operation, which appends a new block b to the BlockTree, and the read() operation, which returns a sequence of blocks of the BlockTree. This sequence of blocks is called the blockchain and is selected according to function f (see below). Only blocks satisfying some validity predicate P ∈ P can be appended to the BlockTree. Predicate P is application dependent. Predicate P mainly abstracts the creation process of a block, which may fail (return false. false is denoted by ⊥) or successfully terminate (returns true. true is denoted by ). For instance, in Bitcoin, a block is considered valid if it can be connected to the current blockchain and does not contain double-spending transactions.

We represent by B a countable and non empty set of uniquely identified blocks and by B ⊆ B a countable and non empty set of uniquely identified valid blocks, i.e., ∀b ∈ B , P (b) = . By assumption b 0 ∈ B ; We also denote by BC a countable non empty set of blockchains, where a blockchain is a path from a leaf of bt to b 0 . A blockchain is denoted by bc. Finally, F is a countable non empty set of selection functions, f ∈ F : BT → BC; f (bt) selects a blockchain bc from the BlockTree bt (note that b 0 is not returned) and if bt = b 0 then f (b 0 ) = b 0 . This reflects for instance the longest chain or the heaviest chain used in some blockchain implementations. The selection function f and the predicate P are parameters of the ADT which are encoded in the state and do not change over the computation.

The following notations are used: {b 0 } f (bt) represents the concatenation of b 0 with the blockchain of bt; and {b 0 } f (bt) {b} represents the concatenation of b 0 with the blockchain of bt and a block b.

Sequential specification of the BlockTree

The sequential specification of the BlockTree is defined as follows.

Definition 4.1 (BlockTree ADT (BT -ADT )). The BlockTree Abstract Data Type is the 6-tuple BT-ADT=

A = {append(b h , b ), read() : b ∈ B}, B = BC ∪ { , ⊥}, Z = BT × F × P), ξ 0 = (b 0 , f ), τ, δ , where the transition function τ : Z × A → Z is defined by τ ((bt, f, P ), read()) = (bt, f, P ) τ ((bt, f, P ), append(b)) = ({b 0 } f (bt) {b}, f, P ) if b ∈ B (bt, f, P ) otherwise ξ 0 ξ 0 = { b0 , f, P } ξ 1 ξ 1 = { b0 b1 , f, P } append(b 1 ) : true if b 1 ∈ B append(b 3 ) : false if b 3 / ∈ B ξ 2 ξ 2 = { b0 b1 b2 , f, P } append(b 2 ) : true if b 2 ∈ B append(b 3 ) : false if b 3 / ∈ B read() : b 0 b 1 read() : b 0 b 1 b 2 Figure 1:
A possible path of the transition system defined by the BT-ADT.

and the output function

δ : Z × A → B is defined by δ((bt, f, P ), read()) = {b 0 } if bt = b 0 {b 0 } f (bt) otherwise δ((bt, f, P ), append(b)) = if b ∈ B ⊥ otherwise
The semantic of the read and the append operations directly depend on the selection function f ∈ F. In this work we let function f generic to suit the different blockchain implementations. In the same way, predicate P is let unspecified. The predicate P mainly abstracts the creation process of a block, which may fail or successfully terminate. This process will be further specified in Section 4.2.

Figure 1 illustrates an execution of the BT-ADT bt. Starting from the initial state ξ 0 , state ξ 1 is obtained by appending block b 1 to ξ 0 and state ξ 2 is obtained by appending block b 2 to ξ 1 . The read operation applied in state ξ 1 returns blockchain {b 0 } {b 1 }, and the read applied in state ξ 2 returns blockchain {b 0 } f (bt) {b 2 } = {b 0 } {b 1 } {b 2 }.

Concurrent specification of a BT-ADT and consistency criteria

The concurrent specification of the BT-ADT is the set of concurrent histories. A BT -ADT consistency criterion is a function that returns the set of concurrent histories admissible for a BlockTree abstract data type. We define two BT consistency criteria: BT Strong consistency and BT Eventual consistency. For ease of readability, we employ the following notations:

• E(a * , r * ) is an infinite set containing an infinite number of append() and read() invocation and response events;

• E(a, r * ) is an infinite set containing (i) a finite number of append() invocation and response events and (ii) an infinite number of read() invocation and response events;

• e inv (o) and e rsp (o) indicate respectively the invocation and response event of an operation o; and e rsp (r) : bc denotes the returned blockchain bc associated with the response event e rsp (r);

• score : BC → N denotes a monotonic increasing deterministic function that takes as input a blockchain bc and returns a natural number s as score of bc, which can be the height, the weight, etc. Informally we refer to such value as the score of a blockchain; by convention we refer to the score of the blockchain uniquely composed by the genesis block as s 0 , i.e. score({b 0 }) = s 0 . Increasing monotonicity means that score(bc {b}) > score(bc);

• mcps : BC × BC → N is a function that given two blockchains bc and bc returns the score of the maximal common prefix between bc and bc ;

• bc bc iff bc prefixes bc .

BlockTree Strong consistency.

Informally the BlockTree Strong consistency says that any two read() operations return blockchains b 1 and b 2 such that one is the prefix of the other, i.e., b 1 ⊆ b 2 or b 1 ⊆ b 2 . This is formalized with the following four properties. The Block validity property imposes that each block in a blockchain returned by a read() operation is valid (i.e., satisfies predicate P ) and has previously been inserted in the BlockTree with the append() operation. Formally, Definition 4.2 (Block validity).

∀e rsp (r) ∈ E, ∀b ∈ e rsp (r) : bc, b ∈ B ∧ ∃e inv (append(b)) ∈ E, e inv (append(b))
e rsp (r).

The Local monotonic read property states that, given the sequence of read() operations at the same process, the score of the returned blockchain never decreases; Formally, Finally, the Ever growing tree states that scores of returned blockchains eventually grow. More precisely, let s be the score of the blockchain returned by a read response event r in E(a * , r * ), then for each read() operation r, the set of read() operations r such that e rsp (r) e inv (r ) that do not return blockchains with a score greater than s is finite. Formally, Figure 2 shows a concurrent history H admissible by the BT Strong consistency criterion. In this example the score is the length of the blockchain and the selection function f selects the longest blockchain, and in case of equality, selects the largest based on the lexicographical order. For ease of readability, we do not depict the append() operation. We assume that the Block validity property is satisfied. The Local monotonic read property is easily verifiable as, for each couple of read blockchains, one prefixes the other. The first read() r operation, enclosed in a black rectangle, is taken as reference to check the consistency criterion (the criterion has to be iteratively verified for each read() operation). Let be the score of the blockchain returned by the first read operation r. We can identify two sets, enclosed in rectangles defined by different patterns: (i) the finite sets of read() operations such that the score associated to each blockchain returned is smaller than or equal to , and (ii) the infinite set of read() operations such that the score is greater than . We can iterate the same reasoning for each read() operation in H. Thus H satisfies the Ever growing tree property. In this scenario f selects the longest blockchain and the blockchain score is length .

BlockTree Eventual consistency.

The BlockTree (BT) Eventual Consistency criterion is a weaker version of the Strong Consistency criterion. Informally, the BT Eventual Consistency criterion says that eventually any two read() operations return blockchains that share the same prefix, which differs from the BT Strong Consistency criterion by the Eventual prefix property. The Eventual prefix property says that for each blockchain returned by a read() operation with s as score, then eventually all the read() operations will return blockchains sharing the same maximum common prefix at least up to s. Say differently, let H be a history with an infinite number of read() operations, and let s be the score of the blockchain returned by a read() operation r then, the set of read() operations r , such that e rsp (r) e inv (r ), that do not return blockchains sharing the same prefix at least up to s is finite. We formalise this notion as follows: Definition 4.7 (Eventual prefix property). Given a concurrent history H = Σ, E(a, r * ), Λ, → , ≺, of the system that uses a BT-ADT, we denote by s, for any read operation r ∈ Σ such that ∃e ∈ E(a, r * ), Λ(r) = e, the score of the returned blockchain, i.e., s = score(e rsp (r) : bc). We denote by E r the set of response events of read operations that occurred after r response, i.e., E r = {e ∈ E | ∃r ∈ Σ, r = read, e = e rsp (r ) ∧ e rsp (r) e rsp (r )}.

Then, H satisfies the Eventual prefix property if for all read() operations r ∈ Σ with score s,

|{(e rsp (r h ), e rsp (r k )) ∈ E 2 r |h = k, mcps(e rsp (r h ) : bc h , e rsp (r k ) : bc k ) < s}| < ∞
The Eventual prefix property captures the fact that two or more concurrent blockchains can co-exist in a finite interval of time, but that eventually all the participants adopts a same branch for each cut of the history. This cut of the history is defined by a read that picks up a blockchain with a given score.

We are now ready to formalize the the BlockTree Eventual Consistency criterion.

Definition 4.8 (BT Eventual Consistency (EC) criterion). A concurrent history H = Σ, E, Λ, →, ≺, of the system that uses a BT-ADT verifies the BT Eventual Consistency criterion if the Block validity, Local monotonic read, Ever growing tree, and the Eventual prefix properties hold.

Figure 3 shows a concurrent history that satisfies the Eventual prefix property but not the Strong prefix one. Strong Prefix is not satisfied as blockchain1 b 0 1 returned from the first read() at process j is not a prefix of blockchain b 0 2 4 returned from the first read at process i. Note that we adopt the same conventions as for the example depicted in Figure 2 regarding the score, length and append() operations. We assume that the Block validity property is satisfied. The Local monotonic read property is easily verifiable. In both Figures 3a and3b, the first read() r operation at i, enclosed in a black rectangle, is taken as reference to check the consistency criterion (the criterion has to be iteratively verified for each read() operation). Let be the score of the blockchain returned by r. In Figure 3b we can identify two sets, enclosed in rectangles defined by different patterns: (i) the finite set of read() operations sharing a maximum common prefix score (mcps) smaller than (the set to check for the satisfiability of the Eventual Prefix property), and (ii) the infinite set of read() operations such that for each couple of them bc, bc , mcps(bc, bc ) ≥ . We can iterate the same reasoning for each read() operation in H. Thus H satisfies the Eventual Prefix property. Figure 4 shows a history that does not satisfy any consistency criteria defined so far.

Relationships between Eventual Consistency (EC) and Strong Consistency (SC)

Let H EC and H SC be the set of histories satisfying respectively the EC and the SC consistency criteria. e inv (r ), score(e rsp (r ) : bc) > s}. The Strong prefix property guarantees that ∀e rsp (r), e rsp (r ) ∈ H, (e rsp (r) : bc e rsp (r) : bc ) ∨ (e rsp (r) : bc e rsp (r ) : bc ), thus in this infinite set, all the read() operations return blockchains sharing the same maximum prefix whose score is at least s + 1, which satisfies the Eventual prefix property. The Eventual Prefix property demands that ∀e rsp (r) ∈ E(a, r * ) with s = score(e rsp (r) : bc) there is an infinite set defined as {(e rsp (r h ), e rsp (r k )) ∈ E 2 r |h = k, mpcs(e rsp (r h ) : bc h , e rsp (r k ) : bc k ) ≥ s} where E r denotes the set of response events of read operations that occurred after r response. To conclude the proof we need to find a H ∈ H EC and H ∈ H SC . Any history H in which at least two read() operations return a blockchain sharing the same prefix but diverging in their suffix violate the Strong prefix property, which concludes the proof. Let us remark that the BlockTree allows at any time to create a new branch in the tree, which is called a fork in the blockchain literature. Note that that histories with no append operations are trivially admitted.

In the following we will introduce a new abstract data type called Token Oracle, which when combined with the BlockTree will help in (i) validating blocks and (ii) controlling the presence of forks and their number, if any. We will first formally introduce the Token Oracle in Section 4.2, then refine the BlockTree with the Token oracle in Section 4.3, and finally study the relationships between the different refinements in Section 4.4.

Token Oracle Θ ADT

We now formalize the Token Oracle Θ to capture the creation of blocks in the BlockTree structure. The block creation process requires that each new block must be closely related to an already existing valid block in the BlockTree structure. We abstract this implementationdependent process by assuming that a process will obtain the right to chain a new block b to b h ∈ B , if it successfully gains a token tkn h from the token oracle Θ. Once obtained, the proposed block b is considered as valid, and will be denoted by b tkn h . By construction b tkn h ∈ B . In the following, in order to be as much general as possible, we model blocks as objects. More formally, when a process wants to access some valid object obj h , i.e., P (obj q ) = it invokes the getToken(obj h , obj ) operation with object obj from set O = {obj 1 , obj 2 , . . . }. If getToken(obj h , obj ) operation is successful, it returns the valid object obj tkn h such that tkn h is the token required to access valid object obj h . The set of valid objects is denoted by O , i.e., ∀obj q ∈ O , P (obj q ) = . We say that a valid object is generated each time it is successfully returned by a getToken(obj h , obj ) operation and it is consumed when the oracle grants the right to associate this valid object obj tkn h to obj h . In the following, once an object is valid, if it is clear from the context, we will not explicit the token tkn with makes the object valid.

A valid object obj tkn h is consumed through the consumeToken(obj tkn h ) operation. No more than k valid objects obj tkn h 1 , . . . , obj tkn h j , 1 ≤ j ≤ k, can be consumed for obj h , where k is a parameter of the token oracle. The side-effect of the consumeToken(obj tkn h ) on the state of the token oracle is the insertion of the valid object obj tkn h in a set related to obj h as long as the cardinality of such set is less than or equal to k.

We specify two token oracles, which differ in the way tokens are managed. The first oracle, called prodigal and denoted by Θ P , has no upper bound on the number of tokens consumed for an object, while the second oracle Θ F , called frugal, and denoted by Θ F , guarantees that no more than k token can be consumed for each object.

The prodigal oracle Θ P when combined with the BlockTree abstract data type will only help in validating blocks, while the frugal oracle Θ F manages tokens in a more controlled way to guarantee that no more than k forks can occur on a given block.

Θ P -ADT and Θ F -ADT definitions

For both oracles, when getToken(obj h , obj ) operation is invoked, the oracle provides a valid object with a certain probability p α i > 0 where α i is a "merit" parameter characterizing the invoking process i. 2 Note that the oracle knows α i of the invoking process i, which might be unknown to the process itself. For each merit α i , the state of the token oracle embeds an infinite tape where each cell of the tape contains either tkn or ⊥. Since each tape is identified by a specific α i and p α i , we assume that each tape contains a pseudorandom sequence of values in {tkn, ⊥} depending on α i . 3 When a getToken(obj h , obj ) operation is invoked by a process with merit α i , the oracle pops the first cell from the tape associated to α i , and a valid obeject is provided to the process if that cell contains tkn. Both oracles enjoy an infinite array of sets, one set for each valid object obj h , which is populated each time a valid object obj is consumed. When the set cardinality reaches k then no more tokens can be consumed for that object. For the sake of generality, Θ P is defined as Θ F with k = ∞ while for Θ F a predetermined k ∈ N is specified. Hence, the state of the token oracle contains (i) the infinite array K of sets (one per valid object) of elements in O , (ii) infinite tapes one for each possible merit, and (iii) the branching parameter k. Figure 5 illustrates the state of a token oracle.

Formally we provide the following definitions. • O = {obj 1 , obj 2 , . . . }, infinite set of generic objects, each of them associated to an unique identifier i, i ∈ N;

{} 1 {} 2 {} 3 {} 4 . . . K obj 1 obj 2 obj 3 obj 4 . . . tkn ⊥ ⊥ tkn ⊥ ⊥ ⊥ . . . tape α 2 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ tkn . . . tape α 1 . . .
• O ⊆ O, the subset of objects valid with respect to predicate P , i.e. ∀obj i ∈ O , P (obj i ) = ;

• T = {tkn 1 , tkn 2 , . . . } infinite set of tokens;

• A = {α 1 , α 2 , . . . } an infinite set of rational values;

• M is a countable not empty set of mapping functions m(α i ) that generate an infinite pseudo random tape tape α i such that the probability to have in a cell the string tkn is related to a specific α i , m ∈ M : A → {tkn, ⊥} * ;

• K is an infinite array domain, such that each element K ∈ K is a infinite array of sets (one per valid object) of elements in O . In particular, the set related to each object

o i ∈ O is accessible at K[i].
Each set is initialized as empty and can be fulfilled with at most k elements, where k ∈ N is a parameter of the token oracle ADT;

• pop : {tkn, ⊥} * → {tkn, ⊥} * , pop(a • w) = w;

• head : {tkn, ⊥} * → {tkn, ⊥} * , head(a • w) = a; • δ(({tape α 1 , . . . , tape α i , . . . }, K, k), getToken(obj h , obj )) = obj tkn h : obj tkn h ∈ O , tkn h ∈ T, if head(tape α i ) = tkn with α i the merit of the invoking process; ⊥ otherwise;

• add : {K} × O → {K}, add(K, obj tkn h ) = K : K[h] = K[h] ∪ {obj tkn h } if |K[h]| < k; K[h] = K[h] otherwise; • get : {K} × N → N, get(K, h) = K[h]; Definition 4.9. (Θ F -ADT). The Θ F Abstract Data type is the 6-tuple Θ F -ADT = A= {getToken(obj h , obj ), consumeToken(obj tkn h ) : obj h , obj tkn h ∈ O , obj ∈ O, tkn h ∈ T}, B= O ∪ Boolean, Z= m(A) * × K × k ∪ {pop,
• δ(({tape α 1 , . . . , tape α i , . . . }, K, k), consumeToken(obj tkn h )) = get(K, h).

Definition 4.10. (Θ P -ADT Definition). The Θ P Abstract Data type is defined as the Θ F -ADT with k = ∞.

We consider oracles that are linearizable (with respect to their sequential specification): they behave as if all operations, including concurrent ones, are applied sequentially, so that each operation appears to take effect instantaneously as some point between their invocation and their response.

In Figure 6 is depicted a possible path of the transition system defined by Θ F,k -ADT and Θ P -ADT. When a process with merit ) is invoked, the oracle checks if the cardinality of the set in K [START_REF] Abraham | The blockchain consensus layer and BFT[END_REF] is strictly smaller than k, and if the affirmative inserts b tkn 1 k in K [START_REF] Abraham | The blockchain consensus layer and BFT[END_REF]. In any cases, consumeToken() returns the content of K [START_REF] Abraham | The blockchain consensus layer and BFT[END_REF], in this case b tkn 1 k . It follows that a process that gets a valid block for some block b h but is not allowed to consume it, is anyway notified with the set of valid blocks that saturated K[h].

We consider oracles that are linearizable (with respect to their sequential specification): they behave as if all operations, including concurrent ones, are applied sequentially, so that each operation appears to take effect instantaneously as some point between their invocation and their response.

BT-ADT augmented with Θ Oracles

We augment the BT-ADT with Θ oracles and we analyze the histories generated by their combination. Specifically, we define a refinement of the append(b ) operation of the BT-ADT with the oracle operations as follows: the append(b ) operation triggers the getToken(b h ←last block(f (bt)), b ) operation as long as it returns a valid block b tkn h , and once obtained, the valid block might be consumed, and in any cases the append(b ) operation terminates. If less than k valid blocks have already been consumed for b h , the valid block is consumed i.e. block b tkn h is appended to the block h in the blockchain f (bt) (i.e., {b 0 } f (bt)| h {b }) and the append(b ) operation returns true, otherwise false. Let us define the following auxiliary function:

• evaluate: B × B Θ → bool. evaluate(b, δ b • δ * a )= true if (∃h : b tkn h ∈ δ b ∧ (∃X : b tkn h ∈ X ∧ X ∈ δ * a )); false otherwise. Definition 4.11. [R(BT -ADT, Θ F ) refinement] Given the BT-ADT= A, B, Z, ξ 0 , τ, δ , and the Θ F -ADT =(A Θ , B Θ , Z Θ , ξ Θ 0 , τ Θ , δ Θ ), we have R(BT -ADT, Θ F )= A = A ∪ A Θ , B = B ∪ B Θ , Z = Z ∪ Z Θ , ξ 0 = ξ 0 ∪ ξ Θ 0 , τ , δ
, where the transition function τ : Z × A → Z is defined by

• τ a = τ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), getToken(b h ← last block(bt), b )) = ({tape α 1 , . . . , pop(tape α i ), . . . }, K, k, bt, f, P ); • τ b = τ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), consumeToken(b tkn h )) = ({tape α 1 , . . . , tape α i , . . . }, add(K, b tkn h ), k, {b 0 } f (bt)| h {b }, f, P ) if b tkn h ∈ get(K, l) ; ({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ) otherwise; • τ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), append(b)) = τ b • τ * a
where τ b • τ * a is the repeated application of τ a until δ a (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), getToken(b h ← last block(bt), b )) = b tkn h concatenated with the τ b application;

• τ ({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), read() = bt. and the output function δ : Z × A → B is defined by:

• δ a = δ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), getToken(b h ← last block(bt), b )) = b tkn h : b tkn h ∈ B , tkn h ∈ T, if head(tape α i ) =
tkn with α i the merit of the invoking process; ⊥ otherwise;

• δ b = δ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), consumeToken(obj tkn h )) = get(K, h); • δ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), append(b)) = evaluate(b, δ b • δ * a ), where δ b • δ * a is the repeated application of δ a until δ a (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), getToken(b h ← last block(bt), b)) = b tkn h concatenated with the δ b application; • δ (({tape α 1 , . . . , tape α i , . . . }, K, k, bt, f, P ), read()) = {b 0 } f (bt);
• δ (({tape α 1 , . . . , tape α i , . . . }, K, kbt 0 , f, P ), read()) = b 0 .

Definition 4.12 (R(BT -ADT, Θ P ) refinement). Same definition as the R(BT -ADT, Θ F ) refinement. erating concurrent histories that satisfy the SC and the EC consistency criteria. When augmented with token oracles we get the following four typologies, where for the frugal oracle we explicit the value of k: R(BT-ADT SC , Θ F,k ), R(BT-ADT SC , Θ P ), R(BT-ADT EC , Θ P ), R(BT-ADT EC , Θ F,k ). We aim at studying the relationships among the different refinements.

R(BT-ADT

SC , Θ F,k=1 ) R(BT-ADT EC , Θ F,k>1 ) R(BT-ADT SC , Θ P ) R(BT-ADT SC , Θ F,k>1 ) R(BT-ADT EC , Θ P )
Let ĤR(BT-ADT,Θ F,k ) be the set of concurrent histories generated by a BT-ADT enriched with Θ F,k -ADT and ĤR(BT-ADT,Θ P ) be the set of concurrent histories generated by a BT-ADT enriched with Θ P -ADT. Without loss of generality, we consider only the set of histories from which have been purged unsuccessful append() response events (i.e., such that the returned value is ⊥).

Theorem 4.3. ĤR(BT-ADT,Θ F ) ⊆ ĤR(BT-ADT,Θ P ) .

Proof. The proof follows from Theorem 4.2 considering that R(BT, Θ P ) can generate histories with an infinite number of append() operations that successfully terminate while R(BT, Θ F ) can generate history with at most k append() operations that successfully terminate.

Theorem 4.4. If k 1 ≤ k 2 then ĤR(BT-ADT,Θ F,k 1 ) ⊆ ĤR(BT-ADT,Θ F,k 2 ) .
Proof. The proof follows from Theorem 4.2 applying the same reasoning as for the proof of Theorem 4.3 with

k 1 ≤ k 2 .
Finally, from Theorem 4.1 the next corollary follows. 5 Implementing BT-ADTs

Implementability in the shared memory model

We now consider a system made of n processes such that up to f of them are faulty (stop prematurely by crashing), f < n. Non faulty processes are said correct. Processes communicate through atomic registers.

Frugal oracle Θ F,k=1 is at least as strong as Consensus

We show that there exists a wait-free implementation of Consensus [START_REF] Lamport | The byzantine generals problem[END_REF] by R(BT-ADT, Θ F,k=1 ). Note that similarly to [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF], we extend the validity property of Consensus to fit the blockchain setting. Specifically, we have Definition 5.1 (Consensus C).

• Validity A value is valid if it satisfies the predefined predicate P .

• Termination. Every correct process eventually decides some value, and that value must be valid.

• Integrity. No correct process decides twice.

• Agreement. If there is a correct process that decides value b, then eventually all the correct processes decide b.

We first show that there exists a wait-free implementation of the Compare&Swap() object by R(BT-ADT, Θ F,k=1 ) assuming that blocks are valid. Doing this implies that, under the assumption that blocks are valid, R(BT-ADT, Θ F,k=1 ) has the same Consensus number as Compare&Swap(), i.e., ∞ (see [START_REF] Herlihy | Wait-free synchronization[END_REF]). We then show that there is a wait-free implementation of Consensus C by R(BT-ADT, Θ F,k=1 ) for any block b ∈ B (i.e., b may not be valid). Doing this will imply that R(BT-ADT, Θ F,k=1 ) has the same Consensus number as Consensus(), i.e., ∞.

Recall that Compare&Swap() takes three parameters as input, the register, the old value and the new value. If the value in register is the same as old value then the new value is stored in register and in any case the operation returns the value that was in register at the beginning of the operation.

Figure 9 proposes an algorithm that reduces CAS object to Θ F,k=1 object. Proof. The proof simply follows by construction. Let us consider the algorithm in Figure 9. When the Compare&Swap() operation is invoked, if f irst is equal to b tkn h (Line 3) then the Compare&Swap returns the value of K at the beginning of the operation, which is {}, otherwise it returns the value in f irst that is value written by another process.

(1) consumeToken(obj tkn h )

(2) proposeValue({obj tkn h })

(3) wait until obj tkn h ∈ LearntValue()

(4) K[h] = K[h]∪ LearntValue() (5) return K[h];
Figure 11: Reduction of the prodigal oracle to Generalized Lattice Agreement present a reduction of the prodigal oracle Θ P to Generalized Lattice Agreement (GLA) [START_REF] Falerio | Generalized lattice agreement[END_REF].

We will first recall the properties of GLA, a version of lattice agreement generalized to a possibly infinite sequence of input values.

Definition 5.2 (GLA Problem [START_REF] Falerio | Generalized lattice agreement[END_REF]). Let L be a join semi-lattice with a partial order . Each process may propose an input value belonging to the lattice at any point in time. There is no bound on the number of input values a process may propose. Let v x i denote the x-th input value proposed by a process p i . The objective is for each process p i to learn a sequence of output values w y i that satisfy the following conditions:

1. Validity. Any learnt value w y i is a join of some set of input values.

2.

Stability. The value learnt by any process p i increases monotonically : x < y ⇒ w x i w y i .

3. Consistency. Any two values w x i and w y j learnt by any two processes p i and p j are comparable.

Liveness. Every value v x

i proposed by a correct process p i is eventually included in some learnt value w y j of every correct process p j , i.e. v x i w y j

Reduction of the prodigal oracle to Generalized Lattice Agreement

In order to show the reduction of the prodigal oracle to GLA, we consider a lattice for each possible object obj h a process wants to append its own object to. Intuitively, in the context of the BT-ADT, the object obj h is a vertex of a tree that maps to a lattice whose input values are subsets of the vertexś children. In order to formally define the input values of the lattice, let us recall that a consume token operation invoked to chain an object obj to a given object obj h , i.e., consumeToken(obj tkn h ), returns a set of objects that includes the chained object obj tkn h . In this context, the lattice input values belong then to the objects power set, where the greatest lower bound is the empty set.

Figure 11 shows an implementation of consumeToken by GLA, where the process executes proposeValue({obj tkn h }) of GLA, taking the singleton set {obj tkn h } to be a newly proposed value. The consume token returns a set that reflects all the objects in the learnt set, which includes the proposed object.

Theorem 5.3. Θ P Oracle is not stronger than Generalized Lattice Agreement.

Proof. (Sketch)

The proof follows from the implementation in Figure 11. Let us recall that the oracle must behave as an atomic object, which means that we need to show that the oracle is linearizable through GLA. GLA proposed values in our implementation are sets, where each proposed value is a singleton set containing a uniquely identified object. The join of any two proposed values is the union of the proposed singleton sets. Any learnt set is the union of some proposed sets. Any two learnt sets are comparable through the inclusion operator. The first step is to show that the order of non-overlapping consumeToken operations is preserved: if a process p i completes a consumeToken ct 1 operation before another process p j invokes another ct 2 operation, then we must ensure that ct 1 occurs before ct 2 in the linearization order, i.e. the effect of ct 1 is visible to ct 2 . Note that from the pseudo-code, the only values included in K[h] are learnt values, i.e. a join of some proposed values by the GLA Validity and from Line 2. Moreover, from Line 3 each process waits for its own proposed set to be learnt before the consumeToken completes. This means that the proposed set set 1 by ct 1 is learnt and included in K[h], before ct 2 is invoked. Since the learnt value set 1 through ct 1 must now be comparable to the learnt set set 2 through ct 2 , this implies that the learnt set set 2 through ct 2 must also include set 1 . K[h] will then include set 1 , i.e. ct 2 has seen the effect of ct 1 . The second step is to show that any two concurrent operations ct 1 and ct 2 can be linearized. By Consistency, even in this case the learnt values must be comparable, either set 1 is included in set 2 or the other way round. In both cases the effect of one operation is visible to the other one, and then they can be linearized. The last step is to show the the implementation is wait-free. Wait-freedom is ensured by the Liveness property of GLA that ensures that the execution time of Line 3 is finite.

Implementability in a message-passing system model

In this section we are interested in distributed message-passing implementations of BT-ADTs. In the following, we will present (i) the necessity of a light form of reliable broadcast to implement BT Eventual consistency, (ii) refinement of BTs with Oracles that are not implementable in a message-passing system and (iii) the mapping of current existing implementations with our abstract data types.

To this end, we consider a message-passing system composed of an arbitrarily large but finite set of n processes, such that a subset of them can fail by exhibiting Byzantine failures, that is deviates arbitrarily from the distributed protocol P it should execute. A non-faulty process is said correct. Processes communicate by exchanging messages over communication channels that can be asynchronous or synchronous (see [START_REF] Cachin | Introduction to Reliable and Secure Distributed Programming[END_REF]). We will specify whenever necessary the synchrony assumptions of the channels. By default we consider asynchronous channels.

The BlockTree is considered as a shared object replicated at each process. Let bt i be the local copy of the BlockTree maintained at process i. To maintain the replicated object we consider histories made of events related to the read and append operations on the shared object, i.e. the send and receive operations for process communications and the update operation for BlockTree replica updates. We also use subscript i to indicate that the operation occurred at process i: update i (b g , b ) indicates that i inserts its locally generated valid block b in bt i with b g as a predecessor. Updates are communicated through send and receive operations: an update related to a block b generated on a process p i , which is sent through the send i (b g , b ) operation, and which is received through the receive j (b g , b ) operation, takes effect on the local replica bt j of p j with the update j (b g , b ) operation.

In the remaining of this work we consider implementations of BT-ADT in a Byzantine failure model where the set of events E is restricted to a countable set of events that contains (i) all the BT-ADT read() operations invocation events by the correct processes, (ii) all BT-ADT read() operations response events at the correct processes, (iii) all append(b) operations invocation events such that b satisfies predicate P and, finally (iv) send, receive and update events generated at correct processes. Note that the Oracle-ADT is by construction agnostic to failures.

Necessity of reliable communication

We define the properties on the communication primitive that each history H generated by a BT-ADT satisfying the Eventual Prefix Property must satisfy. We need to first introduce the following definition: Definition 5.3 (Update agreement). A concurrent history H = Σ, E, Λ, →, ≺, generated by a BT-ADT satisfies the update agreement property if properties R1, R2 and R3 hold.

• R1. ∀update i (b g , b ) ∈ H, ∃send i (b g , b ) ∈ H; • R2. ∀update i (b g , b ) ∈ H, ∃receive i (b g , b ) ∈ H such that receive i (b g , b ) → update i (b g , b ); • R3. ∀update i (b g , b ) ∈ H, ∃receive k (b g , b ) ∈ H, ∀k.
Theorem 5.4. The update agreement property is necessary to construct concurrent histories H = Σ, E, Λ, →, ≺, generated by a BT-ADT that satisfy the BT Eventual Consistency criterion.

Proof. The intuition of the proof is that to meet BT Eventual Consistency all the processes must have the same view of BlockTree eventually. In fact missing an update on the branch that will be eventually selected (which cannot be a-priori-known) would imply that the prefix (which will be arbitrarily long) for the process that missed the update will diverge forever. For space reason the proof of the theorem can be found in the supplementary materials.

We can now present the Light Reliable Communication (LRC) primitive. Definition 5.4 (Light Reliable Communication (LRC)). A concurrent history H satisfies the properties of the LRC abstraction if and only if:

• (Validity): ∀send i (b, b i ) ∈ H, ∃receive i (b, b i ) ∈ H; • (Agreement): ∀receive i (b, b j ) ∈ H, ∀k∃receive k (b, b i ) ∈ H
From Theorem 5.4, it is straightforward to show that LRC is necessary to implement BT Eventual consistency (by using arguments from [START_REF] Cachin | Introduction to Reliable and Secure Distributed Programming[END_REF]). The proof of the necessity is based on the Validity and Agreement for R1, R2 and R3. The interested reader can refer to the supplementary materials for the proof.

Theorem 5.5. The LRC primitive is necessary for any BT-ADT implementation that generates concurrent histories which satisfies the BT Eventual Consistency criterion. By Theorem 4.1, the results trivially hold for the BT Strong consistency criterion.

Impossibility of BT Strong Consistency with forks

The following theorem states that BT Strong consistency cannot be implemented if forks can occur. Intuitively the proof is based on showing a scenario in which two concurrent updates b i and b j are issued, linked to a same block b and two reads at two different processes read b b i and b b j , violating the Strong prefix property. Observation. Following our Oracle based abstraction (Section 4.3) we assume by definition that the synchronization on the block to append is oracle side and takes place during the append operation. It follows that when an append operation occurs and a correct process updates its local blocktree then it cannot use anything weaker than the LRC communication abstraction.

Theorem 5.6. There does not exist an implementation of R(BT-ADT SC , Θ) with Θ = Θ F,k=1 that uses a LRC primitive and generates histories satisfying the BT Strong consistency.

The non-implementability of refinement R(BT-ADT SC , Θ P ) and R(BT-ADT SC , Θ F,k>1 ) is a direct implication of the theorem, whose effect is reported in gray in Figure 8.

From Theorem 5.6 the next Corollary follows.

Corollary 5.6.1. Θ F,k=1 is necessary for any implementation of any R(BT-ADT SC , Θ) that generates histories satisfying the BT Strong consistency.

Thanks to Theorem 5.2 the next Corollary also follows.

Corollary 5.6.2. Consensus is necessary for any implementation of a BT-ADT that generates histories satisfying the BT Strong consistency.

Mapping with existing Blockchain implementations

We complete this work by illustrating the mapping in the following table between different existing systems and the specifications and abstractions presented in this paper. Interestingly, the mapping shows that all the proposed abstractions are implemented (even though in a probabilistic way in some case), and that the only two refinements used are R(BT -ADT SC , Θ F,k=1 ) and R(BT -ADT EC , Θ P ). In the following we discuss Bitcoin and Redbelly, an interested reader can find the discussions for the other systems in the supplementary materials.

Table 1: Mapping of some existing systems.

Refinement Bitcoin [START_REF] Nakamoto | Bitcoin: A Peer-to-Peer Electronic Cash System[END_REF] R(BT -ADT EC , Θ P ) EC w.h.p Ethereum [START_REF] Wood | Ethereum: A secure decentralised generalised transaction ledger[END_REF] R(BT -ADT EC , Θ P ) EC w.h.p Algorand [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF] R(BT -ADT SC , Θ F,k=1 ) SC w.h.p ByzCoin [START_REF] Kokoris-Kogias | Enhancing bitcoin security and performance with strong consistency via collective signing[END_REF] R(BT -ADT SC , Θ F,k=1 ) PeerCensus [START_REF] Decker | Bitcoin meets strong consistency[END_REF] R(BT -ADT SC , Θ F,k=1 ) Redbelly [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF] R(BT -ADT SC , Θ F,k=1 ) Hyperledger [3] R(BT -ADT SC , Θ F,k=1 )

Bitcoin

In Bitcoin [START_REF] Nakamoto | Bitcoin: A Peer-to-Peer Electronic Cash System[END_REF] each process p ∈ V is allowed to read the BlockTree and append blocks to the BlockTree. Processes are characterized by their computational power represented by α p , normalized as p∈V α p = 1. Processes communicate through reliable FIFO authenticated channels, which models a partially synchronous setting [START_REF] Dwork | Consensus in presence of partial synchrony[END_REF]. Valid blocks are flooded in the system. The getToken operation is implemented by a proof-of-work mechanism. The con-sumeToken operation returns true for all valid blocks, thus there is no bounds on the number of consumed tokens. Thus Bitcoin implements a Prodigal Oracle. The selection function f selects the blockchain which has required the most computational work, guaranteeing that concurrent blocks can only refer to the most recently appended blocks of the blockchain returned by a read() operation. Garay and al [START_REF] Oswald | The Bitcoin Backbone Protocol: Analysis and Applications[END_REF] have shown, under a synchronous environment assumption, that Bitcoin ensures Eventual consistency criteria with high probability. 4

Red Belly

Red Belly [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF] is a consortium blockchain, meaning that any process p ∈ V is allowed to read the BlockTree but a predefined subset M ⊆ V of processes are allowed to append blocks. Each process p ∈ M has a merit parameter set to α p = 1/|M | while each process p ∈ V \ M has a merit parameter α p = 0. Each process p ∈ M can invoke the getToken operation with their new block and will receive a token. The consumeToken operation, implemented by a Byzantine consensus algorithm run by all the processes in V , returns true for the uniquely decided block. Thus Red Belly BlockTree contains a unique blockchain, meaning that the selection function f is the trivial projection function from BT → BC which associates to the BT-ADT its unique existing chain of the BlockTree. As a consequence Red Belly relies on a Frugal Oracle with k = 1, and by the properties of Byzantine agreement implements a strongly consistent BlockTree (see Theorem 3 [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF]).

Definition 4 . 3 (

 43 Local monotonic read).∀e rsp (r), e rsp (r ) ∈ E 2 , if e rsp (r) → e rsp (r ), then score(e rsp (r) : bc) ≤ score(e rsp (r ) : bc ).The Strong prefix property says that for each pair of read operations, one of the returned blockchains is a prefix of the other returned one. Formally, Definition 4.4 (Strong prefix). ∀e rsp (r), e rsp (r ) ∈ E 2 , (e rsp (r ) : bc e rsp (r) : bc) ∨ (e rsp (r) : bc e rsp (r ) : bc ).

Definition 4 . 5 (

 45 Ever growing tree). ∀e rsp (r) ∈ E(a * , r * ), s = score(e rsp (r) : bc) then |{e inv (r ) ∈ E | e rsp (r) e inv (r ), score(e rsp (r ) : bc ) ≤ s}| < ∞.

Definition 4 . 6 (

 46 BT Strong Consistency (SC) criterion). A concurrent historyH = Σ, E, Λ, → , ≺,of the system that uses a BT-ADT verifies the BT Strong Consistency criterion if the Block validity, Local monotonic read, Strong prefix and the Ever growing tree properties hold.

Figure 2 :

 2 Figure 2: A concurrent history that satisfies the BlockTree (BT) Strong consistency criterion.In this scenario f selects the longest blockchain and the blockchain score is length .

  bc score ≤ set with each bc score > (a) Sets for the Ever growing tree property. mcps < set with blockchains mcps ≥ (b) Sets for the Eventual prefix property.

Figure 3 :

 3 Figure3: A concurrent history that satisfies the Eventual BT consistency criterion. In this scenario function f selects the longest blockchain and the blockchain score is the length . In both cases (case (a) and case (b)) the concurrent history is the same but different sets are outlined.

  bc score ≤ set with each bc score > (a) Sets for the Ever growing tree property. mcps < (b) Sets for the Eventual prefix property.

Figure 4 :

 4 Figure4: A concurrent history that does not satisfy any BT consistency criteria. In this scenario function f selects the longest blockchain and the blockchain score is the length .

Figure 5 :

 5 Figure5: The Θ F abstract state. The K set, initialized to ∅ and, the infinite set of infinite tapes, one for each merit α i in A.

1 , b k ) : b tkn 1 k 2 ξ 2 tkn 1 k) : {b tkn 1 k}Figure 6 :

 1122116 Figure 6: A possible path of the transition system defined by the Θ F and Θ F,k -ADTs.

  α 1 invokes getToken(b 1 , b k ), with b 1 the leaf of f (bt)), the first cell of tape α 1 is popped, and if it contains a token, then getToken(b 1 , b k ) returns a valid block b tkn 1 k . Afterwards, when consumeToken(b tkn 1 k

Figure 8 :

 8 Figure 8: R(BT-ADT, Θ) Hierarchy. In gray we anticipate the combinations impossible in a message-passing system due to Theorem 5.6.

Corollary 4 . 4 . 1 .

 441 Ĥ(R(BT-ADT SC ,Θ) ⊆ ĤR(BT-ADT EC ,Θ) . Combining Theorem 4.1 and Theorem 4.3 we obtain the hierarchy depicted in Figure 8. The arrows A → B in the figure indicate that the set of histories in A are included in the set of histories in B according to Theorems and Lemmas presented in Section 5.

Theorem 5 . 1 .

 51 If input values are in B then there exists an implementation of CAS by Θ F,k=1 .

  head, add, get}, ξ 0 , τ, δ , where the transition function τ : Z × A → Z is defined by • τ (({tape α 1 , . . . , tape α i , . . . }, K, k), getToken(obj h , obj )) = ({tape α 1 , . . . , pop(tape α i ), . . . }, K, k) with α i the merit of the invoking process;

• τ (({tape α 1 , . . . , tape α i , . . . }, K, k), consumeToken(obj tkn h )) = ({tape α 1 , . . . , tape α i , . . . }, add(K, obj tkn h ), k).

For ease of readability we extend the notation b i b j to represent concatenated blocks in a blockchain.

The merit parameter can reflect for instance the hashing power of the invoking process.

We assume a pseudorandom sequence mostly indistinguishable from a Bernoulli sequence consisting of a finite or infinite number of independent random variables X1, X2, X3, . . . such that (i) for each k, the value of X k is either tkn or ⊥; and (ii) ∀X k the probability that X k = tkn is p αi .

The same conclusion applies as well for the FruitChain protocol[START_REF] Pass | Fruitchains: A fair blockchain[END_REF], which proposes a protocol similar to BitCoin except for the rewarding mechanism.

Conclusions and Future Work

The paper presented a formal specification of blockchains and derived interesting conclusions on their implementability. Let us note that the presented work is intended to provide the groundwork for the construction of a sound hierarchy of blockchain abstractions and correct implementations. We believe that the presented results are also of practical interests since our oracle construction not only reflects the design of many current implementations, but will help designers in choosing the oracle they want to implement with a clear semantics and inherent trade-offs in mind. Future work will focus on several open issues, such as the solvability of Eventual Prefix in message-passing, the synchronization power of other oracle models, and fairness properties for oracles.

) : Proof. We prove the theorem by considering the defined refinement (Definition 4.11) where (i) there are a infinite number of getToken() invocations for object obj and (ii) given a valid block as input parameter, the consumeToken() operation successfully terminates if it has been invoked less than k times for the same token. From the properties of the pseudo random sequences of tapes, if there are an infinite number of getToken() invocations for object obj then there exists at least one response for which getToken() operation returns a token t, which, when passed as input of the consumeToken() operation it successfully terminates if at most k -1 tokens t have been already consumed.

Let us notice, the Θ F -ADT guarantees by construction the safety property (Theorem 4.2). Liveness properties (i.e., the Termination) for Θ F -ADT and Θ P -ADT depend on the communication model and failure model in which those are implemented.

Hierarchy

We propose a hierarchy between BT-ADTs augmented with token oracle ADTs. We use the following notation: BT-ADT SC and BT-ADT EC to refer respectively to BT-ADT gen-

then previous value = {}; [START_REF] Cachin | Introduction to Reliable and Secure Distributed Programming[END_REF] else previous value = f irst; (6) endIf (7) return previous value; Figure 10 describes a simple implementation of Consensus by Θ F,k=1 . When a process p invokes procedure Consensus with the block b h to which p wishes to append its block b, it first sets its proposal (Line 1), and then loops invoking the getToken(b h , proposal) operation until a valid block is returned (Lines 3-4). Once process p obtain a valid block, it invokes the consumeToken() operation with this valid block as a parameter. The consumeToken() returns the unique valid block for level level (Line 5). Note that this unique valid block is the one of the first process that invoked the consumeToken() operation. Thus the decision value is the valid block of the first process that invoked the consumeToken() operation (see Line 5), and thus it is the same for all the processes. Theorem 5.2. Θ F,k=1 Oracle has Consensus number ∞.

Proof. The proof proceeds by construction. Let us consider the implementation in Figure 10. All correct processes performing the Consensus are looping on the getToken(b h , proposal) operation. From the properties of the pseudo random sequences of tapes, if there are an infinite number of getToken() invocations for an block b h then eventually the getToken() operation returns a valid block proposal tkn h . Thus, all correct processes eventually invoke the consumeToken(proposal tkn h ) operation with a valid proposal. Since all the processes invoke such operation with valid blocks we can apply Theorem 5.1, which concludes the proof considering that CAS has Consensus number ∞ ([14]).

5.1.2

The prodigal oracle Θ P is not stronger than Generalized Lattice Agreement

In this section we present a reduction of the prodigal oracle Θ P to Generalized Lattice Agreement (GLA) [START_REF] Falerio | Generalized lattice agreement[END_REF]. We will first recall the properties of GLA, a version of lattice agreement generalized to a possibly infinite sequence of input values. In this section we


INTRODUCTION

Sandwich structures are widely used for many different applications since they offer exceptional benefits, providing a high bending stiffness with a very low weight. In aeronautics, sandwich panels are commonly made of Nomex honeycomb, and therefore this core has been studied for decades. Concerning the literature, most of the investigations on honeycomb cores are focused on the compression properties of the structure, for energy absorption applications or impacts on sandwich panels.

In the other hand, there are far fewer studies concerning the understanding of the shear nonlinear behavior of the honeycomb [START_REF] Seemann | Numerical Modeling of Nomex Honeycomb Sandwich Cores at Meso-Scale Level[END_REF], this can be considered a major drawback, knowing that it's the core who absorbs most of the shear components when a bending force is applied.

To help fill this gap, this work focuses on to study the shear behavior of the honeycomb structure. Several experimental tests are conducted using different boundary conditions to observe the buckling of the cells. This helps to understand the causes of the phenomenological stages that appear when the honeycomb structure is submitted to shear loads.

Finally, a numerical approach is used to simulate the honeycomb response to be able to see on the interior cell walls and to better understand this phenomenon.

EXPERIMENTAL STUDY Testing with double lap specimens

The first part of this research consisted into test 12 double lap specimens to determine the shear response of the honeycomb core; 6 specimens oriented in the W and other 6 oriented in the L direction. Of the 6 specimens, 3 were submitted to a continuum displacement, and the other 3 to an incremental cyclic displacement.

While the tests were performed a 3D-DIC was installed to be able to measure the buckling of the cells at the exterior surface of the honeycomb.

Fig. 1: Description of the shear behavior of the HRH-78 Nomex Honeycomb core a) The elastic limits were detected trough an incremental cyclic testing, b) The buckling of the cells is detected at a relatively low shear stress, c) Buckling scenario of collapsing and non-collapsing cells.

The results showed that the buckling of the cells starts to be visible at relatively low shear stress considering that the shear strength was around 0.58 MPa. By looking the deepness of the buckles, it was observed that the cells buckled predominantly to the inside of the specimen.

Also, the incremental cyclic tests revealed that the honeycomb structure presented a nonlinear elastic behavior beyond the buckling point. Finally, it has been seen that the buckling scenario of the cells was very different at the bifurcation point and at the shear strength limit (0.58 MPa). To explain this behavior a hypothesis was made: this difference is attributed to two different phenomenological phenomena, first the buckling and then the collapse of the cells. And so, an artificial neural network (ANN) was developed that was able to detect the collapse of the alveolus based on the shape of the buckles.

Testing sandwich beam specimens with lateral stabilization

The second part consisted into tests other 6 specimens. This time, the specimens consisted on a sandwich beam that had potting at the borders and at the middle. This was made in the purpose to study how the lateral stabilization (provided by the potting) affected the behavior of the cells.

The sandwich beams were submitted to a classical 3 point bending test and the response of the specimens was compared to the double lap specimens.

It was detected that the initial behavior of both types of specimens was very similar as the shear modulus was the same. However, there were three principal differences: the linear behavior of the cells was extended, the shear strength was increased by approximately 16% and 35% for the W and L directions respectively, and the collapse of the cells was much more dramatic.

Fig. 2: Comparison of the shear behavior of the same honeycomb structure under two different boundary conditions; Double lap and sandwich bending with lateral stabilization.

The experimental study revealed important aspects of the shear behavior of the honeycomb structure. The shear behavior of the honeycomb structure is mainly a postbuckling behavior. The nonlinear response of the cells can be divided into two phenomenological stages, buckling and collapse. And finally, that the boundary conditions of the cells strongly modify the nonlinear response of the honeycomb structure.

NUMERICAL STUDY

To complement this research, a numerical study was also performed by modeling the two types of test specimens that were used in the experimental part. This helps to see some aspects that were not very clear in the experimental part such as the buckling shape of the cells located at the interior of the core and to clarify the influence of the boundary conditions that modifies the nonlinear behavior of the cells.

The first part of this study was the modeling of the double lap test. The simulation revealed that the buckling shape of the cells of the exterior and interior part of the specimens were very different due to the lack of stabilization of the surrounding cells. Also, it was possible to find a relation between the shear stress and the rotation of the cell walls.

The second part was the modeling of the lateral stabilized honeycomb structure, where the buckling of the cells and the rotation of the cell walls was also obtained.

The comparison of both buckling shapes between the two types of specimens revealed that for the linear part the buckling is very similar but for the nonlinear behavior it's completely different, explaining the differences that were found on the experimental part.

Fig. 3: Comparison of the buckling of the cells in the interior of the double lap specimen and the sandwich beam with lateral

stabilization.

Institut Clément Ader (ICA), Université de Toulouse, CNRS UMR 5312-INSA-ISAE-Mines Albi-UPS, Toulouse, France. a jddrodri@insa-toulouse.fr a castanie@insa-toulouse.fr c christophe.bouvet@isae.fr


D Rodríguez-Ramírez

B Castanié
email: bcastanie@insa-toulouse.fr

C Bouvet

J D D Rodríguez-Ramírez

VIRTUAL TESTING OF METALLIC INSERTS FOR SANDWICH STRUCTURES

Keywords: Sandwich, inserts, FEA, honeycomb, Nomex

In this research, the virtual testing approach is used to study the failure of inserts in sandwich structures. First, a reduced F.E. model of inserts is presented, which includes nonlinear aspects of the materials such as the buckling and collapse of the honeycomb cells, the failure of the potting and the matrix failure of the skins. These model are validated through comparison with real tests showing a good agreement. This work is part of the development of an insert sizing method that could be an alternative to the classical analytical methods.

Introduction

Sandwich structures are widely used for helicopters, business jets, satellites, etc. These structures allow to design very lightweights panels and most of the time metallic inserts are used to assembly them.

The most complete reference for this type of inserts is the Insert design handbook of the ESA [START_REF] Ecss | Insert design handbook[END_REF], where an approach to size the inserts is presented. This method consists with calculating the pulloutforce that induces the failure of the parts that composes the insert, then, the weakest part causes the failure of the insert. This is based on an analytical model of the sandwich panel that was developed in 1953 [START_REF] Ericksen | THE BENDING OF A CIRCULAR SANDWICH PLATE UNDER NORMAL LOAD[END_REF], which despite the complexity of the equations is very used in the industry. Also, it is well known that this method overestimates the failure force of the inserts. If the ESA procedure is applied to the inserts of the literature (ref. [START_REF] Roy | Testing and modeling of Nomex TM honeycomb sandwich Panels with bolt insert[END_REF]- [START_REF] Heimbs | Failure behaviour of honeycomb sandwich corner joints and inserts[END_REF] for instance), the calculated load is always higher than in the tests by 18% to 32 %. Yet, the values obtained through this method are acceptable but not very accurate.

For this reason, F.E. methods have been proposed as a good alternative for the insert design instead of the analytical approaches [START_REF] Zenkert | The handbook of sandwich construction[END_REF], [START_REF] Seemann | VIRTUAL TESTING OF NOMEX HONEYCOMB SANDWICH PANEL INSERTS[END_REF]. However, the core and insert geometry are not only very complex to model, but also the numerous features that should be included demands a very good expertise or time investment, and even if these models are very accurate, they might be not suitable to be implemented for large scale simulations.

In this context, we propose the implementation of reduced F.E. models for the insert design, which allows to have accurate results without the main disadvantages of the detailed modeling. The model is based on the study presented in [START_REF] De | Experimental and numerical analysis of the shear nonlinear behaviour of Nomex honeycomb core: Application to insert sizing[END_REF] and the damage modeling method proposed in [START_REF] De | Damage Mechanics Modelling of the shear nonlinear behaviour of Nomex honeycomb core. Application to sandwich beams[END_REF].

Real specimen's description

Three inserts studied in [START_REF] Phacharaporn | Contribution à l'étude du comportement des inserts dans les structures sandwichs composites[END_REF] are used as experimental reference. All the three specimens are made using the same materials but the geometry is different as showed in figure 1-a. The core is a Nomex Honeycomb of 3.0 pcf and 20 mm of thickness with a cell diameter of 3.175 mm. The potting is made with the AV-121 B mixed with 10 % of phenolic microspheres. The skins are made of two layers [0,90] of the G0939/145.8 woven with a total thickness of 0.55 mm. All the specimens are submitted to pull-out until complete failure using a metallic support as shown in figure 1-b.

Virtual model features

The insert specimens are modeled using Abaqus standard. Only volume elements are used to represent the materials. The Z-displacement of the nodes at a radius of 15 mm is fixed to simulate the support of figure 1-b. The displacement is imposed at the center of the fastener as shown in figure 2. Because of the characteristics of the test, it is possible to use symmetry to simplify the model and simulate only one quarter of the specimen.

The behavior of the core, potting and skins included the linear and the post failure behavior. These behaviors laws are obtained through an extensive experimental and numerical analysis (see for example ref. [START_REF] De | Experimental and numerical analysis of the shear nonlinear behaviour of Nomex honeycomb core: Application to insert sizing[END_REF]). Some variations of the characteristics of the materials, such as the strength of the core or the potting elastic modulus, are taken into account to define an envelop of possible behaviors. This range is delimited between the best case (the core and potting are stronger due to manufacturing defects and the insert size is higher) and the worst possible case (when the core and potting are weaker and the insert is as his minimun possible size).

Finally, all these characteristics are introduced in the model through an Abaqus UMAT subroutine. These laws are discussed in the following sections.

Modeling of the core

The experimental reference of the shear behavior of this honeycomb core is in the work of Bunyawanichakul et al. in ref. [START_REF] Phacharaporn | Contribution à l'étude du comportement des inserts dans les structures sandwichs composites[END_REF], where a three point beam test is performed. However, even if this test is recommended by the ASTM C393 [START_REF]ASTM C393/C 393 M -06 Standard Test Method for Core Shear Properties of Sandwich Constructions by Beam Flexure[END_REF], the method is only accurate to determine the shear modulus and strength of the core, but it doesn't provide coherent values of the nonlinear behavior. This is because the cells in the middle collapse first, and therefore, the behavior curve only reflects the failure of those cells as shown in [START_REF] De | Experimental and numerical analysis of the shear nonlinear behaviour of Nomex honeycomb core: Application to insert sizing[END_REF] and [START_REF] Giglio | Numerical investigation of a three point bending test on sandwich panels with aluminum skins and Nomex TM honeycomb core[END_REF]. To estimate the natural complete shear behavior of this honeycomb core, the initial part of the curve provided by Bunyawanichakul [START_REF] Phacharaporn | Contribution à l'étude du comportement des inserts dans les structures sandwichs composites[END_REF] is used as initial reference and a typical shear curve of these Nomex cores (ref. [START_REF] Seemann | Numerical Modeling of Nomex Honeycomb Sandwich Cores at Meso-Scale Level[END_REF] and [START_REF] De | Experimental and numerical analysis of the shear nonlinear behaviour of Nomex honeycomb core: Application to insert sizing[END_REF] for instance) is scaled to fit the values, including the start of the nonlinear behavior (see figure 3).

Figure 3.

Comparison of the experimental Bunyawanichakul's curves [START_REF] Phacharaporn | Contribution à l'étude du comportement des inserts dans les structures sandwichs composites[END_REF] and the curves used as reference for this research.

Once the semi-experimental reference curve is defined, the modeling of the honeycomb core is made following the recommendations of [START_REF] De | Damage Mechanics Modelling of the shear nonlinear behaviour of Nomex honeycomb core. Application to sandwich beams[END_REF], where a CDM (Continumm Damage Mechanics) approach is proposed to include the nonlinear shear behavior of a honeycomb using only one volume elements through the thickness, allowing to obtain accurate results and reducing the computational cost.

Also, as explained in [START_REF] De | Experimental and numerical analysis of the shear nonlinear behaviour of Nomex honeycomb core: Application to insert sizing[END_REF], the behavior of the cells near the insert should be about 16 % and 35 % stronger in the W and L directions, respectively, in comparison to the nominal values, but also they should collapse earlier. This is because the honeycomb cells that are closer to the insert are much more stable due to the presence of the potting, and therefore have a different shear behavior. This increment of the shear strength is only considered for the best case and not for the worst case.

For this reason, the core is divided in two sections; the first one which is near the insert (Figure 2 in blue) with an equivalent radius of three cells after the potting, and the second one, the rest of the honeycomb, which is far from the insert (Figure 2 in red color).

The model curves in the L and W directions of the figure 3 are fitted using the CDM approach of ref.

[9], including two shear nonlinear stages; initial buckling and collapse, as explained in [START_REF] De | Experimental and numerical analysis of the shear nonlinear behaviour of Nomex honeycomb core: Application to insert sizing[END_REF]. Finally, the behavior of both core sections is given in figure 4.

Modeling of the potting

The potting is considered as a perfect cylinder. For insert type 1 and 2, the typical and minimum values of the potting effective radius recommended by the Insert design book of the ESA are considered for the worst and best case respectively (see ref [START_REF] Ecss | Insert design handbook[END_REF] and equations 1 and 2).

Concerning the material, the potting behavior is highly nonlinear because of the added microspheres, which transforms the adhesive into a polymer syntactic foam. When this material is submitted to tension, its Young modulus is 1851 MPa and it breaks at 15 MPa, while in compression the Young modulus is 1233 MPa and has an almost perfectly plastic behavior starting at 31 MPa (instead of breaking).

This similar behavior was programed into the UMAT and is given in figure 5a.

(2)

Modeling of the skins

The elastic modulus of the skins are E X = E Y = 52 GPa and E Z = 5 GPa in the principal directions, while the shear modulus are G XY = 32 GPa and G XZ = G YZ = 3.5 GPa. Both superior and inferior skins are modeled as a homogenous material with uncoupled damage laws implemented to take into account the matrix damage in the shear XY, XZ and YZ directions. Once the elastic limits are reached (100 MPa) the stiffness is reduced to 15% of the original value. Both curves are shown in figure 5b.

Results

The simulations are run with 8 processors, and it takes between 7 to 12 min depending on the insert case and considerations of the materials. This calculation time is very acceptable. Also, the numerical and experimental results can be compared. Visually (see figure 6), the failure modes of the real test specimens seems well represented; the shear buckling and collapse of the cells, ECCM18 -18 th European Conference on Composite Materials Athens, Greece, 24-28 th June 2018 6

the plasticity of the potting and the deformation in the skins. The only important failure mode that is not represented is the breaking of the skins/potting interface at the bottom of the insert. Concerning the loading curves (see fig 7), for inserts type 1 and 2, the consideration of the best and worst cases seems to describe the range of maximal strength of all the experimental tests; which is relevant. For the insert type 3, only the typical values are considered, showing a good agreement with the experimental results until a displacement of 1.5 mm. After this, the stiffness of the model increased dramatically presumably due to the fact that the fiber failure of the skins is not included in the insert model.

Finally, the method proposed in [START_REF] De | Damage Mechanics Modelling of the shear nonlinear behaviour of Nomex honeycomb core. Application to sandwich beams[END_REF] allows to discern the elastic buckling from the permanent damage of the cells. The same procedure is used to detect the matrix failure of the skins. All these failures are identified in figures 7 and 8 for the insert type 1 and are denoted with the letters from A to H.

Conclusions

The proposed method allows to simulate the behavior of inserts at a very low computational cost and to obtain very accurate results. Also, in contrast to the detailed modeling of inserts, this method is easier to implement and allows to easily identify the failure modes introduced in the model as shown in figure 7.

Another interesting aspect is that the consideration of the best and worst cases seems a good method to determine the strength range of inserts.

Finally, although more work is still having to be done in this part, it is shown that the influence of small variations, such as defects, of the parameters of the materials, plays a very important role in the insert behavior and is still to be investigated.

Figure 1 .

 1 Figure 1. Insert's description of type 1, 2, 3 and testing set up. [10]

  ECCM18 -18 th European Conference on Composite Materials Athens, Greece, 24-28 th June 2018 3 J.D.D. Rodríguez-Ramírez, B. Castanié and C. Bouvet

Figure 2 .

 2 Figure 2. Reduced F.E. models of inserts type 1, 2 and 3.

Figure 4 .

 4 Figure 4. Behavior laws of the honeycomb far and near to the insert. (based in [9])

  ECCM18 -18 th European Conference on Composite Materials Athens, Greece, 24-28 th June 2018 5 J.D.D. Rodríguez-Ramírez, B. Castanié and C. Bouvet

Figure 5 .

 5 Figure 5. Potting and skin behavior laws

Figure 6 .

 6 Figure 6. Comparison of the experimental and numerical damage scenario of the insert type 1 after the pull out test.

Figure 7 .

 7 Figure 7. Comparison of the experimental and numerical behavior of the loading curves for the inserts type 1, 2 and 3.

Figure 8 .

 8 Figure 8. Identification of the failure modes in the insert type 1. (see figure 6)

ECCM18 -18 th European Conference on Composite Materials Athens, Greece, 24-28 th June 2018

J.D.D. Rodríguez-Ramírez, B. Castanié and C. Bouvet

Acknowledgments

This research was developed at the ICA laboratory at Toulouse, France, and was co-financed by the CONACYT from Mexico.