| CIP | Title | Category | Status | Authors | Implementors | Discussions | Created | License | ||
|---|---|---|---|---|---|---|---|---|---|---|
92 |
First-class errors in Plutus |
Plutus |
Proposed |
|
|
2023-03-01 |
CC-BY-4.0 |
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
errora 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
delayandforce.
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:
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 IntersectMBO/plutus#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 forces 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.
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.
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.
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.
runPLCScript 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.
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:
let factorial n = ifThenElse (n == 0) 1 (factorial (n - 1))
in factorial 2The 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) is:
let* !boom = λ {a} -> ERROR
!id = λ {a} (x :: a) -> x
in λ (b :: Bool) -> ifThenElse {∀ a. a -> a} b boom idIndeed, this example works without adding delays to type abstractions, as the untyped form
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.
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.
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.
It would be needed to implement the necessary changes in cardano-ledger and plutus.
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
toBuiltinMeaning DefaultFunVX IfThenElse =
makeLazyBuiltinMeaning
(\b x y -> b >>= \case True -> x ; False -> y)
(runCostingFunThreeArguments . paramIfThenElse)