IntersectMBO · ana-pantilie · Apr 8, 2026 · Apr 9, 2026 · Apr 14, 2026 · Apr 15, 2026
diff --git a/doc/docusaurus/docs/delve-deeper/plinth-compiler-options.md b/doc/docusaurus/docs/delve-deeper/plinth-compiler-options.md
@@ -22,6 +22,7 @@ For each boolean option, you can add a `no-` prefix to switch it off, such as `n
 |-|-|-|-|
 |`apply-to-case`|Bool|True|Run the apply-to-case pass, turning multi-argument applications into case-constr form.|
 |`certify`|Maybe [Char]||Produce a certificate for the compiled program, with the given name. This certificate provides evidence that the compiler optimizations have preserved the functional behavior of the original program. Currently, this is only supported for the UPLC compilation pipeline.|
+|`certified-opts-only`|Bool|False|Run only those optimisation passes which are certified to preserve the functional behavior of the original program.|
 |`conservative-optimisation`|Bool|False|When conservative optimisation is used, only the optimisations that never make the program worse (in terms of cost or size) are employed. Implies `no-relaxed-float-in`, `no-inline-constants`, `no-inline-fix`, `no-simplifier-evaluate-builtins`, and `preserve-logging`.|
 |`context-level`|Int|1|Set context level for error messages.|
 |`coverage-all`|Bool|False|Add all available coverage annotations in the trace output|

diff --git a/plutus-benchmark/certifier/bench/Main.hs b/plutus-benchmark/certifier/bench/Main.hs
@@ -5,7 +5,7 @@ import Control.DeepSeq (force)
 import Control.Exception (evaluate)
 import Control.Monad
 import Criterion.Main
-import FFI.SimplifierTrace
+import FFI.OptimizerTrace
 import FFI.Untyped (UTerm)
 import MAlonzo.Code.Certifier (runCertifierMain)
 

diff --git a/plutus-benchmark/certifier/src/Certifier/Common.hs b/plutus-benchmark/certifier/src/Certifier/Common.hs
@@ -4,10 +4,11 @@ import Control.Lens ((&), (.~))
 import Control.Monad.Trans.Except
 import Data.ByteString qualified as B
 import Data.ByteString.Short qualified as SBS
-import FFI.SimplifierTrace
+import FFI.OptimizerTrace
 import FFI.Untyped (UTerm)
 import PlutusBenchmark.Common (getDataDir)
 import PlutusCore.Default.Builtins
+import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultBuiltinCostModelForTesting)
 import PlutusCore.Quote
 import PlutusLedgerApi.Common
 import System.FilePath
@@ -32,21 +33,22 @@ loadFrom name = do
           . runQuote
           . runExceptT
           $ UPLC.unDeBruijnTerm (UPLC._progTerm prog)
-  pure . runQuote $ mkFfiSimplifierTrace . snd <$> simplify term
+  pure . runQuote $ mkFfiOptimizerTrace . snd <$> simplify term
 
 simplify
   :: Term Name DefaultUni DefaultFun ()
   -> Quote
        ( Term Name DefaultUni DefaultFun ()
-       , SimplifierTrace Name DefaultUni DefaultFun ()
+       , OptimizerTrace Name DefaultUni DefaultFun ()
        )
 simplify =
-  runSimplifierT
-    . termSimplifier
-      ( defaultSimplifyOpts
-          & soPreserveLogging .~ False
+  runOptimizerT
+    . termOptimizer
+      ( defaultOptimizeOpts
+          & ooPreserveLogging .~ False
       )
       DefaultFunSemanticsVariantE
+      defaultBuiltinCostModelForTesting
 
 testScripts :: [FilePath]
 testScripts =

diff --git a/plutus-benchmark/certifier/test/Main.hs b/plutus-benchmark/certifier/test/Main.hs
@@ -4,7 +4,7 @@ import Certifier.Common (loadFrom, testScripts)
 import Control.DeepSeq (force)
 import Control.Exception (evaluate)
 import Control.Monad
-import FFI.SimplifierTrace
+import FFI.OptimizerTrace
 import FFI.Untyped (UTerm)
 import MAlonzo.Code.Certifier (runCertifierMain)
 import Test.Tasty (defaultMain, testGroup)

diff --git a/plutus-core/changelog.d/20260415_215659_ana.pantilie95_safe_opt_mode.md b/plutus-core/changelog.d/20260415_215659_ana.pantilie95_safe_opt_mode.md
@@ -0,0 +1,3 @@
+### Added
+
+- Added a new command line option `--certified-opts-only` which disables those optimization passes which are not certified.
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
@@ -230,12 +230,13 @@ library
     UntypedPlutusCore.Transform.Certify.Hints
     UntypedPlutusCore.Transform.Certify.Trace
     UntypedPlutusCore.Transform.Cse
+    UntypedPlutusCore.Transform.EvaluateBuiltins
     UntypedPlutusCore.Transform.FloatDelay
     UntypedPlutusCore.Transform.ForceCaseDelay
     UntypedPlutusCore.Transform.ForceDelay
     UntypedPlutusCore.Transform.Inline
     UntypedPlutusCore.Transform.LetFloatOut
-    UntypedPlutusCore.Transform.Simplifier
+    UntypedPlutusCore.Transform.Optimizer
 
   other-modules:
     Data.Aeson.Flatten
@@ -289,8 +290,8 @@ library
     UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode
     UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode
     UntypedPlutusCore.Evaluation.Machine.CommonAPI
-    UntypedPlutusCore.Simplify
-    UntypedPlutusCore.Simplify.Opts
+    UntypedPlutusCore.Optimize
+    UntypedPlutusCore.Optimize.Opts
     UntypedPlutusCore.Subst
 
   reexported-modules: Data.SatInt
@@ -479,6 +480,7 @@ library untyped-plutus-core-testlib
     Generators.Spec
     Scoping.Spec
     Transform.CaseOfCase.Spec
+    Transform.EvaluateBuiltins.Spec
     Transform.Inline.Spec
     Transform.Simplify.Lib
     Transform.Simplify.Spec

diff --git a/plutus-core/plutus-core/src/PlutusCore/Compiler.hs b/plutus-core/plutus-core/src/PlutusCore/Compiler.hs
@@ -5,14 +5,15 @@ module PlutusCore.Compiler
   , compileProgramWithTrace
   ) where
 
+import PlutusCore.Builtin (CostingPart)
 import PlutusCore.Compiler.Erase
 import PlutusCore.Compiler.Opts as Opts
 import PlutusCore.Compiler.Types
 import PlutusCore.Core
 import PlutusCore.Name.Unique
 import PlutusCore.Rename
 import UntypedPlutusCore.Core.Type qualified as UPLC
-import UntypedPlutusCore.Simplify qualified as UPLC
+import UntypedPlutusCore.Optimize qualified as UPLC
 
 import Control.Lens (view)
 import Control.Monad.Reader (MonadReader)
@@ -22,38 +23,42 @@ compileTerm
   :: ( Compiling m uni fun name a
      , MonadReader (CompilationOpts name fun a) m
      )
-  => Term tyname name uni fun a
+  => CostingPart uni fun
+  -> Term tyname name uni fun a
   -> m (UPLC.Term name uni fun a)
-compileTerm t = do
-  simplOpts <- view coSimplifyOpts
+compileTerm costingPart t = do
+  optimizeOpts <- view coOptimizeOpts
   builtinSemanticsVariant <- view coBuiltinSemanticsVariant
   let erased = eraseTerm t
   renamed <- rename erased
-  UPLC.simplifyTerm simplOpts builtinSemanticsVariant renamed
+  UPLC.optimizeTerm optimizeOpts builtinSemanticsVariant costingPart renamed
 
 -- | Compile a PLC program to UPLC, and optimize it.
 compileProgram
   :: ( Compiling m uni fun name a
      , MonadReader (CompilationOpts name fun a) m
      )
-  => Program tyname name uni fun a
+  => CostingPart uni fun
+  -> Program tyname name uni fun a
   -> m (UPLC.Program name uni fun a)
-compileProgram (Program a v t) = UPLC.Program a v <$> compileTerm t
+compileProgram costingPart (Program a v t) = UPLC.Program a v <$> compileTerm costingPart t
 
 {-| Compile a PLC program to UPLC, and optimize it. This includes
 the compilation trace in the result. -}
 compileProgramWithTrace
   :: ( Compiling m uni fun name a
      , MonadReader (CompilationOpts name fun a) m
      )
-  => Program tyname name uni fun a
-  -> m (UPLC.Program name uni fun a, UPLC.SimplifierTrace name uni fun a)
-compileProgramWithTrace (Program a v t) = do
-  simplOpts <- view coSimplifyOpts
+  => CostingPart uni fun
+  -> Program tyname name uni fun a
+  -> m (UPLC.Program name uni fun a, UPLC.OptimizerTrace name uni fun a)
+compileProgramWithTrace costingPart (Program a v t) = do
+  optimizeOpts <- view coOptimizeOpts
   builtinSemanticsVariant <- view coBuiltinSemanticsVariant
   let erased = eraseTerm t
   renamedProgram <- UPLC.Program a v <$> rename erased
-  UPLC.simplifyProgramWithTrace
-    simplOpts
+  UPLC.optimizeProgramWithTrace
+    optimizeOpts
     builtinSemanticsVariant
+    costingPart
     renamedProgram
diff --git a/plutus-core/plutus-core/src/PlutusCore/Compiler/Opts.hs b/plutus-core/plutus-core/src/PlutusCore/Compiler/Opts.hs
@@ -2,18 +2,18 @@
 
 module PlutusCore.Compiler.Opts
   ( CompilationOpts (..)
-  , coSimplifyOpts
+  , coOptimizeOpts
   , coBuiltinSemanticsVariant
   , defaultCompilationOpts
   ) where
 
 import Control.Lens (makeLenses)
 import Data.Default.Class (Default (def))
 import PlutusCore.Builtin.Meaning (BuiltinSemanticsVariant)
-import UntypedPlutusCore.Simplify.Opts (SimplifyOpts, defaultSimplifyOpts)
+import UntypedPlutusCore.Optimize.Opts (OptimizeOpts, defaultOptimizeOpts)
 
 data CompilationOpts name fun a = CompilationOpts
-  { _coSimplifyOpts :: SimplifyOpts name a
+  { _coOptimizeOpts :: OptimizeOpts name a
   , _coBuiltinSemanticsVariant :: BuiltinSemanticsVariant fun
   }
 
@@ -22,6 +22,6 @@ $(makeLenses ''CompilationOpts)
 defaultCompilationOpts :: Default (BuiltinSemanticsVariant fun) => CompilationOpts name fun a
 defaultCompilationOpts =
   CompilationOpts
-    { _coSimplifyOpts = defaultSimplifyOpts
+    { _coOptimizeOpts = defaultOptimizeOpts
     , _coBuiltinSemanticsVariant = def
     }
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/Tests/Lib.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictLetRec/Tests/Lib.hs
@@ -91,7 +91,7 @@ compileTplcProgramOrFail
   -> m (UPLC.Program Name DefaultUni DefaultFun ())
 compileTplcProgramOrFail plcProgram =
   handlePirErrorByFailing @SrcSpan =<< do
-    TPLC.compileProgram plcProgram
+    TPLC.compileProgram defaultBuiltinCostModelForTesting plcProgram
       & flip runReaderT TPLC.defaultCompilationOpts
       & runQuoteT
       & runExceptT

diff --git a/plutus-core/testlib/PlutusCore/Test.hs b/plutus-core/testlib/PlutusCore/Test.hs
@@ -194,14 +194,15 @@ instance
   , TPLC.GEq uni
   , TPLC.Closed uni
   , TPLC.Everywhere uni Eq
+  , Default (CostingPart uni fun)
   )
   => ToUPlc (TPLC.Program TPLC.TyName UPLC.Name uni fun ()) uni fun
   where
   toUPlc =
     pure
       . TPLC.runQuote
       . flip runReaderT TPLC.defaultCompilationOpts
-      . TPLC.compileProgram
+      . TPLC.compileProgram def
 
 instance ToUPlc (UPLC.Program UPLC.NamedDeBruijn uni fun ()) uni fun where
   toUPlc p =

diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore.hs
@@ -13,8 +13,8 @@ import UntypedPlutusCore.AstSize as Export
 import UntypedPlutusCore.Check.Scope as Export
 import UntypedPlutusCore.Core as Export
 import UntypedPlutusCore.DeBruijn as Export
+import UntypedPlutusCore.Optimize as Export
 import UntypedPlutusCore.Parser as Parser (parseScoped)
-import UntypedPlutusCore.Simplify as Export
 import UntypedPlutusCore.Subst as Export
 
 import PlutusCore.Default qualified as PLC

diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs
@@ -34,6 +34,7 @@ import PlutusPrelude
 import Data.Vector
 import PlutusCore.Builtin qualified as TPLC
 import PlutusCore.Core qualified as TPLC
+import PlutusCore.Evaluation.Machine.ExMemoryUsage (ExMemoryUsage (..))
 import PlutusCore.MkPlc
 import PlutusCore.Name.Unique qualified as TPLC
 import Universe
@@ -152,6 +153,10 @@ instance TPLC.HasConstant (Term name uni fun ()) where
 
   fromConstant = Constant ()
 
+-- See Note [ExMemoryUsage instances for non-constants].
+instance ExMemoryUsage (Term name uni fun ann) where
+  memoryUsage = Prelude.error "Internal error: 'memoryUsage' for UPLC 'Term' is not supposed to be forced"
+
 type instance TPLC.HasUniques (Term name uni fun ann) = TPLC.HasUnique name TPLC.TermUnique
 type instance TPLC.HasUniques (Program name uni fun ann) = TPLC.HasUniques (Term name uni fun ann)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		### Added

		- Added a new command line option `--certified-opts-only` which disables those optimization passes which are not certified.