Skip to main content

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