Skip to main content

2024-06-21

· One min read

Present​

  • Implemented cryptographic details of votes.
  • Modeling of vote diffusion via ΔQ.
  • Diagnosing problems with ΔQ libraries.
  • Voting rules and voting strings in Agda.
  • Reviewed Quviq's Agda-to-Haskell efforts for Peras.
  • Analytic studies and documentation of additional adversarial scenarios.
  • Preparations for June 25-28 working meeting in Edinburgh.

Future​

  • Additions to second technical report.
  • Complete Agda-to-Haskell efforts.
  • Meet with partner-chain stakeholders.

Issues​

  • None.

2024-06-14

· One min read

Present​

  • Switched to using IOG Agda prelude for more readable proofs.
  • Further progress on formal specification in Agda.
  • Settled cryptographic details (keys, algorithms, nonces) for votes, certificates, and membership proofs.
  • Private deployment of Peras visualizer and web site.
  • Markov-chain simulations of adversarial scenarios.
  • Met with Quviq to coordinate Agda-to-Haskell efforts.

Future​

  • Delta-Q simulations of certificates and votes.
  • Documentation of cryptographic details (keys, algorithms, nonces) for votes, certificates, and membership proofs.
  • Complete the documentation of the analytic computations of Peras behaviors.
  • Connect Agda-generated code to dynamic quickcheck properties.
  • June 25-28 working meeting in Edinburgh.

Issues​

  • No public availability yet for the Peras website, repository, and visualizations.

2024-06-07

· One min read

Present​

  • Briefed Peras to Consensus Technical Working Group.
  • Completed one more round of stakeholder interviews, focusing on SPOs.
  • Readied Peras website for deployment.
  • Major improvements to web-based interactive visualizer of Peras protocol operation, so it is ready to deploy internally at IOG.
  • Progress on formal specification in Agda.
  • Refined Haskell prototype of Peras, so it is fully in sync with the draft paper, aside from the some details of preagreement.
  • Cataloged constraints on and interactions among Peras parameters and determined reasonable defaults for simulations.
  • Collaboration with Quviq on Agda-to-Haskell efforts.

Future​

  • Connect Agda-generated code to dynamic quickcheck properties.
  • Delta-Q analyses of vote propagation.
  • Extend and document analytic computations of Peras behaviors.

Issues​

  • The in-person Peras workshop is approved for June 25-28.

2024-05-31

· One min read

Present​

  • Progress on formal specification in Agda.
  • Findings from stakeholder interviews.
  • Haskell prototype of latest version of Peras.
  • Rudimentary conformance test using Dynamic QuickCheck.
  • Collaboration with Quviq on Agda-to-Haskell efforts.
  • Visualization of prototype results.
  • Monthly status meeting.
  • Repository cleanup in preparation for it being opened to the public.
  • Skeletal web server for stakeholder-facing demonstrations.

Future​

  • Connect Agda-generated code to dynamic quickcheck properties.
  • One more round of stakeholder interviews, focusing on SPOs.

Issues​

  • The Peras protocol paper is near completion.
  • The target date for the in-person Peras meetings is the week of June 24.

2024-05-17

· 2 min read

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.