[IMPACT] Please describe your proposed solution.
Idea
CEM-machines are a well-known abstraction for specifying on-chain scripts. They were used in the definitional "The Extended UTXO Model" paper, and a similar model was used in Plutus-apps for some sub-cases of our proposal.
Multiple known on-chain specifications, including ours, use such style for non-formal specification and subsequent code audits.
This makes CEM-machines a natural candidate for on-chain script specification. This would greatly simplify both code reuse between multiple modes of off-chain code and provide checking for security invariants, which are much harder to state manually.
Yet the main technical problem with CEM machines is that they should be both non-deterministic on-chain and deterministic in any off-chain usage. Such distinction leads to duplicated models and complicates code reuse because Haskell is not suited for handling non-deterministic code.
Solutions known to us do not aim to cover such use cases. They either give up on reusing common domain logic or are trying to solve non-determinism automatically. Solving it is a hard problem, probably not properly solvable without resorting to a full logic programming engine, which leads to complex API and missing some cases.
We believe that handling non-determinism with a strategy specified manually by the DApp implementor is a good solution to this. It retains most of the code reuse benefits while not inducing any error-prone boilerplate.
Proposed API
Let's first take a look at the core API: CEMScript typeclass. Instances for it should be written by DApp implementers for each on-chain script. The meaning of this API will be explained later.
> – This covers constraints on blockchain slot time,
> – used by both on- and off-chain code
> class TimedScript script where
> data Stage
> stageToOnChainInterval :: Stage -> Interval POSIXTime
>
> class TimedScript script => CEMScript script where
> data State – This is in fact just a script Datum
> data Transition – Transitions for deterministic CEM-machine
> data Redeemer – Transitions for non-deterministic CEM-machine, aka on-chain code
>
> – This functions define domain logic
> transitionSpec :: Transition -> TransitionSpec
> – This is optional function re-used for and Tx logic tests
> stateCustomInvariants :: State -> [TxDeterministicConstraints]
>
> – This function is the only part needed to translate deterministic CEM
> – into working Plutus on-chain script
> parseTxToTransition :: Tx -> Maybe Transition
>
> – Generic library datatype
> data TransitionSpec = MkTransitionSpec {
> transitionStates :: (State, State)
> transitionConstraints :: TxDeterministicConstraints
> transitionStage :: Stage
> }
Solving non-determinism and getting free implementations
Let's see an example instance for the case of a simple auction:
> instance CEMScript AuctionScript where
> – Omitting some details including bidder
> data State = Open {
> currentBid :: Maybe (UserPKH, Lovelace),
> seller :: UserPKH,
> lotTxInput :: TxIn,
> }
> | Closed { winner :: UserPKH }
> data Transition =
> OpenAuction {
> auctionLot :: SomeNFTAssetAmount,
> seller :: UserPKH
> }
> | PlaceABid {
> bidAmount :: Lovelace,
> – TxIns locked on some deposit script
> lockedPaymentInputs :: [TxIn],
> bidder :: UserPKH,
> }
> | CloseAuction {
> winner :: UserPKH,
> lotToWinnerTxOut :: [TxIn],
> }
>
> data Redeemer = OpenAuctionR | PlaceABidR | CloseAuctionR
>
> – …
As you may see, Transition is a data type with the same constructors as a Redeemer, but augmented with all information required to reconstruct the rest of the transaction.
Such Transition will cover Tx intention for any kind of off-chain Tx submitting code. With TxDeterministicConstraints, Stage (and some other annotations omitted here) known for Transition, all such Tx code is implemented generically.
What about on-chain code? parseTxToTransition is enough to get is as well! One can get genericDeterministicScipt :: Transition -> ScriptContext -> Bool easily from direct TxDeterministicConstraints translation. Then real on-chain script implementation would be morally just genericDeterministicScipt . parseTxToTransition !
For reusing this for performant off-chain query/indexation implementation, parseTxToTransition should be written via a more abstract Parser-like notion, which is omitted here for clarity of explanation.
Also included would be additional API parts required for script parameterization, tx inputs re-submitting handling, user-facing errors, custom extension via hooks, and some other parts.
PROFIT?!
What else does such CEMScript give a DApp implementer? Such presentation is
much easier to modularize, test, and reason about.
One can re-use and combine CEMScipts and their parts without the need to track common or inter-script invariants in at least three places in the codebase. They could just use normal Haskell patterns for reusing such code.
State transitions are clear, and user-facing spec/API can be generated from them. This removes most of the need to audit spec/script mapping, which is a well-known vulnerability source.
Such a state machine is vital for any PDD spec in eUTxO. It gives some important free (script should not be stuck in a non-final state, transactions should not exceed Cardano ledger restrictions, Tx mutations should be found by on-chain code) or re-usable (script should not lose auth token or deposit, etc) invariants. Similar benefits would be achieved for performance benchmarking.
We will consider the following sources with similar approaches:
-
https://abailly.github.io/posts/mutation-testing.html
[IMPACT] How does your proposed solution address the challenge and what benefits will this bring to the Cardano ecosystem?
The library developed by this project will significantly improve the Cardano developer experience by allowing high-level definitions of an app's redeemers/datums, CEM machines, and invariants/interactions to be turned into free implementations of on-chain scripts, transaction building and submission code, model-based tests, and data indexing code. This project goes beyond previous similar projects, which mainly dealt with common types and formal specs, towards handling the actual logic of the application.
Reducing this duplicated low-level effort through automatic derivation will accelerate the pace of development on Cardano and lead to higher-quality applications.
[IMPACT] How do you intend to measure the success of your project?
The main measure of the success of this project is the range of application logic for which the library can derive valid low-level code from the high-level definitions that the developer provides.
A further measure of success is the ease of adoption by Cardano developers of this library, as evidenced by the experience of early adopters.
[IMPACT] Please describe your plans to share the outputs and results of your project?
We will be developing this project's library in an open repository where we will include helpful documentation, which is crucial for its adoption by the Cardano developer community. We will also promote the library via community forums like the Cardano Developer Experience Working Group.
We intend to dogfood this library in an upcoming project that coincides with the Catalyst project timeline (i.e. starts around October 2023). Preferably, this will be a project that straddles the L1/L2 boundary so that we can verify suitability across blockchain layers.
[CAPABILITY/ FEASIBILITY] What is your capability to deliver your project with high levels of trust and accountability?
MLabs, a leading consultancy in the Cardano ecosystem, has a proven track record and significant experience. Our team consists of seasoned engineers, each holding expertise in their respective fields. Moreover, we have consistently demonstrated our ability to deliver complicated projects with a high degree of trust and accountability. We have an extensive portfolio of satisfied client projects as well as several popular Catalyst projects. We're committed to upholding these standards for this proposal.
[CAPABILITY/ FEASIBILITY] What are the main goals for the project and how will you validate if your approach is feasible?
The main goal of this project is to increase the range of types and application logic that can be derived from high-level definitions provided by developers into the low-level code. This will improve DApp logic re-usability and implementation velocity, improve ease of audit, and level of non-functional guarantees achievable with realistic budget/time restrictions.
We will pursue this goal by changing the point of work from on-chain script PL into more high-level abstraction, which greatly simplifies DApp design.
Another, just as important, goal of the project is for the resulting library to be easy to use by developers, hopefully leading to growing adoption by new projects in Cardano. We will pursue this goal by consulting with developers throughout the project timeline and dogfooding the library in a real Cardano application project.
The usability of the library will be clearly validated by using it to rewrite two already implemented model DApps and some common eUTxO design patterns.
[CAPABILITY/ FEASIBILITY] Please provide a detailed breakdown of your project’s milestones and each of the main tasks or activities to reach the milestone plus the expected timeline for the delivery.
Month 1
- Designing and specifying main API: type class and constraint language
- Research and consultation
- Project setup
Month 2
- Generic implementation of Tx submit/query code
- Generic Plutus on-chain implementation
Month 3
- Support for model-based testing (with quickcheck-dynamic) and tx mutation testing
- Support for (basic) markdown spec generation
Month 4
- On-chain code optimization, profiling, and Plutarch on-chain code generation
Month 5
- Support for L1 chain indexing
Month 6
-
Finalize library testing, documentation, and overall demonstration
[CAPABILITY/ FEASIBILITY] Please describe the deliverables, outputs and intended outcomes of each milestone.
Month 1
- An open-source repository exists and is structured for the project.
- Main API definitions (for constraint language and state machines) are present.
- Research, consultation, and spec documents are provided in the repository
- This includes existing solutions and similar methods review and evaluation of API usage on examples for our model examples
Month 2
- Generic implementation for transaction submit/query code, and Plutus on-chain script are present.
- Implementation is checked by rewriting the main Hydra Auction and POCRE scripts using it, checking it works fine, and documenting problems and code simplification. They will be used for all later work evaluations.
- Implementation is checked by implementing the main eUTxO model patterns described in Plutomicon.
Month 3
- The library supports generic model-based testing (with quickcheck-dynamic) and tx mutation testing (mostly copying or reusing already available tx mutation solutions)
- The library supports markdown spec generation as well as CIP-0057 script API
- Example projects are evaluated, and results are documented (e.g. such as problems and code simplification)
Month 4
- The library supports Plutarch on-chain code generation and various on-chain code optimizations. Both solutions are documented.
- Benchmark utils are provided, different backends are evaluated on examples, and results are analyzed and documented.
Month 5
- The library supports L1 production chain indexing.
- Examples (and overall related Hydra SDK) are changed to use this feature and evaluated.
Month 6
-
A finalized repository exists with clean code, documentation, and examples for the features developed in this project.
-
An overall tutorial is written demonstrating the integrated workflow with the library.
[RESOURCES & VALUE FOR MONEY] Please provide a detailed budget breakdown of the proposed work and resources.
Month 1:
- Reviewing existing solutions and asking for input from experts - 40h
- Specifying, validating on model examples and documenting of main API - 50h
Month 2:
- On- and off-chain constraint translation and testing - 40h
- Fleshing out rest of implementation and validating result on model projects - 40h
Month 3:
- Adding common invariants and necessarily utils for model-based testing - 50h
- Adding or reusing utils for basic tx mutation testing - 40h
- Debbuging possible generator distribution issues and covering performance testing invariants - 40h
- Support for state diagrams and basic spec generation - 20h
- Support for CIP-0057 API generation - 20h
Month 4:
- Adding optimization layer and test various logical and general rewritings - 40h
- Improving benchmarking between different backends - 20h
- Add Plutarch backend - 60h
- More reflection on profiling results - 30h
Month 5:
- Research on-chain indexing solutions - 25h
- Contstraint language into indexing solution language traslation - 40h
- Rest of implementation and its validation - 30h
Month 6:
- More reflection on community input and fixing API - 30h
- More documentation - 30h
Total hours: 645h
Total cost @ $95/h: $61,275
Total ADA @ 0.21 USD/ADA: 291,786
[RESOURCES & VALUE FOR MONEY] Who is in the project team and what are their roles?
Gregory Gerasev – Tech Lead:
- Led the dev team for the Hydra auction project – one of the first non-trivial smart contract applications to use the Hydra Head technologies in a hybrid L1/L2 workflow. Helped implement the overall protocol design, the service architecture, on-chain and off-chain code, and SDK components.
- Led the dev team that implemented the Hydra backend for the POCRE project.
- Helped develop the Cardano Transaction Library (CTL), including the Blockfrost backend for CTL (funded in Fund 8).
Delivery Manager – TBD
Dev team – TBD
[RESOURCES & VALUE FOR MONEY] How does the cost of the project represent value for money for the Cardano ecosystem?
The project aims to improve Cardano DX for a range of use cases (teams using Haskell for backend/on-chain code) while comparable in the required work to some proposals only covering a more modest extension or support of already existing solutions.
