[Builtins] Allow casing on lists #7188
Conversation
SeungheonOh
force-pushed
the
sho/6602-list
branch
from
118e668 to
5ac006c
Compare
|
/benchmark lists |
SeungheonOh
added
No Changelog Required
|
|
Click here to check the status of your benchmark. |
|
Comparing benchmark results of 'lists' on '837a15684' (base) and '5ac006c50' (PR) Results table
|
| | FrameConstr !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann) | ||
| -- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@ | ||
| | FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann) | ||
| | FrameCases ann !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann) -- TODO: This is bad |
There was a problem hiding this comment.
Interestingly, this doesn't hurt the performance. I still think this is bad tough
There was a problem hiding this comment.
Okay, #7189 will allow us to fix this by constructing term with arbitrary annotation.
| , TyBuiltin @TyName ann $ SomeTypeIn $ DefaultUniList ty | ||
| ]) | ||
| ] | ||
| _ -> Left $ "Casing on list requires two branches" |
There was a problem hiding this comment.
I discussed it with @zliu41 and IIRC we agreed that we should allow only one branch too for the cons case, since a lot of time it's expected that the list is gonna be non-empty and it would be wasteful to have a branch for the nil case when it's supposed to fail evaluation anyway.
@zliu41 we still need to reconcile it with False being the default for Bool. It's not too late to change things I think. Maybe we should make True and (:) the default branches for consistency. We can do it with or without reordering them. So let's discuss it some time.
There was a problem hiding this comment.
I added single case as well
There was a problem hiding this comment.
Change the error message too.
I suppose do it for booleans too while you're here? To make it consistent.
There was a problem hiding this comment.
For Bool, do we want to enforce that number of branches can only be exactly one or two?
Current the type annotation allows some other "trailing" branches to be present--like case (con bool False) foo bar baz bob rob cob) where everything besides foo and bar will be ignored. However, current builtin casing itself doesn't allow it, so it would need to be fixed to match one behavior or another.
I don't see any use of this; bool casing with more than two branches would need to be statically removed anyways for script size optimization. We should only allow one or two branches on bool casing
There was a problem hiding this comment.
I'll go forward with only one or two branches allowed, but please let me know if there is a good argument against this.
There was a problem hiding this comment.
Yeah, that's what I attempted to suggest. Thanks.
plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
Outdated
Show resolved
Hide resolved
SeungheonOh
force-pushed
the
sho/6602-list
branch
from
cc4c4f6 to
430635f
Compare
| , TyBuiltin @TyName ann $ SomeTypeIn $ DefaultUniList ty | ||
| ]) | ||
| ] | ||
| _ -> Left $ "Casing on list requires two branches" |
There was a problem hiding this comment.
Change the error message too.
I suppose do it for booleans too while you're here? To make it consistent.
| headSpine :: Opaque val asToB -> [val] -> Opaque (HeadSpine val) b | ||
| headSpine (Opaque f) = Opaque . \case | ||
| headSpineOpaque :: Opaque val asToB -> [val] -> Opaque (MonoHeadSpine val) b | ||
| headSpineOpaque (Opaque f) = Opaque . \case |
There was a problem hiding this comment.
Reuse headSpine? Doesn't matter much, I'm gonna remove this anyway.
There was a problem hiding this comment.
headSpineOpaque is no longer needed at all?
There was a problem hiding this comment.
Yes, with the removal of CaseData and CaseList. I will remove
There was a problem hiding this comment.
I think it's okay to leave this actually. This can be useful future for adding other builtins
plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
Outdated
Show resolved
Hide resolved
| Right res -> computeCek ctx env res | ||
| Left err -> throwErrorDischarged (OperationalError $ CekCaseBuiltinError err) e | ||
| Right (HeadOnly fX) -> computeCek ctx env fX | ||
| Right (HeadSpine f xs) -> computeCek (transferConstantSpine xs ctx) env f |
There was a problem hiding this comment.
Using Either here was stupid on my part, should've introduced a dedicated strict data type.
But now that I look at it, it's probably best to inline HeadSpine business in such a data type, so that it has three constructors (error / success with only head / success with head and spine).
Not in this PR though, let's do it separately and measure whether it helps.
There was a problem hiding this comment.
I'll make a PR for this after this one
| @@ -1 +1 @@ | |||
| forall a. Opaque Val (Integer -> [Data] -> TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val ([(Data,Data)] -> TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val ([Data] -> TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (Integer -> TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (ByteString -> TyVarRep * ('TyNameRep * "a" 0)) -> Data -> Opaque (HeadSpine Val) (TyVarRep * ('TyNameRep * "a" 0)) No newline at end of file | |||
There was a problem hiding this comment.
This will go anyways, but need to appease CI
SeungheonOh
force-pushed
the
sho/6602-list
branch
from
a8e9fae to
bb7314d
Compare
SeungheonOh
had a problem deploying
to
github-pages
GitHub Actions
Failure
SeungheonOh
force-pushed
the
sho/6602-list
branch
from
d5d8c3e to
87639ad
Compare
|
/benchmark lists |
|
Click here to check the status of your benchmark. |
|
Comparing benchmark results of 'lists' on '589516f72' (base) and '87639ad20' (PR) Results table
|
|
Not bad! |
|
|
|
Make sure to check that the budget reductions are aligned with the performance improvements. We don't want to see, say, a 70% budget reduction when the code is only 40% faster. |
|
Do we currently have configurable budgeting mechanism for casing? I haven't seen any budget related code on CEK for casing. |
We don't, it's just the regular cost of a single CEK step. |
| (/\dead -> z) | ||
| (/\dead -> f (headList {a} xs) (tailList {a} xs)) | ||
| {r}) | ||
| \(z : r) (f : a -> list a -> r) (xs : list a) -> case r xs [z, f]) |
There was a problem hiding this comment.
Hm, check how annAlwaysInline instead of annMayInline in PlutusTx.Compiler.Builtins affects things.
There was a problem hiding this comment.
Yeah, can confirm, I checked too, no changes
| Term Size: 1_391 | ||
| Flat Size: 1_977 | ||
| CPU: 186_924_676 | ||
| Memory: 721_804 |
There was a problem hiding this comment.
20% MEM reduction is pretty wild.
| CPU: 20_088_713 | ||
| Memory: 72_250 | ||
| Term Size: 89 | ||
| Flat Size: 654 | ||
| CPU: 8_111_579 | ||
| Memory: 33_498 | ||
| Term Size: 71 | ||
| Flat Size: 641 |
| CPU: 5_706_022 | ||
| Memory: 10_678 | ||
| Term Size: 165 | ||
| Flat Size: 1_208 | ||
| Term Size: 147 | ||
| Flat Size: 1_194 |
There was a problem hiding this comment.
Wait, how is is possible that CPU and MEM didn't change?
There was a problem hiding this comment.
probably because the script never needed to match on list. This is before fully evaluating term so makes sense
| Left _ -> False | ||
| Right EvaluationFailure -> length is /= 2 && (scrut || length is /= 1) | ||
| Left _ -> length is /= 1 && length is /= 2 | ||
| Right EvaluationFailure -> scrut || length is == 2 -- scrut implies length = 2 |
There was a problem hiding this comment.
Hm. So let's say there's a bug in the evaluator causing it to fail whenever scrut is True. Type checking succeeds, evaluation fails and you say it's ok? Or am I reading it wrong?
There was a problem hiding this comment.
Type checker is checking is correct number of branches and correct type for branches. If type checking passes but evaluation fails then it means that's matching True with single branch.
There was a problem hiding this comment.
oh wait, I think I messed up. It should be scrut && length is /= 2
There was a problem hiding this comment.
If type checking passes but evaluation fails then it means that's matching True with single branch.
No it doesn't, because maybe I implemented casing on lists wrong and it just always throws on True or something.
| force | ||
| (force (force chooseList) | ||
| (\s acc xs -> | ||
| case xs [acc, (\hd -> (\x -> s s x) (force mkCons hd acc))]))) |
There was a problem hiding this comment.
Nevermind about inlining caseList, it seems to inline perfectly well in the end.
| CPU: 1_827_714 | ||
| Memory: 7_992 | ||
| Term Size: 81 | ||
| Flat Size: 76 | ||
| CPU: 752_100 | ||
| Memory: 4_800 | ||
| Term Size: 66 | ||
| Flat Size: 66 |
| l | ||
| [ `$dMkNil` | ||
| , (\ds xs -> | ||
| force (force (drop (delay (\x -> x)))) |
There was a problem hiding this comment.
"force force drop delay id" is a piece of modern art.
| CPU: 19_055_427 | ||
| Memory: 84_856 | ||
| Term Size: 119 | ||
| Flat Size: 122 | ||
| CPU: 4_736_100 | ||
| Memory: 29_700 | ||
| Term Size: 86 | ||
| Flat Size: 96 |
|
Should be good to go now |
|
Performance improvement here is pretty sweat, but multi-let will improve it much more. Since multi-bind will remove the need for matching on list repeatedly which will be a massive improvement. Alternatively, we can have annotated case matching which would be also very useful. |
| -- only matching branches get executed. | ||
| -- | Generate a term that does a lot of casing on boolean | ||
| casingBool :: Integer -> Term | ||
| casingBool 0 = constant () $ someValueOf DefaultUniInteger 42 |
| headSpine :: Opaque val asToB -> [val] -> Opaque (HeadSpine val) b | ||
| headSpine (Opaque f) = Opaque . \case | ||
| headSpineOpaque :: Opaque val asToB -> [val] -> Opaque (MonoHeadSpine val) b | ||
| headSpineOpaque (Opaque f) = Opaque . \case |
There was a problem hiding this comment.
headSpineOpaque is no longer needed at all?
plutus-core/untyped-plutus-core/test/Evaluation/Golden/caseNonTag.type.golden
Outdated
Show resolved
Hide resolved
| listElem | ||
| (mkConstant () scrut) | ||
| [ mkConstant @Integer () 42 | ||
| , lamAbs () x listElem $ lamAbs () xs list $ var () x |
There was a problem hiding this comment.
We should rename Bool success to Bool success 2 and add Bool success 1 for when there's only one branch. And do the same here. Because Bool any doesn't properly cover the case with a single branch and the False scrutinee.
But that can be a separate PR.
| kase () | ||
| listElem | ||
| (mkConstant () scrut) | ||
| [ lamAbs () x listElem $ lamAbs () xs list $ var () x |
There was a problem hiding this comment.
This doesn't cover the case when there's more branches than expected.
It's also out of sync with the Bool tests, which have very similar constraints. I do think it's a good idea to have the two that you have there, but then we should also
- add a test for when there's more branches than expected
- structure the
Booltests the same way
I felt like Bool any was an OK way to merge what you have here and the too-many-branches test into a single test, but I never actually measured coverage, so if you want to split it into two, that's even better I guess.
There was a problem hiding this comment.
I tested coverage, and it was pretty okay. Regardlessly, I think it's better to have separate cases.
plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Definition.hs
Show resolved
Hide resolved
2 participants
Part of #6602
We haven't fully decided how casing on list should be. I tried simply casing into nil case and cons case.