Property Based Testing the spec of IMTs
In order to explore different alternatives to combine verification and property-based testing, we will take advantage of the fact that the predicates used for the functional verification of the Incremental Merkle Trees library (See nomadic-labs/private/tzchain#66,!7 (merged)) are small boolean predicates. This gives us the opportunity to envision a process to share the specification between the development, testing and verification phases.
Tasks
!6 (closed)
Experiments in-
Implement in OCaml the basic API specs/predicates from the Coq spec #1 (closed) -
Split into different files/modules: implementation, the instrumentation, specs, tests_suits proper. -
Explore QCheck to test the incrementality spec. -
Explore Crowbar to test the incrementality spec. -
Build system for experiments.
Sapling library targets
-
Refactor the instrumentation and test_suite to use the real code. It will require working on top of the sapling integration branch. -
Clean up build system and make tests/docs comply with tezos/tezos#900 (closed).
Integration
-
Refactor the library to integrate the tests with the protocol branch. -
Reflect towards a general methodology for designing property based tests for the codebase. -
Integration with Alcotest? Alcotest is the framework used in the code-base for unit tests, both crowbar and qcheck can be integrated with alcotest.
Edited by Germán Delbianco