Property tests help ensure mission-critical dApps don’t contain vulnerabilities. However, writing tests to check every contract permutation and edge-case state is exhausting if not wholly impossible.
While QuickCheck is effective, we propose Apropos which generates thousands of property tests based on a logical dApp construct greatly increasing confidence in code and reducing the developer burden.
This is the total amount allocated to MLabs - Apropos for Property Tests
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.
dApp builders, Cardano developers, and auditors working to ensure applications function as designed.
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.
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.
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:
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.
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.
1 Month: GHC support (development ongoing) being built out and nearing completion, with notable progress underway concerning API ergonomic/usability improvements.
4 Months: Work begun on the meatier features including transaction graphs, transaction modeling, script context generation and testing support. Work also begun on resource modeling. Minor API improvements undertaken as the needs arise
8 Months: Major features above completed or nearing completion. Attention turned to nice-to-haves and usability improvements as well as thorough documentation. Tutorials and examples under development.
Hours involved: 780
Feature Total Time
API Simplifications and Improvements 120
GHC 9 Support 130
Constraint-based Script Context Generation 90
Better Validator/Minting Policy Support 90
Script Resource Consumption Modeling 70
Transaction Modeling and Transaction Graphs 140
Improve Documentation Including Tutorials/How-tos 60
Change Budget 80
Total Time 780 hours
Total Cost $62,400
MLabs has quickly become one of the premier development firms in the Cardano Ecosystem. We are an IOG Plutus Partner and work regularly with IOG to develop the Cardano blockchain and ecosystem. Our team is composed of talented developers who have helped build community projects such as:
Through our work with early-stage projects, we have one of the largest groups of Haskell/Plutus developers in the community. Developers working on our testing suite will bring their collective experience to the project and ensure a successful launch.
Moreover, MLabs has the capacity to conceptualize and ship developer ecosystem tools like Apropos. Please visit the MLabs-Haskell repo and Plutonomicon repo for more information on our contribution to open-source tooling on Cardano.
Haskell and Plutus Engineer
Ari works on testing infrastructure at MLabs. Ari has previously worked as a software consultant before joining MLabs in 2021. Ari is primarily interested in functional programming and correct software.
Before joining MLabs in 2022, James worked on developing his own programming language and compiler, a subtyping calculus of constructions. James is particularly interested in type theory and optimizing compilers, with a focus on beta optimality and managing memory using linear types and call-graph-based arena allocation.
This is a possibility but remains to be determined. Apropos is a highly-effective testing suite for Plutus smart contracts and an open-source initiative. If we continue to see adoption among community projects – something we are confident in – we will continue to integrate community feedback via GitHub issues, etc. In so doing, we may support further features and functionality upgrades per this community input by applying again to future Catalyst rounds.
We will measure:
We expect growth/positive results in these areas and are committed to meeting the milestones we have established throughout this proposal.
Success for this project involves a timely execution of the feature set described. As mentioned, this project is already in an MVP state, so there are no large hurdles expected towards achieving our goals. This success can be viewed by the public via the number of features merged to the repo as well as the number of resolved issues. While a handful of Cardano dApps under development have already adopted the testing suite, a key measure of success is the expansion of this number and the general acceptance of Apropos by the Plutus dev community.
Sure enough, this proposal stands to benefit the Cardano community in several key ways:
1) Best Practices: Apropos allows developers to generate thousands of property – perhaps eventually millions – of property tests to ensure the validity of their protocol model.
2) Testing and Reliable Implementation: While Apropos involves some perhaps unfamiliar concepts, it brings a robust set of testing practices to the Cardano ecosystem while extending the testing scope of commonly used tools such as QuickCheck. The use of Apropos helps ensure that designs are robust and that development proceeds properly.
3) Reduced Development Costs: With such a large degree of automated test generation and model checking offered, Apropos offers a dramatic reduction in the engineering hours involved in creating the same number of property tests by hand. This will dramatically reduce the cost of bringing dApps to market meaning, over time, a more vibrant ecosystem built on Cardano.
Finally, the deliverables of this proposal will be easily audited by interested community members. As mentioned, the GitHub repo is open-sourced and available for scrutiny by the public. Moreover, our code is licensed under Apache 2.0. We will also post regular updates on the progress of Apropos via Medium and our other social channels.
This is a new proposal for furthering the development of an ongoing open-source initiative concerning a highly-effective testing suite for Plutus smart contracts. Please see our repo link:
Compiler developers and other advanced Haskell / Plutus engineers.
Moreover, our engineers are committed to open-source tooling for the Cardano ecosystem. See our work on the Cardano Transaction Library (Fund8 successful proposal) and the Plutonomicon GitHub repo. Links below.