2024-07-05
· One min read
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
- Automated using
- 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
agda2hsawkwardness and bugs