Simulation of short Leios via nodes interacting through mini-protocols

[Saizan]

Details

• [ ] Implement nodes that follow the short Leios protocol, using simplified but realistic "mini-protocols" to share blocks and other necessary state with their peers. Ledger modeling will be limited to a parameter for cost of validating blocks, and nodes will directly generate Leios' Input Blocks.
• [ ] Produce visualizations of networks of nodes, under different topologies and parameters.
• [ ] Measure the following quantities, which are useful to estimate performance and resource cost of the protocol:
  • diffusion latency for each kind of block/message
  • total data transmitted per unit time.

Definition of Done

We can provide simulation traces and visualizations, and extract measurements of the above quantities.

[ghost]

Does this mean you plan to define specific mini-protocol(s) for Short Leios?

[Saizan]

Yes, we will iterate on such protocols as the way the different nodes in the simulation communicate.

I assume we won't necessarily end up with DoS-proof protocols, or at least won't commit the time for that analysis, but we want the overall structure of them to actually be feasible in practice.

[ghost]

I think it would be useful to have a rough idea how this work will integrate formal specification in Agda from @WhatisRT and @yveshauser

[dcoutts]

We intend somehow to do testing against an executable version of the specification, derived from or related to the agda specification. The presentation yesterday on the use of dynamic-quickcheck with an executable version of the small step semantics provides a plausible roadmap.

[WhatisRT]

I'd honestly just do the style of conformance testing we've done for the ledger. We've gotten really good results with it, it's relatively low effort and it allows for negative testing.

All we'd need to do for that is to add translations for all the message and state types between the implementation & spec. Then you can throw arbitrary states & traces at both of them and see how they react, and if they do the same thing we're good.

[Saizan]

@WhatisRT is there documentation describing the style of conformance testing used for the ledger?

[ghost]

What can be problematic is that this style assumes the state of the model can be directly projected into a state for the implementation. This is not a problem in the ledger case because the conformance tests target only a single implementation, in Haskell, but it's not what we would like for Leios: there could be, and actually there will be, implementation in other languages (e.g Rust) and in this case forcing the implementation to use the model's state will be annoying.

[dcoutts]

I'm not worried about abstracting from the prototype's state to the model's state. I'm worried about the non-determinism. We can't use simple lock-step testing as with a ledger spec/impl. We need a strategy that accommodates the concurrency and non-determinism.