SCP-266 - Add linting for PartialPay and PartialDeposit (with constants)

marlowe-playground-client/src/Marlowe/Linter.purs

@@ -88,6 +88,7 @@ data WarningDetail
   | SimplifiableValue (Term Value) (Term Value)
   | SimplifiableObservation (Term Observation) (Term Observation)
   | PayBeforeDeposit Semantics.AccountId
+  | PartialPayment Semantics.AccountId Semantics.Token BigInteger BigInteger
 
 instance showWarningDetail :: Show WarningDetail where
   show NegativePayment = "The contract can make a non-positive payment"
@@ -101,7 +102,14 @@ instance showWarningDetail :: Show WarningDetail where
   show DivisionByZero = "Scale construct divides by zero"
   show (SimplifiableValue oriVal newVal) = "The value \"" <> (show oriVal) <> "\" can be simplified to \"" <> (show newVal) <> "\""
   show (SimplifiableObservation oriVal newVal) = "The observation \"" <> (show oriVal) <> "\" can be simplified to \"" <> (show newVal) <> "\""
-  show (PayBeforeDeposit account) = "The contract makes a payment to account " <> show account <> " before a deposit has been made"
+  show (PayBeforeDeposit account) = "The contract makes a payment from account " <> show account <> " before a deposit has been made"
+  show (PartialPayment accountId tokenId availableAmount demandedAmount) =
+    "The contract makes a payment of " <> show demandedAmount <> " "
+      <> show tokenId
+      <> " from account "
+      <> show accountId
+      <> " but the account only has "
+      <> show availableAmount
 
 derive instance genericWarningDetail :: Generic WarningDetail _
 
@@ -166,7 +174,7 @@ newtype LintEnv
   = LintEnv
   { letBindings :: Set Semantics.ValueId
   , maxTimeout :: MaxTimeout
-  , deposits :: Set (Semantics.AccountId /\ Semantics.Token)
+  , deposits :: Map (Semantics.AccountId /\ Semantics.Token) (Maybe BigInteger)
   }
 
 derive instance newtypeLintEnv :: Newtype LintEnv _
@@ -181,7 +189,7 @@ _letBindings = _Newtype <<< prop (SProxy :: SProxy "letBindings")
 _maxTimeout :: Lens' LintEnv (TermWrapper Slot)
 _maxTimeout = _Newtype <<< prop (SProxy :: SProxy "maxTimeout") <<< _Newtype
 
-_deposits :: Lens' LintEnv (Set (Semantics.AccountId /\ Semantics.Token))
+_deposits :: Lens' LintEnv (Map (Semantics.AccountId /\ Semantics.Token) (Maybe BigInteger))
 _deposits = _Newtype <<< prop (SProxy :: SProxy "deposits")
 
 data TemporarySimplification a b
@@ -235,14 +243,22 @@ constToObs false = Term FalseObs { row: 0, column: 0 }
 constToVal :: BigInteger -> Term Value
 constToVal x = Term (Constant x) { row: 0, column: 0 }
 
+addMoneyToEnvAccount :: BigInteger -> Semantics.AccountId -> Semantics.Token -> LintEnv -> LintEnv
+addMoneyToEnvAccount amountToAdd accTerm tokenTerm = over _deposits (Map.alter (addMoney amountToAdd) (accTerm /\ tokenTerm))
+  where
+  addMoney :: BigInteger -> Maybe (Maybe BigInteger) -> Maybe (Maybe BigInteger)
+  addMoney amount Nothing = Just (Just amount)
+
+  addMoney amount (Just prevVal) = Just (maybe Nothing (Just <<< (\prev -> prev + amount)) prevVal)
+
 -- | We lintContract through a contract term collecting all warnings and holes etc so that we can display them in the editor
 -- | The aim here is to only traverse the contract once since we are concerned about performance with the linting
 -- FIXME: There is a bug where if you create holes with the same name in different When blocks they are missing from
 -- the final lint result. After debugging it's strange because they seem to exist in intermediate states.
 lint :: Semantics.State -> Term Contract -> State
 lint contractState contract = state
   where
-  deposits = contractState ^. (_accounts <<< to Map.keys)
+  deposits = contractState ^. (_accounts <<< to (Map.mapMaybe (Just <<< Just)))
 
   bindings = contractState ^. (_boundValues <<< to Map.keys)
 
@@ -258,19 +274,38 @@ lintContract env t@(Term (Pay acc payee token payment cont) pos) = do
     gatherHoles = getHoles acc <> getHoles payee <> getHoles token
   modifying _holes gatherHoles
   sa <- lintValue env payment
-  case sa of
+  payedValue <- case sa of
     (ConstantSimp _ _ c)
-      | c <= zero -> addWarning NegativePayment t pos
-    _ -> pure unit
+      | c <= zero -> do
+        addWarning NegativePayment t pos
+        pure (Just zero)
+      | otherwise -> pure (Just c)
+    _ -> pure Nothing
   markSimplification constToVal SimplifiableValue payment sa
-  case (fromTerm acc /\ fromTerm token) of
+  newEnv <- case (fromTerm acc /\ fromTerm token) of
     Just accTerm /\ Just tokenTerm -> do
       let
         deposits = view _deposits env
-      unless (Set.member (accTerm /\ tokenTerm) deposits)
+
+        key = accTerm /\ tokenTerm
+      unless (Map.member key deposits)
         (addWarning (PayBeforeDeposit accTerm) t pos)
