Present​

• Met with Intersect Consensus WG to discuss CIP process as it relates to Peras
• Simulation of margin and reach
• Began internal reviews of Peras technical report
• Dynamic QuickCheck tests for peras-markov
• Added configurable adversarial behaviors to Markov-chain simulation
• Website improvements (rendering as PDF)

Future​

• Rough draft of CIP
• Continue internal reviews of Peras website, technical report, Agda specification, and online simulator

Issues​

• A CIP to establish a "consensus category" is required prior to submitting specific CIPs like Peras

Present​

• Completed reviewable version of second technical report
• Deployed Peras website for internal review
• Additional work on soundness proofs
• Dynamic quickcheck tests for Markov-chain simulator
• Analyzed papers on adversarial scenarios, in preparation for improved Markov-chain simulation

Future​

• Complete soundness proofs
• Internal reviews of Peras website, technical report, Agda specification, and online simulator

Present​

• Analytics for adversarial scenarios
• Reach/margin computations for settlement
• Healing-time computations
• Settled on strategy for handling non-determinism in executable specification
• Additional work on soundness proof
• Second technical report ready for final edits
• Planned Peras tasks for PI7

Future​

• Complete soundness proofs
• Review, edit, and proofread second technical report

Present​

• Conformance test based on Peras executable specification in Agda
  • Automated using agda2hs
  • State-machine property-based test using quickcheck-dynamic
  • Full coverage of voting logic
  • Successful testing of the Haskell prototype/reference implementation
• Partial completion of soundness proof
  • Agda proofs connect relational specification to executable specification
  • Linked directly to conformance tests
• Implemented cryptography for voting sortition
• Successful experiments with fast convolution for use in ΔQ modeling
• UX enhancements for simulation and visualization tools
• Updates to second technical report

Future​

• Complete soundness proofs
• Complete second technical report
• Draft CIP
• Plan PI7

Issues​

• Various agda2hs awkwardness and bugs

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)