Skip to main content

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