Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't evaluate away builtins where the result might be unserializable #5664

Merged
merged 3 commits into from
Dec 7, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
### Fixed

- The `EvaluateBuiltins` pass will no longer produce constants that can't be serialized.
69 changes: 67 additions & 2 deletions plutus-core/plutus-ir/src/PlutusIR/Analysis/Builtins.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
Expand All @@ -13,9 +14,13 @@ module PlutusIR.Analysis.Builtins
, BuiltinsInfo (..)
, biSemanticsVariant
, biMatcherLike
, biUnserializableConstants
, builtinArityInfo
, constantIsSerializable
, termIsSerializable
, asBuiltinDatatypeMatch
, builtinDatatypeMatchBranchArities
, defaultUniUnserializableConstants
) where

import Control.Lens hiding (parts)
Expand All @@ -29,6 +34,8 @@ import PlutusCore.Builtin qualified as PLC
import PlutusCore.Default
import PlutusCore.MkPlc (mkIterTyAppNoAnn)
import PlutusIR.Contexts
import PlutusIR.Core (Term)
import PlutusIR.Core.Plated (_Constant, termSubtermsDeep)
import PlutusPrelude (Default (..))

-- | The information we need to work with a builtin that is like a datatype matcher.
Expand All @@ -41,15 +48,18 @@ makeLenses ''BuiltinMatcherLike

-- | All non-static information about builtins that the compiler might want.
data BuiltinsInfo (uni :: Type -> Type) fun = BuiltinsInfo
{ _biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun
, _biMatcherLike :: Map.Map fun (BuiltinMatcherLike uni fun)
{ _biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun
, _biMatcherLike :: Map.Map fun (BuiltinMatcherLike uni fun)
-- See Note [Unserializable constants]
, _biUnserializableConstants :: Some (ValueOf uni) -> Bool
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we care about -ize versus -ise? Probably not: I think we're pretty inconsistent elsewhere. You could go for broke and call them "unzerializable" though.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We're massively inconsistent. I'm inconsistent in my own writing. I have no idea which is which, I just use them randomly.

}
makeLenses ''BuiltinsInfo

instance Default (BuiltinsInfo DefaultUni DefaultFun) where
def = BuiltinsInfo
{ _biSemanticsVariant = def
, _biMatcherLike = defaultUniMatcherLike
, _biUnserializableConstants = defaultUniUnserializableConstants
}

-- | Get the arity of a builtin function from the 'PLC.BuiltinInfo'.
Expand All @@ -61,6 +71,19 @@ builtinArityInfo
-> Arity
builtinArityInfo binfo = builtinArity (Proxy @uni) (binfo ^. biSemanticsVariant)

constantIsSerializable
:: forall uni fun
. BuiltinsInfo uni fun
-> Some (ValueOf uni)
-> Bool
constantIsSerializable bi v = not $ _biUnserializableConstants bi v

termIsSerializable :: BuiltinsInfo uni fun -> Term tyname name uni fun a -> Bool
termIsSerializable binfo =
allOf
(termSubtermsDeep . _Constant)
(constantIsSerializable binfo . snd)

-- | Split a builtin 'match'.
asBuiltinDatatypeMatch ::
Ord fun
Expand Down Expand Up @@ -162,3 +185,45 @@ defaultUniMatcherLike = Map.fromList
vars <> TypeAppContext resTy resTyAnn (TermAppContext scrut scrutAnn branches)
-- both branches have no args
chooseListBranchArities = [[], []]

-- See Note [Unserializable constants]
defaultUniUnserializableConstants :: Some (ValueOf DefaultUni) -> Bool
defaultUniUnserializableConstants = \case
Some (ValueOf DefaultUniBLS12_381_G1_Element _) -> True
Some (ValueOf DefaultUniBLS12_381_G2_Element _) -> True
Some (ValueOf DefaultUniBLS12_381_MlResult _) -> True
_ -> False
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You could tediously spell out all the other cases here so that if we add more types to the universe we'd be forced to look at this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I could, but I'm not sure it's worth it. This is a weird special case...


{- Note [Unserializable constants]
Generally we require that programs are (de-)serializable, which requires that all constants
in the program are (de-)serializable. This is enforced by the type system, we have to
have instances for all builtin types in the universe.

However, in practice we have to limit this somewhat. In particular, some builtin types
have no _cheap_ (de-)serialization method. This notably applies to the BLS constants, where
both BLS "deserialization" and "uncompression" do some sanity checks that take a non-trivial
amount of time.

This is a problem: in our time budgeting for validating transactions we generally assume
that deserialization is proportional to input size with low constant factors. But for a
malicious program made up of only BLS points, this would not be true!

So pragmatically we disallow (de-)serialization of constants of such types (the instances
still exist, but they will fail at runtime). The problem then is that we need to make
sure that we don't accidentally create any such constants. It's one thing if the _user_
does it - then we can just tell them not to (there are usually workarounds). But the
compiler should also not do it! Notably, the EvaluateBuiltins pass can produce _new_
constants.

To deal with this problem we pass around a predicate that tells us which constants are
bad, so we can just refuse to perform a transformation if it would produce unrepresentable
constants.

An alternative approach would be to instead add a pass to rewrite the problematic
constants into a non-problematic form (e.g. conversion from a bytestring instead of a constant).
This would be better for optimization, since we wouldn't be blocking EvaluateBuiltins
from working, even if it was good, but it has two problems:
1. It would fight with EvaluateBuiltins, which each undoing the other.
2. It can't work generically, since we don't always have a way to do the transformation. In
particular, there isn't a way to do this for the ML-result BLS type.
-}
5 changes: 5 additions & 0 deletions plutus-core/plutus-ir/src/PlutusIR/Core/Plated.hs
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ module PlutusIR.Core.Plated
, termUniquesDeep
, varDeclSubtypes
, underBinders
, _Constant
) where

