Merge pull request #113 from mlabs-haskell/euonymos/dynamic-test

Improve quickcheck-dynamic tests for CEM Script

Author: euonymos

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
 

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,21 +124,29 @@ 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 ctxParams.seller)
-                (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.betAmount)
-            , output
-                (userUtxo buyoutBid.better)
-                (cMinLovelace @<> ctxParams.lot)
+                (userUtxo buyoutBid.bidder) -- NOTE: initial zero bidder is seller
+                auctionValue
+            , if'
+                (ctxParams.seller `eq'` buyoutBid.bidder)
+                noop
+                ( output
+                  (userUtxo ctxParams.seller)
+                  (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.bidAmount)
+                )
             ]
           )
         ]

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

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)

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 ::

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