Skip to main content

2024-06-28

· One min read

Present​

  • Peras workshop at the University of Edinburgh
    • Agda proofs
    • Conformance testing
    • Peras cryptography
    • Delta-Q simulations
    • Protocol simulation and visualization
    • Markov-chain simulations
    • Tasks for remainder of PI6
  • Settled Peras versioning
    • pre-alpha: basic algorithm without pre-agreement
    • alpha: full algorithm, including pre-agreement
    • beta: final, polished version
  • Finalized details of certificate and vote diffusion and persistence
  • Refactoring decidable portions of Agda code to be compatible with agda2hs

Future​

  • Complete Agda-to-Haskell conformance test framework
  • Protocol simulation
  • Markov-chain simulations of Peras margin and reach
  • Plan for post-PI6 efforts

Issues​

  • (none)

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.