Skip to content

[Test] Add 'fix id' #6800

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

Merged
merged 1 commit into from
Jan 29, 2025
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
Expand Up @@ -140,6 +140,7 @@ module PlutusCore.Evaluation.Machine.ExBudget
, ExBudgetBuiltin(..)
, ExRestrictingBudget(..)
, LowerInitialCharacter
, largeBudget
, enormousBudget
) where

Expand Down Expand Up @@ -206,6 +207,12 @@ newtype ExRestrictingBudget = ExRestrictingBudget
deriving newtype (Semigroup, Monoid)
deriving newtype (Pretty, PrettyBy config, NFData)

-- | When we want to just evaluate the program that is intended to run out of budget we use the
-- 'Restricting' mode with this big budget designed to make the CEK machine terminate in a
-- fraction of a second on the reference machine.
largeBudget :: ExRestrictingBudget
largeBudget = ExRestrictingBudget $ ExBudget (2 * 10 ^ (11 :: Int)) (10 ^ (10 :: Int))

-- | When we want to just evaluate the program we use the 'Restricting' mode with an enormous
-- budget, so that evaluation costs of on-chain budgeting are reflected accurately in benchmarks.
enormousBudget :: ExRestrictingBudget
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ import PlutusIR.Generators.QuickCheck

import PlutusCore.Builtin (fromValue)
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekParametersForTesting)
import PlutusCore.Name.Unique
import PlutusCore.Pretty
Expand All @@ -25,7 +24,7 @@ import PlutusCore.Version (latestVersion)
import PlutusIR
import PlutusIR.Test ()
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek (restricting, runCekNoEmit,
import UntypedPlutusCore.Evaluation.Machine.Cek (restrictingLarge, runCekNoEmit,
unsafeSplitStructuralOperational)

import Control.Exception
Expand Down Expand Up @@ -203,11 +202,10 @@ noStructuralErrors term =
-- Throw on a structural evaluation error and succeed on both an operational evaluation error and
-- evaluation success.
void . evaluate . unsafeSplitStructuralOperational . fst $ do
let -- The numbers are picked so that evaluation of the arbitrarily generated term always
-- finishes in reasonable time even if evaluation loops (in which case we'll get an
-- out-of-budget failure).
budgeting = restricting . ExRestrictingBudget $ ExBudget 1000000000 1000000000
runCekNoEmit defaultCekParametersForTesting budgeting term
-- Using 'restrictingLarge' so that evaluation of the arbitrarily generated term always finishes
-- in reasonable time even if evaluation loops (in which case we'll get an out-of-budget
-- failure).
runCekNoEmit defaultCekParametersForTesting restrictingLarge term

-- | Test that evaluation of well-typed terms doesn't fail with a structural error.
prop_noStructuralErrors :: Property
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ module UntypedPlutusCore.Evaluation.Machine.Cek
, counting
, tallying
, restricting
, restrictingLarge
, restrictingEnormous
, enormousBudget
-- * Emitter modes
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ module UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode
, enormousBudget
, tallying
, restricting
, restrictingLarge
, restrictingEnormous
)
where
Expand Down Expand Up @@ -159,6 +160,10 @@ restricting (ExRestrictingBudget initB@(ExBudget cpuInit memInit)) = ExBudgetMod
final = RestrictingSt . ExRestrictingBudget <$> remaining
pure $ ExBudgetInfo spender final cumulative

-- | 'restricting' instantiated at 'largeBudget'.
restrictingLarge :: ThrowableBuiltins uni fun => ExBudgetMode RestrictingSt uni fun
restrictingLarge = restricting largeBudget

-- | 'restricting' instantiated at 'enormousBudget'.
restrictingEnormous :: ThrowableBuiltins uni fun => ExBudgetMode RestrictingSt uni fun
restrictingEnormous = restricting enormousBudget
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@ import PlutusCore.Builtin
import PlutusCore.Compiler.Erase (eraseTerm)
import PlutusCore.Data
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Examples.Builtins
Expand Down Expand Up @@ -497,16 +496,33 @@ test_TrackCostsRetaining =
]
assertBool err $ expected > actual

typecheckAndEvalToOutOfEx :: Term TyName Name DefaultUni DefaultFun () -> Assertion
typecheckAndEvalToOutOfEx term =
let evalRestricting params = fst . runCekNoEmit params restrictingLarge
in case typecheckAnd def evalRestricting defaultBuiltinCostModelForTesting term of
Right (Left (ErrorWithCause (OperationalEvaluationError (CekOutOfExError _)) _)) ->
pure ()
err -> assertFailure $ "Expected a 'CekOutOfExError' but got: " ++ displayPlc err

test_SerialiseDataImpossible :: TestTree
test_SerialiseDataImpossible =
testCase "Serialising an impossible 'Data' object finishes" $ do
testCase "Serialising an impossible 'Data' object runs out of budget and finishes" $ do
let dataLoop :: Term TyName Name DefaultUni DefaultFun ()
dataLoop = Apply () (Builtin () SerialiseData) $ mkConstant () loop where
loop = List [loop]
budgetMode = restricting . ExRestrictingBudget $ ExBudget 10000000000 10000000
evalRestricting params = unsafeSplitStructuralOperational . fst . runCekNoEmit params budgetMode
typecheckAnd def evalRestricting defaultBuiltinCostModelForTesting dataLoop @?=
Right EvaluationFailure
dataLoop =
let loop = List [loop]
in Apply () (Builtin () SerialiseData) $ mkConstant () loop
typecheckAndEvalToOutOfEx dataLoop

test_fixId :: TestTree
test_fixId =
testCase "'fix id' runs out of budget and finishes" $ do
let fixId :: Term TyName Name DefaultUni DefaultFun ()
fixId =
mkIterAppNoAnn (mkIterInstNoAnn Plc.fix [integer, integer])
[ tyInst () Plc.idFun (TyFun () integer integer)
, mkConstant @Integer () 42
]
typecheckAndEvalToOutOfEx fixId

-- | If the first char is an opening paren and the last chat is a closing paren, then remove them.
-- This is useful for rendering a term-as-a-test-name in CLI, since currently we wrap readably
Expand Down Expand Up @@ -1195,6 +1211,7 @@ test_definition =
, test_TrackCostsRetaining
#endif
, test_SerialiseDataImpossible
, test_fixId
, runTestNestedHere
[ test_Integer
, test_String
Expand Down