For every s,s′∈ S, i ∈ I, t(s,i)≠t(s′,i) 
s≠s′.
Warning:
this component has no documented requirements. A new requirements page should be created and linked to this component.
|
Contents |
Consensus is the fundamental backbone of the GCL. It is the thing which provides global agreement on the inputs to a set of composable blockchains, and stakes signifcant economic collateral on the promise that those inputs will never change (fulfilling the Globally trusted requirement). In this way it forms the basis of composability protocols and the applications that use them. The inputs finalized by Espresso consensus are also treated as inputs to Espresso’s own state machine, which in a sense makes Espresso a blockchain in itself.
Specifically, Espresso uses the HotShot consensus protocol, which builds on the HotStuff protocol by adapting it to
High data-throughput use cases
Permissionless proof of stake
TODO give an overview of HotShot, linking to other pages for details of sub-protocols. I would love to try to specify consensus as a pure function from state to state. This would drastically simplify catchup by telling us exactly what data needs to be persisted so that we can restart in exactly the same state as if we had never shut down at all. The following is an incomplete attempt at that.
The consensus state machine is a tuple (S,I,O,t) consisting of
A set of possible states S
A set of input events I
A set of output events O
A transition function t : (S × I) → (S × [O]), mapping each state and possible input to a new state along with a sequence of output events.
This state machine satisfies several properties
For every s,s′∈ S, i ∈ I, t(s,i)≠t(s′,i) s≠s′.