Skip to main content

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.