Skip to content

Commit

Permalink
PLT-4248: Added SemiArbitrary as in marlowe-cardano
Browse files Browse the repository at this point in the history
  • Loading branch information
yveshauser committed Mar 16, 2023
1 parent 1ec19a7 commit 988487e
Show file tree
Hide file tree
Showing 4 changed files with 482 additions and 119 deletions.
1 change: 1 addition & 0 deletions marlowe-spec-test/marlowe-spec-test.cabal
Expand Up @@ -47,6 +47,7 @@ library
aeson,
base >=4.9 && <5,
bytestring,
containers,
marlowe,
tasty,
tasty-hunit,
Expand Down
129 changes: 41 additions & 88 deletions marlowe-spec-test/src/Marlowe/Spec/Core/Arbitrary.hs
Expand Up @@ -18,19 +18,18 @@ 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 QuickCheck.GenT (GenT, MonadGen (..), frequency, resize, 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.Gen (chooseInteger, elements)
import qualified Test.QuickCheck.Gen as QC (chooseInteger, elements)

data RandomResponse a
= RandomValue a
| UnknownType TypeId


instance ToJSON a => ToJSON (RandomResponse a) where
toJSON (RandomValue v) = object
[ "value" .= v
Expand All @@ -49,17 +48,14 @@ instance FromJSON a => FromJSON (RandomResponse a) where
data GenerateRandomValueException = GenerateRandomValueException String
deriving (Show, Exception)


-- | Part of the Fibonacci sequence.
fibonaccis :: Num a => [a]
fibonaccis = [2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584]


-- | Inverse-Fibanoncci frequencies.
fibonacciFrequencies :: Integral a => [a]
fibonacciFrequencies = (1000000 `div`) <$> fibonaccis


-- | Select an element of a list with propability proportional to inverse-Fibonacci weights.
arbitraryFibonacci :: [a] -> Gen a
arbitraryFibonacci = frequency . zip fibonacciFrequencies . fmap pure
Expand All @@ -80,9 +76,9 @@ 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)
chooseinteger :: (Arith.Int, Arith.Int) -> Gen Arith.Int
chooseinteger (Arith.Int_of_integer i, Arith.Int_of_integer j) =
Arith.Int_of_integer <$> QC.chooseInteger (i, j)

-- | An arbitrary non-negative integer, mostly small.
arbitraryNonnegativeInteger :: Gen Arith.Int
Expand All @@ -102,42 +98,40 @@ arbitraryPositiveInteger = Arith.Int_of_integer <$>
, (30, arbitraryFibonacci fibonaccis)
]

type TimeInterval = (Arith.Int, Arith.Int)

