Plutus compiler generates excessively large code

[savaki]

Area

[x] Plutus Foundation Related to the GHC plugin, Haskell-to-Plutus compiler, on-chain code
[] Plutus Application Framework Related to the Plutus application backend (PAB), emulator, Plutus libraries
[] Marlowe Related to Marlowe
[] Other Any other topic (Playgrounds, etc.)

Summary

Compiling to Plutus generates code that is significantly larger than the current 16k transaction size limit. The code itself has only modest responsibilities: initializing a few state values and minting tokens.

Expected behavior

Given the limited logic of the contract, our expectation was the code size would fit well within the 16k transaction size limit.

System info (please complete the following information):

• OS: ubuntu
• Version 20.04
• Plutus version - e750b7e

Additional context

The team has had a working version of the protocol running in the PAB and was looking to transition to the testnet. The issue we ran into almost immediately was the compiled size of the script. The following is a rough history of our efforts to get the script down to size:

Initial size was roughly 28k

1. Removed use of ExceptT String and replaced with error () - saved 3.5k
2. Replaced generated IsData instances with hand written serialization - saved 3k
3. Replaced use of StateMachine with hand written checks - saved 1.5k
4. Minimized constraint checks - saved 2k

At this point, it became clear to the team that something was not right. We decompiled the script to attempt to understand what was going on. Here are some observations:

• There were 3,666 instances of either delay or force. And while they're only 1 byte a pop, this adds up.
• In addition, it appears (we could be wrong on this) that there are a significant number of unused parameters (close to 2,400 at first count)

Just these two issues alone would represent over 6k or close to 40% of the entire transaction size budget.

One of our engineers came across this while scanning the plutus repo which appears seems to indicate this is a known issue, https://github.com/input-output-hk/plutus/blob/cc953b36ec9681cc28edf1accf08f48a31238e69/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs#L54

Our hope would be either the compiler be changed to generate far more efficient code or the 16k transaction size limit be raised to 32k.

[edmundnoble]

On investigating further, Delay and Force are only used to help the interpreter manage environments around polymorphic values (see the comment whose start is linked below).
https://github.com/input-output-hk/plutus/blob/cc953b36ec9681cc28edf1accf08f48a31238e69/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs#L34

I tried applying the following patch to Plutus Core, hoping it would significantly cut down size by not proliferating Scott-encoded `()`s everywhere. Not sure how it could really do that because Plutus Core's datatypes are supposed to be Scott-encoded regardless... anyway, no dice, only decreased size by ~400 bytes.

diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
index 8c6984006..7d02b2403 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
@@ -23,6 +23,7 @@ import qualified PlutusCore.StdLib.Type        as Types
 import qualified PlutusCore.TypeCheck.Internal as PLC
 
 import qualified Data.Text                     as T
+import Universe
 
 -- | Extra flag to be passed in the TypeCheckM Reader context,
 -- to signal if the PIR expression currently being typechecked is at the top-level
@@ -112,6 +113,7 @@ type Compiling m e uni fun a =
     , Ord a
     , PLC.Typecheckable uni fun
     , PLC.GEq uni
+    , uni `Includes` ()
     )
 
 type TermDef tyname name uni fun a = PLC.Def (PLC.VarDecl tyname name uni fun a) (PIR.Term tyname name uni fun a)
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs
index 33b5a7dda..3da4b415f 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeOperators     #-}
 -- | Compile non-strict bindings into strict bindings.
 module PlutusIR.Transform.NonStrict (compileNonStrictBindings) where
 
@@ -9,12 +10,13 @@ import           PlutusIR.Transform.Rename        ()
 import           PlutusIR.Transform.Substitute
 
 import           PlutusCore.Quote
-import qualified PlutusCore.StdLib.Data.ScottUnit as Unit
+import qualified PlutusCore.StdLib.Data.Unit      as Unit
 
 import           Control.Lens                     hiding (Strict)
 import           Control.Monad.State
 
 import qualified Data.Map                         as Map
