Present​

• Implemented prototype ALBA-based certificate construction and measured the CPU and message resources needed to use it for Peras voting certificates.
  • CPU resources required would not burden the node.
  • Certificate size is moderate and likely not a major concern.
• Began aligning the Peras formalization in Agda to the latest draft of the research paper.
• Translated the Peras protocol definition in the latest draft of the research paper into an executable Agda specification, used agda2hs to convert it to Haskell code, and implemented basic dynamic tests using quickcheck-dynamic
• Computed probabilities of various adversarial Peras scenarios.
• Drafted the outline for the Peras CIP.
• Mapped stakeholder relationships, concerns, and artifacts.
• Conducted a retrospective of Peras PI5.
• Hans Lahe joined the Peras team (1/3 time) as a product representative. ❤️

Future​

• Continue alignment of Peras formalization with the latest draft of the research paper.
  • voting strings
  • big-step semantics
• Simulate certificate and vote diffusion with ΔQ.
  • Review results with PNSol (Neil and Peter).
• Construct Dynamic QuickCheck tests for adversarial scenarios.
• Define requirements for conformance testing.
• Conduct stakeholder interviews.
  • Meet with Consensus team and Tweag to learn their preferences for Peras documentation, tests, and other artifacts.
  • Consider ideal form of CIP from the perspective of SPOs, CF, Intersect, etc.

Issues​

• Details of the Peras protocol may continue to be refined until the research paper is submitted before the end of May.
• An in-person meeting in late June would solidify Peras progress and resolve outstanding issues that might block PI6 objectives.

Present​

• The whole team met in person for a 2-days workshop in Paris
• Complete Technical report with simulation work results
• Quviq demonstrated Agda ↔ QC integration process on a toy protocol example

Future​

• "Publish" Peras protocol in Agda to serve as reference point for researchers and engineers
• Prepare and deliver PI Planning value demo & next PI planning objectives
• Discuss implementation phase and involvement of consensus engineer(s) in R&D stream
• Work on ΔQ vote diffusion model with PNSol team
• Model Peras property check in Agda-QCD

Issues​

Present​

• Monthly Review & Demo with slides and video
• Discussing Paris workshop agenda
• Review newest version of the protocol and integrate in Agda model
• New quickcheck-dynamic model representing more faithful interactions between environment and node

Future​

::: [!NOTE]

Part of the team will be on holidays next week so we won't post an update

:::

• Continue work on formal model in Agda, to prove knowledge propagation theorem

Issues​

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

Present​

• Got results from "split-brain" experiment with 100 nodes that basically confirm the faithfulness of the IOSim implementation and highlights some "interesting" consequences of Peras, namely that when the split-brain heals, it's not the longest chain that wins but the one with the most votes
• Started work on implementing IOSim node that represents network interactions more faithfully, eg. using a pull model that mirrors the actual ChainSync protocol implemented in the cardano-node
• Rust node passes the NetworkModel tests, with multiple nodes connected through a netsim-based layer. Aligning the implementations posed some interesting challenges, especially in the domain of time management (real vs. simulated time) and the scheduling of the various "actors" in the system
• Research shared with engineering a new version of the protocol which introduces Certificates to aggregate votes in the block headers and mostly get rid of the problematic dangling votes concept
• First meeting with PNSol on ΔQSD modelling of the protocol
• Meeting with Spyros Voulgaris on Peernet on the topic of network simulator. This is the tool that's used by researchers when they need some numbers.
• Starting significant redesign of IOSim node to cope with changes in the protocol

Issues​

• We need to improve communication between research and engineering, and how changes are shared and notified