MLabs: Static analysis with Covenant

[GENERAL] Name and surname of main applicant

MLabs Ltd.

[GENERAL] Are you delivering this project as an individual or as an entity (whether formally incorporated or not)

Entity (Incorporated)

[GENERAL] Requested funds in ada

199727

[GENERAL] Please specify how many months you expect your project to last (from 2-12 months)

6

[GENERAL] Please indicate if your proposal has been auto-translated into English from another language

No

[GENERAL] Summarize your solution to the problem (200-character limit including spaces)

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.

[GENERAL] Does your project have any dependencies on other organizations, technical or otherwise?

Yes

[GENERAL] If YES, please describe what the dependency is and why you believe it is essential for your project’s delivery. If NO, please write “No dependencies.”

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.

[GENERAL] Will your project’s output/s be fully open source?

Yes

[GENERAL] Please provide here more information on the open source status of your project outputs

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.

[METADATA] Horizons

Developer Tools

[SOLUTION] 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

[IMPACT] Please define the positive impact your project will have on the wider Cardano community

Covenant will bring significant value to the Cardano community by addressing several critical needs in smart contract development:

1. Enhanced Security and Reliability: Covenant's focus on totality and static analysis empowers developers to write more robust and error-resistant smart contracts. This directly translates to a more secure Cardano ecosystem, reducing the risk of vulnerabilities and exploits that can undermine user confidence and adoption.
2. Improved Efficiency: By enabling code optimization and providing clarity on Cardano's specifics, Covenant streamlines the development process and promotes the creation of more efficient smart contracts. This leads to reduced transaction costs and improved overall network performance, benefiting all Cardano users.
3. Empowerment and Collaboration: Covenant's open-source nature and emphasis on clarity foster a collaborative environment where developers can learn, contribute, and build upon each other's work. This promotes knowledge sharing and accelerates innovation within the Cardano community.

Measuring Impact

We will measure the impact of Covenant through a combination of quantitative and qualitative metrics:

• Quantitative:
• Adoption rate: tracking the number of projects using Covenant for smart contract development.
• Code analysis results: measuring the reduction in errors and vulnerabilities detected in smart contracts developed with Covenant compared to other solutions.
• Performance benchmarks: comparing the efficiency of smart contracts built with Covenant against those developed using alternative approaches.
• Qualitative:
• Expert opinions: soliciting feedback from Cardano experts and researchers on the effectiveness and potential of Covenant.
• Educational resources: assessing the impact of Covenant-related tutorials and documentation on developer understanding and adoption.

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:

• Open-source repository: maintaining a public repository where all project code, documentation, and updates will be readily available.
• Community forums and social media: participating in discussions, sharing progress updates, and addressing questions and feedback from the community.

[CAPABILITY & FEASIBILITY] What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?

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.

[PROJECT MILESTONES] What are the key milestones you need to achieve in order to complete your project successfully?

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

1. The standalone library for Covenant exists.
2. The library from 1 does not depend on Plutus or Nix.
3. The library from 1 has been uploaded to Hackage.
4. The library from 1 follows standard Haskell idioms, including, but not limited to, the PVP.
5. A changelog for the library from 1 exists and is current.
6. Tests for the library from 1 exist and all pass.
7. Haddocks for the library from 1 exist, and satisfy the criteria for the Reference quadrant of the Diataxis framework.

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

1. At least two conformance cases of the serial form exist.
2. All conformance cases deserialize correctly and without error.
3. A description of the serial form, independent of its Haskell implementation, exists as a written document in the Covenant repository.
4. An implementation in Haskell of serialization and deserialization of Covenant exists as an extension to the library in Milestone 1.
5. Documentation for the implementation from 4 exists and satisfies the criteria for the Reference quadrant of the Diataxis framework.
6. Documentation for the serial form from 3 exists and satisfies the criteria for the Reference quadrant of the Diataxis framework.

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

1. An executable for generating UPLC from Covenant exists. Due to its dependency on Plutus, this can be in a separate repository from the rest of Covenant.
2. The executable from 1 accepts a file path to a Covenant serial form.
3. The executable from 1, when given a valid Covenant serial form, emits valid UPLC whose execution semantics match.
4. The executable from 1, when given an invalid Covenant serial form, does not perform a translation, instead erroring with a clear and appropriate message. 
5. All the Milestone 2 conformance cases translate correctly using the executable from 1.
6. The executable comes with documentation in the Tutorials quadrant of the Diataxis framework.

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

1. An executable that reads a Covenant serial form, and produces an analysis, exists. This executable may or may not be in the same repository as the rest of Covenant.
2. If given a path to a valid Covenant serial form, the executable from 1 returns a correct analysis. 
3. If given a path to an invalid Covenant serial form, the executable from 1 does not perform any analysis, instead erroring with a clear and appropriate message.
4. At least one example input for the executable from 1 exists, demonstrating that its analysis is correct.
5. Documentation for the executable from 1 exists, fitting the criteria for the Tutorial quadrant of the Diataxis framework.

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:

• Writing a front-end that targets Covenant
• Writing an analysis tool that works with Covenant’s serial form
• Using Covenant as a Haskell library

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

1. All documentation fits the Diataxis framework across all work done in Milestones 1 to 4.
2. How-To Guide quadrant documentation exists for writing a front-end targeting Covenant.
3. How-To Guide quadrant documentation exists for writing an analysis tool that works with Covenant’s serial form.
4. How-To Guide documentation exists for using Covenant as a Haskell library.

Evidence

Documentation fits Diataxis

Documentation for frontend writing

Documentation for analysis tool writing

Documentation for use of Covenant as a Haskell library

[RESOURCES] Who is in the project team and what are their roles?

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:

• Indigo
• 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.

https://mlabs.city/

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 & COSTS] Please provide a cost breakdown of the proposed work and resources

Budget/cost breakdown:

• 86h - Haskell Library of Datatypes
• 23 h - Test Suite
• 6 h - Hackage upload
• 61 h - 2+ Conformance Cases
• 12 h - Documentation of Serial Form
• 122 h - Covenant Executable
• 8 h - Conformance tests pass
• 110 h - Analysis program executable
• 6 h - Published to Hackage
• 12 h - Conformance tests pass
• 86 h - Integrating Covenant Documentation

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.

[VALUE FOR MONEY] How does the cost of the project represent value for money for the Cardano ecosystem?

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.