Blockchain Abstract Data Type
Emmanuelle Anceaume Antonella Del Pozzo Romaric Ludinard Maria Potop-Butucaru Sara Tucci-Piergiovanni

	
			
			linecounter
			
			
			
Recent Belle results related to π-K interactions
    Bilas Pal
 (On behalf of the Belle Collaboration)
 Brookhaven National Laboratory, Upton, NY & University of Cincinnati, Cincinnati, OH
    December 30, 2023
===========================================================================================================================================




	
 


The presented work continues the line of recent distributed computing community efforts dedicated to the theoretical aspects of blockchains. This paper is the first to specify blockchains as a composition of abstract data types all together with a hierarchy of consistency criteria that formally characterizes the histories admissible for distributed  programs that use them. Our work is based on an original oracle-based construction that, along with new consistency definitions, captures the eventual convergence process in blockchain systems. The paper presents as well some results on implementability of the presented abstractions  and a mapping of representative existing blockchains from both academia and industry in our framework. 





 




§ INTRODUCTION




























The paper proposes a new data type to formally model blockchains and their behaviors. 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 <cit.>. The question is about the consistency criterion of blockchains as Bitcoin <cit.> and Ethereum <cit.> 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 a semantics equivalent to  eventual consistent append-only queue but as well weaker semantics. More in detail, we define a semantic equivalent to  eventual 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 <cit.>). 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. 








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 <cit.>) 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, 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 number of forks, in terms of branches of the tree from a given block. In this respect we define oracles models such that, depending on the model, the number of forks from a given block can be: unbounded, up to k>1, and k=1 (no fork) for the  strongest oracle model. 

The blockchain is then 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 <cit.> independent of the  underlying communication and failure model. 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  <cit.> (Theorem <ref>). It must be noted that we considered Consensus  defined  in <cit.>, in which the Validity property states that  a valid block can be decided even if sent by a faulty process.
	
	
  * The weakest oracle,  which validates a potential unbounded number of blocks to be appended to a given block, has Consensus number  1   (Theorem <ref>). 
	



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

  * A necessary condition (Theorem <ref>) for  Eventual Prefix in a message-passing system,  called Update Agreement stating that  each update sent by a correct process must be eventually received by every correct process. The result implies that it is impossible to implement Eventual Prefix if even only one message sent by a correct process is dropped. 
	

	
	
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 <cit.> and Ethereum <cit.> have a validation mechanism that maps to our weakest oracle and then they only implement Eventual prefix, while other proposals maps to our strongest oracle, falling in the class of those that guarantee Strong Prefix (e.g. Hyperledger Fabric <cit.>, PeerCensus <cit.>, ByzCoin  <cit.>, see Section <ref> for further details).  







		

Related Work.
Formalisation of blockchains in the lens of distributed computing has been recognized as an extremely important topic <cit.>. The topic is recent and to the best of our knowledge,  no other attempt proposed a unified  framework capturing both Consensus-based and proof-of-work blockchains, as the presented paper aims at proposing.


In <cit.>, the authors present a study about the relationship of  BFT consensus and blockchains. In order to abstract the proof-of-work mechanism the authors propose a specific oracle, in the same spirit of our oracle abstraction. While  their oracle is more specific then ours, since it makes a direct reference to proof-of-work properties, it offers as well a fairness property. Note that we do not formalize fairness properties in this paper, we only offer a generic merit parameter that can be used to define fairness. Let us note that apart from the fairness property, our oracle captures the semantics of <cit.>'s oracle. 



In parallel and independently of the work  in <cit.>,  <cit.> 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. They discuss how Hyperldger Fabric implements eventual consistency and propose implementations for sequential consistency and linearizability using a total order broadcast abstraction.  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 and corroborate our mapping of Hyperledger Fabric. On the other hand the proposed formalization does not propose weaker consistency semantics more suitable for proof-of-work blockchains as BitCoin. Indeed, <cit.> continues and it is complementary to the work on the first formalisation of Bitcoin as a distributed ledger proposed in <cit.> where the distributed ledger is modelled as a simple register. These works suggest different abstractions  to model proof-of-work and Consensus-based blockchains, respectively.
The presented paper, on the other hand, thanks to our oracle-based construction  (not present in <cit.>, <cit.>) generalizes both  <cit.> and   <cit.> to encompass both kind of blockchains in a unified framework. 


Finally,  <cit.> 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. Nicely, this result and more in general solvability results for eventual consistency <cit.> immediately apply to our Strong Prefix criterion. 


















§ 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 <cit.>:  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 in a set Z. 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, the corresponding transition in the transition system being formalized by a transition function τ. Second, operations can return values taken in an output alphabet B, which depend 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 (its side effect) and returns that element (its output).

The formal definition of abstract data types is as follows. 




 

