Skip to content

Commit

Permalink
[Builtins] [Test] Dump denotation signatures to golden files (#6462)
Browse files Browse the repository at this point in the history
This dumps the type signature of the denotation of each of the builtins to a golden file. All changes in type signatures must be reflected explicitly whenever they're captured by semantics variants (see the test code). This is a very important test given how easy it is to change the behavior of a builtin just by slightly tweaking the signature of its denotation.
  • Loading branch information
effectfully authored Sep 13, 2024
1 parent cbf99fb commit 179e07c
Show file tree
Hide file tree
Showing 128 changed files with 292 additions and 20 deletions.
Empty file added 4
Empty file.
27 changes: 21 additions & 6 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,7 @@ data ExtensionFun
| ExtensionVersion -- Reflect the version of the Extension
| TrackCosts -- For checking that each cost is released and can be picked up by GC once it's
-- accounted for in the evaluator.
| IntNoIntegerNoWord -- For testing the signature dump test.
deriving stock (Show, Eq, Ord, Enum, Bounded, Ix, Generic)
deriving anyclass (Hashable)

Expand Down Expand Up @@ -231,9 +232,12 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
type CostingPart uni ExtensionFun = ()

data BuiltinSemanticsVariant ExtensionFun =
ExtensionFunSemanticsVariantX
| ExtensionFunSemanticsVariantY
deriving stock (Enum, Bounded, Show)
ExtensionFunSemanticsVariant0
| ExtensionFunSemanticsVariant1
| ExtensionFunSemanticsVariant2
| ExtensionFunSemanticsVariant3
| ExtensionFunSemanticsVariant4
deriving stock (Eq, Ord, Enum, Bounded, Show)

toBuiltinMeaning :: forall val. HasMeaningIn uni val
=> BuiltinSemanticsVariant ExtensionFun
Expand Down Expand Up @@ -464,8 +468,11 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
makeBuiltinMeaning
@(() -> Integer)
(\_ -> case semvar of
ExtensionFunSemanticsVariantX -> 0
ExtensionFunSemanticsVariantY -> 1)
ExtensionFunSemanticsVariant0 -> 0
ExtensionFunSemanticsVariant1 -> 1
ExtensionFunSemanticsVariant2 -> 2
ExtensionFunSemanticsVariant3 -> 3
ExtensionFunSemanticsVariant4 -> 4)
whatever

-- We want to know if the CEK machine releases individual budgets after accounting for them and
Expand Down Expand Up @@ -537,5 +544,13 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
(\_ -> unsafePerformIO $ reverse <$> readMVar numsOfGcedVar)
(\_ -> unsafePerformIO . regBudgets . runCostingFunOneArgument model)

toBuiltinMeaning semvar IntNoIntegerNoWord =
case semvar of
ExtensionFunSemanticsVariant0 -> makeBuiltinMeaning @(Int -> ()) mempty whatever
ExtensionFunSemanticsVariant1 -> makeBuiltinMeaning @(Integer -> ()) mempty whatever
ExtensionFunSemanticsVariant2 -> makeBuiltinMeaning @(Integer -> ()) mempty whatever
ExtensionFunSemanticsVariant3 -> makeBuiltinMeaning @(Word -> ()) mempty whatever
ExtensionFunSemanticsVariant4 -> makeBuiltinMeaning @(Word -> ()) mempty whatever

instance Default (BuiltinSemanticsVariant ExtensionFun) where
def = ExtensionFunSemanticsVariantY
def = maxBound
18 changes: 15 additions & 3 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
Expand Down Expand Up @@ -90,15 +91,26 @@ class
-> fun
-> BuiltinMeaning val (CostingPart uni fun)

-- | Feed the 'TypeScheme' of the given built-in function to the continuation.
withTypeSchemeOfBuiltinFunction
:: forall val fun r.
(ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val, HasConstant val)
=> BuiltinSemanticsVariant fun
-> fun
-> (forall args res. TypeScheme val args res -> r)
-> r
withTypeSchemeOfBuiltinFunction semVar fun k =
case toBuiltinMeaning semVar fun of
BuiltinMeaning sch _ _ -> k sch

-- | Get the type of a built-in function.
typeOfBuiltinFunction
:: forall uni fun. ToBuiltinMeaning uni fun
=> BuiltinSemanticsVariant fun
-> fun
-> Type TyName uni ()
typeOfBuiltinFunction semvar fun =
case toBuiltinMeaning @_ @_ @(Term TyName Name uni fun ()) semvar fun of
BuiltinMeaning sch _ _ -> typeSchemeToType sch
typeOfBuiltinFunction semVar fun =
withTypeSchemeOfBuiltinFunction @(Term TyName Name uni fun ()) semVar fun typeSchemeToType

