Closed Niols closed 5 months ago
Below is a summary of what we've found so far.
We first found this comment on a related scenario: https://github.com/input-output-hk/plutus/blob/75ccaf42ac5a452c32d76c8bb4ff49006eb56c7a/plutus-tx-plugin/src/PlutusTx/Compiler/Type.hs#L168-L171
We then experimented around to observe different outputs of different writing styles. A relevant finding is that inlining the if then else
code doesn't reproduce the bug, but calling ||
does.
Unfortunately, changing this INLINEABLE
pragma to INLINE
still doesn't inline ||
.
https://github.com/input-output-hk/plutus/blob/75ccaf42ac5a452c32d76c8bb4ff49006eb56c7a/plutus-tx/src/PlutusTx/Bool.hs#L22-L30
We then took a look at the compiled PIR.
example :: Bool
example = if fromBuiltin (BI.equalsInteger 1 1) then True else trace "no" False
Is compiled (with PlutusTx.Plugin:defer-errors
only) to:
...
[
[
{
[
Bool_match_321
(let
(nonrec)
(termbind
(strict)
(vardecl b_378 (con bool))
[
[ (builtin equalsInteger) (con integer 1) ] (con integer 1)
]
)
[
[ [ { (builtin ifThenElse) Bool_318 } b_378 ] True_319 ]
False_320
]
)
]
(all dead_374 (type) Bool_318)
}
(abs dead_375 (type) True_319)
]
(abs
dead_376
(type)
[ [ { (builtin trace) Bool_318 } (con string "no") ] False_320 ]
)
]
(all dead_377 (type) dead_377)
...
While:
example :: Bool
example = fromBuiltin (BI.equalsInteger 1 1) || trace "no" False
Is compiled (with PlutusTx.Plugin:defer-errors
only) to:
...
(let
(nonrec)
(termbind
(strict)
(vardecl l_381 Bool_254)
(let
(nonrec)
(termbind
(strict)
(vardecl b_393 (con bool))
[ [ (builtin equalsInteger) (con integer 1) ] (con integer 1) ]
)
[
[ [ { (builtin ifThenElse) Bool_254 } b_393 ] True_255 ] False_256
]
)
)
(lam
r_382
Bool_254
{
[
[
{ [ Bool_match_257 l_381 ] (all dead_383 (type) Bool_254) }
(abs dead_384 (type) True_255)
]
(abs dead_385 (type) r_382)
]
(all dead_386 (type) dead_386)
}
)
)
[ [ { (builtin trace) Bool_254 } (con string "no") ] False_256 ]
...
This inspired an attempt (#4118) that removes the lam
wrapper for ||
and &&
, by compiling the function call directly to a case expression.
-- Lazy ||
GHC.App (GHC.App (GHC.Var fid) a) b | GHC.getOccString fid == "||" ->
compileExpr $ GHC.mkIfThenElse a (GHC.Var GHC.trueDataConId) b
-- Lazy &&
GHC.App (GHC.App (GHC.Var fid) a) b | GHC.getOccString fid == "&&" ->
compileExpr $ GHC.mkIfThenElse a b (GHC.Var GHC.falseDataConId)
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 let
, case
and if-then-else
are compiled lazily, however.
Indeed, Plutus Core is strict, which makes a lot of sense. So I guess I would expect <e1> || <e2>
to be compiled lazily just like the case
and if-then-else
by putting e2
in a thunk. I guess in my head <e1> || <e2> ~= if <e1> then True else <e2>
and this should be (and is) lazy in Plutus.
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 ||
and &&
: they are just functions, and they behave the same as all functions. We could compile all function application non-strictly, but this would add a massive amount of overhead. Or we could special-case ||
and &&
- but this is just setting people up for confusion since it makes them behave differently to every other function.
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.
Is there a reason why that is?
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:
Bool
that gets or
-ed correctly, the final answer is deterministic. That said, trueCondition || error ()
would invalidate an actually valid transaction. It is increasingly dangerous when it is embedded in a lazy (for example, case) branch. A non-exhaustive test suite might lead to forever-locked assets.simpleCommonCheck || expensiveChecks
is still common enough.||
simply behaves so in most popular languages. We had no clues about the strict behavior until @Niols did some concolic execution work that ended up with odd traces. We're still puzzled after a week after some involved investigation. Typical applications might just evaluate unnecessary things with users paying extra fees for the whole lifespan without anyone noticing. To back these speculations, we're going to find and study the raw on-chain scripts that use ||
, &&
, or generally error
usage in strict semantics fetched from the chain index.
As for solutions, we have the following proposals:
||
and &&
. I went for #4118 because I saw many inlining and removals of GHC.App
in plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs
. Better solutions are always welcomed as long as we have lazy ||
and &&
in the end.|
/or
and &
/and
or something like that.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.
It can reduce size and improve execution of the scripts. And for many strict languages &&
and ||
execute short-circuit
this seems to be surprising deviation for Plutus.
We had to define our own versions of all
and any
because of that.
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 traceError
quite a lot...
I agree that the behaviour is confusing:
&&
and ||
to make them lazySo 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 &&
and ||
are just functions). What secret knowledge are they missing that makes them behave differently? Could other things behave differently?
Even if we did special-case &&
and ||
, you're going to trip over this immediately at the next level. any
is a good example: you give it a list of booleans... which will be evaluated strictly! So you're hit with the strict behaviour again, except this time it's (IMO) worse because it's now weirdly inconsistent.
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 &&
and ||
as INLINE
, in which case by the time we get to them they would have been replaced by their (lazy) bodies.
(You might find the discussion of the similar issue in purescript interesting: https://github.com/purescript/purescript/issues/3457. There they have &&
and ||
being lazy by accident, and people are not happy about it.)
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 &&
and ||
which must be lazy to work correctly, which I am now replacing with if
-expressions after reading this issue.
We had some time to revisit the issue today and did a quick check on this cheapCheck || expensiveChecks
example at plutus-use-cases
:
https://github.com/HachiSecurity/plutus-use-cases/pull/1/files
This innocent-looking ||
might require over 1.5 times more resources than an unnatural-looking if-then-else
.
-- || 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
as documented in the official how-to.
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 ||
still evaluates the heavy-weight right-hand side that yields a much larger script and requires over 1.5 times more resources than a short-circuit solution in if-then-else
. The behaviour might be extremely costly and wasteful had a frequently updated oracle feed falls into this case.
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. hlint
itself suggests the change!
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 ||
s or &&
s just a few lines apart in the same module, or in two adjacent modules can have different semantics.
&&
is even more common than ||
with patterns like con1 && con2 && con3
. Even though most APIs would invalidate and refuse to submit the transaction off-chain for an early False
, they are still wasteful calculations that could be saved. One never gets enough resource savings for blockchain tech.
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 ||
and &&
with if-then-else
or case-of
like Edmund did.
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 ||
and &&
lazily (through a flag?). We will not convince people which is the way, just let the developers decide based on their needs.
...
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 if-then-else
expansion with TH.
We can use TH to transform and
and or
expressions to boring long versions that implement short circuit.
Here is PR #4191
@anton-k Awesome! That is definitely useful in several use cases :+1:.
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 UnliftedDatatypes
, which is some way away from being usable in practice, I fear. Maybe we could get away with making things generally non-strict, but I'm pretty wary.
@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.
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.
The above CIP in fact also fixes the issue with expensive1 || expensive2
being suboptimal.
I'm annoyed by the problem and want to keep the issue open until we come to the conclusion that we don't care.
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.
@L-as
Fixed by https://github.com/cardano-foundation/CIPs/pull/469
The above CIP in fact also fixes the issue with expensive1 || expensive2 being suboptimal.
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 expensive2
, unless we turn it into if expensive1 then True else expensive2
, which we don't have any reasonable and reliable way of doing in the first place (hardcoding specific operator names isn't reasonable and marking definitions with INLINE
isn't reliable).
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.