diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md new file mode 100644 index 0000000000..4f9bd2ea3e --- /dev/null +++ b/CIP-XXXX/README.md @@ -0,0 +1,205 @@ +--- +CIP: 92 +Title: First-class errors in Plutus +Category: Plutus +Status: Proposed +Authors: + - Las Safin +Implementors: + - Las Safin +Discussions: + - https://github.com/cardano-foundation/cips/pulls/? +Created: 2023-03-01 +License: CC-BY-4.0 +--- + +## Abstract + +Plutus is a strictly evaluated language, where users heavily rely on **impure** errors +to cause transaction failure to rule out invalid cases. + +We propose three changes: +- Make `error` a first-class value you can pass around. Using it does not inherently + cause an error. +- Change condition for script success from not erring to returning `True`. +- Erase type abstractions and type applications entirely when going from + TPLC to UPLC rather than turning them into `delay` and `force`. + +UPLC is now **truly pure** wrt. transaction validation. +This enables another use-case: We can **optimise** it as if it +were entirely pure. We can turn `const () x` into `()` for any `x`! +We can turn `expensive1 || expensive2` into `if expensive1 then True else expensive2`, +and in general do any transformations that we'd do on a pure language without +regard for side-effects. + +Issues fixed / PRs closed by this CIP: +- https://github.com/input-output-hk/plutus/issues/4826 +- https://github.com/input-output-hk/plutus/issues/4114 +- https://github.com/input-output-hk/plutus/pull/4118 +- https://github.com/cardano-foundation/CIPs/pull/459 + +## Motivation + +Users write code in the style of `if cond then error else False`, which is unidiomatic and also problematic, +since the seemingly equivalent `cond && error` will **always err**. +This is not a good situation, and issues have been opened about it before, +notably https://github.com/input-output-hk/plutus/issues/4114 (over a year ago!). +The issue was righly not deemed a "vulnerability" or "bug", yet it is quite clearly a misfeature. + +The current design in fact **encourages impurity**, as the return value of scripts is ignored entirely; +only the effects matter. This is entirely antithetical to the design of Plutus. +With the changes in this CIP, users will naturally return `False` in cases that are +disallowed explicitly, `True` when it's allowed explicitly, and all other cases are +disallowed "implicitly" as they're also not `True`. + +There is also the issue of efficiency: `delay` and `force`s have added more of an +overhead than initially assumed, and a common trick used by alternative toolchains is to +avoid emitting these. PlutusTx still emits these as it targets PIR, the erasure of which into UPLC +adds this overhead. +However, removing this from the erasure itself doesn't just help PlutusTx get closer to the alternative +toolchains, but also means that all built-ins will no longer need to be forced before application. + +Making Plutus lazy would also solve the problems, yet this has not been done as a strict language +is easier to reason about wrt. budgetting. Instead, we turn to making errors first-class values. + +As noted in the abstract, we can now also do optimisations on the UPLC that were impossible +before, as the effects mattered. This notably meant we previously couldn't regard code which result +wasn't used as dead code. With this change, it's possible to entirely elide such (now) dead code. + +One minor effect of this CIP is that evaluation strategy is less important, meaning that you +could theoretically take a script in this new language and evaluate it lazily, without breaking +anything. + +## Specification + +The changes below would need to take effect in a new ledger era and Plutus version. +It is not yet clear which, as that depends on when it gets implemented. + +### Plutus Core + +To solve this problem at its root, this CIP proposes making errors **first-class values**. +Errors are no longer a special type of term that "infect" their environment, but can instead +be passed around freely. Using an error incorrectly is of course still an error, hence it still +bubbles up in that respect. + +We remove the following small-step reduction rule: +``` +f {(error)} -> (error) +``` +from [Plutus Core Specification](https://github.com/input-output-hk/plutus/blob/72d82f9d04cbef144727fad1f86ce43476e4cc63/doc/plutus-core-spec/untyped-reduction.tex#L133). + +#### Built-ins + +Errors passed to a built-in only cause an error if the built-in attempts +to inspect it, i.e. morally pattern-match on it in the Haskell definition. + +The matter of costing is a bit more complicated: +Arguments are still always in WHNF, and hence we still derive the cost from their +size. We can regard an error as a member of every type, and assign it a size in every type. +The size can be any constant, as it would be if it were explicitly added as a new +constructor to every built-in type. +If it is used, evaluation of the built-in halts immediately. +If it isn't used, it doesn't use any compute. +Whether it should take from the budget if not used is up to the implementors. + +### Ledger + +[`runPLCScript`](https://github.com/input-output-hk/cardano-ledger/blob/f58187e1f2ebb7bbd9f5c3072cab5b1b6568c93f/eras/alonzo/formal-spec/utxo.tex#L213) from the ledger will need a new version that checks +that the result is `True`, not that it didn't fail. This change can be done +transparently in the Plutus library by adding another version of evaluateScriptRestricting +with an equivalent type but for a new version of Plutus. + +## Rationale + +Plutus isn't made lazy by this change, errors are instead not immediately propagated up. +Errors are less special-cased now, as evident by the removal of a rule, not addition. + +One (somewhat obvious) issue is that `error` isn't the only source of divergence. +As @effectfully pointed out, the following is still problematic: +```haskell +let factorial n = ifThenElse (n == 0) 1 (factorial (n - 1)) +in factorial 2 +``` +The arguments to `ifThenElse` are evaluated first, leading to infinite recursion. +Fixing this would require making Plutus to some extent lazy, which is a much larger change. + +Is this change still worth it in light of this? +Even _purely_ for the sake of making scripts more functional, it would still be worth it. +Very few people will make their own `loopforever` function to replicate the old `error` to write impure scripts. +It is a bonus that we in addition 1) simplify the language 2) remove a foot-gun for new Plutusers/Plutors/Plutonites +3) make Plutus scripts more efficient by removing `delay` and `force` from the erasure. + +It is not immediately obvious that the third step is possible, as we still have the above issue. +The common example (from [Well-Typed](https://well-typed.com/blog/2022/08/plutus-cores/)) is: +```haskell +let* !boom = λ {a} -> ERROR + !id = λ {a} (x :: a) -> x +in λ (b :: Bool) -> ifThenElse {∀ a. a -> a} b boom id +``` +Indeed, this example works _without_ adding delays to type abstractions, +as the untyped form +```haskell +f = λ b -> ifThenElse b ERROR (λ x -> x) +``` +is precisely the example we seek to make work. +`f True ()` will fail as expected, +while `f False ()` will return `()` as expected. + +### Soundness of optimisations + +We note that you can soundly optimise `(\x -> M) N` into `M` if `x` is not mentioned in `M`, +or similar occurrences where the result of `N` isn't needed. +Such an optimisation will change the behaviour of the script necessarily, +as any traces in `N` will no longer happen, yet, this is not important in practice +as traces are merely a debugging tool. The budget used will decrease, +but people do not rely on budget exhaustion to signal invalidity. + +Transformations like `M || N` into `force (ifThenElse M (delay True) (delay N))` follow a similar principle: +traces that happened before might no longer happen. +The used budget will increase if M is `False`, yet this is likely +still an acceptable transformation for most people. + +### Backward compatibility + +This CIP has the issue of old scripts not being portable to the new version trivially. +You need to make sure your script isn't making use of any impure assumptions. + +## Path to Active + +### Acceptance Criteria + +It would be needed to implement the necessary changes in `cardano-ledger` and `plutus`. + +### Implementation Plan + +#### Implementation of built-ins + +This section does not have to be followed and is merely initial speculation +on how to implement this feature. + +The implementation of built-in functions in the Plutus library must +change to support built-ins that don't inspect all arguments, notably `ifThenElse`. +The naive way would be to translate errors to `undefined` and catch that impurely, yet this is hardly satisfying. + +Built-ins defined by `makeBuiltinMeaning` would, for a Plutus function of type `a0 -> a1 -> ... -> an`, +be defined by a Haskell-function `forall m. m a0 -> m a1 -> ... m an` instead. +If you don't bind an argument, it is not used, hence evaluation will still succeed +regardless of whether it is an error. +If it is bound, but is an error, then it will return an error as usual. + +To reduce the changes needed, you could instead of changing `makeBuiltinMeaning` provide +an alternative `makeLazyBuiltinMeaning` with the above functionality, changing the original +function to instead bind all arguments immediately, as most built-ins would do anyway. + +With this, the implementation of `ifThenElse` would be +```haskell +toBuiltinMeaning DefaultFunVX IfThenElse = + makeLazyBuiltinMeaning + (\b x y -> b >>= \case True -> x ; False -> y) + (runCostingFunThreeArguments . paramIfThenElse) +``` + +## Copyright + +[CC-BY-4.0]: https://creativecommons.org/licenses/by/4.0/legalcode +[Apache-2.0]: http://www.apache.org/licenses/LICENSE-2.0