Current Cardano contract languages cannot perform static analysis for several reasons. Alongside a lack of specifications & clear development stages, this creates notable challenges for developers.
This is the total amount allocated to MLabs: Static analysis with Covenant.
NB: Monthly reporting was deprecated from January 2024 and replaced fully by the Milestones Program framework. Learn more here
We propose Covenant: a total, functional eDSL with call-by-push-value semantics and a stable, JSON-based serial form for static analysis, plus translation to UPLC.
Covenant will depend on Plutus Core for translation to UPLC. This will only be required in the translation component, which will stand apart from the rest of Covenant.
Covenant may also depend on Haskell ecosystem libraries that stand apart from GHC and its boot libraries. These dependencies will be minimal and restricted to libraries available on Hackage.
We intend to license Covenant under the Apache 2.0 License. This permissive licence allows for broad use and modification while providing clear attribution and disclaimers.
All elements of the Covenant project, including the Haskell library, the serial form specification, the UPLC code generator, and the analysis pass, will be open source and available in public repositories throughout the entire project lifecycle, and subsequently.
Problem
Writing Cardano smart contracts poses some unique challenges. We must contend with a computation model that likely doesn’t resemble what we are used to and must also be much more mindful of correctness. Furthermore, we would like to allow good separation of concerns when dealing with the various aspects of this work, ranging from the actual contract logic, to optimization, to analysis to verify the aforementioned correctness properties.
Writing UPLC directly, or by way of Haskell, is not a reasonable choice given these requirements. Thus, a range of higher-level approaches have been developed by the community, ranging from true DSLs (Plutarch) to compiler backend extensions (Plinth, Purus), and even solutions that are independent of Haskell altogether (Aiken). Despite this embarrassment of riches at our disposal, none of these approaches really suit their stated purposes, limiting their usefulness and creating difficulties for developers of Cardano applications, which are neither necessary nor particularly easy to work around. This makes these solutions far more restrictive, monolithic and rigid than they need to be for the task we have before us.
Specifically, the limitations are as follows; while our descriptions, and experience, are coloured by Plutarch, everything we discuss applies to all other existing solutions just the same.
Lack of totality and static analysis
In this context, we define ‘totality’ in the sense of Turner. The lack of such totality in the context of tools to write Cardano smart contracts is, in our view, both rather strange and totally unnecessary. In practice, the execution semantics of UPLC do not allow for Turing completeness, or even proper codata: there is a finite (and extremely limited) execution budget imposed on us, both in time and space. However, the stated semantics of UPLC (and indeed, all solutions targeting it) mislead us by insisting that they can support a true fixpoint operation, thus claiming Turing-completeness. This is a worst-of-both-worlds situation: we end up having neither the ability to do static analysis (as we are vulnerable to Rice’s theorem not least of all), nor can we even make use of this claimed power due to budget limitations!
This problem is both pernicious and, to our surprise, quite invisible, as every existing solution targeting UPLC continues to perpetuate this myth, to their detriment. This ranges from the ‘embedding’ approach into Haskell taken by Plinth (and indeed, into PureScript by Purus), to the pfix operation in Plutarch, to the while loops available to Aiken code via Rust, all of which promise general recursion, which in practice is unrealizable. While we could argue that this limitation is true of any computer language that exists today (our machines, and the observable universe, are of course finite), we believe that this lack of honesty is far more apparent, and far more problematic, in the context of Cardano, as the limits are far harsher than what we impose on general programming environments, even in embedded settings.
Excessive coupling
In practically all higher-level languages in existence today, we can see a separation of processes and concerns, roughly as follows:
These three concerns require different skill sets and should exist as independently of each other as possible. In the context of Cardano scripts, this is even more critical: we have more onerous performance requirements due to the restrictions imposed on us onchain and need to ensure a much higher degree of correctness and safety than many other application domains.
As we have already discussed, current solutions are already deficient at the analysis concern. However, the problem extends further, as disentangling these three concerns in most current solutions is difficult, if not outright impossible. Consider Plinth as an example: developers of scripts in Plinth often (some would say always) have to keep in mind how exactly the machinery of the Haskell plugin will translate their code, which is opaque, arcane, and frequently extremely surprising. This forces the use of some quite un-Haskelly, and arguably cryptic, techniques to ensure that the functionality we want is runnable at all, much less optimally: this forces the functionality and optimization concerns to be one and the same. This is a bad idea for either a functionality specialist (who would rather be focusing on delivering the application logic instead of wondering how, or whether, it will run) or for an optimization specialist (who would prefer to define general performance improvements without being chained to a single application’s specifics).
Other existing solutions are no better here: Purus wordlessly inherits all the limitations that Plinth has, merely changing the target language; Plutarch requires painful amounts of wrangling, high-level Haskell knowledge and low-level Cardano knowledge to properly understand what you end up with; and Aiken’s impedance mismatches make this kind of separation just as difficult. This makes work of this kind much longer and harder than it needs to be, as this entanglement leads to the mixing of unrelated concerns.
To see a counter-example, consider LLVM. In its design, these three concerns are cleanly separated: the functionality concern is dealt with by a language-specific frontend, translating into an interchange format (LLVM IR); then, the optimization concern deals only with LLVM IR, without ever having to consider what exact frontend it came from; and likewise, the analysis concern can assume a faithful translation, and work against LLVM IR, without having to consider either how this logic was defined or optimised. This separation means that not only is extending its ecosystem straightforward, specialists in each concern can do their work without needing to understand, or be aware of, other concerns that they are not specialists in.
Laziness versus strictness impedance mismatches
UPLC has strict execution semantics. While this is not a problem in itself, developers from a Haskell background, who make up a large number of both current and likely future developers of Cardano scripts, can and do find this surprising. Problems and confusion stemming from this are most apparent in Plinth, as it is embedded into Haskell in a semi-direct way. This easily leads to results that Haskellers, even with experience, don’t expect or want. At the same time, this problem is hardly unique to Plinth: for example, Plutarch requires manual control over laziness and strictness, which is confusing at best, and tedious at worst.
While we could see this as a Haskell problem specifically, the reality is that control over strictness should be far more predictable, far less manual, and generally far better, than what we currently have. No solution is currently good at doing all the above: it’s either opaque and inscrutable (Plinth), tediously manual (Plutarch), or some combination of the two.
Solution
We will define Covenant: a standalone DSL, with an independent, JSON-based serial form. Covenant will be designed as a Turner-total functional language, which uses call-by-push-value semantics. Together, these will combine to enable static analysis, which is currently not possible with any other existing solution for defining onchain scripts.
The design is intended as a fairly low-level target, similar in spirit to LLVM IR: specifically, it will have a standalone textual form (JSON-based), which will allow tools to interact with it without depending on Plutus, Covenant, or potentially even Haskell itself. As part of the work, we will provide a Haskell implementation of Covenant as a standalone library, requiring no dependency on Plutus or Nix. We aim to publish Covenant on Hackage as a demonstration of this autonomy: currently, this is impossible for any other such solution, including Plinth.
To demonstrate the capabilities of Covenant, we will also define a single analysis pass, performing a useful type of static analysis against Covenant's serial form. The analysis pass will be written with a dependency on Covenant-the-library for convenience, but will still consume Covenant's JSON-based serial form. This will demonstrate that in theory, such a pass could be defined without using Haskell at all.
Lastly, we will provide a small executable designed to generate serialized UPLC from Covenant's serial form. This will require a dependency on Plutus (and thus, we must use Nix by extension): however, we will show that the dependency is minimal, and not required to either generate or process Covenant in any other way. This executable will also demonstrate that we are able to generate valid UPLC from a valid Covenant serial form.
Goals and outcomes
We will design Covenant to be a standalone DSL, with a JSON-based serial form. While we will use Haskell as the implementation language, the goal is to make the definition of Covenant as detached from Haskell specifics as possible. In particular, we aim for the following as a definition of 'independence':
We also aim for clarity and idiomatic code above all else. We don't expect (or want) anyone using or working with Covenant to have to know anything about the peculiarities of GHC Haskell, either in terms of its front end or its back end,to use Covenant. Furthermore, we aim to document everything we do as a primary goal, along with why we chose to do this, to ensure that others who want to work with Covenant, or define tools to interact with it, have a minimum of surprise to contend with.
Lastly, we will pedantically avoid over-generalization. The goal of Covenant is to be as simple, and as low-level, as possible: instead of forcing our opinions regarding abstractions onto its users, we instead aim to enable them to bring their own, depending on their use cases. Lastly, we aim to minimize the number of rakes developers can step on when dealing with Plutus, up to and including dealing with its peculiarities: Covenant is, and always will be, a specialist DSL for writing onchain scripts, and only this, without any provisions for further generality now or in the future.
Market
Covenant will primarily engage developers and researchers within the Cardano ecosystem. We specifically aim to benefit developers and researchers concerned with the following:
By providing a focused and well-documented tool, with a clear separation of concerns and examples, we aim to empower such developers and researchers to create more sophisticated, efficient and secure smart contracts, as well as to enable them to be made more easily, with fewer defects and lower costs. By releasing Covenant as open-source, we also encourage community contributions and scrutiny, fostering a collaborative environment for continuous improvement.
We will demonstrate the impact of Covenant through:
Features
Related work
Covenant will bring significant value to the Cardano community by addressing several critical needs in smart contract development:
Measuring Impact
We will measure the impact of Covenant through a combination of quantitative and qualitative metrics:
Sharing Outputs and Opportunities
We are committed to open communication and knowledge sharing throughout the project lifecycle. We will actively engage with the Cardano community through various channels, including:
MLabs has a proven track record of delivering high-quality projects on Cardano, with a history of collaboration with IOG, Intersect and other important organizations within the Cardano Ecosystem. Our expertise in Haskell and blockchain development, paired with a strong focus on formal verification and testing, ensures a robust and reliable solution.
We will validate the feasibility of Covenant through iterative development, prototyping key features, and gathering feedback from the community. We will maintain transparency by regularly sharing our progress publicly, ensuring accountability and trust throughout the project.
Our team's deep understanding of Cardano's intricacies and our commitment to open-source development demonstrate our capability to deliver this project successfully. We will adhere to strict financial management practices, providing detailed reports and transparent accounting in this submission to ensure responsible use of funds.
Outputs
We will define a library implementing data types, and appropriate functionality, for Covenant, as well as tests to ensure it works as expected. We will ensure that the library has minimal dependencies: in particular, we require that it depends on neither Plutus nor Nix. We will upload this library to Hackage as a demonstration of its stand-alone nature. We will also include documentation for this library, primarily in the Reference quadrant, with some in the Explanation quadrant if required.
Acceptance Criteria
Evidence
Haskell Library of Datatypes
Test suite
Haddocks
Outputs
We will provide a specification of the JSON-based textual form of Covenant, as well as an implementation of that specification into the library from Milestone 1. As part of the specification, we will provide at least two conformance cases designed for use in tests for the implementation of the specification. These tests will be provided as part of the library from Milestone 1 as well. We will also provide documentation for both the specification and the extra parts of the Milestone 1 library; both will primarily be in the Reference quadrant, with possibly some Explanation quadrant work if deemed useful.
Acceptance Criteria
Evidence
Conformance Tests
Documentation of Serial Form
Specification for serial form
Outputs
We will define c2uplc: an executable that translates the Covenant serial form as specified in Milestone 2 into serialized UPLC. We will also include documentation for the use of this tool, focusing primarily on the Tutorials quadrant, with possibly some Explanation or How-To Guide quadrant work if necessary. We will use the conformance test cases from Milestone 2 to verify that c2uplc works correctly.
Acceptance Criteria
Evidence
Covenant Executable
Conformance tests pass
Documentation
Outputs
We will define an executable that performs static analysis of some sort on a Covenant serial form. The executable will not execute, or simulate, Covenant in order to achieve this. Furthermore, this executable will have no dependency on either Plutus or Nix. We will provide at least one example program demonstrating this static analysis. The executable will be published on Hackage, either as part of the library package from Milestone 1, or separately. Lastly, we will provide documentation on the executable, with emphasis on the Tutorials quadrant.
Acceptance Criteria
Evidence
Analysis program executable
Documentation
Hackage publication
Example program
Integrating Covenant Documentation
Outputs
We will add more integrated documentation for the entire Covenant ecosystem, focused towards the How-To Guides quadrant of the Diataxis framework. In particular, we will focus on the following cases:
Our goal is to ensure that the documentation from previous Milestones doesn’t remain atomized to their specific contexts, and is supplemented and integrated as necessary. We will do this by using the Diataxis framework as a guiding principle.
Acceptance Criteria
Evidence
Documentation fits Diataxis
Documentation for frontend writing
Documentation for analysis tool writing
Documentation for use of Covenant as a Haskell library
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:
Through our work with early-stage projects, we have one of the largest groups of Haskell/Plutus developers in the community.
Core team
Koz Ross - Tech Lead
Koz is a software engineer with experience ranging from SIMD implementation of a UTF-8 validator in the bytestring library to DSL development to Plutus Core development. He has almost a decade of experience in Haskell, including almost four years working on Cardano and Plutus-related projects, having been involved in projects in the Cardano ecosystem ranging from Liqwid to other client projects to work on Plutus itself.
https://github.com/kozross
Jordan Hill - Project Manager
Seasoned Delivery Manager specialising in blockchain technology and non-EVM chains, adept at orchestrating cross-functional teams for timely and budget-conscious project deliveries. With expertise in both on-chain and off-chain development, Jordan crafts blockchain solutions that harness the potential of decentralized systems, driving innovation in the field.
https://www.linkedin.com/in/jordan-hill-64024772/
Budget/cost breakdown:
Subtotal: 532 hours @110 USD/hour = 58,520 USD
Total (@ rate $0.293 USD / ADA): 199,727 ADA
**In the interest of full transparency, please note we have applied a conservative USD/ADA exchange rate in pricing this proposal. This is to ensure our operations remain stable regardless of market conditions. Although we firmly believe the future of Cardano is bright, we recognize the price of ADA and all cryptocurrencies is inherently volatile. Our financial obligations are denominated in fiat. Most importantly, this includes the salary of our engineers whose hard work makes projects like this possible.
In the unlikely scenario of severe negative price movement beyond our forecasted rate, it is possible that MLabs may need to temporarily suspend work on this proposal until the market recovers. Rest assured, this decision would be made solely to protect our business's long-term viability and never taken lightly. We appreciate your understanding and support, and we are excited to see what we can achieve together.
By enabling static analysis and enhancing code efficiency, Covenant contributes to long-term network security and scalability, benefiting all stakeholders. Our team's expertise and commitment to transparency ensure responsible financial management and maximise the impact of the ADA invested. We believe that Covenant's positive influence on the Cardano community will create a ripple effect providing lasting value for years to come.