Skip to content

Commit

Permalink
Don't evaluate away builtins where the result might be unserializable (
Browse files Browse the repository at this point in the history
…#5664)

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

See the note. The test case does evaluate the uncompress application
until you add the guard, so this is working as desired. We can see if it
fixes Kenneth's problem.

* Fix warning

* Comments
  • Loading branch information
michaelpj authored Dec 7, 2023
1 parent 42989c4 commit f20dd9b
Show file tree
Hide file tree
Showing 15 changed files with 150 additions and 5 deletions.
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
}
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

{- 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
)
]

0 comments on commit f20dd9b

Please sign in to comment.