overzZzealous: Non-lazy Semantics of || and && in Plutus Core

[Niols]

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

• [x] Plutus Foundation
• [ ] Plutus Application Framework
• [ ] Marlowe
• [ ] Other

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:

1. Take any Plutus code that runs on-chain.
2. Introduce side-effects on the right of a || or &&. (eg. if True || error () then do_something else True)
3. Observe that the side-effect is triggered.

More guided, within the Plutus Application Backend (PAB) example:

1. Clone the input-output-hk/plutus-starter project.
2. Follow the README to setup the project and to play the game with the PAB. Check that everything works: you get a validation error if you guess wrong, and the transation is validated if you guess right.
3. Update validateGuess in ./examples/src/Plutus/Contracts/Game.hs to introduce an error () side-effect on the right of an ||. We suggest to use: validateGuess hs cs _ = if True || error () then isGoodGuess hs cs else True.
4. Play the game again and observe that you get a validation error whether you guess right or wrong.

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 to False and True 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.

• 1:
  • OS: NixOS 21.05, up-to-date as of Friday, October 15th, 2021.
  • GHC: 8.10.4
• 2:
  • OS: MacOS 11.6
  • GHC: 8.10.4

Attachments

See our blog post on the topic: overzZzealous: the Peculiar Semantics of || and && in Plutus Core.

[kk-hainq]

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!

[michaelpj]

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.

[Niols]

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.

[michaelpj]

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.

[Niols]

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.

[michaelpj]

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.

[kk-hainq]

In my humble opinion, we should still consider this particular case given the following contexts:

• Bug-wise, it only matters in the presence of side effects. Elsewhere it would evaluate to a typical 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.
• Performance-wise, it costs users more fees evaluating unnecessary things. Most real code I've seen is written in case-style pattern matching, but simpleCommonCheck || expensiveChecks is still common enough.
• We don't necessarily think that short-circuit evaluations are good. || 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:

• Apply a fix to have lazy || 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.
• Add the strict versions in |/or and &/and or something like that.
• Clearly document the differences between the two. It should hopefully catch more attention with two variants now. If having either is confusing, maybe just have and document both.
• Write tight tests.

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!

[anton-k]

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.

[anton-k]

We had to define our own versions of all and any because of that.

[michaelpj]

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:

• People don't know that function application will be strict
• Other strict languages often special-case && and || to make them lazy

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 && 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.)

[kk-hainq]

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.

[edmundnoble]

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.

Commentary

Something 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.

[kk-hainq]

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.

[michaelpj]

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.

[kk-hainq]

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.

https://github.com/input-output-hk/plutus-apps/blob/c3676cfe11bcd8512d7353ee337de8e84c7f2278/plutus-use-cases/src/Plutus/Contracts/Swap.hs#L133-L163

    ...
    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?)

[anton-k]

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

[kk-hainq]

@anton-k Awesome! That is definitely useful in several use cases :+1:.

[treeowl]

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.

[michaelpj]

@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.

[treeowl]

@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.

[aquynh]

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.

[Mercurial]

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.

[Niols]

Since it is not an issue but the correct semantics, I suppose we can close this issue?

[effectfully]

I'm annoyed by the problem and want to keep the issue open until we come to the conclusion that we don't care.

[L-as]

Fixed by https://github.com/cardano-foundation/CIPs/pull/469

[L-as]

The above CIP in fact also fixes the issue with expensive1 || expensive2 being suboptimal.

[effectfully]

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).

[L-as]

You can just have a RULE for it @effectfully