# FlexBFT: A Flexible and Effective Optimistic Asynchronous BFT Protocol
## 3 Problem Formulation
### Component Definitions  
Our goal is to achieve an atomic broadcasting protocol (ABC). ABC is frequently implemented via ACS, where ACS typically comprises components such as AVID, ABA, and MVBA, which are defined as follows:  
**AVID (Asynchronous Verifiable Information Dispersal)**  
The purpose of the AVID protocol is to disperse a message from a sender to other nodes in a group of nodes, which may include adversaries. An AVID protocol has two functions: DISPERSE (\(M\)), which a dispersing client invokes to disperse a message \(M\) to \(n\) nodes, and RETRIEVE, which a (possibly different) retrieving client invokes to retrieve the message \(M\). AVID is frequently employed for implementing RBC (reliable broadcast) and satisfies the following properties:  
* Termination: If an honest client invokes DISPERSE (\(M\)) and no other client invokes DISPERSE at the same instance, then every honest node eventually finishes the dispersal phase.
* Agreement: If any honest node finishes the dispersal phase, all honest nodes eventually finish the dispersal phase.
* Availability: If an honest node has finished the dispersal phase, and some honest client initiates RETRIEVE, then the client eventually reconstructs some message \(M^{\prime}\).
* Correctness: If an honest node has finished the dispersal phase, then honest clients always reconstruct the same message \(M^{\prime}\) when invoking RETRIEVE. Furthermore, if an honest client invoked DISPERSE (\(M\)) and no other client invokes DISPERSE at the same instance, then \(M^{\prime}=M\).  
ABA (Asynchronous Binary Agreement Protocol)  
The ABA protocol's purpose is for a group of nodes, which may include adversaries, to each provide a 0 or 1 as input. At the end of the protocol, each node outputs one bit and satisfies the following properties:  
* Agreement: If an honest node outputs b, then all honest nodes output b.
* Termination: If all honest nodes provide the same input b, then all honest nodes output b.
* Validity: If an honest node outputs b, then at least one honest node had b as input.  
MVBA (Multivalued Validated Byzantine Agreement)  
MVBA allows agreement on arbitrary values instead of being restricted to binary values. The protocol has a global, polynomial-time computable predicate \(Q\) known to all nodes, which is determined by the particular application. The basic idea of the protocol is that each party proposes a (different) value that contains certain validation information as input and outputs a value that satisfies \(Q\) as the decision value. The protocol ensures that the decision value was proposed by at least one party. Each honest node only inputs a value to MVBA that satisfies \(Q\). MVBA satisfies the following properties:  
* Termination: If every honest node \(P_{i}\) inputs with an externally valid value \(v_{i}\), then every honest node outputs a value;
* External validity: If an honest node outputs a value \(v\), then \(Q(v)=\textit{True}\);
* Agreement: All honest nodes that terminate output the same value;
* Integrity: If all nodes are honest and if some nodes output \(v\), then some nodes proposed \(v\).  
ACS (Asynchronous Common Subset Protocol)  
The ACS protocol runs in a system composed of V nodes, where the number of adversaries satisfies \(n\geqslant 3f+1\). Each node proposes a set of suggested values as input. At the end of the protocol, each node selects a subset of these suggested values as output, satisfying the following properties:  
* Validity: If an honest node outputs a set S of suggested values, then S contains at least \(2f+1\) suggested values, with at least \(f+1\) coming from honest nodes.
* Agreement: If an honest node outputs a set S of suggested values, then all honest nodes output S.
* Totality: If every honest node provides an input to the ACS protocol, then eventually, all honest nodes will receive an output.