2024-02-09
· 2 min read
Present
- Started "serious" work with the team on modeling and simulating Peras protocol.
- Main focus is currently on ensuring all the pieces of the puzzle fit together:
- Yves is working on the modelisation in Agda of the protocol, leveraging previous work done in Coq on Ouroboros Praos
- Brian is experimenting with simulation of Praos/Peras in Haskell, with the goal of being able to visualise the evolution of the system over large periods of time and simulating the impact of the protocol parameters
- Arnaud is exploring model-based testing, towards applying quickcheck-dynamic generated tests on a simulated network of nodes
- Creative engineering started work on a Network simulator in Rust and we have made some preliminary experiments to connect such a simulator to tests generation process
- Quviq SoW has been completed and is now in the hands of Procurement to be hopefully finalised in the forthcoming days
Future
- Quviq SoW signature and execution
- Continue work on the whole "Simulation process", fitting the various parts together:
- Express (and prove?) some properties in Agda...
- ... then generate code from Agda to use in Model-based tests generation and simulations ...
- ... to run properties against code and produce simulation results.
- We plan to start recording hosting monthly demos
Issues
- What's the situation of the alternative remediations for faster settlement proposed during the Edinburgh Peras workshop?
- Open-sourcing the repository is not desirable while research is still working on the paper