This issue tracks the work of documenting and specifying the interaction between the consensus reactor and the P2P Layer, as well as the interactions inside the consensus reactor itself, between the consensus implementation and the consensus gossip layer.

First, this work will produce an initial set of draft specifications for the abstract behavior expected of the gossip layer and of its interactions Consensus and P2P, both in English and in Quint.
Quint specs will contain tests and will be model checked, once the tooling allows it.

Second, the specs will be refined to produce lower level abstractions, closer to the implementation level.
A primary concern here is to ensure that the abstractions can be efficiently implemented.

Third, the current implementation will be described in documented, in English, and abstracted in Quint.
The implementation will be matched to the abstract specs from the previous steps in a high level refinement mapping.
This work will possibly be completed with formal refinement mapping proofs, manual and/or automated.

The following list breaks these tasks down for easier tracking:

• Draft specification of the P2P/Gossip/Consensus interaction

  • Exploratory study of the interaction between Consensus and Gossip (done in spec/consensus: Draft specification of the P2P/Gossip/Consensus interaction #16)
    • Identify main abstractions to specify.
      • It has been identified that Gossip may be implemented as a 2P-Set CRDT.
      • It has been identified that a "garbage collection" must run in the 2P-Set; the definition will happen later.
  • Draft of high level GOSSIP-I, in English (done in spec/consensus: Draft specification of the P2P/Gossip/Consensus interaction #16)
  • Draft of high level GOSSIP-I, in Quint (done in spec/consensus: Draft specification of the P2P/Gossip/Consensus interaction #16)
  • Draft of high level P2P-I, in English (done in spec/consensus: Draft specification of the P2P/Gossip/Consensus interaction #16)
  • Draft of high level P2P-I, in Quint (done in spec/consensus: Draft specification of the P2P/Gossip/Consensus interaction #16)
    • A very simple interface was defined here and further work will be done in collaboration with other team members.
  • Quint tests for provided specs
    • P2P-I tests
    • GOSSIP-I tests
    • Quint mocks of GOSSIP
    • Quint mocks of P2P
  • Specification of the "garbage collection", GC (spec/consensus: Draft specification state Garbage Collection #608)
    • English
    • Quint
    • Tests

• Further Investigate CRDT, including implementations.

  • spec/consensus: Further investigate CRDT #610
  • spec/consensus: Investigate Delta State Based CRDT #751

• Refine specification of the P2P/Gossip/Consensus interaction (spec/consensus: Refined specification of the P2P/Gossip/Consensus interaction #17)

  • Refine GOSSIP-I, in english
  • Refine GOSSIP-I, in Quint
  • Refine P2P-I, in English (collaboration with other spec work)
  • Refine P2P-I, in Quint (collaboration with other spec work)
  • Update Quint tests.

• Document the current implementation State/Gossip/P2P interaction (docs/consensus: Document the current implementation State/Gossip/P2P interaction #18)

DoD:

• The current implementation is well understood
  • all components of the current implementation are documented
  • the interaction between the components of the Consensus reactor are is documented.
  • the interaction between the consensus reactor and the P2P layer is documented.
• There exists a formal specification of the interactions inside the Consensus reactor and between Consensus and P2P
• Mismatches between the formal specification and the current implementation are identified.

The output of this task will serve as input for #30