(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.
 


(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.

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. 
The language recognized by an ADT is the set of all possible words. This language defines the sequential specification of the ADT. More formally, 

(Sequential specification L(T))
A finite or infinite sequence 
σ = (σ_i)_i ∈ D∈Σ^∞, D = ℕ 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, 
	
		
  * the output alphabet of σ_i is compatible with ξ_i: ξ_i ∈δ_T ^-1(σ_i);
		
  * the execution of the operation σ_i is such that the state changed from ξ_i to ξ_i+1: τ_T(ξ_i,σ_i)=ξ_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 asymmetric event structures, i.e., partial order relations among events executed by different processes <cit.>.

(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 relation over the events in E. Two events are ordered by ↦ if they are produced by the same process;
		
  * ≺: is the operation order, irreflexive order over the events of E. For each couple (e, e') ∈ E^2, if e is an operation invocation and e' is the response for the same operation then 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' 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




The 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,

(Consistency criterion C)
	A consistency criterion is a function 
    C: 𝒯→𝒫(ℋ)
 where 𝒯 is the set of abstract data types, ℋ is a set of histories and  𝒫(ℋ) is the sets of parts of ℋ. 


 Let 𝒞 be the set of all the consistency criteria.
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. The height of a block refers to its distance to the root. We denote by b_k a block located at height k. By convention, the root of the BlockTree is denoted by b_0. Blocks are said valid if  they satisfy a predicate P which is application dependent (for instance, in Bitcoin, a block is considered valid if it can be connected to the current blockchain and does not contain transactions that double spend a previous transaction). 

We represent by ℬ  a countable and non empty set of blocks and by ℬ'⊆ℬ a countable and non empty set of valid blocks, i.e.,  ∀ b ∈ℬ', P(b)=⊤.  By assumption b_0 ∈ℬ'; We also denote by ℬ𝒞 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, ℱ is a countable non empty set of selection functions, f ∈ℱ : ℬ𝒯→ℬ𝒞;  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 also deeply 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.



The BlockTree Abstract Data Type 
is the 6-tuple 
BT-ADT=⟨ A={ append(b),  read(): 
b ∈ℬ}, B= ℬ𝒞∪{ true, false}, Z= ℬ𝒯×ℱ× (ℬ→{ true, false}), ξ_0 = (bt^0, f), τ, δ⟩, where the transition function τ:Z × A → Z is defined by

	
  * τ((bt,f, P),  append(b))= ({b_0}^⌢f(bt)^ ⌢{b},f,P)  if b∈ℬ'; (bt,f, P) otherwise;

	
  * τ((bt,f, P),  read())= (bt,f, P), 

and the output function δ:Z × A → B is defined by

	
  * δ((bt,f, P),  append(b))=  true if b ∈ℬ'; false otherwise;
	
	
  * δ((bt,f, P),  read())= {b_0}^⌢ f(bt);
	
  * δ((bt_0,f, P),  read())= b_0.





























































The semantic of the read and the append operations directly depend on the selection function f ∈ℱ. In this work we let this function 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 <ref>. 






















































































































  §.§.§ 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: ℬ𝒞→ℕ 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: ℬ𝒞×ℬ𝒞→ℕ 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^'.
	





  
BT Strong consistency.


The BT Strong Consistency criterion is the conjunction of 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 been inserted in the BlockTree with the append() operation. The Local monotonic read states  that, given the sequence of read() operations at the same process, the score of the returned blockchain never decreases.  The Strong prefix property states that for each couple of read operations, one of the returned blockchains is a prefix of the other returned one (i.e., the prefix never diverges).  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.  More formally, the BT Strong consistency criterion is defined as follows:






	A concurrent history H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ of the system that uses a BT-ADT verifies the BT Strong Consistency criterion if the following  properties hold:
	
		
  * Block validity: 
		 ∀ e_rsp(r) ∈ E, ∀ b ∈ e_rsp(r):bc, b ∈ℬ' ∧∃ e_inv( append(b)) ∈ E, 
		 
		 e_inv(append(b)) ↗ e_rsp(r).	
		
  * Local monotonic read: 
		
    ∀ e_rsp(r), e_rsp(r') ∈ E^2,  if  e_rsp(r) ↦ e_inv(r'),  then  score(e_rsp(r):bc)≤ score(e_rsp(r'):bc').

		
  * 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').
		
		
  * 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 }| <∞.
	
	



Figure <ref> shows a concurrent history H admissible by the BT Strong consistency criterion. In this example the score is the length l 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 the block validity property is satisfied. The Local monotonic read 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 l be the score of the blockchain returned by 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 l, and (ii) the infinite set of read() operations such that the score is greater than l. We can iterate the same reasoning for each read() operation in H. Thus H satisfies the Ever growing tree property.






	mystyle/.style=
		circle,
		inner sep=1pt,
		thick,
		align=center,
		draw=black,
	



	mystyleLight/.style=
		circle,
		inner sep=1pt,
		thick,
		align=center,
		draw=gray!40,
	    text=gray!40
	









  
BT Eventual consistency.



The BT Eventual consistency criterion is the conjunction of the block validity, 
the Local monotonic read and the Ever growing tree of the BT Strong consistency criterion together with the Eventual prefix which states 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 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.


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_r^2 | h≠ k,  mpcs(e_rsp(r_h):bc_h, e_rsp(r_k):bc_k) < s } | < ∞



 The Eventual prefix properties captures the fact that two or more concurrent blockchains can co-exist in a finite interval of time, but that  ly 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.  

Based on this definition, the BT Eventual consistency criterion is defined as follows:



	A concurrent history H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ of the system that uses a BT-ADT verifies the BT Eventual consistency criterion if it satisfies the Block validity, Local monotonic read, Ever growing tree, and the Eventual prefix properties.

 
			
		




		
		
		
		
		
		

		 
	





Figure <ref> shows a concurrent history that satisfies the Eventual prefix property but not the Strong prefix one. Strong Prefix is not satisfied as blockchain[For ease of readability we extend the notation b_i^ ⌢ b_j to represent concatenated blocks in a blockchain.] 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 <ref> 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 <ref> and <ref>, 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 l be the score of the blockchain returned by r. In Figure <ref> 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 l (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') ≥ l. We can iterate the same reasoning for each read() operation in H. Thus H satisfies the Eventual Prefix property.

Figure <ref>  shows a history that does not satisfy any consistency criteria defined so far.











  
Relationships between EC and SC.

Let us denote by 

ℋ_EC and by ℋ_SC the set of histories satisfying respectively the EC and the SC consistency criteria.  



Any history H satisfying SC criterion satisfies EC  and ∃ H satisfying  EC that does not satisfy SC, i.e.,  
ℋ_SC⊂ℋ_EC. 






	
	
E C ≤ SC implies that ℋ_SC⊂ℋ_E C, and ℋ_SC⊂ℋ_E C implies that ∀ H ∈ℋ_SC⇒ H∈ℋ_E C. By hypothesis, H  verifies the Ever Growing Tree property, thus ∀ e_rsp(r) ∈ E(a^*,r^*) with s=score(e_rsp(r):bc) then set { e_inv(r') ∈  E |e_rsp(r) ↗ e_inv(r'), score(e_rsp(r”):bc)≤ s } is finite, and thus, there is an infinite set  { e_inv(r') ∈  E |e_rsp(r) ↗ 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 for each  ∀ 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_r^2 | 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∈ℋ_E C and H∉ℋ_SC. 
Any 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. Moreover, an append is successful only if the input block is valid with respect to a predicate. This means that histories with no append operations are trivially admitted. 
In the following we will introduce a new abstract data type called Token Oracle that when combined with the BlockTree will help in (i) validating blocks and (ii) controlling forks. We will first formally introduce the Token Oracle in Section <ref> and then we will define the properties on the BlockTree augmented with the Token Oracle in Section <ref>.








 



 §.§ Token oracle Θ-ADT








In this section we formalize the Token Oracle Θ to capture the creation of blocks in the BlockTree structure. The block creation process requires that the new block must be closely related to an already existing valid block in the BlockTree structure. We abstract this implementation-dependent process by assuming that a process will obtain the right to chain a new block b_ℓ to b_h 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∈ℬ'. 

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 a generic object obj_h, it invokes the getToken(obj_h,obj_ℓ) operation with object obj_ℓ from set 𝒪={obj_1,obj_2, …}.  If getToken(obj_h,obj_ℓ) operation is successful, it returns an object obj_ℓ^tkn_h∈𝒪', where (i) tkn_h is the token required to access object obj_h and (ii) each object obj_k ∈𝒪' is valid with respect to predicate P, i.e. P(obj_k)=⊤.  We say that a token is generated each time it is provided to a process and it is consumed when the oracle grants the right to connect it to the previous object. Each token can be consumed at most once. To consume a token we define the token consumption consumeToken( obj_ℓ^tkn_h) operation, where the consumed token tkn_h is the token required for the object obj_h.  A maximal number of tokens k for an object obj_h is managed by the oracle. 
The consumeToken(obj_ℓ^tkn_h) side-effect on the state is the insertion of the object obj_ℓ^tkn_h in a set K_h as long as the cardinality of such set is less than k.

In the following 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, assures controls that no more than k token can be consumed for each object. 

Θ_P when combined with the BlockTree abstract data type will only help in validating blocks, while Θ_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_k,obj_h) operation is invoked, the oracle provides a token with a certain probability p_α_i>0 where α_i is a merit parameter characterizing  the invoking process i. [The merit parameter can reflect for instance the hashing power of the invoking process.] 
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. [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.] When a getToken(obj_k,obj_h) operation is invoked by a process with merit α_i, the oracle pops the first cell from the tape associated to α_i, and a token is provided to the process if that cell contains tkn. 



Both oracles also enjoy  an infinite array of sets, one for each object, which is populated each time a token is consumed for a specific object. When the set cardinality reaches k then no more tokens can be consumed for that object. For a sake of generality, Θ_P is defined as Θ_F with k=∞ while for Θ_F a predetermined k ∈ℕ is specified. 















 
We  first introduce some definitions and notations.

	
  * 𝒪={obj_1,obj_2, …}, infinite set of generic objects uniquely identified by their index i;
	
  * 𝒪'⊂𝒪,  the subset of objects  valid with respect to predicate P, i.e. ∀ obj'_i ∈𝒪', P(obj'_i)=⊤.
	
  * 𝔗={tkn_1,tkn_2, …}  infinite set of tokens;
	
  * 𝒜={α_1, α_2, …} an infinite set of rational values;
	
  * ℳ 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 ∈ℳ: 𝒜→{tkn ,}^*; 
	
  * K[ ] is a infinite array of sets (one per object) of elements in 𝒪'. All the sets are initialized as empty and can be fulfilled with at most k elements, where k∈ℕ is a parameter of the oracle ADT;
	
  * pop: {tkn ,}^* →{tkn ,}^*, pop(a· w)=w;
	
  * head: {tkn ,}^* →{tkn ,}^*, head(a· w)=a;	

	
  * add : {K}×ℕ×𝒪'→{K}, add(K, i, obj_ℓ^tkn_h )=K : K[i]=K[i] ∪{obj_ℓ^tkn_h} if |K[i]|<k; else K[i]=K[i];
	
  * get : {K}×ℕ→ℕ, get(K, i)=K[i];   



(Θ_F-ADT Definition).
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∈𝒪', obj_ℓ∈𝒪, tkn_h ∈𝔗}, B= 𝒪'∪ Boolean, Z= m(𝒜)^* ×{K}× k ∪{pop, head, dec, 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, h,obj_ℓ^tkn_h)), if
	tkn_h∈𝔗  ;  { ({tape_α_1,…, tape_α_i, …}, K, k)} otherwise.
	 

and the output function δ:Z × A → B is defined by 

	
  * δ(({tape_α_1,…, tape_α_i, …}, K,k) , getToken(obj_h,obj_ℓ))= obj_ℓ^tkn_h:  obj_ℓ^tkn_h∈𝒪',tkn_h ∈𝔗, if head(tape_α_i)=tkn with α_i the merit of the invoking process;   otherwise;
	
  * δ( ({tape_α_1,…, tape_α_i, …}, K,k) ,  consumeToken(obj_ℓ^tkn_h))= get(K, h).
	




(Θ_P-ADT Definition).
The Θ_P Abstract Data type is defined as the Θ_F-ADT with k=∞.




Figure <ref> shows a possible path of the transition system defined  by the Θ_F and  Θ_P-ADTs. 
 






	
From the Θ_F-ADT with k=1 specification (Definition <ref>) the next properties follow:


	Θ_F,k=1:

	
  * Mutual Exclusion. For each object obj_h, consumeToken_i(obj_ℓ^tkn_h) returns a set containing at most 1 token;
	
  * Validity. Each token returned by consumeToken_i() is valid;
	
  * No Deadlock. If there is a process i that performs getToken_i(obj_h, obj_ℓ) infinitely often then at least one process j performs consumeToken_i(obj_ℓ^'^tkn_h) and returns at least the object obj_ℓ^'^tkn_h.   




	[Mutual Exclusion] For each object obj_h, consumeToken_i(obj_ℓ^tkn_h) returns a set containing at most 1 token;



	The proof follows by construction. The consumeToken_i(obj_ℓ^tkn_h) operation inserts obj_ℓ^tkn_h in the Oracle sets K[h] only if obj_ℓ^tkn_h is valid and |K[h]|<k=1. Since the consumeToken() operation returns object stored in the Oracle sets then, for each object b_h the set returned by the consumeToken() contains at most one object. 




	[Validity] Each token returned by consumeToken_i() is valid;



	The proof follows by construction. The consumeToken_i(obj_ℓ^tkn_h) operation inserts obj_ℓ^tkn_h in the Oracle sets K[h] only if obj_ℓ^tkn_h is valid. Since the consumeToken() operation returns object stored in the Oracle sets then all the objects returned by the consumeToken() operation are valid.



	[No Deadlock] If there is a process i that performs getToken_i(obj_h, obj_ℓ) infinitely often then at least one process j performs consumeToken_i(obj_ℓ^'^tkn_h) and returns at least the object obj_ℓ^'^tkn_h.   



	The proof follows by construction. By hypothesis process i performs  an infinite number of getToken(obj_h, obj_ℓ) invocations for object obj_h and from the properties of the pseudo random sequences of tapes, if there are an infinite number of getToken() invocations for  object obj_h then there exists at least one response for which getToken() operation returns a valid object obj_ℓ^tkn_h.
	Thus process i can invoke the consumeToken(obj_ℓ^tkn_h) operation. The operation can return either obj_ℓ^tkn_h or obj_ℓ^'^tkn_h. In the former case the proof is concluded. In the latter case, there has been another process j ≠ i that obtained a valid object obj_ℓ^'^tkn_h before i and invoked consumerToken(obj_ℓ^'^tkn_h).




	The Θ_F-ADT with k=1 satisfies the Mutual Exclusion, Validity and No Deadlock.



	The proof follows considering Lemma <ref>, Lemma <ref> and Lemma <ref>.


 this should be moved to the Related Work Part
Those properties, except for the Validity, are the same properties that characterize the Mutual Exclusion problem (<cit.>). Informally this is the problem to manage the access to a single, indivisible resource that can be accessed by at most one process at a time.








 §.§ BT-ADT augmented with Θ Oracles

In this section 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 which triggers the getToken(b_h←last_block(f(bt)), b_ℓ) operation as long as it returns a token on b_k, i.e., b_ℓ^tkn_h which is a valid block in ℬ'. Once obtained, the token is consumed and the append terminates, i.e. the block b_ℓ^tkn_h is appended to the block h in the blockchain f(bt) ({b_0}^⌢f(bt)|_h^ ⌢{b_ℓ}). Notice that those two operations and the concatenation occur atomically.
 
We say that the BT-ADT augmented with Θ_F or Θ_P oracle is a refinement  ℜ(BT-ADT, Θ_F) or ℜ(BT-ADT, Θ_P) respectively. 



































































































Let us define the following auxiliary function:

	
  * evaluate: ℬ× B^Θ→ bool. evaluate(b, δ_b ∘δ_a^* )= true if (∃ h: b^tkn_h∈δ_b ∧ (∃ X : b^tkn_h∈ X ∧ X ∈δ_a^*)); false otherwise.


[ℜ(BT-ADT, Θ_F)  refinement]
Given the   BT-ADT=⟨ A, B, Z,ξ_0, τ, δ⟩, 
and the 
Θ_F-ADT =(A^Θ, B^Θ, Z^Θ, ξ_0^Θ, τ^Θ, δ^Θ), 
we have 
ℜ(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_k ←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, h, b_ℓ^tkn_h),k, {b_0}^⌢f(bt)|_h^ ⌢{b_ℓ},f,P) if
	tkn_h∈𝔗∧ 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_k ←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_k ←last_block(bt),b_ℓ) )= b_ℓ^tkn_h:  b_ℓ^tkn_h∈ℬ',tkn_h ∈𝔗, 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(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,k bt_0,f,P),  read())= b_0.
	


 Same definition as the ℜ(BT-ADT, Θ_F)  refinement.
















	A concurrent history H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ of the BT-ADT  composed with Θ_F-ADT satisfies the k-Fork Coherence if there are at most k append() operations that return ⊤ for the same token. 




	Each concurrent history H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ of the BT-ADT composed with  a Θ_F-ADT satisfies the k-Fork Coherence.
	



	We prove the theorem by considering the defined refinement (Definition <ref>) 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 <ref>). 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

In this section we define a hierarchy between different BT-ADT satisfying different consistency criteria when augmented with different oracle ADT. We use the following notation:  BT-ADT_SC and BT-ADT_E C to refer respectively to BT-ADT generating concurrent histories that satisfies the SC and the E C consistency criteria. When augmented with the oracles we have the following four typologies, where for the frugal oracle we explicit the value of k: ℜ(BT-ADT_SC, Θ_F,k), ℜ(BT-ADT_SC, Θ_P), ℜ(BT-ADT_ E C, Θ_P), ℜ(BT-ADT_E C, Θ_F,k).



In the following we want study the relationship among the different refinements. Without loss of generality, let us consider only the set of histories ℋ̂^ℜ(BT-ADT,Θ) such that each history Ĥ^ℜ(BT-ADT,Θ)∈ℋ̂^ℜ(BT-ADT,Θ)  is purged from the unsuccessful append() response events (i.e., such that the returned value is ). Let ℋ̂^ℜ(BT-ADT,Θ_F,k) be the concurrent set of histories generated by a BT-ADT refined with Θ_F,k-ADT and let ℋ̂^ℜ(BT-ADT,Θ_P) be the concurrent set of histories generated by a BT-ADT refined with Θ_P-ADT.


	ℋ̂^ℜ(BT-ADT,Θ_F)⊆ℋ̂^ℜ(BT-ADT,Θ_P). 



	The proof follows from Theorem <ref> considering that ℜ(BT,Θ_P) can generate histories with an infinite number of append() operations that successfully terminate while ℜ(BT,Θ_F) can generate history with at most k append() operations that successfully terminate.
	



	If k_1 ≤ k_2 then ℋ̂^ℜ(BT-ADT,Θ_F,k_1)⊆ℋ̂^ℜ(BT-ADT,Θ_F,k_2). 



	The proof follows from Theorem <ref> applying the same reasoning as for the proof of Theorem <ref> with k_1 ≤ k_2.
	


Finally, from Theorem <ref> the next corollary follows.


	ℋ̂^(ℜ(BT-ADT_SC,Θ)⊆ℋ̂^ℜ(BT-ADT_E C,Θ). 







Combining Theorem <ref> and Theorem <ref> we obtain the hierarchy depicted in Figure <ref>.








































 










§ 
	IMPLEMENTING BT-ADTS






 §.§ Implementability in a concurrent model

In this Section we show that Θ_F,k=1 has consensus number ∞ and that Θ_P 
has consensus number 1.


We consider a concurrent system composed by n processes such that up to f processes are faulty (stop prematurely by crashing), f<n. Moreover, processes can communicate through atomic registers.







  §.§.§ Frugal with k=1 at least as strong as Consensus





In the following we prove that there exists a wait-free implementation of the Consensus <cit.> by the Θ_F,k=1 Oracle object.
In particular, in this case Θ_F,k=1 = ⟨ A= {getToken(b_h,b_ℓ), consumeToken( b_ℓ^tkn_h):
b_h, b_ℓ^tkn_h∈ℬ^', b_ℓ∈ℬ, tkn_h ∈𝔗}, B= ℬ^'∪ Boolean, Z= m(𝒜)^* ×{K}× k ∪{pop, head, dec, get}, ξ_0, τ, δ⟩. We explicit consider blocks and valid blocks (ℬ and ℬ^') rather than objects and valid objects (𝒪 and 𝒪^'). Moreover, we consider a version of the Consensus problem for the blockchain. Thus, we consider the Validity property as in <cit.> such that the decided block b satisfies the predicate P. 

	Consensus 𝒞:
	
		
  * Termination. Every correct process eventually decides some value.
		
  * Integrity. No correct process decides twice.
		
  * Agreement. If there is a correct process that decides a value b, then eventually all the correct processes decide b.
		
  * Validity<cit.>. A decided value is valid, it satisfies the predefined predicate denoted P.
	




To this aim, we first prove that there exists a wait-free implementation of Compare&Swap() object by consumeToken() object in the case of Θ_F,k=1, implying that consumeToken() has the same Consensus number as Compare&Swap() which is ∞ (see <cit.>). Finally we compose the consumeToken() with the getToken() object proving that there exist a wait-free implementation of 𝒞 by Θ_F,k=1.

Figure <ref> describes consumeToken() (CT), as specified by the Θ-ADT, along with the Compare&Swap() (CAS). 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. 
In comparison with consumeToken(b_ℓ^tkn_h) we have that b_ℓ^tkn_h is the new_value, register is K[h] and the implicit old_value is {}. That is, add(K,h,b) stores b in K[h] if |K[h]|<k=1, then if K[h]={}. In any case the operation returns the content of K[h] at the end of the operation itself. Figure <ref> describes and algorithm that reduces CAS to consumeToken().







	If input values are in ℬ' then there exists an implementation of CAS by CT in the case of Θ_F,k=1.



	The proof simply follows by construction. Let us consider the algorithm in Figure <ref>. When the Compare&Swap() operation is invoked, if K[h] is empty, then when consumeToken() is invoked with b_ℓ^tkn_h (valid by hypothesis) K[h] is populated with b_ℓ^tkn_h. Such value is later returned by the consumeToken() operation in retuend_value. Since it is the same value as b_ℓ^tkn_h (line <ref>) then the Compare&Swap returns the value of K[h] at the beginning of the operation, {}. If the condition at line (line <ref>) does not hold, then this means that K[h] did not change during the operation and its value, in returned_value is returned.



Figure <ref> describes a simple implementation of Consensus by Θ_F,k=1. When a correct process p_i invokes the propose(b) operation it loops invoking the getToken(b_0, b) operation as long as a valid block is returned (lines <ref>-<ref>). In this case the getToken() operation takes as input some block b_0 and the proposed block b. Afterwards, when the valid block has been obtained p_i invokes the consumeToken(validBlock) operation whose result in stored in the tokenSet variable (line <ref>). Notice, the first process that invokes such operation is able to successfully consume the token, i.e., the valid block is in the Oracle set corresponding to b_0, which cardinality is k=1, and such set is returned each time the consumeToken() operation is invoked for a block related to b_0. Finally, (line <ref>) the decision is triggered on such set (with contains one element).





	A decided value is valid, it satisfies the predefined predicate denoted P.



	The lemma follows considering that the decided values are valid values returned by the consumeToken() operation. 
	The consumeToken_i(obj_ℓ^tkn_h) operation inserts obj_ℓ^tkn_h in the Oracle sets K[h] only if obj_ℓ^tkn_h is valid. Since the consumeToken() operation returns object stored in the Oracle sets then all the objects returned by the consumeToken() operation are valid.
	



	Every correct process eventually decides some value.	



	Each correct process p_i eventually gets out of the loop, obtains a valid block and invoke the consumeToken() operation. By definition, such operation, when invoked with a valid block b', returns either b' or another valid block, which is decided.	
	



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




	If a correct process p_i decides b then such value has been returned by the consumeToken() operation. Since k=1, then the set associated to b_0, K[0] contains the first valid block for which the consumeToken() is invoked. Such operation add a new valid block to the K[0] if |K[0]|<k=1, otherwise such set is not modified. It follows that afterwards, b is always returned by the consumeToken() operation and all the other correct processes decide on b.


 
	No correct process decides twice.



	The proof trivially follow since the algorithm terminates after the decision.

	contenuto...



	Θ_F,k=1 Oracle has Consensus number ∞.



	The proof proceeds by construction, let us consider the implementation in Figure <ref>. All correct processes performing the Consensus are looping on the getToken(b_0,b) operation. From the properties of the pseudo random sequences of tapes, if there are an infinite number of getToken() invocations for an block b_0 then there exists at least one response for which getToken() operation returns a valid block b^tkn_0.
	Thus, all correct process i can invoke the consumeToken(b^tkn_0) operation with valid values. Since all the processes invoke such operation with valid values with can apply Theorem <ref> which concludes the proof considering that CAS has Consensus number ∞ (<cit.>).





 Notice, I searched for an already proved reduction between mutex and consensus but I could not manage to find any.


	There not exists and algorithm 𝒯_Θ_F,k=1→𝒞 such that Θ_F,k=1 Oracle reduces to 𝒞.


 
	Let us suppose that 𝒯_Θ_F,k=1→𝒞 exists. When a correct process p_i invokes getToken() or consumeToken() then 𝒯_Θ_F,k=1→𝒞 has to invoke the propose() Consensus operation. From the Consensus Termination property follows that every correct process eventually decides, which implies that all the correct processes proposes. If p_i is the only process invoking getToken() or consumeToken() then there are no guarantees about the Consensus Termination and then no guarantees on the getToken() or consumeToken() termination, violating the No Deadlock property. It follows that  𝒯_Θ_F,k=1→𝒞 concluding the proof.




 



  §.§.§ Prodigal not stronger than an Atomic Register




In order to show that the Prodigal oracle Θ_P has consensus number 1, it suffices to find a wait-free implementation of the oracle by an object with consensus number 1. To this end we present a straightforward implementation of the Prodigal oracle by Atomic Snapshot<cit.>. 


Let us firstly simplify the notation of the consume token operation. Let us consider a consume token invoked for a given block b_h, denoted as consumeToken_h(tkn_m), which simply writes a token from the set 𝔗={tkn_1,tkn_2, …, tkn_m,…} in the set K[h]. Without loss of generality let us assume that: (i) tokens are  uniquely identified , (ii)  cardinality of 𝔗 is n finite but not known and (iii) the set K[h] is  represented by a collection of n atomic registers 𝔎[𝔥={R_h,1,R_h,2, …, R_h,m,… R_h,n}, where R_h,m is assigned to the tkn_m token, i.e. R_h,m can contain either  or tkn_m. 

It can be observed that the  consumeToken_h(tkn_m) in the case of k infinite, always allows to write the token tkn_m in R_h,m, i.e. there always exists a register R_h,m for the proposed token tkn_m. By the oracle definition, moreover, the consumeToken_h(tkn_m) returns a read of the n registers that includes the last written token. Figure <ref> shows a  trivial implementation of commit token CT using Atomic Snapshot that offers  update(R_i, value),  scan(R_1, R_2, …, R_n) operation to update a particular register and perform an atomic read of input registers, respectively. 




	Θ_P Oracle has Consensus number 1.



	The proof trivially follows from  implementation  in Figure <ref>  of the consensus token operation of the Prodigal oracle by the Atomic Snaposhot object and from <cit.>. 
 



 §.§ Implementability in a message-passing system model


We consider a message-passing system composed of an arbitrary large but finite set of n processes, Π={p_1, …, p_n}.

The passage of time is measured by a fictional global clock (e.g., that spans the set of natural integers). Processes in the system do not have access to the fictional global time.
Each process of the distributed system executes a single instance of a distributed protocol 𝒫 composed of a set of algorithms, i.e., each process is running an algorithm. Processes can exhibit a Byzantine behavior  (i.e., they can arbitrarily deviate from the protocol 𝒫 they are supposed to run). A process affected by a Byzantine behavior is said to be faulty, otherwise we refer to such process as non-faulty or correct. We make no assumption on the number of failures that can occur during the system execution. Processes communicate by exchanging messages via communication channels. We say that a communication channels are asynchronous if the is no upper bound on the message delivery delay. Contrarily, communication channels are synchronous if messages sent by correct processes at time t are delivered by correct processes by time t+δ. Finally, communication channels are weakly synchronous if there exist an unknown a priori time τ after which the communication channels behave as synchronous.  We specify time to time the channels synchrony assumption considered, when left untold we consider asynchronous channels.


The BlockTree being now a shared object replicated at each process, we note by  bt_i 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 updates.  We also use subscript  i to indicate that the operation occurred at process i: update_i(b_g,b_i) indicates that i inserts its locally generated valid block b_i in bt_i with b_g as a predecessor. Updates are communicated through send and receive operations. An update related to a block b_i generated on a process p_i, sent through send_i(b_g,b_i), and received through a receive_j(b_g,b_i), takes effect on the local replica bt_j of p_j with the operation update_j(b_g,b_i). 


We assume a generic implementation of the update operation: when process i locally updates its BlockTree bt_i  with the valid block b_i (returned from the consumeToken() operation), we write   update_i(b,b_i). When a process j execute the receive_j(b,b_i) operation, it locally updates its BlockTree bt_j by invoking the update_j(b,b_i) operation.  

In the remaining part of the work we consider implementations of BT-ADT  in a Byzantine failure model where the set of events is restricted as follows.

	The execution of the system that uses the BT-ADT =(A, B, Z, ξ_0, τ, δ) in a Byzantine failure model defines the concurrent history  H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ (see Definition <ref>) where we restrict E 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 the predicate P and,  (iv) send, receive and update events generated at correct processes.

 
 




In this Section we consider a message passing system model and we show the

(i) impossibility to achieve Strong Prefix without Consensus and impossibility to achieve Eventual Prefix if at least one message sent by a correct process is lost. 

TBC: 
(ii)Eventual Prefix is impossible in an asynchronous system
(iii)Eventual Prefix is impossible if the interval between the generation of two successive blocks is less than the upper bound on the message delay. 

(iv) Impossible to solve Strong Prefix without the Frugal oracle with k=1.







 §.§ Communication Abstractions







We now define the properties that each history H generated by a BT-ADT satisfying the Eventual Prefix Property has to satisfy and then we prove their necessity.


	A concurrent history H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ of the system that uses a BT-ADT satisfies the Update Agreement if satisfies the following  properties:
	
		
  * R1. ∀ update_i(b_g,b_i) ∈ H,∃ send_i(b_g,b_i)∈ H;
		
  * R2. ∀ update_i(b_g,b_j) ∈ H, ∃ receive_i(b_g,b_j) ∈ H such that receive_i(b_g,b_j) ↦ update_i(b_g,b_j);
		
  * R3. ∀ update_i(b_g,b_j) ∈ H, ∃ receive_k(b_g,b_j)∈ H, ∀ k.
	

Figure <ref> depicts a concurrent history that satisfies the Update Agreement properties. 


In the following, for ease of notation we consider that the selection function f ∈ℱ returns directly also the genesis block.


	Property R1 or Property R2 are necessary conditions for any protocol 𝒫 to implement a BT-ADT generating histories H satisfying the Eventual Prefix property.



	
	Let us assume that there exists a protocol 𝒫 implementing a BT-ADT that generates histories H satisfying Eventual Prefix property but not Property R1 or Property R2. Thus, in H there is some update u that is not sent to the other processes (R1) or once received, u is not locally applied (R2). Let us consider the following history where R1 is not verified and process i issues the first update event in H. 

	Let us construct the following execution history H. i issues the update_i(b_0,b_i^') (thus bt_i=b_0 ^⌢ b_i^') but not the send_i(b_0,b_i^') event. It follows that if there is no send_i(b_0,b_i^') event in H then in H are no present any receive_j(b_0,b) events, j ≠ i and thus not process j ≠ i can issue update_j(b_0,b_i^') (on the other side, if R2 is not satisfied, even if the the receive_j(b_0,b) event occur then update_j(b_0,b_i^') may not occur), thus ∀ j≠ i, bt_j=b_0. Let us assume that i performs a read() operation, the selection function f∈ℱ is applied on bt_i=b_0 ^⌢ b_i^'. 
	By the score function definition it follows that score(b_0 ^⌢ b_i^')> score(b_0). Thus if i issues a read() operation after update_i(b_0,b_i^') it returns a blockchain such that score(b_0 ^⌢ b) and the possible infinite read() operations issued by other processes always return blockchain such that score(b_0), violating the Eventual Prefix property. The construction of H can be completed iterating the same reasoning for an infinite number of append() operation issued by i, thus H violates the Eventual Prefix Property leading to a contradiction. 
	



	Property R3 is a necessary condition for any protocol 𝒫 to implement a BT-ADT generating histories H satisfying the Eventual Prefix property.



	Let us assume that there exists a protocol 𝒫 implementing a BT-ADT that generates histories H satisfying Eventual Prefix property but not Property R3. Thus, in H there is some update_i(b,b_i^') u at some process i such that the receive_j(b,b_i^') events do not occur at all processes j ≠ i. 
Let us consider a system composed by three processes, i,j and k. The system execution generates the following history H where R3 is not verified. In particular, in H are present the update_i(b_0,b_i ^'), receive_j(b_0,b_i ^') events but there is no any receive_k(b_0,b_i ^') event. It follows that bt_i=bt_j=b_0 ⌢ b_i^' and bt_z=b_0.
	We apply the same argument as for Lemma <ref>. Let us assume that j and k perform read() operations. Such operation returns the result of f(bt_j) and f(bt_k) respectively. By the score function definition it follows that score(b_0 ^⌢ b_i^')> score(b_0). If j issues a read() operation after update_j(b_0, b_i^') it returns a blockchain with score(b_0 ^⌢ b) and the other read() operations issued by k will always return blockchain with score(b_0). The construction of H can be completed iterating the same reasoning for an infinite number of append() operation issued by i, thus H violates the Eventual Prefix Property leading to a contradiction. 
	



	
	The update agreement property is necessary to construct concurrent histories H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ generated by a BT-ADT that satisfy the BT Eventual Consistency criterion.



	The proof follows directly from Lemma <ref>, Lemma <ref> and the definition of Eventual BT consistency criterion. 
	


Considering Theorem <ref> and Theorem <ref> the next Corollary follows.


	There not exists a concurrent history H=⟨Σ, E, Λ, ↦, ≺, ↗⟩ of the system that uses a BT-ADT that satisfies the Strong BT consistency criterion but not the Update Agreement.


















In the following we consider a communication primitive that is inspired by the Liveness properties of the reliable broadcast <cit.>. We will prove that this abstraction is necessary to implement Eventual BT Consistency.















	
	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
	

In other words, if a correct process i sends a message m then i eventually receives m and if a message m is received by some correct process (e.g., i itself), them m is eventually received by every correct process.


	The LRC abstraction is necessary to for any BT-ADT implementation that generates concurrent histories that satisfies the BT Eventual Consistency criterion.



	The proof done by generating a concurrent history H that violates the LRC properties and showing that H also violate the Update Agreement properties.  For Theorem <ref> the Update Agreement properties are necessary condition to implement BT-ADT that generates concurrent histories that satisfies the BT Eventual Consistency criterion. 

	Let us consider H where at process n occurs the event update_n(b,b_n) and send_n(b,b_n) and where the LRC2 property is not satisfied. 
	If LRC2 is violated then in H we can have that there exist some process i at which occurs the  receive_i(b,b_n) event and some process j at which never occurs the receive_j(b,b_n) event. Since at process n occurred the event update_n(b,b_n), then, for the R3 property, for each process k update_n(b,b_n) has to occur. For R2 the update_m(b,b_n) event at some process m has to be preceded by a receive_m(b,b_n) event at the same process m. Since by hypothesis not at all processes m the receive_m(b,b_n) occurs then the property is violated, violating the Update Agreement properties, which are necessary conditions to implement BT-ADT that generates concurrent histories that satisfies the BT Eventual Consistency criterion, which concludes the proof.

	


Finally, from Theorem <ref> and Theorem <ref> the next Corollary follows. 


	The LRC abstraction is necessary to for any BT-ADT implementation that generates concurrent histories that satisfies the BT Strong Consistency criterion.







 §.§ System model and hierarchy















Observation.
Following our Oracle based abstraction (Section <ref>) 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 a process takes the token to append a block it can only use the LRC communication abstraction.


	There does not exist an implementation of ℜ(BT-ADT_ SC, Θ) with  Θ≠Θ_F,k=1 that uses a LRC primitive and generates histories satisfying the BT Strong consistency.



	Let us assume that there exist a BT-ADT implementation that satisfies the BT Strong consistency criterion refined with a Θ-ADT different from Θ_F,k=1, which implies that forks in the bt can occur. Let us now construct the following history H generated by the system execution at two correct processes i and j. At the beginning bt_i=bt_j=b_0. 
	At the same time instant t_0 both processes invoke append(b_1) and append(b_2) operations respectively and b_1, b_2 ∈ℬ'. By definition, the append() operation applies a selection function f ∈ℱ to select the block from the BlockTree to which the new block has to be appended, in this case such block is f(bt_i)=f(bt_j)=f(b_0)=b_0. 
	By construction, b_i, b_j ∈ℬ', let us assume that a fork occurs and both  append() operations take place and update events are triggered. Since an LRC primitive is used, each update is sent to the other processes. Since synchronous channels are employed, then by time t_0+δ the update events are delivered by i and j.
	
	Let us consider that H contains the following ordered events: update_i(b_0,b_j) ↦ update_i(b_0,b_i) and update_j(b_0,b_i) ↦ update_j(b_0,b_j). It follows that at a time instant t<t_0+δ it can occur that bt_i=b_0 ^⌢ b_j and bt_j=b_0 ^⌢ b_i. Let us finally assume that at time t both i and j issue a read() operation. By definition it returns the result of the selection function f to the BlockTree. For both processes the BlockTree is a blockchain, thus the read() operations returns b_0 ^⌢ b_j at i and b_0 ^⌢ b_i at j violating the Strong Prefix property leading to a contradiction. Thus, there no exists an implementation of a BT-ADT refined with a Θ-ADT different from Θ_F,k=1 that generates histories satisfying the BT Strong consistency even in a fault-free environment.
	


From Theorem <ref> the next Corollary follows.

	Θ_F,k=1 is necessary for any implementation of any ℜ(BT-ADT_ SC, Θ) that generates histories satisfying the BT Strong consistency.



Thanks to Theorem <ref> the next Corollary also follows.


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




As direct implication of the Theorem <ref> we can eliminate from the hierarchy in Figure <ref> both ℜ(BT-ADT_ SC, Θ_P) and ℜ(BT-ADT_ SC, Θ_F,k>1), since in both cases the Θ-ADT employed allows forks, thus such enriched ADTs can not generate histories that satisfies the BT Strong consistency criterion. The resulting hierarchy is depicted in Figure <ref>.


































































	There does not exist an implementation of a BT-ADT refined with a Θ_P-ADT that uses the LRC primitive and generates histories satisfying the BT Eventual consistency in an asynchronous communication system. 



	
	Let us proceed by constructing the following execution history H. Let us consider two correct processes i and j. Both processes issues append() operations and for the LRC primitive all the update_i events in H are followed by receive_j events and vice versa. W.l.g. we assume that the selection function f always returns the longest chain and in case of tie selects a branch based on the lexicographical order. 
	Given that the system is asynchronous the following scenario may happen. At the beginning both, i and j issue respectively an append(b_1) operation on f(bt_i) and an append(b_2) operation on f(bt_2), which in this case is equal to b_0 and both of them succeed since we are considering  Θ_P-ADT Oracle, that allows forks. Thus, in H there is update_i(b_0,b_1) ( bt_i=b_0 ^⌢ b_1) and update_j(b_0,b_2) (bt_j=b_0 ^⌢ b_2). Let us assume that i issues another append(b_3) operation before delivering receive_j(b_0,b_2), then i issues update_i(b_1,b_3) (bt_i=b_0 ^⌢ b_1^⌢ b_3). Symmetrically, j issues update_i(b_2,b_4) (thus bt_j=b_0 ^⌢ b_2^⌢ b_4). This scenario can be iterated forever, having that i has always the longest branch composed by blocks labeled with odd numbers whilst j has always the longest branch composed by blocks labeled with even numbers.
	It follows that the possible infinite read() operations issued by i and j always return blockchains sharing b_0 as maximum prefix, while by construction for all the read() operation applied on bt ≠ b_0,  score(f(bt_i))> score(b_0) and score(f(bt_j))> score(b_0), which violates the Eventual Prefix property. 	



	There does not exist an implementation of a BT-ADT refined with a Θ_P-ADT that uses the LRC primitive and generates histories satisfying the BT Eventual consistency in an synchronous communication system if the interval T between the generation of two consecutive blocks is always smaller than δ, the upper bound on message delay. 



	The proof follows the same argument as the proof for Lemma <ref> in which processes invoke the append() operation before delivering the update messages due to a previous append() operation. In this case this scenario still holds since T < δ.





	




	There exists an implementation of a BT-ADT refined with a Θ_P-ADT and uses the LRC primitive that generates histories satisfying the BT Eventual consistency in a weakly synchronous communication system such that the interval T between the generation of two consecutive blocks is always greater than the message delay δ. 




	Let us consider the protocol described in Figure <ref> and let us suppose that such algorithm does not implement an ADT that generates and history H that satisfies the BT Eventual Consistency.
	This means that there exist two correct processes i and j that invoke the read() and append() operations infinitively often and the returned blockchains bc_i and bc_j share a maximum prefix whose score never reached the score of the whole blockchain returned by previous read() operations. In other words, the selection function f selects different branches at i and j and being f deterministic by definition then bt_i ≠ bt_j. For the LRC primitive, if some process issues append() operations then  all the update_i events in H are followed by receive_j events and vice versa.
	By hypothesis there exists an unknown a priori time instant τ after which the communication system became synchronous. Let δ be the upper bound on the message delay. Then, by time τ+δ all the receive messages will be delivered and the update applied. Then by this time bt_i=bt_j. Moreover, the interval T between the generation of two consecutive blocks is always greater than the message delay δ. It implies...TBC
	






§ MAPPING WITH EXISTING BLOCKCHAIN-LIKE SYSTEMS




This section completes this work by illustrating the mapping between different existing systems and the specifications and abstractions presented in this paper.  The following table summarizes the mapping between different existing systems and these abstractions. 
More details are given in the following sections. In those sections we refer to a permissionless system as a system where the cardinality of the process set is not a-priori known and each process can read and append into the blockchain. When we do not consider permissionless systems we explicitly state the differences.
























 §.§ Bitcoin

Bitcoin <cit.> is the pioneer of blockchain systems. Any 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 (implemented with TCP), which models a partially synchronous setting <cit.>.  Valid blocks are flooded in the system. The  getToken operation is implemented by a proof-of-work mechanism. The consumeToken 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  f selects returns 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 <cit.> have shown, under a synchronous environment assumption, that Bitcoin ensures Eventual consistency criteria. The same conclusion applies as well for the FruitChain protocol <cit.>, which proposes a protocol similar to BitCoin except for the rewarding mechanism.



 §.§ Ethereum

Ethereum <cit.> is a permissionless blockchain. Processes are characterized by their merit parameter represented by α_p (once normalized as ∑_p∈ Vα_p = 1). Contrarily to Bitcoin, where this merit parameter is representative of a computational power, that is this ability to quickly compute hash functions, in Ethereum this merit is bounded by the ability to move data in memory.  This proof-of-work mechanism is especially designed for commodity hardware. Any process p∈ V is allowed to read the BlockTree and append blocks to the BlockTree.  Processes communicate through reliable FIFO authenticated channels (implemented with TCP), which models a partially synchronous setting <cit.>.  Valid blocks are flooded in the system. The  getToken operation is implemented by a proof-of-work mechanism. The consumeToken operation returns true for all valid blocks, thus there is no bounds on the number of consumed tokens. Thus Ethereum implements a Prodigal Oracle. The  f selects returns the blockchain which has required the most work (see Section 10 of <cit.>), guaranteeing that concurrent blocks can only refer to  the most recently appended blocks of the blockchain returned by a read() operation. This function is implemented through GHOST algorithm <cit.>. Kiayias has shown <cit.>, under a synchronous environment assumption, that GHOST protocol enjoys both common prefix and chain growth properties. Ethereum thus ensures the Eventual consistency criteria.



 §.§ ByzCoin

ByzCoin <cit.> is a permissionless blockchain. Processes are characterized by their computational power represented by α_p (once normalized as ∑_p∈ Vα_p = 1). Byzcoin assumes a semi synchronous environment, that is,
in every period of length b there must be a strongly synchronous period of length s < b. The block creation process is separated from  the transaction validation one. The former one is realized by  a proof-of-work mechanism (similar to the Bitcoin's one), and the latter one is achieved by a Byzantine tolerant algorithm (i.e., a variant of PBFT <cit.>) which  creates micro blocks made of  transactions. 

The  getToken operation is implemented by a proof-of-work mechanism.
Due to the PoW mechanism, several key blocks can be concurrently created. The consumeToken operation guarantees that during  the   synchronous periods of the semi-synchronous setting  (those synchronous periods ensure  that everyone receives all the concurrent key blocks in a short period of time), a single key block  will be appended to the BlockTree by relying on a deterministic function f which selects the key block whose digest (fingerprint) has the smallest least significant bits among the concurrent key blocks. Under those assumptions, Byzcoin is an implementation of a strongly consistent BlockTree composed with a Frugal Oracle, with k=1. 

Note that transactions do not belong to key blocks but to microblocks which are created by  a variant of PBFT where (i) the committee members are the miners of the last w appended key blocks in the BlockTree  as returned by a read() operation; (ii)  each committee member receives a voting share for each block it has created blocks among these w ones, and (iii)  committee members are  organized on a tree rooted at the leader, and (iv) this  leader is the process that invoked the last  successful consumeToken operation. 




 §.§ Algorand


Algorand <cit.> is an algorithm dedicated to permisionless blockchains. 
Users are characterized by the quantity of coins (stake) they own, represented by α_p once normalized as ∑_p∈ Vα_p = 1. Algorand  assumes a synchronous setting (rounds) in order to ensure that (i) with overwhelming probability all users agree on the same transactions (safety property) and (ii)  new transactions are added to the blockchain (liveness property). Note that safety holds even in a semi synchronous environment.  Users  communicate among themselves through reliable communication channels (implemented via TCP).
Algorand algorithm relies on two main ingredients: a cryptographic sortition and a variant of a Byzantine agreement algorithm.
The cryptographic sortition implements the getToken operation by selecting the block proposer.
This is achieved by selecting at random  a committee (that is a small fraction of users weighed by their currency balance α_p, which boils down to a proof-of-stake mechanism) and providing them a random priority, so that with high probability, the highest priority committee member will be in charge of proposing the new block for the current round. 
The variant of Byzantine agreement algorithm BA* implements the consumeToken operation, that is the commitment to append this new valid block in the blockchain. 
BA* guarantees that in a favorable environment (strongly synchronous environment augmented with synchronized clocks), if all honest participants have received the same valid block, then this block will be appended to the blockchain (see Lemma 2 <cit.>). On the other hand, if there is no agreement on that block (because the highest priority committee member is malicious or the network is not strongly synchronous), then BA* may create forks with probability less than 10^-7 (Theorem 2 <cit.>). This makes  Algorand
 a probabilistic implementation of a strongly consistent BlockTree composed with a Frugal Oracle, with k=1.




 §.§ PeerCensus



PeerCensus <cit.>  is a permissionless blockchain. Processes are characterized by their computational power represented by α_p (once normalized as ∑_p∈ Vα_p = 1). PeerCensus  assumes a semi synchronous environment, that is,
in every period of length b there must be a strongly synchronous period of length s < b.  PeerCensus is not  strictly speaking a blockchain-based algorithm (as Bitcoin or Byzcoin), in the sense that it does not store a sequence of application transactions, but provides a secure and fully distributed timestamping service. This service is implemented by a 
dynamic Byzantine tolerant consensus algorithm which tracks the committee members of the consensus algorithm through the creation of chained key blocks. The getToken operation is implemented by a proof-of-work mechanism, and the  consumeToken operation, implemented by the Byzantine consensus, commits a single key block among the concurrent ones, that is returns true for a single token, as long as no more than a 1/3 of the committees members are Byzantine (secure state). Theorem 1 <cit.> states that the secure state is reachable with high probability if the computational power owned by the adversary, α_A, is less than 1/3. Thus under these assumptions PeerCensus  implements a strongly consistent BlockTree composed with a Frugal Oracle, with k=1.   Note however that in <cit.> the authors have analyzed the probability that PeerCensus reaches a secure  state by examing the composition of successive quorums, and have shown that this probability is decreasing as a function of α_A. For instance, if α_A = 1/4, then the probability that PeerCensus reaches a secure state is only equal to 1/3. 
 




 §.§ Red Belly

Red Belly <cit.> 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 as a merit parameter set to α_p = 1/|M| while each process p ∈ V ∖ M has a merit parameter α_p = 0. Processes are asynchronous (i.e.,  there is  no assumption on their respective computational speed) and are connected with partially synchronous <cit.> (i.e., messages are delivered in unknown but finite time), reliable and authenticated communication channels. 
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 ℬ𝒯↦ℬ𝒞 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 <cit.>). 
 
 

 §.§ HyperLedger Fabric

 HyperLedger Fabric <cit.> is a system allowing to deploy and operate persmissioned blockchains. Any process p∈ V is allowed to read the BlockTree, however, only a subset of M ⊆ V is allowed to append blocks to the BlockTree. Every process of M has the same merit parameter α_M = 1/|M| while processes of V ∖ M have a null merit parameter. 
HyperLedger Fabric assumes eventual synchrony and reliable channels. Transactions are executed by a dedicated set of processes called endorsers. Executed transactions are then ordered through atomic broadcast primitive so as to gather them into a block. HyperLedger Fabric relies on a leader election to determine which process will generate the next block. Transactions are appended in a block until a stop condition is met. A stop condition refers either on a maximal number of transactions in a block or a maximal elapsed time since the first transaction included in the block. The block is then broadcasted and a new block is created to gather new incoming transactions.
By construction, HyperLedger Fabric ensures that a unique token (k=1) is consumed, thus HyperLedger Fabric implement a strongly consistent BlockTree.
























































§ CONCLUSIONS AND FUTURE WORK


The paper presented an extended formal specification of blockchains and derived interesting conclusion 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.  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. 



§ ACKNOWLEDGMENT

We are grateful to Mathieu Perrin and anonymous reviewers for their insightful comments on a previous version of the current paper.








plain



