Please describe your proposed solution
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:
- Functionality, which is the high-level logic that a developer wants to implement;
- Optimization, which deals with producing the most performant low-level representation of that logic; and
- Analysis, which deals with the verification of certain properties of the resulting program.
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':
- Covenant, itself, should be defined as a standalone library, not requiring Plutus, or even Nix, to build.
- Covenant will have a canonical serial form, based on JSON. This form will not depend on what language, or tool, is being used to handle Covenant, and will be specified separately from Covenant's Haskell definition.
- Any analysis or transformation pass would interact with Covenant only in its serial form (as described above). While a Haskell-defined pass could be defined by using Covenant-the-library, this is not required.
- A minimal amount of dependence on Plutus or Nix will be required. Only those parts that must interact with Plutus somehow (such as the UPLC code generator) will depend on Plutus or Nix in any way.
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:
- Extending the ability to write Cardano smart contracts to other languages, programming environments and ecosystems;
- Generation of optimized UPLC, whether in time and space, independent of specific applications or ‘front-ends’;
- Tooling and applications for analysis, whether for safety or otherwise, of Cardano smart contracts.
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:
- Showcasing the ease of analysis and optimization of smart contracts targeting Covenant;
- Measuring improvements in code reliability, efficiency and development time by targeting Covenant; and
- Actively participating in the Cardano community, gathering and incorporating feedback to enhance Covenant’s usability and effectiveness.
Features
- Clear, standalone DSL specification, not tied to the particulars of Haskell or Plutus
- Stable serial form for the DSL, allowing translations to and from as well as manipulations of it without requiring a Haskell dependency.
- Total and call-by-push value semantics for the DSL, enabling static analysis and optimization passes.
- Clarity and simplicity for an intuitive development experience.
- Open-source and community-driven development.
Related work
- LLVM IR
- Pact
- Free Applicative and Selective analysis
- Call-by-push-value