-- | Geneate a semi-random time interval.
arbitraryTimeInterval :: Gen TimeInterval
arbitraryTimeInterval :: Gen (Arith.Int, Arith.Int)
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 :: Arith.Int -> Gen (Arith.Int, Arith.Int)
arbitraryTimeIntervalAround limit =
do
start <- arbitraryInteger `suchThat` (less_eq limit)
start <- arbitraryInteger `suchThat` (flip 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 :: Arith.Int -> Arith.Int -> Gen (Arith.Int, Arith.Int)
arbitraryTimeIntervalBefore lower upper =
do
start <- arbitraryInteger `suchThat` (less_eq lower)
duration <- chooseInteger' (0, upper - start - 1)
start <- arbitraryInteger `suchThat` (flip 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 :: Arith.Int -> Gen (Arith.Int, Arith.Int)
arbitraryTimeIntervalAfter lower =
do
start <- arbitraryInteger `suchThat` (\t -> less t lower)
start <- arbitraryInteger `suchThat` (less_eq lower)
duration <- arbitraryNonnegativeInteger
pure (start, start + duration)

-- | Shrink a generated time interval.
shrinkTimeInterval :: TimeInterval -> [TimeInterval]
shrinkTimeInterval :: (Arith.Int, Arith.Int) -> [(Arith.Int, Arith.Int)]
shrinkTimeInterval (start, end) =
let
mid = (start + end) `Arith.divide_int` 2
Expand All @@ -152,7 +146,6 @@ shrinkTimeInterval (start, end) =
, (end , end )
]


arbitrarySeed :: Gen Int
arbitrarySeed = resize 10000 $ choose (1, 10000000)

Expand All @@ -178,6 +171,17 @@ genParty interpret = do
Right (UnknownType _) -> throwIO $ GenerateRandomValueException "Client process doesn't know how to generate Core.Party"
Right (RandomValue t) -> pure t

genContract :: InterpretJsonRequest -> GenT IO Contract
genContract interpret = do
size <- liftGen $ getSize
seed <- liftGen $ arbitrarySeed
liftIO do
res <- interpret (GenerateRandomValue (TypeId "Core.Contract" (Proxy :: Proxy Contract)) size seed)
case parseValidResponse res of
Left err -> throwIO $ GenerateRandomValueException err
Right (UnknownType _) -> throwIO $ GenerateRandomValueException "Client process doesn't know how to generate Core.Contract"
Right (RandomValue t) -> pure t

genPayee :: InterpretJsonRequest -> GenT IO Payee
genPayee i = do
isParty <- liftGen arbitrary
Expand Down Expand Up @@ -338,8 +342,8 @@ genObservation i = sized (

genAction :: InterpretJsonRequest -> GenT IO Action
genAction i = frequency
[ (4, Deposit <$> genParty i <*> genParty i <*> genToken i <*> genValue i)
, (5, do
[ (7, Deposit <$> genParty i <*> genParty i <*> genToken i <*> genValue i)
, (2, do
lSize <- liftGen $ chooseInt (1, 4)
Choice <$> genChoiceId i <*> vectorOf lSize (liftGen genBound)
)
Expand All @@ -349,32 +353,6 @@ genAction i = frequency
genCase :: InterpretJsonRequest -> GenT IO Case
genCase i = Case <$> genAction i <*> genContract i

genContract :: InterpretJsonRequest -> GenT IO Contract
genContract i = sized (
\case n | n <= 1 -> genClose
| otherwise -> frequency
[ ( 30, genClose)
, ( 20, genPay n)
, ( 15, genIf n)
, ( 20, genWhen n)
, ( 10, genLet n)
, ( 5, genAssert n)
]
)
where
genClose = pure Close
genPay n = Pay <$> genParty i <*> genPayee i <*> genToken i <*> limit (genValue i) <*> resize (n - 1) (genContract i)
genIf n = If <$> limit (genObservation i) <*> resize (n - 1) (genContract i) <*> resize (n - 1) (genContract i)
genWhen n = do
lSize <- liftGen $ chooseInt (0, 3)
cases <- vectorOf lSize (resize (n - lSize) (genCase i))
timeout <- liftGen $ arbitraryInteger
cont <- resize (n - 1) (genContract i)
pure $ When cases timeout cont
genLet n = Let <$> liftGen genValueId <*> limit (genValue i) <*> resize (n - 1) (genContract i)
genAssert n = Assert <$> limit (genObservation i) <*> resize (n - 1) (genContract i)
limit = scale (min 3)

genInput :: InterpretJsonRequest -> GenT IO Input
genInput i = frequency
[ (50, IDeposit <$> genParty i <*> genParty i <*> genToken i <*> liftGen arbitraryInteger)
Expand Down Expand Up @@ -469,27 +447,22 @@ arbitraryValidStep state (When cases timeout _) =
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] ()
else
do
times <- arbitraryTimeIntervalBefore minTime' timeout
case' <- QC.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 <- QC.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
Expand All @@ -502,34 +475,14 @@ arbitraryValidStep state contract =
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.
txIn <- arbitraryValidStep state contract
case computeTransaction txIn 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
TransactionOutput (TransactionOutputRecord_ext _ _ txOutState txOutContract _) -> (txIn :) <$> arbitraryValidInputs txOutState txOutContract
19 changes: 11 additions & 8 deletions marlowe-spec-test/src/Marlowe/Spec/Core/Semantics.hs
@@ -1,13 +1,16 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}

module Marlowe.Spec.Core.Semantics where
module Marlowe.Spec.Core.Semantics
( tests
)
where

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, arbitraryValidStep)
import Marlowe.Spec.Core.Arbitrary (genValue, genState, genEnvironment, genContract, genTransaction, arbitraryNonnegativeInteger, arbitraryValidInputs)
import Marlowe.Spec.Interpret (InterpretJsonRequest, Request (..), Response (..))
import Marlowe.Spec.Reproducible (reproducibleProperty, reproducibleProperty', generate, generateT, assertResponse)
import Test.Tasty (TestTree, testGroup)
Expand All @@ -31,10 +34,10 @@ tests i = testGroup "Semantics"
[ evalValueTest i
, divisionRoundsTowardsZeroTest i
-- TransactionBound.thy
-- , playTrace_only_accepts_maxTransactionsInitialStateTest i -- FIXME: does not make sense!
-- , playTrace_only_accepts_maxTransactionsInitialStateTest i -- FIXME: does not make sense
-- SingleInputTransactions.thy
, traceToSingleInputIsEquivalentTest i
, reduceContractUntilQuiescentIdempotentTest i -- FIXME: new request
, reduceContractUntilQuiescentIdempotentTest i
-- QuiescentResults.thy
, computeTransactionIsQuiescentTest i
, playTraceIsQuiescentTest i
Expand Down Expand Up @@ -94,7 +97,7 @@ playTrace_only_accepts_maxTransactionsInitialStateTest interpret = reproducibleP
RequestResponse res <- run $ liftIO $ interpret req

case JSON.fromJSON res of
JSON.Success (TransactionOutput (TransactionOutputRecord_ext _ _ _ txOutContract _)) -> do
JSON.Success (TransactionOutput (TransactionOutputRecord_ext _ _ _ _ _)) -> do
monitor
( counterexample $
"Request: " ++ showAsJson req ++ "\n"
Expand Down Expand Up @@ -144,7 +147,7 @@ reduceContractUntilQuiescentIdempotentTest interpret = reproducibleProperty "red
RequestResponse res <- run $ liftIO $ interpret req

case JSON.fromJSON res of
JSON.Success (ContractQuiescent reduced warnings payments nsta ncont) -> do
JSON.Success (ContractQuiescent _ _ _ nsta ncont) -> do
monitor
( counterexample $
"Request: " ++ showAsJson req ++ "\n"
Expand Down Expand Up @@ -210,9 +213,9 @@ computeTransactionIsQuiescentTest interpret = reproducibleProperty "Compute tran
-- isQuiescent (txOutContract traOut) (txOutState traOut)"
playTraceIsQuiescentTest :: InterpretJsonRequest -> TestTree
playTraceIsQuiescentTest interpret = reproducibleProperty "playTrace is quiescent" do
contract <- run $ generateT $ genContract interpret
contract <- run $ generateT $ genContract interpret `suchThat` (/=Close)
startTime <- run $ generate $ arbitraryNonnegativeInteger
transactions <- run $ generate $ listOf1 $ arbitraryValidStep (State_ext [] [] [] startTime ()) contract
transactions <- run $ generate $ arbitraryValidInputs (State_ext [] [] [] startTime ()) contract `suchThat` ((>0) . length)
let
req :: Request JSON.Value
req = PlayTrace (integer_of_int startTime) contract transactions
Expand Down

0 comments on commit 988487e

Please sign in to comment.