From 1c1cc0d0afd969e436fba31f4c9818cacdf4e1d6 Mon Sep 17 00:00:00 2001 From: Gregory Gerasev Date: Tue, 19 Mar 2024 00:38:54 +0700 Subject: [PATCH 1/5] WIP --- docs/goals_and_soa.md | 97 +++++++++++++++++++++++++++++++++---------- 1 file changed, 75 insertions(+), 22 deletions(-) diff --git a/docs/goals_and_soa.md b/docs/goals_and_soa.md index 320f4d3..f9f0499 100644 --- a/docs/goals_and_soa.md +++ b/docs/goals_and_soa.md @@ -48,7 +48,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 @@ -56,8 +56,6 @@ what we use to demonstrate problems in following: * Plutonomicon patterns * plutus-usecases -@todo #3: Add more links to specific bugs and code size blowups in existing DApps. - ## On-chain correctness ### Known common vulnerabilities @@ -77,27 +75,36 @@ 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: * https://github.com/mlabs-haskell/hydra-auction/issues/146 -Another important case is maintaining invariants -of token value or immutable UTxOs. -Such kind of constraints naturally lead to script -for which more performant implementation should -eliminate some constraint following from others. -Such kind of manual SMT solving exercises are -known source for security bugs and complicated code. - Making Plutus contract invariant to `TxIn` ordering and participation in multi-script scenarios lead to similar kind of complications. @@ -106,6 +113,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. ### Single script safety and liveliness @@ -169,6 +179,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 @@ -195,15 +218,38 @@ is much less obvious to implement, and out of scope of current Catalyst project, but it is very much possible feature as well. -### On-/Off-chain and spec code duplication +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 @todo #3: Add more off-chain code duplication examples from existing PABs. Include problems with querying coin-selection, tests, retrying and errors. -### 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. ### Common backend features @@ -274,12 +320,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 From 6fece23ef3c5b643be9f4684f0fac0cea9caa31c Mon Sep 17 00:00:00 2001 From: euonymos Date: Tue, 17 Dec 2024 16:25:50 -0600 Subject: [PATCH 2/5] fix: dynamic test is green, but without mutations --- example/CEM/Example/Auction.hs | 23 ++- src/Cardano/CEM/DSL.hs | 2 +- src/Cardano/CEM/Smart.hs | 22 ++- src/Cardano/CEM/Testing/StateMachine.hs | 203 +++++++++++++++++------- test/CEM/Test/Auction.hs | 67 ++++++++ test/CEM/Test/Dynamic.hs | 16 +- test/Main.hs | 4 +- 7 files changed, 259 insertions(+), 78 deletions(-) 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..4e8f93c 100644 --- a/src/Cardano/CEM/DSL.hs +++ b/src/Cardano/CEM/DSL.hs @@ -298,7 +298,7 @@ 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 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..04bf940 100644 --- a/src/Cardano/CEM/Testing/StateMachine.hs +++ b/src/Cardano/CEM/Testing/StateMachine.hs @@ -6,14 +6,16 @@ -- | Generic utils for using `quickcheck-dynamic` module Cardano.CEM.Testing.StateMachine where -import Prelude - import Cardano.Api (PaymentKey, SigningKey, TxId, Value) -import Cardano.CEM ( +import Cardano.CEM.DSL ( CEMScript, CEMScriptTypes (Params, State, Transition), + SameScriptArg (MkSameScriptArg), + TxConstraint (Utxo), + Utxo (SameScript), + UtxoKind (Out), + getMainSigner, ) -import Cardano.CEM.DSL (SameScriptArg (MkSameScriptArg), TxConstraint (Utxo), Utxo (SameScript), UtxoKind (Out), getMainSigner) import Cardano.CEM.Monads ( BlockchainMonadEvent (..), CEMAction (..), @@ -24,7 +26,12 @@ import Cardano.CEM.Monads ( TxSpec (..), ) import Cardano.CEM.Monads.CLB (ClbRunner, execOnIsolatedClb) -import Cardano.CEM.OffChain +import Cardano.CEM.OffChain ( + TxResolutionError (UnhandledSubmittingError), + compileActionConstraints, + construct, + process, + ) import Cardano.CEM.OnChain (CEMScriptCompiled) import Cardano.Extras (signingKeyToPKH) import Clb (ClbT) @@ -39,7 +46,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,14 +55,20 @@ 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 +-- ----------------------------------------------------------------------------- --- FIXME: add more mutations and documentation data TxMutation = RemoveConstraint {num :: Int} | ShuffleConstraints @@ -70,41 +83,33 @@ isNegativeMutation (Just (RemoveConstraint _)) = True isNegativeMutation (Just (ShuffleConstraints {})) = False permute :: Int -> [a] -> [a] -permute num arr = - pms !! (num `mod` length pms) +permute ind as = + perms !! (ind `mod` n) where - pms = permutations arr + perms = permutations as + n = length perms applyMutation :: Maybe TxMutation -> [TxConstraint True script] -> [TxConstraint True script] applyMutation Nothing cs = cs -applyMutation (Just (RemoveConstraint num)) cs = - take num cs ++ tail (drop num cs) +applyMutation (Just (RemoveConstraint _num)) cs = + -- take num cs ++ tail (drop num cs) + cs applyMutation (Just (ShuffleConstraints shift)) cs = permute shift cs -data TestConfig = MkTestConfig - { actors :: [SigningKey PaymentKey] - , doMutationTesting :: Bool - } - deriving stock (Generic, Eq, Show) - -data ScriptStateParams a = MkScriptStateParams - { config :: TestConfig - , params :: Params a - } - deriving stock (Generic) - -deriving stock instance (CEMScript a) => Eq (ScriptStateParams a) -deriving stock instance (CEMScript a) => Show (ScriptStateParams a) +-- ----------------------------------------------------------------------------- +-- The model +-- ----------------------------------------------------------------------------- -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,17 +118,35 @@ 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 +-- ----------------------------------------------------------------------------- + +class (CEMScriptCompiled script) => CEMScriptArbitrary script where + arbitraryParams :: + [SigningKey PaymentKey] -> Gen (Params script) arbitraryTransition :: ScriptStateParams script -> Maybe (State script) -> Gen (Transition script) @@ -141,35 +164,47 @@ 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 Void {} -> Gen.oneof [] - ConfigSet config -> - Some . SetupParams <$> arbitraryParams (actors config) + ConfigSet config -> Some . SetupParams <$> arbitraryParams (actors config) ScriptState {dappParams, state} -> do transition <- arbitraryTransition dappParams state Some <$> (ScriptTransition transition <$> genMutation transition) where + genMutation :: Transition script -> Gen (Maybe TxMutation) 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 - + return Nothing + + -- 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 +215,17 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where compiled = compileActionConstraints state cemAction in case compiled of - Right _ -> not finished && not (isNegativeMutation mutation) + Right _ -> not finished && not (isNegativeMutation mutation) -- FIXME: why not isNegative 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 +257,26 @@ 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 {finished, state}) (ScriptTransition _ mutation) = + isNegativeMutation mutation && 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 +287,9 @@ deriving stock instance instance (CEMScriptArbitrary script) => DynLogicModel (ScriptState script) +-- ----------------------------------------------------------------------------- -- RunModel +-- ----------------------------------------------------------------------------- type instance Realized (ClbT m) () = () @@ -259,6 +312,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 @@ -297,11 +362,25 @@ instance ExceptT $ return result (_, _) -> error "Unreachable" + 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 +389,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 +403,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..d33a7a2 100644 --- a/test/CEM/Test/Dynamic.hs +++ b/test/CEM/Test/Dynamic.hs @@ -59,11 +59,7 @@ 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 @@ -72,7 +68,15 @@ dynamicSpec = describe "Quickcheck Dynamic" $ do SetupConfig $ MkTestConfig { actors - , doMutationTesting = True + , doMutationTesting = False } 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 From 836389a0578975bd644d97fbdbec938039dc3ff7 Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 19 Dec 2024 12:55:56 -0600 Subject: [PATCH 3/5] feat: rethink negative mutations --- src/Cardano/CEM/DSL.hs | 13 ++ src/Cardano/CEM/Monads.hs | 2 +- src/Cardano/CEM/OffChain.hs | 9 +- src/Cardano/CEM/Testing/StateMachine.hs | 166 +++++++++++++++--------- test/CEM/Test/Dynamic.hs | 34 ++++- 5 files changed, 155 insertions(+), 69 deletions(-) diff --git a/src/Cardano/CEM/DSL.hs b/src/Cardano/CEM/DSL.hs index 4e8f93c..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 (..), @@ -304,6 +305,18 @@ getMainSigner cs = case mapMaybe f cs of 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 + f _ = Nothing + -- ----------------------------------------------------------------------------- -- Main CEM Script API -- ----------------------------------------------------------------------------- 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..af97419 100644 --- a/src/Cardano/CEM/OffChain.hs +++ b/src/Cardano/CEM/OffChain.hs @@ -57,6 +57,7 @@ import Data.Map qualified as Map import Data.Maybe (fromJust) import Data.Singletons (sing) import Data.Spine (HasSpine (..)) +import Debug.Trace (traceShowId) import Plutarch (Config (..), (#)) import Plutarch.Evaluate (evalTerm) import Plutarch.Lift (pconstant, plift) @@ -138,8 +139,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 +197,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 +208,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 +218,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 diff --git a/src/Cardano/CEM/Testing/StateMachine.hs b/src/Cardano/CEM/Testing/StateMachine.hs index 04bf940..8b8758b 100644 --- a/src/Cardano/CEM/Testing/StateMachine.hs +++ b/src/Cardano/CEM/Testing/StateMachine.hs @@ -3,18 +3,36 @@ {-# HLINT ignore "Use fewer imports" #-} --- | Generic utils for using `quickcheck-dynamic` -module Cardano.CEM.Testing.StateMachine where +{- | 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.DSL ( CEMScript, CEMScriptTypes (Params, State, Transition), SameScriptArg (MkSameScriptArg), - TxConstraint (Utxo), + TxConstraint (Noop, Utxo), Utxo (SameScript), UtxoKind (Out), getMainSigner, + getMbMainSigner, ) import Cardano.CEM.Monads ( BlockchainMonadEvent (..), @@ -27,7 +45,7 @@ import Cardano.CEM.Monads ( ) import Cardano.CEM.Monads.CLB (ClbRunner, execOnIsolatedClb) import Cardano.CEM.OffChain ( - TxResolutionError (UnhandledSubmittingError), + TxResolutionError (CEMScriptTxInResolutionError, UnhandledSubmittingError), compileActionConstraints, construct, process, @@ -69,18 +87,36 @@ 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. + 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 +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], 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), Just (cs !! num)) +applyMutation (Just (ShuffleConstraints shift)) cs = + (permute shift cs, Nothing) permute :: Int -> [a] -> [a] permute ind as = @@ -89,16 +125,6 @@ permute ind as = perms = permutations as n = length perms -applyMutation :: - Maybe TxMutation -> - [TxConstraint True script] -> - [TxConstraint True script] -applyMutation Nothing cs = cs -applyMutation (Just (RemoveConstraint _num)) cs = - -- take num cs ++ tail (drop num cs) - cs -applyMutation (Just (ShuffleConstraints shift)) cs = permute shift cs - -- ----------------------------------------------------------------------------- -- The model -- ----------------------------------------------------------------------------- @@ -144,12 +170,17 @@ instance {-# OVERLAPS #-} HasVariables (Action (ScriptState script) a) where -- 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) () @@ -174,31 +205,40 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where 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 script -> Gen (Maybe TxMutation) - genMutation transition = - return Nothing - - -- 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 + 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) => @@ -215,7 +255,7 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where compiled = compileActionConstraints state cemAction in case compiled of - Right _ -> not finished && not (isNegativeMutation mutation) -- FIXME: why not isNegative + Right cs -> not finished && not (isNegativeMutation mutation cs) Left _ -> False -- Unreachable precondition _ _ = False @@ -262,7 +302,8 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where f _ = Nothing nextState _ _ _ = error "Unreachable" - -- Precondition for filtering an Action that can meaningfully run but is supposed to fail. + -- 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. @@ -273,8 +314,14 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where ScriptState script -> Action (ScriptState script) a -> Bool - validFailingAction (ScriptState {finished, state}) (ScriptTransition _ mutation) = - isNegativeMutation mutation && isJust state && not finished + 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 @@ -303,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 @@ -336,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 + -- \| FIXME: can we delegate handling Nothing case to process/construct? + specSigner <- case mbSignerPKH of + Nothing -> ExceptT $ pure $ Left CEMScriptTxInResolutionError -- FIXME: + Just signerPKH -> pure $ findSkForPKH (actors $ config dappParams) signerPKH resolutions <- mapM (process cemAction) cs let resolvedTx = (construct resolutions) {signer = specSigner} result <- @@ -360,7 +410,7 @@ instance logEvent $ SubmittedTxSpec spec (mapLeft (const ()) result) ExceptT $ return result - (_, _) -> error "Unreachable" + (_, _) -> error "Unreachable branch of `perform`" monitoring :: ( Realized m () ~ () diff --git a/test/CEM/Test/Dynamic.hs b/test/CEM/Test/Dynamic.hs index d33a7a2..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 @@ -62,13 +84,13 @@ dynamicSpec = describe "Quickcheck Dynamic" $ do quickCheckDLScript :: DL (ScriptState SimpleAuction) () -> IO () quickCheckDLScript dl = do actors <- execClb getTestWalletSks - result <- quickCheckResult $ runDLScript $ do + result <- quickCheckResult $ withMaxSuccess 100 $ runDLScript $ do _ <- action $ SetupConfig $ MkTestConfig { actors - , doMutationTesting = False + , doMutationTesting = True } dl isSuccess result `shouldBe` True From 8ce26d6d74ac2621fcaaf0b814dad7eeb3aacc53 Mon Sep 17 00:00:00 2001 From: euonymos Date: Thu, 19 Dec 2024 13:02:01 -0600 Subject: [PATCH 4/5] chore: fix imports and comments --- src/Cardano/CEM/OffChain.hs | 9 ++++----- src/Cardano/CEM/Testing/StateMachine.hs | 6 +++--- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Cardano/CEM/OffChain.hs b/src/Cardano/CEM/OffChain.hs index af97419..c3b9b16 100644 --- a/src/Cardano/CEM/OffChain.hs +++ b/src/Cardano/CEM/OffChain.hs @@ -57,7 +57,6 @@ import Data.Map qualified as Map import Data.Maybe (fromJust) import Data.Singletons (sing) import Data.Spine (HasSpine (..)) -import Debug.Trace (traceShowId) import Plutarch (Config (..), (#)) import Plutarch.Evaluate (evalTerm) import Plutarch.Lift (pconstant, plift) @@ -265,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/Testing/StateMachine.hs b/src/Cardano/CEM/Testing/StateMachine.hs index 8b8758b..b6ba7c7 100644 --- a/src/Cardano/CEM/Testing/StateMachine.hs +++ b/src/Cardano/CEM/Testing/StateMachine.hs @@ -45,7 +45,7 @@ import Cardano.CEM.Monads ( ) import Cardano.CEM.Monads.CLB (ClbRunner, execOnIsolatedClb) import Cardano.CEM.OffChain ( - TxResolutionError (CEMScriptTxInResolutionError, UnhandledSubmittingError), + TxResolutionError (NoSignerError, UnhandledSubmittingError), compileActionConstraints, construct, process, @@ -396,9 +396,9 @@ instance let (cs, _) = applyMutation mutation cs' mbSignerPKH = getMbMainSigner cs - -- \| FIXME: can we delegate handling Nothing case to process/construct? + -- \| TODO: can we delegate handling Nothing case to process/construct? specSigner <- case mbSignerPKH of - Nothing -> ExceptT $ pure $ Left CEMScriptTxInResolutionError -- FIXME: + Nothing -> ExceptT $ pure $ Left NoSignerError Just signerPKH -> pure $ findSkForPKH (actors $ config dappParams) signerPKH resolutions <- mapM (process cemAction) cs let resolvedTx = (construct resolutions) {signer = specSigner} From 79fc3b6e725f07b910ac004428f17b07bdf52a6b Mon Sep 17 00:00:00 2001 From: euonymos Date: Fri, 17 Jan 2025 12:51:59 -0600 Subject: [PATCH 5/5] chore: cosmetics --- example/CEM/Example/Auction.hs | 45 ++++++++++++------------- src/Cardano/CEM/Testing/StateMachine.hs | 3 +- test/CEM/Test/Auction.hs | 24 ++++++------- test/CEM/Test/Dynamic.hs | 2 +- 4 files changed, 36 insertions(+), 38 deletions(-) diff --git a/example/CEM/Example/Auction.hs b/example/CEM/Example/Auction.hs index 758a476..7118506 100644 --- a/example/CEM/Example/Auction.hs +++ b/example/CEM/Example/Auction.hs @@ -16,8 +16,8 @@ data SimpleAuction -- | A bid data Bid = MkBet - { better :: PubKeyHash - , betAmount :: Integer + { bidder :: PubKeyHash -- FIXME: rename to bidder + , bidAmount :: Integer -- FIXME: rename to bidder } deriving stock (Prelude.Eq, Prelude.Show) @@ -69,8 +69,8 @@ instance CEMScript SimpleAuction where initialBid = cOfSpine MkBetSpine - [ #better ::= ctxParams.seller - , #betAmount ::= lift 0 + [ #bidder ::= ctxParams.seller + , #bidAmount ::= lift 0 ] auctionValue = cMinLovelace @<> ctxParams.lot @@ -96,7 +96,7 @@ instance CEMScript SimpleAuction where , [ input (ownUtxo $ inState CurrentBidSpine) auctionValue , byFlagError - (ctxTransition.bid.betAmount @<= ctxState.bid.betAmount) + (ctxTransition.bid.bidAmount @<= ctxState.bid.bidAmount) "Bid amount is less or equal to current bid" , output ( ownUtxo @@ -105,7 +105,7 @@ instance CEMScript SimpleAuction where [#bid ::= ctxTransition.bid] ) auctionValue - , signedBy ctxTransition.bid.better + , signedBy ctxTransition.bid.bidder ] ) , @@ -124,31 +124,28 @@ instance CEMScript SimpleAuction where ( BuyoutSpine , [ input (ownUtxo $ inState WinnerSpine) auctionValue + , byFlagError (lift False) "Some err" + , byFlagError (lift False) "Another err" , -- Example: In constraints redundant for on-chain offchainOnly - ( spentBy - buyoutBid.better - ( cMkAdaOnlyValue buyoutBid.betAmount - @<> cMinLovelace - ) + (if' + (ctxParams.seller `eq'` buyoutBid.bidder) + (signedBy ctxParams.seller) + (spentBy + buyoutBid.bidder + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) cEmptyValue + ) ) + , output + (userUtxo buyoutBid.bidder) -- NOTE: initial zero bidder is seller + auctionValue , 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) + (ctxParams.seller `eq'` buyoutBid.bidder) noop ( output - (userUtxo ctxParams.seller) - (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.betAmount) + (userUtxo ctxParams.seller) + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount) ) ] ) diff --git a/src/Cardano/CEM/Testing/StateMachine.hs b/src/Cardano/CEM/Testing/StateMachine.hs index b6ba7c7..4ac6cbd 100644 --- a/src/Cardano/CEM/Testing/StateMachine.hs +++ b/src/Cardano/CEM/Testing/StateMachine.hs @@ -90,7 +90,7 @@ import Prelude -- 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. +-- 2. All non-noop constraints are important - if we remove any the app stops working. data TxMutation = RemoveConstraint {num :: Int} @@ -110,6 +110,7 @@ isNegativeMutation (Just (ShuffleConstraints {})) _ = False applyMutation :: Maybe TxMutation -> [TxConstraint True script] -> + -- (mutated, maybe removed constraint) ([TxConstraint True script], Maybe (TxConstraint True script)) applyMutation Nothing cs = (cs, Nothing) -- \| Removes num+1 element from the list of constraints diff --git a/test/CEM/Test/Auction.hs b/test/CEM/Test/Auction.hs index daee676..63b6270 100644 --- a/test/CEM/Test/Auction.hs +++ b/test/CEM/Test/Auction.hs @@ -58,8 +58,8 @@ auctionSpec = describe "AuctionSpec" $ do let bid1 = MkBet - { better = signingKeyToPKH bidder1 - , betAmount = 1_000_000 + { bidder = signingKeyToPKH bidder1 + , bidAmount = 1_000_000 } result <- @@ -111,8 +111,8 @@ auctionSpec = describe "AuctionSpec" $ do let bid1 = MkBet - { better = signingKeyToPKH bidder1 - , betAmount = 0 + { bidder = signingKeyToPKH bidder1 + , bidAmount = 0 } result <- @@ -164,18 +164,18 @@ auctionSpec = describe "AuctionSpec" $ do let initBid = MkBet - { better = signingKeyToPKH seller - , betAmount = 0 + { bidder = signingKeyToPKH seller + , bidAmount = 0 } bid1 = MkBet - { better = signingKeyToPKH bidder1 - , betAmount = 3_000_000 + { bidder = signingKeyToPKH bidder1 + , bidAmount = 3_000_000 } bid2 = MkBet - { better = signingKeyToPKH bidder1 - , betAmount = 4_000_000 + { bidder = signingKeyToPKH bidder1 + , bidAmount = 4_000_000 } (preBody, utxo) <- @@ -288,8 +288,8 @@ auctionSpec = describe "AuctionSpec" $ do let initBid = MkBet - { better = signingKeyToPKH seller - , betAmount = 0 + { bidder = signingKeyToPKH seller + , bidAmount = 0 } submitAndCheck $ diff --git a/test/CEM/Test/Dynamic.hs b/test/CEM/Test/Dynamic.hs index 21b9e97..d773c0c 100644 --- a/test/CEM/Test/Dynamic.hs +++ b/test/CEM/Test/Dynamic.hs @@ -63,7 +63,7 @@ instance CEMScriptArbitrary SimpleAuction where Just (Winner {}) -> return Buyout where genBidder = elements (map signingKeyToPKH $ actors $ config dappParams) - genBid bid = (betAmount bid +) <$> chooseInteger (0, 100_500) + genBid bid = (bidAmount bid +) <$> chooseInteger (0, 100_500) instance CEMScriptRunModel SimpleAuction where performHook