Present​

• Summarized the status of Peras prototyping and defined next steps.
• Outlined the business value of formal methods.
• Investigated different approaches for representing a voting string in Agda: the first attempt implemented a formal language using equational reasoning and a coalgebraic style.
• Changed the reflexive transitive closure of the small-step semantics to a List-like syntax similar to what has been proposed in test-demo. This allows to express execution steps in a concise way and could be used as DSL for specifying test-cases and attack-scenarios.
• Computed the size in bytes of the various keys and certificates involved in Peras, under the assumption that it uses existing keys and crypto available to a Cardano node.
• Sketched a detailed design of what the independent voting layer would look like.
• Designed an Agda+Haskell workflow where Agda formal specifications for Peras can be made decidable and then exported as an executable specification for Haskell quickcheck-dynamic tests.
• Met with Max (Quviq) to settle next steps in their support of Peras.
  • Suggest improvements in exising Agda+Haskell workflow and code, including identifying changes to agda and/or agda2hs that would streamline the workflow.
  • Demonstrate how to convert proofs present in the workflow into property-based tests in quickcheck-dynamic.
• Started mapping the spectrum of conformance testing relevant for a Peras CIP and RFP. The overall goal is "conformance without over-specification".
• Discussed strategies for making the Peras specification readable by the broad Cardano commmunity.

Future​

• Complete Praos proofs à la Baspitter.
• Model voting and vote diffusion in detail using Dynamic QuickCheck and ΔQ.
• Construct Dynamic QuickCheck tests for adversarial scenarios.
• Continue refining requirements for conformance testing.
• Conduct additional stakeholder interviews, with an aim to define the ideal form of a Peras CIP.

Issues​

• The Peras protocol paper is expected to be submitted May 22.
• The target date for the in-person Peras meeting is June 24.

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