-
Notifications
You must be signed in to change notification settings - Fork 483
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
overzZzealous: Non-lazy Semantics of || and && in Plutus Core #4114
Comments
Below is a summary of what we've found so far. We first found this comment on a related scenario: We then experimented around to observe different outputs of different writing styles. A relevant finding is that inlining the Unfortunately, changing this We then took a look at the compiled PIR.
Is compiled (with
While:
Is compiled (with
This inspired an attempt (#4118) that removes the
This solves the problem but is a bit too specific for our taste. We wonder if there may be further problems in either the compiler, the current interpreter, or if there is a better general fix. We've made a few guesses along the way and agreed that discussing here first would be best. Any insights from the core team would be well appreciated! |
Function application in Plutus Core is strict, and function application in Haskell is compiled directly to function application in Plutus Core. This is a difference in the expected semantics, for sure. Syntactic constructs such as |
Indeed, Plutus Core is strict, which makes a lot of sense. So I guess I would expect I do think it should be considered a bug that it is not compiled lazily, as most people would expect that. I can see how it can be made a feature, but I think it should then be heavily documented. |
The issue is not with Yes, we need to document this clearly. |
Oh. I did not realise they were functions and not operators of the language. This indeed explains everything. Is there a reason why that is? I suppose it can come from Haskell seeing them as functions, which reproduces the semantics of other languages because of the lazy evaluation of arguments, but it does create a surprising change of semantics when going to a strict language. |
Booleans aren't a special type either. Booleans and their functions are compiled just like any other datatypes and functions, there's no special handling. |
In my humble opinion, we should still consider this particular case given the following contexts:
To back these speculations, we're going to find and study the raw on-chain scripts that use As for solutions, we have the following proposals:
Also, as someone who cheers for both sides, I feel it's better to do ad-hoc optimizations on the compiler side in exchange for better UX and performance for end developers and users. The compilation pipeline is non-trivial, but the language itself is not large. We can write more documentation and refactor code more freely (as long as things are backward-compatible, which is still the compiler complication that we propose to accept?) while deployed scripts stick. A small compiler optimization might translate to a considerable amount of ADA for long-lived and high-traffic dApps! Most end developers wouldn't work anywhere close to the Plutus Core level to face this complexity too. Either way, we're always ready to help when needed! |
It's worth to consider Boolean as special case. Since it is so ubiquitous for contract logic. |
We had to define our own versions of |
Programming with side-effects is always tricky, and in Plutus no less. Ideally we would encourage people from using side-effects too much, but in fact people use I agree that the behaviour is confusing:
So we are doing something unusual! The question is what alternative is worse. I think having special cases for just a few functions is quite costly in its own way. It breaks people's mental model of what's going on (especially if they know that Even if we did special-case So for the time being I think it is better just to document the behaviour carefully. If we did want to implement this, we could consider just marking (You might find the discussion of the similar issue in purescript interesting: purescript/purescript#3457. There they have |
Yeah, I agree with @anton-k that the current state is not ideal for dApp developers. That said, until we get to know the compiler better and have real data on the way developers write scripts, we're not 100% confident with any change as well. I think the sane solution for any direction going forward is to document better for end developers. We are always ready to help on this front, just never knowing in which format would it be useful for the community to justify the efforts. |
Just as a representative example, our contract code has quite a few uses of CommentarySomething I haven't seen mentioned is that the Plutus compiler's input is GHC Core that has already been processed by GHC's simplifier. It's well known that some optimizations are good, or even legal, for lazy languages and not on strict languages. The simplifier has no idea of this difference in Plutus between let-bindings and function application, and is free to inline let-bindings and even common out function argument expressions, should it be tempted, under the assumption that this doesn't change semantics.I don't understand why Plutus Core is strict, rather than nonstrict like GHC Core. I read that this was to keep gas consumption predictable, but having let-bound variables evaluated every time they're used has in practice been very unpredictable, and only forced us to litter code with bang-patterns. |
We had some time to revisit the issue today and did a quick check on this This innocent-looking -- || is surprisingly way more expensive!
isUpdateValid = (not isCurrentValueSigned) ||
(fromMaybe False $ validateGameStatusChanges <$>
(osmGameStatus <$> extractSigendMessage (ovSignedMessage oracleData)) <*>
(osmGameStatus <$> extractSigendMessage outputSignedMessage))
-- if-then-else is way cheaper!
isUpdateValid = if not isCurrentValueSigned then True else
(fromMaybe False $ validateGameStatusChanges <$>
(osmGameStatus <$> extractSigendMessage (ovSignedMessage oracleData)) <*>
(osmGameStatus <$> extractSigendMessage outputSignedMessage)) We calculate the required budget using writeScriptsTo
(ScriptsConfig "." (Scripts UnappliedValidators))
"updateOracleTrace"
Spec.Oracle.updateOracleTrace
def The difference is rather significant: -- With `||`:
( Sum {getSum = 9539}
, ExBudget {exBudgetCPU = ExCPU 1124168956, exBudgetMemory = ExMemory 3152700}
)
-- With `if-then-else`:
( Sum {getSum = 3531}
, ExBudget {exBudgetCPU = ExCPU 698345767, exBudgetMemory = ExMemory 2069978}
) When the quick check is satisfied, the strict The worst part is that we had no clues about this behaviour until we diligently built a PLC concolic execution engine. Otherwise, we would write such wasteful code ourselves, given how natural that code looks like. src/Contracts/Oracle/OnChain.hs:(136,21)-(139,69): Warning: Redundant if
Found:
if not isCurrentValueSigned then
True
else
(fromMaybe False
$ validateGameStatusChanges
<$>
(osmGameStatus
<$> extractSigendMessage (ovSignedMessage oracleData))
<*> (osmGameStatus <$> extractSigendMessage outputSignedMessage))
Perhaps:
not isCurrentValueSigned
||
(fromMaybe False
$ validateGameStatusChanges
<$>
(osmGameStatus
<$> extractSigendMessage (ovSignedMessage oracleData))
<*> (osmGameStatus <$> extractSigendMessage outputSignedMessage)) It is common to write contracts with on-chain and off-chain code very close to each other. It is scary how two
We'd love to help document and communicate the behaviour to end developers. We'll add another example with dangerous side-effects, search for deployed scripts with unnecessarily-expensive/side-effect patterns, and implement a fix if the core team decided on any. |
Plutus Core is a strict language, for better or worse at this point. Yes we need to communicate that better, I agree. Possibly we just need an explainer piece in the documentation. |
We've already been writing a blog post documenting this topic in more depth. If it's welcomed I can port the content rewritten in formal documentation style to a PR somewhere appropriate. I've talked to a few developers and they're probably going to rewrite all Code like quoted below would become very hard to read, but most products desire cheaper transaction fees, even faster off-chain validations (few users would run their own node, and project nodes are already accompanied with a currently-still-slow chain index and all the extra infrastructure required) at the moment. Alternatively, developers can compile with an ad-hoc fork that has an extra commit that compiles ...
iP1 :: TxInInfo -> Bool
iP1 TxInInfo{txInInfoResolved=TxOut{txOutValue}} = ...
iP2 :: TxInInfo -> Bool
iP2 TxInInfo{txInInfoResolved=TxOut{txOutValue}} = ...
inConditions = (iP1 t1 && iP2 t2) || (iP1 t2 && iP2 t1)
ol1 :: TxOut -> Bool
ol1 o@TxOut{txOutValue} = ...
ol2 :: TxOut -> Bool
ol2 o@TxOut{txOutValue} = ...
outConditions = (ol1 o1 && ol2 o2) || (ol1 o2 && ol2 o1)
in inConditions && outConditions In conclusion, most developers I've talked to agree that this is very nice to have, but not critical at the moment. They would love us to reduce script sizes more, for instance. Let's document this nicely and move on for now I guess. (Unless you would accept an ad-hoc flag for the ad-hoc behaviour?) |
I've defined possible solution to clumsy Here is PR #4191 |
@anton-k Awesome! That is definitely useful in several use cases 👍. |
I may be a outlier here, but I don't think it makes any sense to compile GHC Core as though it were for a strict language. It would make much more sense to me to treat it as exactly the language it is, and to expect user-written code to be as strict as it should be. Doing this efficiently does mean changing some datatypes. For example, a builtin list read from the blockchain should be encoded as an entirely strict list. Eventually, it will make sense to use unlifted datatypes (9.2.1 doesn't handle those right for worker/wrapper; the fix might get backported for 9.2.2). But the current approach is much too wild. Perfectly reasonable core2core transformations can produce wildly different performance in Plutus, and there are all sorts of horrible hacks to try to avoid that. |
@treeowl I don't think you're an outlier. I think it's pretty arguable that the approach we take isn't the best one. One alternative would be what you expect: get users to write strict Haskell if they want strict Plutus Core. But this also leaves people lots of scope for footguns in terms of making things less trict than they meant to. And, as you point out, doing it in a systematic and principled fashion would really need |
@michaelpj, yes, there would be footguns, but I think a lot fewer than there are now. This is just too wild to be able to program. Have you been able to take a look at some of my recent questions in #4206? I could use a bit of help. |
Hachi team had a detailed writeup on this issue at https://blog.hachi.one/post/overzzzealous-peculiar-semantics-or-and-plutus-core. Hopefully, this raises awareness in the Cardano community, helping developers to avoid the issue and write more efficient validator scripts. |
this definitely raised awareness and there were some unexpected behaviors with our && operator inside a validator. We'll report back with more information once we apply the knowledge shared in the article if it was really a problem of Plutus Core or was it on our side. |
Since it is not an issue but the correct semantics, I suppose we can close this issue? |
I'm annoyed by the problem and want to keep the issue open until we come to the conclusion that we don't care. |
Fixed by cardano-foundation/CIPs#469 |
The above CIP in fact also fixes the issue with |
I now have a task on writing a proposal on adding limited laziness to the language. It'll probably take time for me to get to it, but at least we seem to have some path forward.
I wouldn't say your proposal fixes the issue entirely, if I understand your proposal correctly. While it does fix the denotational semantics of boolean functions, their operational semantics would still suck. Namely, the user would still have to pay for unnecessary evaluation of |
You can just have a RULE for it @effectfully |
Hi there,
While developping tools with Hachi, we noticed something that we believe is a bug in the compiler from Plutus to Plutus Core.
Best,
Nicolas
EDIT: It seems to not be considered a bug. Since we believe it will still come up regularly in issues here and there, we decided to give this peculiarity the sweet name of “overzZzealous”. See also our blog post on the topic.
Area
Summary
The compiler from Plutus to Plutus Core seems to compile
||
and&&
as non-lazy, that is where the right-hand side is evaluated regardless of what the left-hand side evaluates to.Steps to reproduce
In general:
||
or&&
. (eg.if True || error () then do_something else True
)More guided, within the Plutus Application Backend (PAB) example:
validateGuess
in./examples/src/Plutus/Contracts/Game.hs
to introduce anerror ()
side-effect on the right of an||
. We suggest to use:validateGuess hs cs _ = if True || error () then isGoodGuess hs cs else True
.Check our fork of the Plutus Platform starter project for a more guided version, including Shell scripts to play and modify the code in your place.
Expected behavior
We would expect
||
and&&
to be lazy and to only evaluate their second argument only if the first one evaluates toFalse
andTrue
respectively. This expectation is based on the fact that it is the case in a lot of languages and therefore we believe programmers will expect this as well. Moreover, it seems to be the case both in Haskell and in off-chain Plutus.System info
Tested on several machines, all with latest Plutus.
Attachments
See our blog post on the topic: overzZzealous: the Peculiar Semantics of
||
and&&
in Plutus Core.The text was updated successfully, but these errors were encountered: