From 1ec19a75857d6d27cd13a0d19affbf217f5b7843 Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Thu, 16 Mar 2023 11:04:28 +0100 Subject: [PATCH] PLT-4248: Generating valid transaction --- isabelle/marlowe.cabal | 2 +- .../src/Marlowe/Spec/Core/Arbitrary.hs | 193 ++++++++++++++++-- .../src/Marlowe/Spec/Core/Semantics.hs | 15 +- 3 files changed, 183 insertions(+), 27 deletions(-) diff --git a/isabelle/marlowe.cabal b/isabelle/marlowe.cabal index 10c4430a..78a11584 100644 --- a/isabelle/marlowe.cabal +++ b/isabelle/marlowe.cabal @@ -31,7 +31,6 @@ library ListTools MList Option - Orderings OptBoundTimeInterval Product_Lexorder Product_Type @@ -44,6 +43,7 @@ library Examples.Escrow Examples.Swap MarloweCoreJson + Orderings PositiveAccounts Semantics SemanticsTypes diff --git a/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs b/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs index bbdb5f5e..2487f607 100644 --- a/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs +++ b/marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs @@ -1,27 +1,30 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} module Marlowe.Spec.Core.Arbitrary where -import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), parseValidResponse) -import Data.Data (Proxy(..)) -import Marlowe.Spec.TypeId (TypeId(..)) -import Control.Monad.IO.Class (liftIO) -import Control.Exception (throwIO, Exception) -import Data.Aeson (FromJSON(..), withObject, (.:), (.=)) -import Control.Applicative ((<|>)) -import Data.Aeson (ToJSON (..), object) import qualified Arith +import Control.Applicative ((<|>)) +import Control.Exception (Exception, throwIO) import Control.Monad (liftM2) -import QuickCheck.GenT (vectorOf, GenT, MonadGen (..), suchThat, frequency, sized, resize, scale) -import Semantics (Transaction_ext(..), Payment(..), TransactionWarning (..), TransactionError (..), TransactionOutput(..), TransactionOutputRecord_ext (..)) -import SemanticsTypes (Token(..), Party, Payee(..), ChoiceId (ChoiceId), Bound(..), Value(..), ValueId(..), Observation(..), Action (..), Case(..), Contract (..), Input (..), State_ext(..), IntervalError (..), Environment_ext (..)) +import Control.Monad.IO.Class (liftIO) +import Data.Aeson (FromJSON (..), ToJSON (..), object, withObject, (.:), (.=)) +import Data.Data (Proxy (..)) +import Data.List (nub) +import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), parseValidResponse) +import Marlowe.Spec.TypeId (TypeId (..)) +import Orderings (Ord (..), max) +import QuickCheck.GenT (GenT, MonadGen (..), frequency, resize, scale, sized, suchThat, vectorOf) +import Semantics (Payment (..), TransactionError (..), TransactionOutput (..), TransactionOutputRecord_ext (..), TransactionWarning (..), Transaction_ext (..), computeTransaction, evalValue) import SemanticsGuarantees (valid_state) +import SemanticsTypes (Action (..), Bound (..), Case (..), ChoiceId (ChoiceId), Contract (..), Environment_ext (..), Input (..), IntervalError (..), Observation (..), Party, Payee (..), State_ext (..), Token (..), Value (..), ValueId (..), minTime) import Test.QuickCheck (Gen, chooseInt, getSize) -import Test.QuickCheck.Arbitrary (Arbitrary(..)) +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Gen (chooseInteger, elements) data RandomResponse a = RandomValue a @@ -61,6 +64,10 @@ fibonacciFrequencies = (1000000 `div`) <$> fibonaccis arbitraryFibonacci :: [a] -> Gen a arbitraryFibonacci = frequency . zip fibonacciFrequencies . fmap pure +-- | Shrink a string. +shrinkString :: (a -> String) -> [a] -> a -> [a] +shrinkString f universe selected = filter + (\candidate -> length (f candidate) > 0 && length (f candidate) < length (f selected)) universe -- | An arbitrary integer, mostly small. arbitraryInteger :: Gen Arith.Int @@ -73,6 +80,10 @@ arbitraryInteger = Arith.Int_of_integer <$> , (60, arbitraryFibonacci fibonaccis) ] +chooseInteger' :: (Arith.Int, Arith.Int) -> Gen Arith.Int +chooseInteger' (Arith.Int_of_integer i, Arith.Int_of_integer j) = + Arith.Int_of_integer <$> chooseInteger (i, j) + -- | An arbitrary non-negative integer, mostly small. arbitraryNonnegativeInteger :: Gen Arith.Int arbitraryNonnegativeInteger = Arith.Int_of_integer <$> @@ -82,6 +93,66 @@ arbitraryNonnegativeInteger = Arith.Int_of_integer <$> , (30, arbitraryFibonacci fibonaccis) ] +-- | An arbitrary positive integer, mostly small. +arbitraryPositiveInteger :: Gen Arith.Int +arbitraryPositiveInteger = Arith.Int_of_integer <$> + frequency + [ + (60, arbitrary `suchThat` (> 0)) + , (30, arbitraryFibonacci fibonaccis) + ] + +type TimeInterval = (Arith.Int, Arith.Int) + +-- | Geneate a semi-random time interval. +arbitraryTimeInterval :: Gen TimeInterval +arbitraryTimeInterval = + do + start <- arbitraryInteger + duration <- arbitraryNonnegativeInteger + pure (start, start + duration) + +-- | Generate a semi-random time interrval straddling a given time. +arbitraryTimeIntervalAround :: Arith.Int -> Gen TimeInterval +arbitraryTimeIntervalAround limit = + do + start <- arbitraryInteger `suchThat` (less_eq limit) + duration <- ((limit - start) +) <$> arbitraryNonnegativeInteger + pure (start, start + duration) + +-- | Generate a semi-random time interval before a given time. +arbitraryTimeIntervalBefore :: Arith.Int -> Arith.Int -> Gen TimeInterval +arbitraryTimeIntervalBefore lower upper = + do + start <- arbitraryInteger `suchThat` (less_eq lower) + duration <- chooseInteger' (0, upper - start - 1) + pure (start, start + duration) + +-- | Generate a semi-random time interval after a given time. +arbitraryTimeIntervalAfter :: Arith.Int -> Gen TimeInterval +arbitraryTimeIntervalAfter lower = + do + start <- arbitraryInteger `suchThat` (\t -> less t lower) + duration <- arbitraryNonnegativeInteger + pure (start, start + duration) + +-- | Shrink a generated time interval. +shrinkTimeInterval :: TimeInterval -> [TimeInterval] +shrinkTimeInterval (start, end) = + let + mid = (start + end) `Arith.divide_int` 2 + in + filter (/= (start, end)) + $ nub + [ + (start, start) + , (start, mid ) + , (mid , mid ) + , (mid , end ) + , (end , end ) + ] + + arbitrarySeed :: Gen Int arbitrarySeed = resize 10000 $ choose (1, 10000000) @@ -140,6 +211,10 @@ randomChoiceNames = arbitraryChoiceName :: Gen String arbitraryChoiceName = arbitraryFibonacci randomChoiceNames +-- | Shrink a generated choice name +shrinkChoiceName :: String -> [String] +shrinkChoiceName = shrinkString id randomChoiceNames + genChoiceId :: InterpretJsonRequest -> GenT IO ChoiceId genChoiceId i = ChoiceId <$> liftGen arbitraryChoiceName <*> genParty i @@ -332,9 +407,10 @@ genState i = rawGen `suchThat` valid_state accounts <- vectorOf accountSize ((genParty i >*< genToken i) >*< liftGen arbitraryNonnegativeInteger) choices <- vectorOf choiceSize (genChoiceId i >*< liftGen arbitraryInteger) bounds <- vectorOf boundSize (liftGen genValueId >*< liftGen arbitraryInteger) - minTime <- liftGen arbitraryNonnegativeInteger - pure $ State_ext accounts choices bounds minTime () + minTime' <- liftGen arbitraryNonnegativeInteger + pure $ State_ext accounts choices bounds minTime' () ) + genTransactionWarning :: InterpretJsonRequest -> GenT IO TransactionWarning genTransactionWarning i = frequency [ ( 30, TransactionNonPositiveDeposit <$> genParty i <*> genParty i <*> genToken i <*> liftGen arbitraryInteger) @@ -343,7 +419,6 @@ genTransactionWarning i = frequency , ( 10, pure TransactionAssertionFailed) ] - genIntervalError :: Gen IntervalError genIntervalError = do lower <- arbitraryInteger @@ -378,3 +453,83 @@ genTransactionOutput i = genEnvironment :: Gen (Environment_ext ()) genEnvironment = Environment_ext <$> genInterval <*> pure () + +-- | Generate a random step for a contract. +arbitraryValidStep :: State_ext () -- ^ The state of the contract. + -> Contract -- ^ The contract. + -> Gen (Transaction_ext ()) -- ^ Generator for a transaction input for a single step. +arbitraryValidStep _ (When [] timeout _) = Transaction_ext <$> arbitraryTimeIntervalAfter timeout <*> pure [] <*> pure () +arbitraryValidStep state (When cases timeout _) = + do + let + isEmptyChoice (Choice _ []) = True + isEmptyChoice _ = False + minTime' = minTime state + + isTimeout <- frequency [(9, pure False), (1, pure True)] + if isTimeout || less_eq timeout minTime' || all (isEmptyChoice . getAction) cases + then Transaction_ext <$> arbitraryTimeIntervalAfter timeout <*> pure [] <*> pure () + else do + times <- arbitraryTimeIntervalBefore minTime' timeout + case' <- elements $ filter (not . isEmptyChoice . getAction) cases + i <- case getAction case' of + Deposit a p t v -> pure . IDeposit a p t $ evalValue (Environment_ext times ()) state v + Choice n bs -> do + Bound lower upper <- elements bs + IChoice n <$> chooseInteger' (lower, upper) + Notify _ -> pure INotify + pure $ Transaction_ext times [i] () + where + getAction :: Case -> Action + getAction (Case a _) = a + +arbitraryValidStep state contract = +{- + NOTE: Alternatively, if semantics should allow applying `[]` to a non-quiescent contract + without ever throwing a timeout-related error, then replace the above with the following: + + TransactionInput <$> arbitraryTimeIntervalAround minTime <*> pure [] +-} + let + nextTimeout Close = minTime state + nextTimeout (Pay _ _ _ _ continuation) = nextTimeout continuation + nextTimeout (If _ thenContinuation elseContinuation) = maximum' $ nextTimeout <$> [thenContinuation, elseContinuation] + nextTimeout (When _ timeout _) = timeout + nextTimeout (Let _ _ continuation) = nextTimeout continuation + nextTimeout (Assert _ continuation) = nextTimeout continuation + in + Transaction_ext <$> arbitraryTimeIntervalAfter (maximum' [minTime state, nextTimeout contract]) <*> pure [] <*> pure () + where + maximum' = foldl1 Orderings.max + +-- | Generate random transaction input. +arbitraryValidInput :: State_ext () -- ^ The state of the contract. + -> Contract -- ^ The contract. + -> Gen (Transaction_ext ()) -- ^ Generator for a transaction input. +arbitraryValidInput = arbitraryValidInput' Nothing + +arbitraryValidInput' :: Maybe (Transaction_ext ()) -> State_ext () -> Contract -> Gen (Transaction_ext ()) +arbitraryValidInput' Nothing state contract = arbitraryValidStep state contract +arbitraryValidInput' (Just tr@(Transaction_ext timeInterval input _)) state contract = + case computeTransaction tr state contract of + TransactionError _ -> pure tr + TransactionOutput (TransactionOutputRecord_ext _ _ txOutState txOutContract _) -> do + Transaction_ext a nextInput b <- arbitraryValidStep state contract + let + combinedInput = input ++ nextInput -- {txInputs = txInputs input ++ txInputs nextInput} + newTr = Transaction_ext a combinedInput b + case computeTransaction newTr txOutState txOutContract of + TransactionError _ -> pure tr + TransactionOutput (TransactionOutputRecord_ext _ _ _ _ _) -> pure newTr + +-- | Generate a random path through a contract. +arbitraryValidInputs :: State_ext () -- ^ The state of the contract. + -> Contract -- ^ The contract. + -> Gen [Transaction_ext ()] -- ^ Generator for a transaction inputs. +arbitraryValidInputs _ Close = pure [] +arbitraryValidInputs state contract = + do + input <- arbitraryValidInput state contract + case computeTransaction input state contract of -- FIXME: It is tautological to use `computeTransaction` to filter test cases. + TransactionError _ -> pure [] + TransactionOutput (TransactionOutputRecord_ext _ _ txOutState txOutContract _) -> (input :) <$> arbitraryValidInputs txOutState txOutContract diff --git a/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs b/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs index 0fabf614..1608c506 100644 --- a/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs +++ b/marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs @@ -7,15 +7,15 @@ import qualified Arith as Arith import Control.Monad.IO.Class (MonadIO(..)) import Data.Aeson (ToJSON(..)) import qualified Data.Aeson as JSON -import Marlowe.Spec.Core.Arbitrary (genValue, genState, genEnvironment, genContract, genTransaction, arbitraryNonnegativeInteger) +import Marlowe.Spec.Core.Arbitrary (genValue, genState, genEnvironment, genContract, genTransaction, arbitraryNonnegativeInteger, arbitraryValidStep) import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), Response (..)) import Marlowe.Spec.Reproducible (reproducibleProperty, reproducibleProperty', generate, generateT, assertResponse) import Test.Tasty (TestTree, testGroup) import Test.QuickCheck (withMaxSuccess) import Test.QuickCheck.Monadic (assert, run, monitor, pre) -import Semantics (evalValue, playTrace, computeTransaction, TransactionOutput (..), TransactionOutputRecord_ext (TransactionOutputRecord_ext), isQuiescent, TransactionWarning, txOutWarnings, reduceContractUntilQuiescent, ReduceResult (..)) +import Semantics (evalValue, playTrace, computeTransaction, TransactionOutput (..), TransactionOutputRecord_ext (TransactionOutputRecord_ext), isQuiescent, TransactionWarning, txOutWarnings, reduceContractUntilQuiescent, ReduceResult (..), Transaction_ext (..)) import Timeout (isClosedAndEmpty) -import SemanticsTypes (Value(..), State_ext (..), Contract(..)) +import SemanticsTypes (Value(..), State_ext (..), Contract(..), minTime) import SingleInputTransactions (traceListToSingleInput) import QuickCheck.GenT (suchThat) import QuickCheck.GenT (listOf) @@ -24,6 +24,7 @@ import Marlowe.Utils (showAsJson) import PositiveAccounts (validAndPositive_state) import QuickCheck.GenT (listOf1) import TransactionBound (maxTransactionsInitialState) +import Orderings (Ord(..)) tests :: InterpretJsonRequest -> TestTree tests i = testGroup "Semantics" @@ -208,10 +209,10 @@ computeTransactionIsQuiescentTest interpret = reproducibleProperty "Compute tran -- "playTrace sl cont (Cons h t) = TransactionOutput traOut ⟹ -- isQuiescent (txOutContract traOut) (txOutState traOut)" playTraceIsQuiescentTest :: InterpretJsonRequest -> TestTree -playTraceIsQuiescentTest interpret = reproducibleProperty "Play trace is quiescent" do +playTraceIsQuiescentTest interpret = reproducibleProperty "playTrace is quiescent" do contract <- run $ generateT $ genContract interpret - transactions <- run $ generateT $ listOf1 $ genTransaction interpret startTime <- run $ generate $ arbitraryNonnegativeInteger + transactions <- run $ generate $ listOf1 $ arbitraryValidStep (State_ext [] [] [] startTime ()) contract let req :: Request JSON.Value req = PlayTrace (integer_of_int startTime) contract transactions @@ -239,7 +240,7 @@ playTraceIsQuiescentTest interpret = reproducibleProperty "Play trace is quiesce timedOutTransaction_closes_contractTest :: InterpretJsonRequest -> TestTree timedOutTransaction_closes_contractTest interpret = reproducibleProperty "Timed-out transaction closes contract" do state <- run $ generateT $ genState interpret `suchThat` validAndPositive_state - txIn <- run $ generateT $ genTransaction interpret + txIn <- run $ generateT $ genTransaction interpret `suchThat` \(Transaction_ext (_,upper) _ _) -> less_eq (minTime state) upper let req :: Request JSON.Value req = ComputeTransaction txIn state Close @@ -264,7 +265,7 @@ timedOutTransaction_closes_contractTest interpret = reproducibleProperty "Timed- closeIsSafeTest :: InterpretJsonRequest -> TestTree closeIsSafeTest interpret = reproducibleProperty "Close is safe" do state <- run $ generateT $ genState interpret - txIn <- run $ generateT $ genTransaction interpret + txIn <- run $ generateT $ genTransaction interpret `suchThat` \(Transaction_ext (_,upper) _ _) -> less_eq (minTime state) upper let req :: Request JSON.Value req = ComputeTransaction txIn state Close