import PlutusCore qualified as PLC
Expand All @@ -49,6 +50,10 @@ infixr 6 <^>
(<^>) :: Fold s a -> Fold s a -> Fold s a
(f1 <^> f2) g s = f1 g s *> f2 g s

-- | View a term as a constant.
_Constant :: Prism' (Term tyname name uni fun a) (a, PLC.Some (PLC.ValueOf uni))
_Constant = prism' (uncurry Constant) (\case { Constant a v -> Just (a, v); _ -> Nothing })

{-# INLINE bindingSubterms #-}
-- | Get all the direct child 'Term's of the given 'Binding'.
bindingSubterms :: Traversal' (Binding tyname name uni fun a) (Term tyname name uni fun a)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ evaluateBuiltins conservative binfo costModel = transformOf termSubterms process
-- suboptimal, e.g. in `ifThenElse True x y`, we will get back `x`, but
-- with the annotation that was on the `ifThenElse` node. But we can't
-- easily do better.
Just t' -> x <$ t'
Nothing -> t
-- See Note [Unserializable constants]
Just t' | termIsSerializable binfo t' -> x <$ t'
_ -> t
processTerm t = t
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,27 @@ import Test.QuickCheck.Property (Property, withMaxSuccess)
test_evaluateBuiltins :: TestTree
test_evaluateBuiltins = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
testNested "EvaluateBuiltins" $
conservative ++ nonConservative
where
conservative =
map
(goldenPir (evaluateBuiltins True def def) pTerm)
[ "addInteger"
, "ifThenElse"
, "trace"
, "traceConservative"
, "failingBuiltin"
, "nonConstantArg"
, "overApplication"
, "underApplication"
, "uncompressBlsConservative"
]
nonConservative =
map
(goldenPir (evaluateBuiltins False def def) pTerm)
-- We want to test the case where this would reduce, i.e.
[ "traceNonConservative"
, "uncompressBlsNonConservative"
, "uncompressAndEqualBlsNonConservative"
]

-- | Check that a term typechecks after a `PlutusIR.Transform.EvaluateBuiltins`
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
-- In non-conservative mode should be removed
[{(builtin trace) (con integer) } (con string "hello") (con integer 1)]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(con integer 1)
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
-- This would evaluate all the way to a boolean constant (which is serializable!) but we block the intermediate states
-- (which have unserializable constants), so we can't get there.
[
(builtin bls12_381_G1_equal)
[(builtin bls12_381_G1_uncompress) (con bytestring #97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb)]
[(builtin bls12_381_G1_uncompress) (con bytestring #97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb)]
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
[
[
(builtin bls12_381_G1_equal)
[
(builtin bls12_381_G1_uncompress)
(con
bytestring
#97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb
)
]
]
[
(builtin bls12_381_G1_uncompress)
(con
bytestring
#97f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb
)
]
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-- In conservative mode should be left
[
(builtin bls12_381_G2_uncompress)
(con
bytestring
#c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
)
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[
(builtin bls12_381_G2_uncompress)
(con
bytestring
#c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
)
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-- Should also be left in non-conservative mode because the result is unrepresentable
[
(builtin bls12_381_G2_uncompress)
(con
bytestring
#c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
)
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[
(builtin bls12_381_G2_uncompress)
(con
bytestring
#c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
)
]