PLT-3564 PLT-6070 PLT-6071 PLT-6072 PLT-6073 PLT-5817 Safety checks for REST and CLI #622

bwbush · 2023-06-20T01:59:04Z

Added safety analysis report to creation of contracts into marlowe-runtime-web and marlowe-runtime-cli.

Pre-submit checklist:

Branch
- Tests are provided (if possible)
- Test report is updated (if relevant)
- Commit sequence broadly makes sense
- Key commits have useful messages
- Relevant tickets are mentioned in commit messages
- Formatting, PNG optimization, etc. are updated
PR
- Self-reviewed the diff
- Useful pull request description
  - Review required
  - Substantial changes to code, test, or documentation
  - Change made to Marlowe validator (@bwbush and @palas must be included as reviewers)
  - Review not required
  - Minor changes to non-critical code, documentation, nix derivations, configuration files, or scripts
  - Formatting, spelling, grammar, or reorganization
- Reviewer requested

bwbush · 2023-06-21T17:19:55Z

marlowe-runtime-cli/app/Language/Marlowe/Runtime/CLI/Command/Create.hs

+    (ContractId contractId, safetyErrors) <- run MarloweV1 minting'
+    liftIO
+      $ if null safetyErrors
+        then hPutStrLn stderr "Safety analysis found no errors in the contract."
+        else do
+               hPutStrLn stderr "Safety analysis found the following errors in the contract:"
+               BS8.hPutStrLn stderr $ Yaml.encode safetyErrors


Safety errors are printed as YAML to stderr. Another approach would have been to have these written to a file.

bwbush · 2023-06-21T17:22:27Z

marlowe-runtime-web/test/Spec.hs

@@ -143,7 +143,7 @@ instance Arbitrary Web.PostTransactionsRequest where
  shrink = genericShrink

 instance Arbitrary (Web.CreateTxEnvelope tx) where
-  arbitrary = Web.CreateTxEnvelope <$> arbitrary <*> arbitrary
+  arbitrary = Web.CreateTxEnvelope <$> arbitrary <*> arbitrary <*> resize 5 arbitrary


The property-based tests become slow if we let large contracts/transactions be generated in the Arbitrary instance for safety errors. Five seems a good enough size limit here.

Yeah, that seems fine

bwbush · 2023-06-21T17:23:35Z

marlowe-runtime/marlowe-tx/Main.hs

@@ -214,6 +219,14 @@ getOptions = execParser $ info (helper <*> parser) infoMod
      , showDefault
      ]

