diff --git a/docs/goals_and_soa.md b/docs/goals_and_soa.md index ba592a3..489acf2 100644 --- a/docs/goals_and_soa.md +++ b/docs/goals_and_soa.md @@ -52,7 +52,7 @@ what we use to demonstrate problems in following: * Fracada * JPG Vesting Contract * Indigo Protocol -* DApp project we participate, audited or otherwise know it codebase +* DApp projects we participated, audited or otherwise know their codebase * Hydra Auction * POCRE * CNS @@ -64,8 +64,6 @@ what we use to demonstrate problems in following: * [Game Model](https://github.com/IntersectMBO/plutus-apps/blob/dbafa0ffdc1babcf8e9143ca5a7adde78d021a9a/doc/plutus/tutorials/GameModel.hs) * plutus-usecases -@todo #3: Add more links to specific bugs and code size blowups in existing DApps. - ## On-chain correctness ### Known common vulnerabilities @@ -85,14 +83,31 @@ taking that burden from developers and auditors. Those problems are similar to previous in that they tend to arise in naive Plutus implementations, -if developer was did not make measures to prevent them. +if developer was did not take measures to prevent them. + +Plutus forces developers to write TxIn/TxOut constraints from scratch, +leading by subtle bugs from copy-pasting logic or +trying to optimize them by hand. + +Examples: + +* Security bug in MinSwap audit - 2.2.1.3 Unauthorized Hijacking of Pools Funds +* Non-security bug in MinSwap audit - 2.2.2.2 Batcher Is Not Allowed to Apply Their Own Order + +Such constraints naturally lead to conditions +for which more performant implementation should +omit some constraints always following from others. +Such kind of manual SMT solving exercises are +known source for security bugs and complicated code. -Almost all transactions which require fungible tokens as input, +One of important cases is maintaining invariants of token value. +TODO - add explanation + +Most of transactions which require fungible tokens as input, should not depend from exact UTxO coin-change distribution. Failure to expect that leads to prohibition of correct transactions. -On other side too broad constraint might lead to -fund stealing. +On other side too broad constraint might lead to fund stealing. Example of bugs: @@ -117,6 +132,9 @@ Examples: * Non-security bug: https://github.com/mlabs-haskell/hydra-auction/issues/129 * Non-security bug: https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997 +* Non-intentionally under-specified behavior in MinSwap audit: + * `2.2.2.1 Batchers Can Choose Batching Order` + * Triggered by `2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs"` * Multiple kind of code complication was observed in CNS audit. * Utilities [from Indigo](https://github.com/IndigoProtocol/indigo-smart-contracts/blob/main/src/Indigo/Utils/Spooky/Helpers.hs) @@ -182,6 +200,19 @@ Our script stages abstraction cover all those kind of problems. * @todo #3: document problems with slots in Plutus/Cardano API * https://github.com/mlabs-haskell/hydra-auction/issues/236 +## Matching off-chain logic + +Problem of duplicating logic between on- and off-chain is twofold. +Testing is essentially offchain, thus, you may miss that your onchain code +is not actually enforcing part of Tx provided in tests. + +CEM Script is constructing Tx for submission from same specification, +which is used for onchain script. Thus it is much harder to miss constraint +to be checked. + +Examples: + +* MinSwap audit - 2.2.1.2 LP Tokens Can Be Duplicated ## Logic duplication and spec subtleness @@ -211,6 +242,33 @@ is much less obvious to implement, and out of scope of current Catalyst project, but it is very much possible feature as well. +Examples of diagrams in DApp specifications: + +* ... +* ... +* ... + +### On-/Off-chain and spec logic duplication + +Writing on-chain contracts manually encodes non-deterministic state machine, +which cannot be used for off-chain transaction construction. +Thus developer need to write them again in different style in off-chain code, +which is tedious and error prone. + +They should add checks for all errors possible, +like coins being available and correct script states being present, +to prevent cryptic errors and provide retrying strategies +for possible utxo changes. + +Our project encodes scripts in deterministic machine, +containing enough information to construct transaction automatically. +This also gives a way to check for potential on/off-chain logic differences +semi-automatically. + +Example: +* MinSwap Audit - 2.2.4.3 Large Refactoring Opportunities +* `availableVestings` - пример чего-то подобного для SimpleAuction + Examples of this done by hand: * [State graph for Agora](https://github.com/Liqwid-Labs/agora/blob/staging/docs/diagrams/ProposalStateMachine.png) @@ -244,10 +302,8 @@ Examples of boilerplate: * https://github.com/MELD-labs/cardano-defi-public/tree/eacaa527823031105eba1730f730e1b32f1470bc/lending-index/src/Lending/Index -### Correct off-chain Tx construction logic +Timing ... -A lot of on-chain problems, like timing and coin change issues -have their counterpart on Tx submission side. @todo #3: Add more off-chain code duplication examples from existing PABs. Include problems with coin-selection, tests, retrying and errors. @@ -305,12 +361,19 @@ and multiple commiters schemes (used in `hydra`). ### Atlas -Atlas provides (emulate-everything) and overall more humane DX -on top of cardano-api. But it has no feature related to goals +Atlas provides more humane DX on top of cardano-api. +But it has no features related to goals (synced-by-construction), (secure-by-construction) and (declarative-spec). +(emulate-everything) is planned, but is not implemented currently. + +Atlas includes connectors to Blockfrost and other backends, +which our project lacks. + +Also our project has slight differences in API design decisions. +Our monad interfaces is meant to be slightly more modular. +We use much less custom type wrappers, resorting to Plutus types where possible. -@todo #3: Add more specifics on Atlas to docs. ## Testing tools diff --git a/example/CEM/Example/Auction.hs b/example/CEM/Example/Auction.hs index ef3927f..758a476 100644 --- a/example/CEM/Example/Auction.hs +++ b/example/CEM/Example/Auction.hs @@ -133,12 +133,23 @@ instance CEMScript SimpleAuction where ) cEmptyValue ) - , output - (userUtxo ctxParams.seller) - (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.betAmount) - , output - (userUtxo buyoutBid.better) - (cMinLovelace @<> ctxParams.lot) + , if' + (ctxParams.seller `eq'` buyoutBid.better) + ( output + (userUtxo ctxParams.seller) + (cMinLovelace @<> ctxParams.lot) + ) + ( output + (userUtxo buyoutBid.better) + (cMinLovelace @<> ctxParams.lot) + ) + , if' + (ctxParams.seller `eq'` buyoutBid.better) + noop + ( output + (userUtxo ctxParams.seller) + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.betAmount) + ) ] ) ] diff --git a/src/Cardano/CEM/DSL.hs b/src/Cardano/CEM/DSL.hs index 26dcefd..ad53157 100644 --- a/src/Cardano/CEM/DSL.hs +++ b/src/Cardano/CEM/DSL.hs @@ -17,6 +17,7 @@ module Cardano.CEM.DSL ( UtxoKind (..), SameScriptArg (..), getMainSigner, + getMbMainSigner, -- * DSL ConstraintDSL (..), @@ -298,7 +299,19 @@ getMainSigner cs = case mapMaybe f cs of [pkh] -> pkh _ -> error - "Transition should have exactly one MainSignerCoinSelection constraint" + "Transition should have exactly one MainSigner* constraint" + where + f (MainSignerNoValue pkh) = Just pkh + f (MainSignerCoinSelect pkh _ _) = Just pkh + f _ = Nothing + +getMbMainSigner :: [TxConstraint True script] -> Maybe PubKeyHash +getMbMainSigner cs = case mapMaybe f cs of + [] -> Nothing + [pkh] -> Just pkh + _ -> + error + "Transition should have exactly one MainSigner* constraint" where f (MainSignerNoValue pkh) = Just pkh f (MainSignerCoinSelect pkh _ _) = Just pkh diff --git a/src/Cardano/CEM/Monads.hs b/src/Cardano/CEM/Monads.hs index 1e2022b..8c19827 100644 --- a/src/Cardano/CEM/Monads.hs +++ b/src/Cardano/CEM/Monads.hs @@ -124,7 +124,7 @@ data TxSubmittingError -- | Error occurred while trying to execute CEMScript transition data TransitionError - = CannotFindTransitionInput + = CannotFindTransitionInput String | CompilationError String | SpecExecutionError {errorMessage :: String} deriving stock (Show, Eq) diff --git a/src/Cardano/CEM/OffChain.hs b/src/Cardano/CEM/OffChain.hs index 38593a9..c3b9b16 100644 --- a/src/Cardano/CEM/OffChain.hs +++ b/src/Cardano/CEM/OffChain.hs @@ -138,8 +138,7 @@ construct rs = constructGo rs emptyResolvedTx , toMint = TxMintNone , additionalSigners = [] , signer = error "TODO: Unreachable laziness trick" - , -- FIXME - interval = always + , interval = always -- TODO: use validity intervals } constructGo (r : rest) !acc = let newAcc = case r of @@ -197,7 +196,7 @@ process (MkCEMAction params transition) ec = case ec of map (withKeyWitness . fst) $ Map.toList $ unUTxO utxo -- FIXME: do actuall coin selection return $ TxInR $ head utxoPairs - (Utxo kind fanFilter value) -> do + c@(Utxo kind fanFilter value) -> do case kind of Out -> do let value' = convertTxOut $ fromPlutusValue value @@ -208,6 +207,7 @@ process (MkCEMAction params transition) ec = case ec of someIn -> do utxo <- lift $ queryUtxo $ ByAddresses [address] let + -- utxoPairs = traceShowId $ Map.toList $ unUTxO utxo utxoPairs = Map.toList $ unUTxO utxo matchingUtxos = map (addWittness . fst) $ filter predicate utxoPairs @@ -217,7 +217,7 @@ process (MkCEMAction params transition) ec = case ec of In -> TxInR x InRef -> TxInRefR x [] -> - throwError $ PerTransitionErrors [CannotFindTransitionInput] + throwError $ PerTransitionErrors [CannotFindTransitionInput $ show c] where predicate (_, txOut) = txOutValue txOut == fromPlutusValue value @@ -264,11 +264,11 @@ process (MkCEMAction params transition) ec = case ec of -- ----------------------------------------------------------------------------- data TxResolutionError - = CEMScriptTxInResolutionError - | -- FIXME: record transition and action involved + = NoSignerError + | CEMScriptTxInResolutionError + | -- TODO: record transition and action involved PerTransitionErrors [TransitionError] - | -- FIXME: this is weird - UnhandledSubmittingError TxSubmittingError + | UnhandledSubmittingError TxSubmittingError deriving stock (Show) resolveTx :: diff --git a/src/Cardano/CEM/Smart.hs b/src/Cardano/CEM/Smart.hs index 3017065..7ad1f0b 100644 --- a/src/Cardano/CEM/Smart.hs +++ b/src/Cardano/CEM/Smart.hs @@ -19,8 +19,8 @@ import Plutarch.Prelude ( (#&&), ) import PlutusLedgerApi.V2 (PubKeyHash, ToData (..), Value) -import Prelude hiding (error) -import Prelude qualified (error) +import Prelude hiding (Eq, error) +import Prelude qualified (Eq, error) -- ----------------------------------------------------------------------------- -- Helpers to be used in actual definitions @@ -118,7 +118,7 @@ inState :: inState spine = UnsafeUpdateOfSpine ctxState spine [] (@==) :: - (Eq x) => ConstraintDSL script x -> ConstraintDSL script x -> ConstraintDSL script Bool + (Prelude.Eq x) => ConstraintDSL script x -> ConstraintDSL script x -> ConstraintDSL script Bool (@==) = Eq (@<=) :: @@ -254,3 +254,19 @@ match :: Map (Spine datatype) (TxConstraint resolved script) -> TxConstraint resolved script match = MatchBySpine + +if' :: + forall (resolved :: Bool) script. + DSLPattern resolved script Bool -> + TxConstraint resolved script -> + TxConstraint resolved script -> + TxConstraint resolved script +if' = If + +eq' :: + forall x script. + (Prelude.Eq x) => + ConstraintDSL script x -> + ConstraintDSL script x -> + ConstraintDSL script Bool +eq' = Eq diff --git a/src/Cardano/CEM/Testing/StateMachine.hs b/src/Cardano/CEM/Testing/StateMachine.hs index e45d8a0..b6ba7c7 100644 --- a/src/Cardano/CEM/Testing/StateMachine.hs +++ b/src/Cardano/CEM/Testing/StateMachine.hs @@ -3,17 +3,37 @@ {-# HLINT ignore "Use fewer imports" #-} --- | Generic utils for using `quickcheck-dynamic` -module Cardano.CEM.Testing.StateMachine where - -import Prelude +{- | Model-based testing based on `quickcheck-dynamic`. +Main purpose of this kind of testing is to ensure that +OnChain code works the same way OffChain code does. +Additinally custom user invariants for OffChain code +can be tested using 'CEMScriptRunModel' type class. +-} +module Cardano.CEM.Testing.StateMachine ( + -- * Model + ScriptState (..), + ScriptStateParams (..), + TestConfig (..), + Action (..), + CEMScriptArbitrary (..), + + -- * SUT Implementation utils + CEMScriptRunModel (..), + runActionsInClb, + findSkForPKH, +) where import Cardano.Api (PaymentKey, SigningKey, TxId, Value) -import Cardano.CEM ( +import Cardano.CEM.DSL ( CEMScript, CEMScriptTypes (Params, State, Transition), + SameScriptArg (MkSameScriptArg), + TxConstraint (Noop, Utxo), + Utxo (SameScript), + UtxoKind (Out), + getMainSigner, + getMbMainSigner, ) -import Cardano.CEM.DSL (SameScriptArg (MkSameScriptArg), TxConstraint (Utxo), Utxo (SameScript), UtxoKind (Out), getMainSigner) import Cardano.CEM.Monads ( BlockchainMonadEvent (..), CEMAction (..), @@ -24,7 +44,12 @@ import Cardano.CEM.Monads ( TxSpec (..), ) import Cardano.CEM.Monads.CLB (ClbRunner, execOnIsolatedClb) -import Cardano.CEM.OffChain +import Cardano.CEM.OffChain ( + TxResolutionError (NoSignerError, UnhandledSubmittingError), + compileActionConstraints, + construct, + process, + ) import Cardano.CEM.OnChain (CEMScriptCompiled) import Cardano.Extras (signingKeyToPKH) import Clb (ClbT) @@ -39,7 +64,7 @@ import Data.Maybe (isJust, mapMaybe) import Data.Set qualified as Set import Data.Spine (HasSpine (..), deriveSpine) import PlutusLedgerApi.V1 (PubKeyHash) -import Test.QuickCheck +import Test.QuickCheck (Gen, Property, counterexample, ioProperty, label, tabulate) import Test.QuickCheck.DynamicLogic (DynLogicModel) import Test.QuickCheck.Gen qualified as Gen import Test.QuickCheck.Monadic (monadic) @@ -48,63 +73,69 @@ import Test.QuickCheck.StateModel ( Any (..), Generic, HasVariables (..), + LookUp, Realized, RunModel (..), StateModel (..), runActions, ) +import Test.QuickCheck.StateModel.Variables (Var, VarContext) import Text.Show.Pretty (ppShow) +import Prelude + +-- ----------------------------------------------------------------------------- +-- Mutations +-- ----------------------------------------------------------------------------- + +-- We use mutations to verify that on-chain and off-chain implementations +-- work the same way: +-- 1. The order of constrainsts doesn't matter +-- 2. All non-noop constraints are important - if we remove them both impls stop working. --- FIXME: add more mutations and documentation data TxMutation = RemoveConstraint {num :: Int} - | ShuffleConstraints - {shift :: Int} + | ShuffleConstraints {shift :: Int} deriving stock (Eq, Show) deriveSpine ''TxMutation -isNegativeMutation :: Maybe TxMutation -> Bool -isNegativeMutation Nothing = False -isNegativeMutation (Just (RemoveConstraint _)) = True -isNegativeMutation (Just (ShuffleConstraints {})) = False - -permute :: Int -> [a] -> [a] -permute num arr = - pms !! (num `mod` length pms) - where - pms = permutations arr +isNegativeMutation :: Maybe TxMutation -> [TxConstraint True script] -> Bool +isNegativeMutation Nothing _ = False +isNegativeMutation m@(Just (RemoveConstraint {})) cs = + case applyMutation m cs of + (_, Just Noop) -> False + _ -> True +isNegativeMutation (Just (ShuffleConstraints {})) _ = False applyMutation :: Maybe TxMutation -> [TxConstraint True script] -> - [TxConstraint True script] -applyMutation Nothing cs = cs + ([TxConstraint True script], Maybe (TxConstraint True script)) +applyMutation Nothing cs = (cs, Nothing) +-- \| Removes num+1 element from the list of constraints applyMutation (Just (RemoveConstraint num)) cs = - take num cs ++ tail (drop num cs) -applyMutation (Just (ShuffleConstraints shift)) cs = permute shift cs + (take num cs ++ tail (drop num cs), Just (cs !! num)) +applyMutation (Just (ShuffleConstraints shift)) cs = + (permute shift cs, Nothing) -data TestConfig = MkTestConfig - { actors :: [SigningKey PaymentKey] - , doMutationTesting :: Bool - } - deriving stock (Generic, Eq, Show) +permute :: Int -> [a] -> [a] +permute ind as = + perms !! (ind `mod` n) + where + perms = permutations as + n = length perms -data ScriptStateParams a = MkScriptStateParams - { config :: TestConfig - , params :: Params a - } - deriving stock (Generic) +-- ----------------------------------------------------------------------------- +-- The model +-- ----------------------------------------------------------------------------- -deriving stock instance (CEMScript a) => Eq (ScriptStateParams a) -deriving stock instance (CEMScript a) => Show (ScriptStateParams a) - -data ScriptState a +-- | Model: the ideal CEM script state. +data ScriptState script = Void | ConfigSet TestConfig | ScriptState - { dappParams :: ScriptStateParams a - , state :: Maybe (State a) + { dappParams :: ScriptStateParams script + , state :: Maybe (State script) , involvedActors :: Set.Set PubKeyHash , finished :: Bool } @@ -113,20 +144,43 @@ data ScriptState a deriving stock instance (CEMScript a) => Eq (ScriptState a) deriving stock instance (CEMScript a) => Show (ScriptState a) +data ScriptStateParams script = MkScriptStateParams + { config :: TestConfig + , params :: Params script + } + deriving stock (Generic) + +deriving stock instance (CEMScript a) => Eq (ScriptStateParams a) +deriving stock instance (CEMScript a) => Show (ScriptStateParams a) + +data TestConfig = MkTestConfig + { actors :: [SigningKey PaymentKey] + , doMutationTesting :: Bool + } + deriving stock (Generic, Eq, Show) + +-- We don't use symbolic variables so far. instance HasVariables (ScriptState a) where getAllVariables _ = Set.empty instance {-# OVERLAPS #-} HasVariables (Action (ScriptState script) a) where getAllVariables _ = Set.empty -class - (CEMScriptCompiled script) => - CEMScriptArbitrary script - where - arbitraryParams :: [SigningKey PaymentKey] -> Gen (Params script) +-- ----------------------------------------------------------------------------- +-- CEMScriptArbitrary & StateModel instance +-- ----------------------------------------------------------------------------- + +-- | Arbitrary for a CEM Script (compiled). +class (CEMScriptCompiled script) => CEMScriptArbitrary script where + arbitraryParams :: + [SigningKey PaymentKey] -> Gen (Params script) arbitraryTransition :: ScriptStateParams script -> Maybe (State script) -> Gen (Transition script) +{- | StateModel, which is QD model is basically our off-chain logic. +It delivers checks to `compileActionConstraints` from "Cardano.CEM.Offchain" +module. So `model === offchain`. +-} instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where data Action (ScriptState script) output where SetupConfig :: TestConfig -> Action (ScriptState script) () @@ -141,35 +195,56 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where initialState = Void - actionName (ScriptTransition transition _) = head . words . show $ transition actionName SetupConfig {} = "SetupConfig" actionName SetupParams {} = "SetupParams" + actionName (ScriptTransition transition _) = head . words . show $ transition + arbitraryAction :: + (CEMScriptArbitrary script) => + VarContext -> + ScriptState script -> + Gen (Any (Action (ScriptState script))) arbitraryAction _varCtx modelState = case modelState of - -- SetupConfig action should be called manually + -- SetupConfig action should be always called manually Void {} -> Gen.oneof [] - ConfigSet config -> - Some . SetupParams <$> arbitraryParams (actors config) - ScriptState {dappParams, state} -> - do - transition <- arbitraryTransition dappParams state - Some <$> (ScriptTransition transition <$> genMutation transition) - where - genMutation transition = - let cemAction = MkCEMAction (params dappParams) transition - in case compileActionConstraints state cemAction of - Right cs -> - Gen.oneof - [ return Nothing - , Just . RemoveConstraint - <$> Gen.chooseInt (0, length cs - 1) - , Just - <$> ( ShuffleConstraints - <$> Gen.chooseInt (1, length cs) - ) - ] - Left _ -> return Nothing - + ConfigSet config -> Some . SetupParams <$> arbitraryParams (actors config) + ScriptState + { dappParams = + dappParams@MkScriptStateParams + { config = MkTestConfig {doMutationTesting} + } + , state + } -> + do + transition <- arbitraryTransition dappParams state + Some <$> (ScriptTransition transition <$> genMutation transition) + where + genMutation :: Transition script -> Gen (Maybe TxMutation) + genMutation transition = + if doMutationTesting + then mutate + else return Nothing + where + mutate = + let cemAction = MkCEMAction (params dappParams) transition + in case compileActionConstraints state cemAction of + Right cs -> + Gen.oneof + [ return Nothing + , Just . RemoveConstraint + <$> Gen.chooseInt (0, length cs - 1) + , Just + <$> ( ShuffleConstraints + <$> Gen.chooseInt (1, length cs) + ) + ] + Left _ -> return Nothing + + precondition :: + (CEMScriptArbitrary script) => + ScriptState script -> + Action (ScriptState script) a -> + Bool precondition Void (SetupConfig {}) = True precondition (ConfigSet {}) (SetupParams {}) = True precondition @@ -180,16 +255,17 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where compiled = compileActionConstraints state cemAction in case compiled of - Right _ -> not finished && not (isNegativeMutation mutation) + Right cs -> not finished && not (isNegativeMutation mutation cs) Left _ -> False -- Unreachable precondition _ _ = False - -- Check on ScriptState and it fields is required for shrinking - validFailingAction (ScriptState {finished, state}) (ScriptTransition _ mutation) = - isNegativeMutation mutation && isJust state && not finished - validFailingAction _ _ = False - + nextState :: + (CEMScriptArbitrary script, Typeable a) => + ScriptState script -> + Action (ScriptState script) a -> + Var a -> + ScriptState script nextState Void (SetupConfig config) _var = ConfigSet config nextState (ConfigSet config) (SetupParams params) _var = ScriptState @@ -221,11 +297,33 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where [] -> Nothing _ -> error - "Scripts with >1 SameScript outputs are not supported by QD" + "Scripts with >1 SameScript outputs are not supported in CEM testing framework" f (Utxo Out (SameScript (MkSameScriptArg outState)) _) = Just outState f _ = Nothing nextState _ _ _ = error "Unreachable" + -- Precondition for filtering an Action that can meaningfully run + -- but is supposed to fail. + -- An action will run as a _negative_ action if the 'precondition' fails and + -- 'validFailingAction' succeeds. + -- A negative action should have _no effect_ on the model state. + -- This may not be desirable in all situations - in which case + -- one can override this semantics for book-keeping in 'failureNextState'. + validFailingAction :: + (CEMScriptArbitrary script) => + ScriptState script -> + Action (ScriptState script) a -> + Bool + validFailingAction + (ScriptState {dappParams, finished, state}) + (ScriptTransition transition mutation) = + let cemAction = MkCEMAction (params dappParams) transition + cs' = compileActionConstraints state cemAction + in case cs' of + Left _ -> True + Right cs -> isNegativeMutation mutation cs && isJust state && not finished + validFailingAction _ _ = False + instance (CEMScriptArbitrary script) => Show (Action (ScriptState script) a) where show (ScriptTransition t m) = "ScriptTransition " <> show t <> " mutated as " <> show m show (SetupConfig {}) = "SetupConfig" @@ -236,7 +334,9 @@ deriving stock instance instance (CEMScriptArbitrary script) => DynLogicModel (ScriptState script) +-- ----------------------------------------------------------------------------- -- RunModel +-- ----------------------------------------------------------------------------- type instance Realized (ClbT m) () = () @@ -250,6 +350,10 @@ class (CEMScriptArbitrary script) => CEMScriptRunModel script where Action (ScriptState script) () -> m () +{- | The SUT implementation is CLB-backed blockchain emulator. Here we execute +both offchain part and the onchain part also. That way we can assume that +`implementation === onchain`. +-} instance ( Realized m () ~ () , MonadIO m @@ -259,6 +363,18 @@ instance ) => RunModel (ScriptState script) m where + perform :: + ( Realized m () ~ () + , MonadIO m + , MonadSubmitTx m + , CEMScriptArbitrary script + , CEMScriptRunModel script + , Typeable a + ) => + ScriptState script -> + Action (ScriptState script) a -> + LookUp m -> + m (Either (Error (ScriptState script)) (Realized m a)) perform modelState action _lookup = do case (modelState, action) of (Void, SetupConfig {}) -> do @@ -271,20 +387,19 @@ instance , ScriptTransition transition mutation ) -> do _ <- performHook modelState action - bimap show (const ()) <$> mutatedResolveAndSubmit + bimap show (const ()) <$> mutateResolveAndSubmit where - -- This should work like `resolveAndSubmit` - -- FIXME: DRY it and move Mutations to main implementation - mutatedResolveAndSubmit :: m (Either TxResolutionError TxId) - mutatedResolveAndSubmit = runExceptT $ do + mutateResolveAndSubmit :: m (Either TxResolutionError TxId) + mutateResolveAndSubmit = runExceptT $ do let cemAction = MkCEMAction (params dappParams) transition - -- FIXME: refactor all ExceptT mess cs' <- ExceptT $ return $ compileActionConstraints state cemAction let - cs = applyMutation mutation cs' - signerPKH = getMainSigner cs - specSigner = - findSkForPKH (actors $ config dappParams) signerPKH + (cs, _) = applyMutation mutation cs' + mbSignerPKH = getMbMainSigner cs + -- \| TODO: can we delegate handling Nothing case to process/construct? + specSigner <- case mbSignerPKH of + Nothing -> ExceptT $ pure $ Left NoSignerError + Just signerPKH -> pure $ findSkForPKH (actors $ config dappParams) signerPKH resolutions <- mapM (process cemAction) cs let resolvedTx = (construct resolutions) {signer = specSigner} result <- @@ -295,13 +410,27 @@ instance logEvent $ SubmittedTxSpec spec (mapLeft (const ()) result) ExceptT $ return result - (_, _) -> error "Unreachable" - + (_, _) -> error "Unreachable branch of `perform`" + + monitoring :: + ( Realized m () ~ () + , MonadIO m + , MonadSubmitTx m + , CEMScriptArbitrary script + , CEMScriptRunModel script + ) => + (ScriptState script, ScriptState script) -> + Action (ScriptState script) a -> + LookUp m -> + Either (Error (ScriptState script)) (Realized m a) -> + Property -> + Property monitoring (stateFrom, stateTo) action _ _ prop = do tabMutations $ tabStateFrom $ labelIfFinished prop where isFinished (ScriptState {finished}) = finished isFinished _ = False + labelIfFinished :: Property -> Property labelIfFinished prop' = if isFinished stateTo then @@ -310,11 +439,13 @@ instance [show $ length $ involvedActors stateTo] $ label "Reached final state" prop' else prop' + tabStateFrom :: Property -> Property tabStateFrom prop' = case stateFrom of ScriptState {state} -> tabulate "States (from)" [show $ getSpine state] prop' _ -> prop' + tabMutations :: Property -> Property tabMutations prop' = case (stateFrom, action) of (ScriptState {dappParams}, ScriptTransition _ mutation) @@ -322,9 +453,11 @@ instance tabulate "Mutations" [show $ getSpine mutation] prop' _ -> prop' - monitoringFailure state _ _ err prop = + monitoringFailure state action _ err prop = counterexample - ( "In model state " + ( "Failed action is:\n" + <> ppShow action + <> "In model state:\n" <> ppShow state <> "\nGot error from emulator: " <> err diff --git a/test/CEM/Test/Auction.hs b/test/CEM/Test/Auction.hs index 40b8d74..daee676 100644 --- a/test/CEM/Test/Auction.hs +++ b/test/CEM/Test/Auction.hs @@ -255,5 +255,72 @@ auctionSpec = describe "AuctionSpec" $ do mEvent <- liftIO $ extractEvent @SimpleAuction network $ resolvedTxToOura preBody utxo liftIO $ mEvent `shouldBe` Just (Following BuyoutSpine) + -- stats <- perTransitionStats + -- liftIO $ putStrLn $ ppShow stats + + it "Zero bids flow" $ execClb $ do + seller <- (!! 0) <$> getTestWalletSks + + let + auctionParams = + MkAuctionParams + { seller = signingKeyToPKH seller + , lot = + assetClassValue + testNftAssetClass + 10 + } + + mintTestTokens seller 10 + + Nothing <- queryScriptState auctionParams + + submitAndCheck $ + MkTxSpec + { actions = + [ MkSomeCEMAction $ MkCEMAction auctionParams Create + ] + , specSigner = seller + } + + Just NotStarted <- queryScriptState auctionParams + + let + initBid = + MkBet + { better = signingKeyToPKH seller + , betAmount = 0 + } + + submitAndCheck $ + MkTxSpec + { actions = + [ MkSomeCEMAction $ + MkCEMAction auctionParams Start + ] + , specSigner = seller + } + + Just (CurrentBid currentBid') <- queryScriptState auctionParams + liftIO $ currentBid' `shouldBe` initBid + + submitAndCheck $ + MkTxSpec + { actions = + [ MkSomeCEMAction $ + MkCEMAction auctionParams Close + ] + , specSigner = seller + } + + submitAndCheck $ + MkTxSpec + { actions = + [ MkSomeCEMAction $ + MkCEMAction auctionParams Buyout + ] + , specSigner = seller + } + -- stats <- perTransitionStats -- liftIO $ putStrLn $ ppShow stats diff --git a/test/CEM/Test/Dynamic.hs b/test/CEM/Test/Dynamic.hs index cde74f7..21b9e97 100644 --- a/test/CEM/Test/Dynamic.hs +++ b/test/CEM/Test/Dynamic.hs @@ -7,13 +7,35 @@ import CEM.Example.Compiled () import CEM.Test.TestNFT (testNftAssetClass) import CEM.Test.Utils (execClb, mintTestTokens) import Cardano.Api (lovelaceToValue) -import Cardano.CEM -import Cardano.CEM.Testing.StateMachine +import Cardano.CEM (MonadTest (getTestWalletSks)) +import Cardano.CEM.Testing.StateMachine ( + Action (SetupConfig, SetupParams), + CEMScriptArbitrary (..), + CEMScriptRunModel (..), + ScriptState (ConfigSet), + ScriptStateParams (config), + TestConfig (MkTestConfig, actors, doMutationTesting), + findSkForPKH, + runActionsInClb, + ) import Cardano.Extras (signingKeyToPKH) import PlutusLedgerApi.V1.Value (assetClassValue) import Test.Hspec (describe, it, shouldBe) -import Test.QuickCheck -import Test.QuickCheck.DynamicLogic +import Test.QuickCheck ( + Property, + chooseInteger, + elements, + frequency, + isSuccess, + quickCheckResult, + withMaxSuccess, + ) +import Test.QuickCheck.DynamicLogic ( + DL, + action, + anyActions_, + forAllDL, + ) import Prelude -- Defining generic instances @@ -59,14 +81,10 @@ dynamicSpec = describe "Quickcheck Dynamic" $ do quickCheckDLScript $ do anyActions_ where - genesisValue = lovelaceToValue 300_000_000_000 - runDLScript dl = - forAllDL - dl - (runActionsInClb @SimpleAuction genesisValue) + quickCheckDLScript :: DL (ScriptState SimpleAuction) () -> IO () quickCheckDLScript dl = do actors <- execClb getTestWalletSks - result <- quickCheckResult $ runDLScript $ do + result <- quickCheckResult $ withMaxSuccess 100 $ runDLScript $ do _ <- action $ SetupConfig $ @@ -76,3 +94,11 @@ dynamicSpec = describe "Quickcheck Dynamic" $ do } dl isSuccess result `shouldBe` True + + runDLScript :: DL (ScriptState SimpleAuction) () -> Property + runDLScript dl = + forAllDL + dl + (runActionsInClb @SimpleAuction genesisValue) + + genesisValue = lovelaceToValue 300_000_000_000 diff --git a/test/Main.hs b/test/Main.hs index 45d241a..3b8b49a 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -7,7 +7,7 @@ import Data.Maybe (isJust) import Test.Hspec (hspec, runIO) import Prelude --- import CEM.Test.Dynamic (dynamicSpec) +import CEM.Test.Dynamic (dynamicSpec) import CEM.Test.OffChain (offChainSpec) import CEM.Test.OuraFilters.Simple (simpleSpec) import CEM.Test.Utils (clearLogs) @@ -21,7 +21,7 @@ main = do auctionSpec votingSpec offChainSpec - -- dynamicSpec + dynamicSpec if runIndexing then do -- These tests are not currently supported on CI