Merge pull request #21 from Isaac-DeFrain/main

Mempool & Tenderbake
tezedge · Dec 14, 2021 · b77695f · b77695f
2 parents 158b0f3 069e768
commit b77695f
Show file tree

Hide file tree

Showing 5 changed files with 177 additions and 88 deletions.
diff --git a/consensus/Tenderbake/README.md b/consensus/Tenderbake/README.md
@@ -1,21  1,49 @@
 # Tenderbake specification
 
-For more information about Tenderbake, see [Tenderbake](./Tenderbake.md)
 For more information about Tenderbake and dynamic repeated consensus, see [Tenderbake](./Tenderbake.md)
 
 For the TLA  spec, see [Tenderbake spec](./Tenderbake.tla)
 
 ## Spec design
 
-TODO
 This specification follows the design of Tenderbake laid out in [Tendbake - A Solution to Dynamic Repeated Consenses for Blockchains](https://arxiv.org/abs/2001.11965). Liberal simplifications/abstractions are used to produce a tractable spec and will be explained below. As with all TLA  specs, we specify the consensus protocol as an automaton (state machine).
 
 ### Possible actions of the state machine
 
 The spec contains both *correct* and *faulty* processes. Correct processes follow the protocol while faulty processes behave arbitrarily. We describe the actions allowed by correct processes.
 
 #### Propose
 
 At the beginning of each round, a designated committee member, called the *proposer*, can propagate a new block to be preendorsed, then endorsed by the committee.
 
 #### Preendorse
 
 After a value has been proposed, the committee members signal their intention to "lock" on this value by boradcasting preendorsement messages.
 
 #### Endorse
 
 If a member sees a quorum of preendorsement messages for a value, they broadcast an endorsement message for that value. If a member sees a quorum of endorsement messages for a value, they consider this value to be correct and add the block to their local chain.
 
 #### Observation
 
 Observation actions are only enabled for noncommittee processes, . The committee depends on the level, not all processes will be part of each committee. These observers simply handle the network messages and adjust any corresponding local information.
 
 #### Timeout
 
 At any point in the execution of the state machine, it is possible for a correct process to timeout. When this occurs, the process pulls chains from all other processes.
 
 ### Simplifications/assumptions
 
 - dynamic level comittees
   - committes depend only on the level
   - proposer depends on the round within the level
-- `n >= 3f   1` where `n` is the number of bakers and `f` is the number of faulty bakers
 - `n >= 3f   1` where `n` is the number of bakers (correct   faulty processes) and `f` is the number of faulty bakers (processes)
 - all committee members have the ability to communicate with one another
-- no mempool
-- TODO
 - bakers do not maintain or exchange mempools
 - chains are always pulled from all other processes (complete network topology)
 
 ## Run the code = verify the specification's properties
 
-TODO
 The spec's properties can be found [here](./Tenderbake.tla#L1006). To verify these properties using TLC,
 1. Clone the repo
 2. From the Tenderbake directory (/consensus/Tenderbake), do `tlc MC_safety.tla`
diff --git a/consensus/Tenderbake/Tenderbake.md b/consensus/Tenderbake/Tenderbake.md
@@ -40,8  40,15 @@ Each round consists of *three* phases:
 - `ENDORSE`
   - if a baker has a preendorsement quorum for a value `v`, they endorse `v`
   - `Endorse` messages are broadcast to committee members along with the pQC justifying the endorsement
-  - if a baker has an endorsement quorum for  value `v`, they decide `v`
   - if a baker has an endorsement quorum for value `v`, they decide `v`
 
 ## Messages
 
-Message types and corresponding payloads
 There is a message type and corresponding payload for each phase. The message types and corresponding payloads are:
 
 | Type | Payload |
 |------|---------|
 | Propose         | 4-tuple of endorsement quorum certificate, endorsable value, endorsable round, and preendorsement quorum certificate |
 | Preendorse      | value |
 | Preendorsements | preendorsement quorum certificate |
 | Endorse         | endorsed value |