PLT-7745: Basic rewrite rules for builtins #5584

bezirg · 2023-10-12T12:36:35Z

This is something like GHC's RULES, but for PIR. The complication is that the rewrite pass is supposed to be parameterized over the universe, which requires some boilerplate similar to the BuiltinsInfo boilerplate.

More rewrite rules to come. I just want to get this into master so I can further add more rules.
Also turned the previous CommuteFnWithConst transformation to a RewriteRule

Pre-submit checklist:

Branch
- Tests are provided (if possible)
- Commit sequence broadly makes sense
- Key commits have useful messages
- Changelog fragments have been written (if appropriate)
- Relevant tickets are mentioned in commit messages
- Formatting, PNG optimization, etc. are updated
PR
- (For external contributions) Corresponding issue exists and is linked in the description
- Targeting master unless this is a cherry-pick backport
- Self-reviewed the diff
- Useful pull request description
- Reviewer requested

bezirg · 2023-10-12T12:37:18Z

Can you take a first look? I am going to refactor it a bit and add comments.

Also I am thinking to incorporate commuteFnWithConst pass as a rewrite rule,
and add more rules.

bezirg · 2023-10-12T12:39:01Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

 import Control.Lens.TH
 import Data.Kind
 import PlutusCore.Builtin
 import PlutusCore.Builtin qualified as PLC
 import PlutusPrelude (Default (..))
