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://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-testing.html#goal-directed-testing-with-dynamic-logic
- https://abailly.github.io/posts/mutation-testing.html
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.
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.
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.