From 6414603b4b9f337ecc1fc3a9184833e72d033ae3 Mon Sep 17 00:00:00 2001 From: Michael Peyton Jones Date: Mon, 6 Feb 2023 13:36:05 +0000 Subject: [PATCH] Unrestricted force Don't look here yet. This is an experiment I've wanted to do for a while, just looking to get some benchmark numbers. --- .../nofib/test/formulaBudget.budget.golden | 4 +- .../nofib/test/knightsBudget.budget.golden | 4 +- .../nofib/test/queens4budget.budget.golden | 4 +- .../nofib/test/queens5budget.budget.golden | 4 +- .../test/checkScriptContext1-20.budget.golden | 4 +- .../test/checkScriptContext1-4.budget.golden | 4 +- .../test/checkScriptContext2-20.budget.golden | 4 +- .../test/checkScriptContext2-4.budget.golden | 4 +- .../test/datatypes/listMatchEval.golden | 2 +- .../plutus-ir/test/recursion/even3Eval.golden | 2 +- .../Evaluation/Machine/Cek/Internal.hs | 3 +- .../UntypedPlutusCore/Transform/ForceDelay.hs | 114 +++++++++++++++++- .../Golden/mulInstError3.uplc.golden | 4 +- .../test/Transform/extraDelays.plc.golden | 2 +- .../test/Budget/any.budget.golden | 4 +- .../test/Budget/applicative.budget.golden | 4 +- .../test/Budget/elem.budget.golden | 4 +- .../test/Budget/filter.budget.golden | 4 +- .../test/Budget/find.budget.golden | 4 +- .../test/Budget/monadicDo.budget.golden | 4 +- .../test/Budget/patternMatch.budget.golden | 4 +- .../test/Budget/show.budget.golden | 4 +- .../test/Budget/sum.budget.golden | 4 +- .../test/Budget/toFromData.budget.golden | 4 +- .../test/Optimization/maybeFun.plc.golden | 11 +- 25 files changed, 157 insertions(+), 53 deletions(-) diff --git a/plutus-benchmark/nofib/test/formulaBudget.budget.golden b/plutus-benchmark/nofib/test/formulaBudget.budget.golden index 1f07e8586e8..00d12a40081 100644 --- a/plutus-benchmark/nofib/test/formulaBudget.budget.golden +++ b/plutus-benchmark/nofib/test/formulaBudget.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 37605791908 -| mem: 161972648 +({ cpu: 36552184908 +| mem: 157391748 }) \ No newline at end of file diff --git a/plutus-benchmark/nofib/test/knightsBudget.budget.golden b/plutus-benchmark/nofib/test/knightsBudget.budget.golden index 3a9e1880585..1e8495065f3 100644 --- a/plutus-benchmark/nofib/test/knightsBudget.budget.golden +++ b/plutus-benchmark/nofib/test/knightsBudget.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 7563493298 -| mem: 28459340 +({ cpu: 7131990298 +| mem: 26583240 }) \ No newline at end of file diff --git a/plutus-benchmark/nofib/test/queens4budget.budget.golden b/plutus-benchmark/nofib/test/queens4budget.budget.golden index 8a0ff65977c..3534dda5a80 100644 --- a/plutus-benchmark/nofib/test/queens4budget.budget.golden +++ b/plutus-benchmark/nofib/test/queens4budget.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 14229364305 -| mem: 54977742 +({ cpu: 13274289305 +| mem: 50825242 }) \ No newline at end of file diff --git a/plutus-benchmark/nofib/test/queens5budget.budget.golden b/plutus-benchmark/nofib/test/queens5budget.budget.golden index caf42a8636a..4fe2fccd4a5 100644 --- a/plutus-benchmark/nofib/test/queens5budget.budget.golden +++ b/plutus-benchmark/nofib/test/queens5budget.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 191619634648 -| mem: 725849980 +({ cpu: 179471264648 +| mem: 673030980 }) \ No newline at end of file diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden index 0c88fdaa6bd..bc4c42c2906 100644 --- a/plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden +++ b/plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 492446997 -| mem: 1613269 +({ cpu: 479244997 +| mem: 1555869 }) \ No newline at end of file diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden index 0892934b216..771e2d4b222 100644 --- a/plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden +++ b/plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 141826245 -| mem: 466293 +({ cpu: 138192245 +| mem: 450493 }) \ No newline at end of file diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden index 2418271f80a..3c68d22552d 100644 --- a/plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden +++ b/plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 438942997 -| mem: 1400528 +({ cpu: 429259997 +| mem: 1358428 }) \ No newline at end of file diff --git a/plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden b/plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden index e9a8c0ebbc0..8b9d6c4ad44 100644 --- a/plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden +++ b/plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 127689877 -| mem: 410384 +({ cpu: 124998877 +| mem: 398684 }) \ No newline at end of file diff --git a/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden b/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden index 5d050430f86..70168b4a0eb 100644 --- a/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden +++ b/plutus-core/plutus-ir/test/datatypes/listMatchEval.golden @@ -1 +1 @@ -(delay (lam x_0 x_0)) \ No newline at end of file +(lam x_0 x_0) \ No newline at end of file diff --git a/plutus-core/plutus-ir/test/recursion/even3Eval.golden b/plutus-core/plutus-ir/test/recursion/even3Eval.golden index 4e8ddacc956..e583d88f65f 100644 --- a/plutus-core/plutus-ir/test/recursion/even3Eval.golden +++ b/plutus-core/plutus-ir/test/recursion/even3Eval.golden @@ -1 +1 @@ -(delay (lam case_True_0 (lam case_False_1 case_False_1))) \ No newline at end of file +(lam case_True_0 (lam case_False_1 case_False_1)) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs index 0d58e59df19..9afe367b9fe 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs @@ -702,8 +702,7 @@ enterComputeCek = computeCek (toWordArray 0) where returnCek unbudgetedSteps ctx res _ -> throwingWithCause _MachineError BuiltinTermArgumentExpectedMachineError (Just term') - forceEvaluate !_ !_ val = - throwingDischarged _MachineError NonPolymorphicInstantiationMachineError val + forceEvaluate !unbudgetedSteps !ctx val = returnCek unbudgetedSteps ctx val -- | Apply a function to an argument and proceed. -- If the function is a lambda 'lam x ty body' then extend the environment with a binding of @v@ diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/ForceDelay.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/ForceDelay.hs index 8d29fc7aeec..183fb86b950 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/ForceDelay.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/ForceDelay.hs @@ -12,5 +12,115 @@ forceDelayCancel = transformOf termSubterms processTerm processTerm :: Term name uni fun a -> Term name uni fun a processTerm = \case - Force _ (Delay _ t) -> t - t -> t + Force _ (Delay _ t) -> t + -- TODO: flag to turn this off, see + -- Note [Removing delays makes more programs succeed] + Delay _ t | canRemoveDelay t -> t + Force _ t | canRemoveForce t -> t + t -> t + +{- Note [Removing redundant delays and forces] + +We do a few transformations here. The simplest and best is to cancel out +a force/delay pair. This is a pure win, since it's exactly what the machine +would do. + +The next thing we try and do is to get rid of force/delays that are independently +pointless. In particular +- delaying something that does no work does nothing +- forcing something that cannot be a delay does nothing + +So we can remove them in those cases. + +However, there are a few wrinkles. The first is that we don't want this to +cannibalize our opportunities to do force/delay pair cancellations. Consider: + +let x = delay (\y . t) +in force x +---> (remove delay) +let x = \y . t +in force x +---> (inline) +force (\y . t) + +In this case it's fine because the term _inside_ the delay was something +that we can remove the force from around (a lambda). But we need to be +careful that this is always the case. So we require that the set of terms +that we remove delays from around be a _subset_ of the set of terms that +we remove forces from around. + +The case where this is strange is delay itself. Consider: + +let x = delay (delay [f z]) +in force (force x) +---> (remove delay) +let x = delay [f z] +in force (force x) +---> (inline) +force (force (delay [f z])) +---> (force/delay cancel) +force [f z] + +We now can't remove the last force, whereas if we had just +inlined the first thing we could have removed both by +repeated force/delay cancellation. + +So although it seems like it _should_ be fine to remove a delay +from around a delay, we don't do this for the above reason. +In practice this doesn't matter much. +-} + +{- Note [Removing delays makes more programs succeed] + +Note that removing redundant delays doesn't quite preserve the +semantics of the program! It can make some programs that would +otherwise fail succeed instead, e.g. + +let f = delay (\y. t) +in f x + +This would fail with the delay (can't apply a delay!) but will +succeed if we take it out. That makes this transformation ever +so slightly questionable, and so we should provide a flag to turn +it off. +-} + +-- | Can we remove a 'delay' from around this term? +-- +-- Broadly, this means anything that's a value, but +-- also this must be a subset of 'canRemoveForce', see +-- Note [Removing redundant delays and forces] for why. +canRemoveDelay :: Term name uni fun a -> Bool +canRemoveDelay = \case + LamAbs{} -> True + Constant{} -> True + -- You would expect this to be true, since it's a + -- value, but that would violate the subset condition. + Delay{} -> False + _ -> False + +-- | Can we remove a 'force' from around this term? +-- +-- Broadly, this means anything that we know can't turn +-- out to be a 'delay' (which would need the 'force'). +canRemoveForce :: Term name uni fun a -> Bool +canRemoveForce = \case + -- Delay is delay + Delay{} -> False + + -- Everything that computes could turn into delay + + -- A variable might be delay, we don't know + Var{} -> False + -- An application might compute to anything, including delay + Apply{} -> False + -- A force will compute to whatever's inside it, + -- which could be a delay + Force{} -> False + -- Builtins can't be delay, but they can require forcing + Builtin{} -> False + + -- Everything else can't be delay + Constant{} -> True + LamAbs{} -> True + Error{} -> True diff --git a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/mulInstError3.uplc.golden b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/mulInstError3.uplc.golden index 2f90b39bb7f..5d7bf930084 100644 --- a/plutus-core/untyped-plutus-core/test/Evaluation/Golden/mulInstError3.uplc.golden +++ b/plutus-core/untyped-plutus-core/test/Evaluation/Golden/mulInstError3.uplc.golden @@ -1,3 +1 @@ -(Left An error has occurred: error: -Attempted to instantiate a non-polymorphic term. -Caused by: (con integer 242)) \ No newline at end of file +(Right (con integer 242)) \ No newline at end of file diff --git a/plutus-core/untyped-plutus-core/test/Transform/extraDelays.plc.golden b/plutus-core/untyped-plutus-core/test/Transform/extraDelays.plc.golden index 2d9e39f20bb..132831f390c 100644 --- a/plutus-core/untyped-plutus-core/test/Transform/extraDelays.plc.golden +++ b/plutus-core/untyped-plutus-core/test/Transform/extraDelays.plc.golden @@ -1 +1 @@ -(delay (con integer 1)) \ No newline at end of file +(con integer 1) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/any.budget.golden b/plutus-tx-plugin/test/Budget/any.budget.golden index 66f8c5ab85d..d7ab6ff0301 100644 --- a/plutus-tx-plugin/test/Budget/any.budget.golden +++ b/plutus-tx-plugin/test/Budget/any.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 28136630 -| mem: 110020 +({ cpu: 26641630 +| mem: 103520 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/applicative.budget.golden b/plutus-tx-plugin/test/Budget/applicative.budget.golden index 81f5ff947d2..661f4c35df5 100644 --- a/plutus-tx-plugin/test/Budget/applicative.budget.golden +++ b/plutus-tx-plugin/test/Budget/applicative.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 2023577 -| mem: 8002 +({ cpu: 1862577 +| mem: 7302 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/elem.budget.golden b/plutus-tx-plugin/test/Budget/elem.budget.golden index 136f0ab9107..a21d97a5de3 100644 --- a/plutus-tx-plugin/test/Budget/elem.budget.golden +++ b/plutus-tx-plugin/test/Budget/elem.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 28171990 -| mem: 110020 +({ cpu: 26676990 +| mem: 103520 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/filter.budget.golden b/plutus-tx-plugin/test/Budget/filter.budget.golden index 553ad391bda..04729bbba62 100644 --- a/plutus-tx-plugin/test/Budget/filter.budget.golden +++ b/plutus-tx-plugin/test/Budget/filter.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 28773590 -| mem: 92930 +({ cpu: 27393590 +| mem: 86930 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/find.budget.golden b/plutus-tx-plugin/test/Budget/find.budget.golden index 589918740c7..ce573f797ec 100644 --- a/plutus-tx-plugin/test/Budget/find.budget.golden +++ b/plutus-tx-plugin/test/Budget/find.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 26917630 -| mem: 104720 +({ cpu: 25192630 +| mem: 97220 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/monadicDo.budget.golden b/plutus-tx-plugin/test/Budget/monadicDo.budget.golden index dd105d1dcd5..a803af59733 100644 --- a/plutus-tx-plugin/test/Budget/monadicDo.budget.golden +++ b/plutus-tx-plugin/test/Budget/monadicDo.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 2207577 -| mem: 8802 +({ cpu: 2000577 +| mem: 7902 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/patternMatch.budget.golden b/plutus-tx-plugin/test/Budget/patternMatch.budget.golden index 404ee07fbc8..d2dded65f53 100644 --- a/plutus-tx-plugin/test/Budget/patternMatch.budget.golden +++ b/plutus-tx-plugin/test/Budget/patternMatch.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 1540577 -| mem: 5902 +({ cpu: 1425577 +| mem: 5402 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/show.budget.golden b/plutus-tx-plugin/test/Budget/show.budget.golden index 54c0670c646..c74d5f3643d 100644 --- a/plutus-tx-plugin/test/Budget/show.budget.golden +++ b/plutus-tx-plugin/test/Budget/show.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 9526961630 -| mem: 35235273 +({ cpu: 8910009630 +| mem: 32552873 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/sum.budget.golden b/plutus-tx-plugin/test/Budget/sum.budget.golden index e2d90f40209..302691206dd 100644 --- a/plutus-tx-plugin/test/Budget/sum.budget.golden +++ b/plutus-tx-plugin/test/Budget/sum.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 23293870 -| mem: 92420 +({ cpu: 22028870 +| mem: 86920 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Budget/toFromData.budget.golden b/plutus-tx-plugin/test/Budget/toFromData.budget.golden index 608edcb509d..e29cc59b43a 100644 --- a/plutus-tx-plugin/test/Budget/toFromData.budget.golden +++ b/plutus-tx-plugin/test/Budget/toFromData.budget.golden @@ -1,3 +1,3 @@ -({ cpu: 15479457 -| mem: 51292 +({ cpu: 14950457 +| mem: 48992 }) \ No newline at end of file diff --git a/plutus-tx-plugin/test/Optimization/maybeFun.plc.golden b/plutus-tx-plugin/test/Optimization/maybeFun.plc.golden index 72d467cf310..83818a3c359 100644 --- a/plutus-tx-plugin/test/Optimization/maybeFun.plc.golden +++ b/plutus-tx-plugin/test/Optimization/maybeFun.plc.golden @@ -24,13 +24,10 @@ [ (lam arg_0_i0 - (delay + (lam + case_Just_i0 (lam - case_Just_i0 - (lam - case_Nothing_i0 - [ case_Just_i2 arg_0_i3 ] - ) + case_Nothing_i0 [ case_Just_i2 arg_0_i3 ] ) ) ) @@ -51,6 +48,6 @@ ) ) ) - (delay (delay (lam case_Just_i0 (lam case_Nothing_i0 case_Nothing_i1)))) + (lam case_Just_i0 (lam case_Nothing_i0 case_Nothing_i1)) ] ) \ No newline at end of file