+import PlutusIR qualified as PIR
+
+newtype RewriteRules uni fun = RewriteRules {


i am not fond of this newtype, but I had to do it to make makeLenses happy.

Also i could derive-newtype semigroup,monoid but then I had to write some boilerplate instances

I'm confused by the makeLenses problem?

I would have thought you could just derive semigroup and monoid via Dual Endo whatever if that's what you need.

Can you try it out? RankNTypes get in the way for me both for makeLenses and for derive-newtype Semigroup,Monoid

The lenses seem fine, deriving doesn't work because of the foralls. I would either just write the instances by hand or have a list in there and evaluate it where you use it.

michaelpj

General approach looks fine

michaelpj · 2023-10-12T12:55:34Z

plutus-core/plutus-ir/src/PlutusIR/Transform/Rewrite.hs

+decodeEncode = \case
+    BA DecodeUtf8 a1 a2 (BA EncodeUtf8 a3 a4 t) ->
+        -- place the missed annotations inside the rewritten term
+        (<> a1 <> a2 <> a3 <> a4) <$> t


I think this works here but might not work in general. Probably what I would do is require the caller of userRewrite to pass in an annotation to use for any newly generated terms that don't come from the source. Then we can pass in noProvenance or whatever.

Sounds complicated :(

Just a function argument?

They could use mempty for that reason?

instance Ord a => Monoid (Provenance a) where mempty = noProvenance

plutus-core/plutus-ir/src/PlutusIR/Transform/Rewrite.hs

michaelpj · 2023-10-12T13:02:25Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

 import Control.Lens.TH
 import Data.Kind
 import PlutusCore.Builtin
 import PlutusCore.Builtin qualified as PLC
 import PlutusPrelude (Default (..))
+import PlutusIR qualified as PIR
+
+newtype RewriteRules uni fun = RewriteRules {


I'm confused by the makeLenses problem?

michaelpj · 2023-10-12T13:02:48Z

plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs

 import Control.Lens.TH
 import Data.Kind
 import PlutusCore.Builtin
 import PlutusCore.Builtin qualified as PLC
 import PlutusPrelude (Default (..))
+import PlutusIR qualified as PIR
+
+newtype RewriteRules uni fun = RewriteRules {


I would have thought you could just derive semigroup and monoid via Dual Endo whatever if that's what you need.

michaelpj · 2023-10-12T13:03:50Z

plutus-core/plutus-ir/src/PlutusIR/Transform/Rewrite.hs

+defaultUniRewriteRules :: RewriteRules DefaultUni DefaultFun
+defaultUniRewriteRules = RewriteRules $ combineRules
+    -- rules are applied from left to right because of Dual
+    [ decodeEncode


As discussed, I'm not 100% sure this is safe. Maybe we should do head (mkCons x xs) = let !_ = xs in x or something?

Y I am also not certain.

Turns out that this rewrite is safe in Haskell because Text.fromString will handle gracefully non-unicode literal characters, see: https://hackage.haskell.org/package/text-2.1/docs/Data-Text.html#g:2

It would be safe for us if we:

handle unicode text in plutus-tx (currently broken)

handle non-unicode text gracefully in ghc-core like what is happening in Haskell . We have to replicate this behaviour in our plugin: https://hackage.haskell.org/package/text-2.1/docs/src/Data.Text.Internal.html#pack

bezirg · 2023-10-27T12:12:41Z

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs

+                   . (MonadQuote m, Semigroup a)
+                   => VarsInfo tyname name uni a
+                   -> PIR.Term tyname name uni fun a
+                   -> m (PIR.Term tyname name uni fun a)


@zliu41 @effectfully You probably wonder why MonadQuote m and VarsInfo are here. It is needed by all further rewrite rules (which are not yet in this PR).

effectfully

Looks good to me, comments are basically just nitpicking.

effectfully · 2023-10-27T14:14:50Z

plutus-core/plutus-ir/src/PlutusIR/Subst.hs

-- TODO: these could be Traversals
 -- | Get all the term variables in a term.
 vTerm :: Fold (Term tyname name uni fun ann) name
 vTerm = termSubtermsDeep . termVars


Do you disagree with the TODO?

I think I tried it, but I was hit but cosmosOf. CosmosOf requires Contravariant f, which Traversals cannot provide

I mean, is it in principle possible to have a Traversal focused on all the variables of a term? I think it is. If cosmosOf is getting in the way, then it just means cosmosOf isn't suitable for the job and we should use something else. Maybe we need to define this one in terms of deepOf or something, I'm not intimately familiar with lens.

I mean, is it in principle possible to have a Traversal focused on all the variables of a term? I think it is.

Or do you disagree with that?

I do think it is possible, it's just we don't crucially need atm. Also it can be misused and lead to more variable capturing problems? Anyway, I will bring back the note in another PR but with a MAYBE tag.

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/CommuteFnWithConst.hs

effectfully · 2023-10-27T21:13:37Z

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs

+{- | This rewrites: `(decodeUtf8 (encodeUtf8 x)) => x`
+
+This rewrite is safe because x is either valid by construction *In Haskell, but not in GHC-CORE*
+(see <https://hackage.haskell.org/package/text-2.1/docs/Data-Text.html#g:2>)


I'm not sure I understand the relevance of the link.

I will address it in a new PR solely for this decode/encode rewriterule

effectfully · 2023-10-27T21:18:00Z

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs

+decodeEncodeUtf8 = \case
+    BA DecodeUtf8 a1 a2 (BA EncodeUtf8 a3 a4 t) ->
+        -- place the missed annotations inside the rewritten term
+        (<> a1 <> a2 <> a3 <> a4) <$> t


Just nitpicking, but I'd use sconcat :: NonEmpty a -> a instead, because we have

data Provenance a = <...> | MultipleSources (S.Set (Provenance a))

and that would be a natural target for sconcat.

... except no implementation for sconcat is provided in

instance Ord a => Semigroup (Provenance a) where x <> y = MultipleSources (toSet x `S.union` toSet y) where toSet = \case MultipleSources ps -> ps other -> S.singleton other

but I think it's just an oversight and so I'd provide an implementation for sconcat and define <> in terms of that instead.

Do feel free to ignore this comment.

effectfully · 2023-10-27T21:20:22Z

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs

+    t -> t
+
+pattern BA :: fun -> a -> a -> Term tyname name uni fun a -> Term tyname name uni fun a
+pattern BA b a1 a2 t <- Apply a1 (Builtin a2 b) t


Too short of a global name IMO.

I'd just write Apply a1 (Builtin a2 b) t directly, it's not that longer and it's much more readable, but do feel free to ignore that.

effectfully · 2023-10-27T21:21:54Z

plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8.golden

The test is disabled but the golden file exists?

I will get rid of this rewrite rule completely for now

effectfully · 2023-10-27T21:25:12Z

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs

+import PlutusCore.Default
+import PlutusIR
+
+{- | This rewrites: `(decodeUtf8 (encodeUtf8 x)) => x`


I'd add a property test that decodeUtf8 . encodeUtf8 is id. Who knows what kind of horrible infernal UTF8 weirdness might be going on within those functions.

effectfully · 2023-10-27T21:26:31Z

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs

+    -- We collect `VarsInfo` on the whole program term and pass it on as arg to each RewriteRule.
+    -- This has the limitation that any variables newly-introduced by the rules would
+    -- not be accounted in `VarsInfo`. This is currently fine, because we only rely on VarsInfo
+    -- for isPure; isPure is safe w.r.t "open" terms.


Kinda nasty tbh, but I'm not sure what to do about it.

effectfully · 2023-10-27T21:31:38Z

plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs

+        (goldenPir (runQuote . RewriteRules.userRewrite def)  pTerm)
+        [ "equalsInt" -- this tests that the function works on equalInteger
+        , "divideInt" -- this tests that the function excludes not commutative functions
+        , "multiplyInt" -- this tests that the function works on multiplyInteger


I'd consider adding a property test that tests whether optimizing a term permutes all bulitin applications that are supposed to be permuted and leaves others intact, but this is quite a bit more work, so having several golden tests is probably enough indeed.

effectfully · 2023-10-27T21:32:31Z

plutus-tx/src/PlutusTx/Lift.hs

@@ -63,6 +65,8 @@ safeLift
       , PLC.Typecheckable uni fun
       , PrettyUni uni, Pretty fun
       , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)


Constraints in Plutus Tx are completely out of order.

By order you mean, i should stick to a certain e.g. alphabetical order accoss the file?

Sorry, I mean in the sense of "If something someone says or does is out of order, it is unpleasant or not suitable and it is likely to upset or offend people". They're way too bloated, but I don't know if we can have sensible type synonyms there.

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs

plutus-tx-plugin/src/PlutusTx/Options.hs

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs

zliu41

I don't see the rule for constrData and unConstrData; are you going to add it separately?

bezirg · 2023-10-30T10:18:06Z

I don't see the rule for constrData and unConstrData; are you going to add it separately?

Yes

Make CommuteFnWithConst transformation a RewriteRule

bezirg requested review from michaelpj and thealmarty October 12, 2023 12:36

bezirg self-assigned this Oct 12, 2023

bezirg commented Oct 12, 2023

View reviewed changes

michaelpj reviewed Oct 12, 2023

View reviewed changes

bezirg force-pushed the bezirg/pir-rewrite branch 6 times, most recently from fe39b51 to 9364099 Compare October 19, 2023 12:51

bezirg force-pushed the bezirg/pir-rewrite branch from 9364099 to 3288132 Compare October 19, 2023 14:40

bezirg force-pushed the bezirg/pir-rewrite branch 2 times, most recently from a45e706 to e023b19 Compare October 27, 2023 11:38

bezirg marked this pull request as ready for review October 27, 2023 11:38

bezirg requested review from effectfully and zliu41 and removed request for thealmarty October 27, 2023 11:39

bezirg force-pushed the bezirg/pir-rewrite branch 2 times, most recently from 3062a31 to 91155f9 Compare October 27, 2023 12:09

bezirg commented Oct 27, 2023

View reviewed changes

bezirg force-pushed the bezirg/pir-rewrite branch 4 times, most recently from ac26414 to 83ac15d Compare October 27, 2023 12:44

effectfully approved these changes Oct 27, 2023

View reviewed changes

effectfully reviewed Oct 27, 2023

View reviewed changes

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs Outdated Show resolved Hide resolved

zliu41 reviewed Oct 28, 2023

View reviewed changes

plutus-tx-plugin/src/PlutusTx/Options.hs Outdated Show resolved Hide resolved

plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs Outdated Show resolved Hide resolved

zliu41 reviewed Oct 28, 2023

View reviewed changes

PLT-7745: Basic rewrite rules for builtins

82c38e0

Make CommuteFnWithConst transformation a RewriteRule

bezirg force-pushed the bezirg/pir-rewrite branch from 83ac15d to 82c38e0 Compare October 30, 2023 12:39

bezirg enabled auto-merge (squash) October 30, 2023 14:00

bezirg merged commit fcd13d1 into master Oct 30, 2023
6 checks passed

bezirg deleted the bezirg/pir-rewrite branch October 30, 2023 14:47

PLT-7745: Basic rewrite rules for builtins #5584

PLT-7745: Basic rewrite rules for builtins #5584

Conversation

bezirg commented Oct 12, 2023 • edited Loading

bezirg commented Oct 12, 2023

bezirg Oct 12, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michaelpj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bezirg Oct 18, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bezirg Oct 27, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

effectfully left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zliu41 left a comment

Choose a reason for hiding this comment

bezirg commented Oct 30, 2023

bezirg commented Oct 12, 2023 •

edited

Loading

bezirg Oct 12, 2023 •

edited

Loading

bezirg Oct 18, 2023 •

edited

Loading

bezirg Oct 27, 2023 •

edited

Loading