From 444d4a5bf4d5da2fa0ca55b1d0fc9f6667acf040 Mon Sep 17 00:00:00 2001 From: euonymos Date: Mon, 20 Jan 2025 12:44:15 -0600 Subject: [PATCH 01/15] chore: remove obsolete parts --- docs/arch_principles.md | 41 ---- docs/goals_and_soa.md | 487 ---------------------------------------- docs/non_cardano_soa.md | 40 ---- docs/tech_debt.md | 9 - 4 files changed, 577 deletions(-) delete mode 100644 docs/arch_principles.md delete mode 100644 docs/goals_and_soa.md delete mode 100644 docs/non_cardano_soa.md delete mode 100644 docs/tech_debt.md diff --git a/docs/arch_principles.md b/docs/arch_principles.md deleted file mode 100644 index d55280f..0000000 --- a/docs/arch_principles.md +++ /dev/null @@ -1,41 +0,0 @@ -# Constraints design - -## Principles - -* Generic compilation across: - * on-chain code - * offchain Tx construction - * indexing backend -* Simple normalization and SMT conversion for: - * Equivalence checking - * Bi-simulation checking -* Constraints determine TxIn/Outs up to UTxO coin-selection (we call it almost-determinacy) -* Datum properties encoded as class types -* Common on-chain optimizations are performed if possible - * Constraints normalization, and CSE - * Best error short-cutting - * Common security problems prevention - -## Potential obstacles - -* Ease and optimality of backend compilation -* Robustness of SMT conversion and overall normalization -* Possibility for parsing and correct offchain usage of almost-determinacy -* Having enough information for Tx submit retrying strategies -* Design for using custom Datum properties is not obvious - -# CEM machine design - -As it is done on top of constraints language, -all their principles and obstacles are affecting CEM as well. - -## Principles - -* State-machine is deterministic modulo coin-change -* Transaction can always be parsed back into SM transitions -* Potential non-deterministic on-chain optimizations should not affect this principle. - -## Potential obstacles - -* Some scripts inexpressible by such model (as it happens in PAB) -* Sub-optimal code from deterministic transitions model diff --git a/docs/goals_and_soa.md b/docs/goals_and_soa.md deleted file mode 100644 index 489acf2..0000000 --- a/docs/goals_and_soa.md +++ /dev/null @@ -1,487 +0,0 @@ -# Design principles - -## Why Cardano DApp modeling language is important? - -While prototypes can be easily constructed with existing Cardano frameworks, -making it secure and production ready is sisyphean task. - -We believe, that onchain PL improvements by themselves could not change that. -Only higher-level modeling framework can lead to reliable DApp production. - -In following enumerate our high-level design goals -and demonstrate them by list of specific problems -arising in existing DApps codebase. - -Such problems are specific security vulnerabilities types -and various kinds development, audit and support cost increase. -After that we examine how existing solutions -are covering our high-level goals. - -## High-level goals - -1. DApp logic as whole (synced-by-construction) -2. Code is free from common security weaknesses by construction (secure-by-construction) -3. Seamlessly emulate and test anything (emulate-anything) -4. Being declarative: close to informal specification and bridging lightweight formal methods (declarative-spec) -5. Generally production ready (production-ready) - -## Not in scope at all - -* Composable inter-DApp interactions and DApp migrations -* Scheduled actions - -## Not in scope for current Catalyst funding - -* CTL and overall frontend transaction construction model -* No specific support, but can be added manually - * Metadata, reference scripts and non-inlined datums - * Stacking and governance features (apart for (security-by-default)) - * ZK-proofs - -# Details of examples of problems to be solved - -## Reference apps - -Those are list of open-source DApps, -what we use to demonstrate problems in following: - -* Audited production DApps - * Agora - * [MinSwap](https://github.com/minswap/minswap-stableswap?tab=readme-ov-file#references) - (with spec) - * Fracada - * JPG Vesting Contract - * Indigo Protocol -* DApp projects we participated, audited or otherwise know their codebase - * Hydra Auction - * POCRE - * CNS - * Hydra -* Public DApp projects with specification - * [SundaeSwap](https://cdn.sundaeswap.finance/SundaeV3.pdf) -* Plutonomicon patterns -* Plutus tutorial - * [Game Model](https://github.com/IntersectMBO/plutus-apps/blob/dbafa0ffdc1babcf8e9143ca5a7adde78d021a9a/doc/plutus/tutorials/GameModel.hs) -* plutus-usecases - -## On-chain correctness - -### Known common vulnerabilities - -There is a list of known security vulnerabilities, -for which naive Plutus implementation is very often prone to. -Our implementation makes them impossible to happen, -taking that burden from developers and auditors. - -* Double satisfaction - * Shown twice in CNS Audit - * Shown once in Fracada audit (3.2.7) -* Insufficient staking control - * Shown once in CNS Audit - https://github.com/mlabs-haskell/cns-plutus-audit/issues/24 - -### TxIn ordering and coin change support - -Those problems are similar to previous in that they tend to -arise in naive Plutus implementations, -if developer was did not take measures to prevent them. - -Plutus forces developers to write TxIn/TxOut constraints from scratch, -leading by subtle bugs from copy-pasting logic or -trying to optimize them by hand. - -Examples: - -* Security bug in MinSwap audit - 2.2.1.3 Unauthorized Hijacking of Pools Funds -* Non-security bug in MinSwap audit - 2.2.2.2 Batcher Is Not Allowed to Apply Their Own Order - -Such constraints naturally lead to conditions -for which more performant implementation should -omit some constraints always following from others. -Such kind of manual SMT solving exercises are -known source for security bugs and complicated code. - -One of important cases is maintaining invariants of token value. -TODO - add explanation - -Most of transactions which require fungible tokens as input, -should not depend from exact UTxO coin-change distribution. - -Failure to expect that leads to prohibition of correct transactions. -On other side too broad constraint might lead to fund stealing. - -Example of bugs: - -* https://github.com/mlabs-haskell/hydra-auction/issues/146 - -Another important case is maintaining invariants -of token value or immutable UTxOs. -Such kind of constraints naturally lead to script -for which more performant implementation should -eliminate some constraint following from others. -Such kind of manual SMT solving exercises are -known source for security bugs and complicated code. - -Checking such constraints leads to code bloat -in form of bunch of utility functions. - -Making Plutus contract invariant to `TxIn` ordering -and participation in multi-script scenarios lead to -similar kind of complications. - -Examples: - -* Non-security bug: https://github.com/mlabs-haskell/hydra-auction/issues/129 -* Non-security bug: https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997 -* Non-intentionally under-specified behavior in MinSwap audit: - * `2.2.2.1 Batchers Can Choose Batching Order` - * Triggered by `2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs"` -* Multiple kind of code complication was observed in CNS audit. -* Utilities [from Indigo](https://github.com/IndigoProtocol/indigo-smart-contracts/blob/main/src/Indigo/Utils/Spooky/Helpers.hs) - - -### Single script safety and liveliness - -Main feature of any correct application is that it -behave same as it specification presumes. In our case -specification for single script is CEM state machine, -and correctness means that on-chain script have exactly -same transitions possible. - -On-chain script having transition not possible in model -usually leads to security vulnerability. Other way around -it might be DoS vulnerability or just usability bug. -We aim to check most of such problems automatically. -Almost all on-chain code bugs are specific cases of -such violations, at least once we are analyzing -not single script, but whole DApp, which is covered -in next section. - -One very important example of liveliness violation -is originated from Cardano Tx limits. Such kind -of bugs are very hard to detect, without transaction fuzzing. -Such fuzzing can be automated as part of our testing framework. -Moreover similar task of script usecase benchmarking -can be covered by same automation. Such kind of benchmarking, -either on list of scenarios or arbitrary generated inputs -is essential for checking economics and performance regressions of DApp. - -https://plutus.readthedocs.io/en/latest/reference/writing-scripts/common-weaknesses/index.html - -### Multiple script safety and liveliness - -Whole DApp may be modeled as another kind of state-machine. -It operates on level of whole DApp and generates specific script transitions. Liveliness could be checked by `quickcheck-dynamic`, -or providing specific usecases just as single script case. - -Safety checks is harder to automate. This is not in the scope of current Catalyst project it is possible to cover this case as well -by employing constraint equivalence check, -and verifying that any deviation from generated transitions -is not possible. Another solution might be mutation testing. -Such kind of vulnerabilities are now the most complex kind of attack -to consider as part of DApp design or auditing. -Thus, automating it may be beneficial. - -### Time and stages handling - -Plutus time is described by allowed intervals. -Such abstraction is prone to off-by-one and similar kind of errors. -At least three errors of this kind are known in Cardano/Plutus -interval logic, showing that this is not simple to implement -correctly. - -Another problem is keeping time logic in sync between on- -and off-chain code. This is even more hard given that Plutus time -to slot conversion is not obvious to implement correctly. -Slot time differences and overall need to make test cases match -real blockchain behavior may lead to flaky test behavior. - -Our script stages abstraction cover all those kind of problems. - -* @todo #3: document problems with slots in Plutus/Cardano API - * https://github.com/mlabs-haskell/hydra-auction/issues/236 - -## Matching off-chain logic - -Problem of duplicating logic between on- and off-chain is twofold. -Testing is essentially offchain, thus, you may miss that your onchain code -is not actually enforcing part of Tx provided in tests. - -CEM Script is constructing Tx for submission from same specification, -which is used for onchain script. Thus it is much harder to miss constraint -to be checked. - -Examples: - -* MinSwap audit - 2.2.1.2 LP Tokens Can Be Duplicated - -## Logic duplication and spec subtleness - -There is a bunch of very common tasks shared by multiple DApps, -which could be tackled generically in our framework. - -### Human-readable specification - -Designing, understanding and auditing any non-trivial DApp -is almost impossible without human-readable spec. -That is why in all reference DApps either used spec in development, -or was asked to provide specification by auditor. -Tweag and MLabs audits specifically list validating provided specification -as one of main tasks of audit. - -This leads to lot of cruft with writing, linking and updating specifications. Quite often not only one, but up to three levels of spec granularity would be beneficial for project, which worsens situation. -We observe great amount of cruft and spec rot in all projects we were personally involved. Such kind of cruft is often present -not only on level of single developers, but on communication - -Such kind of human-readable specs are very much similar to our model, -they almost always include enumeration of possible transitions -and/or state-machine diagrams. -Our project will generate such kind of specifications automatically -as Markdown file with Mermaid diagrams. -Adding usecases scenarios generated from one specified in tests -is much less obvious to implement, -and out of scope of current Catalyst project, -but it is very much possible feature as well. - -Examples of diagrams in DApp specifications: - -* ... -* ... -* ... - -### On-/Off-chain and spec logic duplication - -Writing on-chain contracts manually encodes non-deterministic state machine, -which cannot be used for off-chain transaction construction. -Thus developer need to write them again in different style in off-chain code, -which is tedious and error prone. - -They should add checks for all errors possible, -like coins being available and correct script states being present, -to prevent cryptic errors and provide retrying strategies -for possible utxo changes. - -Our project encodes scripts in deterministic machine, -containing enough information to construct transaction automatically. -This also gives a way to check for potential on/off-chain logic differences -semi-automatically. - -Example: -* MinSwap Audit - 2.2.4.3 Large Refactoring Opportunities -* `availableVestings` - пример чего-то подобного для SimpleAuction - -Examples of this done by hand: - -* [State graph for Agora](https://github.com/Liqwid-Labs/agora/blob/staging/docs/diagrams/ProposalStateMachine.png) - -### Computer readable spec and hashes - -Script hashes and sizes summary is essential -for DApp users and testers to check on-chain script are matching. -We provide generic implementation showing all DApp hashes via CIP. - -### Indexing and querying code duplication - -Our framework simplifies generation of common queries -and custom indexing. - -Querying of current script state is required for almost any DApp, -and they are usually implemented with bunch of boilerplate. - -Examples of boilerplate: - -* [Querying available vestings](https://github.com/geniusyield/atlas-examples/blob/main/vesting/offchain/Vesting/Api.hs#L27) - -Customized transaction indexing is important for providing -data to almost any kind of custom web-backend. -Customized indexing may reduce storage space or SaaS dependence. - -Indexing transactions and parsing it back to state-machine transition -is required for delegated architectures, including many DApps and Hydra L2. - -Examples of boilerplate: - -* https://github.com/MELD-labs/cardano-defi-public/tree/eacaa527823031105eba1730f730e1b32f1470bc/lending-index/src/Lending/Index - -Timing ... - - -@todo #3: Add more off-chain code duplication examples from existing PABs. - Include problems with coin-selection, tests, retrying and errors. - -# Existing solutions - -## Backends - -### PAB - -PABs state-machines and `plutus-contract-model` package -are the ony existing project close to our design. - -They are providing CEM state machine model script, -translatable to on-chain and off-chain code. -On top of that you may specify custom `ContractModel` -specifying multi-script DApp as a whole, -and model check your custom invariants and -very generic "CrashTolerance" safety property -and "No Locked Funds" liveliness property. -Thus they are the only project known to us, -which aim to cover (declarative-spec) and (synced-by-construction) goals. - -This model is generic and covered in Plutus Pioneer tutorial, -thus already known to many people. -Our design is based on very similar model. -Unfortunately, existing `plutus-apps` solution seem to be completely -not (production-ready). We could not find any `ContractModel` usage example on github, apart from forks and tutorials, thus it does not seem that it is indeed not much used in practice. -Also they provide much less free guaranties and features then we aim to. -As we will demonstrate in sequel, -this is most probably impossible to fix without changing PAB design. - -State Machine to on-chain translation is very naive -and would not produce optimal code in multiple typical cases. -Constraint language used by PAB is fundamentally more expressible than ours, -and that complicates possibility of implementing required optimizations. -Specifics of those design considerations are detailed in arch documentation. - -Same logic stands for (security-by-default) goal, -in particular providing SMT encoding for constrains, -which may be used to drastically shrink model-check fuzzing space -or even completely remove a need to use fuzzing. -Automatic check for various other important security properties, -like almost-determinism is complicated by this as well. - -Another important restriction, -is that PAB state machines always produce state-thread-token contract. -This makes impossible to encode tree like UTxO based data-structures, -which are used for encoding all kinds of public registry logic. -Also it prohibits any kind of non-trivial state-thread-token logic, -like optimization by sharing (used for example in `hydra-auction`) -and multiple commiters schemes (used in `hydra`). - -@todo #3: Write more about PAB issues with emulator, packaging and Plutus - -### Atlas - -Atlas provides more humane DX on top of cardano-api. -But it has no features related to goals -(synced-by-construction), (secure-by-construction) -and (declarative-spec). -(emulate-everything) is planned, but is not implemented currently. - -Atlas includes connectors to Blockfrost and other backends, -which our project lacks. - -Also our project has slight differences in API design decisions. -Our monad interfaces is meant to be slightly more modular. -We use much less custom type wrappers, resorting to Plutus types where possible. - - -## Testing tools - -### Tweag's cooked-validators - -Project definitely covers goal (production-ready), -because it was successfully used in real-world audits. -but only partially covers -(emulate-anything) and (declarative-spec) goals. - -While it, surely, can do transaction emulation, -it, to best of our knowledge, does not have monad instance -for real L1 blockchain. So you still cannot reuse same code -across tests and real blockchain Tx construction. - -`TxSkel` datatype is similar to design we are implementing, -and other parts API have a lot of cool DX decisions. -But `cooked-validators` lack script transition model, -so it cannot provide declarative Tx submission error handling -we aim to get, because it does not have information to decide, -if specific Tx input is critical (like auth token), -or can be re-selected again (like coin-selected ADA for payment). - -Having declarative transition model is even -more important for mutation testing purposes. -`cooked-validators` gives Cardano Tx level API, -for construction of mutations. -That means, that you should select, write and evaluate -them manually, depending on logic of your script. -This lead to logic coupling between spec, L1 code and test code. -Such coupling and overall manual construction -complicates spec validation and might lead -to attack vectors missed by mistake. - -Our API presumes that means of on-script validation, -in our case behavior equivalence (aka bi-similarity) -of declarative CEM state-machine and real on-chain script -is verified and validated semi-automatically. -Also we plan to make some kind of vulnerabilities covered by -`cooked-validators` impossible by construction, specifically modules: -`ValidityRange`, `DoubleSat`, `AddInputsAndOutputs` -and `OutPermutations`. - -Another important feature is support for LTL logic formulas, -which are known language for specifying state transitions in BMC. -It seems like this feature is subsumed by -`quickcheck-dynamic` based model checking specification -we are going to provide. - -### Hydra Mutations - -Hydra mutations are similar to cooked-validators in their design -and have similar drawback. Thus they do not cover (synced-by-construction), (secure-by-construction) -and (declarative-spec) goals. - -https://abailly.github.io/posts/mutation-testing.html - -### tasty-plutus - -Only cover (emulate-anything) goal, does not aim to cover others. -Is deprecated as well. -But it has some interesting low-level features, -like `plutus-size-check`, which code we would probably steal. - -### General Haskell verification tools - -We plan to use first two tools in our implementation. -They both are tested in real projects and documented well. - -Other tools are not applicable to our project. - -1. quickcheck-dynamic -2. [SBV](https://hackage.haskell.org/package/sbv) -3. apropos -4. Liquid Haskell -5. Agda - -## On-chain PLs and CIP-30 wrappers - -Any kind of on-chain PL can only cover goals -(emulate-anything) and (production-readiness). -As far as we aware, none of them are trying -to solve other goals. - -Known examples of PLs: - -* [Marlowe](https://github.com/input-output-hk/marlowe-plutus) - - Finance contracts DSL -* [Aiken](https://aiken-lang.org/) - - OnChain PL with IDE support and testing framework -* [Helios](https://www.hyperion-bt.org/helios-book/api/index.html) - - Onchain PL and frontend Tx sending library -* [OpShin](https://github.com/OpShin/opshin) - - Onchain PL -* Purs - PureScript Onchain PL - -Same stands for any known kind of frontend framework: - -* CTL -* Lucid -* meshjs.dev - -Same stands for any kind of `cardano-api` API translation to other PLs: - -* PyCardano - https://pycardano.readthedocs.io/en/latest/guides/plutus.html -* Cardano multi-platform Lib - -## Manual formalizations - -* CEM-machines -* Manual Djed formalization with Kind 2/Lustre model diff --git a/docs/non_cardano_soa.md b/docs/non_cardano_soa.md deleted file mode 100644 index 91ebf52..0000000 --- a/docs/non_cardano_soa.md +++ /dev/null @@ -1,40 +0,0 @@ -# Solidity verification - -## Comparison of account-based and EUtXO verification - -Solidity PL has commands for writing in Design-by-Contract style. -They fail dynamically, and could have been fuzzed for a while. -Same stands for arithmetic overflow and array bounds errors. -Recently they got symbolic execution support as well. - -Overflow and bound errors are less dangerous in Plutus, -because they cannot lead to silent logic bug, -but they can be a reason for getting contract in stuck state as well. -Complications arising from external contract calls support, -and re-entrancy bugs in particular are absent in EUTxO model. - -On other side, checks for unreachable code and balance/gas errors, -are just as important for Plutus as for Solidity. - -Solidity contracts model resembles class-based programming, -and thus is not only very natural for using DbC style, -but overall much simpler to check with formal methods then EUTxO. - -## Recent reviews - -## Known solutions - -List of known solutions based on this: - -* SMTChecker Solidity compiler plugin -https://docs.soliditylang.org/en/latest/smtchecker.html -* HEVM/DApp tools - fuzzer and symbolic executor - * Uses SMT for exploration - * https://github.com/dapphub/dapptools/tree/master -* Echidna - fuzzer (writing in Haskell, pretty simple) -* Etheno - -Other tools: - -* Various static analysis -* KEVM - operation semantics mechanization for EVM diff --git a/docs/tech_debt.md b/docs/tech_debt.md deleted file mode 100644 index 1176f5a..0000000 --- a/docs/tech_debt.md +++ /dev/null @@ -1,9 +0,0 @@ -* Design - * Tx Signers - * Tx stuff naming -* Tests - * Mutation and security -* Code arch and style - * No onchain/offchain GHC options separations of code - * No hlint -* CI and versioning From 571210c3dd80254da80f61180e855627292c8e08 Mon Sep 17 00:00:00 2001 From: euonymos Date: Mon, 20 Jan 2025 12:46:20 -0600 Subject: [PATCH 02/15] feat: add getting started guide --- docs/getting-started.md | 652 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 652 insertions(+) create mode 100644 docs/getting-started.md diff --git a/docs/getting-started.md b/docs/getting-started.md new file mode 100644 index 0000000..732b6b8 --- /dev/null +++ b/docs/getting-started.md @@ -0,0 +1,652 @@ +# CEM Script's getting started guide + +## Basic Concepts + +An instance of `CEMScript` revolves primarily around the following two type classes. + +Here, `script` is an uninhabited type that is used to +tie together the different types associated with an instance of CEMScript. + +`CEMScriptTypes` defines those types: + +```haskell +class CEMScriptTypes script where + -- | `Params` is the immutable part of script Datum + type Params script = params | params -> script + + -- | `State` is the changing part of script Datum. + type State script = params | params -> script + + -- | Transitions for deterministic CEM-machine + type Transition script = transition | transition -> script + + -- | Results of computations that run during each transition. + -- | See `transitionComp` below. + -- | This is optional. + type TransitionComp script + type TransitionComp script = NoTransitionComp +``` + +`CEMScript` defines the following functions: + +```haskell +class + ({- constraints elided for brevity -}) => + CEMScript script + where + -- | The crux part - a map that defines constraints for each transition via DSL. + transitionSpec :: CEMScriptSpec False script + + -- | Optional Plutus script to calculate things, whic can be used in the cases + -- when CEM constrainsts and/or inlining Plutarch functions are not expresisble + -- enough. + transitionComp :: + Maybe + ( Params script -> + State script -> + Transition script -> + TransitionComp script + ) + {-# INLINEABLE transitionComp #-} + transitionComp = Nothing + + compilationConfig :: CompilationConfig + +type CEMScriptSpec resolved script = + ( Map.Map + (Spine (Transition script)) + [TxConstraint resolved script] + ) +``` + +### Spine + +Spine of an ADT is a sum type that is just a list of it’s constructors. + +`HasSpine` type class maps from an ADT to it’s Spine type and: + +- associates the type to it’s Spine type through a type family +- defines a function that translates an instance of the type to an instance of the spine type + +```haskell +-- superclass constraints elided for clarity +class HasSpine sop where + type Spine sop = spine | spine -> sop + getSpine :: sop -> Spine sop +``` + +We provide a function `deriveSpine` to automatically derive `HasSpine` using template haskell. + +### DSL + +When writing `CEMScript` transitions, we start by describing constraints +at a high level using a DSL that consistes of the following types: + +#### TxConstraint + +```haskell +data TxConstraint (resolved :: Bool) script where + -- elided -- +``` + +`TxConstraint` is a GADT (Generalized Algebraic Data Type) parameterized by two things: + +1. **`resolved`**: A Boolean type flag (usually `True` or `False`) indicating whether the constraint is in a "resolved" form. +In on-chain code, `resolved` will be `False`, representing the actual computation that’s going to take place. In off-chain code, `resolved` will be `True`, which is used to derive a valid transaction from a list of `TxConstraint`s. See the Off-chain machinery section for more details on how this works. +2. **`script`**: A phantom type parameter indicating which CEMScript (state machine) the constraints belong to. + +See the reference section for a full reference of `TxConstraint`. + +#### ConstraintDSL + +`ConstraintDSL script value` is a GADT that represents a symbolic expression in the DSL. + +- `script` is a phantom type parameter, just like in `TxConstraint`. +- `value` is the type of the what this expression will resolve to during runtime. + +`ConstraintDSL` allows us to reference parts of the state machine's parameters, the current state, the transition arguments, and so forth. + +It also lets us perform checks (like equality) and apply transformations (like lifting a Plutarch function). + +See the reference section for a full reference of `ConstraintDSL`. + +### DSLValue / DSLPattern + +```haskell +type family DSLValue (resolved :: Bool) script value where + DSLValue False script value = ConstraintDSL script value + DSLValue True _ value = value + +type family DSLPattern (resolved :: Bool) script value where + DSLPattern False script value = ConstraintDSL script value + DSLPattern True _ value = Void +``` + +These are both type level wrappers over `ConstraintDSL`. + +The type parameter `resolved` will be False for on-chain code, while it will be True for off-chain code. + +In an unresolved `TxConstraint` (on-chain), they both assume the type `ConstraintDSL script value` + +In a resolved `TxConstraint` (off-chain), + +- `DSLValue _ value` assumes the type `value` +- `DSLPattern _ value` assumes the uninhabited type `Void` + + Any expression which contains a `DSLPattern`, like `If` and `MatchBySpine`, will get compiled away to the corresponding branch by evaluating the current state. + +See the next **Off-Chain Machinery** section to understand how this works. + +## Off-chain machinery + +In addition to being a language to define on-chain code, +`CEMScript` offers the machinery to safely construct valid transactions +based on the on-chain state as well as the transition constraints. + +```haskell +resolveTx :: + forall m. + (MonadQueryUtxo m, MonadSubmitTx m, MonadIO m) => + TxSpec -> + m (Either TxResolutionError ResolvedTx) + +data TxSpec = MkTxSpec + { actions :: [SomeCEMAction] + , specSigner :: SigningKey PaymentKey + } + deriving stock (Show) + +data SomeCEMAction where + MkSomeCEMAction :: + forall script. + (CEMScriptCompiled script) => + CEMAction script -> + SomeCEMAction + +data CEMAction script = MkCEMAction (Params script) (Transition script) + +data ResolvedTx = MkResolvedTx + { txIns :: [(TxIn, TxInWitness)] + , txInRefs :: [TxIn] + , txOuts :: [TxOut CtxTx Era] + , toMint :: TxMintValue BuildTx Era + , interval :: Interval POSIXTime + , additionalSigners :: [PubKeyHash] + , -- FIXME + signer :: ~(SigningKey PaymentKey) + } + deriving stock (Show, Eq) + +``` + +`resolveTx` is the primary entrypoint for off-chain code. +It accepts a `TxSpec`, which consists of a list of actions and a signer, +and produces a `ResolvedTx`, which is all the information needed to construct +a transaction that’s ready to be submitted to the chain. + +Here’s a rough outline of how it works: + +- For each `Transition` in the list of actions + - Find the corresponding transition in the `transitionSpec` + - If the transition spec contains a `TxFan In SameScript` , check the current on-chain state is the same a required by the constraint. + - Convert the `[TxConstraint (resolved :: False)]` of the `Transition` to `[TxConstraint (resolved :: True)]` by invoking `compileConstraint` . + + This evaluates all the `DSLValue _ value` expressions and resolve it to a value of type `value`. + + The following variants of `TxConstraint` + + ```haskell + = TxFan + { kind :: TxFanKind + , cFilter :: TxFanFilterNew resolved script + , value :: ConstraintDSL script Value + } + | MainSignerCoinSelect + { user :: ConstraintDSL script PubKeyHash + , inValue :: ConstraintDSL script Value + , outValue :: ConstraintDSL script Value + } + | MainSignerNoValue (ConstraintDSL script PubKeyHash) + ``` + + turns into + + ```haskell + = TxFan + { kind :: TxFanKind + , cFilter :: TxFanFilterNew resolved script + , value :: Value + } + | MainSignerCoinSelect + { user :: PubKeyHash + , inValue :: Value + , outValue :: Value + } + | MainSignerNoValue PubKeyHash + + ``` + + This also eliminates control structures that use `DSLPattern _ _`. + + The following variants + + ```haskell + | If + -- | Condition + (ConstraintDSL script Bool) + -- | Then block + (TxConstraint resolved script) + -- | Else block + (TxConstraint resolved script) + | forall sop. + (HasPlutusSpine sop) => + MatchBySpine + -- | Value being matched by its Spine + (ConstraintDSL script sop) + -- | Case switch + (Map.Map (Spine sop) (TxConstraint resolved script)) + ``` + + will become a single `TxConstraint` value based on which branch is taken based on the current state and the condition expression. + +- Concatenate and deduplicate the thus obtained `[[TxConstraint (resolved :: True)]]` to get a flat list `[TxConstraint (resolved :: True)]` . +- For each `TxConstraint`, query the current on-chain state and produce a value of type `Resolution` + + ```haskell + data Resolution + = TxInR (TxIn, TxInWitness) + | TxInRefR (TxIn, TxInWitness) + | TxOutR (TxOut CtxTx Era) + | AdditionalSignerR PubKeyHash + | NoopR + deriving stock (Show, Eq) + ``` + +- Use the list of `Resolution` thus obtained to build the `ResolvedTx` record. + +The `ResolvedTx` can be used with an instance of `MonadSubmitTx` to submit it to the chain. + +`MonadSubmitTx` is provided by default for CLB and local cardano node. + +## Reference + +### TxConstraint + +```haskell +data TxConstraint (resolved :: Bool) script + = TxFan + { kind :: TxFanKind + , cFilter :: TxFanFilterNew resolved script + , value :: DSLValue resolved script Value + } + | MainSignerCoinSelect + { user :: DSLValue resolved script PubKeyHash + , inValue :: DSLValue resolved script Value + , outValue :: DSLValue resolved script Value + } + | MainSignerNoValue (DSLValue resolved script PubKeyHash) + | Error Text + | If + -- | Condition + (DSLPattern resolved script Bool) + -- | Then block + (TxConstraint resolved script) + -- | Else block + (TxConstraint resolved script) + | forall sop. + (HasPlutusSpine sop) => + MatchBySpine + -- | Value being matched by its Spine + (DSLPattern resolved script sop) + -- | Case switch + -- FIXME: might use function instead, will bring `_` syntax, + -- reusing matched var and probably implicitly type-checking spine + -- by saving it to such var DSL value + (Map.Map (Spine sop) (TxConstraint resolved script)) + | Noop +``` + +- `TxFan` Ensure that there exists a utxo with the specified constraints. + - `kind` + - `TxFanKind.In`: Utxo must be part of the inputs. + - `TxFanKind.InRef`: Utxo must be part of the reference inputs. + - `TxFanKind.Out` : Utxo must be part of the outputs. + - `cFilter` + - `UserAddress addr`: Utxo must have the given address + - `SameScript state`: Utxo must be a script address belonging to the current script, and it’s datum must be equal to the given state value. + - `value`: Utxo must have the given value. It is of the PlutusLedger `Value` type. +- `MainSignerCoinSelect user inValue outValue` + + Ensure + + - The sum of input utxos belonging to `user` is greater than `inValue` + - The sume of output utxos belonging to `user` is greater than `outValue` +- `MainSignerNoValue address` Ensure that the given address is part of the transaction signatories. +- `Error message` Output `message` using `ptrace` as an error message. +- `If` + - Evaluate the condition and resolve to the `TxConstraint` in the “then” branch or the “else” branch. +- `MatchBySpine pattern map` Evaluate pattern and execute the corresponding action from `map` + - `map` Map from `Spine` to `TxConstraint` + +In addition to the above, CEMScript provides the following helper functions to create `TxConstraint`s + +```haskell +cNot :: ConstraintDSL script Bool -> ConstraintDSL script Bool +cNot = LiftPlutarch pnot + +offchainOnly :: TxConstraint False script -> TxConstraint False script +offchainOnly c = If IsOnChain Noop c + +byFlagError :: + ConstraintDSL script Bool -> Text -> TxConstraint False script +byFlagError flag message = If flag (Error message) Noop + +``` + +- `cNot` invert a boolean +- `offchainOnly` execute only on chain. Resolve to `Noop` off chain. +- `byFlagError` evaluate to `Error message` if `flag` evaluates to true. + +### ConstraintDSL + +```haskell +data ConstraintDSL script value where + -- Request contextual values (parameters, state, transition, etc.) + -- from the DSL environment during constraint evaluation + Ask :: (..) => Proxy var -> ConstraintDSL script datatype + -- Lifts pure values into the DSL context + Pure :: ( .., ToData value') => value' -> ConstraintDSL script value' + -- Are we running in the on-chain validator context or the off-chain code + IsOnChain :: ConstraintDSL script Bool + -- Accesses record fields in a type-safe way + -- Evaluates to sop.label + GetField :: (..) => ConstraintDSL script sop -> Proxy label -> ConstraintDSL script value + -- Constructs a new value of a data type given its spine (constructor choice) and field values. + -- DO NOT use this directly. Use `cOfSpine` instead. + UnsafeOfSpine :: (..) => Spine datatype -> [RecordSetter (ConstraintDSL script) datatype] -> ConstraintDSL script datatype + -- Similar to UnsafeOfSpine but updates an existing value, keeping unmodified fields. + -- Used for efficient partial updates of data structures. + UnsafeUpdateOfSpine :: (..) => ConstraintDSL script datatype -> Spine datatype -> [RecordSetter (ConstraintDSL script) datatype] -> ConstraintDSL script datatype + + -- Primitives + + -- A wildcard pattern that matches any value. + -- Used in pattern matching contexts where the actual value is irrelevant. + Anything :: ConstraintDSL script x + -- Compare two DSL values + Eq :: (..) => ConstraintDSL script x -> ConstraintDSL script x -> ConstraintDSL script Bool + -- Lifts single-argument Plutarch functions into the DSL context + LiftPlutarch :: (..) => (ClosedTerm (px :--> py)) -> ConstraintDSL script (PLifted px) -> ConstraintDSL script (PLifted py) + -- Lifts two-argument Plutarch functions into the DSL context + LiftPlutarch2 :: (..) => + (forall s. Term s px1 -> Term s px2 -> Term s py) -> + ConstraintDSL script (PLifted px1) -> + ConstraintDSL script (PLifted px2) -> + ConstraintDSL script (PLifted py) +``` + +Safe helpers + +```haskell + +-- Safe version of `UnsafeOfSpine` +cOfSpine :: (..) => Spine datatype -> [RecordSetter (ConstraintDSL script) datatype] -> ConstraintDSL script datatype +-- Safe version of `UnsafeUpdateOfSpine` +cUpdateOfSpine :: (..) => ConstraintDSL script datatype -> Spine datatype -> [RecordSetter (ConstraintDSL script) datatype] -> ConstraintDSL script datatype +``` + +Helper functions for convenience + +```haskell +cMkAdaOnlyValue :: + ConstraintDSL script Integer -> ConstraintDSL script Value +cMkAdaOnlyValue = LiftPlutarch pMkAdaOnlyValue + +cEmptyValue :: ConstraintDSL script Value +cEmptyValue = cMkAdaOnlyValue $ Pure 0 + +cMinLovelace :: ConstraintDSL script Value +cMinLovelace = cMkAdaOnlyValue $ Pure 3_000_000 + +(@==) :: (Eq x) + => ConstraintDSL script x + -> ConstraintDSL script x + -> ConstraintDSL script Bool +(@==) = Eq +``` + +The following are lifted versions of plutrach operators + +```haskell +(@<=) -- #<= +(@<) -- #< +(@<) -- #< +(@>=) -- #>= +(@>) -- #> + +``` + +```haskell +-- Merge the contents of two `Value` instances. +(@<>) :: + ConstraintDSL script Value -> + ConstraintDSL script Value -> + ConstraintDSL script Value +``` + +## Usage and Examples + +### How to define a script + +- Define an empty type for your script: `data MyScript` , where MyScript can be any name. +- Define a `CEMScript` instance for it by providing `Params`, `State`, `Transition`, `transitionSpec` and optionally `transitionComp`. +- Do Template Haskell derivations (`deriveCEMAssociatedTypes`) to generate data and spine instances for pattern matching. +- Invoke the `compileCEM` function (e.g., `$(compileCEM True ''MyScript)`) to process the DSL specification, compile optional `transitionComp` code, and produce a `CEMScriptCompiled` instance. + - This generates an instance of `CEMScriptCompiled` for your script type. + - You may invoke `cemScriptCompiled` on your script type to get an instance of `Plutarch.Script` + +### Example: Auction + +#### Setup: The Types + +First we define a type to denote our script. It’s an uninhabited type, it can’t be constructed. It’s only used as a tag for connecting different type classes together. + +```haskell +data SimpleAuction +``` + +We define a type for the read-only state of our script. This state can’t be modified once created. This becomes the `Params` associated type of the `CEMScript` typeclass. + +```haskell +data SimpleAuctionParams = MkAuctionParams + { seller :: PubKeyHash, + lot :: Value + } + deriving stock (Prelude.Eq, Prelude.Show) +``` + +We define a type for the evolving state of our script. This becomes the `State` associated type of the `CEMScript` typeclass. + +```haskell +data Bid = MkBid + { bidder :: PubKeyHash, + bidAmount :: Integer + } + deriving stock (Prelude.Eq, Prelude.Show) + +derivePlutusSpine ''Bid -- This will be explained below. + +data SimpleAuctionState + = NotStarted + | CurrentBid + { bid :: Bid + } + | Winner + { bid :: Bid + } + deriving stock (Prelude.Eq, Prelude.Show) +``` + +Lastly, we define a type for the state transitions of our script. This becomes the `Transition` associated type of the `CEMScript` typeclass. + +```haskell +data SimpleAuctionTransition + = Create + | Start + | MakeBid + { bid :: Bid + } + | Close + | Buyout + deriving stock (Prelude.Eq, Prelude.Show) +``` + +We can now define an instance of the `CEMScriptTypes` for `SimpleAuction` . `CEMScriptTypes` is a super class of `CEMScript`, which just includes the associated types. By defining the associated types separately, we can use the `deriveCEMAssociatedTypes` template haskell function to generate some boilerplate. + +```haskell +instance CEMScriptTypes SimpleAuction where + type Params SimpleAuction = SimpleAuctionParams + type State SimpleAuction = SimpleAuctionState + type Transition SimpleAuction = SimpleAuctionTransition + +$(deriveCEMAssociatedTypes False ''SimpleAuction) +``` + +`deriveCEMAssociatedTypes` just executes `derivePlutusSpine` for all three of the associated types. But it can only do that if all the members of a type have a `HasPlutusSpine` implementation. This is why we need to do `derivePlutusSpine` for the `Bid` type ourselves. + +The boolean argument to `deriveCEMAssociatedTypes` is unused for now, and it is recommended to use a value of `False` . + +#### Implementation + +To implement the logic of our script, we define an instance of `CEMScript` for our script type `SimpleAuction` + +```haskell +instance CEMScript SimpleAuction where +``` + +We provide a value for `compilationConfig` , which at the moment contains only a prefix for error codes to tell errors from different programs apart. + +```haskell + compilationConfig = MkCompilationConfig "AUC" +``` + +Next comes the meat of the script: `transitionSpec` . This is where we define state transitions + +We create a Map of `Spine (Transition script)` → `[TxConstraint False script]` + +```haskell + transitionSpec = Map.fromList + [ .. ] +``` + +Before we go into the entries in detail, let’s define some helpers: + +```haskell +buyoutBid = ctxState.bid + +initialBid = + cOfSpine + MkBetSpine + [ #bidder ::= ctxParams.seller + , #bidAmount ::= lift 0 + ] + +auctionValue = cMinLovelace @<> ctxParams.lot +``` + +We make extensive use of `OverloadedRecordDot` and custom `HasField` instances to make accessing the fields of the params and state values ergonomic. + +Let’s examine each of the entries of the map in detail. + +1. Create + + ```haskell + ( CreateSpine + , + [ spentBy ctxParams.seller cMinLovelace cEmptyValue + , output (ownUtxo $ withNullaryState NotStartedSpine) auctionValue + ] + ) + ``` + +2. Start + + ```haskell + ( StartSpine + , + [ input (ownUtxo $ inState NotStartedSpine) auctionValue + , output (ownUtxo $ withState CurrentBidSpine [#bid ::= initialBid]) auctionValue + , signedBy ctxParams.seller + ] + ) + ``` + +3. MakeBid + + ```haskell + ( MakeBidSpine + , + [ input (ownUtxo $ inState CurrentBidSpine) auctionValue + , byFlagError + (ctxTransition.bid.bidAmount @<= ctxState.bid.bidAmount) + "Bid amount is less or equal to current bid" + , output + ( ownUtxo + $ withState + CurrentBidSpine + [#bid ::= ctxTransition.bid] + ) + auctionValue + , signedBy ctxTransition.bid.bidder + ] + ) + ``` + +4. Close + + ```haskell + ( CloseSpine + , + [ input (ownUtxo $ inState CurrentBidSpine) auctionValue + , output + ( ownUtxo + $ withState WinnerSpine [#bid ::= ctxState.bid] + ) + auctionValue + , signedBy ctxParams.seller + ] + ) + ``` + +5. Buyout + + ```haskell + ( BuyoutSpine + , + [ input (ownUtxo $ inState WinnerSpine) auctionValue + , byFlagError (lift False) "Some err" + , byFlagError (lift False) "Another err" + , -- Example: In constraints redundant for on-chain + offchainOnly + (if' + (ctxParams.seller `eq'` buyoutBid.bidder) + (signedBy ctxParams.seller) + (spentBy + buyoutBid.bidder + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) + cEmptyValue + ) + ) + , output + (userUtxo buyoutBid.bidder) -- NOTE: initial zero bidder is seller + auctionValue + , if' + (ctxParams.seller `eq'` buyoutBid.bidder) + noop + ( output + (userUtxo ctxParams.seller) + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) + ) + ] + ) + ``` From 71161ba7c1755773ceeee0961ccea017ca687a8b Mon Sep 17 00:00:00 2001 From: Ilia Rodionov <103441514+euonymos@users.noreply.github.com> Date: Mon, 20 Jan 2025 14:51:11 -0600 Subject: [PATCH 03/15] chore: typos on getting started guide --- docs/getting-started.md | 83 +++++++++++++++++++++++------------------ 1 file changed, 47 insertions(+), 36 deletions(-) diff --git a/docs/getting-started.md b/docs/getting-started.md index 732b6b8..af9d848 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -5,7 +5,7 @@ An instance of `CEMScript` revolves primarily around the following two type classes. Here, `script` is an uninhabited type that is used to -tie together the different types associated with an instance of CEMScript. +tie together the different types associated with an instance of CEMScript.on `CEMScriptTypes` defines those types: @@ -37,8 +37,8 @@ class -- | The crux part - a map that defines constraints for each transition via DSL. transitionSpec :: CEMScriptSpec False script - -- | Optional Plutus script to calculate things, whic can be used in the cases - -- when CEM constrainsts and/or inlining Plutarch functions are not expresisble + -- | Optional Plutus script to calculate things, which can be used in the cases + -- when CEM constraints and/or inlining Plutarch functions are not expressible -- enough. transitionComp :: Maybe @@ -61,11 +61,11 @@ type CEMScriptSpec resolved script = ### Spine -Spine of an ADT is a sum type that is just a list of it’s constructors. +The spine of an ADT is a sum type that is just a list of its constructors. -`HasSpine` type class maps from an ADT to it’s Spine type and: +`HasSpine` type class maps from an ADT to its Spine type and: -- associates the type to it’s Spine type through a type family +- associates the type to its Spine type through a type family - defines a function that translates an instance of the type to an instance of the spine type ```haskell @@ -75,12 +75,12 @@ class HasSpine sop where getSpine :: sop -> Spine sop ``` -We provide a function `deriveSpine` to automatically derive `HasSpine` using template haskell. +Using the Template Haskell, we provide a function `deriveSpine` to automatically derive `HasSpine`. ### DSL When writing `CEMScript` transitions, we start by describing constraints -at a high level using a DSL that consistes of the following types: +at a high level using a DSL that consists of the following types: #### TxConstraint @@ -92,8 +92,10 @@ data TxConstraint (resolved :: Bool) script where `TxConstraint` is a GADT (Generalized Algebraic Data Type) parameterized by two things: 1. **`resolved`**: A Boolean type flag (usually `True` or `False`) indicating whether the constraint is in a "resolved" form. -In on-chain code, `resolved` will be `False`, representing the actual computation that’s going to take place. In off-chain code, `resolved` will be `True`, which is used to derive a valid transaction from a list of `TxConstraint`s. See the Off-chain machinery section for more details on how this works. -2. **`script`**: A phantom type parameter indicating which CEMScript (state machine) the constraints belong to. +In on-chain code, `resolved` will be `False`, representing the actual computation that’s going to take place. +In off-chain code, `resolved` will be `True`, which is used to derive a valid transaction from a list of `TxConstraint`s. +See the Off-chain machinery section for more details on how this works. +3. **`script`**: A phantom type parameter indicating which CEMScript (state machine) the constraints belong to. See the reference section for a full reference of `TxConstraint`. @@ -102,9 +104,10 @@ See the reference section for a full reference of `TxConstraint`. `ConstraintDSL script value` is a GADT that represents a symbolic expression in the DSL. - `script` is a phantom type parameter, just like in `TxConstraint`. -- `value` is the type of the what this expression will resolve to during runtime. +- `value` is the type of what this expression will resolve during runtime. -`ConstraintDSL` allows us to reference parts of the state machine's parameters, the current state, the transition arguments, and so forth. +`ConstraintDSL` allows us to reference parts of the state machine's parameters, +the current state, the transition arguments, and so forth. It also lets us perform checks (like equality) and apply transformations (like lifting a Plutarch function). @@ -122,7 +125,7 @@ type family DSLPattern (resolved :: Bool) script value where DSLPattern True _ value = Void ``` -These are both type level wrappers over `ConstraintDSL`. +These are both type-level wrappers over `ConstraintDSL`. The type parameter `resolved` will be False for on-chain code, while it will be True for off-chain code. @@ -179,7 +182,7 @@ data ResolvedTx = MkResolvedTx ``` -`resolveTx` is the primary entrypoint for off-chain code. +`resolveTx` is the primary entry point for off-chain code. It accepts a `TxSpec`, which consists of a list of actions and a signer, and produces a `ResolvedTx`, which is all the information needed to construct a transaction that’s ready to be submitted to the chain. @@ -188,10 +191,10 @@ Here’s a rough outline of how it works: - For each `Transition` in the list of actions - Find the corresponding transition in the `transitionSpec` - - If the transition spec contains a `TxFan In SameScript` , check the current on-chain state is the same a required by the constraint. - - Convert the `[TxConstraint (resolved :: False)]` of the `Transition` to `[TxConstraint (resolved :: True)]` by invoking `compileConstraint` . + - If the transition spec contains a `TxFan In SameScript`, check the current on-chain state is the same as required by the constraint. + - Convert the `[TxConstraint (resolved :: False)]` of the `Transition` to `[TxConstraint (resolved :: True)]` by invoking `compileConstraint`. - This evaluates all the `DSLValue _ value` expressions and resolve it to a value of type `value`. + This evaluates all the `DSLValue _ value` expressions and resolves it to a value of type `value`. The following variants of `TxConstraint` @@ -320,12 +323,12 @@ data TxConstraint (resolved :: Bool) script Ensure - The sum of input utxos belonging to `user` is greater than `inValue` - - The sume of output utxos belonging to `user` is greater than `outValue` + - The sum of output utxos belonging to `user` is greater than `outValue` - `MainSignerNoValue address` Ensure that the given address is part of the transaction signatories. - `Error message` Output `message` using `ptrace` as an error message. - `If` - Evaluate the condition and resolve to the `TxConstraint` in the “then” branch or the “else” branch. -- `MatchBySpine pattern map` Evaluate pattern and execute the corresponding action from `map` +- `MatchBySpine pattern map` Evaluate the pattern and execute the corresponding action from `map` - `map` Map from `Spine` to `TxConstraint` In addition to the above, CEMScript provides the following helper functions to create `TxConstraint`s @@ -343,9 +346,9 @@ byFlagError flag message = If flag (Error message) Noop ``` -- `cNot` invert a boolean -- `offchainOnly` execute only on chain. Resolve to `Noop` off chain. -- `byFlagError` evaluate to `Error message` if `flag` evaluates to true. +- `cNot` inverts a boolean +- `offchainOnly` executes only on chain. Resolve to `Noop` off chain. +- `byFlagError` evaluates to `Error message` if `flag` evaluates to true. ### ConstraintDSL @@ -371,7 +374,7 @@ data ConstraintDSL script value where -- Primitives -- A wildcard pattern that matches any value. - -- Used in pattern matching contexts where the actual value is irrelevant. + -- Used in pattern-matching contexts where the actual value is irrelevant. Anything :: ConstraintDSL script x -- Compare two DSL values Eq :: (..) => ConstraintDSL script x -> ConstraintDSL script x -> ConstraintDSL script Bool @@ -415,7 +418,7 @@ cMinLovelace = cMkAdaOnlyValue $ Pure 3_000_000 (@==) = Eq ``` -The following are lifted versions of plutrach operators +The following are lifted versions of Plutarch operators ```haskell (@<=) -- #<= @@ -438,8 +441,8 @@ The following are lifted versions of plutrach operators ### How to define a script -- Define an empty type for your script: `data MyScript` , where MyScript can be any name. -- Define a `CEMScript` instance for it by providing `Params`, `State`, `Transition`, `transitionSpec` and optionally `transitionComp`. +- Define an empty type for your script: `data MyScript`, where MyScript can be any name. +- Define a `CEMScript` instance for it by providing `Params`, `State`, `Transition`, `transitionSpec`, and optionally `transitionComp`. - Do Template Haskell derivations (`deriveCEMAssociatedTypes`) to generate data and spine instances for pattern matching. - Invoke the `compileCEM` function (e.g., `$(compileCEM True ''MyScript)`) to process the DSL specification, compile optional `transitionComp` code, and produce a `CEMScriptCompiled` instance. - This generates an instance of `CEMScriptCompiled` for your script type. @@ -449,13 +452,15 @@ The following are lifted versions of plutrach operators #### Setup: The Types -First we define a type to denote our script. It’s an uninhabited type, it can’t be constructed. It’s only used as a tag for connecting different type classes together. +First, we define a type to denote our script. It’s an uninhabited type, it can’t be constructed. +It’s only used as a tag for connecting all instances of type classes together. ```haskell data SimpleAuction ``` -We define a type for the read-only state of our script. This state can’t be modified once created. This becomes the `Params` associated type of the `CEMScript` typeclass. +We define a type for the read-only state of our script. This state can’t be modified once created. +This becomes the `Params` associated type of the `CEMScript` type class. ```haskell data SimpleAuctionParams = MkAuctionParams @@ -465,7 +470,7 @@ data SimpleAuctionParams = MkAuctionParams deriving stock (Prelude.Eq, Prelude.Show) ``` -We define a type for the evolving state of our script. This becomes the `State` associated type of the `CEMScript` typeclass. +We define a type for the evolving state of our script. This becomes the `State` associated type of the `CEMScript` type class. ```haskell data Bid = MkBid @@ -487,7 +492,7 @@ data SimpleAuctionState deriving stock (Prelude.Eq, Prelude.Show) ``` -Lastly, we define a type for the state transitions of our script. This becomes the `Transition` associated type of the `CEMScript` typeclass. +Lastly, we define a type for the state transitions of our script. This becomes the `Transition` associated type of the `CEMScript` type class. ```haskell data SimpleAuctionTransition @@ -501,7 +506,10 @@ data SimpleAuctionTransition deriving stock (Prelude.Eq, Prelude.Show) ``` -We can now define an instance of the `CEMScriptTypes` for `SimpleAuction` . `CEMScriptTypes` is a super class of `CEMScript`, which just includes the associated types. By defining the associated types separately, we can use the `deriveCEMAssociatedTypes` template haskell function to generate some boilerplate. +We can now define an instance of the `CEMScriptTypes` for `SimpleAuction`. +`CEMScriptTypes` is a superclass of `CEMScript`, which just includes the associated types. +By defining the associated types separately, we can use the `deriveCEMAssociatedTypes` +Template Haskell function to generate some boilerplate. ```haskell instance CEMScriptTypes SimpleAuction where @@ -512,9 +520,11 @@ instance CEMScriptTypes SimpleAuction where $(deriveCEMAssociatedTypes False ''SimpleAuction) ``` -`deriveCEMAssociatedTypes` just executes `derivePlutusSpine` for all three of the associated types. But it can only do that if all the members of a type have a `HasPlutusSpine` implementation. This is why we need to do `derivePlutusSpine` for the `Bid` type ourselves. +`deriveCEMAssociatedTypes` just executes `derivePlutusSpine` for all three of the associated types. +But it can only do that if all the members of a type have a `HasPlutusSpine` implementation. +This is why we need to do `derivePlutusSpine` for the `Bid` type ourselves. -The boolean argument to `deriveCEMAssociatedTypes` is unused for now, and it is recommended to use a value of `False` . +The boolean argument to `deriveCEMAssociatedTypes` is unused for now, and it is recommended to use a value of `False`. #### Implementation @@ -524,13 +534,14 @@ To implement the logic of our script, we define an instance of `CEMScript` for o instance CEMScript SimpleAuction where ``` -We provide a value for `compilationConfig` , which at the moment contains only a prefix for error codes to tell errors from different programs apart. +We provide a value for `compilationConfig`, which at the moment contains +only a prefix for error codes to tell errors from different programs apart. ```haskell compilationConfig = MkCompilationConfig "AUC" ``` -Next comes the meat of the script: `transitionSpec` . This is where we define state transitions +Next comes the meat of the script: `transitionSpec`. This is where we define state transitions We create a Map of `Spine (Transition script)` → `[TxConstraint False script]` @@ -556,7 +567,7 @@ auctionValue = cMinLovelace @<> ctxParams.lot We make extensive use of `OverloadedRecordDot` and custom `HasField` instances to make accessing the fields of the params and state values ergonomic. -Let’s examine each of the entries of the map in detail. +Let’s examine each of the entries in the map in detail. 1. Create From 3851e7b4151ca6e2ee5d758835560c239a8a2d3c Mon Sep 17 00:00:00 2001 From: euonymos Date: Mon, 20 Jan 2025 16:28:45 -0600 Subject: [PATCH 04/15] feat: revise exising goals and design --- docs/catalyst_milestone_reports.md | 9 +- docs/goals_and_design.md | 487 +++++++++++++++++++++++++++++ src/Cardano/CEM/DSL.hs | 4 +- 3 files changed, 496 insertions(+), 4 deletions(-) create mode 100644 docs/goals_and_design.md diff --git a/docs/catalyst_milestone_reports.md b/docs/catalyst_milestone_reports.md index 487292a..30affcb 100644 --- a/docs/catalyst_milestone_reports.md +++ b/docs/catalyst_milestone_reports.md @@ -6,9 +6,14 @@ * [Basic indexing support PR #98](https://github.com/mlabs-haskell/cem-script/pull/98) * [Oura config generation PR #100](https://github.com/mlabs-haskell/cem-script/pull/100) * [Source](https://github.com/mlabs-haskell/cem-script/blob/master/src/Cardano/CEM/Indexing.hs) - * [Tests for Auction example](https://github.com/mlabs-haskell/cem-script/blob/master/test/OuraFilter/Auction.hs) -* Final code clean-up + * [Indexing tests for Auction example](https://github.com/mlabs-haskell/cem-script/blob/master/test/OuraFilter/Auction.hs) +* Final code clean-up: + * [PR#113 - finalize mutation tests](https://github.com/mlabs-haskell/cem-script/pull/113) + * [PR#109 - cosmetic changes](https://github.com/mlabs-haskell/cem-script/pull/109) * Final tutorial and docs + * [PR on docs](https://github.com/mlabs-haskell/cem-script/pull/115) + * [Getting Started Guide](https://github.com/mlabs-haskell/cem-script/pull/115/files#diff-31bcba2ccafa41d46fbbd6d1219f7f1e3b1fb3cad9faa8e4dc521bbb579dd7b3) + * Updated [Goals And Design](TODO: link) ## Clarifications on M3 Deliverables diff --git a/docs/goals_and_design.md b/docs/goals_and_design.md new file mode 100644 index 0000000..06c2b4e --- /dev/null +++ b/docs/goals_and_design.md @@ -0,0 +1,487 @@ +# CEM Script project: goals and design + +## Why Cardano dApp modeling language is important? + +While prototypes can be easily constructed with existing Cardano frameworks, +making it secure and production ready is a sisyphean task. + +We believe, that onchain PL improvements by themselves could not change that. +Only higher-level modeling framework can lead to reliable dApp production. + +In following enumerate our high-level design goals +and demonstrate them by list of specific problems +arising in existing dApps codebase. + +Such problems are specific security vulnerabilities types +and various kinds development, audit and support cost increase. +After that we examine how existing solutions +are covering our high-level goals. + +## High-level goals + +1. dApp logic as a whole (synced-by-construction) +2. Code is free from common security weaknesses by construction (secure-by-construction) +3. Seamlessly emulate and test anything (emulate-anything) +4. Being declarative: close to informal specification and +bridging lightweight formal methods (declarative-spec) +5. Generally production ready (production-ready) + +## The scope + +We restrict the scope of the project by deliberately +keeping some features out of the scope now and in foreseable future. +Among them: + +* Composable inter-dApp interactions +* dApp migrations +* Scheduled actions and bots + +Some features that can be thought as a part of the project +but which are not in the Fund10 Catalyst proposal: + +* CTL and overall frontend transaction construction model +* Metadata, reference scripts and non-inlined datums +* Stacking and governance features, apart for (security-by-default) +* ZK-proofs + +## Reference dApps + +Those are list of open-source dApps, +that we use to demonstrate problems is following: + +* Audited production dApps + * Agora + * MinSwap + * Fracada + * JPG Vesting Contract + * Indigo Protocol +* dApp projects we participated, audited or otherwise know their codebase + * Hydra Auction + * POCRE + * CNS +* Public dApp projects with specification + * [SundaeSwap](https://cdn.sundaeswap.finance/SundaeV3.pdf) +* Plutonomicon patterns +* Plutus tutorial + * [Game Model](https://github.com/IntersectMBO/plutus-apps/blob/dbafa0ffdc1babcf8e9143ca5a7adde78d021a9a/doc/plutus/tutorials/GameModel.hs) +* plutus-usecases + +## On-chain correctness + +### Known common vulnerabilities + +There is a list of known security vulnerabilities, +for which naive Plutus implementation is very often prone to. +Our implementation makes them impossible to happen, +taking that burden from developers and auditors. + +* Double satisfaction + * Shown twice in CNS Audit + * Shown once in Fracada audit (3.2.7) +* Insufficient staking control + * Shown once in CNS Audit - https://github.com/mlabs-haskell/cns-plutus-audit/issues/24 + +### TxIn ordering and coin change support + +Those problems are similar to previous in that they tend to +arise in naive Plutus implementations, +if developers did not take measures to prevent them. + +Plutus forces developers to write TxIn/TxOut constraints from scratch, +leading by subtle bugs from copy-pasting logic or +trying to optimize them by hand. + +Examples: +* Security bug in MinSwap audit - 2.2.1.3 Unauthorized Hijacking of Pools Funds +* Non-security bug in MinSwap audit - 2.2.2.2 Batcher Is Not Allowed to Apply Their Own Order + +Most of transactions which require fungible tokens as input, +should not depend on exact UTxO coin-change distribution. +Failure to expect that leads to prohibition of correct transactions. +On other side too broad constraint might lead to fund stealing. + +See an example of such a [bug](https://github.com/mlabs-haskell/hydra-auction/issues/146). + +Another important case is maintaining invariants +of token value or immutable UTxOs. +Such kind of constraints naturally lead to scripts +for which more performant implementation should +eliminate some constraint following from others. +Such kind of manual SMT solving exercises are +known source for security bugs and complicated code. +Checking all constraints leads to code bloat +in form of bunch of utility functions which is +suboptimal. +Making Plutus contract invariant to `TxIn` ordering +and participat* `availableVestings` - пример чего-то подобного для SimpleAuctionion in multi-script scenarios lead to +similar kind of complications. + +Examples: +* Non-security bug: https://github.com/mlabs-haskell/hydra-auction/issues/129 +* Non-security bug: https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997 +* Non-intentionally under-specified behavior in MinSwap audit: + * `2.2.2.1 Batchers Can Choose Batching Order` + * `2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs"` +* Multiple kind of code complications was observed in CNS audit. +* Utilities [from Indigo](https://github.com/IndigoProtocol/indigo-smart-contracts/blob/main/src/Indigo/Utils/Spooky/Helpers.hs) + +### Single script safety and liveliness + +Main feature of any correct application is that it +behave same way as it specification presumes. In our case +specification for single script is a CEM state machine, +and correctness means that on-chain script have exactly +same transitions possible. + +On-chain scripts having transition not possible in model +usually leads to security vulnerability. Other way around +it might be DoS vulnerability or just usability bug. +We aim to check most of such problems automatically. +Almost all on-chain code bugs are specific cases of +such violations, at least once we are analyzing +not single script, but a whole dApp, see the next section. + +One very important example of liveliness violation +is originated from Cardano Tx limits. Such kind +of bugs are very hard to detect, without transaction fuzzing. +Such fuzzing can be automated as part of our testing framework. +Moreover, similar task of script usecase benchmarking +can be covered by same automation. Such kind of benchmarking, +either on list of scenarios or arbitrary generated inputs +is essential for checking economics and performance +regressions of dApps. + +### Multiple script safety and liveliness + +Whole dApp may be modeled as another kind of a state machine. +It operates a level above - the whole dApp and generates +specific script transitions. + +Liveliness could be checked the same way with `quickcheck-dynamic` +or by providing specific usecases just as with single script case. + +Safety checks is harder to automate. +This is not in the scope of current Catalyst project +but it should be possible to cover this case +by employing constraint equivalence check, +and verifying that any deviation from generated transitions +don't get through. +Another solution might be mutation testing. +Such kind of vulnerabilities are now the most complex kind of attack +to consider as part of dApps design or auditing. +Thus, automating it away may be very beneficial. + +### Time and stages handling + +Plutus time is described by allowed intervals. +Such abstraction is prone to off-by-one and similar errors. +At least three errors of this kind are known in Cardano/Plutus +interval logic, showing being not simple to implement +correctly. + +Another problem is keeping time logic in sync between on- +and off-chain code. This is even harder given that Plutus time +to slot conversion gets into the way. +Slot time differences and overall need to make test cases match +real blockchain behavior may lead to flaky test behavior. + +Our script stages abstraction cover all those kind of problems. + +### Matching to off-chain logic + +Problem of duplicating logic between on-chain and off-chain is twofold. +Testing is essentially done offchain, thus, one may easily miss +that your on-chain code is not actually enforcing some parts of +a transaction provided in tests. + +CEM Script is constructing transactions for submission from exactly +the same specification used for on-chain script. +Thus it is much harder to miss constraint to be checked. + +Examples: +* MinSwap audit - 2.2.1.2 LP Tokens Can Be Duplicated + +### Logic duplication + +There is a bunch of very common tasks shared by multiple dApps, +which could be tackled generically in framework like CEM Script. + +## Human-readable specification + +Designing, understanding and auditing any non-trivial dApp +is almost impossible without a human-readable spec. +That is why in all reference dApps there either existed +a spec or it was asked to be provided by an auditor. +Tweag and MLabs audits specifically list validating +provided specification as one of main tasks of an audit. + +This leads to lot of cruft with writing, linking, and +updating specifications. Quite often not only one but +up to three levels of spec granularity which worsens +the situation. +We observe great amount of cruft and spec rot in all +projects we were personally involved. +Such kind of cruft is often present not only on level +of single developers, but on the community level. + +Such kind of human-readable specs are very much similar to our model, +they almost always include enumeration of possible transitions +and/or state-machine diagrams. +Our project will generate such kind of specifications automatically. +Adding usecases scenarios generated from those specified in tests +is much less obvious to implement and out of scope of current project +but it is a very much possible feature as well. + +Examples of this done by hand: +* [State graph for Agora](https://github.com/Liqwid-Labs/agora/blob/staging/docs/diagrams/ProposalStateMachine.png) + +### On-chaion, off-chain, and spec logic duplication + +Writing on-chain contracts manually encodes non-deterministic +state machine that cannot be used for off-chain transaction +construction. +Thus developer need to write them again in different style +for off-chain code which is tedious and error-prone. + +They should add checks for all errors possible, +like coins being available and correct script states being present, +to prevent cryptic errors and provide retrying strategies +for possible utxo changes. + +Our project encodes scripts in the form of a deterministic machine, +which contains enough information to construct transaction automatically. +This also gives a way to check for potential on-chain vs off-chain logic differences semi-automatically. + +Examples: +* MinSwap Audit - 2.2.4.3 Large Refactoring Opportunities + +### Computer readable spec and hashes + +Script hashes and sizes summary is essential for dApp users +and testers to check on-chain script are matching. +We provide generic implementation showing all dApp hashes +via CIP. + +### Indexing and querying code duplication + +Our framework simplifies generation of common queries and +custom indexing. + +Querying of current script state is required for almost all dApps, +and they are usually implemented with bunch of boilerplate. + +Examples: +* [Querying available vestings](https://github.com/geniusyield/atlas-examples/blob/main/vesting/offchain/Vesting/Api.hs#L27) + +Customized transaction indexing is important for providing +data to almost any kind of custom web-backend. +Customized indexing may reduce storage space or SaaS dependence. + +Indexing transactions and parsing it back to state-machine transition +is required for delegated architectures, including many dApps and Hydra L2. + +Examples: +* https://github.com/MELD-labs/cardano-defi-public/tree/eacaa527823031105eba1730f730e1b32f1470bc/lending-index/src/Lending/Index + +## Existing solutions + +This section covers some existing approches that can be +considered competative to CEM Script project. + +## IOG's Plutus Application Framework + +PABs `state-machines` and `plutus-contract-model` package +are the ony existing project close to our design. + +They are providing CEM state machine model script, +translatable to on-chain and off-chain code. +On top of that you may specify custom `ContractModel` +specifying multi-script dApp as a whole, +and model check your custom invariants and +very generic "CrashTolerance" safety property +and "No Locked Funds" liveliness property. +Thus they are the only project known to us, +which aim to cover (declarative-spec) +and (synced-by-construction) goals. + +This model is generic and covered in Plutus Pioneer tutorial, +thus already known to many people. +Our design is based on very similar model. +Unfortunately, existing `plutus-apps` solution seems +to be completely not (production-ready). +We could not find any `ContractModel` usage example on GitHub, +the repository is archived and thus it does seem that it is indeed +not much used in practice. +Also they provide much less free guaranties and features +then we aim to. As we will explain in the following sections, +this is most probably impossible to fix without significant +changes within design of PAB. + +State Machine to on-chain translation is very naive +and would not produce optimal code in multiple typical cases. +Constraint language used by PAB is fundamentally more expressible +than ours, and that complicates possibility of implementing +required optimizations. + +Same logic stands for (security-by-default) goal, +in particular providing SMT encoding for constrains, +which may be used to drastically shrink model-check fuzzing space +or even completely remove a need to use fuzzing. +Automatic check for various other important security properties, +like almost-determinism is complicated as well. + +Another important restriction is the fact that PAB's +state machines always produce state-thread-token contract. +This makes impossible to encode tree like UTxO based data-structures, +which are used for encoding all kinds of public registry logic. +Also it prohibits any kind of non-trivial state-thread-token logic, +like optimization by sharing (used for example in `hydra-auction`) +and multiple commiters schemes (used in `hydra`). + +### GeniusYield's Atlas PAB + +Atlas provides more humane DX on top of `cardano-api`. +But it has no features related to the goals of +(synced-by-construction), (secure-by-construction), +and (declarative-spec). +Currently is covers (emulate-everything) though. + +Atlas includes connectors to Blockfrost and other backends, +which our project lacks. + +Also our project has slight differences in API design decisions. +Our monad interfaces is meant to be slightly more modular. +We use much less custom type wrappers, resorting to Plutus +types where possible. + +### Tweag's cooked-validators + +The project definitely covers the (production-ready) goal, +because it was successfully used in real-world audits. +but only partially covers +(emulate-anything) and (declarative-spec) goals. + +While it, surely, can do transaction emulation, +it, to best of our knowledge, does not have monad instance +for real L1 blockchain. So one still cannot reuse same code +across tests and real blockchain Tx construction. + +`TxSkel` datatype is similar to design we are implementing, +and other parts API have a lot of cool DX decisions. +But `cooked-validators` lack script transition model, +so it cannot provide declarative Tx submission error handling +we aim to get, because it does not have information to decide, +if specific Tx input is critical (like auth token), +or can be re-selected again (like coin-selected ADA for payment). + +Having declarative transition model is even +more important for mutation testing purposes. +For construction of mutations `cooked-validators` +gives low-level Cardano API. +That means, that you should select, write and evaluate +them manually, depending on logic in scripts. +This lead to logic coupling between spec, L1 code and test code. +Such coupling and overall manual construction +complicates spec validation and might lead +to attack vectors missed by accident. + +Our API presumes that means of on-script validation, +in our case behavior equivalence (AKA bi-similarity) +of a declarative CEM state machine and a real +on-chain script is verified and validated semi-automatically. +Also we plan to make some kind of vulnerabilities covered by +`cooked-validators` impossible by construction, +specifically in modules: +`ValidityRange`, `DoubleSat`, `AddInputsAndOutputs` +and `OutPermutations`. + +Another important feature is support for LTL logic formulas, +which are known language for specifying state transitions in BMC. +It seems like this feature is subsumed by +`quickcheck-dynamic` based model checking specification +we are going to provide. + +### Mutation-based testing of Hydra's validators + +[Hydra mutations](https://abailly.github.io/posts/mutation-testing.html) +are similar to `cooked-validators` in their design +and have similar drawback. +Thus they do not cover (synced-by-construction), +(secure-by-construction), +and (declarative-spec) goals. + +### tasty-plutus + +Only cover (emulate-anything) goal, does not aim to cover others +and is not being developer either. +On the other hand it has some interesting low-level features, +like `plutus-size-check`. + +### On-chain PLs and CIP-30 wrappers + +Any kind of on-chain PL can only cover goals +(emulate-anything) and (production-readiness). +As far as we aware, none of them are trying +to solve other goals. + +Known examples of PLs: + +* [Marlowe](https://github.com/input-output-hk/marlowe-plutus) + - Finance contracts DSL +* [Aiken](https://aiken-lang.org/) + - on-chain PL with IDE support and testing framework +* [Helios](https://www.hyperion-bt.org/helios-book/api/index.html) + - on-chain PL and frontend Tx sending library +* [OpShin](https://github.com/OpShin/opshin) + - on-chain PL +* [Purus](https://github.com/mlabs-haskell/purus) + - on-chain PL based on PureScript compiler (WIP by MLabs) + +The same stands for any known kind of frontend frameworks: + +* [CTL](https://github.com/Plutonomicon/cardano-transaction-lib) +* [lucid-evolution](https://github.com/Anastasia-Labs/lucid-evolution) +* [meshjs.dev](https://meshjs.dev/) + +Same stands for any kind of `cardano-api` API translation to other PLs: + +* [Transaction Village](https://github.com/mlabs-haskell/tx-village) +* [PyCardano](https://pycardano.readthedocs.io/en/latest/guides/plutus.html) +* [Cardano Multiplatform Lib](https://github.com/dcSpark/cardano-multiplatform-lib) + +## Architectural principles + +### Constraints design + +* Generic compilation across: + * on-chain code + * off-chain tx construction + * indexing backend +* Constraints determine input and outputs up to UTxO coin-selection (we call it almost-determinacy) +* Datum properties encoded as type classes +* Common on-chain optimizations are performed if possible + * Constraints normalization + * Best error short-cutting + * Common security problems prevention + +### CEM machine design + +As it is done on top of constraints language, +all their principles and obstacles are affecting CEM as well: + +* State-machine is deterministic modulo coin-selection +* Transaction can always be parsed back into CEM transitions +* Potential non-deterministic on-chain optimizations should not affect + +### General Haskell verification tools + +The definition of the property we aim to check is simple +and completely generic: + +> Given a transaction with some UTxO context, and a function +> that generates SomeMutation from a valid transaction and +> context pair, this property checks applying any generated +> mutation makes the transaction invaild. + +We are using `quickcheck-dynamic`library to run model-based +testing and mutation-based testing. \ No newline at end of file diff --git a/src/Cardano/CEM/DSL.hs b/src/Cardano/CEM/DSL.hs index ad53157..4c074aa 100644 --- a/src/Cardano/CEM/DSL.hs +++ b/src/Cardano/CEM/DSL.hs @@ -346,8 +346,8 @@ class -- | The crux part - a map that defines constraints for each transition via DSL. transitionSpec :: CEMScriptSpec False script - -- | Optional Plutus script to calculate things, whic can be used in the cases - -- when CEM constrainsts and/or inlining Plutarch functions are not expresisble + -- | Optional Plutus script to calculate things, which can be used in the cases + -- when CEM constraints and/or inlining Plutarch functions are not expressible -- enough. transitionComp :: Maybe From 222a69aa018dfd7123007173b083315cc66797fd Mon Sep 17 00:00:00 2001 From: Ilia Rodionov <103441514+euonymos@users.noreply.github.com> Date: Tue, 21 Jan 2025 10:56:59 -0600 Subject: [PATCH 05/15] chore: goal and design typos and wording --- docs/goals_and_design.md | 316 ++++++++++++++++++++------------------- 1 file changed, 160 insertions(+), 156 deletions(-) diff --git a/docs/goals_and_design.md b/docs/goals_and_design.md index 06c2b4e..5759b7f 100644 --- a/docs/goals_and_design.md +++ b/docs/goals_and_design.md @@ -1,22 +1,26 @@ # CEM Script project: goals and design -## Why Cardano dApp modeling language is important? +## Why is Cardano dApp modeling language important? While prototypes can be easily constructed with existing Cardano frameworks, -making it secure and production ready is a sisyphean task. +making it secure and production-ready is a Sisyphean task. -We believe, that onchain PL improvements by themselves could not change that. -Only higher-level modeling framework can lead to reliable dApp production. +On-chain PL improvements could not change that by themselves. +Only a higher-level modeling framework can lead to reliable dApp production. -In following enumerate our high-level design goals -and demonstrate them by list of specific problems -arising in existing dApps codebase. +In the following, we enumerate our high-level design goals +and demonstrate them by listing specific problems that +arouse in the existing dApps codebase. -Such problems are specific security vulnerabilities types -and various kinds development, audit and support cost increase. -After that we examine how existing solutions +Such problems are specific security vulnerabilities of different +types. They are still common in development which increases +audit and support costs. + +Also, this document describes how existing solutions are covering our high-level goals. +Finally, we describe high-level architecture. + ## High-level goals 1. dApp logic as a whole (synced-by-construction) @@ -24,30 +28,30 @@ are covering our high-level goals. 3. Seamlessly emulate and test anything (emulate-anything) 4. Being declarative: close to informal specification and bridging lightweight formal methods (declarative-spec) -5. Generally production ready (production-ready) +5. Being generally production-ready (production-ready) ## The scope We restrict the scope of the project by deliberately -keeping some features out of the scope now and in foreseable future. +keeping some features out of the scope now and in the foreseeable future. Among them: * Composable inter-dApp interactions * dApp migrations * Scheduled actions and bots -Some features that can be thought as a part of the project +Some features that can be thought of as a part of the project but which are not in the Fund10 Catalyst proposal: * CTL and overall frontend transaction construction model -* Metadata, reference scripts and non-inlined datums -* Stacking and governance features, apart for (security-by-default) +* Metadata, reference scripts, and non-inlined datums +* Stacking and governance features, apart from (security-by-default) * ZK-proofs ## Reference dApps -Those are list of open-source dApps, -that we use to demonstrate problems is following: +Those are a list of open-source dApps, +that we use to demonstrate problems: * Audited production dApps * Agora @@ -55,7 +59,7 @@ that we use to demonstrate problems is following: * Fracada * JPG Vesting Contract * Indigo Protocol -* dApp projects we participated, audited or otherwise know their codebase +* dApp projects we participated in, audited, or otherwise know their codebase * Hydra Auction * POCRE * CNS @@ -71,177 +75,179 @@ that we use to demonstrate problems is following: ### Known common vulnerabilities There is a list of known security vulnerabilities, -for which naive Plutus implementation is very often prone to. -Our implementation makes them impossible to happen, +for which naive Plutus implementation is often prone. +Our implementation eliminates them, taking that burden from developers and auditors. * Double satisfaction * Shown twice in CNS Audit - * Shown once in Fracada audit (3.2.7) + * Shown once in the Fracada audit (3.2.7) * Insufficient staking control - * Shown once in CNS Audit - https://github.com/mlabs-haskell/cns-plutus-audit/issues/24 + * [Shown once in CNS Audit](https://github.com/mlabs-haskell/cns-plutus-audit/issues/24) ### TxIn ordering and coin change support -Those problems are similar to previous in that they tend to +Those problems are similar to previous ones in that they tend to arise in naive Plutus implementations, if developers did not take measures to prevent them. Plutus forces developers to write TxIn/TxOut constraints from scratch, leading by subtle bugs from copy-pasting logic or -trying to optimize them by hand. +trying to optimize it by hand. Examples: * Security bug in MinSwap audit - 2.2.1.3 Unauthorized Hijacking of Pools Funds * Non-security bug in MinSwap audit - 2.2.2.2 Batcher Is Not Allowed to Apply Their Own Order -Most of transactions which require fungible tokens as input, +Most transactions that require fungible tokens as input, should not depend on exact UTxO coin-change distribution. -Failure to expect that leads to prohibition of correct transactions. -On other side too broad constraint might lead to fund stealing. +Failure to expect that leads to the prohibition of correct transactions. +On the other hand, too weak constraints might lead to fund stealing. See an example of such a [bug](https://github.com/mlabs-haskell/hydra-auction/issues/146). Another important case is maintaining invariants of token value or immutable UTxOs. -Such kind of constraints naturally lead to scripts +Such kinds of constraints naturally lead to scripts for which more performant implementation should -eliminate some constraint following from others. -Such kind of manual SMT solving exercises are -known source for security bugs and complicated code. +eliminate some constraints following from others. +Such kind of manual SMT-solving exercises are +a known source of security bugs and complicated code. Checking all constraints leads to code bloat -in form of bunch of utility functions which is +in the form of a bunch of utility functions which is suboptimal. Making Plutus contract invariant to `TxIn` ordering -and participat* `availableVestings` - пример чего-то подобного для SimpleAuctionion in multi-script scenarios lead to -similar kind of complications. +in multi-script scenarios leads to similar kinds of complications. Examples: -* Non-security bug: https://github.com/mlabs-haskell/hydra-auction/issues/129 -* Non-security bug: https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997 -* Non-intentionally under-specified behavior in MinSwap audit: - * `2.2.2.1 Batchers Can Choose Batching Order` - * `2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs"` -* Multiple kind of code complications was observed in CNS audit. +* [Non-security bug in Hydra Auctions #1](https://github.com/mlabs-haskell/hydra-auction/issues/129) +* [Non-security bug in Hydra Auctions #2](1https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997) +* Non-intentionally under-specified behavior in MinSwap audit + * 2.2.2.1 "Batchers Can Choose Batching Order" + * 2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs" +* Multiple kinds of code complications were observed in the CNS audit. * Utilities [from Indigo](https://github.com/IndigoProtocol/indigo-smart-contracts/blob/main/src/Indigo/Utils/Spooky/Helpers.hs) ### Single script safety and liveliness -Main feature of any correct application is that it -behave same way as it specification presumes. In our case -specification for single script is a CEM state machine, -and correctness means that on-chain script have exactly +The main feature of any correct application is that it +behave the same way as its specification presumes. In our case +specification for a single script is a CEM state machine, +and correctness means that on-chain scripts have exactly same transitions possible. -On-chain scripts having transition not possible in model -usually leads to security vulnerability. Other way around -it might be DoS vulnerability or just usability bug. +On-chain scripts having transition not possible in the model +usually lead to security vulnerability. Another way around +it might be a DoS vulnerability or just a usability bug. We aim to check most of such problems automatically. Almost all on-chain code bugs are specific cases of such violations, at least once we are analyzing -not single script, but a whole dApp, see the next section. +not a single script, but a whole dApp, see the next section. One very important example of liveliness violation -is originated from Cardano Tx limits. Such kind +originated from Cardano transaction limits. Such kind of bugs are very hard to detect, without transaction fuzzing. Such fuzzing can be automated as part of our testing framework. -Moreover, similar task of script usecase benchmarking -can be covered by same automation. Such kind of benchmarking, -either on list of scenarios or arbitrary generated inputs -is essential for checking economics and performance +Moreover, the similar task of script use case benchmarking +can be covered by the same automation based either on +a list of scenarios or arbitrarily generated inputs. +It is essential for checking the economics and performance regressions of dApps. ### Multiple script safety and liveliness -Whole dApp may be modeled as another kind of a state machine. +The whole dApp may be modeled as another kind of a state machine. It operates a level above - the whole dApp and generates specific script transitions. Liveliness could be checked the same way with `quickcheck-dynamic` -or by providing specific usecases just as with single script case. +or by providing specific use cases just as with a single script case. -Safety checks is harder to automate. -This is not in the scope of current Catalyst project +Safety checks are harder to automate. +This is not in the scope of the current Catalyst project but it should be possible to cover this case by employing constraint equivalence check, and verifying that any deviation from generated transitions don't get through. Another solution might be mutation testing. + Such kind of vulnerabilities are now the most complex kind of attack to consider as part of dApps design or auditing. Thus, automating it away may be very beneficial. ### Time and stages handling -Plutus time is described by allowed intervals. +Time in Plutus is described by allowed intervals. Such abstraction is prone to off-by-one and similar errors. At least three errors of this kind are known in Cardano/Plutus -interval logic, showing being not simple to implement -correctly. +interval logic, showing that it is not easy to do. Another problem is keeping time logic in sync between on- -and off-chain code. This is even harder given that Plutus time -to slot conversion gets into the way. +and off-chain code. This is even harder given that Plutus' +time-to-slot conversion gets in the way. Slot time differences and overall need to make test cases match real blockchain behavior may lead to flaky test behavior. -Our script stages abstraction cover all those kind of problems. +Our script stages abstraction cover all those kinds of problems. ### Matching to off-chain logic -Problem of duplicating logic between on-chain and off-chain is twofold. -Testing is essentially done offchain, thus, one may easily miss +The problem of duplicating logic between on-chain and off-chain +is twofold. +Testing is essentially done off-chain, thus, one may easily miss that your on-chain code is not actually enforcing some parts of a transaction provided in tests. CEM Script is constructing transactions for submission from exactly -the same specification used for on-chain script. -Thus it is much harder to miss constraint to be checked. +the same specification used for the on-chain script. +Thus it is much harder to miss a constraint to be checked. Examples: -* MinSwap audit - 2.2.1.2 LP Tokens Can Be Duplicated +* MinSwap audit - 2.2.1.2 "LP Tokens Can Be Duplicated" ### Logic duplication -There is a bunch of very common tasks shared by multiple dApps, -which could be tackled generically in framework like CEM Script. +There are a bunch of very common tasks shared by multiple dApps, +which could be tackled generically in a framework like CEM Script. ## Human-readable specification -Designing, understanding and auditing any non-trivial dApp +Designing, understanding, and auditing any non-trivial dApp is almost impossible without a human-readable spec. That is why in all reference dApps there either existed a spec or it was asked to be provided by an auditor. Tweag and MLabs audits specifically list validating -provided specification as one of main tasks of an audit. +provided specification as one of the main tasks of an audit. -This leads to lot of cruft with writing, linking, and +This leads to a lot of cruft with writing, linking, and updating specifications. Quite often not only one but up to three levels of spec granularity which worsens the situation. -We observe great amount of cruft and spec rot in all + +We observe a great amount of cruft and spec rot in all projects we were personally involved. Such kind of cruft is often present not only on level of single developers, but on the community level. Such kind of human-readable specs are very much similar to our model, -they almost always include enumeration of possible transitions +they almost always include an enumeration of possible transitions and/or state-machine diagrams. Our project will generate such kind of specifications automatically. -Adding usecases scenarios generated from those specified in tests -is much less obvious to implement and out of scope of current project + +Adding use case scenarios generated from those specified in tests +is much less obvious to implement and out of the scope of the current project but it is a very much possible feature as well. Examples of this done by hand: * [State graph for Agora](https://github.com/Liqwid-Labs/agora/blob/staging/docs/diagrams/ProposalStateMachine.png) -### On-chaion, off-chain, and spec logic duplication +## On-chain, off-chain, and spec logic duplication Writing on-chain contracts manually encodes non-deterministic -state machine that cannot be used for off-chain transaction +state machine that cannot be used directly for off-chain transaction construction. -Thus developer need to write them again in different style -for off-chain code which is tedious and error-prone. +Thus developers need to write them again in a different style +for off-chain code which is a tedious and error-prone work. They should add checks for all errors possible, like coins being available and correct script states being present, @@ -249,53 +255,54 @@ to prevent cryptic errors and provide retrying strategies for possible utxo changes. Our project encodes scripts in the form of a deterministic machine, -which contains enough information to construct transaction automatically. -This also gives a way to check for potential on-chain vs off-chain logic differences semi-automatically. +which contains enough information to construct transactions automatically. +This also gives a way to check for potential on-chain +vs off-chain logic differences semi-automatically. Examples: -* MinSwap Audit - 2.2.4.3 Large Refactoring Opportunities +* MinSwap Audit - 2.2.4.3 "Large Refactoring Opportunities" -### Computer readable spec and hashes +## Computer readable spec and hashes Script hashes and sizes summary is essential for dApp users -and testers to check on-chain script are matching. -We provide generic implementation showing all dApp hashes -via CIP. +and testers to check that on-chain scripts are matching. +We provide a generic implementation showing all dApp hashes. -### Indexing and querying code duplication +## Indexing and querying code duplication -Our framework simplifies generation of common queries and +Our framework simplifies the generation of common queries and custom indexing. -Querying of current script state is required for almost all dApps, -and they are usually implemented with bunch of boilerplate. +Querying the current script state is required for almost all dApps, +and they are usually implemented with a bunch of boilerplate. Examples: * [Querying available vestings](https://github.com/geniusyield/atlas-examples/blob/main/vesting/offchain/Vesting/Api.hs#L27) Customized transaction indexing is important for providing -data to almost any kind of custom web-backend. +data to almost any kind of custom web backend. Customized indexing may reduce storage space or SaaS dependence. -Indexing transactions and parsing it back to state-machine transition +Indexing transactions and parsing them back to state-machine transition is required for delegated architectures, including many dApps and Hydra L2. Examples: -* https://github.com/MELD-labs/cardano-defi-public/tree/eacaa527823031105eba1730f730e1b32f1470bc/lending-index/src/Lending/Index +* [Indexing in MELD Lending and Borrowing protocol](https://github.com/MELD-labs/cardano-defi-public/tree/eacaa527823031105eba1730f730e1b32f1470bc/lending-index/src/Lending/Index) ## Existing solutions -This section covers some existing approches that can be -considered competative to CEM Script project. +This section covers some existing approaches that can be +considered competitive to the project. ## IOG's Plutus Application Framework -PABs `state-machines` and `plutus-contract-model` package -are the ony existing project close to our design. +`state-machines` and `plutus-contract-model` packages from +the currently archived **Plutus Application Framework** +are only existing tools close to our design. They are providing CEM state machine model script, translatable to on-chain and off-chain code. -On top of that you may specify custom `ContractModel` +On top of that you may specify a custom `ContractModel` specifying multi-script dApp as a whole, and model check your custom invariants and very generic "CrashTolerance" safety property @@ -304,54 +311,54 @@ Thus they are the only project known to us, which aim to cover (declarative-spec) and (synced-by-construction) goals. -This model is generic and covered in Plutus Pioneer tutorial, +This model is generic and covered in the Plutus Pioneer tutorial, thus already known to many people. -Our design is based on very similar model. -Unfortunately, existing `plutus-apps` solution seems +Our design is based on a very similar model. +Unfortunately, the existing `plutus-apps` solution seems to be completely not (production-ready). We could not find any `ContractModel` usage example on GitHub, the repository is archived and thus it does seem that it is indeed not much used in practice. -Also they provide much less free guaranties and features -then we aim to. As we will explain in the following sections, +Also, they provide much less free guarantees and features +than we aim to. As we will explain in the following sections, this is most probably impossible to fix without significant -changes within design of PAB. +changes within the design of PAF/PAB. State Machine to on-chain translation is very naive and would not produce optimal code in multiple typical cases. Constraint language used by PAB is fundamentally more expressible -than ours, and that complicates possibility of implementing +than ours, and that complicates the possibility of implementing required optimizations. -Same logic stands for (security-by-default) goal, -in particular providing SMT encoding for constrains, +The same logic stands for (security-by-default) goal, +in particular, providing SMT encoding for constraints, which may be used to drastically shrink model-check fuzzing space -or even completely remove a need to use fuzzing. +or even completely remove the need to use fuzzing. Automatic check for various other important security properties, like almost-determinism is complicated as well. -Another important restriction is the fact that PAB's -state machines always produce state-thread-token contract. -This makes impossible to encode tree like UTxO based data-structures, +Another important restriction is the fact that PAF's +state machines always produce a __state-thread-token__ contract. +This makes it impossible to encode UTxO-based data structures, which are used for encoding all kinds of public registry logic. -Also it prohibits any kind of non-trivial state-thread-token logic, +Also, it prohibits any kind of non-trivial state-thread-token logic, like optimization by sharing (used for example in `hydra-auction`) and multiple commiters schemes (used in `hydra`). ### GeniusYield's Atlas PAB -Atlas provides more humane DX on top of `cardano-api`. +Atlas provides a more humane DX on top of `cardano-api`. But it has no features related to the goals of (synced-by-construction), (secure-by-construction), and (declarative-spec). -Currently is covers (emulate-everything) though. +Currently, it covers (emulate-everything) though. Atlas includes connectors to Blockfrost and other backends, which our project lacks. -Also our project has slight differences in API design decisions. -Our monad interfaces is meant to be slightly more modular. -We use much less custom type wrappers, resorting to Plutus +Also, our project has slight differences in API design decisions. +Our monad interfaces are meant to be slightly more modular. +We use much less custom-type wrappers, resorting to Plutus types where possible. ### Tweag's cooked-validators @@ -362,41 +369,41 @@ but only partially covers (emulate-anything) and (declarative-spec) goals. While it, surely, can do transaction emulation, -it, to best of our knowledge, does not have monad instance -for real L1 blockchain. So one still cannot reuse same code +it, to the best of our knowledge, does not have a monad instance +for real L1 blockchain. So one still cannot reuse the same code across tests and real blockchain Tx construction. -`TxSkel` datatype is similar to design we are implementing, -and other parts API have a lot of cool DX decisions. +`TxSkel` datatype is similar to the design we are implementing, +and other parts of API have a lot of cool DX decisions. But `cooked-validators` lack script transition model, -so it cannot provide declarative Tx submission error handling -we aim to get, because it does not have information to decide, -if specific Tx input is critical (like auth token), +so it cannot provide declarative transaction submission error handling +we aim to get because it does not have information to decide +whether a specific Tx input is critical (like an auth token), or can be re-selected again (like coin-selected ADA for payment). -Having declarative transition model is even +Having a declarative transition model is even more important for mutation testing purposes. -For construction of mutations `cooked-validators` +For the construction of mutations `cooked-validators` gives low-level Cardano API. -That means, that you should select, write and evaluate -them manually, depending on logic in scripts. -This lead to logic coupling between spec, L1 code and test code. +It means that you should select, write, and evaluate +them manually, depending on the logic in the scripts. +This leads to logic coupling between spec, L1 code, and test code. Such coupling and overall manual construction -complicates spec validation and might lead +complicate spec validation and might lead to attack vectors missed by accident. -Our API presumes that means of on-script validation, +Our API presumes that means of on-chain validation, in our case behavior equivalence (AKA bi-similarity) -of a declarative CEM state machine and a real -on-chain script is verified and validated semi-automatically. -Also we plan to make some kind of vulnerabilities covered by +of a declarative CEM state machine and a real on-chain +script is verified and validated semi-automatically. +Also, we plan to make some kind of the vulnerabilities covered by `cooked-validators` impossible by construction, specifically in modules: `ValidityRange`, `DoubleSat`, `AddInputsAndOutputs` and `OutPermutations`. Another important feature is support for LTL logic formulas, -which are known language for specifying state transitions in BMC. +which are known languages for specifying state transitions in BMC. It seems like this feature is subsumed by `quickcheck-dynamic` based model checking specification we are going to provide. @@ -405,23 +412,22 @@ we are going to provide. [Hydra mutations](https://abailly.github.io/posts/mutation-testing.html) are similar to `cooked-validators` in their design -and have similar drawback. -Thus they do not cover (synced-by-construction), -(secure-by-construction), +and have similar drawbacks. +Thus they do not cover (synced-by-construction), (secure-by-construction), and (declarative-spec) goals. ### tasty-plutus -Only cover (emulate-anything) goal, does not aim to cover others -and is not being developer either. -On the other hand it has some interesting low-level features, +This library only covers the (emulate-anything) goal, does not aim to cover others +and is not being actively developed either. +On the other hand, it has some interesting low-level features, like `plutus-size-check`. -### On-chain PLs and CIP-30 wrappers +### On-chain PLs Any kind of on-chain PL can only cover goals (emulate-anything) and (production-readiness). -As far as we aware, none of them are trying +As far as we are aware, none of them are trying to solve other goals. Known examples of PLs: @@ -431,20 +437,18 @@ Known examples of PLs: * [Aiken](https://aiken-lang.org/) - on-chain PL with IDE support and testing framework * [Helios](https://www.hyperion-bt.org/helios-book/api/index.html) - - on-chain PL and frontend Tx sending library + - on-chain PL and frontend transaction sending library * [OpShin](https://github.com/OpShin/opshin) - on-chain PL * [Purus](https://github.com/mlabs-haskell/purus) - on-chain PL based on PureScript compiler (WIP by MLabs) -The same stands for any known kind of frontend frameworks: +The same stands for any known kind of frontend frameworks +and any kind of translations of `cardano-api` to other PLs:: * [CTL](https://github.com/Plutonomicon/cardano-transaction-lib) * [lucid-evolution](https://github.com/Anastasia-Labs/lucid-evolution) * [meshjs.dev](https://meshjs.dev/) - -Same stands for any kind of `cardano-api` API translation to other PLs: - * [Transaction Village](https://github.com/mlabs-haskell/tx-village) * [PyCardano](https://pycardano.readthedocs.io/en/latest/guides/plutus.html) * [Cardano Multiplatform Lib](https://github.com/dcSpark/cardano-multiplatform-lib) @@ -457,7 +461,7 @@ Same stands for any kind of `cardano-api` API translation to other PLs: * on-chain code * off-chain tx construction * indexing backend -* Constraints determine input and outputs up to UTxO coin-selection (we call it almost-determinacy) +* Constraints determine input and outputs up to UTxO coin selection (we call it "almost-determinacy") * Datum properties encoded as type classes * Common on-chain optimizations are performed if possible * Constraints normalization @@ -479,9 +483,9 @@ The definition of the property we aim to check is simple and completely generic: > Given a transaction with some UTxO context, and a function -> that generates SomeMutation from a valid transaction and -> context pair, this property checks applying any generated -> mutation makes the transaction invaild. +that generates some mutation from a valid transaction and +the context, this property checks that applying a +mutation makes the transaction invalid. -We are using `quickcheck-dynamic`library to run model-based -testing and mutation-based testing. \ No newline at end of file +We are using `quickcheck-dynamic` library to run model-based +testing and mutation-based testing. From a509e2b5f5d3c75b3a1172d2e9d0f0bcd576711e Mon Sep 17 00:00:00 2001 From: euonymos Date: Tue, 21 Jan 2025 15:13:37 -0600 Subject: [PATCH 06/15] chore: how to generate diagrams --- .ghci | 1 - docs/getting-started.md | 27 +++++++++++++++++++-------- src/Cardano/CEM.hs | 1 + 3 files changed, 20 insertions(+), 9 deletions(-) diff --git a/.ghci b/.ghci index e34911c..6636221 100644 --- a/.ghci +++ b/.ghci @@ -1,2 +1 @@ :set -Wunused-binds -Wunused-imports -Worphans -:set -isrc -itest diff --git a/docs/getting-started.md b/docs/getting-started.md index af9d848..34822b0 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -106,7 +106,7 @@ See the reference section for a full reference of `TxConstraint`. - `script` is a phantom type parameter, just like in `TxConstraint`. - `value` is the type of what this expression will resolve during runtime. -`ConstraintDSL` allows us to reference parts of the state machine's parameters, +`ConstraintDSL` allows us to reference parts of the state machine's parameters, the current state, the transition arguments, and so forth. It also lets us perform checks (like equality) and apply transformations (like lifting a Plutarch function). @@ -452,14 +452,14 @@ The following are lifted versions of Plutarch operators #### Setup: The Types -First, we define a type to denote our script. It’s an uninhabited type, it can’t be constructed. +First, we define a type to denote our script. It’s an uninhabited type, it can’t be constructed. It’s only used as a tag for connecting all instances of type classes together. ```haskell data SimpleAuction ``` -We define a type for the read-only state of our script. This state can’t be modified once created. +We define a type for the read-only state of our script. This state can’t be modified once created. This becomes the `Params` associated type of the `CEMScript` type class. ```haskell @@ -507,8 +507,8 @@ data SimpleAuctionTransition ``` We can now define an instance of the `CEMScriptTypes` for `SimpleAuction`. -`CEMScriptTypes` is a superclass of `CEMScript`, which just includes the associated types. -By defining the associated types separately, we can use the `deriveCEMAssociatedTypes` +`CEMScriptTypes` is a superclass of `CEMScript`, which just includes the associated types. +By defining the associated types separately, we can use the `deriveCEMAssociatedTypes` Template Haskell function to generate some boilerplate. ```haskell @@ -520,8 +520,8 @@ instance CEMScriptTypes SimpleAuction where $(deriveCEMAssociatedTypes False ''SimpleAuction) ``` -`deriveCEMAssociatedTypes` just executes `derivePlutusSpine` for all three of the associated types. -But it can only do that if all the members of a type have a `HasPlutusSpine` implementation. +`deriveCEMAssociatedTypes` just executes `derivePlutusSpine` for all three of the associated types. +But it can only do that if all the members of a type have a `HasPlutusSpine` implementation. This is why we need to do `derivePlutusSpine` for the `Bid` type ourselves. The boolean argument to `deriveCEMAssociatedTypes` is unused for now, and it is recommended to use a value of `False`. @@ -534,7 +534,7 @@ To implement the logic of our script, we define an instance of `CEMScript` for o instance CEMScript SimpleAuction where ``` -We provide a value for `compilationConfig`, which at the moment contains +We provide a value for `compilationConfig`, which at the moment contains only a prefix for error codes to tell errors from different programs apart. ```haskell @@ -661,3 +661,14 @@ Let’s examine each of the entries in the map in detail. ] ) ``` + +### Generating state diagram + +Use `genCemGraph` function from `Cardano.CEM.Documentation` module +to produce `graphviz` definition: + +```bash +$ cabal repl cem-script-example +ghci> :m +System.IO Cardano.CEM CEM.Example.Auction Data.Proxy +ghci> withFile "auction_diagram.dot" WriteMode (\h -> hPutStrLn h (genCemGraph "CEM Simple Acutoin" (Proxy :: Proxy SimpleAuction))) +``` diff --git a/src/Cardano/CEM.hs b/src/Cardano/CEM.hs index 08cbce8..86e83d4 100644 --- a/src/Cardano/CEM.hs +++ b/src/Cardano/CEM.hs @@ -8,6 +8,7 @@ import Cardano.CEM.Address as X ( cemScriptPlutusCredential, ) import Cardano.CEM.Compile as X +import Cardano.CEM.Documentation as X (genCemGraph) import Cardano.CEM.DSL as X ( CEMScript (..), CEMScriptDatum, From 64b662d8db94c67307377e26931e2eafb2122f24 Mon Sep 17 00:00:00 2001 From: euonymos Date: Tue, 21 Jan 2025 15:45:08 -0600 Subject: [PATCH 07/15] chore: update README --- README.md | 59 +++++-------------- docs/catalyst_milestone_reports.md | 5 +- ...{getting-started.md => getting_started.md} | 0 docs/goals_and_design.md | 14 ++--- 4 files changed, 26 insertions(+), 52 deletions(-) rename docs/{getting-started.md => getting_started.md} (100%) diff --git a/README.md b/README.md index b8b32c2..124882d 100644 --- a/README.md +++ b/README.md @@ -1,59 +1,32 @@ -# CEM SDK +# CEM Script ## Project pitch -Define and reuse Cardano DApp logic via annotated CEM-machines, resulting in free implementations for: +CEM Script is a framework to define Cardano DApp logic via annotated CEM-machines, +resulting in free implementations for: * On-chain scripts -* Tx building/submission/resubmission on L1/emulated testnet -* Tx parsing/indexing +* Transaction building/submission (off-chain) +* Transaction parsing/indexing * Automatically testing invariants * Human-readable specs -## Building +## Documentation + +* [Getting Started Guide](https://github.com/mlabs-haskell/cem-script/blob/master/docs/getting_started.md) +* [Goals and Design](https://github.com/mlabs-haskell/cem-script/blob/master/docs/goals_and_design.md) +* Article on [testing with CLB](TODO: link) is another introduction to testing CEM Script dApps. -Building is performed with cabal. -Building requires `libblst` and `libsodium` installed. +## Building -Arch Linux has `libblst` in AUR, nix are exemplified by IOHK, -and manual installation is described here: -https://github.com/input-output-hk/cardano-node-wiki/blob/main/docs/getting-started/install.md#installing-blst +Building is performed with `cabal`inside IOG's `github:input-output-hk/devx` shell. +See `.envrc` for details. Make sure to `cabal update` before building. -The project uses `github:input-output-hk/devx` to make the development shell. See `.envrc` for details. - ## Running tests -Tests are runned in emulated environment by default. - -Just run: `cabal test`. - -For development and fast response once could consider `ghcid`. - -## Starting local devnet - -Tests depend on localdevnet, which is runned in Docker. -To start it do: - -```bash -./prepare-devnet.sh -docker-compose -f docker-compose.devnet.yaml up -sudo chown -R $USER:$USER ./devnet/ -``` - -## Devnet stalling bug - -Sometimes devnet stalls, due to some bug, in that case one should restart it, -and wipe directory `./devnet/db`. To look for stalling one could check: -`CARDANO_NODE_SOCKET_PATH=./devnet/node.socket cardano-cli query tip --testnet-magic 42`. For properly working devnet slots should change -and sync be marked as 100%. - -On this bug: -https://forum.cardano.org/t/restarting-custom-private-networks-cardano-node-forge35/116921 - -## Project status +Tests are runned in emulated environment using +[CLB](https://github.com/mlabs-haskell/clb). -Project is in early development stage and is funded by -[Catalyst proposal](https://projectcatalyst.io/funds/10/f10-development-and-infrastructure/mlabs-cemscript-sdk-get-your-dapp-implementation-from-annotated-on-chain-logic-state-machine). -Detailed milestones of proposal and their status [are available](https://milestones.projectcatalyst.io/projects/1000118) as well. +Just run: `cabal run cem-script-test`. \ No newline at end of file diff --git a/docs/catalyst_milestone_reports.md b/docs/catalyst_milestone_reports.md index 30affcb..5cfec43 100644 --- a/docs/catalyst_milestone_reports.md +++ b/docs/catalyst_milestone_reports.md @@ -10,10 +10,11 @@ * Final code clean-up: * [PR#113 - finalize mutation tests](https://github.com/mlabs-haskell/cem-script/pull/113) * [PR#109 - cosmetic changes](https://github.com/mlabs-haskell/cem-script/pull/109) -* Final tutorial and docs +* Final tutorial and docs: * [PR on docs](https://github.com/mlabs-haskell/cem-script/pull/115) * [Getting Started Guide](https://github.com/mlabs-haskell/cem-script/pull/115/files#diff-31bcba2ccafa41d46fbbd6d1219f7f1e3b1fb3cad9faa8e4dc521bbb579dd7b3) - * Updated [Goals And Design](TODO: link) + * Updated [Goals And Design](https://github.com/mlabs-haskell/cem-script/pull/115/files#diff-ef1a1e144302d41f2687f34dc1885cd8434e6395aa5443c81a2bca8414911972) +* [Closeout video](TODO: link) ## Clarifications on M3 Deliverables diff --git a/docs/getting-started.md b/docs/getting_started.md similarity index 100% rename from docs/getting-started.md rename to docs/getting_started.md diff --git a/docs/goals_and_design.md b/docs/goals_and_design.md index 5759b7f..2c913e3 100644 --- a/docs/goals_and_design.md +++ b/docs/goals_and_design.md @@ -13,7 +13,7 @@ and demonstrate them by listing specific problems that arouse in the existing dApps codebase. Such problems are specific security vulnerabilities of different -types. They are still common in development which increases +types. They are still common in development which increases audit and support costs. Also, this document describes how existing solutions @@ -183,7 +183,7 @@ At least three errors of this kind are known in Cardano/Plutus interval logic, showing that it is not easy to do. Another problem is keeping time logic in sync between on- -and off-chain code. This is even harder given that Plutus' +and off-chain code. This is even harder given that Plutus' time-to-slot conversion gets in the way. Slot time differences and overall need to make test cases match real blockchain behavior may lead to flaky test behavior. @@ -192,7 +192,7 @@ Our script stages abstraction cover all those kinds of problems. ### Matching to off-chain logic -The problem of duplicating logic between on-chain and off-chain +The problem of duplicating logic between on-chain and off-chain is twofold. Testing is essentially done off-chain, thus, one may easily miss that your on-chain code is not actually enforcing some parts of @@ -256,7 +256,7 @@ for possible utxo changes. Our project encodes scripts in the form of a deterministic machine, which contains enough information to construct transactions automatically. -This also gives a way to check for potential on-chain +This also gives a way to check for potential on-chain vs off-chain logic differences semi-automatically. Examples: @@ -371,14 +371,14 @@ but only partially covers While it, surely, can do transaction emulation, it, to the best of our knowledge, does not have a monad instance for real L1 blockchain. So one still cannot reuse the same code -across tests and real blockchain Tx construction. +across tests and real blockchain transaction construction. `TxSkel` datatype is similar to the design we are implementing, and other parts of API have a lot of cool DX decisions. But `cooked-validators` lack script transition model, so it cannot provide declarative transaction submission error handling we aim to get because it does not have information to decide -whether a specific Tx input is critical (like an auth token), +whether a specific transaction input is critical (like an auth token), or can be re-selected again (like coin-selected ADA for payment). Having a declarative transition model is even @@ -394,7 +394,7 @@ to attack vectors missed by accident. Our API presumes that means of on-chain validation, in our case behavior equivalence (AKA bi-similarity) -of a declarative CEM state machine and a real on-chain +of a declarative CEM state machine and a real on-chain script is verified and validated semi-automatically. Also, we plan to make some kind of the vulnerabilities covered by `cooked-validators` impossible by construction, From d38fdb5e74b49c9bcc5b38658abcf39c769bfb8d Mon Sep 17 00:00:00 2001 From: euonymos Date: Tue, 21 Jan 2025 15:48:29 -0600 Subject: [PATCH 08/15] chore: remove private testnet --- devnet/byron-delegate.key | Bin 130 -> 0 bytes devnet/byron-delegation.cert | 8 - devnet/cardano-node.json | 80 ------- devnet/credentials/alice.sk | 5 - devnet/credentials/alice.vk | 5 - devnet/credentials/bob.sk | 5 - devnet/credentials/bob.vk | 5 - devnet/credentials/carol.sk | 5 - devnet/credentials/carol.vk | 5 - devnet/credentials/dave.sk | 5 - devnet/credentials/dave.vk | 5 - devnet/credentials/eve.sk | 5 - devnet/credentials/eve.vk | 5 - devnet/credentials/faucet.sk | 5 - devnet/credentials/faucet.vk | 5 - devnet/credentials/frank.sk | 5 - devnet/credentials/frank.vk | 5 - devnet/credentials/grace.sk | 5 - devnet/credentials/grace.vk | 5 - devnet/credentials/hans.sk | 5 - devnet/credentials/hans.vk | 5 - devnet/credentials/oscar.sk | 5 - devnet/credentials/oscar.vk | 5 - devnet/credentials/patricia.sk | 5 - devnet/credentials/patricia.vk | 5 - devnet/credentials/rupert.sk | 5 - devnet/credentials/rupert.vk | 5 - devnet/genesis-alonzo.json | 365 -------------------------------- devnet/genesis-conway.json | 38 ---- devnet/kes.skey | 5 - devnet/opcert.cert | 5 - devnet/protocol-parameters.json | 1 - devnet/topology.json | 1 - devnet/vrf.skey | 5 - docker-compose.devnet.yaml | 20 -- prepare-devnet.sh | 4 - 36 files changed, 652 deletions(-) delete mode 100755 devnet/byron-delegate.key delete mode 100755 devnet/byron-delegation.cert delete mode 100755 devnet/cardano-node.json delete mode 100755 devnet/credentials/alice.sk delete mode 100755 devnet/credentials/alice.vk delete mode 100755 devnet/credentials/bob.sk delete mode 100755 devnet/credentials/bob.vk delete mode 100755 devnet/credentials/carol.sk delete mode 100755 devnet/credentials/carol.vk delete mode 100755 devnet/credentials/dave.sk delete mode 100755 devnet/credentials/dave.vk delete mode 100755 devnet/credentials/eve.sk delete mode 100755 devnet/credentials/eve.vk delete mode 100755 devnet/credentials/faucet.sk delete mode 100755 devnet/credentials/faucet.vk delete mode 100755 devnet/credentials/frank.sk delete mode 100755 devnet/credentials/frank.vk delete mode 100755 devnet/credentials/grace.sk delete mode 100755 devnet/credentials/grace.vk delete mode 100755 devnet/credentials/hans.sk delete mode 100755 devnet/credentials/hans.vk delete mode 100755 devnet/credentials/oscar.sk delete mode 100755 devnet/credentials/oscar.vk delete mode 100755 devnet/credentials/patricia.sk delete mode 100755 devnet/credentials/patricia.vk delete mode 100755 devnet/credentials/rupert.sk delete mode 100755 devnet/credentials/rupert.vk delete mode 100755 devnet/genesis-alonzo.json delete mode 100755 devnet/genesis-conway.json delete mode 100755 devnet/kes.skey delete mode 100755 devnet/opcert.cert delete mode 100755 devnet/protocol-parameters.json delete mode 100755 devnet/topology.json delete mode 100755 devnet/vrf.skey delete mode 100644 docker-compose.devnet.yaml delete mode 100755 prepare-devnet.sh diff --git a/devnet/byron-delegate.key b/devnet/byron-delegate.key deleted file mode 100755 index 6693ec7706777aa4da360aeb4ef9a8dd56d923b1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 130 zcmV-|0Db>hfJhJpMAL|soH`HS$J85Ti_uO*&)dR|kV1;ij>55VRpM>_gJ@~-Ve=4b z6*4KMp|mD#my~k2q4Pg0GS#Vq%-e^fM6aX>J2iuc_dUuT6h#GA14UZb=DL9`RR{e1 kh_;Vv?p$}9CT3Yaye$FN$zuTGNK5P Date: Wed, 22 Jan 2025 16:31:34 -0600 Subject: [PATCH 09/15] chore: comments in the code, reformat --- docs/getting_started.md | 5 ++--- example/CEM/Example/Auction.hs | 24 ++++++++++++------------ src/Cardano/CEM.hs | 2 +- src/Cardano/CEM/DSL.hs | 12 +++++++----- src/Cardano/CEM/OffChain.hs | 21 +++++++++++---------- src/Cardano/CEM/Smart.hs | 2 +- 6 files changed, 34 insertions(+), 32 deletions(-) diff --git a/docs/getting_started.md b/docs/getting_started.md index 34822b0..80f7cbf 100644 --- a/docs/getting_started.md +++ b/docs/getting_started.md @@ -175,8 +175,7 @@ data ResolvedTx = MkResolvedTx , toMint :: TxMintValue BuildTx Era , interval :: Interval POSIXTime , additionalSigners :: [PubKeyHash] - , -- FIXME - signer :: ~(SigningKey PaymentKey) + , signer :: ~(SigningKey PaymentKey) } deriving stock (Show, Eq) @@ -302,7 +301,7 @@ data TxConstraint (resolved :: Bool) script -- | Value being matched by its Spine (DSLPattern resolved script sop) -- | Case switch - -- FIXME: might use function instead, will bring `_` syntax, + -- TODO: might use function instead, will bring `_` syntax, -- reusing matched var and probably implicitly type-checking spine -- by saving it to such var DSL value (Map.Map (Spine sop) (TxConstraint resolved script)) diff --git a/example/CEM/Example/Auction.hs b/example/CEM/Example/Auction.hs index 7118506..5404060 100644 --- a/example/CEM/Example/Auction.hs +++ b/example/CEM/Example/Auction.hs @@ -16,8 +16,8 @@ data SimpleAuction -- | A bid data Bid = MkBet - { bidder :: PubKeyHash -- FIXME: rename to bidder - , bidAmount :: Integer -- FIXME: rename to bidder + { bidder :: PubKeyHash + , bidAmount :: Integer } deriving stock (Prelude.Eq, Prelude.Show) @@ -128,14 +128,14 @@ instance CEMScript SimpleAuction where , byFlagError (lift False) "Another err" , -- Example: In constraints redundant for on-chain offchainOnly - (if' - (ctxParams.seller `eq'` buyoutBid.bidder) - (signedBy ctxParams.seller) - (spentBy - buyoutBid.bidder - (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) - cEmptyValue - ) + ( if' + (ctxParams.seller `eq'` buyoutBid.bidder) + (signedBy ctxParams.seller) + ( spentBy + buyoutBid.bidder + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) + cEmptyValue + ) ) , output (userUtxo buyoutBid.bidder) -- NOTE: initial zero bidder is seller @@ -144,8 +144,8 @@ instance CEMScript SimpleAuction where (ctxParams.seller `eq'` buyoutBid.bidder) noop ( output - (userUtxo ctxParams.seller) - (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) + (userUtxo ctxParams.seller) + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) ) ] ) diff --git a/src/Cardano/CEM.hs b/src/Cardano/CEM.hs index 86e83d4..93f3549 100644 --- a/src/Cardano/CEM.hs +++ b/src/Cardano/CEM.hs @@ -8,7 +8,6 @@ import Cardano.CEM.Address as X ( cemScriptPlutusCredential, ) import Cardano.CEM.Compile as X -import Cardano.CEM.Documentation as X (genCemGraph) import Cardano.CEM.DSL as X ( CEMScript (..), CEMScriptDatum, @@ -17,6 +16,7 @@ import Cardano.CEM.DSL as X ( RecordSetter ((::=)), TxConstraint, ) +import Cardano.CEM.Documentation as X (genCemGraph) import Cardano.CEM.Monads as X import Cardano.CEM.Monads.CLB as X import Cardano.CEM.OffChain as X diff --git a/src/Cardano/CEM/DSL.hs b/src/Cardano/CEM/DSL.hs index 4c074aa..0839713 100644 --- a/src/Cardano/CEM/DSL.hs +++ b/src/Cardano/CEM/DSL.hs @@ -122,7 +122,7 @@ data ConstraintDSL script value where Proxy label -> ConstraintDSL script value -- | Builds a datatype value from the spine and field setters. - -- Used in Utxo Out spec. + -- Used in Utxo Out spec. Only specified fields are compared. UnsafeOfSpine :: forall script datatype spine. ( spine ~ Spine datatype @@ -173,7 +173,7 @@ instance Show (ConstraintDSL x y) where (GetField valueDsl proxyLabel) -> show valueDsl <> "." <> symbolVal proxyLabel Eq x y -> show x <> " @== " <> show y - -- FIXME: add user annotations + -- TODO: add user annotations LiftPlutarch _ x -> "somePlutarchCode (" <> show x <> ")" LiftPlutarch2 _ x y -> "somePlutarchCode (" <> show x <> ") (" <> show y <> ")" @@ -346,9 +346,10 @@ class -- | The crux part - a map that defines constraints for each transition via DSL. transitionSpec :: CEMScriptSpec False script - -- | Optional Plutus script to calculate things, which can be used in the cases - -- when CEM constraints and/or inlining Plutarch functions are not expressible - -- enough. + -- | Optional Plutus script to calculate a value of type + -- (TransitionComp script), which can be used in the cases + -- when CEM constraints and/or inlining Plutarch functions + -- are not expressive enough. transitionComp :: Maybe ( Params script -> @@ -385,6 +386,7 @@ class CEMScriptTypes script where -- | See 'transitionComp' type TransitionComp script + -- | By default it's not set. type TransitionComp script = Void -- | Options used for compiling. diff --git a/src/Cardano/CEM/OffChain.hs b/src/Cardano/CEM/OffChain.hs index c3b9b16..2db2966 100644 --- a/src/Cardano/CEM/OffChain.hs +++ b/src/Cardano/CEM/OffChain.hs @@ -118,7 +118,6 @@ queryScriptState params = do mTxInOut <- queryScriptTxInOut params return (cemTxOutState . snd =<< mTxInOut) --- FIXME: doc, naming data OffchainTxIR = TxInR (TxIn, TxInWitness) | TxInRefR (TxIn, TxInWitness) @@ -171,15 +170,16 @@ compileActionConstraints throwError CEMScriptTxInResolutionError let - -- FIXME: fromJust laziness trick + -- TODO: fromJust laziness trick datum = (params, fromJust mState) compiled' = map (compileConstraint datum transition) uncompiled - -- FIXME: raise lefts from compiled + -- NB: raise lefts from compiled let f x = case x of Left message -> throwError $ PerTransitionErrors [CompilationError message] Right x' -> return x' - -- FIXME: add resolution logging + + -- TODO: add resolution logging mapM f compiled' process :: @@ -194,7 +194,7 @@ process (MkCEMAction params transition) ec = case ec of utxo <- lift $ queryUtxo $ ByAddresses [pubKeyHashAddress $ user c] let utxoPairs = map (withKeyWitness . fst) $ Map.toList $ unUTxO utxo - -- FIXME: do actuall coin selection + -- TODO: do actuall coin selection return $ TxInR $ head utxoPairs c@(Utxo kind fanFilter value) -> do case kind of @@ -213,7 +213,7 @@ process (MkCEMAction params transition) ec = case ec of map (addWittness . fst) $ filter predicate utxoPairs case matchingUtxos of x : _ -> return $ case someIn of - -- FIXME: log/fail on >1 options to choose for script + -- TODO: log/fail on >1 options to choose for script In -> TxInR x InRef -> TxInRefR x [] -> @@ -222,7 +222,7 @@ process (MkCEMAction params transition) ec = case ec of predicate (_, txOut) = txOutValue txOut == fromPlutusValue value && case fanFilter of - -- FIXME: refactor DRY + -- TODO: refactor DRY SameScript (MkSameScriptArg state) -> cemTxOutDatum txOut == Just @@ -240,9 +240,10 @@ process (MkCEMAction params transition) ec = case ec of , state ) ) - -- FIXME: understand what is happening + convertTxOut x = TxOutValueShelleyBased shelleyBasedEra $ toMaryValue x + addWittness = case fanFilter of UserAddress {} -> withKeyWitness SameScript {} -> (,scriptWitness) @@ -315,7 +316,7 @@ awaitTx txId = do go 5 where go :: Integer -> m () - go 0 = liftIO $ fail "Tx was not awaited." -- FIXME: + go 0 = liftIO $ fail "Tx was not awaited." go n = do exists <- checkTxIdExists liftIO $ threadDelay 1_000_000 @@ -404,7 +405,7 @@ compileDsl datum@(params, state) transition dsl = case dsl of UnsafeUpdateOfSpine valueDsl _spine setters -> do case setters of [] -> recur valueDsl - _ -> error "FIXME: not implemented" + _ -> error "Not implemented yet." LiftPlutarch pterm argDsl -> do arg <- recur argDsl case evalTerm NoTracing $ pterm # pconstant arg of diff --git a/src/Cardano/CEM/Smart.hs b/src/Cardano/CEM/Smart.hs index 7ad1f0b..3170a48 100644 --- a/src/Cardano/CEM/Smart.hs +++ b/src/Cardano/CEM/Smart.hs @@ -68,7 +68,7 @@ cOfSpine :: Spine datatype -> [RecordSetter (ConstraintDSL script) datatype] -> ConstraintDSL script datatype --- FIXME: should it be ordered? +-- TODO: should it be ordered? cOfSpine spine setters = if toInteger (length setters) == toInteger (spineFieldsNum spine) then UnsafeOfSpine spine setters From 06a7d2f9b6e6bf4e39923bfbfad321d59096c571 Mon Sep 17 00:00:00 2001 From: euonymos Date: Wed, 22 Jan 2025 16:31:43 -0600 Subject: [PATCH 10/15] chore: revise onchain module --- src/Cardano/CEM/OnChain.hs | 344 ++++++++++++++++++++----------------- 1 file changed, 185 insertions(+), 159 deletions(-) diff --git a/src/Cardano/CEM/OnChain.hs b/src/Cardano/CEM/OnChain.hs index aaf5350..3f9a1f0 100644 --- a/src/Cardano/CEM/OnChain.hs +++ b/src/Cardano/CEM/OnChain.hs @@ -124,16 +124,15 @@ import PlutusTx qualified import Text.Show.Pretty (ppShow) import Prelude --- Interfaces - +-- | Interface of a compiled CEM Script. class (CEMScript script) => CEMScriptCompiled script where -- | Code, original error message - -- FIXME: track transition it might be raised + -- TODO: track transitions along with the errors errorCodes :: Proxy script -> [(String, String)] cemScriptCompiled :: Proxy script -> Script --- Compilation +-- | On-chain compilation logic. genericPlutarchScript :: forall script. (CEMScript script) => @@ -153,6 +152,10 @@ genericPlutarchScript spec code = ctx <- pletFields @'["txInfo"] ctx' ownAddress <- plet $ getOwnAddress # ctx' spineIndex <- plet $ pfstBuiltin # (pasConstr # redm) + -- We _always_ delay `comp` and force it _only_ when a user asks for + -- its result and this is the moment when Nothing should error. + -- TODO: Can we prevent user from calling `askC @CComp` if + -- 'transitionComp' is not set? comp <- plet $ pdelay $ case code of Just x -> let @@ -160,142 +163,163 @@ genericPlutarchScript spec code = script = foreignImport x in script # params # state # redm - Nothing -> ptraceInfo "Unreachable" perror - perSpineChecks ctx.txInfo ownAddress comp spineIndex + Nothing -> ptraceInfo "transitionComp is nothing" perror + -- Builds checks for transition (its spine) + let checks = perTransitionCheck ctx.txInfo ownAddress comp + -- Checks for transition spine from redeemer + compileSpineCaseSwitch spineIndex checks where - params = datumTupleOf 0 - state = datumTupleOf 1 - datumTupleOf ix = getRecordField ix datum - getRecordField ix d = ptryIndex ix $ psndBuiltin # (pasConstr # d) - perSpineChecks txInfo ownAddress comp spineIndex = - compileSpineCaseSwitch spineIndex f - where - f = perTransitionCheck txInfo ownAddress redm comp - perTransitionCheck txInfo ownAddress transition comp transitionSpine = P.do + -- We are done + + -- Builds 'Spine (Transition script) -> Term s PUnit' + perTransitionCheck txInfo ownAddress comp transitionSpine = P.do ptraceDebug (pconstant $ fromString $ "Checking transition " <> Prelude.show transitionSpine) - constraintChecks + perTransitionCheck' where - -- FIXME: fold better - constraintChecks = P.do + perTransitionCheck' = P.do pif - (foldr ((\x y -> pand' # x # y) . compileConstr) (pconstant True) constrs) + -- Constraints + ( foldr + ((\x y -> pand' # x # y) . compileConstr) + (pconstant True) + constrs + ) + -- Common checks (commonChecks # pfromData txInfo) + -- Fail (ptraceInfoError "Constraint check failed") + + -- Get constraints from the definition + constrs = case Map.lookup transitionSpine spec of + Just x -> x + Nothing -> + error $ + "Compilation error: transition: " + <> (Prelude.show transitionSpine) + <> " lacks spec" + + -- Actual constraint compilation compileConstr :: TxConstraint False script -> Term s PBool - compileConstr c = - ptraceInfoIfFalse - ( pconstant $ fromString $ "Checking constraint " <> Prelude.show c - ) - $ case c of - MainSignerCoinSelect pkhDsl inValueDsl outValueDsl -> - P.do - -- FIXME: check final difference - -- FIXME: DRY with TxSpec implemenation - let - txIns = resolve #$ pfromData $ pfield @"inputs" # txInfo - txOuts = pfromData $ pfield @"outputs" # txInfo - punsafeCoerce (compileDsl inValueDsl) - #<= (txFansValue txIns) - #&& (punsafeCoerce (compileDsl outValueDsl) #<= (txFansValue txOuts)) - where - merge :: - Term - s - ( PValue Unsorted NonZero - :--> ( (PValue Sorted NonZero) - :--> PValue Sorted NonZero - ) - ) - merge = plam $ \x y -> ((passertSorted # x) <> y) - mapGetValues :: - Term - s - (PBuiltinList PTxOut :--> PBuiltinList (PValue Unsorted NonZero)) - mapGetValues = - pmap - # plam (\x -> pforgetSorted $ pforgetPositive $ pfromData $ pfield @"value" # x) - resolve = - pmap # plam (\x -> pfromData $ pfield @"resolved" # x) - predicate :: Term s (PTxOut :--> PBool) - predicate = plam $ \txOut -> - (ppkhAddress #$ punsafeCoerce $ compileDsl pkhDsl) - #== pfromData (pfield @"address" # txOut) - txFansValue txIns = - let validTxIns = pfilter # predicate # txIns - in pfoldr - # merge - # (passertSorted #$ pMkAdaOnlyValue # 0) - #$ mapGetValues - # validTxIns - Utxo fanKind fanSpec value -> - let - resolve = - pmap # plam (\x -> pfromData $ pfield @"resolved" # x) - fanList :: Term s (PBuiltinList PTxOut) - fanList = case fanKind of - In -> - resolve #$ pfromData $ pfield @"inputs" # txInfo - InRef -> resolve #$ pfield @"referenceInputs" # txInfo - Out -> pfromData $ pfield @"outputs" # txInfo - predicate = plam $ \txOut -> case fanSpec of - UserAddress pkhDsl -> - let - correctAddress = - (ppkhAddress #$ punsafeCoerce $ compileDsl pkhDsl) - #== pfromData (pfield @"address" # txOut) - in - correctAddress - SameScript (MkSameScriptArg expectedState) -> - pmatch (pfromData (pfield @"datum" # txOut)) $ \case - POutputDatum datum' -> P.do - PDatum fanDatum <- - pmatch $ pfromData $ pfield @"outputDatum" # datum' - let - fanParams = getRecordField 0 fanDatum - fanState = getRecordField 1 fanDatum - ( (ownAddress #== pfield @"address" # txOut) - #&& ( (checkDsl expectedState fanState) - #&& fanParams - #== params - ) - ) - _ -> pconstant False - in - -- FIXME: do not use phead - checkDsl - value - (punsafeCoerce $ pfield @"value" #$ phead #$ pfilter # predicate # fanList) - MainSignerNoValue dsl -> + compileConstr c = ptraceInfoIfFalse + (pconstant $ fromString $ "Checking constraint " <> Prelude.show c) + $ case c of + -- + MainSignerCoinSelect pkhDsl inValueDsl outValueDsl -> + P.do let - signatories = pfromData $ pfield @"signatories" # txInfo - xSigner = punsafeCoerce $ pdata (compileDsl dsl) - in - ptraceInfoIfFalse (pshow xSigner) $ - ptraceInfoIfFalse (pshow signatories) $ - pelem # xSigner # signatories - Noop -> pconstant True - Error message -> ptraceInfoError $ pconstant message - If condDsl thenDsl elseDsl -> - pif - (pfromData $ punsafeCoerce $ compileDsl condDsl) - (compileConstr thenDsl) - (compileConstr elseDsl) - MatchBySpine valueDsl caseSwitch -> - let - value = punsafeCoerce $ compileDsl valueDsl - valueSpineNum = pfstBuiltin # (pasConstr # value) - in - compileSpineCaseSwitch - valueSpineNum - (compileConstr . (caseSwitch Map.!)) + txIns = resolve #$ pfromData $ pfield @"inputs" # txInfo + txOuts = pfromData $ pfield @"outputs" # txInfo + punsafeCoerce (compileDsl inValueDsl) + #<= (txFansValue txIns) + #&& (punsafeCoerce (compileDsl outValueDsl) #<= (txFansValue txOuts)) + where + merge :: + Term + s + ( PValue Unsorted NonZero + :--> ( (PValue Sorted NonZero) + :--> PValue Sorted NonZero + ) + ) + merge = plam $ \x y -> ((passertSorted # x) <> y) + mapGetValues :: + Term + s + (PBuiltinList PTxOut :--> PBuiltinList (PValue Unsorted NonZero)) + mapGetValues = + pmap + # plam (\x -> pforgetSorted $ pforgetPositive $ pfromData $ pfield @"value" # x) + resolve = + pmap # plam (\x -> pfromData $ pfield @"resolved" # x) + predicate :: Term s (PTxOut :--> PBool) + predicate = plam $ \txOut -> + (ppkhAddress #$ punsafeCoerce $ compileDsl pkhDsl) + #== pfromData (pfield @"address" # txOut) + txFansValue txIns = + let validTxIns = pfilter # predicate # txIns + in pfoldr + # merge + # (passertSorted #$ pMkAdaOnlyValue # 0) + #$ mapGetValues + # validTxIns + -- + Utxo fanKind fanSpec value -> + let + resolve = + pmap # plam (\x -> pfromData $ pfield @"resolved" # x) + fanList :: Term s (PBuiltinList PTxOut) + fanList = case fanKind of + In -> + resolve #$ pfromData $ pfield @"inputs" # txInfo + InRef -> resolve #$ pfield @"referenceInputs" # txInfo + Out -> pfromData $ pfield @"outputs" # txInfo + predicate = plam $ \txOut -> case fanSpec of + UserAddress pkhDsl -> + let + correctAddress = + (ppkhAddress #$ punsafeCoerce $ compileDsl pkhDsl) + #== pfromData (pfield @"address" # txOut) + in + correctAddress + SameScript (MkSameScriptArg expectedState) -> + pmatch (pfromData (pfield @"datum" # txOut)) $ \case + POutputDatum datum' -> P.do + PDatum fanDatum <- + pmatch $ pfromData $ pfield @"outputDatum" # datum' + let + fanParams = getRecordField 0 fanDatum + fanState = getRecordField 1 fanDatum + ( (ownAddress #== pfield @"address" # txOut) + #&& ( (checkDsl expectedState fanState) + #&& fanParams + #== params + ) + ) + _ -> pconstant False + in + checkDsl + value + (punsafeCoerce $ pfield @"value" #$ phead #$ pfilter # predicate # fanList) + -- + MainSignerNoValue dsl -> + let + signatories = pfromData $ pfield @"signatories" # txInfo + xSigner = punsafeCoerce $ pdata (compileDsl dsl) + in + ptraceInfoIfFalse (pshow xSigner) $ + ptraceInfoIfFalse (pshow signatories) $ + pelem # xSigner # signatories + -- + Noop -> pconstant True + -- + Error message -> ptraceInfoError $ pconstant message + -- + If condDsl thenDsl elseDsl -> + pif + (pfromData $ punsafeCoerce $ compileDsl condDsl) + (compileConstr thenDsl) + (compileConstr elseDsl) + -- + MatchBySpine valueDsl caseSwitch -> + let + value = punsafeCoerce $ compileDsl valueDsl + valueSpineNum = pfstBuiltin # (pasConstr # value) + in + compileSpineCaseSwitch + valueSpineNum + (compileConstr . (caseSwitch Map.!)) + + -- Compiles and check the value checkDsl :: ConstraintDSL script1 x -> Term s PData -> Term s PBool checkDsl expectationDsl value = case expectationDsl of + -- Trivial case Anything -> pconstant True + -- Special case - compares spine and all fields that defined by setters UnsafeOfSpine spine setters -> (pfstBuiltin #$ pasConstr # xValue) #== pconstant (Prelude.toInteger $ Prelude.fromEnum spine) @@ -307,24 +331,22 @@ genericPlutarchScript spec code = foldAnd (!x : xs) = x #&& (foldAnd xs) foldAnd [] = pconstant True in - foldAnd $ - map perIxCheck ixAndSetters + foldAnd $ map perIxCheck ixAndSetters + -- Standard case - evaluate and compare _ -> xValue #== value where xValue = compileDsl expectationDsl - -- FIXME: Some typing? `newtype MyPData x`? - -- ConstraintDSL script1 (PLifted x) -> Term s (AsData x) + + -- Compiles a DSL term into a value compileDsl :: forall script1 x. ConstraintDSL script1 x -> Term s PData compileDsl dsl = punsafeCoerce $ case dsl of Pure x -> pconstant $ PlutusTx.toData x - IsOnChain -> compileDsl $ Pure True - -- XXX: returns PBuiltinList PData in fact + IsOnChain -> compileDsl $ Pure True -- short-cut Ask @cvar @_ @dt Proxy -> case sing @cvar of SCParams -> params SCState -> state - SCTransition -> transition - -- FIXME: is this force good? + SCTransition -> redm SCComp -> pforce comp GetField @_ @y @_ @value valueDsl proxyLabel -> getRecordField @@ -339,7 +361,7 @@ genericPlutarchScript spec code = where pcons' x y = pcons # x # y fieldValue (_ ::= valueDsl) = compileDsl valueDsl - -- FIXME: Should we lift AsData functins? + -- TODO: Should we lift AsData functions? LiftPlutarch @_ @py plutrachFunc valueDsl -> let x = pfromDataImpl $ punsafeCoerce $ compileDsl valueDsl @@ -356,8 +378,7 @@ genericPlutarchScript spec code = Eq xDsl yDsl -> case (xDsl, yDsl) of (Anything, _) -> compileDsl $ Pure True (_, Anything) -> compileDsl $ Pure True - (_, _) -> - pdataImpl $ (compileDsl xDsl) #== (compileDsl yDsl) + (_, _) -> pdataImpl $ (compileDsl xDsl) #== (compileDsl yDsl) UnsafeUpdateOfSpine @_ @datatype notUpdatedValueDsl spine setters -> pmatch ( (pfstBuiltin #$ pasConstr # notUpdatedValue) @@ -373,8 +394,7 @@ genericPlutarchScript spec code = # pconstant (Prelude.toInteger $ Prelude.fromEnum spine) #$ foldr pcons' pnil $ map perIxValue [0 .. (toInteger (spineFieldsNum spine) - 1)] - -- FIXME: use error code - PFalse -> ptraceInfoError "Spines not matching" + PFalse -> ptraceInfoError "Spines do not match" where pcons' x y = pcons # x # y notUpdatedValue = compileDsl notUpdatedValueDsl @@ -389,30 +409,21 @@ genericPlutarchScript spec code = perIxValue ix = case updatedFields Map.!? ix of Just value -> value Nothing -> ptryIndex (fromInteger ix) notUpdatedFields - Anything -> nonDetMessage dsl - nonDetMessage dsl = - error $ - "Non-deterministic code in place it should not be " - <> " while compiling on-chain: \n" - <> ppShow dsl - constrs = case Map.lookup transitionSpine spec of - Just x -> x - Nothing -> error "Compilation error: some spine lacks spec" + Anything -> + error $ + "Non-deterministic code in place it should not be " + <> " while compiling on-chain: \n" + <> ppShow dsl -commonChecks :: Term s (PTxInfo :--> PUnit) -commonChecks = plam go - where - go :: Term s1 PTxInfo -> Term s1 PUnit - go txInfo = - pif - (stackingStuffDisabled txInfo) - (pconstant ()) - (ptraceInfo "Stacking feature used" perror) - stackingStuffDisabled :: Term s1 PTxInfo -> Term s1 PBool - stackingStuffDisabled txInfo = - (pnull # pfromData (pfield @"dcert" # txInfo)) - #&& (PMap.pnull #$ pfromData (pfield @"wdrl" # txInfo)) + -- Datum deconstruction + params = datumTupleOf 0 + state = datumTupleOf 1 + datumTupleOf ix = getRecordField ix datum + getRecordField ix d = ptryIndex ix $ psndBuiltin # (pasConstr # d) +{- | Tries all spines from 'Spine sop' and if it matches the index +calculates 'Term s x' by applying given `caseSwitchFunc' to the spine. +-} compileSpineCaseSwitch :: forall x sop s. (HasPlutusSpine sop) => @@ -436,3 +447,18 @@ compileSpineCaseSwitch spineIndex caseSwitchFunc = ) cont ) + +-- | Currently checks that staking features are not used. +commonChecks :: Term s (PTxInfo :--> PUnit) +commonChecks = plam go + where + go :: Term s1 PTxInfo -> Term s1 PUnit + go txInfo = + pif + (stakingStuffDetected txInfo) + (pconstant ()) + (ptraceInfo "Staking feature was used: currently not supported" perror) + stakingStuffDetected :: Term s1 PTxInfo -> Term s1 PBool + stakingStuffDetected txInfo = + (pnull # pfromData (pfield @"dcert" # txInfo)) + #&& (PMap.pnull #$ pfromData (pfield @"wdrl" # txInfo)) From d495eb14e72e090ea23277fd1aa4211af3375a5f Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 30 Jan 2025 10:17:13 -0600 Subject: [PATCH 11/15] chore: update article link --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 124882d..306b351 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ resulting in free implementations for: * [Getting Started Guide](https://github.com/mlabs-haskell/cem-script/blob/master/docs/getting_started.md) * [Goals and Design](https://github.com/mlabs-haskell/cem-script/blob/master/docs/goals_and_design.md) -* Article on [testing with CLB](TODO: link) is another introduction to testing CEM Script dApps. +* Article about [testing dApps on Cardano with CLB](https://www.mlabs.city/blog/testing-dapps-on-cardano-with-clb-emulator) is another introduction to testing CEM Script dApps. ## Building From ea46b36334227e4045fc0b09ab1046a6341c7167 Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 30 Jan 2025 10:18:10 -0600 Subject: [PATCH 12/15] chore: cosmetic changes --- example/CEM/Example/Auction.hs | 2 -- src/Cardano/CEM/OffChain.hs | 6 +++--- src/Cardano/CEM/OnChain.hs | 20 +++++++++----------- 3 files changed, 12 insertions(+), 16 deletions(-) diff --git a/example/CEM/Example/Auction.hs b/example/CEM/Example/Auction.hs index 5404060..c6ed059 100644 --- a/example/CEM/Example/Auction.hs +++ b/example/CEM/Example/Auction.hs @@ -124,8 +124,6 @@ instance CEMScript SimpleAuction where ( BuyoutSpine , [ input (ownUtxo $ inState WinnerSpine) auctionValue - , byFlagError (lift False) "Some err" - , byFlagError (lift False) "Another err" , -- Example: In constraints redundant for on-chain offchainOnly ( if' diff --git a/src/Cardano/CEM/OffChain.hs b/src/Cardano/CEM/OffChain.hs index 2db2966..c03c372 100644 --- a/src/Cardano/CEM/OffChain.hs +++ b/src/Cardano/CEM/OffChain.hs @@ -166,6 +166,7 @@ compileActionConstraints Map.! getSpine transition xSpine = transitionInStateSpine uncompiled + -- Check input state when (fmap getSpine mState /= xSpine) $ throwError CEMScriptTxInResolutionError @@ -286,8 +287,8 @@ resolveTx spec = runExceptT $ do SomeCEMAction -> (ExceptT TxResolutionError m) [OffchainTxIR] resolveSomeAction (MkSomeCEMAction @script action) = do let MkCEMAction params _ = action - mScript <- lift $ queryScriptState params - cs <- ExceptT $ return $ compileActionConstraints mScript action + mState <- lift $ queryScriptState params + cs <- ExceptT $ return $ compileActionConstraints mState action mapM (process action) cs resolveTxAndSubmitRet :: @@ -368,7 +369,6 @@ compileConstraint datum transition c = case c of UserAddress dsl -> UserAddress <$> compileDslRecur dsl SameScript (MkSameScriptArg stateDsl) -> SameScript . MkSameScriptArg <$> compileDslRecur stateDsl --- TODO: types errors compileDsl :: forall script x. (CEMScript script) => diff --git a/src/Cardano/CEM/OnChain.hs b/src/Cardano/CEM/OnChain.hs index 3f9a1f0..f932c1a 100644 --- a/src/Cardano/CEM/OnChain.hs +++ b/src/Cardano/CEM/OnChain.hs @@ -165,12 +165,11 @@ genericPlutarchScript spec code = script # params # state # redm Nothing -> ptraceInfo "transitionComp is nothing" perror -- Builds checks for transition (its spine) + -- checks :: Spine (Transition script) -> Term s PUnit let checks = perTransitionCheck ctx.txInfo ownAddress comp -- Checks for transition spine from redeemer compileSpineCaseSwitch spineIndex checks where - -- We are done - -- Builds 'Spine (Transition script) -> Term s PUnit' perTransitionCheck txInfo ownAddress comp transitionSpine = P.do ptraceDebug @@ -178,6 +177,14 @@ genericPlutarchScript spec code = perTransitionCheck' where perTransitionCheck' = P.do + -- Get constraints from the definition + let constrs = case Map.lookup transitionSpine spec of + Just x -> x + Nothing -> + error $ + "Compilation error: transition: " + <> (Prelude.show transitionSpine) + <> " lacks spec" pif -- Constraints ( foldr @@ -190,15 +197,6 @@ genericPlutarchScript spec code = -- Fail (ptraceInfoError "Constraint check failed") - -- Get constraints from the definition - constrs = case Map.lookup transitionSpine spec of - Just x -> x - Nothing -> - error $ - "Compilation error: transition: " - <> (Prelude.show transitionSpine) - <> " lacks spec" - -- Actual constraint compilation compileConstr :: TxConstraint False script -> Term s PBool compileConstr c = ptraceInfoIfFalse From b5d96e3e2b34dace0552f1ef6cc69ef125c670a4 Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 30 Jan 2025 10:26:00 -0600 Subject: [PATCH 13/15] chore: update milestone 5 report --- docs/catalyst_milestone_reports.md | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/docs/catalyst_milestone_reports.md b/docs/catalyst_milestone_reports.md index 5cfec43..a1e3fc3 100644 --- a/docs/catalyst_milestone_reports.md +++ b/docs/catalyst_milestone_reports.md @@ -1,6 +1,6 @@ # Milestone 5 -## Summary +## Summary of deliverables * L1 indexing: * [Basic indexing support PR #98](https://github.com/mlabs-haskell/cem-script/pull/98) @@ -14,21 +14,17 @@ * [PR on docs](https://github.com/mlabs-haskell/cem-script/pull/115) * [Getting Started Guide](https://github.com/mlabs-haskell/cem-script/pull/115/files#diff-31bcba2ccafa41d46fbbd6d1219f7f1e3b1fb3cad9faa8e4dc521bbb579dd7b3) * Updated [Goals And Design](https://github.com/mlabs-haskell/cem-script/pull/115/files#diff-ef1a1e144302d41f2687f34dc1885cd8434e6395aa5443c81a2bca8414911972) -* [Closeout video](TODO: link) - -## Clarifications on M3 Deliverables - -### Running an Emulated Environment by CLB - -The CLB monad is designed to interact seamlessly with a Cardano mockchain environment. It can read from a shared environment, query blockchain parameters such as the current slot, and retrieve UTXO information, among other functions. This module facilitates simulation and testing, making it essential for unit tests and other testing scenarios where a controlled blockchain environment is needed. Using this emulated environment, developers can test and validate their Cardano applications in a reliable and repeatable manner. - -### Running QuickCheck Dynamic Tests, Including Mutation Support +* [Closeout video](TODO:link) -QuickCheck is a powerful Haskell library for property-based testing, which helps ensure that programs behave correctly for a wide range of inputs. The quickcheck-dynamic library extends this tool to stateful systems, making it particularly suitable for testing blockchain applications. Our testing framework uses a state machine model to simulate real-world scenarios, incorporating support for mutation testing. This approach helps verify that the system maintains correct behavior under various conditions, including edge cases and unexpected changes, thereby enhancing the robustness of the application. +## Clarifications on M5 deliverables -### Rendering CEMScript State Graphs +in the final milestone we added support for indexing CEM Scripts based on +[Oura](https://github.com/txpipe/oura) utility. The framework provide utilities +to generate Oura's configs and parse transaction from Oura-based format into +CEM Script transitions. -Understanding state transitions and the overall system flow is critical for ensuring blockchain applications do not enter invalid states. To aid developers, we have implemented automated rendering of state graphs through our documentation module. This module generates DOT graph representations of CEMScript state transitions, providing an easy-to-understand visual model of how a DApp functions in real-world scenarios. This visualization tool increases developer confidence by highlighting the system's behavior and identifying potential shortcomings. +The documentation has been reworked. Getting started guide has beeen added. +An introductory video on CEM Script has been recorded and published on YouTube. # Milestone 4 From 7e55aefebd55b3a72e97a6cbcdc1ad2addc590d9 Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 30 Jan 2025 10:43:21 -0600 Subject: [PATCH 14/15] chore: comment out cabal-fmt check --- .github/workflows/haskell-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index dcb8bd6..1161c47 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -42,7 +42,7 @@ jobs: run: | cabal install --overwrite-policy=always cabal-fmt cabal install --overwrite-policy=always fourmolu - /home/runner/.cabal-devx/bin/cabal-fmt --check cem-script.cabal + # /home/runner/.cabal-devx/bin/cabal-fmt --check cem-script.cabal /home/runner/.cabal-devx/bin/fourmolu --mode check . - name: Cabal build and test shell: devx {0} From 9b6d8c8cf960543e8ae00221747fd02b649cbe2c Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 30 Jan 2025 10:48:29 -0600 Subject: [PATCH 15/15] chore: comment out fourmolu --- .github/workflows/haskell-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index 1161c47..21d32cc 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -43,7 +43,7 @@ jobs: cabal install --overwrite-policy=always cabal-fmt cabal install --overwrite-policy=always fourmolu # /home/runner/.cabal-devx/bin/cabal-fmt --check cem-script.cabal - /home/runner/.cabal-devx/bin/fourmolu --mode check . + # /home/runner/.cabal-devx/bin/fourmolu --mode check . - name: Cabal build and test shell: devx {0} run: |