From 04eff2722cef63e8eccd95225090550b5934ad70 Mon Sep 17 00:00:00 2001 From: Moritz Kiefer Date: Tue, 15 Feb 2022 12:31:32 +0100 Subject: [PATCH] Drop daml-lf-verify (#12942) This is completely unmaintained, unused and partially broken so delete it for now. Worst case, we recover it from Git history. closes #6550 because it now refers to deleted code. changelog_begin changelog_end --- WORKSPACE | 9 - compiler/daml-lf-verify/BUILD.bazel | 146 --- compiler/daml-lf-verify/README.rst | 253 ----- .../daml/conditionals/daml/Conditional.daml | 60 -- .../daml/general/daml/General.daml | 65 -- .../daml/quickstart/daml/Iou.daml | 89 -- .../daml/quickstart/daml/IouTrade.daml | 50 - .../daml/recursion/daml/Recursion.daml | 143 --- .../daml-lf-verify/src/DA/Daml/LF/Verify.hs | 132 --- .../src/DA/Daml/LF/Verify/Context.hs | 963 ------------------ .../src/DA/Daml/LF/Verify/Generate.hs | 636 ------------ .../src/DA/Daml/LF/Verify/Read.hs | 103 -- .../src/DA/Daml/LF/Verify/ReferenceSolve.hs | 302 ------ .../src/DA/Daml/LF/Verify/Solve.hs | 607 ----------- .../tests/DA/Daml/LF/Verify/Tests.hs | 273 ----- nix/bazel.nix | 2 - 16 files changed, 3833 deletions(-) delete mode 100644 compiler/daml-lf-verify/BUILD.bazel delete mode 100644 compiler/daml-lf-verify/README.rst delete mode 100644 compiler/daml-lf-verify/daml/conditionals/daml/Conditional.daml delete mode 100644 compiler/daml-lf-verify/daml/general/daml/General.daml delete mode 100644 compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml delete mode 100644 compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml delete mode 100644 compiler/daml-lf-verify/daml/recursion/daml/Recursion.daml delete mode 100644 compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs delete mode 100644 compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs delete mode 100644 compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs delete mode 100644 compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs delete mode 100644 compiler/daml-lf-verify/src/DA/Daml/LF/Verify/ReferenceSolve.hs delete mode 100644 compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs delete mode 100644 compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs diff --git a/WORKSPACE b/WORKSPACE index 775bcf7914b3..c77d56c3736e 100644 --- a/WORKSPACE +++ b/WORKSPACE @@ -821,15 +821,6 @@ 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/compiler/daml-lf-verify/BUILD.bazel b/compiler/daml-lf-verify/BUILD.bazel deleted file mode 100644 index 42d4593440b9..000000000000 --- a/compiler/daml-lf-verify/BUILD.bazel +++ /dev/null @@ -1,146 +0,0 @@ -# Copyright (c) 2022 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 = "general", - srcs = glob(["daml/general/**/*.daml"]), - version = "1.0.0", -) - -daml_compile( - name = "conditionals", - srcs = glob(["daml/conditionals/**/*.daml"]), - version = "1.0.0", -) - -daml_compile( - name = "recursion", - srcs = glob(["daml/recursion/**/*.daml"]), - version = "1.0.0", -) - -da_haskell_test( - name = "verify-tests", - srcs = glob(["tests/**/*.hs"]), - data = [ - ":quickstart.dar", - ":general.dar", - ":conditionals.dar", - ":recursion.dar", - ] if not is_windows else [], - hackage_deps = [ - "base", - "containers", - "filepath", - "tasty", - "tasty-expected-failure", - "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/README.rst b/compiler/daml-lf-verify/README.rst deleted file mode 100644 index e09aafd7d9bf..000000000000 --- a/compiler/daml-lf-verify/README.rst +++ /dev/null @@ -1,253 +0,0 @@ -.. Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. -.. SPDX-License-Identifier: Apache-2.0 - -Daml Verification Tool -====================== - -This project performs fully automated formal verification of Daml code. -Provided with a choice of a template and a field of a (potentially different) template, the verification tool employs symbolic -execution and an SMT solver, to verify whether the given choice always preserves -the total amount of the given field. This allows it to automatically answer -the common question "Could this smart contract model ever burn money or create -money out of thin air?" - -Installation -============ - -- Install the `Daml development dependecies`_. - -- Install the `Z3 SMT solver`_. - Note that on Linux, you can alternatively install Z3 using - ``sudo apt install z3``. - -.. _Daml development dependecies: https://github.com/digital-asset/daml/ -.. _Z3 SMT solver: https://github.com/Z3Prover/z3 - -Running the Verification Tool -============================= - -At the moment, the verification tool is launched from a command line interface. -Execute the tool by passing in the DAR file, the choice to be -verified (``--choice`` / ``-c``), and the field which should be preserved (``--field`` / ``-f``): - -.. code-block:: - > bazel run //compiler/daml-lf-verify:daml-lf-verify -- file.dar --choice Module:Template.Choice --field Module:Template.Field - -Examples -======== - -Example 1: Transferring value ------------------------------ - -As a first example, consider a simple ``Account`` template, with a single choice -``Account_Transfer`` for transfering from one account to another. Note that if -someone tries to transfer more than they own, the choice should just do nothing. - -.. code-block:: daml - module Demo where - template Account - with - amount : Decimal - owner : Party - where - ensure amount > 0.0 - - signatory owner - - -- | Transfer some amount to the receiver, or do nothing if this would make the - -- remaining amount in the account negative. - nonconsuming choice Account_Transfer : (ContractId Account, ContractId Account) - with - transferAmount: Decimal - receiverCid: ContractId Account - controller owner - do - if amount >= transferAmount - then do - -- The account has sufficient funds. - receiver <- fetch receiverCid - newSelf <- create this with amount = amount - transferAmount - newReceiver <- create receiver with - amount = receiver.amount + transferAmount - archive receiverCid - return (newSelf, newReceiver) - else do - -- The account does not have sufficient funds, and the transfer is - -- cancelled. - return (self, receiverCid) - -It is clear that making a transfer between two accounts, should always preserve -the total amount of funds. However, running the verification tool produces the -following output: - -.. code-block:: - > bazel run //compiler/daml-lf-verify:daml-lf-verify -- demo.dar --choice Demo:Account.Account_Transfer --field Demo:Account.amount - - ... - - ========== - - Main flow: - - Create: [ if this_6.amount >= arg_5.transferAmount then this_6.amount - arg_5.transferAmount else 0 % 1 - , if this_6.amount >= arg_5.transferAmount then receiver_9.amount + arg_5.transferAmount else 0 % 1 ] - Archive: [ if this_6.amount >= arg_5.transferAmount then receiver_9.amount else 0 % 1 ] - Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: receiver_9.amount > 0.0 - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: this_6.amount > 0.0 - Assert: this_6.amount > 0.0 - Assert: receiver_9.amount > 0.0 - ~~~~~~~~~~ - - Fail. The choice Account_Transfer does not preserve the field amount. Counter example: - this_10.amount = (/ 1.0 2.0) - this_12.amount = 0.0 - receiver_9.amount = (/ 1.0 4.0) - arg_5.transferAmount = (- - (/ 1.0 4.0)) - this_6.amount = (/ 1.0 4.0) - - ========== - - Done. - -The ``Main flow`` describes all updates performed when exercising the -``Account_Transfer`` choice, without making any additional assumptions on the -inputs. It enumerates all create and archive updates, along with a number of -additional assertions (e.g. arising from the ``ensure`` statement in ``Account``). - -The SMT solver figured out that the choice does not actually preserve the total -amount, and provides a handy counter example. In fact, it turns out that we're -creating more money than archiving. A closer look at the create and archive -updates clearly shows that we're never archiving ``this_6.amount``. And indeed, -we forgot to include ``archive self`` in the example. After -adding this line to the definition of ``Account_Transfer``, the new output is as -follows: - -.. code-block:: - > bazel run //compiler/daml-lf-verify:daml-lf-verify -- demo.dar --choice Demo:Account.Account_Transfer --field Demo:Account.amount - - ... - - ========== - - Main flow: - - Create: [ if this_6.amount >= arg_5.transferAmount then this_6.amount - arg_5.transferAmount else 0 % 1 - , if this_6.amount >= arg_5.transferAmount then receiver_9.amount + arg_5.transferAmount else 0 % 1 ] - Archive: [ if this_6.amount >= arg_5.transferAmount then this_6.amount else 0 % 1 - , if this_6.amount >= arg_5.transferAmount then receiver_9.amount else 0 % 1 ] - Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: receiver_9.amount > 0.0 - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: this_6.amount > 0.0 - Assert: this_6.amount > 0.0 - Assert: receiver_9.amount > 0.0 - ~~~~~~~~~~ - - Success! The choice Account_Transfer preserves the field amount. - - ========== - - Done. - -Now the verification tool can prove that ``Account_Transfer`` does in fact -preserve the ``amount`` field. - -Example 2: Recursion --------------------- - -For a second example, consider the ``Account_Divide`` choice, which recursively -donates 1.0 amount from the donor to the receiver account, until the receiver -account has at least as much funds as the donor. - -.. code-block:: daml - -- | Iteratively transfer 1.0 amount to the receiver, until it has at - -- least as much funds as the donor. - nonconsuming Account_Divide : (ContractId Account, ContractId Account) - with - receiverCid: ContractId Account - do - receiverAccount <- fetch receiverCid - if amount <= receiverAccount.amount - -- The receiver has at least as much funds as the donor. - then return (self, receiverCid) - -- The receiver does not yet have enough funds. Make a new transaction. - else do - (newSelf, newReceiver) <- exercise self Account_Transfer with - transferAmount = 1.0, receiverCid = receiverCid - exercise newSelf Account_Divide with receiverCid = newReceiver - -We can again use the formal verification tool to ensure that ``Account_Divide`` -always preserves the field ``amount``. - -.. code-block:: - > bazel run //compiler/daml-lf-verify:daml-lf-verify -- demo.dar --choice Demo:Account.Account_Divide --field Demo:Account.amount - - ... - - ========== - - Main flow: - - Create: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount - 1 % 1 else 0 % 1 - , if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount + 1 % 1 else 0 % 1 ] - Archive: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount else 0 % 1 - , if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount else 0 % 1 ] - Assert: this_18.amount > 0.0 - Assert: receiverAccount_21.amount > 0.0 - Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: receiver_9.amount > 0.0 - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: this_6.amount > 0.0 - Assert: this_6.amount > 0.0 - Assert: receiver_9.amount > 0.0 - ~~~~~~~~~~ - - Success! The choice Account_Divide preserves the field amount. - - ========== - - Recursion cycle: - - Create: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount - 1 % 1 else 0 % 1 - , if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount + 1 % 1 else 0 % 1 ] - Archive: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount else 0 % 1 - , if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount else 0 % 1 ] - Assert: this_18.amount > 0.0 - Assert: receiverAccount_21.amount > 0.0 - Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: receiver_9.amount > 0.0 - Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount - Assert: this_6.amount > 0.0 - Assert: this_6.amount > 0.0 - Assert: receiver_9.amount > 0.0 - ~~~~~~~~~~ - - Success! The choice Account_Divide preserves the field amount. - - ========== - - Done. - -Note that besides the ``Main flow`` verification, the tool also isolates any -(mutual) recursion cycles within the choice. In this scenario, ``Account_Divide`` -has one recursion cycle, shown under ``Recursion cycle``. In order for a field -to be preserved, the choice has to always terminate, and every cycle has to -preserve the given field. - -Testing Framework -================= - -A testing framework is provided for working on the verification tool. Run the -tests as follows: - -.. code-block:: - > bazel run //compiler/daml-lf-verify:verify-tests - ... - All 23 tests passed (9.44s) diff --git a/compiler/daml-lf-verify/daml/conditionals/daml/Conditional.daml b/compiler/daml-lf-verify/daml/conditionals/daml/Conditional.daml deleted file mode 100644 index ce9168498b20..000000000000 --- a/compiler/daml-lf-verify/daml/conditionals/daml/Conditional.daml +++ /dev/null @@ -1,60 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - - -module Conditional where - -template Cond with - owner: Party - content: Int - where - signatory owner - - choice SuccA: ContractId Cond - controller owner - do - if False - then create Cond with owner; content = content - else create Cond with owner; content = content - - choice SuccB: ContractId Cond - controller owner - do - if 1 == 1 - then create Cond with owner; content = content - else create Cond with owner; content = 0 - - choice SuccC: ContractId Cond - controller owner - do - if True - then do - _ <- create Cond with owner; content = content - create Cond with owner; content = 0 - else create Cond with owner; content = content - - choice SuccD: ContractId Cond - controller owner - do - if True - then do - cid1 <- create Cond with owner; content = content - archive cid1 - create Cond with owner; content = content - else create Cond with owner; content = content - - choice FailA: ContractId Cond - controller owner - do - if 1 == 1 - then create Cond with owner; content = 0 - else create Cond with owner; content = content - - choice FailB: ContractId Cond - controller owner - do - if False - then create Cond with owner; content = content - else do - _ <- create Cond with owner; content = content - create Cond with owner; content = content diff --git a/compiler/daml-lf-verify/daml/general/daml/General.daml b/compiler/daml-lf-verify/daml/general/daml/General.daml deleted file mode 100644 index 411385a2dee0..000000000000 --- a/compiler/daml-lf-verify/daml/general/daml/General.daml +++ /dev/null @@ -1,65 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - - -module General where - -template Gen with - owner: Party - content: Int - where - signatory owner - - choice SuccA: ContractId Gen - controller owner - do create this with content - - choice SuccB: ContractId Gen - controller owner - do create this - - nonconsuming choice FailA: ContractId Gen - with - amount: Int - controller owner - do - create Gen with owner; content = amount - - -- Test abstraction over updates. - - nonconsuming choice SuccC: () - controller owner - do let _ = archive self - pure () - - nonconsuming choice SuccD: () - controller owner - do let _ = create Gen with owner; content = 1 - pure () - - nonconsuming choice SuccE: () - controller owner - do let x = create Gen with owner; content = 0 - _ <- x - pure () - - choice SuccF: () - controller owner - do let x = create Gen with owner; content = 1 - _ <- x - _ <- x - _ <- create this with content = content - 2 - pure () - - nonconsuming choice FailB: () - controller owner - do let x = create Gen with owner; content = 1 - _ <- x - pure () - - -- Test exercise. - - choice SuccG: () - controller owner - do _ <- exercise self FailA with amount = content - pure () \ No newline at end of file diff --git a/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml b/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml deleted file mode 100644 index cdd4b6b3aca8..000000000000 --- a/compiler/daml-lf-verify/daml/quickstart/daml/Iou.daml +++ /dev/null @@ -1,89 +0,0 @@ --- Copyright (c) 2022 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 - - -- Split the IOU by dividing the amount. - choice Iou_Split : (IouCid, IouCid) - with - splitAmount: Decimal - controller owner - 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. - choice Iou_Merge : IouCid - with - otherCid: IouCid - controller owner - 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 - - choice Iou_Transfer : ContractId IouTransfer - with - newOwner : Party - controller owner - do create IouTransfer with iou = this; newOwner - - choice Iou_AddObserver : IouCid - with - newObserver : Party - controller owner - do create this with observers = newObserver :: observers - - choice Iou_RemoveObserver : IouCid - with - oldObserver : Party - controller owner - do create this with observers = filter (/= oldObserver) observers - -template IouTransfer - with - iou : Iou - newOwner : Party - where - signatory iou.issuer, iou.owner - - choice IouTransfer_Cancel : IouCid - controller iou.owner - do create iou - - choice IouTransfer_Reject : IouCid - controller newOwner - do create iou - - choice IouTransfer_Accept : IouCid - controller newOwner - 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 deleted file mode 100644 index df82f45def34..000000000000 --- a/compiler/daml-lf-verify/daml/quickstart/daml/IouTrade.daml +++ /dev/null @@ -1,50 +0,0 @@ --- Copyright (c) 2022 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 - - choice IouTrade_Accept : (IouCid, IouCid) - with - quoteIouCid : IouCid - controller seller - 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) - - choice TradeProposal_Reject : () - controller seller - do return () diff --git a/compiler/daml-lf-verify/daml/recursion/daml/Recursion.daml b/compiler/daml-lf-verify/daml/recursion/daml/Recursion.daml deleted file mode 100644 index 5a3e3ac7de86..000000000000 --- a/compiler/daml-lf-verify/daml/recursion/daml/Recursion.daml +++ /dev/null @@ -1,143 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - - -module Recursion where - -type IouCid = ContractId Iou - -template Iou - with - issuer : Party - owner : Party - currency : Text - amount : Decimal - observers : [Party] - where - - signatory issuer, owner - - observer observers - - -- Test recursion A - - nonconsuming choice TestRecA : IouCid - controller owner - do - archive self - _ <- create this with amount = amount - exercise self TestRecA - - -- Test recursion B - - nonconsuming choice TestRecB : IouCid - with - var: Int - controller owner - do - if var > 0 - then do - exercise self TestRecB with var = (var - 1) - else do - archive self - create this with amount = amount - - -- Test recursion C - - nonconsuming choice Iou_Divide : (IouCid, IouCid) - with - receiverCid: IouCid - controller owner - do - receiverIou <- fetch receiverCid - if amount <= receiverIou.amount - then return (self, receiverCid) - else do - newSelf <- create this with amount = amount - 1.0 - newReceiver <- create receiverIou with amount = receiverIou.amount + 1.0 - archive self - archive receiverCid - exercise newSelf Iou_Divide with receiverCid = newReceiver - - -- Test mutual recursion A - - nonconsuming choice TestMutA1 : IouCid - controller owner - do - _ <- create this with amount = 1.0 - exercise self TestMutA2 - - nonconsuming choice TestMutA2 : IouCid - controller owner - do - _ <- create this with amount = -1.0 - res <- exercise self TestMutA1 - _ <- create this with amount = 1.0 - return res - - -- Test mutual recursion B - - nonconsuming choice TestMutB1 : IouCid - controller owner - do - _ <- create this with amount = 1.0 - exercise self TestMutB2 - create this with amount = 5.0 - - nonconsuming choice TestMutB2 : IouCid - controller owner - do - _ <- create this with amount = 2.0 - exercise self TestMutB3 - - nonconsuming choice TestMutB3 : IouCid - controller owner - do - _ <- create this with amount = 3.0 - exercise self TestMutB4 - - nonconsuming choice TestMutB4 : IouCid - controller owner - do - _ <- create this with amount = 4.0 - exercise self TestMutB1 - - -- Test mutual recursion C - - nonconsuming choice Iou_Divide_Mut : (IouCid, IouCid) - with - receiverCid: IouCid - controller owner - do - receiverIou <- fetch receiverCid - if amount <= receiverIou.amount - then return (self, receiverCid) - else do - exercise self Iou_Divide_Sub with receiverCid = receiverCid - - choice Iou_AddOne : IouCid - controller owner - do - create this with amount = amount + 1.0 - - choice Iou_SubOne : IouCid - controller owner - do - create this with amount = amount - 1.0 - - nonconsuming choice Iou_Divide_Sub : (IouCid, IouCid) - with - receiverCid: IouCid - controller owner - do - newSelf <- exercise self Iou_SubOne - exercise newSelf Iou_Divide_Add with receiverCid = receiverCid - - nonconsuming choice Iou_Divide_Add : (IouCid, IouCid) - with - receiverCid: IouCid - controller owner - do - receiverIou <- fetch receiverCid - newReceiver <- exercise receiverCid Iou_AddOne - exercise self Iou_Divide_Mut with receiverCid = newReceiver diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs deleted file mode 100644 index 5e339cbd417d..000000000000 --- a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify.hs +++ /dev/null @@ -1,132 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - -{-# LANGUAGE DataKinds #-} - --- | Static verification of DAML packages. -module DA.Daml.LF.Verify - ( main - , verify - ) where - -import Data.Maybe -import qualified Data.NameMap as NM -import Options.Applicative -import System.Exit -import System.IO - -import DA.Daml.LF.Ast.Base -import DA.Daml.LF.Verify.Generate -import DA.Daml.LF.Verify.Solve -import DA.Daml.LF.Verify.Read -import DA.Daml.LF.Verify.Context -import DA.Daml.LF.Verify.ReferenceSolve -import DA.Bazel.Runfiles - -getSolver :: IO FilePath -getSolver = locateRunfiles "z3_nix/bin/z3" - -main :: IO () -main = do - Options{..} <- execParser optionsParserInfo - let (choiceMod, choiceTmpl, choiceName) = optChoice - (fieldMod, fieldTmpl, fieldName) = optField - _ <- verify optInputDar putStrLn choiceMod choiceTmpl choiceName fieldMod fieldTmpl fieldName - putStrLn "\n==========\n" - putStrLn "Done." - -outputError :: Error - -- ^ The error message. - -> String - -- ^ An additional message providing context. - -> IO a -outputError err msg = do - hPutStrLn stderr msg - hPrint stderr err - exitFailure - --- | Execute the full verification pipeline. -verify :: FilePath - -- ^ The DAR file to load. - -> (String -> IO ()) - -- ^ Function for debugging printouts. - -> ModuleName - -- ^ The module in which the given choice is defined. - -> TypeConName - -- ^ The template in which the given choice is defined. - -> ChoiceName - -- ^ The choice to be verified. - -> ModuleName - -- ^ The module in which the given field is defined. - -> TypeConName - -- ^ The template in which the given field is defined. - -> FieldName - -- ^ The field to be verified. - -> IO [Result] -verify dar debug choiceModName choiceTmplName choiceName fieldModName fieldTmplName fieldName = do - -- Read the packages to analyse, and initialise the provided solver. - pkgs <- readPackages [dar] - solver <- getSolver - -- Find the given template names in the packages. - choiceTmpl <- findTemplate pkgs choiceModName choiceTmplName - fieldTmpl <- findTemplate pkgs fieldModName fieldTmplName - -- Start reading data type and value definitions. References to other - -- values are just stored as references at this point. - case runEnv (genPackages pkgs) (emptyEnv :: Env 'ValueGathering) of - Left err-> outputError err "Value phase finished with error: " - Right env1 -> do - -- All value definitions have been handled. Start computing closures of - -- the stored value references. After this phase, all value references - -- should be inlined. - let env2 = solveValueReferences env1 - -- Start reading template definitions. References to choices are just - -- stored as references at this point. - case runEnv (genPackages pkgs) env2 of - Left err -> outputError err "Choice phase finished with error: " - Right env3 -> do - -- All choice definitions have been handled. Start computing closures - -- of the stored choice references. After this phase, all choice - -- references should be inlined. - let env4 = solveChoiceReferences env3 - -- Construct the actual constraints to be solved by the SMT solver. - let csets = constructConstr env4 choiceTmpl choiceName fieldTmpl fieldName - mapM (debugAndSolve solver) csets - where - -- | Output some debugging information and solve the given constraints. - debugAndSolve :: FilePath -> ConstraintSet -> IO Result - debugAndSolve solver cset = do - -- Pass the constraints to the SMT solver. - (debug_info, result) <- solveConstr solver cset - debug $ debug_info choiceName fieldName - return result - - -- | Lookup the first package that defines the given template. This avoids - -- having to pass in the package reference manually when using the tool. - findTemplate :: [(PackageId, (Package, Maybe PackageName))] - -- ^ The package from the DAR file. - -> ModuleName - -- ^ The module name. - -> TypeConName - -- ^ The template name. - -> IO (Qualified TypeConName) - findTemplate pkgs mod tem = maybe - (outputError (UnknownTmpl tem) "Parsing phase finished with error: ") - (\pacid -> return $ Qualified (PRImport pacid) mod tem) - (listToMaybe $ mapMaybe (templateInPackage mod tem) pkgs) - - -- | Return the package id of the module containing the given template, if - -- it exists. - templateInPackage :: ModuleName - -- ^ The module to look for. - -> TypeConName - -- ^ The template to look for. - -> (PackageId, (Package, Maybe PackageName)) - -- ^ The package to look in. - -> Maybe PackageId - templateInPackage modName temName (id, (pac,_)) = - case NM.lookup modName $ packageModules pac of - Nothing -> Nothing - Just mod -> case NM.lookup temName $ moduleTemplates mod of - Nothing -> Nothing - Just _ -> Just id - diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs deleted file mode 100644 index 476407c64673..000000000000 --- a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Context.hs +++ /dev/null @@ -1,963 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeFamilies #-} - --- | Contexts for Daml-LF static verification -module DA.Daml.LF.Verify.Context - ( Phase(..) - , IsPhase(..) - , BoolExpr(..) - , Cond(..) - , Rec(..) - , Env(..) - , Error(..) - , MonadEnv - , UpdateSet - , BaseUpd(..) - , Upd(..) - , ChoiceData(..) - , UpdChoice(..) - , Skolem(..) - , getEnv, putEnv - , runEnv - , genRenamedVar - , createCond - , introCond - , makeRec, makeMutRec - , addBaseUpd, addChoice - , emptyUpdateSet, extendUpdateSet, concatUpdateSet - , extVarEnv, extRecEnv, extRecEnvTCons, extValEnv, extChEnv, extDatsEnv - , extCidEnv, extPrecond, extCtrRec, extCtr - , lookupVar, lookupRec, lookupVal, lookupChoice, lookupDataCon, lookupCid - , conditionalUpdateSet - , computeCycles - , fieldName2VarName - , recTypConFields, recTypFields, recExpFields - , applySubstInUpd - ) where - -import Control.Monad.Error.Class (MonadError (..), throwError) -import Control.Monad.Extra (whenJust) -import Control.Monad.State.Lazy -import Data.Hashable -import GHC.Generics -import Data.Maybe (isJust) -import Data.List (find) -import Data.Bifunctor -import qualified Data.HashMap.Strict as HM -import qualified Data.Text as T -import Debug.Trace - -import DA.Daml.LF.Ast hiding (lookupChoice) -import DA.Daml.LF.Ast.Subst - --- | Data type denoting the phase of the constraint generator. -data Phase - = ValueGathering - -- ^ The value phase gathers all value and data type definitions across modules. - | ChoiceGathering - -- ^ The choice phase gathers the updates performed in choice definitions. - | Solving - -- ^ During the solving phase, all definitions have been loaded and updates - -- have been inlined. - --- | Data type denoting a boolean condition expression. This data type was --- introduced as DAML-LF does not have build-in boolean operators, and using --- prelude functions gets messy. -data BoolExpr - = BExpr Expr - -- ^ A daml-lf expression. - | BAnd BoolExpr BoolExpr - -- ^ And operator. - | BNot BoolExpr - -- ^ Not operator. - | BEq Expr Expr - -- ^ Equality operator. - | BGt Expr Expr - -- ^ Greater than operator. - | BGtE Expr Expr - -- ^ Greater than or equal operator. - | BLt Expr Expr - -- ^ Less than operator. - | BLtE Expr Expr - -- ^ Less than or equal operator. - deriving (Eq, Show) - --- | Convert an expression constraint into boolean expressions. --- This function covers the supported operations in `ensure` statements. --- Operations that are not currently supported trigger a warning, and are then --- ignored for the remainder of the verification process. No harm comes from an --- unsupported operation. -toBoolExpr :: Expr -> [BoolExpr] -toBoolExpr (EBuiltin (BEBool True)) = [] -toBoolExpr (ETmApp (ETmApp op e1) e2) = case op of - (EBuiltin (BEEqual _)) -> [BEq e1 e2] - (ETyApp (EBuiltin BEGreaterNumeric) _) -> [BGt e1 e2] - (ETyApp (EBuiltin BEGreaterEqNumeric) _) -> [BGtE e1 e2] - (ETyApp (EBuiltin BELessNumeric) _) -> [BLt e1 e2] - (ETyApp (EBuiltin BELessEqNumeric) _) -> [BLtE e1 e2] - (ETyApp (EBuiltin BEEqualGeneric) _) -> [BEq e1 e2] - (ETyApp (EBuiltin BEGreaterGeneric) _) -> [BGt e1 e2] - (ETyApp (EBuiltin BEGreaterEqGeneric) _) -> [BGtE e1 e2] - (ETyApp (EBuiltin BELessGeneric) _) -> [BLt e1 e2] - (ETyApp (EBuiltin BELessEqGeneric) _) -> [BLtE e1 e2] - _ -> trace ("Warning: Unmatched Expr to BoolExpr Operator: " ++ show op) [] -toBoolExpr exp = trace ("Warning: Unmatched Expr to BoolExpr: " ++ show exp) [] - --- | Data type denoting a potentially conditional value. -data Cond a - = Determined a - -- ^ Non-conditional value. - | Conditional BoolExpr [Cond a] [Cond a] - -- ^ Conditional value, with a (Boolean) condition, values in case - -- the condition holds, and values in case it doesn't. - deriving (Eq, Show, Functor) - --- | Construct a simple conditional. -createCond :: BoolExpr - -- ^ The condition to depend on. - -> a - -- ^ The value in case the condition holds. - -> a - -- ^ The value in case the condition does not hold. - -> Cond a -createCond cond x y = Conditional cond [Determined x] [Determined y] - -extCond :: Eq a => BoolExpr -> Cond a -> [Cond a] -extCond bexp cond = - let cond' = case cond of - (Determined x) -> Conditional bexp [Determined x] [] - (Conditional bexp' xs ys) -> Conditional (bexp `BAnd` bexp') xs ys - in simplifyCond cond' - --- | Perform common simplifications on Conditionals. --- This simplification should never alter the meaning of the constraints in any --- way. It's only purpose is to simplify the output shown to the user. --- TODO: This can be extended with additional cases in the future. -simplifyCond :: Eq a => Cond a -> [Cond a] -simplifyCond (Conditional (BAnd b1 b2) xs ys) - | b1 == b2 = simplifyCond (Conditional b1 xs ys) - | b1 == BNot b2 = ys - | b2 == BNot b1 = ys -simplifyCond (Conditional b [Conditional b1 xs1 _] [Conditional b2 _ ys2]) - | b1 == b2 = simplifyCond (Conditional b xs1 ys2) -simplifyCond (Conditional _ xs ys) - | xs == ys = concatMap simplifyCond xs -simplifyCond c = [c] - --- | Shift the conditional inside of the update set, by extending each update --- with the condition. -introCond :: IsPhase ph => Cond (UpdateSet ph) -> UpdateSet ph -introCond (Determined upds) = upds -introCond (Conditional e updx updy) = buildCond e updx updy extCondUpd - where - -- | Construct a single conditional update set, combining the two input lists - -- and the boolean expression, if the input is non-empty. - buildCond :: IsPhase ph - => BoolExpr - -> [Cond (UpdateSet ph)] - -> [Cond (UpdateSet ph)] - -> (BoolExpr -> Upd ph -> UpdateSet ph) - -> UpdateSet ph - buildCond bexp cxs cys ext = - let xs = concatMap introCond cxs - ys = concatMap introCond cys - in concatMap (ext bexp) xs ++ concatMap (ext $ BNot bexp) ys - --- | Data type denoting a potential recursion cycle. -data Rec a - = Simple a - -- ^ Basic, non-recursive value. - | Rec [a] - -- ^ (Possibly multiple) recursion cycles. - -- Note that future optimisations could possible introduce an empty list here, - -- so no assumptions are made that this list is non-empty. - | MutRec [(String,a)] - -- ^ (Possibly multiple) mutual recursion cycles. - -- Note that this behaves idential to regular recursion, with the addition of - -- an information field for debugging purposes. - -- In the current version, this String stores the names of all values or - -- choices in the cycle. - deriving Functor - --- | Split a list of Rec values by constructor. -splitRecs :: [Rec [a]] -> ([a], [Rec [a]], [Rec [a]]) -splitRecs inp = (simples, recs, mutrecs) - where - simples = concat [x | Simple x <- inp] - recs = [Rec xs | Rec xs <- inp] - mutrecs = [MutRec xs | MutRec xs <- inp] - --- | Introduce a Rec constructor. --- Note that nested recursion is flattened. This is fine as each cycles has to --- preserve the field, meaning that the total result should be a nop for field. -makeRec :: [Rec [Cond a]] -> [Rec [Cond a]] -makeRec inp = Rec [simples] : recs ++ mutrecs - where - (simples, recs, mutrecs) = splitRecs inp - --- | Introduce a MutRec constructor. -makeMutRec :: [Rec [Cond a]] -> String -> [Rec [Cond a]] -makeMutRec inp str = MutRec [(str,simples)] : recs ++ mutrecs - where - (simples, recs, mutrecs) = splitRecs inp - --- | Take a conditional Rec value apart, by splitting into the simple values, --- and constructing a list of all possible cycles (along with some debugging --- information). -computeCycles :: [Rec [Cond a]] -> [(String, [Cond a])] -computeCycles inp = ("Main flow: ", simples) : recs - where - simples = concat [x | Simple x <- inp] - recs = [("Recursion cycle: ", x) | Rec xs <- inp, x <- xs] - ++ [("Mutual recursion cycle: " ++ info, x) | MutRec xs <- inp, (info, x) <- xs] - --- | Data type denoting a simple update. -data BaseUpd - = UpdCreate - -- ^ Data type denoting a create update. - { _creTemp :: !(Qualified TypeConName) - -- ^ Qualified type constructor corresponding to the contract template. - , _creField :: ![(FieldName, Expr)] - -- ^ The fields to be verified, together with their value. - } - | UpdArchive - -- ^ Data type denoting an archive update. - { _arcTemp :: !(Qualified TypeConName) - -- ^ Qualified type constructor corresponding to the contract template. - , _arcField :: ![(FieldName, Expr)] - -- ^ The fields to be verified, together with their value. - } - deriving (Eq, Show) - --- | The collection of updates being performed. -type UpdateSet ph = [Upd ph] - --- | Construct an empty update set. -emptyUpdateSet :: UpdateSet ph -emptyUpdateSet = [] - --- | Extend an update set. -extendUpdateSet :: Upd ph -> UpdateSet ph -> UpdateSet ph -extendUpdateSet = (:) - --- | Combine two update sets. -concatUpdateSet :: UpdateSet ph -> UpdateSet ph -> UpdateSet ph -concatUpdateSet = (++) - --- | Data type denoting an exercised choice. -data UpdChoice = UpdChoice - { _choTemp :: !(Qualified TypeConName) - -- ^ Qualified type constructor corresponding to the contract template. - , _choName :: !ChoiceName - -- ^ The name of the choice. - } - deriving (Eq, Generic, Hashable, Show) - --- | Class containing the environment, and operations on it, for each generator phase. -class IsPhase (ph :: Phase) where - -- | The updates which can be performed. - data Upd ph - -- | The environment for the DAML-LF verifier. - data Env ph - -- | Construct a base update. - baseUpd :: Rec [Cond BaseUpd] -> Upd ph - -- | Construct a choice exercise update. - choiceUpd :: Cond UpdChoice -> Upd ph - -- | Construct a value update. - valueUpd :: Cond (Qualified ExprValName) -> Upd ph - -- | Map over a single base update. - mapBaseUpd :: (Rec [Cond BaseUpd] -> Upd ph) -> Upd ph -> Upd ph - -- | Check whether the update set contains any choice references. - containsChoiceRefs :: UpdateSet ph -> Bool - -- | Extend the conditional of an update. - extCondUpd :: BoolExpr -> Upd ph -> UpdateSet ph - -- | Construct an empty environment. - emptyEnv :: Env ph - -- | Get the skolemised term variables and fields from the environment. - envSkols :: Env ph -> [Skolem] - -- | Update the skolemised term variables and fields in the environment. - setEnvSkols :: [Skolem] -> Env ph -> Env ph - -- | Get the bound values from the environment. - envVals :: Env ph -> HM.HashMap (Qualified ExprValName) (Expr, UpdateSet ph) - -- | Get the data constructors from the environment. - envDats :: Env ph -> HM.HashMap (Qualified TypeConName) DefDataType - -- | Get the fetched cid's mapped to their current variable name, along with - -- a list of any potential old variable names, from the environment. - envCids :: Env ph -> HM.HashMap Cid (ExprVarName, [ExprVarName]) - -- | Update the fetched cid's in the environment. - setEnvCids :: HM.HashMap Cid (ExprVarName, [ExprVarName]) -> Env ph -> Env ph - -- | Get the set of preconditions from the environment. - envPreconds :: Env ph -> HM.HashMap (Qualified TypeConName) (Expr -> Expr) - -- | Get the additional constraints from the environment. - envCtrs :: Env ph -> [BoolExpr] - -- | Update the additional constraints in the environment. - setEnvCtrs :: [BoolExpr] -> Env ph -> Env ph - -- | Get the set of relevant choices from the environment. - envChoices :: Env ph -> HM.HashMap UpdChoice (ChoiceData ph) - -instance IsPhase 'ValueGathering where - data Upd 'ValueGathering - = UpdVGBase ![Cond BaseUpd] - -- ^ A base update. - | UpdVGChoice !(Cond UpdChoice) - -- ^ An exercised choice. - | UpdVGVal !(Cond (Qualified ExprValName)) - -- ^ A referenced value. - data Env 'ValueGathering = EnvVG - ![Skolem] - -- ^ The skolemised term variables and fields. - !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering)) - -- ^ The bound values. - !(HM.HashMap (Qualified TypeConName) DefDataType) - -- ^ The set of data constructors. - !(HM.HashMap Cid (ExprVarName, [ExprVarName])) - -- ^ The set of fetched cid's mapped to their current variable name, along - -- with a list of any potential old variable names. - ![BoolExpr] - -- ^ Additional constraints. - baseUpd = \case - Simple upd -> UpdVGBase upd - _ -> error "The value gathering phase can't contain recursive updates." - choiceUpd = UpdVGChoice - valueUpd = UpdVGVal - mapBaseUpd f = \case - UpdVGBase b -> f (Simple b) - upd -> upd - containsChoiceRefs upds = not $ null [x | UpdVGChoice x <- upds] - extCondUpd bexp = \case - (UpdVGBase base) -> map (UpdVGBase . extCond bexp) base - (UpdVGChoice cho) -> map UpdVGChoice $ extCond bexp cho - (UpdVGVal val) -> map UpdVGVal $ extCond bexp val - emptyEnv = EnvVG [] HM.empty HM.empty HM.empty [] - envSkols (EnvVG sko _ _ _ _) = sko - setEnvSkols sko (EnvVG _ val dat cid ctr) = EnvVG sko val dat cid ctr - envVals (EnvVG _ val _ _ _) = val - envDats (EnvVG _ _ dat _ _) = dat - envCids (EnvVG _ _ _ cid _) = cid - setEnvCids cid (EnvVG sko val dat _ ctr) = EnvVG sko val dat cid ctr - envPreconds _ = HM.empty - envCtrs (EnvVG _ _ _ _ ctr) = ctr - setEnvCtrs ctr (EnvVG sko val dat cid _) = EnvVG sko val dat cid ctr - envChoices _ = HM.empty - -instance IsPhase 'ChoiceGathering where - data Upd 'ChoiceGathering - = UpdCGBase !(Rec [Cond BaseUpd]) - -- ^ A single recursion cycle, containing a list of updates. - | UpdCGChoice !(Cond UpdChoice) - -- ^ An exercised choice. - data Env 'ChoiceGathering = EnvCG - ![Skolem] - -- ^ The skolemised term variables and fields. - !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ChoiceGathering)) - -- ^ The bound values. - !(HM.HashMap (Qualified TypeConName) DefDataType) - -- ^ The set of data constructors. - !(HM.HashMap Cid (ExprVarName, [ExprVarName])) - -- ^ The set of fetched cid's mapped to their current variable name, along - -- with a list of any potential old variable names. - !(HM.HashMap (Qualified TypeConName) (Expr -> Expr)) - -- ^ The set of preconditions per template. The precondition is represented - -- using a function from the `this` variable to the constraint expression. - ![BoolExpr] - -- ^ Additional constraints. - !(HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering)) - -- ^ The set of relevant choices. - baseUpd = UpdCGBase - choiceUpd = UpdCGChoice - valueUpd = error "The choice gathering phase no longer contains value references." - mapBaseUpd f = \case - UpdCGBase b -> f b - upd -> upd - containsChoiceRefs upds = not $ null [x | UpdCGChoice x <- upds] - extCondUpd bexp = \case - (UpdCGBase base) -> - let base' = case base of - Simple upd -> map (Simple . extCond bexp) upd - Rec cycles -> [Rec $ map (concatMap (extCond bexp)) cycles] - MutRec cycles -> [MutRec $ map (second (concatMap (extCond bexp))) cycles] - in map UpdCGBase base' - (UpdCGChoice cho) -> map UpdCGChoice (extCond bexp cho) - emptyEnv = EnvCG [] HM.empty HM.empty HM.empty HM.empty [] HM.empty - envSkols (EnvCG sko _ _ _ _ _ _) = sko - setEnvSkols sko (EnvCG _ val dat cid pre ctr cho) = EnvCG sko val dat cid pre ctr cho - envVals (EnvCG _ val _ _ _ _ _) = val - envDats (EnvCG _ _ dat _ _ _ _) = dat - envCids (EnvCG _ _ _ cid _ _ _) = cid - setEnvCids cid (EnvCG sko val dat _ pre ctr cho) = EnvCG sko val dat cid pre ctr cho - envPreconds (EnvCG _ _ _ _ pre _ _) = pre - envCtrs (EnvCG _ _ _ _ _ ctr _) = ctr - setEnvCtrs ctr (EnvCG sko val dat cid pre _ cho) = EnvCG sko val dat cid pre ctr cho - envChoices (EnvCG _ _ _ _ _ _ cho) = cho - -instance IsPhase 'Solving where - data Upd 'Solving - = UpdSBase !(Rec [Cond BaseUpd]) - -- ^ A single recursion cycle, containing a list of updates. - data Env 'Solving = EnvS - ![Skolem] - -- ^ The skolemised term variables and fields. - !(HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'Solving)) - -- ^ The bound values. - !(HM.HashMap (Qualified TypeConName) DefDataType) - -- ^ The set of data constructors. - !(HM.HashMap Cid (ExprVarName, [ExprVarName])) - -- ^ The set of fetched cid's mapped to their current variable name, along - -- with a list of any potential old variable names. - !(HM.HashMap (Qualified TypeConName) (Expr -> Expr)) - -- ^ The set of preconditions per template. The precondition is represented - -- using a function from the `this` variable to the constraint expression. - ![BoolExpr] - -- ^ Additional constraints. - !(HM.HashMap UpdChoice (ChoiceData 'Solving)) - -- ^ The set of relevant choices. - baseUpd = UpdSBase - choiceUpd = error "The solving phase no longer contains choice references." - valueUpd = error "The solving phase no longer contains value references." - mapBaseUpd f (UpdSBase b) = f b - containsChoiceRefs _ = False - extCondUpd bexp (UpdSBase base) = - let base' = case base of - Simple upd -> map (Simple . extCond bexp) upd - Rec cycles -> [Rec $ map (concatMap (extCond bexp)) cycles] - MutRec cycles -> [MutRec $ map (second (concatMap (extCond bexp))) cycles] - in map UpdSBase base' - emptyEnv = EnvS [] HM.empty HM.empty HM.empty HM.empty [] HM.empty - envSkols (EnvS sko _ _ _ _ _ _) = sko - setEnvSkols sko (EnvS _ val dat cid pre ctr cho) = EnvS sko val dat cid pre ctr cho - envVals (EnvS _ val _ _ _ _ _) = val - envDats (EnvS _ _ dat _ _ _ _) = dat - envCids (EnvS _ _ _ cid _ _ _) = cid - setEnvCids cid (EnvS sko val dat _ pre ctr cho) = EnvS sko val dat cid pre ctr cho - envPreconds (EnvS _ _ _ _ pre _ _) = pre - envCtrs (EnvS _ _ _ _ _ ctr _) = ctr - setEnvCtrs ctr (EnvS sko val dat cid pre _ cho) = EnvS sko val dat cid pre ctr cho - envChoices (EnvS _ _ _ _ _ _ cho) = cho - --- | Update the bound values in the environment. -setEnvVals :: HM.HashMap (Qualified ExprValName) (Expr, UpdateSet 'ValueGathering) - -> Env 'ValueGathering -> Env 'ValueGathering -setEnvVals val (EnvVG sko _ dat cid ctr) = EnvVG sko val dat cid ctr - --- | Update the set of preconditions in the environment. -setEnvPreconds :: HM.HashMap (Qualified TypeConName) (Expr -> Expr) - -> Env 'ChoiceGathering -> Env 'ChoiceGathering -setEnvPreconds pre (EnvCG sko val dat cid _ ctr cho) = - EnvCG sko val dat cid pre ctr cho - --- | Update the data constructors in the environment. -setEnvDats :: HM.HashMap (Qualified TypeConName) DefDataType - -> Env 'ValueGathering -> Env 'ValueGathering -setEnvDats dat (EnvVG sko val _ cid ctr) = EnvVG sko val dat cid ctr - --- | Update the set of relevant choices in the environment. -setEnvChoices :: HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering) - -> Env 'ChoiceGathering -> Env 'ChoiceGathering -setEnvChoices cho (EnvCG sko val dat cid pre ctr _) = - EnvCG sko val dat cid pre ctr cho - --- | Add a single BaseUpd to an UpdateSet. -addBaseUpd :: IsPhase ph - => UpdateSet ph - -- ^ The update set to extend. - -> BaseUpd - -- ^ The update to add. - -> UpdateSet ph -addBaseUpd upds upd = baseUpd (Simple [Determined upd]) : upds - --- | Add a single choice reference to an UpdateSet. -addChoice :: IsPhase ph - => UpdateSet ph - -- ^ The update set to extend. - -> Qualified TypeConName - -- ^ The template name in which this choice is defined. - -> ChoiceName - -- ^ The choice name to add. - -> UpdateSet ph -addChoice upds tem cho = choiceUpd (Determined $ UpdChoice tem cho) : upds - --- | Make an update set conditional. A second update set can also be introduced --- for the case where the condition does not hold. -conditionalUpdateSet :: IsPhase ph - => Expr - -- ^ The condition on which to combine the two update sets. - -> UpdateSet ph - -- ^ The update set in case the condition holds. - -> UpdateSet ph - -- ^ The update set in case the condition does not hold. - -> UpdateSet ph -conditionalUpdateSet exp upd1 upd2 = - introCond $ createCond (BExpr exp) upd1 upd2 - --- | Refresh a given expression variable by producing a fresh renamed variable. -genRenamedVar :: MonadEnv m ph - => ExprVarName - -- ^ The variable to be renamed. - -> m ExprVarName -genRenamedVar (ExprVarName x) = ExprVarName . T.append x . T.pack <$> fresh - --- | Data type denoting a skolemized variable. -data Skolem - = SkolVar ExprVarName - -- ^ Skolemised term variable. - | SkolRec ExprVarName [FieldName] - -- ^ List of skolemised field names, with their variable. - -- e.g. `this.field` - deriving (Eq, Show) - --- | Data type denoting a contract id. -data Cid - = CidVar ExprVarName - -- ^ An expression variable denoting a contract id. - | CidRec ExprVarName FieldName - -- ^ A record projection denoting a contract id. - deriving (Generic, Hashable, Eq, Show) - --- | Convert an expression to a contract id, if possible. --- The function can optionally refresh the contract id, and returns both the --- converted contract id, and the substitution originating from the refresh. -expr2cid :: (IsPhase ph, MonadEnv m ph) - => Bool - -- ^ Whether or not the refresh the contract id. - -> Expr - -- ^ The expression to be converted. - -> m (Cid, Subst) -expr2cid b (EVar x) = do - (y, subst) <- refresh_cid b x - return (CidVar y, subst) -expr2cid b (ERecProj _ f (EVar x)) = do - (y, subst) <- refresh_cid b x - extRecEnv y [f] - return (CidRec y f, subst) -expr2cid b (EStructProj f (EVar x)) = do - (y, subst) <- refresh_cid b x - extRecEnv y [f] - return (CidRec y f, subst) -expr2cid _ _ = throwError ExpectCid - --- | Internal function, for refreshing a given contract id. -refresh_cid :: MonadEnv m ph - => Bool - -- ^ Whether or not the refresh the contract id. - -> ExprVarName - -- ^ The variable name to refresh. - -> m (ExprVarName, Subst) -refresh_cid False x = return (x, mempty) -refresh_cid True x = do - y <- genRenamedVar x - return (y, exprSubst x (EVar y)) - --- | Data type containing the data stored for a choice definition. -data ChoiceData (ph :: Phase) = ChoiceData - { _cdSelf :: ExprVarName - -- ^ The variable denoting `self`. - , _cdThis :: ExprVarName - -- ^ The variable denoting `this`. - , _cdArgs :: ExprVarName - -- ^ The variable denoting `args`. - , _cdUpds :: UpdateSet ph - -- ^ The updates performed by this choice. Note that this update set depends - -- on the above variables. - , _cdType :: Type - -- ^ The return type of this choice. - } - --- | Convert a fieldname into an expression variable name. -fieldName2VarName :: FieldName -> ExprVarName -fieldName2VarName = ExprVarName . unFieldName - --- | Type class constraint with the required monadic effects for functions --- manipulating the verification environment. -type MonadEnv m ph = (MonadError Error m, MonadState (Int,Env ph) m) - --- | Fetch the current environment. -getEnv :: MonadEnv m ph => m (Env ph) -getEnv = snd <$> get - --- | Set the current environment. -putEnv :: MonadEnv m ph => Env ph -> m () -putEnv env = get >>= \(uni,_) -> put (uni,env) - --- | Generate a new unique name. -fresh :: MonadEnv m ph => m String -fresh = do - (cur,env) <- get - put (cur + 1,env) - return $ "_" ++ show cur - --- | Evaluate the MonadEnv to produce an error message or the final environment. -runEnv :: StateT (Int, Env ph) (Either Error) () - -- ^ The monadic computation to be evaluated. - -> Env ph - -- ^ The initial environment to start from. - -> Either Error (Env ph) -runEnv comp env0 = do - (_res, (_uni,env1)) <- runStateT comp (0,env0) - return env1 - --- | Skolemise an expression variable and extend the environment. -extVarEnv :: (IsPhase ph, MonadEnv m ph) - => ExprVarName - -- ^ The expression variable to be skolemised. - -> m () -extVarEnv x = extSkolEnv (SkolVar x) - --- | Skolemise a list of record projection and extend the environment. -extRecEnv :: (IsPhase ph, MonadEnv m ph) - => ExprVarName - -- ^ The variable on which is being projected. - -> [FieldName] - -- ^ The fields which should be skolemised. - -> m () -extRecEnv x fs = do - env <- getEnv - let skols = envSkols env - -- Note that x might already be in the skolem list. We thus lookup the - -- current (latest) entry, and overwrite it with a new entry containing - -- both the current and new fields. - newFs = case [fs' | SkolRec x' fs' <- skols, x == x'] of - [] -> fs - (curFs:_) -> fs ++ curFs - extSkolEnv (SkolRec x newFs) - --- | Extend the environment with the fields of any given record or type --- constructor type. -extRecEnvTCons :: (IsPhase ph, MonadEnv m ph) - => [(FieldName, Type)] - -- ^ The given fields and their corresponding types to analyse. - -> m () -extRecEnvTCons = mapM_ step - where - step :: (IsPhase ph, MonadEnv m ph) => (FieldName, Type) -> m () - step (f,typ) = do - mbFields <- recTypFields typ - whenJust mbFields $ \fsRec -> - extRecEnv (fieldName2VarName f) $ map fst fsRec - --- | Extend the environment with a new skolem variable. -extSkolEnv :: (IsPhase ph, MonadEnv m ph) - => Skolem - -- ^ The skolem variable to add. - -> m () -extSkolEnv skol = do - env <- getEnv - when (notElem skol $ envSkols env) - (putEnv $ setEnvSkols (skol : envSkols env) env) - --- | Extend the environment with a new value definition. -extValEnv :: MonadEnv m 'ValueGathering - => Qualified ExprValName - -- ^ The name of the value being defined. - -> Expr - -- ^ The (partially) evaluated value definition. - -> UpdateSet 'ValueGathering - -- ^ The updates performed by this value. - -> m () -extValEnv val expr upd = do - env <- getEnv - putEnv $ setEnvVals (HM.insert val (expr, upd) $ envVals env) env - --- | Extends the environment with a new choice. -extChEnv :: MonadEnv m 'ChoiceGathering - => Qualified TypeConName - -- ^ The type of the template on which this choice is defined. - -> ChoiceName - -- ^ The name of the new choice. - -> ExprVarName - -- ^ Variable to bind the ContractId on which this choice is exercised on to. - -> ExprVarName - -- ^ Variable to bind the contract on which this choice is exercised on to. - -> ExprVarName - -- ^ Variable to bind the choice argument to. - -> UpdateSet 'ChoiceGathering - -- ^ The updates performed by the new choice. - -> Type - -- ^ The result type of the new choice. - -> m () -extChEnv tc ch self this arg upd typ = do - env <- getEnv - putEnv $ setEnvChoices (HM.insert (UpdChoice tc ch) (ChoiceData self this arg upd typ) $ envChoices env) env - --- | Extend the environment with a list of new data type definitions. -extDatsEnv :: MonadEnv m 'ValueGathering - => HM.HashMap (Qualified TypeConName) DefDataType - -- ^ A hashmap of the data constructor names, with their corresponding definitions. - -> m () -extDatsEnv hmap = do - env <- getEnv - putEnv $ setEnvDats (hmap `HM.union` envDats env) env - --- | Extend the environment with a refreshed contract id, and the variable to --- which the fetched contract is bound. Returns a substitution, mapping the --- given contract id, to the refreshed one. --- While it might seem counter intuitive, the function only refreshes the --- contract id on its first encounter. The reason is that it needs to be able to --- keep track of old bindings. --- Note that instead of overwriting old bindings, the function creates a new --- synonym between the old and new binding. -extCidEnv :: (IsPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether the contract id should be refreshed. - -- Note that even with the flag on, contract id are only refreshed on their - -- first encounter. - -> Expr - -- ^ The contract id expression. - -> ExprVarName - -- ^ The variable name to which the fetched contract is bound. - -> m Subst -extCidEnv b exp var = do - prev <- do - { (cur, old) <- lookupCid exp - ; return $ cur : old } - `catchError` (\_ -> return []) - proj_def <- check_proj_cid exp - (cid, subst) <- expr2cid (b && null prev && proj_def) exp - env <- getEnv - putEnv $ setEnvCids (HM.insert cid (var, prev) $ envCids env) env - return subst - where - -- | Internal function to check whether the given cid has not yet been - -- defined in a different projection. - check_proj_cid :: (IsPhase ph, MonadEnv m ph) - => Expr - -- ^ The cid expression to verify. - -> m Bool - check_proj_cid (ERecProj _ _ (EVar x)) = do - skols <- envSkols <$> getEnv - return $ null [fs' | SkolRec x' fs' <- skols, x == x'] - check_proj_cid (EStructProj _ (EVar x)) = do - skols <- envSkols <$> getEnv - return $ null [fs' | SkolRec x' fs' <- skols, x == x'] - check_proj_cid _ = return True - --- | Extend the environment with an additional precondition, assigned to the --- corresponding template. -extPrecond :: MonadEnv m 'ChoiceGathering - => Qualified TypeConName - -- ^ The template to assign the precondition to. - -> (Expr -> Expr) - -- ^ The precondition function, taking the `this` variable. - -> m () -extPrecond tem precond = do - env <- getEnv - putEnv (setEnvPreconds (HM.insert tem precond (envPreconds env)) env) - --- | Extend the environment with additional equality constraints, between a --- variable and its field values. -extCtrRec :: (IsPhase ph, MonadEnv m ph) - => ExprVarName - -- ^ The variable to be asserted. - -> [(FieldName, Expr)] - -- ^ The fields with their values. - -> m () -extCtrRec var fields = do - let ctrs = map (\(f, e) -> BEq e (EStructProj f (EVar var))) fields - env <- getEnv - putEnv $ setEnvCtrs (ctrs ++ envCtrs env) env - --- | Extend the environment with the given constraint. -extCtr :: (IsPhase ph, MonadEnv m ph) - => Expr - -- ^ The constraint to add. - -> m () -extCtr exp = do - let ctrs = toBoolExpr exp - env <- getEnv - putEnv $ setEnvCtrs (ctrs ++ envCtrs env) env - --- | Lookup an expression variable in the environment. Returns `True` if this variable --- has been skolemised, or `False` otherwise. -lookupVar :: (IsPhase ph, MonadEnv m ph) - => ExprVarName - -- ^ The expression variable to look up. - -> m Bool -lookupVar x = do - skols <- envSkols <$> getEnv - return $ elem (SkolVar x) skols - --- | Lookup a record project in the environment. Returns a boolean denoting --- whether or not the record projection has been skolemised. -lookupRec :: (IsPhase ph, MonadEnv m ph) - => ExprVarName - -- ^ The expression variable on which is being projected. - -> FieldName - -- ^ The field name which is being projected. - -> m Bool -lookupRec x f = do - skols <- envSkols <$> getEnv - case [ fs | SkolRec y fs <- skols, x == y ] of - [] -> return False - (fields:_) -> return (f `elem` fields) - --- | Lookup a value name in the environment. Returns its (partially) evaluated --- definition, together with the updates it performs. -lookupVal :: (IsPhase ph, MonadEnv m ph) - => Qualified ExprValName - -- ^ The value name to lookup. - -> m (Maybe (Expr, UpdateSet ph)) -lookupVal val = do - vals <- envVals <$> getEnv - return $ HM.lookup val vals - --- | Lookup a choice name in the environment. Returns a function which, once --- self, this and args have been instantiated, returns the set of updates it --- performs. Also returns the return type of the choice. -lookupChoice :: (IsPhase ph, MonadEnv m ph) - => Qualified TypeConName - -- ^ The template name in which this choice is defined. - -> ChoiceName - -- ^ The choice name to lookup. - -> m (Maybe (Expr -> Expr -> Expr -> UpdateSet ph, Type)) -lookupChoice tem ch = do - chs <- envChoices <$> getEnv - case HM.lookup (UpdChoice tem ch) chs of - Nothing -> return Nothing - Just ChoiceData{..} -> do - let updFunc (self :: Expr) (this :: Expr) (args :: Expr) = - let subst = foldMap (uncurry exprSubst) [(_cdSelf,self),(_cdThis,this),(_cdArgs,args)] - in map (applySubstInUpd subst) _cdUpds - return $ Just (updFunc, _cdType) - --- | Lookup a data type definition in the environment. -lookupDataCon :: (IsPhase ph, MonadEnv m ph) - => Qualified TypeConName - -- ^ The data constructor to lookup. - -> m DefDataType -lookupDataCon tc = do - dats <- envDats <$> getEnv - case HM.lookup tc dats of - Nothing -> throwError (UnknownDataCons tc) - Just def -> return def - --- | Lookup a contract id in the environment. Returns the variable its fetched --- contract is bound to, along with a list of any previous bindings. -lookupCid :: (IsPhase ph, MonadEnv m ph) - => Expr - -- ^ The contract id to lookup. - -> m (ExprVarName, [ExprVarName]) -lookupCid exp = do - (cid, _) <- expr2cid False exp - cids <- envCids <$> getEnv - case HM.lookup cid cids of - Nothing -> throwError $ UnknownCid cid - Just var -> return var - --- | Lookup the field names and corresponding types, for a given record type --- constructor name, if possible. --- TODO: At the moment, this does not work recursively for nested type --- constructors. This might be a useful extension later on. -recTypConFields :: (IsPhase ph, MonadEnv m ph) - => Qualified TypeConName - -- ^ The record type constructor name to lookup. - -> m (Maybe [(FieldName,Type)]) -recTypConFields tc = lookupDataCon tc >>= \dat -> case dataCons dat of - DataRecord fields -> return $ Just fields - _ -> return Nothing - --- | Lookup the fields for a given record type, if possible. -recTypFields :: (IsPhase ph, MonadEnv m ph) - => Type - -- ^ The type to lookup. - -> m (Maybe [(FieldName,Type)]) -recTypFields (TCon tc) = do - recTypConFields tc -recTypFields (TStruct fs) = return $ Just fs -recTypFields (TApp (TBuiltin BTContractId) t) = recTypFields t -recTypFields _ = return Nothing - --- | Lookup the record fields and corresponding values from a given expression. -recExpFields :: (IsPhase ph, MonadEnv m ph) - => Expr - -- ^ The expression to lookup. - -> m (Maybe [(FieldName, Expr)]) -recExpFields (EVar x) = do - skols <- envSkols <$> getEnv - case [ fs | SkolRec y fs <- skols, x == y ] of - [] -> throwError $ UnboundVar x - (fss:_) -> return $ Just $ zip fss (map (\f -> EStructProj f (EVar x)) fss) -recExpFields (ERecCon _ fs) = return $ Just fs -recExpFields (EStructCon fs) = return $ Just fs -recExpFields (ERecUpd _ f recExp fExp) = do - recExpFields recExp >>= \case - Just fs -> do - unless (isJust $ find (\(n, _) -> n == f) fs) (throwError $ UnknownRecField f) - return $ Just $ (f, fExp) : [(n, e) | (n, e) <- fs, n /= f] - Nothing -> return Nothing -recExpFields (ERecProj _ f e) = do - recExpFields e >>= \case - Just fields -> case lookup f fields of - Just e' -> recExpFields e' - Nothing -> throwError $ UnknownRecField f - Nothing -> return Nothing -recExpFields (EStructProj f (EVar _)) = recExpFields (EVar $ fieldName2VarName f) -recExpFields (EStructProj f e) = do - recExpFields e >>= \case - Just fields -> case lookup f fields of - Just e' -> recExpFields e' - Nothing -> throwError $ UnknownRecField f - Nothing -> return Nothing -recExpFields (ELocation _ e) = recExpFields e -recExpFields _ = return Nothing - -applySubstInBoolExpr :: Subst -> BoolExpr -> BoolExpr -applySubstInBoolExpr subst = \case - BExpr e -> BExpr (applySubstInExpr subst e) - BAnd e1 e2 -> BAnd (applySubstInBoolExpr subst e1) (applySubstInBoolExpr subst e2) - BNot e -> BNot (applySubstInBoolExpr subst e) - BEq e1 e2 -> BEq (applySubstInExpr subst e1) (applySubstInExpr subst e2) - BGt e1 e2 -> BGt (applySubstInExpr subst e1) (applySubstInExpr subst e2) - BGtE e1 e2 -> BGtE (applySubstInExpr subst e1) (applySubstInExpr subst e2) - BLt e1 e2 -> BLt (applySubstInExpr subst e1) (applySubstInExpr subst e2) - BLtE e1 e2 -> BLtE (applySubstInExpr subst e1) (applySubstInExpr subst e2) - -applySubstInCond :: (Subst -> a -> a) -> Subst -> Cond a -> Cond a -applySubstInCond f subst = \case - Determined a -> Determined (f subst a) - Conditional c xs ys -> - Conditional - (applySubstInBoolExpr subst c) - (map (applySubstInCond f subst) xs) - (map (applySubstInCond f subst) ys) - -applySubstInUpd :: IsPhase ph => Subst -> Upd ph -> Upd ph -applySubstInUpd subst = - mapBaseUpd (baseUpd . fmap (map (applySubstInCond applySubstInBaseUpd subst))) - -applySubstInBaseUpd :: Subst -> BaseUpd -> BaseUpd -applySubstInBaseUpd subst UpdCreate{..} = - UpdCreate _creTemp (map (second $ applySubstInExpr subst) _creField) -applySubstInBaseUpd subst UpdArchive{..} = - UpdArchive _arcTemp (map (second $ applySubstInExpr subst) _arcField) - --- | Data type representing an error. -data Error - = UnknownValue (Qualified ExprValName) - | UnknownDataCons (Qualified TypeConName) - | UnknownChoice ChoiceName - | UnboundVar ExprVarName - | UnknownRecField FieldName - | UnknownCid Cid - | UnknownTmpl TypeConName - | ExpectRecord - | ExpectCid - | CyclicModules [ModuleName] - -instance Show Error where - show (UnknownValue qname) = "Impossible: Unknown value definition: " - ++ (show $ unExprValName $ qualObject qname) - show (UnknownDataCons tc) = "Impossible: Unknown data constructor: " ++ show tc - show (UnknownChoice ch) = "Impossible: Unknown choice definition: " ++ show ch - show (UnboundVar name) = "Impossible: Unbound term variable: " ++ show name - show (UnknownRecField f) = "Impossible: Unknown record field: " ++ show f - show (UnknownCid cid) = "Impossible: Unknown contract id: " ++ show cid - show (UnknownTmpl tem) = "Impossible: Unknown template: " ++ show tem - show ExpectRecord = "Impossible: Expected a record type" - show ExpectCid = "Impossible: Expected a contract id" - show (CyclicModules mods) = "Cyclic modules: " ++ show mods diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs deleted file mode 100644 index 6b4b0b2cd13d..000000000000 --- a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Generate.hs +++ /dev/null @@ -1,636 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} - --- | Constraint generator for Daml-LF static verification -module DA.Daml.LF.Verify.Generate - ( genPackages - , genExpr - , Output(..) - , Phase(..) - , GenPhase - ) where - -import Control.Monad.Error.Class (MonadError (..), throwError) -import Control.Monad.Extra (whenJust) -import Data.Maybe (fromMaybe, listToMaybe) -import qualified Data.HashMap.Strict as HM -import qualified Data.NameMap as NM - -import DA.Daml.LF.Ast hiding (lookupChoice) -import DA.Daml.LF.Ast.Subst -import DA.Daml.LF.Verify.Context - --- | Data type denoting the output of the constraint generator. -data Output (ph :: Phase) = Output - { _oExpr :: Expr - -- ^ The expression, evaluated as far as possible. - , _oUpdate :: UpdateSet ph - -- ^ The updates, performed by this expression. - } - --- | Construct an output with no updates. -emptyOut :: IsPhase ph - => Expr - -- ^ The evaluated expression. - -> Output ph -emptyOut expr = Output expr emptyUpdateSet - --- | Extend a generator output with the updates of the second generator output. --- Note that the end result will contain only the first expression. -combineOut :: IsPhase ph => Output ph -> Output ph -> Output ph -combineOut out1 out2 = extendOutUpds (_oUpdate out2) out1 - --- | Update an output with a new evaluated expression. -updateOutExpr :: Expr - -- ^ The new output expression. - -> Output ph - -- ^ The generator output to be updated. - -> Output ph -updateOutExpr expr out = out{_oExpr = expr} - --- | Update an output with additional updates. -extendOutUpds :: IsPhase ph - => UpdateSet ph - -- ^ The extension of the update set. - -> Output ph - -- ^ The generator output to be updated. - -> Output ph -extendOutUpds upds out@Output{..} = out{_oUpdate = concatUpdateSet upds _oUpdate} - --- | Update an output with an additional Archive update. -addArchiveUpd :: Qualified TypeConName - -- ^ The template to be archived. - -> [(FieldName, Expr)] - -- ^ The fields to be archived, with their respective values. - -> Output 'ChoiceGathering - -- ^ The generator output to be updated. - -> Output 'ChoiceGathering -addArchiveUpd temp fs (Output expr upds) = - Output expr (addBaseUpd upds $ UpdArchive temp fs) - --- | Class containing the generator methods for different generator phases. -class IsPhase ph => GenPhase (ph :: Phase) where - -- | Generate an environment for a given module. - -- Depending on the generator phase, this either adds all value and data type - -- definitions to the environment, or all template definitions with their - -- respective choices. - genModule :: MonadEnv m ph - => PackageRef - -- ^ A reference to the package in which this module is defined. - -> Module - -- ^ The module to analyse. - -> m () - - -- | Analyse a value reference. - genForVal :: MonadEnv m ph - => Qualified ExprValName - -- ^ The value reference to be analysed. - -> m (Output ph) - -instance GenPhase 'ValueGathering where - genModule pac mod = do - let modName = moduleName mod - extDatsEnv (HM.fromList [(Qualified pac modName (dataTypeCon def), def) | def <- NM.toList (moduleDataTypes mod)]) - mapM_ (genValue pac modName) (NM.toList $ moduleValues mod) - genForVal w = return $ Output (EVal w) (extendUpdateSet (valueUpd $ Determined w) emptyUpdateSet) - -instance GenPhase 'ChoiceGathering where - genModule pac mod = - mapM_ (genTemplate pac (moduleName mod)) (NM.toList $ moduleTemplates mod) - genForVal w = lookupVal w >>= \case - Just (expr, upds) -> return (Output expr upds) - Nothing -> throwError (UnknownValue w) - -instance GenPhase 'Solving where - genModule _pac _mod = - error "Impossible: genModule can't be used in the solving phase" - genForVal _w = error "Impossible: genForVal can't be used in the solving phase" - --- | Generate an environment for a given list of packages. --- Depending on the generator phase, this either adds all value and data type --- definitions to the environment, or all template definitions with their --- respective choices. -genPackages :: (GenPhase ph, MonadEnv m ph) - => [(PackageId, (Package, Maybe PackageName))] - -- ^ The list of packages, as produced by `readPackages`. - -> m () -genPackages inp = mapM_ genPackage inp - --- | Generate an environment for a given package. --- Depending on the generator phase, this either adds all value and data type --- definitions to the environment, or all template definitions with their --- respective choices. -genPackage :: (GenPhase ph, MonadEnv m ph) - => (PackageId, (Package, Maybe PackageName)) - -- ^ The package, as produced by `readPackages`. - -> m () -genPackage (id, (pac, _)) = mapM_ (genModule (PRImport id)) (NM.toList $ packageModules pac) - --- | Analyse a value definition and add to the environment. -genValue :: MonadEnv m 'ValueGathering - => PackageRef - -- ^ A reference to the package in which this value is defined. - -> ModuleName - -- ^ The name of the module in which this value is defined. - -> DefValue - -- ^ The value to be analysed and added. - -> m () -genValue pac mod val = do - expOut <- genExpr True (dvalBody val) - let qname = Qualified pac mod (fst $ dvalBinder val) - extValEnv qname (_oExpr expOut) (_oUpdate expOut) - --- | Analyse a choice definition and add to the environment. -genChoice :: MonadEnv m 'ChoiceGathering - => Qualified TypeConName - -- ^ The template in which this choice is defined. - -> ExprVarName - -- ^ The `this` variable referencing the contract on which this choice is - -- called. - -> [(FieldName, Type)] - -- ^ The list of fields available in the template. - -> TemplateChoice - -- ^ The choice to be analysed and added. - -> m () -genChoice tem this' temFs TemplateChoice{..} = do - -- Get the current variable names. - let self' = chcSelfBinder - arg' = fst chcArgBinder - -- Refresh the variable names and extend the environment. - self <- genRenamedVar self' - arg <- genRenamedVar arg' - this <- genRenamedVar this' - extVarEnv self - extVarEnv arg - extVarEnv this - -- Extend the environment with any record fields from the arguments. - argFs <- recTypFields (snd chcArgBinder) >>= \case - Nothing -> throwError ExpectRecord - Just fs -> return fs - extRecEnv arg $ map fst argFs - extRecEnvTCons argFs - -- Extend the environment with any record fields from the template. - extRecEnv this $ map fst temFs - extRecEnvTCons temFs - -- Extend the environment with any contract id's and constraints from the arguments. - extEnvContractTCons argFs arg Nothing - -- Extend the environment with any contract id's and constraints from the template. - extEnvContract (TCon tem) (EVar self) (Just this) - extEnvContractTCons temFs this (Just this) - -- Substitute the renamed variables, and the `Self` package id. - -- Run the constraint generator on the resulting choice expression. - let substVar = foldMap (uncurry exprSubst) [(self',EVar self),(this',EVar this),(arg',EVar arg)] - expOut <- genExpr True - $ applySubstInExpr substVar chcUpdate - -- Add the archive update. - let out = if chcConsuming - then addArchiveUpd tem (fields this) expOut - else expOut - -- Extend the environment with the choice and its resulting updates. - extChEnv tem chcName self this arg (_oUpdate out) chcReturnType - where - fields this = map (\(f,_) -> (f, ERecProj (TypeConApp tem []) f (EVar this))) temFs - --- | Analyse a template definition and add all choices to the environment. -genTemplate :: MonadEnv m 'ChoiceGathering - => PackageRef - -- ^ A reference to the package in which this template is defined. - -> ModuleName - -- ^ The module in which this template is defined. - -> Template - -- ^ The template to be analysed and added. - -> m () -genTemplate pac mod Template{..} = do - let name = Qualified pac mod tplTypeCon - fields <- recTypConFields name >>= \case - Nothing -> throwError ExpectRecord - Just fs -> return fs - let preCond (this :: Expr) = - applySubstInExpr - (exprSubst tplParam this) - tplPrecondition - extPrecond name preCond - mapM_ (genChoice name tplParam fields) - (archive : NM.toList tplChoices) - where - archive :: TemplateChoice - archive = TemplateChoice Nothing (ChoiceName "Archive") True - (ENil (TBuiltin BTParty)) Nothing (ExprVarName "self") - (ExprVarName "arg", TStruct []) (TBuiltin BTUnit) - (EUpdate $ UPure (TBuiltin BTUnit) (EBuiltin BEUnit)) - --- | Analyse an expression, and produce an Output storing its (partial) --- evaluation result and the set of performed updates. -genExpr :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> Expr - -- ^ The expression to be analysed. - -> m (Output ph) -genExpr updFlag = \case - ETmApp fun arg -> genForTmApp updFlag fun arg - ETyApp expr typ -> genForTyApp updFlag expr typ - ELet bind body -> genForLet updFlag bind body - EVar name -> genForVar name - EVal w -> genForVal w - ERecProj tc f e -> genForRecProj updFlag tc f e - EStructProj f e -> genForStructProj updFlag f e - ELocation _ expr -> genExpr updFlag expr - ECase e cs -> genForCase updFlag e cs - EUpdate upd -> if updFlag - then do - (out, _, _) <- genUpdate upd - return out - else return $ emptyOut $ EUpdate upd - -- TODO: This can be extended with missing cases later on. - e -> return $ emptyOut e - --- | Analyse an update expression, and produce both an Output, its return type --- and potentially the field values of any created contracts. -genUpdate :: (GenPhase ph, MonadEnv m ph) - => Update - -- ^ The update expression to be analysed. - -> m (Output ph, Maybe Type, Maybe Expr) -genUpdate = \case - UBind bind expr -> genForBind bind expr - UPure typ expr -> do - out <- genExpr True expr - let out' = updateOutExpr (EUpdate $ UPure typ (_oExpr out)) out - return (out', Just typ, Nothing) - UCreate tem arg -> genForCreate tem arg - UExercise tem ch cid arg -> genForExercise tem ch cid arg - UGetTime -> return (emptyOut (EUpdate UGetTime), Just $ TBuiltin BTTimestamp, Nothing) - -- TODO: This can be extended with missing cases later on. - u -> error ("Update not implemented yet: " ++ show u) - --- | Analyse a term application expression. -genForTmApp :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> Expr - -- ^ The function expression. - -> Expr - -- ^ The argument expression. - -> m (Output ph) -genForTmApp updFlag fun arg = do - funOut <- genExpr updFlag fun - arout <- genExpr updFlag arg - case _oExpr funOut of - ETmLam bndr body -> do - let subst = exprSubst (fst bndr) (_oExpr arout) - resExpr = applySubstInExpr subst body - resOut <- genExpr updFlag resExpr - return $ combineOut resOut - $ combineOut funOut arout - fun' -> return $ updateOutExpr (ETmApp fun' (_oExpr arout)) - $ combineOut funOut arout - --- | Analyse a type application expression. -genForTyApp :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> Expr - -- ^ The function expression. - -> Type - -- ^ The argument type. - -> m (Output ph) -genForTyApp updFlag expr typ = do - exprOut <- genExpr updFlag expr - case _oExpr exprOut of - ETyLam bndr body -> do - let subst = typeSubst (fst bndr) typ - resExpr = applySubstInExpr subst body - resOut <- genExpr updFlag resExpr - return $ combineOut resOut exprOut - expr' -> return $ updateOutExpr (ETyApp expr' typ) exprOut - --- | Analyse a let binding expression. -genForLet :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> Binding - -- ^ The binding to be bound. - -> Expr - -- ^ The expression in which the binding should be available. - -> m (Output ph) -genForLet updFlag bind body = do - bindOut <- genExpr False (bindingBound bind) - let var = fst $ bindingBinder bind - subst = exprSubst var (_oExpr bindOut) - resExpr = applySubstInExpr subst body - resOut <- genExpr updFlag resExpr - return $ combineOut resOut bindOut - --- | Analyse an expression variable. -genForVar :: (GenPhase ph, MonadEnv m ph) - => ExprVarName - -- ^ The expression variable to be analysed. - -> m (Output ph) -genForVar name = lookupVar name >> return (emptyOut (EVar name)) - --- | Analyse a record projection expression. -genForRecProj :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> TypeConApp - -- ^ The type constructor of the record which is projected. - -> FieldName - -- ^ The field which is projected. - -> Expr - -- ^ The record expression which is projected. - -> m (Output ph) -genForRecProj updFlag tc f body = do - bodyOut <- genExpr updFlag body - case _oExpr bodyOut of - EVar x -> do - skol <- lookupRec x f - if skol - then return $ updateOutExpr (ERecProj tc f (EVar x)) bodyOut - else error ("Impossible: expected skolem record: " ++ show x ++ "." ++ show f) - expr -> do - recExpFields expr >>= \case - Just fs -> case lookup f fs of - Just expr -> do - exprOut <- genExpr updFlag expr - return $ combineOut exprOut bodyOut - Nothing -> throwError $ UnknownRecField f - Nothing -> return $ updateOutExpr (ERecProj tc f expr) bodyOut - --- | Analyse a struct projection expression. -genForStructProj :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> FieldName - -- ^ The field which is projected. - -> Expr - -- ^ The record expression which is projected. - -> m (Output ph) -genForStructProj updFlag f body = do - bodyOut <- genExpr updFlag body - case _oExpr bodyOut of - EVar x -> do - skol <- lookupRec x f - if skol - then return $ updateOutExpr (EStructProj f (EVar x)) bodyOut - else error ("Impossible: expected skolem record: " ++ show x ++ "." ++ show f) - expr -> do - recExpFields expr >>= \case - Just fs -> case lookup f fs of - Just expr -> do - exprOut <- genExpr updFlag expr - return $ combineOut exprOut bodyOut - Nothing -> throwError $ UnknownRecField f - Nothing -> return $ updateOutExpr (EStructProj f expr) bodyOut - --- | Analyse a case expression. --- TODO: This should be extended with general pattern matching, instead of only --- supporting boolean cases. -genForCase :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether to analyse update expressions. - -> Expr - -- ^ The expression to match on. - -> [CaseAlternative] - -- ^ The list of alternatives. - -> m (Output ph) -genForCase updFlag exp cs = do - expOut <- genExpr updFlag exp - case findBool True of - Just tru -> do - truOut <- genExpr updFlag tru - case findBool False of - Just fal -> do - falOut <- genExpr updFlag fal - let resExp = ECase (_oExpr expOut) - [ CaseAlternative (CPBool True) (_oExpr truOut) - , CaseAlternative (CPBool False) (_oExpr falOut) ] - resUpd = _oUpdate expOut `concatUpdateSet` - conditionalUpdateSet (_oExpr expOut) (_oUpdate truOut) (_oUpdate falOut) - return $ Output resExp resUpd - Nothing -> error "Impossible: Missing False-case in if statement" - Nothing -> return $ emptyOut (ECase exp cs) - where - findBool :: Bool -> Maybe Expr - findBool b1 = listToMaybe $ [e | CaseAlternative (CPBool b2) e <- cs, b1 == b2] - --- | Analyse a create update expression. --- Returns both the generator output and the return type. -genForCreate :: (GenPhase ph, MonadEnv m ph) - => Qualified TypeConName - -- ^ The template of which a new instance is being created. - -> Expr - -- ^ The argument expression. - -> m (Output ph, Maybe Type, Maybe Expr) -genForCreate tem arg = do - arout <- genExpr True arg - recExpFields (_oExpr arout) >>= \case - Just fs -> do - fsEval <- mapM partial_eval_field fs - return ( Output (EUpdate (UCreate tem $ _oExpr arout)) $ addBaseUpd emptyUpdateSet (UpdCreate tem fsEval) - , Just $ TCon tem - , Just $ EStructCon fsEval ) - Nothing -> throwError ExpectRecord - where - partial_eval_field :: (GenPhase ph, MonadEnv m ph) - => (FieldName, Expr) - -> m (FieldName, Expr) - partial_eval_field (f,e) = do - e' <- genExpr False e - return (f,_oExpr e') - --- | Analyse an exercise update expression. --- Returns both the generator output and the return type of the choice. -genForExercise :: (GenPhase ph, MonadEnv m ph) - => Qualified TypeConName - -- ^ The template on which a choice is being exercised. - -> ChoiceName - -- ^ The choice which is being exercised. - -> Expr - -- ^ The party which exercises the choice. - -> Expr - -- ^ The arguments with which the choice is being exercised. - -> m (Output ph, Maybe Type, Maybe Expr) -genForExercise tem ch cid arg = do - cidOut <- genExpr True cid - arout <- genExpr True arg - lookupChoice tem ch >>= \case - Just (updSubst, resType) -> do - this <- fst <$> lookupCid (_oExpr cidOut) - let updSet_refs = updSubst (_oExpr cidOut) (EVar this) (_oExpr arout) - updSet = if containsChoiceRefs updSet_refs - then addChoice emptyUpdateSet tem ch - else updSet_refs - return ( Output (EUpdate (UExercise tem ch (_oExpr cidOut) (_oExpr arout))) updSet - , Just resType - , Nothing ) - Nothing -> do - let updSet = addChoice emptyUpdateSet tem ch - return ( Output (EUpdate (UExercise tem ch (_oExpr cidOut) (_oExpr arout))) updSet - , Nothing - , Nothing ) - --- | Analyse a bind update expression. --- Returns both the generator output and the return type. -genForBind :: (GenPhase ph, MonadEnv m ph) - => Binding - -- ^ The binding being bound with this update. - -> Expr - -- ^ The expression in which this binding is being made available. - -> m (Output ph, Maybe Type, Maybe Expr) -genForBind bind body = do - bindOut <- genExpr False (bindingBound bind) - (bindUpd, subst) <- case _oExpr bindOut of - EUpdate (UFetch tc cid) -> do - let var0 = fst $ bindingBinder bind - var1 <- genRenamedVar var0 - let subst = exprSubst var0 (EVar var1) - _ <- bindCids False (Just $ TContractId (TCon tc)) cid (EVar var1) Nothing - return (emptyUpdateSet, subst) - EUpdate upd -> do - (updOut, updTyp, creFs) <- genUpdate upd - this <- genRenamedVar (ExprVarName "this") - subst <- bindCids True updTyp (EVar $ fst $ bindingBinder bind) (EVar this) creFs - return (_oUpdate updOut, subst) - _ -> return (emptyUpdateSet, mempty) - extVarEnv (fst $ bindingBinder bind) - bodyOut <- genExpr False $ applySubstInExpr subst body - let bodyUpd = case _oExpr bodyOut of - EUpdate bodyUpd -> bodyUpd - -- Note: This is a bit of a hack, as we're forced to provide some type to - -- UPure, but the type itself doesn't really matter. - -- The only reason where these types are used is in `bindCids`, where - -- they are used to bind fetched / created contract cids, neither of - -- which could originate from a UPure update. - expr -> UPure (TBuiltin BTUnit) expr - (bodyUpdOut, bodyTyp, creFs) <- genUpdate bodyUpd - return ( Output - (_oExpr bodyUpdOut) - (_oUpdate bindOut - `concatUpdateSet` bindUpd - `concatUpdateSet` _oUpdate bodyOut - `concatUpdateSet` _oUpdate bodyUpdOut) - , bodyTyp - , creFs ) - --- | Refresh and bind the fetched contract id to the given variable. Returns a --- substitution, mapping the old id to the refreshed one. -bindCids :: (GenPhase ph, MonadEnv m ph) - => Bool - -- ^ Flag denoting whether the contract id's should be refreshed. - -- Note that even with the flag on, contract id's are only refreshed on their - -- first encounter. - -> Maybe Type - -- ^ The type of the contract id's being bound. - -> Expr - -- ^ The contract id's being bound. - -> Expr - -- ^ The variables to bind them to. - -> Maybe Expr - -- ^ The field values for any created contracts, if available. - -> m Subst -bindCids _ Nothing _ _ _ = return mempty -bindCids b (Just (TContractId (TCon tc))) cid (EVar this) fsExpM = do - fs <- recTypConFields tc >>= \case - Nothing -> throwError ExpectRecord - Just fs -> return fs - extRecEnv this (map fst fs) - subst <- extCidEnv b cid this - case fsExpM of - Just fsExp -> do - fsOut <- genExpr False $ applySubstInExpr subst fsExp - recExpFields (_oExpr fsOut) >>= \case - Just fields -> do - fields' <- mapM (\(f,e) -> genExpr False e >>= \out -> return (f,_oExpr out)) fields - extCtrRec this fields' - return subst - Nothing -> throwError ExpectRecord - Nothing -> return subst -bindCids b (Just (TCon tc)) cid (EVar this) fsExpM = do - fs <- recTypConFields tc >>= \case - Nothing -> throwError ExpectRecord - Just fs -> return fs - extRecEnv this (map fst fs) - subst <- extCidEnv b cid this - case fsExpM of - Just fsExp -> do - fsOut <- genExpr False $ applySubstInExpr subst fsExp - recExpFields (_oExpr fsOut) >>= \case - Just fields -> do - fields' <- mapM (\(f,e) -> genExpr False e >>= \out -> return (f,_oExpr out)) fields - extCtrRec this fields' - return subst - Nothing -> throwError ExpectRecord - Nothing -> return subst -bindCids b (Just (TApp (TApp (TCon con) t1) t2)) cid var fsExpM = - case head $ unTypeConName $ qualObject con of - "Tuple2" -> do - subst1 <- bindCids b (Just t1) (EStructProj (FieldName "_1") cid) var fsExpM - subst2 <- bindCids b (Just t2) (applySubstInExpr subst1 $ EStructProj (FieldName "_2") cid) var fsExpM - return (subst1 <> subst2) - con' -> error ("Binding contract id's for this constructor has not been implemented yet: " ++ show con') -bindCids _ (Just (TBuiltin BTUnit)) _ _ _ = return mempty -bindCids _ (Just (TBuiltin BTTimestamp)) _ _ _ = return mempty --- TODO: This can be extended with additional cases later on. -bindCids _ (Just typ) _ _ _ = - error ("Binding contract id's for this particular type has not been implemented yet: " ++ show typ) - --- Note: It would be much nicer to have these functions in Context.hs, but they --- require the `GenPhase` monad. --- | Lookup the preconditions for a given type, and instantiate the `this` --- variable. -lookupPreconds :: (GenPhase ph, MonadEnv m ph) - => Type - -- ^ The type to lookup. - -> ExprVarName - -- ^ The variable for `this` to instantiate with. - -> m (Maybe Expr) -lookupPreconds typ this = case typ of - (TCon tem) -> do - preconds <- envPreconds <$> getEnv - case HM.lookup tem preconds of - Nothing -> return Nothing - Just preFunc -> do - preOut <- genExpr False (preFunc $ EVar this) - return $ Just $ _oExpr preOut - _ -> return Nothing - --- | Bind the given contract id, and add any required additional constraints to --- the environment. -extEnvContract :: (GenPhase ph, MonadEnv m ph) - => Type - -- ^ The contract id type to add to the environment. - -> Expr - -- ^ The contract id being bound. - -> Maybe ExprVarName - -- ^ The variable to bind the contract id to, if available. - -> m () -extEnvContract (TContractId typ) cid bindM = extEnvContract typ cid bindM -extEnvContract (TCon tem) cid bindM = do - bindV <- genRenamedVar (ExprVarName "var") - let bind = fromMaybe bindV bindM - _ <- bindCids False (Just $ TCon tem) cid (EVar bind) Nothing - mbPreCond <- lookupPreconds (TCon tem) bind - whenJust mbPreCond $ \precond -> do - precondOut <- genExpr False precond - extCtr (_oExpr precondOut) -extEnvContract _ _ _ = return () - --- | Bind any contract id's, together with their constraints, for the fields of --- any given record or type constructor type. -extEnvContractTCons :: (GenPhase ph, MonadEnv m ph) - => [(FieldName, Type)] - -- ^ The record fields to bind, together with their types. - -> ExprVarName - -- ^ The variable name to project from, e.g. the `args` in `args.field`. - -> Maybe ExprVarName - -- ^ The variable to bind the contract id's to, if available. - -> m () -extEnvContractTCons fields var bind = mapM_ step fields - where - step :: (GenPhase ph, MonadEnv m ph) - => (FieldName, Type) -> m () - step (f,typ) = extEnvContract typ (EStructProj f (EVar var)) bind diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs deleted file mode 100644 index e20173a1d302..000000000000 --- a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Read.hs +++ /dev/null @@ -1,103 +0,0 @@ - --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - --- TODO: There is a lot of copying going on here from TsCodeGenMain.hs. --- A nicer alternative would be to just change the exports from this module. - --- | Reading dar files for Daml-LF verification. -module DA.Daml.LF.Verify.Read - ( readPackages - , optionsParserInfo - , Options(..) - ) where - -import qualified DA.Daml.LF.Proto3.Archive as Archive -import qualified DA.Daml.LF.Reader as DAR -import qualified Data.ByteString as B -import qualified Data.ByteString.Lazy as BSL -import qualified Data.Text.Extended as T -import qualified "zip-archive" Codec.Archive.Zip as Zip -import Control.Monad.Extra -import Options.Applicative - -import DA.Daml.LF.Ast - -data Options = Options - { optInputDar :: FilePath - , optChoice :: (ModuleName, TypeConName, ChoiceName) - , optField :: (ModuleName, TypeConName, FieldName) - } - --- | Reads a module, template and choice from an input String. --- The expected syntax is as follows: --- Module:Template.Choice -choiceReader :: String -> Maybe (ModuleName, TypeConName, ChoiceName) -choiceReader str = - let (modStr, remStr) = break (':' ==) str - in if null modStr || null remStr - then Nothing - else let (tmpStr, choStr) = break ('.' ==) (tail remStr) - in if null tmpStr || null choStr - then Nothing - else Just ( ModuleName [T.pack modStr] - , TypeConName [T.pack tmpStr] - , ChoiceName (T.pack $ tail choStr) ) - --- | Reads a module, template and field from an input String. --- The expected syntax is as follows: --- Module:Template.Field -fieldReader :: String -> Maybe (ModuleName, TypeConName, FieldName) -fieldReader str = - let (modStr, remStr) = break (':' ==) str - in if null modStr || null remStr - then Nothing - else let (tmpStr, fldStr) = break ('.' ==) (tail remStr) - in if null tmpStr || null fldStr - then Nothing - else Just ( ModuleName [T.pack modStr] - , TypeConName [T.pack tmpStr] - , FieldName (T.pack $ tail fldStr) ) - -optionsParser :: Parser Options -optionsParser = Options - <$> argument str - ( metavar "DAR-FILE" - <> help "DAR file to analyse" - ) - -- The choice to analyse: e.g. "--choice Module:Template.Choice" - <*> option (maybeReader choiceReader) - ( long "choice" - <> short 'c' - <> metavar "CHOICE" - <> help "The choice to analyse" - ) - -- The field to verify: e.g. "--field Module:Template.Field" - <*> option (maybeReader fieldReader) - ( long "field" - <> short 'f' - <> metavar "Field" - <> help "The field to verify" - ) - -optionsParserInfo :: ParserInfo Options -optionsParserInfo = info (optionsParser <**> helper) - ( fullDesc - <> progDesc "Perform static analysis on a DAR" - ) - --- Build a list of packages from a list of DAR file paths. -readPackages :: [FilePath] -> IO [(PackageId, (Package, Maybe PackageName))] -readPackages dars = concatMapM darToPackages dars - where - darToPackages :: FilePath -> IO [(PackageId, (Package, Maybe PackageName))] - darToPackages dar = do - dar <- B.readFile dar - let archive = Zip.toArchive $ BSL.fromStrict dar - dalfs <- either fail pure $ DAR.readDalfs archive - DAR.DalfManifest{packageName} <- either fail pure $ DAR.readDalfManifest archive - packageName <- pure (PackageName . T.pack <$> packageName) - forM ((DAR.mainDalf dalfs, packageName) : map (, Nothing) (DAR.dalfs dalfs)) $ - \(dalf, mbPkgName) -> do - (pkgId, pkg) <- either (fail . show) pure $ Archive.decodeArchive Archive.DecodeAsDependency (BSL.toStrict dalf) - pure (pkgId, (pkg, mbPkgName)) diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/ReferenceSolve.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/ReferenceSolve.hs deleted file mode 100644 index a7ee08efad3d..000000000000 --- a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/ReferenceSolve.hs +++ /dev/null @@ -1,302 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeFamilies #-} - --- | Solving references (adding support for recursion) for Daml-LF static verification -module DA.Daml.LF.Verify.ReferenceSolve - ( solveValueReferences - , solveChoiceReferences - ) where - -import Data.Hashable -import Data.Maybe (fromMaybe) -import Data.List (foldl', intercalate) -import qualified Data.HashMap.Strict as HM - -import DA.Daml.LF.Ast hiding (lookupChoice) -import DA.Daml.LF.Ast.Subst -import DA.Daml.LF.Verify.Context - --- | Solves the value references by computing the closure of all referenced --- values, for each value in the environment. --- It thus empties `_usValue` by collecting all updates made by this closure. -solveValueReferences :: Env 'ValueGathering -> Env 'ChoiceGathering -solveValueReferences env = - let val_exp_hmap = HM.map fst $ envVals env - val_ref_hmap = HM.map snd $ envVals env - (_, val_sol_hmap) = foldl' (\hmaps ref -> snd $ solveReference lookup_ref_in lookup_ref_out pop_upds ext_upds make_rec make_mutrec intro_cond empty_upds [] hmaps ref) (val_ref_hmap, HM.empty) (HM.keys $ envVals env) - valhmap = HM.intersectionWith (,) val_exp_hmap val_sol_hmap - in EnvCG (envSkols env) valhmap (envDats env) (envCids env) HM.empty (envCtrs env) HM.empty - where - lookup_ref_in :: Qualified ExprValName - -> HM.HashMap (Qualified ExprValName) (UpdateSet 'ValueGathering) - -> Maybe ( UpdateSet 'ValueGathering - , HM.HashMap (Qualified ExprValName) (UpdateSet 'ValueGathering) ) - lookup_ref_in ref hmap = (, HM.delete ref hmap) <$> HM.lookup ref hmap - - lookup_ref_out :: Qualified ExprValName - -> HM.HashMap (Qualified ExprValName) (UpdateSet 'ChoiceGathering) - -> Maybe (UpdateSet 'ChoiceGathering) - lookup_ref_out ref hmap = HM.lookup ref hmap - - pop_upds :: UpdateSet 'ValueGathering - -> Maybe ( Either (Cond (Qualified ExprValName)) - (UpdateSet 'ChoiceGathering) - , UpdateSet 'ValueGathering ) - pop_upds = \case - [] -> Nothing - (upd:updset1) -> - let upd' = case upd of - UpdVGBase base -> Right [UpdCGBase $ Simple base] - UpdVGChoice cho -> Right [UpdCGChoice cho] - UpdVGVal val -> Left val - in Just (upd', updset1) - - ext_upds :: UpdateSet 'ChoiceGathering -> UpdateSet 'ChoiceGathering - -> UpdateSet 'ChoiceGathering - ext_upds = concatUpdateSet - - make_rec :: UpdateSet 'ChoiceGathering -> UpdateSet 'ChoiceGathering - make_rec upds = (map baseUpd $ makeRec [upd | UpdCGBase upd <- upds]) - ++ [UpdCGChoice cho | UpdCGChoice cho <- upds] - - make_mutrec :: [(Qualified ExprValName, UpdateSet 'ChoiceGathering)] - -> UpdateSet 'ChoiceGathering - make_mutrec inp = - let (strs, upds) = unzip inp - debug = intercalate " - " $ map (show . unExprValName . qualObject) strs - updConcat = foldl' concatUpdateSet emptyUpdateSet upds - in (map baseUpd $ makeMutRec [upd | UpdCGBase upd <- updConcat] debug) - ++ [UpdCGChoice cho | UpdCGChoice cho <- updConcat] - - intro_cond :: Cond (UpdateSet 'ChoiceGathering) - -> UpdateSet 'ChoiceGathering - intro_cond (Determined x) = x - intro_cond (Conditional cond cx cy) = - let xs = map intro_cond cx - ys = map intro_cond cy - updx = foldl' concatUpdateSet emptyUpdateSet xs - updy = foldl' concatUpdateSet emptyUpdateSet ys - in (introCond $ createCond cond updx updy) - - empty_upds :: UpdateSet 'ValueGathering - -> UpdateSet 'ChoiceGathering - empty_upds _ = emptyUpdateSet - --- | Solves the choice references by computing the closure of all referenced --- choices, for each choice in the environment. --- It thus empties `_usChoice` by collecting all updates made by this closure. -solveChoiceReferences :: Env 'ChoiceGathering -> Env 'Solving -solveChoiceReferences env = - let (_, chhmap) = foldl' (\hmaps ref -> snd $ solveReference lookup_ref_in lookup_ref_out pop_upds ext_upds make_rec make_mutrec intro_cond empty_upds [] hmaps ref) (envChoices env, HM.empty) (HM.keys $ envChoices env) - valhmap = HM.map (inlineChoices chhmap) (envVals env) - in EnvS (envSkols env) valhmap (envDats env) (envCids env) (envPreconds env) (envCtrs env) chhmap - where - lookup_ref_in :: UpdChoice - -> HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering) - -> Maybe ( ChoiceData 'ChoiceGathering - , HM.HashMap UpdChoice (ChoiceData 'ChoiceGathering) ) - lookup_ref_in ref hmap = (, HM.delete ref hmap) <$> HM.lookup ref hmap - - lookup_ref_out :: UpdChoice - -> HM.HashMap UpdChoice (ChoiceData 'Solving) - -> Maybe (ChoiceData 'Solving) - lookup_ref_out ref hmap = HM.lookup ref hmap - - pop_upds :: ChoiceData 'ChoiceGathering - -> Maybe ( Either (Cond UpdChoice) (ChoiceData 'Solving) - , ChoiceData 'ChoiceGathering ) - pop_upds chdat@ChoiceData{..} = case _cdUpds of - [] -> Nothing - (upd:upds) -> - let upd' = case upd of - UpdCGBase base -> Right chdat{_cdUpds = [UpdSBase base]} - UpdCGChoice cho -> Left cho - in Just (upd', chdat{_cdUpds = upds}) - - ext_upds :: ChoiceData 'Solving - -> ChoiceData 'Solving - -> ChoiceData 'Solving - ext_upds chdat1 chdat2 = - let varSubst = foldMap (uncurry exprSubst) [(_cdSelf chdat2, EVar (_cdSelf chdat1)), (_cdThis chdat2, EVar (_cdThis chdat1)), (_cdArgs chdat2, EVar (_cdArgs chdat1))] - newUpds = _cdUpds chdat1 `concatUpdateSet` - map (applySubstInUpd varSubst) (_cdUpds chdat2) - in chdat1{_cdUpds = newUpds} - - make_rec :: ChoiceData 'Solving -> ChoiceData 'Solving - make_rec chdat@ChoiceData{..} = - let upds = map baseUpd $ makeRec [upd | UpdSBase upd <- _cdUpds] - in chdat{_cdUpds = upds} - - make_mutrec :: [(UpdChoice, ChoiceData 'Solving)] -> ChoiceData 'Solving - make_mutrec inp = - let (strs, chdats) = unzip inp - debug = intercalate " - " $ map (show . unChoiceName . _choName) strs - chdat = concat_chdats chdats - upds = map baseUpd $ makeMutRec [upd | UpdSBase upd <- _cdUpds chdat] debug - in chdat{_cdUpds = upds} - - -- | Internal function for combining choice data's. Note that the return - -- type is considered to be irrelevant here, and the first one is returned - -- arbitrarily. - -- Also note that the input list is expected to be non-empty. - concat_chdats :: IsPhase ph => [ChoiceData ph] -> ChoiceData ph - concat_chdats inp = - let chdat = head inp - upds = foldl' concatUpdateSet emptyUpdateSet $ map _cdUpds inp - in chdat{_cdUpds = upds} - - intro_cond :: IsPhase ph - => Cond (ChoiceData ph) - -> ChoiceData ph - intro_cond (Determined x) = x - intro_cond (Conditional cond cdatxs cdatys) = - let datxs = map intro_cond cdatxs - datys = map intro_cond cdatys - newUpds = introCond (createCond cond - (foldl' - (\upd dat -> upd `concatUpdateSet` _cdUpds dat) - emptyUpdateSet datxs) - (foldl' - (\upd dat -> upd `concatUpdateSet` _cdUpds dat) - emptyUpdateSet datys)) - in (head datxs){_cdUpds = newUpds} - - empty_upds :: ChoiceData 'ChoiceGathering - -> ChoiceData 'Solving - empty_upds dat = dat{_cdUpds = emptyUpdateSet} - - inlineChoices :: HM.HashMap UpdChoice (ChoiceData 'Solving) - -> (Expr, UpdateSet 'ChoiceGathering) - -> (Expr, UpdateSet 'Solving) - inlineChoices chshmap (exp, upds) = - (exp, concatMap inline_choice upds) - where - inline_choice :: Upd 'ChoiceGathering -> UpdateSet 'Solving - inline_choice (UpdCGBase upd) = [UpdSBase upd] - inline_choice (UpdCGChoice (Determined cho)) = - let chdat = fromMaybe (error "Impossible: missing choice while solving") (HM.lookup cho chshmap) - in _cdUpds chdat - inline_choice (UpdCGChoice (Conditional cond chos_a chos_b)) = - let upds_a = map (Determined . inline_choice . UpdCGChoice) chos_a - upds_b = map (Determined . inline_choice . UpdCGChoice) chos_b - in introCond $ Conditional cond upds_a upds_b - --- | Solves a single reference by recursively inlining the references into updates. -solveReference :: forall ref updset0 updset1. (Eq ref, Hashable ref, Show ref) - => (ref -> HM.HashMap ref updset0 -> Maybe (updset0, HM.HashMap ref updset0)) - -- ^ Function for looking up and popping a reference from the update set. - -> (ref -> HM.HashMap ref updset1 -> Maybe updset1) - -- ^ Function for looking up a reference in the solved update set. - -> (updset0 -> Maybe (Either (Cond ref) updset1 , updset0)) - -- ^ Function for popping an element from an update set. Returns Nothing if the - -- update set is empty. Returns a Left value is the element is a reference, or - -- Right if it's an update. - -> (updset1 -> updset1 -> updset1) - -- ^ Function for concatinating update sets. - -> (updset1 -> updset1) - -- ^ Function for marking an update set as recursive. - -> ([(ref, updset1)] -> updset1) - -- ^ Function for combining and marking a list of update sets as mutually recursive. - -> (Cond updset1 -> updset1) - -- ^ Function for moving conditionals inside the update set. - -> (updset0 -> updset1) - -- ^ Function for emptying a given update set of all updates. - -> [(ref, updset1)] - -- ^ The references which have already been visited. Note that this a list - -- rather than a HashMap, as the ordering is important here. - -> ( HM.HashMap ref updset0 - -- ^ The hashmap mapping references to update sets and references. - -- These still need to be solved. - , HM.HashMap ref updset1 ) - -- ^ The hashmap mapping references to solved update sets (without references). - -- This starts out empty. - -> ref - -- ^ The reference to be solved. - -> (updset1, (HM.HashMap ref updset0, HM.HashMap ref updset1)) -solveReference lookupRef lookupSol popUpd extUpds makeRec makeMutRec introCond emptyUpds vis (hmapRef0, hmapSol0) ref0 = - -- Check for loops. If the references has already been visited, then the - -- reference should be flagged as recursive. - case dropWhile (not . (\(ref,_) -> ref == ref0)) vis of - - -- When no recursion has been detected, continue inlining the references. - -- First, lookup the update set for the given reference, and remove it from - -- the hashmap. - [] -> case lookupRef ref0 hmapRef0 of - -- The reference has already been solved, and can just be returned. - Nothing -> case lookupSol ref0 hmapSol0 of - Nothing -> error "Impossible: Unknown reference during solving " - Just upd0 -> (upd0, (hmapRef0, hmapSol0)) - -- The reference has not yet been solved. - Just (upd0, hmapRef1) -> - -- Resolve the references contained in the update set. - let (upd1, (hmapRef2, hmapSol2)) = handle_upds upd0 (emptyUpds upd0) (hmapRef1, hmapSol0) - in (upd1, (hmapRef2, HM.insert ref0 upd1 hmapSol2)) - - -- When recursion has been detected, halt solving and mark the cycle as - -- recursive. - [(_cho,upd2)] -> let upd3 = makeRec upd2 - in (upd3, (hmapRef0, HM.insert ref0 upd3 hmapSol0)) - - -- When mutual recursion has been detected, halt solving and mark all cycles - -- as mutually recursive. - cycle -> let upd2 = makeMutRec cycle - in (upd2, (hmapRef0, HM.insert ref0 upd2 hmapSol0)) - where - -- | Extend the closure by computing the closure over all references in the - -- given update set. - -- Returns the handled update set (no longer contains references), and the - -- altered hash maps. - handle_upds :: updset0 - -- ^ The update set for the current reference that still needs to be - -- handled. This still contains references to solve. - -> updset1 - -- ^ The update set of the current reference that has already been handled. - -> (HM.HashMap ref updset0, HM.HashMap ref updset1) - -- ^ The maps containing the yet to be solved references and the - -- previously solved references, respectively. - -> (updset1, (HM.HashMap ref updset0, HM.HashMap ref updset1)) - handle_upds updset_ref0 updset_sol0 hmaps0 = case popUpd updset_ref0 of - -- When the update set to handle is empty, return. - Nothing -> (updset_sol0, hmaps0) - -- When the update set is non-empty, handle the first entry. - Just (entry, updset_ref_rem) -> case entry of - -- The update the handle is a reference. - Left ref -> - let vis' = vis ++ [(ref0,updset_sol0)] - (updset_sol1, hmaps1) = handle_ref vis' (updset_sol0, hmaps0) ref - in handle_upds updset_ref_rem updset_sol1 hmaps1 - -- The update to handle is a base update. - Right upds -> handle_upds updset_ref_rem (extUpds updset_sol0 upds) hmaps0 - - -- | Extend the closure by resolving a single given reference. - handle_ref :: [(ref,updset1)] - -- ^ The list of previously visited references. - -> (updset1, (HM.HashMap ref updset0, HM.HashMap ref updset1)) - -- ^ The update set of the current reference that has already been handled, - -- along with the maps containing the yet to be solved references and the - -- previously solved references, respectively. - -> Cond ref - -- ^ The reference to be resolved and added. - -> (updset1, (HM.HashMap ref updset0, HM.HashMap ref updset1)) - handle_ref vis (updset0, hmaps0) = \case - -- For a simple reference, the closure is computed straightforwardly. - Determined ref -> - let (upds_ext, hmaps1) = solveReference lookupRef lookupSol popUpd extUpds makeRec makeMutRec introCond emptyUpds vis hmaps0 ref - in (extUpds updset0 upds_ext, hmaps1) - -- A conditional reference is more involved, as the conditional needs to be - -- preserved in the computed closure (update set). - Conditional cond refs_a refs_b -> - -- Compute the closure for the true-case. - let (updset_a, hmaps_a) = foldl' (handle_ref vis) (updset0,hmaps0) refs_a - -- Compute the closure for the false-case. - (updset_b, hmaps_b) = foldl' (handle_ref vis) (updset0,hmaps_a) refs_b - -- Move the conditional inwards, in the update set. - -- TODO: This has the unfortunate side effect of moving all updates inside the conditional. - updset1 = introCond $ createCond cond updset_a updset_b - in (updset1, hmaps_b) diff --git a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs b/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs deleted file mode 100644 index 613e45ce9e97..000000000000 --- a/compiler/daml-lf-verify/src/DA/Daml/LF/Verify/Solve.hs +++ /dev/null @@ -1,607 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - -{-# LANGUAGE DataKinds #-} - --- | Constraint solver for Daml-LF static verification -module DA.Daml.LF.Verify.Solve - ( constructConstr - , solveConstr - , ConstraintSet(..) - , Result(..) - , showResult - ) where - -import Data.Bifunctor -import Data.Maybe -import Data.List -import Data.List.Extra (nubOrd) -import Data.Tuple.Extra (both) -import Prettyprinter -import Prettyprinter.Render.String -import qualified Data.HashMap.Strict as HM -import qualified Data.Text as T -import qualified SimpleSMT as S - -import DA.Daml.LF.Ast.Base -import DA.Daml.LF.Ast.Numeric -import DA.Daml.LF.Verify.Context - --- | A simple form of expressions featuring basic arithmetic. -data ConstraintExpr - -- | Boolean value. - = CBool !Bool - -- | Integer value. - | CInt !Integer - -- | Real value. - | CReal !Rational - -- | Reference to an expression variable. - | CVar !ExprVarName - -- | Sum of two expressions. - | CAdd !ConstraintExpr !ConstraintExpr - -- | Subtraction of two expressions. - | CSub !ConstraintExpr !ConstraintExpr - -- | Multiplication of two expressions. - | CMul !ConstraintExpr !ConstraintExpr - -- | Division of two expressions. - | CDiv !ConstraintExpr !ConstraintExpr - -- | Negation of an expression. - | CNeg !ConstraintExpr - -- | Modulo operation on expressions. - | CMod !ConstraintExpr !ConstraintExpr - -- | Boolean operator. - | COp !CtrOperator !ConstraintExpr !ConstraintExpr - -- | Boolean and operator. - | CAnd !ConstraintExpr !ConstraintExpr - -- | Boolean not operator. - | CNot !ConstraintExpr - -- | If then else expression. - | CIf !ConstraintExpr !ConstraintExpr !ConstraintExpr - deriving (Eq, Ord, Show) - --- | Binary boolean operator for constraint expressions. -data CtrOperator - -- | Equals operator. - = OpEq - -- | Greater than operator. - | OpGt - -- | Greater than or equal operator. - | OpGtE - -- | Less than operator. - | OpLt - -- | Less than or equal operator. - | OpLtE - deriving (Eq, Ord, Show) - -instance Pretty ConstraintExpr where - pretty (CBool b) = pretty b - pretty (CInt i) = pretty i - pretty (CReal i) = pretty $ show i - pretty (CVar x) = pretty $ unExprVarName x - pretty (CAdd e1 e2) = pretty e1 <+> " + " <+> pretty e2 - pretty (CSub e1 e2) = pretty e1 <+> " - " <+> pretty e2 - pretty (CMul e1 e2) = parens (pretty e1) <+> " * " <+> parens (pretty e2) - pretty (CDiv e1 e2) = parens (pretty e1) <+> " / " <+> parens (pretty e2) - pretty (CNeg e) = " -" <+> parens (pretty e) - pretty (CMod e1 e2) = parens (pretty e1) <+> " % " <+> parens (pretty e2) - pretty (COp op e1 e2) = pretty e1 <+> pretty op <+> pretty e2 - pretty (CAnd e1 e2) = pretty e1 <+> " and " <+> pretty e2 - pretty (CNot e) = "not " <+> pretty e - pretty (CIf e1 e2 e3) = "if " <+> pretty e1 <+> " then " <+> pretty e2 - <+> " else " <+> pretty e3 - -instance Pretty CtrOperator where - pretty OpEq = "=" - pretty OpGt = ">" - pretty OpGtE = ">=" - pretty OpLt = "<" - pretty OpLtE = "<=" - --- | Add a bunch of constraint expressions. -addMany :: [ConstraintExpr] -> ConstraintExpr -addMany [] = CReal 0.0 -addMany [x] = x -addMany (x:xs) = CAdd x (addMany xs) - --- | Class covering the types convertible to constraint expressions. -class ConstrExpr a where - -- | Convert the given data type to a constraint expression. - toCExp :: [(ExprVarName, ExprVarName)] - -- ^ The contract name synonyms, along with their current alias. - -> a - -- ^ The data to convert to a constraint expression. - -> ConstraintExpr - -instance ConstrExpr BoolExpr where - toCExp syns (BExpr e) = toCExp syns e - toCExp syns (BAnd b1 b2) = CAnd (toCExp syns b1) (toCExp syns b2) - toCExp syns (BNot b) = CNot (toCExp syns b) - toCExp syns (BEq b1 b2) = COp OpEq (toCExp syns b1) (toCExp syns b2) - toCExp syns (BGt b1 b2) = COp OpGt (toCExp syns b1) (toCExp syns b2) - toCExp syns (BGtE b1 b2) = COp OpGtE (toCExp syns b1) (toCExp syns b2) - toCExp syns (BLt b1 b2) = COp OpLt (toCExp syns b1) (toCExp syns b2) - toCExp syns (BLtE b1 b2) = COp OpLtE (toCExp syns b1) (toCExp syns b2) - -instance ConstrExpr Expr where - toCExp syns (EVar x) = case lookup x syns of - Just y -> CVar y - Nothing -> CVar x - toCExp syns (ERecProj _ f (EVar x)) = case lookup x syns of - Just y -> CVar $ recProj2Var y f - Nothing -> CVar $ recProj2Var x f - toCExp syns (EStructProj f (EVar x)) = case lookup x syns of - Just y -> CVar $ recProj2Var y f - Nothing -> CVar $ recProj2Var x f - toCExp syns (ETmApp (ETmApp op e1) e2) = - builtin_op op (toCExp syns e1) (toCExp syns e2) - where - builtin_op :: Expr -> ConstraintExpr -> ConstraintExpr -> ConstraintExpr - builtin_op (ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName w))) _) _) = case w of - "+" -> CAdd - "-" -> CSub - _ -> error ("Unsupported builtin value: " ++ T.unpack w) - builtin_op (EVal (Qualified _ _ (ExprValName w))) = case w of - "negate" -> const CNeg - _ -> error ("Unsupported builtin value: " ++ T.unpack w) - builtin_op (ETyApp e _) = builtin_op e - builtin_op (EBuiltin op) = case op of - BEEqual _ -> COp OpEq - BEEqualGeneric -> COp OpEq - BEEqualNumeric -> COp OpEq - BEGreater _ -> COp OpGt - BEGreaterGeneric -> COp OpGt - BEGreaterNumeric -> COp OpGt - BEGreaterEq _ -> COp OpGtE - BEGreaterEqGeneric -> COp OpGtE - BEGreaterEqNumeric -> COp OpGtE - BELess _ -> COp OpLt - BELessGeneric -> COp OpLt - BELessNumeric -> COp OpLt - BELessEq _ -> COp OpLtE - BELessEqGeneric -> COp OpLtE - BELessEqNumeric -> COp OpLtE - BEAddInt64 -> CAdd - BEAddNumeric -> CAdd - BESubInt64 -> CSub - BESubNumeric -> CSub - BEMulInt64 -> CMul - BEMulNumeric -> CMul - BEDivInt64 -> CDiv - BEDivNumeric -> CDiv - BEModInt64 -> CMod - _ -> error ("Unsupported builtin operator: " ++ show op) - builtin_op e = error ("Unsupported builtin expression: " ++ show e) - toCExp syns (ETmApp (ETyApp (EVal (Qualified _ _ (ExprValName w))) _) e) = case w of - "intToNumeric" -> toCExp syns e - "$cnegate1" -> CNeg (toCExp syns e) - _ -> error ("Unsupported builtin value: " ++ T.unpack w) - toCExp syns (ETmApp (ETyApp (ETyApp (EBuiltin BECastNumeric) _) _) e) = toCExp syns e - toCExp syns (ELocation _ e) = toCExp syns e - toCExp _syns (EBuiltin (BEBool b)) = CBool b - toCExp _syns (EBuiltin (BEInt64 i)) = CInt $ toInteger i - toCExp _syns (EBuiltin (BENumeric i)) = CReal $ toRational $ numericDecimal i - toCExp syns (ERecProj _ f (ERecCon _ fields)) = toCExp syns $ fromJust $ lookup f fields - toCExp _syns e = error ("Conversion: " ++ show e) - -instance ConstrExpr a => ConstrExpr (Cond a) where - toCExp syns (Determined x) = toCExp syns x - -- TODO: Simplifications could be added here later on. - -- e.g. Remove the conditional when both sides are equal. - toCExp syns (Conditional b x y) = CIf (toCExp syns b) - (addMany $ map (toCExp syns) x) - (addMany $ map (toCExp syns) y) - --- | Gather all free variables in a constraint expression. -gatherFreeVars :: ConstraintExpr - -- ^ The constraint expression to traverse. - -> [ExprVarName] -gatherFreeVars (CBool _) = [] -gatherFreeVars (CInt _) = [] -gatherFreeVars (CReal _) = [] -gatherFreeVars (CVar x) = [x] -gatherFreeVars (CAdd e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (CSub e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (CMul e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (CDiv e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (CNeg e) = gatherFreeVars e -gatherFreeVars (CMod e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (COp _ e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (CAnd e1 e2) = gatherFreeVars e1 `union` gatherFreeVars e2 -gatherFreeVars (CNot e) = gatherFreeVars e -gatherFreeVars (CIf e1 e2 e3) = gatherFreeVars e1 `union` - gatherFreeVars e2 `union` gatherFreeVars e3 - --- | Gather the variable names bound within a skolem variable. -skol2var :: Skolem - -- ^ The skolem variable to handle. - -> [ExprVarName] -skol2var (SkolVar x) = [x] -skol2var (SkolRec x fs) = map (recProj2Var x) fs - --- | Squash a record projection into a single variable name. -recProj2Var :: ExprVarName - -- ^ The variable on which is being projected. - -> FieldName - -- ^ The field name which is being projected. - -> ExprVarName -recProj2Var (ExprVarName x) (FieldName f) = ExprVarName (x `T.append` "." `T.append` f) - --- | The set of constraints to be solved. -data ConstraintSet = ConstraintSet - { _cVars :: ![ExprVarName] - -- ^ The variables to be declared. - , _cCres :: ![ConstraintExpr] - -- ^ The field values of all newly created contracts. - , _cArcs :: ![ConstraintExpr] - -- ^ The field values of all archived contracts. - , _cCtrs :: ![ConstraintExpr] - -- ^ Additional boolean constraints. - , _cInfo :: !String - -- ^ Debugging information. - } - deriving Show - --- | Filters a single update to match the given template, and takes out the --- field of interest. The update gets converted into a constraint expression. --- It returns either a create or an archive update. -filterUpd :: Qualified TypeConName - -- ^ The template name to filter against. - -> [(ExprVarName, ExprVarName)] - -- ^ The contract name synonyms, along with their current alias. - -> FieldName - -- ^ The field name to be verified. - -> BaseUpd - -- ^ The update expression to convert and filter. - -> (Maybe ConstraintExpr, Maybe ConstraintExpr) -filterUpd tem syns f UpdCreate{..} = if tem == _creTemp - then (Just (toCExp syns $ fromJust $ lookup f _creField), Nothing) - else (Nothing, Nothing) -filterUpd tem syns f UpdArchive{..} = if tem == _arcTemp - then (Nothing, Just (toCExp syns $ fromJust $ lookup f _arcField)) - else (Nothing, Nothing) - --- | Filters and converts a conditional update into constraint --- expressions, while splitting it into create and archive updates. -filterCondUpd :: Qualified TypeConName - -- ^ The template name to filter against - -> [(ExprVarName, ExprVarName)] - -- ^ The contract name synonyms, along with their current alias. - -> FieldName - -- ^ The field name to be verified. - -> Cond BaseUpd - -- ^ The conditional update expression to convert and filter. - -> ([ConstraintExpr], [ConstraintExpr]) -filterCondUpd tem syns f (Determined x) = both maybeToList $ filterUpd tem syns f x -filterCondUpd tem syns f (Conditional b xs ys) = - let cb = toCExp syns b - (cxcre,cxarc) = both (addMany . concat) $ unzip $ map (filterCondUpd tem syns f) xs - (cycre,cyarc) = both (addMany . concat) $ unzip $ map (filterCondUpd tem syns f) ys - in ( [CIf cb cxcre cycre] - , [CIf cb cxarc cyarc] ) - --- | Filter the given set of skolems, to only include those that occur in the --- given constraint expressions. Remove duplicates in the process. -filterVars :: [ExprVarName] - -- ^ The list of skolems to filter. - -> [ConstraintExpr] - -- ^ The constraint expressions in which the skolems should occur. - -> [ExprVarName] -filterVars vars cexprs = - let freevars = foldl' (\fv e -> fv `union` gatherFreeVars e) [] cexprs - in freevars `intersect` vars - --- | Construct a list of all contract name synonyms, along with their current --- alias. -constructSynonyms :: [(ExprVarName, [ExprVarName])] - -- ^ The current contract names, along with any previous synonyms. - -> [(ExprVarName, ExprVarName)] -constructSynonyms = foldl' step [] - where - step :: [(ExprVarName, ExprVarName)] -> (ExprVarName, [ExprVarName]) - -> [(ExprVarName, ExprVarName)] - step acc (cur, prevs) = acc ++ map (, cur) prevs - --- | Constructs a constraint set from the generator environment, together with --- the template name, the choice and field to be verified. -constructConstr :: Env 'Solving - -- ^ The generator environment to convert. - -> Qualified TypeConName - -- ^ The template name of the choice to be verified. - -> ChoiceName - -- ^ The choice name to be verified. - -> Qualified TypeConName - -- ^ The template name of the field to be verified. - -> FieldName - -- ^ The field name to be verified. - -> [ConstraintSet] -constructConstr env chtem ch ftem f = - case HM.lookup (UpdChoice chtem ch) (envChoices env) of - Just ChoiceData{..} -> - let upds = [upd | UpdSBase upd <- _cdUpds] - vars = concatMap skol2var (envSkols env) - syns = constructSynonyms $ HM.elems $ envCids env - ctrs = map (toCExp syns) (envCtrs env) - cycleUpds = computeCycles upds - in map (constructSingleSet vars ctrs syns) cycleUpds - Nothing -> error ("Choice not found " ++ show ch) - where - constructSingleSet :: [ExprVarName] - -- ^ The variables to be declared. - -> [ConstraintExpr] - -- ^ The additional constraints. - -> [(ExprVarName, ExprVarName)] - -- ^ The contract name synonyms, along with their current alias. - -> (String, [Cond BaseUpd]) - -- ^ The updates to analyse. - -> ConstraintSet - constructSingleSet vars ctrs syns (info, upds) = - let (cres, arcs) = foldl' - (\(cs,as) upd -> let (cs',as') = filterCondUpd ftem syns f upd in (cs ++ cs',as ++ as')) - ([],[]) - upds - in ConstraintSet vars cres arcs ctrs info - --- | Convert a constraint expression into an SMT expression from the solving library. -cexp2sexp :: [(ExprVarName,S.SExpr)] - -- ^ The set of variable names, mapped to their corresponding SMT counterparts. - -> ConstraintExpr - -- ^ The constraint expression to convert. - -> IO S.SExpr -cexp2sexp _vars (CBool b) = return $ S.bool b -cexp2sexp _vars (CInt i) = return $ S.int i -cexp2sexp _vars (CReal i) = return $ S.real i -cexp2sexp vars (CVar x) = case lookup x vars of - Just exp -> return exp - Nothing -> error ("Impossible: variable not found " ++ show x) -cexp2sexp vars (CAdd ce1 ce2) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ S.add se1 se2 -cexp2sexp vars (CSub ce1 ce2) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ S.sub se1 se2 -cexp2sexp vars (CMul ce1 ce2) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ S.mul se1 se2 -cexp2sexp vars (CDiv ce1 ce2) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ S.realDiv se1 se2 -cexp2sexp vars (CNeg ce) = do - se <- cexp2sexp vars ce - return $ S.neg se -cexp2sexp vars (CMod ce1 ce2) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ S.mod se1 se2 -cexp2sexp vars (COp cop ce1 ce2) = do - let sop = case cop of - OpEq -> S.eq - OpGt -> S.gt - OpGtE -> S.geq - OpLt -> S.lt - OpLtE -> S.leq - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ sop se1 se2 -cexp2sexp vars (CAnd ce1 ce2) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - return $ S.and se1 se2 -cexp2sexp vars (CNot ce) = do - se <- cexp2sexp vars ce - return $ S.not se -cexp2sexp vars (CIf ce1 ce2 ce3) = do - se1 <- cexp2sexp vars ce1 - se2 <- cexp2sexp vars ce2 - se3 <- cexp2sexp vars ce3 - return $ S.ite se1 se2 se3 - --- | Perform some basic simplifications on constraint expressions. -simplifyCExpr :: ConstraintExpr -> ConstraintExpr -simplifyCExpr (CNot e) = case simplifyCExpr e of - CNot e' -> e' - e' -> CNot e' -simplifyCExpr (CAnd e1 e2) = - let e1' = simplifyCExpr e1 - e2' = simplifyCExpr e2 - in if e1' == e2' then e1' - else if e1' == CNot e2' || CNot e1' == e2' then CBool False - else case e2' of - CAnd e3 e4 -> - if e3 == e1' || e4 == e1' then e2' - else if e3 == CNot e1' || e4 == CNot e1' || CNot e3 == e1' || CNot e4 == e1' - then CBool False - else CAnd e1' e2' - _ -> CAnd e1' e2' -simplifyCExpr (CIf e1 e2 e3) = case simplifyCExpr e1 of - CBool True -> e2 - CBool False -> e3 - e1' -> - let e2' = simplifyCExpr e2 - e3' = simplifyCExpr e3 - in if e2' == e3' - then e2' - else CIf e1' e2' e3' -simplifyCExpr (CAdd e1 e2) = CAdd (simplifyCExpr e1) (simplifyCExpr e2) -simplifyCExpr (CSub e1 e2) = CSub (simplifyCExpr e1) (simplifyCExpr e2) -simplifyCExpr (CMul e1 e2) = CMul (simplifyCExpr e1) (simplifyCExpr e2) -simplifyCExpr (CDiv e1 e2) = CDiv (simplifyCExpr e1) (simplifyCExpr e2) -simplifyCExpr (CNeg e) = CNeg (simplifyCExpr e) -simplifyCExpr (CMod e1 e2) = CMod (simplifyCExpr e1) (simplifyCExpr e2) -simplifyCExpr (COp op e1 e2) = COp op (simplifyCExpr e1) (simplifyCExpr e2) --- TODO: This could be extended with additional cases later on. -simplifyCExpr e = e - --- | Declare a list of variables for the SMT solver. Returns a list of the --- declared variables, together with their corresponding SMT counterparts. -declareVars :: S.Solver - -- ^ The SMT solver. - -> [ExprVarName] - -- ^ The variables to be declared. - -> IO [(ExprVarName,S.SExpr)] -declareVars s xs = zip xs <$> mapM (\x -> S.declare s (var2str x) S.tReal) xs - where - var2str :: ExprVarName -> String - var2str (ExprVarName x) = T.unpack x - --- | Assert the additional equality constraints. Binds and returns any --- additional required variables. -declareCtrs :: S.Solver - -- ^ The SMT solver. - -> [(ExprVarName,S.SExpr)] - -- ^ The set of variable names, mapped to their corresponding SMT counterparts. - -> [ConstraintExpr] - -- ^ The constraints to be declared. - -> IO (String, [(ExprVarName,S.SExpr)]) -declareCtrs sol cvars1 exprs = do - let edges = map toTuple exprs - -- let edges = map (\(l,r) -> (l,r,gatherFreeVars l ++ gatherFreeVars r)) ctrs - components = conn_comp edges - useful_nodes = map fst cvars1 - useful_components = filter - (\comp -> let comp_vars = concatMap (\(_,_,_,vars) -> vars) comp - in not $ null $ intersect comp_vars useful_nodes) - components - useful_equalities = concatMap (map (\(o,l,r,_) -> (o,l,r))) useful_components - required_vars = - nubOrd (concatMap (concatMap (\(_,_,_,vars) -> vars)) useful_components) - \\ useful_nodes - cvars2 <- declareVars sol required_vars - debug <- intercalate "\n" <$> mapM (declare $ cvars1 ++ cvars2) useful_equalities - return (debug, cvars2) - where - -- | Convert the constraint expression into a tuple of a binary operator, a - -- left and right expression, and the enclosed variables. - toTuple :: ConstraintExpr - -- ^ The expression to convert. - -> (CtrOperator, ConstraintExpr, ConstraintExpr, [ExprVarName]) - toTuple e = case e of - (COp op cexpr1 cexpr2) -> (op, cexpr1, cexpr2, gatherFreeVars e) - _ -> error ("Invalid constraint expression: " ++ show e) - - -- | Compute connected components of the equality constraints graph. - -- Two edges are adjacent when at least one of their nodes shares a variable. - conn_comp :: [(CtrOperator,ConstraintExpr,ConstraintExpr,[ExprVarName])] - -- ^ The edges of the graph, annotated with the contained variables. - -> [[(CtrOperator,ConstraintExpr,ConstraintExpr,[ExprVarName])]] - conn_comp [] = [] - conn_comp (edge:edges) = let (comp,rem) = cc_step edges edge - in comp : conn_comp rem - - -- | Compute the strongly connected component containing a given edge from - -- the graph, as well as the remaining edges which do not belong to this - -- component. - cc_step :: [(CtrOperator,ConstraintExpr,ConstraintExpr,[ExprVarName])] - -- ^ The edges of the graph, which do not yet belong to any component. - -> (CtrOperator,ConstraintExpr,ConstraintExpr,[ExprVarName]) - -- ^ The current edge for which the component is being computed. - -> ( [(CtrOperator,ConstraintExpr,ConstraintExpr,[ExprVarName])] - -- ^ The computed connected component. - , [(CtrOperator,ConstraintExpr,ConstraintExpr,[ExprVarName])] ) - -- ^ The remaining edges which do not belong to the connected component. - cc_step [] _ = ([],[]) - cc_step edges0 (o,l,r,vars) = - let (neighbors,edges1) = partition (\(_,_,_,vars') -> not $ null $ intersect vars vars') edges0 - in foldl' (\(conn,edges2) edge -> first (conn ++) $ cc_step edges2 edge) - ((o,l,r,vars):neighbors,edges1) neighbors - - declare :: [(ExprVarName,S.SExpr)] - -> (CtrOperator, ConstraintExpr, ConstraintExpr) - -> IO String - declare vars (op, cexp1, cexp2) = do - sexp1 <- cexp2sexp vars cexp1 - sexp2 <- cexp2sexp vars cexp2 - case op of - OpEq -> do - S.assert sol (sexp1 `S.eq` sexp2) - return ("Assert: " ++ S.ppSExpr sexp1 (" = " ++ S.ppSExpr sexp2 "")) - OpGt -> do - S.assert sol (sexp1 `S.gt` sexp2) - return ("Assert: " ++ S.ppSExpr sexp1 (" > " ++ S.ppSExpr sexp2 "")) - OpGtE -> do - S.assert sol (sexp1 `S.geq` sexp2) - return ("Assert: " ++ S.ppSExpr sexp1 (" >= " ++ S.ppSExpr sexp2 "")) - OpLt -> do - S.assert sol (sexp1 `S.lt` sexp2) - return ("Assert: " ++ S.ppSExpr sexp1 (" < " ++ S.ppSExpr sexp2 "")) - OpLtE -> do - S.assert sol (sexp1 `S.leq` sexp2) - return ("Assert: " ++ S.ppSExpr sexp1 (" <= " ++ S.ppSExpr sexp2 "")) - --- | Data type denoting the outcome of the solver. -data Result - = Success - -- ^ The total field amount remains preserved. - | Fail [(S.SExpr, S.Value)] - -- ^ The total field amound does not remain the same. A counter example is - -- provided. - | Unknown - -- ^ The result is inconclusive. - deriving Eq - -instance Show Result where - show Success = "Success!" - show (Fail cs) = "Fail. Counter example:" ++ foldl' (flip step) "" cs - where - step :: (S.SExpr, S.Value) -> String -> String - step (var, val) str = ("\n" ++) $ S.ppSExpr var $ (" = " ++) $ S.ppSExpr (S.value val) str - show Unknown = "Inconclusive." - --- | Output a result to a String, including the choice and field names. -showResult :: ChoiceName -> FieldName -> Result -> String -showResult choice field result = case result of - Success -> "Success! The choice " ++ choiceStr ++ " preserves the field " - ++ fieldStr ++ "." - (Fail cs) -> "Fail. The choice " ++ choiceStr ++ " does not preserve the field " - ++ fieldStr ++ ". Counter example:" ++ foldl' (flip step) "" cs - Unknown -> "Inconclusive result." - where - choiceStr = T.unpack $ unChoiceName choice - fieldStr = T.unpack $ unFieldName field - step :: (S.SExpr, S.Value) -> String -> String - step (var, val) str = ("\n" ++) $ S.ppSExpr var $ (" = " ++) $ S.ppSExpr (S.value val) str - --- | Solve a give constraint set. Prints 'unsat' when the constraint set is --- valid. It asserts that the set of created and archived contracts are not --- equal. Returns both the debugging information, and the result. -solveConstr :: FilePath - -- ^ The path to the constraint solver. - -> ConstraintSet - -- ^ The constraint set to solve. - -> IO (ChoiceName -> FieldName -> String, Result) -solveConstr spath ConstraintSet{..} = do - log <- S.newLogger 1 - sol <- S.newSolver spath ["-in"] (Just log) - vars1 <- declareVars sol $ filterVars _cVars (_cCres ++ _cArcs) - let ctrs = nubOrd $ map simplifyCExpr _cCtrs - (ctr_debug, vars2) <- declareCtrs sol vars1 ctrs - vars <- if null (vars1 ++ vars2) - then declareVars sol [ExprVarName "var"] - else pure (vars1 ++ vars2) - let cres = renderFilter $ map simplifyCExpr _cCres - arcs = renderFilter $ map simplifyCExpr _cArcs - cre <- foldl' S.add (S.real 0.0) <$> mapM (cexp2sexp vars) cres - arc <- foldl' S.add (S.real 0.0) <$> mapM (cexp2sexp vars) arcs - S.assert sol (S.not (cre `S.eq` arc)) - result <- S.check sol >>= \case - S.Sat -> do - counter <- S.getExprs sol $ map snd vars - return $ Fail counter - S.Unsat -> return Success - S.Unknown -> return Unknown - let debug (ch :: ChoiceName) (f :: FieldName) = - "\n==========\n\n" - ++ _cInfo ++ "\n\n" - ++ (renderString $ layoutCompact ("Create: " <+> pretty cres <+> "\n")) - ++ (renderString $ layoutCompact ("Archive: " <+> pretty arcs <+> "\n")) - ++ ctr_debug - ++ "\n~~~~~~~~~~\n\n" - ++ showResult ch f result - return (debug, result) - --- | Remove some redundant values from the list, to unclutter the render. -renderFilter :: [ConstraintExpr] -> [ConstraintExpr] -renderFilter = filter (\c -> c /= CInt 0 && c /= CReal 0.0) diff --git a/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs b/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs deleted file mode 100644 index 0c0ef23569e0..000000000000 --- a/compiler/daml-lf-verify/tests/DA/Daml/LF/Verify/Tests.hs +++ /dev/null @@ -1,273 +0,0 @@ --- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved. --- SPDX-License-Identifier: Apache-2.0 - -module DA.Daml.LF.Verify.Tests - ( mainTest - ) where - -import System.FilePath -import Test.Tasty -import Test.Tasty.ExpectedFailure -import Test.Tasty.HUnit - -import DA.Daml.LF.Ast.Base -import DA.Daml.LF.Verify -import DA.Daml.LF.Verify.Solve -import DA.Bazel.Runfiles - -mainTest :: IO () -mainTest = defaultMain $ testGroup "DA.Daml.LF.Verify" - [ quickstartTests - , generalTests - , conditionalTests - , recursionTests - , ignoreTest recursionTestUnstable - ] - -quickstartPath :: String -quickstartPath = "compiler/daml-lf-verify/quickstart.dar" -generalPath :: String -generalPath = "compiler/daml-lf-verify/general.dar" -conditionalsPath :: String -conditionalsPath = "compiler/daml-lf-verify/conditionals.dar" -recursionPath :: String -recursionPath = "compiler/daml-lf-verify/recursion.dar" - -quickstartTests :: TestTree -quickstartTests = testGroup "Quickstart" - [ testCase "Iou_Split" $ do - quickstartDar <- locateRunfiles (mainWorkspace quickstartPath) - let mod = ModuleName ["Iou"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "Iou_Split" - field = FieldName "amount" - result <- verify quickstartDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for Iou_Split - amount" - [Success] result - , testCase "Iou_Merge" $ do - quickstartDar <- locateRunfiles (mainWorkspace quickstartPath) - let mod = ModuleName ["Iou"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "Iou_Merge" - field = FieldName "amount" - result <- verify quickstartDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for Iou_Merge - amount" - [Success] result - ] - -generalTests :: TestTree -generalTests = testGroup "General" - [ testCase "Success A" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccA" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccA - content" - [Success] result - , testCase "Success B" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccB" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccB - content" - [Success] result - , testCase "Success C" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccC" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccC - content" - [Success] result - , testCase "Success D" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccD" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccD - content" - [Success] result - , testCase "Success E" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccE" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccE - content" - [Success] result - , testCase "Success F" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccF" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccF - content" - [Success] result - , testCase "Success G" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "SuccG" - field = FieldName "content" - result <- verify genDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccG - content" - [Success] result - , testCase "Fail A" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "FailA" - field = FieldName "content" - verify genDar debug mod tmpl choice mod tmpl field >>= \case - [Success] -> assertFailure "Verification wrongfully passed for FailA - content" - [Unknown] -> assertFailure "Verification inconclusive for FailA - content" - [Fail _] -> return () - _ -> assertFailure "Verification produced an incorrect number of outcomes for FailA - content" - , testCase "Fail B" $ do - genDar <- locateRunfiles (mainWorkspace generalPath) - let mod = ModuleName ["General"] - tmpl = TypeConName ["Gen"] - choice = ChoiceName "FailB" - field = FieldName "content" - verify genDar debug mod tmpl choice mod tmpl field >>= \case - [Success] -> assertFailure "Verification wrongfully passed for FailB - content" - [Unknown] -> assertFailure "Verification inconclusive for FailB - content" - [Fail _] -> return () - _ -> assertFailure "Verification produced an incorrect number of outcomes for FailB - content" - ] - -conditionalTests :: TestTree -conditionalTests = testGroup "Conditionals" - [ testCase "Success A" $ do - condDar <- locateRunfiles (mainWorkspace conditionalsPath) - let mod = ModuleName ["Conditional"] - tmpl = TypeConName ["Cond"] - choice = ChoiceName "SuccA" - field = FieldName "content" - result <- verify condDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccA - content" - [Success] result - , testCase "Success B" $ do - condDar <- locateRunfiles (mainWorkspace conditionalsPath) - let mod = ModuleName ["Conditional"] - tmpl = TypeConName ["Cond"] - choice = ChoiceName "SuccB" - field = FieldName "content" - result <- verify condDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccB - content" - [Success] result - , testCase "Success C" $ do - condDar <- locateRunfiles (mainWorkspace conditionalsPath) - let mod = ModuleName ["Conditional"] - tmpl = TypeConName ["Cond"] - choice = ChoiceName "SuccC" - field = FieldName "content" - result <- verify condDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccC - content" - [Success] result - , testCase "Success D" $ do - condDar <- locateRunfiles (mainWorkspace conditionalsPath) - let mod = ModuleName ["Conditional"] - tmpl = TypeConName ["Cond"] - choice = ChoiceName "SuccD" - field = FieldName "content" - result <- verify condDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for SuccD - content" - [Success] result - , testCase "Fail A" $ do - condDar <- locateRunfiles (mainWorkspace conditionalsPath) - let mod = ModuleName ["Conditional"] - tmpl = TypeConName ["Cond"] - choice = ChoiceName "FailA" - field = FieldName "content" - verify condDar debug mod tmpl choice mod tmpl field >>= \case - [Success] -> assertFailure "Verification wrongfully passed for FailA - content" - [Unknown] -> assertFailure "Verification inconclusive for FailA - content" - [Fail _] -> return () - _ -> assertFailure "Verification produced an incorrect number of outcomes for FailA - content" - , testCase "Fail B" $ do - condDar <- locateRunfiles (mainWorkspace conditionalsPath) - let mod = ModuleName ["Conditional"] - tmpl = TypeConName ["Cond"] - choice = ChoiceName "FailB" - field = FieldName "content" - verify condDar debug mod tmpl choice mod tmpl field >>= \case - [Success] -> assertFailure "Verification wrongfully passed for FailB - content" - [Unknown] -> assertFailure "Verification inconclusive for FailB - content" - [Fail _] -> return () - _ -> assertFailure "Verification produced an incorrect number of outcomes for FailB - content" - ] - -recursionTests :: TestTree -recursionTests = testGroup "Recursion" - [ testCase "Iou_TestRecA" $ do - recDar <- locateRunfiles (mainWorkspace recursionPath) - let mod = ModuleName ["Recursion"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "TestRecA" - field = FieldName "amount" - result <- verify recDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for Iou_TestRecA - amount" - [Success, Success] result - , testCase "Iou_TestRecB" $ do - recDar <- locateRunfiles (mainWorkspace recursionPath) - let mod = ModuleName ["Recursion"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "TestRecB" - field = FieldName "amount" - result <- verify recDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for Iou_TestRecB - amount" - [Success, Success] result - , testCase "Iou_Divide" $ do - recDar <- locateRunfiles (mainWorkspace recursionPath) - let mod = ModuleName ["Recursion"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "Iou_Divide" - field = FieldName "amount" - result <- verify recDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for Iou_Divide - amount" - [Success, Success] result - , testCase "Iou_TestMutA1" $ do - recDar <- locateRunfiles (mainWorkspace recursionPath) - let mod = ModuleName ["Recursion"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "TestMutA1" - field = FieldName "amount" - verify recDar debug mod tmpl choice mod tmpl field >>= \case - [Fail _, Success] -> return () - _ -> assertFailure "Verification failed for Iou_TestMutA1 - amount" - , testCase "Iou_TestMutB1" $ do - recDar <- locateRunfiles (mainWorkspace recursionPath) - let mod = ModuleName ["Recursion"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "TestMutB1" - field = FieldName "amount" - verify recDar debug mod tmpl choice mod tmpl field >>= \case - [Fail _, Fail _] -> return () - _ -> assertFailure "Verification failed for Iou_TestMutB1 - amount" - ] - --- Unstable test case! See issue #6550 -recursionTestUnstable :: TestTree -recursionTestUnstable = testGroup "Recursion Unstable" - [ testCase "Iou_Divide_Mut" $ do - recDar <- locateRunfiles (mainWorkspace recursionPath) - let mod = ModuleName ["Recursion"] - tmpl = TypeConName ["Iou"] - choice = ChoiceName "Iou_Divide_Mut" - field = FieldName "amount" - result <- verify recDar debug mod tmpl choice mod tmpl field - assertEqual "Verification failed for Iou_Divide_Mut - amount" - [Success, Success] result - ] - -debug :: String -> IO () -debug _ = return () diff --git a/nix/bazel.nix b/nix/bazel.nix index 237421a91749..3540a0c8e1ab 100644 --- a/nix/bazel.nix +++ b/nix/bazel.nix @@ -159,8 +159,6 @@ let shared = rec { ; }; - z3 = pkgs.z3; - bazel-cc-toolchain = pkgs.callPackage ./tools/bazel-cc-toolchain {}; }; in shared // (if pkgs.stdenv.isLinux then {