plutus icon indicating copy to clipboard operation
plutus copied to clipboard

Published 20 hours ago • verified publisher icon IntersectMBO

Simplification pass assumes laziness, resulting in miscompilation

Open L-as opened this issue 3 years ago • 3 comments

Summary

While UPLC/PLC/PIR are strict, a simplification pass assumes the code is to be interpreted lazily, thus resulting in the following behaviour: let c x _ = x in c True (error ()) will not err. If you however set it to const, it will err, because it's not simplified (for some arcane reason).

Concrete example in fork of Plutus: https://github.com/mlabs-haskell/plutus/commits/las/miscompilation

Do you have a proposed solution for this issue?

It's not clear to me whether it's GHC doing this or a Plutus library. In the former case, disable the optimisation pass, however this would lead to decreased efficiency, in the latter case, keep track of whether it's possible for the term to err.

System info

No response

L-as avatar Aug 25 '22 19:08 L-as

Sorry, can you be more specific? Is this a PIR program? A Haskell program?

Unfortunately we can't stop GHC from touching the program entirely, so if this is Haskell it may indeed be something that GHC is doing.

michaelpj avatar Aug 26 '22 09:08 michaelpj

I've posted a link to a fork in the summary where I've added goldens for the test. Another link: https://github.com/mlabs-haskell/plutus/commit/eee1404aae86594fae0b604a058bbac7e79c295a#diff-1eec071a1e24882fcf29911ff286bec003f983927819ae99ad431fdf75867799 It's a Haskell program.

L-as avatar Aug 26 '22 10:08 L-as

That's helpful, thanks.

michaelpj avatar Aug 26 '22 10:08 michaelpj

This was brought into the sprint, but hasn't been worked on yet. Chances are, it'll take a bit more time for us to get to this issue, I will keep you updated.

effectfully avatar Mar 05 '23 03:03 effectfully

PR #5280 shows that with the noinline pragma the evaluation results for the two examples are now the same. I.e., it IS GHC's inliner that causes the inconsistency.

For now, users will have to turn off the GHC inliner by hand with the noinline pragma for affected functions. For example:

trueOrError :: CompiledCode Bool
trueOrError = $$(compile [|| c True (P.error () :: Bool) ||])
  where
    {-# NOINLINE c #-}
    c x _ = x

The team will be discussing and exploring better solutions. We welcome your input as well.

thealmarty avatar May 01 '23 17:05 thealmarty

More discussion in this ADR.

@zliu41 do you have an idea on what we should do with this issue?

effectfully avatar May 16 '23 02:05 effectfully

Strict is the only option. The other option (nonstrict) requires a way to prevent GHC from inlining things but that isn't currently possible.

zliu41 avatar May 16 '23 03:05 zliu41

@zliu41 should we keep this issue open or advertise using Strict and close the issue or something else? I'm just not sure how proceed with this specific GitHub issue.

effectfully avatar May 16 '23 13:05 effectfully

Let's keep it open until we merge #5292 and start telling people to use Strict.

zliu41 avatar May 16 '23 13:05 zliu41

Let's keep it open until we merge https://github.com/input-output-hk/plutus/pull/5292 and start telling people to use Strict.

@zliu41 we aren't telling people to use Strict quite yet, right?

effectfully avatar Jul 17 '23 23:07 effectfully

@zliu41 we aren't telling people to use Strict quite yet, right?

Right. The internal ticket tracking this is PLT-5830.

zliu41 avatar Jul 19 '23 16:07 zliu41

The internal ticket tracking this is PLT-5830.

It's merged now (has been for a while) and hence we can close this issue with the following general advice: use Strict, otherwise GHC will misbehave.

effectfully avatar Nov 22 '23 11:11 effectfully