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)