Please describe your proposed solution.
Our Solution
Apropos is a metaprogramming toolkit for generating QuickCheck-style property tests from a logical model. This is a particularly powerful approach because the logical model in question can be complex representing thousands of solutions, each of which can become a property test. This makes thorough testing of code simpler – a lot of the heavy lifting is automated – while ensuring edge cases are not overlooked.
Market
dApp builders, Cardano developers, and auditors working to ensure applications function as designed.
Problem Space
dApps are mission-critical protocols that are required to behave as intended. This is especially true of DeFi applications that are often responsible for securing millions of dollars – sometimes billions – worth of value in their smart contract systems. When these applications enter unsound states due to improperly tested code, consequences can be dire.
Like other programming languages, Haskell/Plutus makes use of unit testing libraries to help ensure proper program behavior. Unit testing and spec testing involve checking the atomic pieces of a program for proper performance. More specifically, tests verify that specific functions return the expected computation when given a designated input.
One of the most impactful features of Haskell, however, is property testing available through libraries such as QuickCheck. With QuickCheck, developers can craft property tests that check the formal properties of a program. Inputs are then generated randomly as delineated via the type system. Testing failures signify faulty behavior and code that needs to be refactored.
Despite the extended confidence achievable with property testing limitations remain. Furthermore, QuickCheck can be cumbersome for developers to incorporate into their existing codebase, and large amounts of tailored property tests can be time-consuming to manually create. In short, automation to the extent possible can greatly reduce the burden on programmers while cutting down on development costs.
Please describe how your proposed solution will address the Challenge that you have submitted it in.
Intended Fund – Fund9: Developer Ecosystem
Fund Statement – “How can we create a positive developer experience that helps the developer focus on building successful apps?”
How do developers achieve greater confidence their dApps are properly implemented?
To address this issue, we have developed Apropos, a testing suite for the automatic generation of property tests based on a logical specification. Although in an early stage, Apropos uses a model checking approach to define how code (e.g., smart contract validators) behaves under all possible cases while exhaustively testing edge cases.
Briefly, Apropos achieves this by leveraging SAT solvers and thereby reaching beyond simple property-based testing. In principle, SAT solvers can specify all potentially satisfying variable assignments of a property to enumerate every case that, say, a smart contract validator is supposed to validate.
Overall, the project consists of a Haskell testing framework (Apropos core) for off-chain code and a Plutus-specific component, Apropos-TX, for on-chain testing. These are working frameworks used in production on some of our dApp projects. Naturally, we hope to extend their use cases while making them more ergonomic, feature-rich, and all-around easy to integrate into protocols developing on Cardano.
Our Proposal
https://github.com/mlabs-haskell/apropos-tx
While Apropos represents a powerful approach to smart contract testing, it is currently in a limited state. We aim to build out the functionality and feature set of this open-source testing suite to make it more applicable to dApps building on Cardano.
Concretely, this means:
- Adding support for GHC 9
- Modeling transactions and transaction graphs
- Extending script testing support
- Modeling CPU/Memory usage of scripts in relation to protocol parameters
- Documentation, examples, and how-tos
- Improvements and simplifications to API
- Other ease-of-use improvements
How does Apropos work alongside MLabs’ Spec eDSL, and how do these projects benefit Cardano?
MLabs is an active open-source builder on and contributor to the Cardano ecosystem. As such, we recently received Catalyst funding in Fund8 for our Specification Language for formal verification of dApps, an ongoing project. Briefly, this eDSL allows for a formal description of dApp behavior which can then be used to generate tests to validate an implementation matches the behavior of the engineering design. Used together, these testing tools can achieve an extensive amount of confidence from a logical model of a dApp while working towards a robust formal verification. This includes exhaustive outcome verifications where possible and comprehensive probabilistic verifications elsewhere.
What are the main risks that could prevent you from delivering the project successfully and please explain how you will mitigate each risk?
This proposal is low-risk as a working prototype has already been used to a limited degree in production. Moreover, the developers building out the testing suite have extensive experience with SAT/SMT solvers, property testing, formal verification, dApp development, and other areas involved. In the unlikely case that difficulties arise, the core team can also draw from the expertise of the greater MLabs development team which includes numerous developers, many of whom also have extensive experience in formal verification, compilers, and property testing.