Last updated a week ago
Apps have common types and logic that must be compatible across tx building, on-chain scripts, and indexing. However, they are often re-implemented in each context because dev tools cannot reuse them.
Define and reuse DApp logic via annotated CEM-machines, resulting in free implementations for on-chain scripts, tx building/ submission/resubmission on L1/L2, tx parsing/indexing, specs, and tests.
This is the total amount allocated to MLabs – CEMScript SDK: get your DApp implementation from annotated on-chain logic state-machine. 3 out of 5 milestones are completed.
1/5
Designing and specifying main API
Cost: ₳ 40,714
Delivery: Month 2 - Dec 2023
2/5
Generic implementation of Tx submit/query code
Cost: ₳ 36,190
Delivery: Month 3 - Jan 2024
3/5
Basic model-driven testing and markdown spec generation
Cost: ₳ 76,905
Delivery: Month 4 - Feb 2024
4/5
Advanced features and robustness
Cost: ₳ 67,857
Delivery: Month 5 - Mar 2024
5/5
Finalize testing/docs and add L1 chain indexing support
Cost: ₳ 70,120
Delivery: Month 7 - May 2024
Gregory Gerasev
No dependencies.
Project will be fully open source.
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:
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.
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.
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.
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.
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.
Month 1
Month 2
Month 3
Month 4
Month 5
Month 6
Month 1
Month 2
Month 3
Month 4
Month 5
Month 6
Month 1:
Month 2:
Month 3:
Month 4:
Month 5:
Month 6:
Total hours: 645h
Total cost @ $95/h: $61,275
Total ADA @ 0.21 USD/ADA: 291,786
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.
NB: Monthly reporting was deprecated from January 2024 and replaced fully by the Milestones Program framework. Learn more here
Gregory Gerasev -- Tech Lead:
Delivery Manager -- TBD
Dev team -- TBD