{- Note [Builtin semantics variants]
The purpose of the "builtin semantics variant" feature is to provide multiple,
Expand Down
32 changes: 25 additions & 7 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/TypeScheme.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@ import PlutusCore.Name.Unique
import Data.Kind qualified as GHC (Type)
import Data.Proxy
import Data.Text qualified as Text
import Data.Typeable
import GHC.TypeLits
import Type.Reflection

infixr 9 `TypeSchemeArrow`

Expand Down Expand Up @@ -78,9 +78,27 @@ typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType sch@TypeSchemeResult = toTypeAst sch
typeSchemeToType sch@(TypeSchemeArrow schB) =
TyFun () (toTypeAst $ argProxy sch) $ typeSchemeToType schB
typeSchemeToType (TypeSchemeAll proxy schK) = case proxy of
(_ :: Proxy '(text, uniq, kind)) ->
let text = Text.pack $ symbolVal @text Proxy
uniq = fromIntegral $ natVal @uniq Proxy
a = TyName $ Name text $ Unique uniq
in TyForall () a (demoteKind $ knownKind @kind) $ typeSchemeToType schK
typeSchemeToType (TypeSchemeAll (_ :: Proxy '(text, uniq, kind)) schB) =
let text = Text.pack $ symbolVal @text Proxy
uniq = fromIntegral $ natVal @uniq Proxy
a = TyName $ Name text $ Unique uniq
in TyForall () a (demoteKind $ knownKind @kind) $ typeSchemeToType schB

-- The precedence of @->@ is @-1@, which is why this number appears in the implementation of the
-- instance.
instance Show (TypeScheme val args res) where
showsPrec p sch@TypeSchemeResult =
showParen (p > 0)
$ showsPrec (-1) (typeRep sch)
showsPrec p sch@(TypeSchemeArrow schB) =
showParen (p > 0)
$ -- @0@ is to account for associativity, see https://stackoverflow.com/a/43639618
showsPrec 0 (typeRep $ argProxy sch)
. showString " -> "
. showsPrec (-1) schB
showsPrec p (TypeSchemeAll (_ :: Proxy '(text, uniq, kind)) schB) =
showParen (p > 0)
$ showString "forall "
. showString (symbolVal @text Proxy)
. showString ". "
. showsPrec 0 schB
2 changes: 1 addition & 1 deletion plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1120,7 +1120,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
= DefaultFunSemanticsVariantA
| DefaultFunSemanticsVariantB
| DefaultFunSemanticsVariantC
deriving stock (Eq, Enum, Bounded, Show, Generic)
deriving stock (Eq, Ord, Enum, Bounded, Show, Generic)
deriving anyclass (NFData, NoThunks)

-- Integers
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Bool -> ByteString -> ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Text -> Text -> Text
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> Data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element -> Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> BuiltinResult Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Element -> Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> BuiltinResult Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element -> Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> BuiltinResult Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Element -> Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> BuiltinResult Element
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
MlResult -> MlResult -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Element -> Element -> MlResult
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
MlResult -> MlResult -> MlResult
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Bool -> ByteString -> Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. Data -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. forall b. SomeConstant DefaultUni [TyVarRep * ('TyNameRep * "a" 0)] -> Opaque Val (TyVarRep * ('TyNameRep * "b" 1)) -> Opaque Val (TyVarRep * ('TyNameRep * "b" 1)) -> BuiltinResult (Opaque Val (TyVarRep * ('TyNameRep * "b" 1)))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. () -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Word8 -> ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> [Data] -> Data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> Int
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> BuiltinResult Text
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> BuiltinResult Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Text -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> Data -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Text -> Text -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Natural -> BuiltinResult Natural
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> Int
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. forall b. SomeConstant DefaultUni ((TyVarRep * ('TyNameRep * "a" 0)),(TyVarRep * ('TyNameRep * "b" 1))) -> BuiltinResult (Opaque Val (TyVarRep * ('TyNameRep * "a" 0)))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. SomeConstant DefaultUni [TyVarRep * ('TyNameRep * "a" 0)] -> BuiltinResult (Opaque Val (TyVarRep * ('TyNameRep * "a" 0)))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. Bool -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> Int -> BuiltinResult Word8
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Bool -> NumBytesCostedAsNumWords -> Integer -> BuiltinResult ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> Int
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
[Data] -> Data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
[(Data,Data)] -> Data
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. SomeConstant DefaultUni (TyVarRep * ('TyNameRep * "a" 0)) -> SomeConstant DefaultUni [TyVarRep * ('TyNameRep * "a" 0)] -> BuiltinResult (Opaque Val [TyVarRep * ('TyNameRep * "a" 0)])
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
() -> [Data]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
() -> [(Data,Data)]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> Data -> (Data,Data)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> BuiltinResult Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. SomeConstant DefaultUni [TyVarRep * ('TyNameRep * "a" 0)] -> BuiltinResult Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Bool -> ByteString -> ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> BuiltinResult Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> Int -> BuiltinResult Bool
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> BuiltinResult Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
NumBytesCostedAsNumWords -> Word8 -> BuiltinResult ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> IntegerCostedLiterally -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> IntegerCostedLiterally -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Int -> Int -> ByteString -> ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. forall b. SomeConstant DefaultUni ((TyVarRep * ('TyNameRep * "a" 0)),(TyVarRep * ('TyNameRep * "b" 1))) -> BuiltinResult (Opaque Val (TyVarRep * ('TyNameRep * "b" 1)))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Integer -> Integer -> Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. SomeConstant DefaultUni [TyVarRep * ('TyNameRep * "a" 0)] -> BuiltinResult (Opaque Val [TyVarRep * ('TyNameRep * "a" 0)])
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
forall a. Text -> Opaque Val (TyVarRep * ('TyNameRep * "a" 0)) -> BuiltinResult (Opaque Val (TyVarRep * ('TyNameRep * "a" 0)))
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> BuiltinResult ByteString
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> BuiltinResult (Integer,[Data])
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> BuiltinResult Integer
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> BuiltinResult [Data]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Data -> BuiltinResult [(Data,Data)]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ByteString -> ByteString -> ByteString -> BuiltinResult Bool
Loading

0 comments on commit 179e07c

Please sign in to comment.