diff --git a/doc/read-the-docs-site/reference/writing-scripts/compiler-options-table.rst b/doc/read-the-docs-site/reference/writing-scripts/compiler-options-table.rst
index 1d29257dc0a..f45bb4a5ed2 100644
--- a/doc/read-the-docs-site/reference/writing-scripts/compiler-options-table.rst
+++ b/doc/read-the-docs-site/reference/writing-scripts/compiler-options-table.rst
@@ -132,6 +132,10 @@
      - True
      - Run a simplification pass that removes dead bindings
 
+   * - ``simplifier-rewrite``
+     - Bool
+     - True
+     - Run a pass that performs some pre-defined rewrite rules on builtins (similar to GHC's RULES)
 
    * - ``simplifier-unwrap-cancel``
      - Bool
diff --git a/plutus-core/changelog.d/20231027_133344_bezirg_pir_rewrite.md b/plutus-core/changelog.d/20231027_133344_bezirg_pir_rewrite.md
new file mode 100644
index 00000000000..ac543d8b08a
--- /dev/null
+++ b/plutus-core/changelog.d/20231027_133344_bezirg_pir_rewrite.md
@@ -0,0 +1,5 @@
+### Added
+
+- A new pass in the simplifier that rewrites PIR terms given user-provided rules.
+  It behaves similar to GHC's RULES, but for the PIR language.
+  By default, a pre-defined set of rules are applied when the PIR simplifier is enabled.
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
index b617251865f..9777c51d5a6 100644
--- a/plutus-core/plutus-core.cabal
+++ b/plutus-core/plutus-core.cabal
@@ -503,7 +503,6 @@ library plutus-ir
     PlutusIR.Transform.Beta
     PlutusIR.Transform.CaseOfCase
     PlutusIR.Transform.CaseReduce
-    PlutusIR.Transform.CommuteFnWithConst
     PlutusIR.Transform.DeadCode
     PlutusIR.Transform.EvaluateBuiltins
     PlutusIR.Transform.Inline.CallSiteInline
@@ -516,6 +515,8 @@ library plutus-ir
     PlutusIR.Transform.NonStrict
     PlutusIR.Transform.RecSplit
     PlutusIR.Transform.Rename
+    PlutusIR.Transform.RewriteRules
+    PlutusIR.Transform.RewriteRules.CommuteFnWithConst
     PlutusIR.Transform.StrictifyBindings
     PlutusIR.Transform.Substitute
     PlutusIR.Transform.ThunkRecursions
@@ -532,6 +533,7 @@ library plutus-ir
     PlutusIR.Compiler.Lower
     PlutusIR.Compiler.Recursion
     PlutusIR.Normalize
+    PlutusIR.Transform.RewriteRules.DecodeEncodeUtf8
 
   build-depends:
     , algebraic-graphs     >=0.7
@@ -588,7 +590,6 @@ test-suite plutus-ir-test
     PlutusIR.Transform.Beta.Tests
     PlutusIR.Transform.CaseOfCase.Tests
     PlutusIR.Transform.CaseReduce.Tests
-    PlutusIR.Transform.CommuteFnWithConst.Tests
     PlutusIR.Transform.DeadCode.Tests
     PlutusIR.Transform.EvaluateBuiltins.Tests
     PlutusIR.Transform.Inline.Tests
@@ -598,6 +599,7 @@ test-suite plutus-ir-test
     PlutusIR.Transform.NonStrict.Tests
     PlutusIR.Transform.RecSplit.Tests
     PlutusIR.Transform.Rename.Tests
+    PlutusIR.Transform.RewriteRules.Tests
     PlutusIR.Transform.StrictifyBindings.Tests
     PlutusIR.Transform.ThunkRecursions.Tests
     PlutusIR.Transform.Unwrap.Tests
@@ -607,6 +609,7 @@ test-suite plutus-ir-test
   build-depends:
     , base                                                       >=4.9   && <5
     , containers
+    , data-default-class
     , flat                                                       ^>=0.6
     , hashable
     , hedgehog
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs b/plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs
index f0eccd91ac6..537e230a9bc 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs
@@ -1,22 +1,22 @@
-{-# LANGUAGE GADTs            #-}
-{-# LANGUAGE KindSignatures   #-}
-{-# LANGUAGE RankNTypes       #-}
-{-# LANGUAGE TemplateHaskell  #-}
-{-# LANGUAGE TypeApplications #-}
-module PlutusIR.Analysis.Builtins (
-  BuiltinMatcherLike (..),
-  bmlSplitMatchContext,
-  bmlBranchArities,
-  defaultUniMatcherLike,
-
-  BuiltinsInfo (..),
-  biSemanticsVariant,
-  biMatcherLike,
-
-  builtinArityInfo,
-
-  asBuiltinDatatypeMatch,
-  builtinDatatypeMatchBranchArities) where
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE KindSignatures    #-}
+{-# LANGUAGE PatternSynonyms   #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TemplateHaskell   #-}
+{-# LANGUAGE TypeApplications  #-}
+module PlutusIR.Analysis.Builtins
+    ( BuiltinMatcherLike (..)
+    , bmlSplitMatchContext
+    , bmlBranchArities
+    , defaultUniMatcherLike
+    , BuiltinsInfo (..)
+    , biSemanticsVariant
+    , biMatcherLike
+    , builtinArityInfo
+    , asBuiltinDatatypeMatch
+    , builtinDatatypeMatchBranchArities
+    ) where
 
 import Control.Lens hiding (parts)
 import Data.Functor (void)
@@ -44,11 +44,13 @@ data BuiltinsInfo (uni :: Type -> Type) fun = BuiltinsInfo
   { _biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun
   , _biMatcherLike      :: Map.Map fun (BuiltinMatcherLike uni fun)
   }
-
 makeLenses ''BuiltinsInfo
 
-instance (Ord fun, Default (BuiltinSemanticsVariant fun)) => Default (BuiltinsInfo uni fun) where
-  def = BuiltinsInfo def mempty
+instance Default (BuiltinsInfo DefaultUni DefaultFun) where
+  def = BuiltinsInfo
+        { _biSemanticsVariant = def
+        , _biMatcherLike = defaultUniMatcherLike
+        }
 
 -- | Get the arity of a builtin function from the 'PLC.BuiltinInfo'.
 builtinArityInfo
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
index 43a211683ef..a1765ecdd7b 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
@@ -27,6 +27,7 @@ module PlutusIR.Compiler (
     coDoSimplifierInline,
     coDoSimplifierEvaluateBuiltins,
     coDoSimplifierStrictifyBindings,
+    coDoSimplifierRewrite,
     coInlineHints,
     coProfile,
     coRelaxedFloatin,
@@ -58,7 +59,6 @@ import PlutusIR.Error
 import PlutusIR.Transform.Beta qualified as Beta
 import PlutusIR.Transform.CaseOfCase qualified as CaseOfCase
 import PlutusIR.Transform.CaseReduce qualified as CaseReduce
-import PlutusIR.Transform.CommuteFnWithConst qualified as CommuteFnWithConst
 import PlutusIR.Transform.DeadCode qualified as DeadCode
 import PlutusIR.Transform.EvaluateBuiltins qualified as EvaluateBuiltins
 import PlutusIR.Transform.Inline.Inline qualified as Inline
@@ -69,6 +69,7 @@ import PlutusIR.Transform.LetMerge qualified as LetMerge
 import PlutusIR.Transform.NonStrict qualified as NonStrict
 import PlutusIR.Transform.RecSplit qualified as RecSplit
 import PlutusIR.Transform.Rename ()
+import PlutusIR.Transform.RewriteRules qualified as RewriteRules
 import PlutusIR.Transform.StrictifyBindings qualified as StrictifyBindings
 import PlutusIR.Transform.ThunkRecursions qualified as ThunkRec
 import PlutusIR.Transform.Unwrap qualified as Unwrap
@@ -140,7 +141,9 @@ availablePasses =
                                                                                   binfo <- view ccBuiltinsInfo
                                                                                   Inline.inline hints binfo t
                                                                               )
-    , Pass "commuteFnWithConst" (onOption coDoSimplifiercommuteFnWithConst) (pure . CommuteFnWithConst.commuteFnWithConst)
+    , Pass "rewrite rules" (onOption coDoSimplifierRewrite) (\ t -> do
+                                                                    rules <- view ccRewriteRules
+                                                                    RewriteRules.userRewrite rules t)
     ]
 
 -- | Actual simplifier
@@ -150,11 +153,12 @@ simplify
 simplify = foldl' (>=>) pure (map applyPass availablePasses)
 
 -- | Perform some simplification of a 'Term'.
+--
+-- NOTE: simplifyTerm requires at least 1 prior dead code elimination pass
 simplifyTerm
   :: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
   => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
 simplifyTerm = runIfOpts simplify'
-    -- NOTE: we need at least one pass of dead code elimination
     where
         simplify' :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
         simplify' t = do
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
index a826ec4611a..b19231540ab 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
@@ -27,6 +27,7 @@ import PlutusCore.Quote
 import PlutusCore.StdLib.Type qualified as Types
 import PlutusCore.TypeCheck.Internal qualified as PLC
 import PlutusCore.Version qualified as PLC
+import PlutusIR.Transform.RewriteRules
 import PlutusPrelude
 
 import Control.Monad.Error.Lens (throwing)
@@ -74,29 +75,29 @@ defaultDatatypeCompilationOpts :: DatatypeCompilationOpts
 defaultDatatypeCompilationOpts = DatatypeCompilationOpts SumsOfProducts
 
 data CompilationOpts a = CompilationOpts {
-    _coOptimize                         :: Bool
-    , _coPedantic                       :: Bool
-    , _coVerbose                        :: Bool
-    , _coDebug                          :: Bool
-    , _coDatatypes                      :: DatatypeCompilationOpts
+    _coOptimize                        :: Bool
+    , _coPedantic                      :: Bool
+    , _coVerbose                       :: Bool
+    , _coDebug                         :: Bool
+    , _coDatatypes                     :: DatatypeCompilationOpts
     -- Simplifier passes
-    , _coMaxSimplifierIterations        :: Int
-    , _coDoSimplifierUnwrapCancel       :: Bool
-    , _coDoSimplifierCaseReduce         :: Bool
-    , _coDoSimplifiercommuteFnWithConst :: Bool
-    , _coDoSimplifierBeta               :: Bool
-    , _coDoSimplifierInline             :: Bool
-    , _coDoSimplifierKnownCon           :: Bool
-    , _coDoSimplifierCaseOfCase         :: Bool
-    , _coDoSimplifierEvaluateBuiltins   :: Bool
-    , _coDoSimplifierStrictifyBindings  :: Bool
-    , _coInlineHints                    :: InlineHints PLC.Name (Provenance a)
+    , _coMaxSimplifierIterations       :: Int
+    , _coDoSimplifierUnwrapCancel      :: Bool
+    , _coDoSimplifierCaseReduce        :: Bool
+    , _coDoSimplifierRewrite           :: Bool
+    , _coDoSimplifierBeta              :: Bool
+    , _coDoSimplifierInline            :: Bool
+    , _coDoSimplifierKnownCon          :: Bool
+    , _coDoSimplifierCaseOfCase        :: Bool
+    , _coDoSimplifierEvaluateBuiltins  :: Bool
+    , _coDoSimplifierStrictifyBindings :: Bool
+    , _coInlineHints                   :: InlineHints PLC.Name (Provenance a)
     -- Profiling
-    , _coProfile                        :: Bool
-    , _coRelaxedFloatin                 :: Bool
-    , _coCaseOfCaseConservative         :: Bool
+    , _coProfile                       :: Bool
+    , _coRelaxedFloatin                :: Bool
+    , _coCaseOfCaseConservative        :: Bool
     -- | Whether to try and preserve the logging beahviour of the program.
-    , _coPreserveLogging                :: Bool
+    , _coPreserveLogging               :: Bool
     } deriving stock (Show)
 
 makeLenses ''CompilationOpts
@@ -111,7 +112,7 @@ defaultCompilationOpts = CompilationOpts
   , _coMaxSimplifierIterations = 12
   , _coDoSimplifierUnwrapCancel = True
   , _coDoSimplifierCaseReduce = True
-  , _coDoSimplifiercommuteFnWithConst = True
+  , _coDoSimplifierRewrite = True
   , _coDoSimplifierKnownCon = True
   , _coDoSimplifierCaseOfCase = True
   , _coDoSimplifierBeta = True
@@ -132,12 +133,13 @@ data CompilationCtx uni fun a = CompilationCtx {
     , _ccTypeCheckConfig  :: Maybe (PirTCConfig uni fun)
     , _ccBuiltinsInfo     :: BuiltinsInfo uni fun
     , _ccBuiltinCostModel :: PLC.CostingPart uni fun
+    , _ccRewriteRules     :: RewriteRules uni fun
     }
 
 makeLenses ''CompilationCtx
 
 toDefaultCompilationCtx
-    :: (Ord fun, Default (PLC.BuiltinSemanticsVariant fun), Default (PLC.CostingPart uni fun))
+    :: (Default (BuiltinsInfo uni fun), Default (PLC.CostingPart uni fun), Default (RewriteRules uni fun))
     => PLC.TypeCheckConfig uni fun
     -> CompilationCtx uni fun a
 toDefaultCompilationCtx configPlc =
@@ -145,6 +147,7 @@ toDefaultCompilationCtx configPlc =
         (Just $ PirTCConfig configPlc YesEscape)
         def
         def
+        def
 
 validateOpts :: Compiling m e uni fun a => PLC.Version -> m ()
 validateOpts v = do
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Subst.hs b/plutus-core/plutus-ir/src/PlutusIR/Subst.hs
index e842dbf0daa..a605605bbd5 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Subst.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Subst.hs
@@ -129,7 +129,6 @@ funRes f = \case
   TyFun a dom cod -> TyFun a dom <$> funRes f cod
   t               -> f t
 
--- 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
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs
new file mode 100644
index 00000000000..e24c3bcb0d8
--- /dev/null
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TypeOperators     #-}
+module PlutusIR.Transform.RewriteRules
+    ( userRewrite
+    , RewriteRules (..)
+    , defaultUniRewriteRules
+    ) where
+
+import PlutusCore.Default
+import PlutusCore.Name
+import PlutusCore.Quote
+import PlutusIR as PIR
+import PlutusIR.Analysis.VarInfo
+import PlutusIR.Transform.RewriteRules.CommuteFnWithConst
+import PlutusPrelude
+
+import Control.Lens
+
+
+-- | Rewrite a `Term` using the given `RewriteRules` (similar to functions of Term -> Term)
+-- Normally the rewrite rules are configured at entrypoint time of the compiler.
+userRewrite :: ( Semigroup a, t ~ Term tyname name uni fun a
+              , HasUnique name TermUnique
+              , HasUnique tyname TypeUnique
+              , MonadQuote m
+              )
+            => RewriteRules uni fun
+            -> t
+            -> m t
+userRewrite (RewriteRules rules) t =
+    -- 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.
+    let vinfo = termVarInfo t
+    in transformMOf termSubterms (rules vinfo) t
+
+-- | A bundle of composed `RewriteRules`, to be passed at entrypoint of the compiler.
+newtype RewriteRules uni fun = RewriteRules {
+    unRewriteRules :: forall tyname name m a
+                   . (MonadQuote m, Semigroup a)
+                   => VarsInfo tyname name uni a
+                   -> PIR.Term tyname name uni fun a
+                   -> m (PIR.Term tyname name uni fun a)
+    }
+
+-- | The rules for the Default Universe/Builtin.
+defaultUniRewriteRules :: RewriteRules DefaultUni DefaultFun
+defaultUniRewriteRules = RewriteRules $ \ _vinfo ->
+        -- The rules are composed from left to right.
+        pure . commuteFnWithConst
+        -- FIXME: Unfortunately, unicode text is currently broken (at least on plutus-tx level), so
+        -- we disable this rewrite until fix is in and further tested. See PLT-8314
+        -- >=> pure . decodeEncodeUtf8
+
+instance Default (RewriteRules DefaultUni DefaultFun) where
+  def = defaultUniRewriteRules
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/CommuteFnWithConst.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/CommuteFnWithConst.hs
similarity index 78%
rename from plutus-core/plutus-ir/src/PlutusIR/Transform/CommuteFnWithConst.hs
rename to plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/CommuteFnWithConst.hs
index 8b2e2cfc24c..8615ac016c7 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/CommuteFnWithConst.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/CommuteFnWithConst.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE GADTs            #-}
-{-# LANGUAGE LambdaCase       #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs         #-}
+{-# LANGUAGE LambdaCase    #-}
+{-# LANGUAGE TypeOperators #-}
 
 {- | Commute such that constants are the first arguments. Consider:
 
@@ -28,63 +28,52 @@ might expect that `equalsInteger` is the one that will benefit the most.
 Plutonomy only commutes `EqualsInteger` in their `commEquals`.
 -}
 
-module PlutusIR.Transform.CommuteFnWithConst
-  (commuteFnWithConst
-  , commuteDefaultFun)
-  where
+module PlutusIR.Transform.RewriteRules.CommuteFnWithConst
+    ( commuteFnWithConst
+    ) where
 
-import Control.Lens (over)
-import Data.Typeable (Typeable, eqT)
 import PlutusCore.Default
-import PlutusIR.Core.Plated (termSubterms)
 import PlutusIR.Core.Type (Term (Apply, Builtin, Constant))
 
 isConstant :: Term tyname name uni fun a -> Bool
-isConstant Constant{} = True
-isConstant _          = False
-
-commuteDefaultFun ::
-    forall tyname name uni a.
-    Term tyname name uni DefaultFun a ->
-    Term tyname name uni DefaultFun a
-commuteDefaultFun = over termSubterms commuteDefaultFun . localCommute
-  where
-    localCommute tm@(Apply ann (Apply ann1 (Builtin annB fun) x) y@Constant{})
-      | isCommutative fun && not (isConstant x) =
-          Apply ann (Apply ann1 (Builtin annB fun) y) x
-      | otherwise                   = tm
-    localCommute tm = tm
-
-commuteFnWithConst :: forall tyname name uni fun a. Typeable fun =>
-    Term tyname name uni fun a -> Term tyname name uni fun a
-commuteFnWithConst = case eqT @fun @DefaultFun of
-    Just Refl -> commuteDefaultFun
-    Nothing   -> id
+isConstant = \case
+    Constant{} -> True
+    _          -> False
+
+commuteFnWithConst :: (t ~ Term tyname name uni DefaultFun a) => t -> t
+commuteFnWithConst = \case
+    Apply ann1 (Apply ann2 (Builtin ann3 fun) arg1) arg2
+        | isCommutative fun
+        , not (isConstant arg1)
+        , isConstant arg2
+        -> Apply ann1 (Apply ann2 (Builtin ann3 fun) arg2) arg1
+    t -> t
 
 -- | Returns whether a `DefaultFun` is commutative. Not using
 -- catchall to make sure that this function catches newly added `DefaultFun`.
 isCommutative :: DefaultFun -> Bool
 isCommutative = \case
   AddInteger                      -> True
-  SubtractInteger                 -> False
   MultiplyInteger                 -> True
+  EqualsInteger                   -> True
+  EqualsByteString                -> True
+  EqualsString                    -> True
+  EqualsData                      -> True
+  -- verbose laid down, to revisit this function if a new builtin is added
+  SubtractInteger                 -> False
   DivideInteger                   -> False
   QuotientInteger                 -> False
   RemainderInteger                -> False
   ModInteger                      -> False
-  EqualsInteger                   -> True
   LessThanInteger                 -> False
   LessThanEqualsInteger           -> False
-    -- Bytestrings
   AppendByteString                -> False
   ConsByteString                  -> False
   SliceByteString                 -> False
   LengthOfByteString              -> False
   IndexByteString                 -> False
-  EqualsByteString                -> True
   LessThanByteString              -> False
   LessThanEqualsByteString        -> False
-    -- Cryptography and hashes
   Sha2_256                        -> False
   Sha3_256                        -> False
   Blake2b_224                     -> False
@@ -110,27 +99,19 @@ isCommutative = \case
   Bls12_381_millerLoop            -> False
   Bls12_381_mulMlResult           -> False
   Bls12_381_finalVerify           -> False
-    -- Strings
   AppendString                    -> False
-  EqualsString                    -> True
   EncodeUtf8                      -> False
   DecodeUtf8                      -> False
-    -- Bool
   IfThenElse                      -> False
-    -- Unit
   ChooseUnit                      -> False
-    -- Tracing
   Trace                           -> False
-    -- Pairs
   FstPair                         -> False
   SndPair                         -> False
-    -- Lists
   ChooseList                      -> False
   MkCons                          -> False
   HeadList                        -> False
   TailList                        -> False
   NullList                        -> False
-    -- Data
   ChooseData                      -> False
   ConstrData                      -> False
   MapData                         -> False
@@ -142,7 +123,6 @@ isCommutative = \case
   UnListData                      -> False
   UnIData                         -> False
   UnBData                         -> False
-  EqualsData                      -> True
   SerialiseData                   -> False
   MkPairData                      -> False
   MkNilData                       -> False
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs
new file mode 100644
index 00000000000..0b8f4c8a76e
--- /dev/null
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/DecodeEncodeUtf8.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeOperators   #-}
+
+module PlutusIR.Transform.RewriteRules.DecodeEncodeUtf8
+  ( decodeEncodeUtf8
+  ) where
+
+
+import PlutusCore.Default
+import PlutusIR
+
+{- | 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>)
+, or x is bottom.
+
+The opposite rewrite `(encodeUtf8 (decodeUtf8 x)) => x` is definitely not safe.
+-}
+-- FIXME: Unfortunately, unicode text is currently broken (at least on plutus-tx level), so
+-- we disable this rewrite until fix is in and further tested. See PLT-8314
+decodeEncodeUtf8 :: (Semigroup a, t ~ Term tyname name uni DefaultFun a) => t -> t
+decodeEncodeUtf8 = \case
+    BA DecodeUtf8 a1 a2 (BA EncodeUtf8 a3 a4 t) ->
+        -- place the missed annotations inside the rewritten term
+        (<> a1 <> a2 <> a3 <> a4) <$> t
+    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
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs
index 6c2ea97ddbb..1d086cd8465 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs
@@ -6,7 +6,6 @@ import PlutusIR.Generators.AST
 import PlutusIR.Mark
 import PlutusIR.Transform.Beta
 import PlutusIR.Transform.CaseReduce
-import PlutusIR.Transform.CommuteFnWithConst
 import PlutusIR.Transform.DeadCode
 import PlutusIR.Transform.EvaluateBuiltins
 import PlutusIR.Transform.Inline.Inline qualified as Inline
@@ -16,6 +15,7 @@ import PlutusIR.Transform.LetMerge
 import PlutusIR.Transform.NonStrict
 import PlutusIR.Transform.RecSplit
 import PlutusIR.Transform.Rename
+import PlutusIR.Transform.RewriteRules.CommuteFnWithConst
 import PlutusIR.Transform.ThunkRecursions
 import PlutusIR.Transform.Unwrap
 
@@ -32,8 +32,8 @@ test_names = testGroup "names"
         pure . beta
     , T.test_scopingGood "case-of-known-constructor" genTerm T.BindingRemovalNotOk T.PrerenameYes $
         pure . caseReduce
-    , T.test_scopingGood "'commuteDefaultFun'" genTerm T.BindingRemovalNotOk T.PrerenameYes $
-        pure . commuteDefaultFun
+    , T.test_scopingGood "commuteFnWithConst" genTerm T.BindingRemovalNotOk T.PrerenameYes $
+        pure . commuteFnWithConst
     , -- We say that it's fine to remove bindings, because they never actually get removed,
       -- because the scope checking machinery doesn't create unused bindings, every binding
       -- gets referenced at some point at least once (usually very close to the binding site).
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs
index a4478a8f16e..e02af1a2c68 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs
@@ -4,6 +4,7 @@ module PlutusIR.Transform.CaseOfCase.Tests where
 import Test.Tasty
 import Test.Tasty.Extras
 
+import Control.Lens
 import PlutusCore qualified as PLC
 import PlutusCore.Name
 import PlutusCore.Quote
@@ -26,9 +27,9 @@ test_caseOfCase = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"]
             , "exponential"
             ]
     where
-      binfo = def & biMatcherLike .~ defaultUniMatcherLike
+      binfo = def & set' biMatcherLike defaultUniMatcherLike
       goldenCoCTC t = rethrow . asIfThrown @(PIR.Error PLC.DefaultUni PLC.DefaultFun ()) $ do
         let newT = runQuote $ CaseOfCase.caseOfCase binfo True mempty t
         -- make sure the floated result typechecks
         _ <- runQuoteT . flip inferType (() <$ newT) =<< TC.getDefTypeCheckConfig ()
-        pure $ newT
+        pure newT
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/Tests.hs
deleted file mode 100644
index c50262c78d9..00000000000
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/Tests.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-module PlutusIR.Transform.CommuteFnWithConst.Tests where
-
-import Test.Tasty
-import Test.Tasty.Extras
-
-import PlutusIR.Parser
-import PlutusIR.Test
-import PlutusIR.Transform.CommuteFnWithConst
-
-import PlutusIR.Properties.Typecheck
-import Test.QuickCheck.Property (Property, withMaxSuccess)
-
-test_commuteDefaultFun :: TestTree
-test_commuteDefaultFun = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
-    testNested "CommuteFnWithConst" $
-    map
-        (goldenPir commuteDefaultFun 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
-        , "let" -- this tests that it works in the subterms
-        ]
-
--- | Check that a term typechecks after a `PlutusIR.Transform.CommuteFnWithConst.commuteFnWithConst`
--- pass.
-prop_TypecheckCommuteFnWithConst :: Property
-prop_TypecheckCommuteFnWithConst =
-      withMaxSuccess 3000 (pureTypecheckProp commuteFnWithConst)
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs
index c1eb4dbdef2..c418ed5caa7 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs
@@ -14,6 +14,7 @@ import PlutusPrelude
 import Test.Tasty.ExpectedFailure (ignoreTest)
 import Test.Tasty.QuickCheck
 
+
 test_deadCode :: TestTree
 test_deadCode = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "DeadCode" $
@@ -42,7 +43,7 @@ test_deadCode = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
 typecheckRemoveDeadBindingsProp :: BuiltinSemanticsVariant DefaultFun -> Property
 typecheckRemoveDeadBindingsProp biVariant =
   withMaxSuccess 50000 $ nonPureTypecheckProp $ removeDeadBindings $
-    BuiltinsInfo biVariant defaultUniMatcherLike
+     def {_biSemanticsVariant = biVariant}
 test_TypecheckRemoveDeadBindings :: TestTree
 test_TypecheckRemoveDeadBindings =
   ignoreTest $ testProperty "typechecking" typecheckRemoveDeadBindingsProp
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs
index 357f2f47233..4d5c3a6b028 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs
@@ -33,5 +33,5 @@ prop_TypecheckEvaluateBuiltins ::
 prop_TypecheckEvaluateBuiltins conservative biVariant =
   withMaxSuccess 40000 $
     pureTypecheckProp $
-        evaluateBuiltins conservative (BuiltinsInfo biVariant defaultUniMatcherLike) def
+        evaluateBuiltins conservative (def {_biSemanticsVariant = biVariant}) def
 
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs
index 7f5c5f62802..eda1f1baee5 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs
@@ -106,4 +106,4 @@ checkUniques =
 prop_TypecheckInline :: BuiltinSemanticsVariant DefaultFun -> Property
 prop_TypecheckInline biVariant =
   withMaxSuccess 20000 $ nonPureTypecheckProp $
-    inline mempty (BuiltinsInfo biVariant defaultUniMatcherLike)
+    inline mempty (def {_biSemanticsVariant = biVariant})
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs
index f98498f5148..0e132d11169 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs
@@ -76,4 +76,4 @@ prop_TypecheckFloatTerm ::
 prop_TypecheckFloatTerm biVariant conservative =
   withMaxSuccess 40000 $
     nonPureTypecheckProp $
-      LetFloatIn.floatTerm (BuiltinsInfo biVariant defaultUniMatcherLike) conservative
+      LetFloatIn.floatTerm (def {_biSemanticsVariant = biVariant}) conservative
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs
index b3a5dddb526..a3e5f54ad92 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs
@@ -75,4 +75,4 @@ test_letFloatOut = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"
 prop_TypecheckFloatTerm :: BuiltinSemanticsVariant PLC.DefaultFun -> Property
 prop_TypecheckFloatTerm biVariant =
   withMaxSuccess 20000 $ pureTypecheckProp $
-    LetFloatOut.floatTerm (BuiltinsInfo biVariant defaultUniMatcherLike)
+    LetFloatOut.floatTerm (def { _biSemanticsVariant = biVariant})
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs
new file mode 100644
index 00000000000..0c94226ca26
--- /dev/null
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs
@@ -0,0 +1,23 @@
+module PlutusIR.Transform.RewriteRules.Tests where
+
+import PlutusCore.Quote
+import PlutusIR.Parser
+import PlutusIR.Test
+import PlutusIR.Transform.RewriteRules as RewriteRules
+
+import Data.Default.Class
+import Test.Tasty
+import Test.Tasty.Extras
+
+test_RewriteRules :: TestTree
+test_RewriteRules = runTestNestedIn ["plutus-ir/test/PlutusIR/Transform"] $
+    testNested "RewriteRules" $
+    fmap
+        (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
+        , "let" -- this tests that it works in the subterms
+        -- Disabled, see DecodeEncodeUtf8.hs
+        -- , "decodeEncodeUtf8"
+        ]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8 b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8
new file mode 100644
index 00000000000..dd010c621fc
--- /dev/null
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8
@@ -0,0 +1,5 @@
+(lam
+    x (con string) [ (builtin decodeUtf8) [ (builtin encodeUtf8)
+                   [ (builtin decodeUtf8) [ (builtin encodeUtf8) x
+                   ] ] ] ]
+)
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8.golden
new file mode 100644
index 00000000000..0775693c720
--- /dev/null
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/decodeEncodeUtf8.golden
@@ -0,0 +1 @@
+(lam x (con string) x)
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/divideInt b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/divideInt
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/divideInt
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/divideInt
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/divideInt.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/divideInt.golden
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/divideInt.golden
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/divideInt.golden
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/equalsInt b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/equalsInt
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/equalsInt
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/equalsInt
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/equalsInt.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/equalsInt.golden
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/equalsInt.golden
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/equalsInt.golden
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/let b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/let
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/let.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let.golden
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/let.golden
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let.golden
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/multiplyInt b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/multiplyInt
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/multiplyInt
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/multiplyInt
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/multiplyInt.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/multiplyInt.golden
similarity index 100%
rename from plutus-core/plutus-ir/test/PlutusIR/Transform/CommuteFnWithConst/multiplyInt.golden
rename to plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/multiplyInt.golden
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs
index cdd8d39681b..347def86720 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs
@@ -28,4 +28,4 @@ test_strictifyBindings = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Tran
 prop_TypecheckStrictifyBindings :: BuiltinSemanticsVariant DefaultFun -> Property
 prop_TypecheckStrictifyBindings biVariant =
   withMaxSuccess 5000 $
-    pureTypecheckProp (strictifyBindings (BuiltinsInfo biVariant defaultUniMatcherLike))
+    pureTypecheckProp (strictifyBindings (def {_biSemanticsVariant = biVariant}))
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs
index b8c7ccbb187..31012cd4eea 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs
@@ -32,4 +32,4 @@ test_thunkRecursions = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transf
 prop_TypecheckThunkRecursions :: BuiltinSemanticsVariant DefaultFun -> Property
 prop_TypecheckThunkRecursions biVariant =
   withMaxSuccess 5000 $ pureTypecheckProp $
-    thunkRecursions $ BuiltinsInfo biVariant defaultUniMatcherLike
+    thunkRecursions $ def {_biSemanticsVariant = biVariant}
diff --git a/plutus-core/testlib/PlutusIR/Test.hs b/plutus-core/testlib/PlutusIR/Test.hs
index b61d36aeeea..8ef3dbef538 100644
--- a/plutus-core/testlib/PlutusIR/Test.hs
+++ b/plutus-core/testlib/PlutusIR/Test.hs
@@ -31,8 +31,10 @@ import PlutusCore.Pretty qualified as PLC
 import PlutusCore.Quote (runQuoteT)
 import PlutusCore.Test hiding (ppCatch)
 import PlutusIR as PIR
+import PlutusIR.Analysis.Builtins
 import PlutusIR.Compiler as PIR
 import PlutusIR.Parser (Parser, pTerm, parse)
+import PlutusIR.Transform.RewriteRules
 import PlutusIR.TypeCheck
 import System.FilePath (joinPath, (</>))
 
@@ -53,6 +55,8 @@ instance
   , Typeable a
   , Ord a
   , Default (PLC.CostingPart uni fun)
+  , Default (BuiltinsInfo uni fun)
+  , Default (RewriteRules uni fun)
   ) =>
   ToTPlc (PIR.Program PIR.TyName PIR.Name uni fun a) uni fun
   where
@@ -67,6 +71,8 @@ instance
   , Typeable a
   , Ord a
   , Default (PLC.CostingPart uni fun)
+  , Default (BuiltinsInfo uni fun)
+  , Default (RewriteRules uni fun)
   ) =>
   ToUPlc (PIR.Program PIR.TyName PIR.Name uni fun a) uni fun
   where
@@ -93,7 +99,9 @@ compileWithOpts ::
   , PLC.PrettyUni uni
   , PLC.Pretty fun
   , PLC.Pretty a
+  , Default (BuiltinsInfo uni fun)
   , Default (PLC.CostingPart uni fun)
+  , Default (RewriteRules uni fun)
   ) =>
   (CompilationCtx uni fun a -> CompilationCtx uni fun a) ->
   PIR.Program PIR.TyName PIR.Name uni fun a ->
diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs
index f421a4edb54..13ad48441fc 100644
--- a/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs
@@ -18,6 +18,7 @@ import PlutusTx.PLCTypes
 
 import PlutusIR.Analysis.Builtins qualified as PIR
 import PlutusIR.Compiler.Definitions
+import PlutusIR.Transform.RewriteRules qualified as PIR
 
 import PlutusCore.Annotation
 import PlutusCore.Builtin qualified as PLC
@@ -60,7 +61,8 @@ data CompileContext uni fun = CompileContext {
     ccModBreaks        :: Maybe GHC.ModBreaks,
     ccBuiltinsInfo     :: PIR.BuiltinsInfo uni fun,
     ccBuiltinCostModel :: PLC.CostingPart uni fun,
-    ccDebugTraceOn     :: Bool
+    ccDebugTraceOn     :: Bool,
+    ccRewriteRules     :: PIR.RewriteRules uni fun
     }
 
 data CompileState = CompileState
diff --git a/plutus-tx-plugin/src/PlutusTx/Options.hs b/plutus-tx-plugin/src/PlutusTx/Options.hs
index 1d6c0c0df51..63d48029afb 100644
--- a/plutus-tx-plugin/src/PlutusTx/Options.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Options.hs
@@ -58,6 +58,7 @@ data PluginOptions = PluginOptions
     , _posDoSimplifierEvaluateBuiltins   :: Bool
     , _posDoSimplifierStrictifyBindings  :: Bool
     , _posDoSimplifierRemoveDeadBindings :: Bool
+    , _posDoSimplifierRewrite            :: Bool
     , _posProfile                        :: ProfileOpts
     , _posCoverageAll                    :: Bool
     , _posCoverageLocation               :: Bool
@@ -223,6 +224,9 @@ pluginOptions =
         , let k = "simplifier-remove-dead-bindings"
               desc = "Run a simplification pass that removes dead bindings"
            in (k, PluginOption typeRep (setTrue k) posDoSimplifierRemoveDeadBindings desc [])
+        , let k = "simplifier-rewrite"
+              desc = "Run a pass that performs some pre-defined rewrite rules on builtins (similar to GHC's RULES)"
+           in (k, PluginOption typeRep (setTrue k) posDoSimplifierRewrite desc [])
         , let k = "profile-all"
               desc = "Set profiling options to All, which adds tracing when entering and exiting a term."
            in (k, PluginOption typeRep (flag (const All) k) posProfile desc [])
@@ -304,6 +308,7 @@ defaultPluginOptions =
         , _posDoSimplifierEvaluateBuiltins = True
         , _posDoSimplifierStrictifyBindings = True
         , _posDoSimplifierRemoveDeadBindings = True
+        , _posDoSimplifierRewrite = True
         , _posProfile = None
         , _posCoverageAll = False
         , _posCoverageLocation = False
diff --git a/plutus-tx-plugin/src/PlutusTx/Plugin.hs b/plutus-tx-plugin/src/PlutusTx/Plugin.hs
index 9c3c49c17ec..71dcf80f819 100644
--- a/plutus-tx-plugin/src/PlutusTx/Plugin.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Plugin.hs
@@ -81,6 +81,7 @@ import Data.Set qualified as Set
 import GHC.Num.Integer qualified
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Compiler.Provenance (noProvenance, original)
+import PlutusIR.Transform.RewriteRules
 import Prettyprinter qualified as PP
 import System.IO (openTempFile)
 import System.IO.Unsafe (unsafePerformIO)
@@ -407,9 +408,10 @@ compileMarkedExpr locStr codeTy origE = do
             ccBlackholed = mempty,
             ccCurDef = Nothing,
             ccModBreaks = modBreaks,
-            ccBuiltinsInfo = (def & biMatcherLike .~ defaultUniMatcherLike),
+            ccBuiltinsInfo = def,
             ccBuiltinCostModel = def,
-            ccDebugTraceOn = _posDumpCompilationTrace opts
+            ccDebugTraceOn = _posDumpCompilationTrace opts,
+            ccRewriteRules = def
             }
         st = CompileState 0 mempty
     -- See Note [Occurrence analysis]
@@ -492,6 +494,8 @@ runCompiler moduleName opts expr = do
                     (opts ^. posDoSimplifierEvaluateBuiltins)
                  & set (PIR.ccOpts . PIR.coDoSimplifierStrictifyBindings)
                     (opts ^. posDoSimplifierStrictifyBindings)
+                 & set (PIR.ccOpts . PIR.coDoSimplifierRewrite)
+                    (opts ^. posDoSimplifierRewrite)
                  & set (PIR.ccOpts . PIR.coInlineHints)                    hints
                  & set (PIR.ccOpts . PIR.coRelaxedFloatin) (opts ^. posRelaxedFloatin)
                  & set (PIR.ccOpts . PIR.coCaseOfCaseConservative)
@@ -505,7 +509,7 @@ runCompiler moduleName opts expr = do
                     (if plcVersion < PLC.plcVersion110
                         then PIR.ScottEncoding else PIR.SumsOfProducts)
                  -- TODO: ensure the same as the one used in the plugin
-                 & set PIR.ccBuiltinsInfo (def & biMatcherLike .~ defaultUniMatcherLike)
+                 & set PIR.ccBuiltinsInfo def
                  & set PIR.ccBuiltinCostModel def
         plcOpts = PLC.defaultCompilationOpts
             & set (PLC.coSimplifyOpts . UPLC.soMaxSimplifierIterations)
diff --git a/plutus-tx/src/PlutusTx/Lift.hs b/plutus-tx/src/PlutusTx/Lift.hs
index 7e3f9a504a8..12481aff701 100644
--- a/plutus-tx/src/PlutusTx/Lift.hs
+++ b/plutus-tx/src/PlutusTx/Lift.hs
@@ -26,10 +26,12 @@ import PlutusTx.Lift.TH (LiftError (..), makeLift, makeTypeable)
 
 import PlutusIR
 import PlutusIR qualified as PIR
+import PlutusIR.Analysis.Builtins as PIR
 import PlutusIR.Compiler
 import PlutusIR.Compiler.Definitions
 import PlutusIR.Error qualified as PIR
 import PlutusIR.MkPir qualified as PIR
+import PlutusIR.Transform.RewriteRules as PIR
 
 import PlutusCore qualified as PLC
 import PlutusCore.Builtin qualified as PLC
@@ -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)
        )
     => PLC.Version -> a -> m (PIR.Term PLC.TyName PLC.Name uni fun (), UPLC.Term UPLC.NamedDeBruijn uni fun ())
 safeLift v x = do
@@ -91,6 +95,8 @@ safeLiftProgram
        , PLC.Typecheckable uni fun
        , PrettyUni uni, Pretty fun
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => PLC.Version -> a -> m (PIR.Program PLC.TyName PLC.Name uni fun (), UPLC.Program UPLC.NamedDeBruijn uni fun ())
 safeLiftProgram v x = bimap (PIR.Program () v) (UPLC.Program () v) <$> safeLift v x
@@ -104,6 +110,8 @@ safeLiftCode
        , PLC.Typecheckable uni fun
        , PrettyUni uni, Pretty fun
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => PLC.Version -> a -> m (CompiledCodeIn uni fun a)
 safeLiftCode v =
@@ -126,6 +134,8 @@ unsafely ma = runQuote $ do
 lift
     :: ( Lift.Lift uni a, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun, PLC.GEq uni
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => PLC.Version -> a -> (PIR.Term PLC.TyName PLC.Name uni fun (), UPLC.Term UPLC.NamedDeBruijn uni fun ())
 lift v a = unsafely $ safeLift v a
@@ -134,6 +144,8 @@ lift v a = unsafely $ safeLift v a
 liftProgram
     :: ( Lift.Lift uni a, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun, PLC.GEq uni
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => PLC.Version -> a -> (PIR.Program PLC.TyName PLC.Name uni fun (), UPLC.Program UPLC.NamedDeBruijn uni fun ())
 liftProgram v x = unsafely $ safeLiftProgram v x
@@ -148,6 +160,8 @@ liftProgramDef = liftProgram PLC.latestVersion
 liftCode
     :: ( Lift.Lift uni a, PLC.GEq uni, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => PLC.Version -> a -> CompiledCodeIn uni fun a
 liftCode v x = unsafely $ safeLiftCode v x
@@ -156,6 +170,8 @@ liftCode v x = unsafely $ safeLiftCode v x
 liftCodeDef
     :: ( Lift.Lift uni a, PLC.GEq uni, ThrowableBuiltins uni fun, PLC.Typecheckable uni fun
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => a -> CompiledCodeIn uni fun a
 liftCodeDef = liftCode PLC.latestVersion
@@ -184,6 +200,8 @@ typeCheckAgainst
        , PLC.Typecheckable uni fun
        , PrettyUni uni, Pretty fun
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => Proxy a
     -> PLC.Program PLC.TyName PLC.Name uni fun ()
@@ -226,6 +244,8 @@ typeCode
        , PLC.Typecheckable uni fun
        , PrettyUni uni, Pretty fun
        , Default (PLC.CostingPart uni fun)
+       , Default (PIR.BuiltinsInfo uni fun)
+       , Default (PIR.RewriteRules uni fun)
        )
     => Proxy a
     -> PLC.Program PLC.TyName PLC.Name uni fun ()
diff --git a/plutus-tx/testlib/PlutusTx/Test.hs b/plutus-tx/testlib/PlutusTx/Test.hs
index 921eed4c464..6882c45a4a9 100644
--- a/plutus-tx/testlib/PlutusTx/Test.hs
+++ b/plutus-tx/testlib/PlutusTx/Test.hs
@@ -51,8 +51,10 @@ import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC
 import PlutusCore.Pretty
 import PlutusCore.Pretty qualified as PLC
 import PlutusCore.Test
+import PlutusIR.Analysis.Builtins as PIR
 import PlutusIR.Core.Type (progTerm)
 import PlutusIR.Test ()
+import PlutusIR.Transform.RewriteRules as PIR
 import PlutusPrelude
 import PlutusTx.Code (CompiledCode, CompiledCodeIn, getPir, getPirNoAnn, getPlcNoAnn, sizePlc)
 import UntypedPlutusCore qualified as UPLC
@@ -181,6 +183,8 @@ instance
   , uni `PLC.Everywhere` Flat
   , Flat fun
   , Default (PLC.CostingPart uni fun)
+  , Default (PIR.BuiltinsInfo uni fun)
+  , Default (PIR.RewriteRules uni fun)
   ) =>
   ToTPlc (CompiledCodeIn uni fun a) uni fun
   where