SCP-5141 SCP-5142 Enforced initial and final state validity in valida…

…tor.
input-output-hk · Mar 15, 2023 · 8855fea · 8855fea
1 parent e10be6d
commit 8855fea
Show file tree

Hide file tree

Showing 6 changed files with 82 additions and 29 deletions.
diff --git a/marlowe-test/src/Spec/Marlowe/Marlowe.hs b/marlowe-test/src/Spec/Marlowe/Marlowe.hs
@@ -150,14 +150,14 @@ alternateMarloweValidatorSize :: IO ()
 alternateMarloweValidatorSize = do
     let validator = Scripts.validatorScript alternateMarloweValidator
     let vsize = SBS.length . SBS.toShort . LB.toStrict $ Serialise.serialise validator
-    assertBool ("alternateMarloweValidator is too large " <> show vsize) (vsize <= 15349)
+    assertBool ("alternateMarloweValidator is too large " <> show vsize) (vsize <= 14869)
 
 -- | Test that the untyped validator is not too large.
 marloweValidatorSize :: IO ()
 marloweValidatorSize = do
     let validator = Scripts.validatorScript marloweValidator
     let vsize = SBS.length . SBS.toShort . LB.toStrict $ Serialise.serialise validator
-    assertBool ("marloweValidator is too large " <> show vsize) (vsize <= 12242)
+    assertBool ("marloweValidator is too large " <> show vsize) (vsize <= 12347)
 
 
 -- | Test `extractNonMerkleizedContractRoles`.

diff --git a/marlowe-test/src/Spec/Marlowe/Plutus/Specification.hs b/marlowe-test/src/Spec/Marlowe/Plutus/Specification.hs
@@ -195,7 +195,7 @@ tests referencePaths =
               -- DO NOT ALTER THE FOLLOWING VALUE UNLESS YOU ARE COMMITTING
               -- APPROVED CHANGES TO MARLOWE'S SEMANTICS VALIDATOR. THIS HASH
               -- HAS IMPLICATIONS FOR VERSIONING, AUDIT, AND CONTRACT DISCOVERY.
