2024-03-22
· 2 min read
Present
- Built a first ΔQ model reconstructing the Cardano network high-level modelling originally published in the ΔQSD paper
- Discussed with other innovation streams how ΔQ competes or complements network simulation
- Started work on a Technical Report, currently including only part of ΔQ analysis. The goal is to be able to publish this report as an outcome of Paris Workshop
- Continued refactoring of IOSim node, including contra-tracer based logging to improve observability of the prototype behaviour and standardize analysis
- IOSim node now implements a faithful block diffusion mimicking real-life process
- Started concrete work with Quviq on Agda ⇔ Quickcheck integration and on a first simple example
Future
- Prepare and deliver Monthly Demo, should include network congestion simulation, initial ΔQ analysis of Praos and Peras, new formal model of algorithm in Agda
- Realign various parts of the code (Agda, Haskell node, quickcheck tests, Rust node) over shared interfaces and common types
- Complete prototype implementing new version of the protocol (with certificates)
- Express more interesting properties in QuickCheck
- Work with Quviq on Agda/QuickCheck integration
- Polishing Agda model and more work on proofs
Issues
- How do we make our formal modelling in Agda effort more efficient for both Research and Engineering?
- Brian will be on PTO the first week of April