-    _ -> pure unit
-  lintContract env cont
+      case (Map.lookup key deposits /\ payedValue) of
+        (Just (Just avMoney)) /\ (Just paidMoney) -> do
+          unless (avMoney >= paidMoney) (addWarning (PartialPayment accTerm tokenTerm avMoney paidMoney) t pos)
+          let
+            actualPaidMoney = max (avMoney - paidMoney) zero
+          let
+            tempEnv = over _deposits (Map.insert key (Just actualPaidMoney)) env
+          pure
+            ( case fromTerm payee of
+                Just (Semantics.Account newAcc) -> addMoneyToEnvAccount actualPaidMoney newAcc tokenTerm tempEnv
+                _ -> tempEnv
+            )
+        Nothing /\ _ -> pure env
+        _ -> pure (over _deposits (Map.insert key Nothing) env)
+    _ -> pure env
+  lintContract newEnv cont
 
 lintContract env (Term (If obs c1 c2) _) = do
   sa <- lintObservation env obs
@@ -539,15 +574,17 @@ lintValue env t@(Term (Cond c a b) pos) = do
       pure (ValueSimp pos false t)
 
 data Effect
-  = ConstantDeposit Semantics.AccountId Semantics.Token
+  = ConstantDeposit Semantics.AccountId Semantics.Token BigInteger
+  | UnknownDeposit Semantics.AccountId Semantics.Token
   | NoEffect
 
 lintCase :: LintEnv -> Term Case -> CMS.State State Unit
 lintCase env t@(Term (Case action contract) pos) = do
   effect <- lintAction env action
   let
     newEnv = case effect of
-      ConstantDeposit accTerm tokenTerm -> over _deposits (Set.insert (accTerm /\ tokenTerm)) env
+      ConstantDeposit accTerm tokenTerm amount -> addMoneyToEnvAccount amount accTerm tokenTerm env
+      UnknownDeposit accTerm tokenTerm -> over _deposits (Map.insert (accTerm /\ tokenTerm) Nothing) env
       NoEffect -> env
   lintContract newEnv contract
   pure unit
@@ -559,7 +596,7 @@ lintCase env hole@(Hole _ _ _) = do
 lintAction :: LintEnv -> Term Action -> CMS.State State Effect
 lintAction env t@(Term (Deposit acc party token value) pos) = do
   let
-    accTerm = maybe NoEffect (maybe (const NoEffect) ConstantDeposit (fromTerm acc)) (fromTerm token)
+    accTerm = maybe NoEffect (maybe (const NoEffect) UnknownDeposit (fromTerm acc)) (fromTerm token)
 
     gatherHoles = getHoles acc <> getHoles party <> getHoles token
   modifying _holes (gatherHoles)
@@ -568,10 +605,17 @@ lintAction env t@(Term (Deposit acc party token value) pos) = do
     (ConstantSimp _ _ v)
       | v <= zero -> do
         addWarning NegativeDeposit t pos
-        pure accTerm
+        pure (makeDepositConstant accTerm zero)
+      | otherwise -> do
+        markSimplification constToVal SimplifiableValue value sa
+        pure (makeDepositConstant accTerm v)
     _ -> do
       markSimplification constToVal SimplifiableValue value sa
       pure accTerm
+  where
+  makeDepositConstant (UnknownDeposit ac to) v = ConstantDeposit ac to v
+
+  makeDepositConstant other _ = other
 
 lintAction env t@(Term (Choice choiceId bounds) pos) = do
   modifying _holes (getHoles choiceId <> getHoles bounds)

marlowe-playground-client/test/Marlowe/LintTests.purs

@@ -2,6 +2,7 @@ module Marlowe.LintTests where
 
 import Prelude
 import Data.Array (singleton)
+import Data.BigInteger (fromInt)
 import Data.Either (Either(..))
 import Data.Map as Map
 import Data.Set (toUnfoldable)
@@ -314,12 +315,12 @@ negativePay :: Test
 negativePay = testWarningSimple (payContract "(Constant -1)") "The contract can make a non-positive payment"
 
 payBeforeWarning :: Test
-payBeforeWarning = testWarningSimple contract "The contract makes a payment to account (AccountId 0 (Role \"role\")) before a deposit has been made"
+payBeforeWarning = testWarningSimple contract "The contract makes a payment from account (AccountId 0 (Role \"role\")) before a deposit has been made"
   where
   contract = "When [Case (Deposit (AccountId 1 (Role \"role\") ) (Role \"role\") (Token \"\" \"\") (Constant 100)) (Pay (AccountId 0 (Role \"role\")) (Party (Role \"role\")) (Token \"\" \"\") (Constant 1) Close)] 10 Close"
 
 payBeforeWarningBranch :: Test
-payBeforeWarningBranch = testWarningSimple contract "The contract makes a payment to account (AccountId 1 (Role \"role\")) before a deposit has been made"
+payBeforeWarningBranch = testWarningSimple contract "The contract makes a payment from account (AccountId 1 (Role \"role\")) before a deposit has been made"
   where
   contract = "When [Case (Deposit (AccountId 1 (Role \"role\")) (Role \"role\") (Token \"\" \"\") (Constant 10)) Close] 2 (Pay (AccountId 1 (Role \"role\")) (Party (Role \"role\")) (Token \"\" \"\") (Constant 10) Close)"
 
@@ -341,7 +342,7 @@ depositFromState =
 
     state =
       S.State
-        { accounts: Map.singleton (Tuple accountId (Token "" "")) zero
+        { accounts: Map.singleton (Tuple accountId (Token "" "")) (fromInt 10)
         , choices: mempty
         , boundValues: mempty
         , minSlot: zero