ΔQ model for short Leios to harmonise Haskell and Rust simulations

[rkuhn]

While the intended level of detail (or closeness to an actual implementation) of the Rust and Haskell simulations differ, we want both of them to implement the same basic model of Leios and of the peer to peer network supporting it. To this end, we create a third description that is as abstract as possible but captures the timeliness and resource usage aspects of Leios protocol behaviour as set forth in the Agda spec plus timing as documented by research.

We achieve alignment of the simulations by modelling both the Rust and Haskell simulators using ΔQSD, making sure to employ design parameters and the protocol as formally specified but adapting to each simulation’s level of fidelity. Inconsistencies between ΔQ and simulation results need to be explained by either finding effects that are hard to treat in ΔQSD (a likely example being TCP window collapse) or identifying bugs in either the ΔQ expression or the simulation.

Once this work is complete, we document the approach, the lessons learnt, and a user guide for the ΔQSD tooling developed and improved as part of the endeavour. This will allow others — in particular that wider Cardano community — to benefit from the tools and knowledge.

Definition of Done:

• match ΔQ expression to Rust simulation
• match ΔQ expression to Haskell simulation
• write technical report detailing the observed differences and the findings during the process
• publish report and ΔQ tooling + user guide on the website