+import Universe
 
 {- Note [Compiling non-strict bindings]
 Given `let x : ty = rhs in body`, we
@@ -32,19 +34,21 @@ type Substs uni fun a = Map.Map Name (Term TyName Name uni fun a)
 
 -- | Compile all the non-strict bindings in a term into strict bindings. Note: requires globally
 -- unique names.
-compileNonStrictBindings :: MonadQuote m => Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
+compileNonStrictBindings
+    :: (MonadQuote m, uni `Includes` ())
+    => Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
 compileNonStrictBindings t = do
     (t', substs) <- liftQuote $ flip runStateT mempty $ strictifyTerm t
     -- See Note [Compiling non-strict bindings]
     pure $ termSubstNames (\n -> Map.lookup n substs) t'
 
 strictifyTerm
-    :: (MonadState (Substs uni fun a) m, MonadQuote m)
+    :: (MonadState (Substs uni fun a) m, MonadQuote m, uni `Includes` ())
     => Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
 strictifyTerm = transformMOf termSubterms (traverseOf termBindings strictifyBinding)
 
 strictifyBinding
-    :: (MonadState (Substs uni fun a) m, MonadQuote m)
+    :: (MonadState (Substs uni fun a) m, MonadQuote m, uni `Includes` ())
     => Binding TyName Name uni fun a -> m (Binding TyName Name uni fun a)
 strictifyBinding = \case
     TermBind x NonStrict (VarDecl x' name ty) rhs -> do
diff --git a/plutus-tx/src/PlutusTx/Lift.hs b/plutus-tx/src/PlutusTx/Lift.hs
index 2f4bfb53a..b0f451239 100644
--- a/plutus-tx/src/PlutusTx/Lift.hs
+++ b/plutus-tx/src/PlutusTx/Lift.hs
@@ -43,6 +43,7 @@ import           Control.Monad.Reader            hiding (lift)
 import           Data.Proxy
 import           Data.Text.Prettyprint.Doc
 import qualified Data.Typeable                   as GHC
+import           Universe
 
 type Throwable uni fun =
     ( PLC.GShow uni, PLC.GEq uni, PLC.Closed uni, uni `PLC.Everywhere` PrettyConst, GHC.Typeable uni
@@ -57,6 +58,7 @@ safeLift
        , PLC.AsFreeVariableError e
        , AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m
        , PLC.Typecheckable uni fun
+       , uni `Includes` ()
        )
     => a -> m (UPLC.Term UPLC.NamedDeBruijn uni fun ())
 safeLift x = do
@@ -75,6 +77,7 @@ safeLiftProgram
        , PLC.AsFreeVariableError e
        , AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m
        , PLC.Typecheckable uni fun
+       , uni `Includes` ()
        )
     => a -> m (UPLC.Program UPLC.NamedDeBruijn uni fun ())
 safeLiftProgram x = UPLC.Program () (PLC.defaultVersion ()) <$> safeLift x
@@ -86,6 +89,7 @@ safeLiftCode
        , PLC.AsFreeVariableError e
        , AsError e uni fun (Provenance ()), MonadError e m, MonadQuote m
        , PLC.Typecheckable uni fun
+       , uni `Includes` ()
        )
     => a -> m (CompiledCodeIn uni fun a)
 safeLiftCode x = DeserializedCode <$> safeLiftProgram x <*> pure Nothing
@@ -101,13 +105,13 @@ unsafely ma = runQuote $ do
 
 -- | Get a Plutus Core term corresponding to the given value, throwing any errors that occur as exceptions and ignoring fresh names.
 lift
-    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun)
+    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun, uni `Includes` ())
     => a -> UPLC.Term UPLC.NamedDeBruijn uni fun ()
 lift a = unsafely $ safeLift a
 
 -- | Get a Plutus Core program corresponding to the given value, throwing any errors that occur as exceptions and ignoring fresh names.
 liftProgram
