mirror of
https://github.com/digital-asset/daml.git
synced 2024-11-10 10:46:11 +03:00
cda93db944
* Replace many occurrences of DAML with Daml * Update docs logo * A few more CLI occurrences CHANGELOG_BEGIN - Change DAML capitalization and docs logo CHANGELOG_END * Fix some over-eager replacements * A few mor occurrences in md files * Address comments in *.proto files * Change case in comments and strings in .ts files * Revert changes to frozen proto files * Also revert LF 1.11 * Update get-daml.sh * Update windows installer * Include .py files * Include comments in .daml files * More instances in the assistant CLI * some more help texts
255 lines
10 KiB
ReStructuredText
255 lines
10 KiB
ReStructuredText
.. Copyright (c) 2021 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
|
|
|
|
controller owner can
|
|
|
|
-- | Transfer some amount to the receiver, or do nothing if this would make the
|
|
-- remaining amount in the account negative.
|
|
nonconsuming Account_Transfer : (ContractId Account, ContractId Account)
|
|
with
|
|
transferAmount: Decimal
|
|
receiverCid: ContractId Account
|
|
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)
|