-              "8099cd4eafbe7187b6513adcdb01ea3719296f614b07945a5462b408"
+              "a7cc35084607dab02a50761ca15f6192d0c2ffe12f0d22263fa3f286"
         ]
     , testGroup "Payout Validator"
         [

diff --git a/marlowe/CHANGELOG.md b/marlowe/CHANGELOG.md
@@ -34,3 +34,8 @@ Based on audit findings, we added "Constraint 18. Final balance" to the Marlowe-
 ## SCP-5143: Removed tracing from validator
 
 In order to reduces the validator size, calls to Plutus tracing functions were removed.
+
+
+## SCP-5141: Valid initial and final states
+
+Based on audit finds, we added "Constraint 19. No duplicates" to the Marlowe-Cardano specification and require that the validator ensure that both the intial and final states of the contract obey the invariants of correct total value, positive balances, and non-duplication of keys for accounts, choices, and bound values.
diff --git a/marlowe/debugging-cookbook.md b/marlowe/debugging-cookbook.md
@@ -100,16 +100,24 @@ Transaction failures occur in either phase 1 validation (ledger rules) or phase
 
 *   If a transaction fails phase two validation, a terse Marlowe error will be reported in the Plutus trace log:
     *   `"a"`: The slot/time validity range for the transaction is infinite or semi-infinite. The range should be finite/bounded.
-    *   `"b"`: All accounts must have positive balances.
+    *   `"bi"`: All accounts must have positive balances in the initial state.
+    *   `"bo"`: All accounts must have positive balances in the final state.
     *   `"c"`: A transaction containing a contract that closes may not also include the creation of a new contract.
     *   `"d"`: The datum or value at the script output does not match the contract's transition.
+    *   `"eai"` : The initial state must not have duplicate accounts.
+    *   `"ebi"` : The initial state must not have duplicate bound values.
+    *   `"eci"` : The initial state must not have duplicate choices.
+    *   `"eao"` : The final state must not have duplicate accounts.
+    *   `"ebo"` : The final state must not have duplicate bound values.
+    *   `"eco"` : The final state must not have duplicate choices.
     *   `"f"`: The value in the script's output UTxO does not match the value in its internal state.
     *   `"o"`: Outputting to two Marlowe scripts with the same address in the same transaction is forbidden.
     *   `"p"`: Insufficient value is paid to a public-key address.
     *   `"r"`: Insufficient value is paid in a role payout. This may occur because the role payout was adjusted to satisfy the minimum-ADA ledger rule, despite that adjustment violating the terms of the contract.
     *   `"s"`: A required public-key signature was not present in the transaction.
     *   `"t"`: The role token authorizing the application of input is not present in the transaction.
-    *   `"v"`: The value input from the script does not match that specified in its datum.
+    *   `"vi"`: The value input from the script does not match that specified in its datum.
+    *   `"vo"`: The value output from the script does not match that specified in its datum.
     *   `"w"`: Inputting from two Marlowe scripts with the same address in the same transaction is forbidden.
     *   `"x"`: The input datum was not provided to the script.
     *   If these errors occur during Plutus validation but not outside of it, then there likely is a clock inconsistency between local time and the node.

diff --git a/marlowe/specification/marlowe-cardano-specification.md b/marlowe/specification/marlowe-cardano-specification.md
@@ -318,9 +318,11 @@ all demerkleizes transactionInput ≡ True
 
 #### *Constraint 13.* Positive balances
 
-All accounts in the state have positive balances.
+All accounts in the initial and final states have positive balances.
 ```haskell
-all ((> 0) . snd) (accounts $ marloweState marloweData) ≡ True
+positiveBalances $ marloweState marloweData     ≡ True
+positiveBalances $ txOutState transactionOutput ≡ True
+  where positiveBalances state = all ((> 0) . snd) (accounts state)
 ```
 
 
@@ -364,13 +366,28 @@ The payment to a role must be in a single output, but the payment to an address
 #### *Constraint 18.* Final balance
 
 The value output to the script's UTxO must equal the total value in the output state.
-
 ```haskell
 outValue ≡ foldMap toValue (accounts $ txOutState transactionOutput)
   where toValue ((_, Token currency name), count)) = Value.singleton currency name count
 ```
 
 
+#### *Constraint 19.* No duplicates
+
+The initial and final state must not have duplicate keys in their account entries, choices, or bound values.
+```haskell
+hasDuplicateKey (accounts    inState ) ≡ False
+hasDuplicateKey (choices     inState ) ≡ False
+hasDuplicateKey (boundValues inState ) ≡ False
+hasDuplicateKey (accounts    outState) ≡ False
+hasDuplicateKey (choices     outState) ≡ False
+hasDuplicateKey (boundValues outState) ≡ False
+  where
+    outState = txOutState transactionOutput
+    hasDuplicateKey am = let ks = fst <$> toList am in length ks /= length (nub ks)
+```
+
+
 ## Plutus Validator for Marlowe Payouts
 
 

diff --git a/marlowe/src/Language/Marlowe/Scripts.hs b/marlowe/src/Language/Marlowe/Scripts.hs
@@ -202,35 +202,30 @@ mkMarloweValidator
             case closeInterval $ txInfoValidRange scriptContextTxInfo of
                 Just interval' -> interval'
                 Nothing        -> traceError "a"
-    -- The incoming balance of each account must be positive.
-    -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".]
-    let positiveBalances = traceIfFalse "b" $ validateBalances marloweState
 
     -- Find Contract continuation in TxInfo datums by hash or fail with error.
     let inputs = fmap marloweTxInputToInput marloweTxInputs
+
     {-  We do not check that a transaction contains exact input payments.
         We only require an evidence from a party, e.g. a signature for PubKey party,
         or a spend of a 'party role' token.  This gives huge flexibility by allowing
         parties to provide multiple inputs (either other contracts or P2PKH).
         Then, we check scriptOutput to be correct.
      -}
     let inputContents = fmap getInputContent inputs
+
     -- Check that the required signatures and role tokens are present.
     -- [Marlowe-Cardano Specification: "Constraint 14. Inputs authorized".]
     let inputsOk = validateInputs inputContents
 
-    -- Since individual balances were validated to be positive,
-    -- the total balance is also positive.
-    let inputBalance = totalBalance (accounts marloweState)
-
     -- [Marlowe-Cardano Specification: "Constraint 5. Input value from script".]
-    -- The total incoming balance must match the actual script value being spent.
-    let balancesOk = traceIfFalse "v" $ inputBalance == scriptInValue
-
-    let preconditionsOk = positiveBalances && balancesOk
+    -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".]
+    -- [Marlowe-Cardano Specification: "Constraint 19. No duplicates".]
+    -- Check that the initial state obeys the Semantic's invariants.
+    let preconditionsOk = checkState "i" scriptInValue marloweState
 
-    -- Package the inputs to be applied in the semantics.
     -- [Marlowe-Cardano Specification: "Constraint 0. Input to semantics".]
+    -- Package the inputs to be applied in the semantics.
     let txInput = TransactionInput {
             txInterval = interval,
             txInputs = inputs }
@@ -264,16 +259,17 @@ mkMarloweValidator
                     _ -> let
                         totalIncome = foldMap collectDeposits inputContents
                         totalPayouts = foldMap snd payoutsByParty
-                        finalBalance = inputBalance + totalIncome - totalPayouts
-                        outputBalance = totalBalance (accounts txOutState)
+                        finalBalance = scriptInValue + totalIncome - totalPayouts
                         in
-                          -- The total account balance must be paid to a single output to the script.
-                          -- [Marlowe-Cardano Specification: "Constraint 3. Single Marlowe output".]
-                          -- [Marlowe-Cardano Specification: "Constraint 6. Output value to script."]
-                          checkOwnOutputConstraint marloweData finalBalance
-                          -- The value in the script's output UTxO must match the value in the output state.
-                          -- [Marlowe-Cardano Specification: "Constraint 18. Final balance."]
-                          && traceIfFalse "f" (outputBalance == finalBalance)
+                             -- [Marlowe-Cardano Specification: "Constraint 3. Single Marlowe output".]
+                             -- [Marlowe-Cardano Specification: "Constraint 6. Output value to script."]
+                             -- Check that the single Marlowe output has the correct datum and value.
+                             checkOwnOutputConstraint marloweData finalBalance
+                             -- [Marlowe-Cardano Specification: "Constraint 18. Final balance."]
+                             -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".]
+                             -- [Marlowe-Cardano Specification: "Constraint 19. No duplicates".]
+                             -- Check that the final state obeys the Semantic's invariants.
+                          && checkState "o" finalBalance txOutState
             preconditionsOk && inputsOk && payoutsOk && checkContinuation
         Error TEAmbiguousTimeIntervalError -> traceError "i"
         Error TEApplyNoMatchError -> traceError "n"
@@ -311,6 +307,33 @@ mkMarloweValidator
         TxInInfo{txInInfoResolved=TxOut{txOutAddress=Ledger.Address (ScriptCredential vh2) _}} = vh1 == vh2
     sameValidatorHash _ _ = False
 
+    -- Check a state for the correct value, positive accounts, and no duplicates.
+    checkState :: BuiltinString -> Val.Value -> State -> Bool
+    checkState tag expected State{..} =
+      let
+        positiveBalance :: (a, Integer) -> Bool
+        positiveBalance (_, balance) = balance > 0
+        noDuplicates :: Eq k => AssocMap.Map k v -> Bool
+        noDuplicates am =
+          let
+            test [] = True           -- An empty list has no duplicates.
+            test (x : xs)            -- Look for a duplicate of the head in the tail.
+              | elem x xs = False    -- A duplicate is present.
+              | otherwise = test xs  -- Continue searching for a duplicate.
+          in
+            test $ AssocMap.keys am
+      in
+           -- [Marlowe-Cardano Specification: "Constraint 5. Input value from script".]
+           -- and/or
+           -- [Marlowe-Cardano Specification: "Constraint 18. Final balance."]
+           traceIfFalse ("v"  <> tag) (totalBalance accounts == expected)
+           -- [Marlowe-Cardano Specification: "Constraint 13. Positive balances".]
+        && traceIfFalse ("b"  <> tag) (all positiveBalance $ AssocMap.toList accounts)
+           -- [Marlowe-Cardano Specification: "Constraint 19. No duplicates".]
+        && traceIfFalse ("ea" <> tag) (noDuplicates accounts)
+        && traceIfFalse ("ec" <> tag) (noDuplicates choices)
+        && traceIfFalse ("eb" <> tag) (noDuplicates boundValues)
+
     -- Look up the Datum hash for specific data.
     findDatumHash' :: PlutusTx.ToData o => o -> Maybe DatumHash
     findDatumHash' datum = findDatumHash (Datum $ PlutusTx.toBuiltinData datum) scriptContextTxInfo