-    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun)
+    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun, uni `Includes` ())
     => a -> UPLC.Program UPLC.NamedDeBruijn uni fun ()
 liftProgram x = UPLC.Program () (PLC.defaultVersion ()) $ lift x
 
@@ -119,7 +123,7 @@ liftProgramDef = liftProgram
 
 -- | Get a Plutus Core program corresponding to the given value as a 'CompiledCodeIn', throwing any errors that occur as exceptions and ignoring fresh names.
 liftCode
-    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun)
+    :: (Lift.Lift uni a, Throwable uni fun, PLC.Typecheckable uni fun, uni `Includes` ())
     => a -> CompiledCodeIn uni fun a
 liftCode x = unsafely $ safeLiftCode x
 
@@ -145,6 +149,7 @@ typeCheckAgainst
        , MonadError e m, MonadQuote m
        , PLC.GEq uni
        , PLC.Typecheckable uni fun
+       , uni `Includes` ()
        )
     => Proxy a
     -> PLC.Term PLC.TyName PLC.Name uni fun ()
@@ -178,6 +183,7 @@ typeCode
        , MonadError e m, MonadQuote m
        , PLC.GEq uni
        , PLC.Typecheckable uni fun
+       , uni `Includes` ()
        )
     => Proxy a
     -> PLC.Program PLC.TyName PLC.Name uni fun ()

I also tried to just stop emitting Delay and Force, which broke the interpreter, as obviously they're there for a reason. I don't know what that reason is, but the mention of the value restriction confuses me. From what I know, there is no need for a value restriction in a language without mutation. Anyway, it dropped about 3K as the issue mentions.

Even so, we're way above the maximum transaction size, with a very simple contract. I'd have to ask if we can show you the contract in private, if you're interested. Regardless, my calculations seem to show that the Plutus code being generated is way too big for a 16KB limit:

A state machine contract with a trivial transition function (operating on PlutusTx.Data as redeemer and data to cut out serialization) is ~9KB. A minting script which does nothing but defer to a validation script is ~5KB. This leaves 2KB. The generated IsData instances for any other type of redeemer and datum are likely to be larger than that. For us, they're 4KB. This brings us 2KB over the limit without any actual logic (hand-written serialization saves us 2KB, still bringing us to the limit).

[christianschmitz]

I noticed something similar with two much simpler scripts: the AlwaysFails and AlwaysSucceeds scripts in the chris-moreton/plutus-scripts repo.

AlwaysSucceeds seems to decompile into:

(program 1.0.0 [[(Λ (Λ (Λ (Λ (Λ x5))))) (force (Λ x1))] (Λ x1)])

whereas I was expecting:

(program 1.0.0 (Λ (Λ (Λ ()))))

AlwaysFails seems to decompile into:

(program 1.0.0 [[(Λ (Λ [(Λ [(Λ (Λ (Λ (Λ [(force x4) x7])))) (force (Λ [(force x2) [(force [x3 x1]) ()]]))]) (force (Λ (error)))])) (force (Λ x1))] (Λ x1)])

whereas I was expecting:

(program 1.0.0 (Λ (Λ (Λ (error)))))

Maybe my understanding of Plutus-Core is lacking, but in that case the Plutus-Core documentation is also lacking.

[effectfully]

I've removed the bug label, because since 2021 we've done a lot to reduce the size of the compiled scripts.

We do however recognize that sizes are still far from being ideal. It is one of our objectives to further reduce script sizes, hence I've added the status: objective label.

[effectfully]

... actually, five minutes later I've found another issue that is about script sizes and has more discussion and up-to-date information, so I'm going to make that one have the status: objective label and close this one after we create two tests out of @christianschmitz's snippet.

@christianschmitz thanks a lot for reporting, those are great tests to have!

[effectfully]

close this one after we create two tests out of @christianschmitz's snippet.

The tests were added in #5394, both the cases compile as efficiently as possible when optimizations are turned on.