+    analysisTimeoutParser = option (fromInteger <$> auto) $ mconcat
+      [ long "analysis-timeout"
+      , value 15


The slow phase of the safety analysis is limited to 15 seconds by default, at the marlowe-tx level.

bwbush · 2023-06-21T17:25:57Z

marlowe-runtime/tx/Language/Marlowe/Runtime/Transaction/Safety.hs

+        . either
+          (pure . TransactionValidationError transaction . show)
+          (const $ TransactionWarning transaction <$> V1.txOutWarnings txOutput)


Failures in the analysis of safety are server errors, but the results of successful safety analysis are returned as [SafetyError].

bwbush · 2023-06-21T17:27:50Z

marlowe-runtime/tx/Language/Marlowe/Runtime/Transaction/Server.hs

+    -- Fast analysis of safety: examines bounds for transactions.
+    contractSafetyErrors = checkContract networkId roleTokens version contract' continuations


There is no time limit on the fast analysis of safety, because that doesn't use z3 to find all paths through the contract and it doesn't execute any Plutus transactions.

bwbush · 2023-06-21T17:29:17Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("No roles are present in the contract, but a roles currency was specified." :: String)
+      , "fatal" .= False


Marked as non-fatal because an extraneous roles policy ID doesn't affect execution.

bwbush · 2023-06-21T17:29:58Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("This role token was specified for minting, but that role is not present in the contract." :: String)
+      , "role-name" .= String (T.decodeUtf8 $ fromBuiltin tokenName)
+      , "fatal" .= False


Marked as non-fatal because minting an extra role token doesn't affect execution.

bwbush · 2023-06-21T17:30:52Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("At some point in during its executation, the contract may hold more native tokens than permitted by the ledger rules." :: String)
+      , "bytes" .= natural
+      , "fatal" .= False


Marked as non-fatal because this is an estimate, and the slow analysis would identify if this truly occurs in any transaction.

bwbush · 2023-06-21T17:31:08Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("This transaction's size may exceed the limit permitted by the ledger rules." :: String)
+      , "transaction" .= transaction
+      , "bytes" .= natural
+      , "fatal" .= False


Marked as non-fatal because this is an estimate, and the slow analysis would identify if this truly occurs in any transaction.

bwbush · 2023-06-21T17:31:17Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("This transaction's Plutus execution cost may exceed the limit permitted by the ledger rules." :: String)
+      , "transaction" .= transaction
+      , "cost" .= exBudget
+      , "fatal" .= False


Marked as non-fatal because this is an estimate, and the slow analysis would identify if this truly occurs in any transaction.

bwbush · 2023-06-21T17:32:03Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("A Marlowe semantics warning is reported for this transaction." :: String)
+      , "transaction" .= transaction
+      , "warning" .= warning
+      , "fatal" .= False


Marked as non-fatal because semantics warnings don't prevent execution.

bwbush · 2023-06-21T17:32:40Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+      , "detail" .= ("The contract is missing a continuation that is not present in its map of continuations." :: String)
+      , "hash" .= toJSON (EncodeBase16 $ fromBuiltin datumHash)
+      , "fatal" .= False


Should this be fatal or non-fatal? One might choose to not supply the full set of continuations for analysis.

bwbush · 2023-06-21T17:33:23Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+       , "detail" .= ("The safety analysis exceeded the allotted time." :: String)
+       , "fatal" .= False


Should this be fatal or non-fatal?

bwbush · 2023-06-21T17:36:55Z

@palas and @paluh, please comment on which safety errors should be flagged to the user as "fatal" or "non-fatal" in marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs. This seems somewhat subjective.

bwbush · 2023-06-21T17:48:33Z

nix/marlowe-cardano/deploy/operables.nix

@@ -360,6 +361,7 @@ in

  marlowe-tx = mkOperableWithProbes {
    package = marlowe-tx;
+    runtimeInputs = [ z3 ];


@jhbertra, is this the only derivation where the new runtime dependency of marlowe-tx on z3 will need to be added?

I think this needs to be added to compose.nix as well. You could add this to run-local-service:

export PATH="$PATH:${lib.makeBinPath [ z3 ]}"

Fixed in 34f1d7e.

nhenin · 2023-06-22T07:50:04Z

marlowe-test/src/Spec/Marlowe/Semantics/Arbitrary.hs

+      , NonPositiveBalance <$> arbitrary <*> arbitrary
+      , DuplicateAccount <$> arbitrary <*> arbitrary
+      , DuplicateChoice <$> arbitrary
+      , DuplicateBoundValue <$> arbitrary


FYI @bwbush :

I don't know if DuplicateChoice, DuplicateBoundValue are the same things but next handles cases where some inputs are shadowed by the previous ones ... next doesn't propose invalid applies...

For Deposit, next also handle Identical Evaluated Deposits... something we can't really check at "compile" time, but is 2 identical deposits in a when regardless their value could be considered as a warning ?

These Duplicate... warnings apply to the state of the contract, not to actions like deposits.

nhenin · 2023-06-22T07:55:11Z

marlowe/src/Language/Marlowe/Analysis/Safety/Types.hs

+instance ToJSON SafetyError where
+  toJSON MissingRolesCurrency =
+    object
+      [ "error" .= ("MissingRolesCurrency" :: String)


It's surprising that you need to help the type inference to serialize here (xxxx:: String)

Not at all, with OverloadedStrings the type of a string literal is polymorphic, because it is desugarred as

fromString ("MissingRolesCurrency" :: String)

And in this context, we have

(.= "error") :: forall a. ToJSON a => a ->Pair

So the type a is polymorphic in both its introduction (the output of fromString) and elimination (the input of (.= "error")), thus ambiguous.

nhenin · 2023-06-22T07:57:49Z

marlowe/src/Language/Marlowe/Core/V1/Semantics.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file


Should we remove this ? now that we disabled the feature ?

Yes, can remove

Fixed in 34f1d7e.

nhenin · 2023-06-22T08:03:42Z

marlowe-integration/marlowe-integration.cabal

    , containers
-    , eventuo11y >=0.9 && <0.11
+    , eventuo11y                                                                                                                                    >=0.9 && <0.11


@bwbush you have confilcts with the cabals you have modified and the main because of the formatter .... maybe you should do a cabal-fmt --inplace --no-tabular **/*.cabal in your commits before rebasing...

If you rebase and run pre-commit run --all this should be reverted now.

although hlint will fail until #626 is merged.

Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:20:01Z

marlowe-integration/src/Test/Integration/Marlowe/Local.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file


You can get rid of this now

Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:20:09Z

marlowe-runtime-cli/app/Language/Marlowe/Runtime/CLI/Command/Create.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:21:07Z

marlowe-runtime-cli/changelog.d/20230620_075705_brian.bush_PLT_5817.rst

+Added
+-----
+
+- Create command outputs results of contract safety analysis.


This shouldn't have its own changelog.d folder - this is part of the marlowe-runtime component, not a separate one

Thanks. We should probably document which folders should not have change logs.

Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:21:41Z

marlowe-integration/changelog.d/20230620_075519_brian.bush_PLT_5817.rst

+Added
+-----
+
+- Fifteen-second timeout for contract safety analysis.


We are not doing changelog tracking in this folder

Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:25:23Z

marlowe-runtime/marlowe-tx/Main.hs

@@ -1,7 +1,8 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:25:45Z

marlowe-runtime/src/Language/Marlowe/Runtime/Core/Api.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:25:53Z

marlowe-runtime/test/Language/Marlowe/Runtime/Transaction/CommandSpec.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:25:56Z

marlowe-runtime/test/Language/Marlowe/Runtime/Transaction/SafetySpec.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:26:03Z

marlowe-runtime/tx-api/Language/Marlowe/Runtime/Transaction/Api.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:27:06Z

marlowe-runtime/tx/Language/Marlowe/Runtime/Transaction/Server.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:28:24Z

marlowe-test/src/Spec/Marlowe/Semantics/Arbitrary.hs

@@ -1,3 +1,5 @@
+-- editorconfig-checker-disable-file
+


Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:30:34Z

marlowe-test/src/Spec/Marlowe/Semantics/Arbitrary.hs

+       txInput <- semiArbitrary context
+       txOutput <- arbitrary
+       pure Transaction{..}
+  shrink _ = mempty


Shouldn't we shrink this?

I was undecided, but it is harmless to shrink this. Fixed in 34f1d7e.

jhbertra · 2023-06-22T19:45:48Z

marlowe-runtime/tx/Language/Marlowe/Runtime/Transaction/Server.hs

+          (changeAddress addresses)
+          (toInteger minAda)
+          contract'
+          continuations


Does this actually work? Aren't the safety errors lazily computed in checkTransactions? Z3 will run in IO, so that's fine, that will run in the eval thread, but at the end we have

either throwE (pure . mconcat) . forM transactions $ checkTransaction solveConstraints version marloweContext rolesCurrency changeAddress

Which is a bit complex to reason about regarding laziness. Ultimately, the final IO action depends on pattern matching the Either returned by forM, and transitively from each call to checkTransaction, so that will force the evaluation of the fake solveConstraints calls. The only unevaluated expressions here would be pure . TransactionValidationError transaction . show and const $ TransactionWarning <$> V1.txOutWarnings txOutput. How slow is txOutWarnings?

The txOutWarnings is fast because it is computed from the semantics, not from executing Plutus. However, I think we should demonstrate this as a test case, so I've created the separate ticket PLT-6362.

jhbertra

Looks great, thanks! Just the one question about the timeout and laziness. And some stuff that needs addressing once rebasing happens on #626

bwbush self-assigned this Jun 20, 2023

bwbush force-pushed the PLT-5817 branch from de29d32 to fef0d61 Compare June 21, 2023 14:15

bwbush marked this pull request as ready for review June 21, 2023 14:15

paluh self-requested a review June 21, 2023 15:30

bwbush commented Jun 21, 2023

View reviewed changes

bwbush requested review from nhenin, palas and jhbertra June 21, 2023 17:34

bwbush force-pushed the PLT-5817 branch 2 times, most recently from aec3a6b to 346a17b Compare June 21, 2023 17:48

bwbush commented Jun 21, 2023

View reviewed changes

nhenin reviewed Jun 22, 2023

View reviewed changes

jhbertra reviewed Jun 22, 2023

View reviewed changes

jhbertra approved these changes Jun 22, 2023

View reviewed changes

bwbush added 13 commits June 23, 2023 13:44

PLT-6070 Implemented JSON serialization of safety errors.

ca3da93

PLT-6070 Implemented binary instance for safety errors.

6a3aa67

PLT-6070 Implemented arbitrary instances for safety errors.

fefcbfd

PLT-6070 Added safety report to Create command.

48eaf57

PLT-6073 Added timeout to safety analysis.

2081592

PLT-6072 Added safety analysis output to marlowe-runtime-cli.

e8b3b97

PLT-6071 Added safety analysis to REST API.

5170f21

PLT-5817 Fixed JSON instances for safety errors in web API.

379c53f

PLT-3564 Change logs for integration of safety analysis.

5f47ff2

PLT-5817 Orphans supporting OpenAPI schemas for SafetyError.

10451d2

PLT-5817 Added z3 to runtime dependencies of marlowe-tx.

0ab9f5f

PLT-5817 Fixed botched merge.

dbf8e67

Merge remote-tracking branch 'origin/main' into PLT-5817

30a69cc

bwbush force-pushed the PLT-5817 branch from 346a17b to 34f1d7e Compare June 24, 2023 00:14

PLT-5817 Revisions in response to reviewer comments.

854bf1f

bwbush force-pushed the PLT-5817 branch from 34f1d7e to 854bf1f Compare June 24, 2023 00:28

bwbush enabled auto-merge June 24, 2023 00:29

PLT-5817 Added z3 to path for integration tests.

2ed9725

bwbush merged commit 9e412eb into main Jun 24, 2023

bwbush deleted the PLT-5817 branch June 24, 2023 01:40

		-- Fast analysis of safety: examines bounds for transactions.
		contractSafetyErrors = checkContract networkId roleTokens version contract' continuations

		, "detail" .= ("No roles are present in the contract, but a roles currency was specified." :: String)
		, "fatal" .= False

		, "detail" .= ("The safety analysis exceeded the allotted time." :: String)
		, "fatal" .= False

PLT-3564 PLT-6070 PLT-6071 PLT-6072 PLT-6073 PLT-5817 Safety checks for REST and CLI #622

PLT-3564 PLT-6070 PLT-6071 PLT-6072 PLT-6073 PLT-5817 Safety checks for REST and CLI #622

Conversation

bwbush commented Jun 20, 2023

bwbush Jun 21, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bwbush Jun 21, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bwbush commented Jun 21, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nhenin Jun 22, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jhbertra Jun 22, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nhenin Jun 22, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jhbertra left a comment

Choose a reason for hiding this comment

bwbush Jun 21, 2023 •

edited

Loading

bwbush Jun 21, 2023 •

edited

Loading

nhenin Jun 22, 2023 •

edited

Loading

jhbertra Jun 22, 2023 •

edited

Loading

nhenin Jun 22, 2023 •

edited

Loading