From 2d0a995a09f7b75c8e04d3c4bd4995af731e20a5 Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 00:44:48 +0000 Subject: [PATCH 1/8] First class errors CIP initial commit --- CIP-XXXX/README.md | 165 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 CIP-XXXX/README.md diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md new file mode 100644 index 0000000000..e8db29be70 --- /dev/null +++ b/CIP-XXXX/README.md @@ -0,0 +1,165 @@ +--- +CIP: ? +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`. + +## Motivation: why is this CIP necessary? + +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 TPLC, 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. + +## 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. + +## 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 From 83bb488a059c6a5d4ffabb2dd55aab0daa10fd07 Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 00:46:29 +0000 Subject: [PATCH 2/8] Add note about backward compatibility --- CIP-XXXX/README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index e8db29be70..8e0984cd05 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -124,6 +124,11 @@ is precisely the example we seek to make work. `f True ()` will fail as expected, while `f False ()` will return `()` as expected. +### 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 From f1c00a131458830757b480ee6ea81669cc56a0c5 Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 00:58:23 +0000 Subject: [PATCH 3/8] small change --- CIP-XXXX/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index 8e0984cd05..f58974ae73 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -25,7 +25,7 @@ We propose three changes: - Erase type abstractions and type applications entirely when going from TPLC to UPLC rather than turning them into `delay` and `force`. -## Motivation: why is this CIP necessary? +## 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**. From bcf590e70af44bb4c61e6057d4701c12ee84f134 Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 11:51:57 +0000 Subject: [PATCH 4/8] Add comment about optimisation and list of issues closed --- CIP-XXXX/README.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index f58974ae73..b28cc3f20d 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -25,6 +25,19 @@ We propose three changes: - 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, @@ -49,6 +62,10 @@ toolchains, but also means that all built-ins will no longer need to be forced b 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. + ## Specification The changes below would need to take effect in a new ledger era and Plutus version. From d81aa52be84d814179b461afa1f2c75b458dde8d Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 13:50:45 +0000 Subject: [PATCH 5/8] Add more text about soundness of optimisations --- CIP-XXXX/README.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index b28cc3f20d..5e19e06000 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -66,6 +66,10 @@ As noted in the abstract, we can now also do optimisations on the UPLC that were 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. @@ -141,6 +145,20 @@ 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 `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. From 0c5d382909d2a8069fb480bb79ed6a79dfe23afd Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 13:53:19 +0000 Subject: [PATCH 6/8] 1 TPLC -> PIR --- CIP-XXXX/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index 5e19e06000..3d26859270 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -54,7 +54,7 @@ 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 TPLC, the erasure of which into UPLC +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. From afb05fac675a14d6abc3841299ffce88480ba1e1 Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 2 Mar 2023 13:56:41 +0000 Subject: [PATCH 7/8] Add accidentally removed words --- CIP-XXXX/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index 3d26859270..979f6880b0 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -147,7 +147,7 @@ while `f False ()` will return `()` as expected. ### Soundness of optimisations -We note that you can soundly optimise `(\x -> M) N` into `x` is not mentioned in `M`, +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 From e49ea78306f63c8ae3eb4334537658292199b58d Mon Sep 17 00:00:00 2001 From: Las Safin Date: Thu, 6 Apr 2023 12:11:37 +0000 Subject: [PATCH 8/8] Update CIP-XXXX/README.md Co-authored-by: Matthias Benkort <5680256+KtorZ@users.noreply.github.com> --- CIP-XXXX/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CIP-XXXX/README.md b/CIP-XXXX/README.md index 979f6880b0..4f9bd2ea3e 100644 --- a/CIP-XXXX/README.md +++ b/CIP-XXXX/README.md @@ -1,5 +1,5 @@ --- -CIP: ? +CIP: 92 Title: First-class errors in Plutus Category: Plutus Status: Proposed