diff --git a/marlowe-test/changelog.d/20231121_151418_ramsay.md b/marlowe-test/changelog.d/20231121_151418_ramsay.md new file mode 100644 index 0000000000..bbae219018 --- /dev/null +++ b/marlowe-test/changelog.d/20231121_151418_ramsay.md @@ -0,0 +1,4 @@ +### Added + +- Regression tests for Static Analysis. Specifically: explicit tests for each of the warning types, plus reachability and payouts on close. + diff --git a/marlowe-test/marlowe-test.cabal b/marlowe-test/marlowe-test.cabal index 380b80b868..d8e4989c45 100644 --- a/marlowe-test/marlowe-test.cabal +++ b/marlowe-test/marlowe-test.cabal @@ -192,6 +192,8 @@ test-suite marlowe-test Spec.Marlowe.Serialization.CoreJson Spec.Marlowe.Serialization.ExtendedJson Spec.Marlowe.Service.Isabelle + Spec.Marlowe.StaticAnalysis + Spec.Marlowe.StaticAnalysis.Regression build-depends: , aeson >=2 && <3 diff --git a/marlowe-test/test/Spec.hs b/marlowe-test/test/Spec.hs index 30ed7a0851..5442553cc3 100644 --- a/marlowe-test/test/Spec.hs +++ b/marlowe-test/test/Spec.hs @@ -21,6 +21,7 @@ import qualified Spec.Marlowe.Plutus (tests) import qualified Spec.Marlowe.Semantics (tests) import qualified Spec.Marlowe.Serialization (tests) import qualified Spec.Marlowe.Service.Isabelle (tests) +import qualified Spec.Marlowe.StaticAnalysis (tests) -- | Timeout seconds for static analysis, which can take so much time on a complex contract -- that it exceeds hydra/CI resource limits, see SCP-4267. @@ -49,4 +50,5 @@ tests = , Spec.Marlowe.Semantics.tests , Spec.Marlowe.Plutus.tests , Spec.Marlowe.Service.Isabelle.tests + , Spec.Marlowe.StaticAnalysis.tests ] diff --git a/marlowe-test/test/Spec/Marlowe/StaticAnalysis.hs b/marlowe-test/test/Spec/Marlowe/StaticAnalysis.hs new file mode 100644 index 0000000000..c9f2144626 --- /dev/null +++ b/marlowe-test/test/Spec/Marlowe/StaticAnalysis.hs @@ -0,0 +1,28 @@ +----------------------------------------------------------------------------- +-- +-- Module : Spec.Marlowe.StaticAnalysis +-- License : Apache 2.0 +-- +-- Stability : Experimental +-- Portability : Portable +-- + +----------------------------------------------------------------------------- + +-- | Tests of Marlowe semantics. +module Spec.Marlowe.StaticAnalysis ( + -- * Testing + tests, +) where + +import Test.Tasty (TestTree, testGroup) + +import qualified Spec.Marlowe.StaticAnalysis.Regression (tests) + +-- | Run the tests. +tests :: TestTree +tests = + testGroup + "StaticAnalysis" + [ Spec.Marlowe.StaticAnalysis.Regression.tests + ] diff --git a/marlowe-test/test/Spec/Marlowe/StaticAnalysis/Regression.hs b/marlowe-test/test/Spec/Marlowe/StaticAnalysis/Regression.hs new file mode 100644 index 0000000000..0ca641d08a --- /dev/null +++ b/marlowe-test/test/Spec/Marlowe/StaticAnalysis/Regression.hs @@ -0,0 +1,211 @@ +----------------------------------------------------------------------------- +-- +-- Module : Spec.Marlowe.StaticAnalysis.Regression +-- License : Apache 2.0 +-- +-- Stability : Experimental +-- Portability : Portable +-- +----------------------------------------------------------------------------- +{-# LANGUAGE OverloadedStrings #-} + +-- | Regression tests for the important behaviour of the Static Analysis functions. +module Spec.Marlowe.StaticAnalysis.Regression ( + -- * Testing + tests, +) where + +import Language.Marlowe.Util (ada) +import Test.Tasty (TestTree, testGroup) +import Prelude + +import Data.Either (fromRight, isRight) +import Data.Maybe (isNothing) +import Language.Marlowe ( + Action (..), + Case (..), + Contract (..), + Observation (..), + Payee (..), + Token (..), + TransactionWarning (..), + Value (..), + ) +import Language.Marlowe.Analysis.FSSemantics (warningsTrace) +import Spec.Marlowe.Common (alicePk) +import Test.Tasty.HUnit (assertBool, assertEqual, testCase) + +isTransactionPartialPay :: TransactionWarning -> Bool +isTransactionPartialPay (TransactionPartialPay{}) = True +isTransactionPartialPay _ = False + +isTransactionNonPositivePay :: TransactionWarning -> Bool +isTransactionNonPositivePay (TransactionNonPositivePay{}) = True +isTransactionNonPositivePay _ = False + +isTransactionNonPositiveDeposit :: TransactionWarning -> Bool +isTransactionNonPositiveDeposit (TransactionNonPositiveDeposit{}) = True +isTransactionNonPositiveDeposit _ = False + +isTransactionShadowing :: TransactionWarning -> Bool +isTransactionShadowing (TransactionShadowing{}) = True +isTransactionShadowing _ = False + +isTransactionAssertionFailed :: TransactionWarning -> Bool +isTransactionAssertionFailed (TransactionAssertionFailed{}) = True +isTransactionAssertionFailed _ = False + +getWarning :: Contract -> IO (Maybe TransactionWarning) +getWarning contract = + do + res <- warningsTrace contract + return $ case res of + Right (Just (_, _, w : _)) -> Just w + _ -> Nothing + +analysisWorks :: IO () +analysisWorks = do + let contract n d = + If + (DivValue (Constant n) (Constant d) `ValueGE` Constant 5) + Close + (Pay alicePk (Party alicePk) Language.Marlowe.Util.ada (Constant (-100)) Close) + result <- warningsTrace (contract 10 11) + assertBool "Analyse a contract" $ isRight result + +emptyTrace :: IO () +emptyTrace = do + let contract = Close + result <- warningsTrace contract + assertBool "Close passes static analysis" $ isRight result && isNothing (fromRight Nothing result) + +nonPositivePay :: IO () +nonPositivePay = do + let contract n = Pay alicePk (Party alicePk) Language.Marlowe.Util.ada (Constant n) Close + result <- getWarning $ contract (-100) + assertBool "Detect negative pay" $ maybe False isTransactionNonPositivePay result + result2 <- getWarning $ contract 0 + assertBool "Detect zero pay" $ maybe False isTransactionNonPositivePay result2 + +partialPay :: IO () +partialPay = do + let contract = Pay alicePk (Party alicePk) Language.Marlowe.Util.ada (Constant 100) Close + result <- getWarning contract + assertBool "Detect partial pay" $ maybe False isTransactionPartialPay result + +nonPositiveDeposit :: IO () +nonPositiveDeposit = do + let contract v = + When + [ Case + ( Deposit + alicePk + alicePk + (Token "" "") + (Constant v) + ) + Close + ] + 1699974289397 + Close + result <- getWarning (contract (-100)) + assertBool "Negative deposit" $ maybe False isTransactionNonPositiveDeposit result + result2 <- getWarning (contract 0) + assertBool "Zero deposit" $ maybe False isTransactionNonPositiveDeposit result2 + +transactionShadowing :: IO () +transactionShadowing = do + let contract = Let "x" (Constant 1) (Let "x" (Constant 2) Close) + result <- getWarning contract + assertBool "Shadowing x" $ maybe False isTransactionShadowing result + +assertionFailed :: IO () +assertionFailed = do + let contract = Let "x" (Constant 1) (Assert (ValueEQ (UseValue "x") (Constant 2)) Close) + result <- getWarning contract + assertBool "Detect wrong assertion" $ maybe False isTransactionAssertionFailed result + +-- The current UI drops in instrumentation in the form of assertions and then checks for AssertionFailed +reachability :: IO () +reachability = do + let contract = + Let + "x" + (Constant 1) + ( If + ( ValueGE + (UseValue "x") + (Constant 2) + ) + ( Assert + ( ValueGE + (UseValue "x") + (Constant 2) + ) + Close + ) + ( Assert + ( ValueLT + (UseValue "x") + (Constant 2) + ) + (Assert FalseObs Close) + ) + ) + result <- getWarning contract + assertBool "Detect reachable path" $ maybe False isTransactionAssertionFailed result + let contract2 = + Let + "x" + (Constant 1) + ( If + ( ValueGE + (UseValue "x") + (Constant 2) + ) + ( Assert + ( ValueGE + (UseValue "x") + (Constant 2) + ) + (Assert FalseObs Close) + ) + ( Assert + ( ValueLT + (UseValue "x") + (Constant 2) + ) + Close + ) + ) + result2 <- getWarning contract2 + assertEqual "Don't trigger a warning on the unreachable path" result2 Nothing + +-- The current UI drops in instrumentation in the form of assertions and then checks for AssertionFailed +fundsOnClose :: IO () +fundsOnClose = do + let contract = + When + [ Case + (Deposit alicePk alicePk Language.Marlowe.Util.ada (Constant 100)) + (Assert (ValueEQ (AvailableMoney alicePk Language.Marlowe.Util.ada) (Constant 0)) Close) + ] + 1699974289397 + Close + result <- getWarning contract + assertBool "Detect funds on close" $ maybe False isTransactionAssertionFailed result + +tests :: TestTree +tests = + testGroup + "Static Analysis Regression" + [ testCase "Analysis works" analysisWorks + , testCase "Empty trace" emptyTrace + , testCase "Partial Pay" partialPay + , testCase "Non-Positive Pay" nonPositivePay + , testCase "Non-Positive Deposit" nonPositiveDeposit + , testCase "Transaction shadowing" transactionShadowing + , testCase "Assertion failed" assertionFailed + , testCase "Reachability checks" reachability + , testCase "Funds on Close" fundsOnClose + ]