WIP: Draft version constraint generation (digital-asset#5472)

First version of static verification tool. The current state of the tool: - Reads DAR files. - Partially evaluates the code. - Generates constraints for the field and choice to be verified. - Passes the constraints to an SMT solver. - Some basic tests.
FlashSheridan · May 20, 2020 · 2af134c · 2af134c
1 parent d7cc5e0
commit 2af134c
Show file tree

Hide file tree

Showing 16 changed files with 2,656 additions and 1 deletion.
diff --git a/WORKSPACE b/WORKSPACE
@@ -896,6 +896,15 @@ nixpkgs_package(
     repositories = dev_env_nix_repos,
 )
 
+nixpkgs_package(
+    name = "z3_nix",
+    attribute_path = "z3",
+    fail_not_supported = False,
+    nix_file = "//nix:bazel.nix",
+    nix_file_deps = common_nix_file_deps,
+    repositories = dev_env_nix_repos,
+) if not is_windows else None
+
 dev_env_tool(
     name = "postgresql_dev_env",
     nix_include = [

diff --git a/bazel-haskell-deps.bzl b/bazel-haskell-deps.bzl
@@ -640,6 +640,7 @@ exports_files(["stack.exe"], visibility = ["//visibility:public"])
             "semigroups",
             "semver",
             "silently",
+            "simple-smt",
             "sorted-list",
             "split",
             "stache",

diff --git a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Numeric.hs b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/Numeric.hs
@@ -3,7 +3,7 @@
 
 -- | DAML-LF Numeric literals, with scale attached.
 module DA.Daml.LF.Ast.Numeric
-    ( Numeric
+    ( Numeric (..)
     , NumericError (..)
     , E10
     , numeric

diff --git a/compiler/daml-lf-verify/BUILD.bazel b/compiler/daml-lf-verify/BUILD.bazel
@@ -0,0 +1,131 @@
+# Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+load("//rules_daml:daml.bzl", "daml_compile")
+load("//bazel_tools:haskell.bzl", "da_haskell_binary", "da_haskell_library", "da_haskell_test")
+load("@os_info//:os_info.bzl", "is_windows")
+
+da_haskell_binary(
+    name = "daml-lf-verify",
+    srcs = glob(["src/**/*.hs"]),
+    data = [
+        "@z3_nix//:bin/z3",
+    ] if not is_windows else [],
+    hackage_deps = [
+        "aeson",
+        "base",
+        "bytestring",
+        "containers",
+        "deepseq",
+        "Decimal",
+        "extra",
+        "filepath",
+        "ghc-lib-parser",
+        "hashable",
+        "lens",
+        "mtl",
+        "optparse-applicative",
+        "prettyprinter",
+        "recursion-schemes",
+        "safe",
+        "scientific",
+        "simple-smt",
+        "template-haskell",
+        "text",
+        "time",
+        "unordered-containers",
+        "zip-archive",
+    ],
+    main_function = "DA.Daml.LF.Verify.main",
+    src_strip_prefix = "src",
+    visibility = ["//visibility:public"],
+    deps = [
+        "//compiler/daml-lf-ast",
+        "//compiler/daml-lf-proto",
+        "//compiler/daml-lf-reader",
+        "//compiler/daml-lf-tools",
+        "//libs-haskell/bazel-runfiles",
+        "//libs-haskell/da-hs-base",
+    ],
+)
+
+da_haskell_library(
+    name = "daml-lf-verify-lib",
+    srcs = glob(["src/**/*.hs"]),
+    data = [
+        "@z3_nix//:bin/z3",
+    ] if not is_windows else [],
+    hackage_deps = [
+        "aeson",
+        "base",
+        "bytestring",
+        "containers",
+        "deepseq",
+        "Decimal",
+        "extra",
+        "filepath",
+        "ghc-lib-parser",
+        "hashable",
+        "lens",
+        "mtl",
+        "optparse-applicative",
+        "prettyprinter",
+        "recursion-schemes",
+        "safe",
+        "scientific",
+        "simple-smt",
+        "template-haskell",
+        "text",
+        "time",
+        "unordered-containers",
+        "zip-archive",
+    ],
+    src_strip_prefix = "src",
+    visibility = ["//visibility:public"],
+    deps = [
+        "//compiler/daml-lf-ast",
+        "//compiler/daml-lf-proto",
+        "//compiler/daml-lf-reader",
+        "//compiler/daml-lf-tools",
+        "//libs-haskell/bazel-runfiles",
+        "//libs-haskell/da-hs-base",
+    ],
+)
+
+daml_compile(
+    name = "quickstart",
+    srcs = glob(["daml/quickstart/**/*.daml"]),
+    version = "1.0.0",
+)
+
+daml_compile(
+    name = "conditionals",
+    srcs = glob(["daml/conditionals/**/*.daml"]),
+    version = "1.0.0",
+)
+
+da_haskell_test(
+    name = "verify-tests",
+    srcs = glob(["tests/**/*.hs"]),
+    data = [
+        ":conditionals.dar",
+        ":quickstart.dar",
+    ] if not is_windows else [],
+    hackage_deps = [
+        "base",
+        "containers",
+        "filepath",
+        "tasty",
+        "tasty-hunit",
+    ],
+    main_function = "DA.Daml.LF.Verify.Tests.mainTest",
+    src_strip_prefix = "tests",
+    visibility = ["//visibility:public"],
+    deps = [
+        ":daml-lf-verify-lib",
+        "//compiler/daml-lf-ast",
+        "//libs-haskell/bazel-runfiles",
+        "//libs-haskell/da-hs-base",
+        "//libs-haskell/test-utils",
+    ],
+) if not is_windows else None
diff --git a/compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml b/compiler/daml-lf-verify/daml/conditionals/daml/Iou.daml
@@ -0,0 +1,61 @@
+-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+
+module Iou where
+
+template Iou with
+    owner: Party
+    content: Int
+  where
+    signatory owner
+
+    choice SuccA: ContractId Iou
+      controller owner
+      do
+        if False
+        then create Iou with owner; content = content
+        else create Iou with owner; content = content
+
+    choice SuccB: ContractId Iou
+      controller owner
+      do
+        if 1 == 1
+        then create Iou with owner; content = content
+        else create Iou with owner; content = 0
+
+    choice SuccC: ContractId Iou
+      controller owner
+      do
+        if True
+        then do
+          _ <- create Iou with owner; content = content
+          create Iou with owner; content = 0
+        else create Iou with owner; content = content
+
+    choice SuccD: ContractId Iou
+      controller owner
+      do
+        if True
+        then do
+          cid1 <- create Iou with owner; content = content
+          archive cid1
+          create Iou with owner; content = content
+        else create Iou with owner; content = content
+
+    choice FailA: ContractId Iou
+      controller owner
+      do
+        if 1 == 1
+        then create Iou with owner; content = 0
+        else create Iou with owner; content = content
+
+    choice FailB: ContractId Iou
+      controller owner
+      do
+        if False
+        then create Iou with owner; content = content
+        else do 
+          _ <- create Iou with owner; content = content
+          create Iou with owner; content = content
+
diff --git a/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml b/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml
@@ -0,0 +1,86 @@
+-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+
+module Iou where
+
+type IouCid = ContractId Iou
+
+template Iou
+  with
+    issuer : Party
+    owner : Party
+    currency : Text
+    amount : Decimal
+    observers : [Party]
+  where
+    ensure amount > 0.0
+
+    signatory issuer, owner
+
+    observer observers
+
+    controller owner can
+
+      -- Split the IOU by dividing the amount.
+      Iou_Split : (IouCid, IouCid)
+         with
+          splitAmount: Decimal
+        do
+          let restAmount = amount - splitAmount
+          splitCid <- create this with amount = splitAmount
+          restCid <- create this with amount = restAmount
+          return (splitCid, restCid)
+
+      -- Merge two IOUs by aggregating their amounts.
+      Iou_Merge : IouCid
+        with
+          otherCid: IouCid
+        do
+          otherIou <- fetch otherCid
+          -- Check the two IOU's are compatible
+          assert (
+            currency == otherIou.currency &&
+            owner == otherIou.owner &&
+            issuer == otherIou.issuer
+            )
+          -- Retire the old Iou
+          archive otherCid
+          -- Return the merged Iou
+          create this with amount = amount + otherIou.amount
+
+      Iou_Transfer : ContractId IouTransfer
+        with
+          newOwner : Party
+        do create IouTransfer with iou = this; newOwner
+
+      Iou_AddObserver : IouCid
+        with
+          newObserver : Party
+        do create this with observers = newObserver :: observers
+
+      Iou_RemoveObserver : IouCid
+        with
+          oldObserver : Party
+        do create this with observers = filter (/= oldObserver) observers
+
+template IouTransfer
+  with
+    iou : Iou
+    newOwner : Party
+  where
+    signatory iou.issuer, iou.owner
+
+    controller iou.owner can
+      IouTransfer_Cancel : IouCid
+        do create iou
+
+    controller newOwner can
+      IouTransfer_Reject : IouCid
+        do create iou
+
+      IouTransfer_Accept : IouCid
+        do
+          create iou with
+            owner = newOwner
+            observers = []
diff --git a/compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml b/compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml
@@ -0,0 +1,49 @@
+-- Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+
+module IouTrade where
+
+import DA.Assert
+
+import Iou
+
+template IouTrade
+  with
+    buyer : Party
+    seller : Party
+    baseIouCid : IouCid
+    baseIssuer : Party
+    baseCurrency : Text
+    baseAmount : Decimal
+    quoteIssuer : Party
+    quoteCurrency : Text
+    quoteAmount : Decimal
+  where
+    signatory buyer
+
+    controller seller can
+      IouTrade_Accept : (IouCid, IouCid)
+        with
+          quoteIouCid : IouCid
+        do
+          baseIou <- fetch baseIouCid
+          baseIssuer === baseIou.issuer
+          baseCurrency === baseIou.currency
+          baseAmount === baseIou.amount
+          buyer === baseIou.owner
+          quoteIou <- fetch quoteIouCid
+          quoteIssuer === quoteIou.issuer
+          quoteCurrency === quoteIou.currency
+          quoteAmount === quoteIou.amount
+          seller === quoteIou.owner
+          quoteIouTransferCid <- exercise quoteIouCid Iou_Transfer with
+            newOwner = buyer
+          transferredQuoteIouCid <- exercise quoteIouTransferCid IouTransfer_Accept
+          baseIouTransferCid <- exercise baseIouCid Iou_Transfer with
+            newOwner = seller
+          transferredBaseIouCid <- exercise baseIouTransferCid IouTransfer_Accept
+          return (transferredQuoteIouCid, transferredBaseIouCid)
+
+      TradeProposal_Reject : ()
+        do return ()