Present​

• Completed CIP for Peras as self-contained literate Agda with supporting technical analyses and arguments
• Worked on soundness proofs for Peras executable specification
• Briefed Intersect's Core Infrastructure (CI) working group on Peras
• Coordinated plan with Quviq for including adversarial actions in conformance tests
• Created standalone version of IOG Agda Prelude

Future​

• Reviews of Peras CIP

Issues​

• We need a decision process for determining when to move the Peras CIP from its current draft state (internal review) to the ready to review state (public review).

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