MLabs - Apropos for Property Tests

[IMPACT] 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.

[IMPACT] 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.

[IMPACT] 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.

[FEASIBILITY] Please provide a detailed plan, including timeline and key milestones for delivering your proposal.

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.

[FEASIBILITY] Please provide a detailed budget breakdown.

Funding:

Hours involved: 780

Total: $62,400

Breakdown:

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

Subtotal 700

Change Budget 80

Total Time 780 hours

Total Cost $62,400

[FEASIBILITY] Please provide details of the people who will work on the project.

OUR TEAM

MLabs

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:

• Liqwid
• SundaeSwap
• Minswap
• Optim
• Many others

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.

https://mlabs.city/

https://github.com/Plutonomicon

https://github.com/mlabs-haskell

Core Team

Haskell and Plutus Engineer

Ari Fordsham

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.

https://arifordsham.com

Haskell Engineer

James Faure

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.

https://github.com/jfaure/Irie-lang

[FEASIBILITY] If you are funded, will you return to Catalyst in a later round for further funding? Please explain why / why not.

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.

[FEASIBILITY] Are you or any member of your team working on any other proposals in this Fund9?

[FEASIBILITY] Are you or your team working on any other proposals from previous Funds?

[AUDITABILITY] Please describe what you will measure to track your project's progress, and how will you measure these?

We will measure:

• the number of features implemented
• the number of issues discovered and resolved
• the usability of Apropos to dApp projects that have incorporated it
• the number of contributors adding to the GitHub repo
• the number of Cardano projects relying on Apropos
• the general perception of the project in the space

We expect growth/positive results in these areas and are committed to meeting the milestones we have established throughout this proposal.

[AUDITABILITY] What does success for this project look like?

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.

[AUDITABILITY] Please provide information on whether this proposal is a continuation of a previously funded project in Catalyst or an entirely new one.

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:

https://github.com/mlabs-haskell/apropos-tx