Pact Core Concepts Part 3 - Testing and Formal Verification in the Pact REPL

3. Testing and Formal Verification in the Pact REPL

Smart contracts are notoriously difficult to secure. Vulnerabilities in smart contracts have contributed to billions of dollars in total losses across the web3 ecosystem over the past few years. The blockchain environment is a harsh one: smart contracts can be read and executed by anyone and they manage sensitive data like account balances and asset ownership. Mistakes are easy to make and easy to find and exploit. A bad one can produce enormous financial losses and end a project altogether.

The Pact programming language is designed for security. Some design decisions remove (or at least obstruct) potential footguns like re-entrancy attacks and infinite loops. Others give the language extra power not found in other languages, such as being able to formally verify your code, which is much better than unit tests alone. If your smart contract is for a real application and will be handling sensitive data you should also considera security audit. An audit can catch subtle but critical issues in contracts — such as this convoluted but (technically) possible vulnerability in a Pact contract.

Most issues, however, can be caught with a combination of unit tests, typechecking, and formal verification. Unit tests are written in Pact REPL files, while types and formal verification are written into your Pact modules directly and are then executed in the Pact REPL. Pact provides many REPL-only functions that help you write tests, benchmark your code, predict gas consumption, simulate different blockchain states, and more.

Before we begin: this article was written with Pact 4.6. If you are a Nix user then you can get the same version of Pact in your shell from pact-nix with one of the following commands:

1# To temporarily drop directly into the Pact interpreter
2$ nix run github:thomashoneyman/pact-nix#pact-4_6_0
3pact>
4
5# To temporarily get Pact in your shell
6$ nix develop github:thomashoneyman/pact-nix#pact-4_6_0
7$ pact --version
8pact version 4.6
9

Otherwise, see the Pact GitHub repository for installation instructions. Once installed, you can execute a Pact REPL file with the command pact test-file.repl or you can load a file to play around with interactively by entering the REPL and then running (load "test-file.repl").

Unit Testing in the Pact REPL

Pact supplies three basic functions for implementing unit tests in the REPL: expect, expect-that, and expect-failure.

The expect function is a simple equality check that reports an error if the two provided expressions are not equal to one another.

1pact> (expect "1 equals 1" 1 1)
2"Expect: success: 1 equals 1"
3
4pact> (expect "1 does not equal 2" 1 2)
5"FAILURE: 1 does not equal 2: expected 1:integer, received 2:integer"
6
7pact> (expect "different lists" [1] [2])
8"FAILURE: different lists: expected [1]:[<a>], received [2]:[<b>]"
9
10pact> (expect "different objects" { 'a': 1 } { 'a': 2 })
11"FAILURE: different objects: expected {"a": 1}:object:*, received {"a": 2}:object:*"
12

The expect-that function is similar, but it uses a predicate function instead of simple equality to perform its test. Accordingly, expect-that is a little more versatile than expect because you only have to assert a condition, not a specific value. In fact, you can express expect via expect-that by providing equality as the predicate function:

1pact> (expect-that "1 equals 1" (= 1) 1)
2"Expect-that: success: 1 equals 1"
3

The expect-that function makes it easy to express a condition over a range of inputs. Below, we test a function to determine if a list is non-empty over a few inputs:

1pact> (map (expect-that "nonempty" (compose (length) (< 0))) [[] [1] [1 2]])
2["FAILURE: nonempty: did not satisfy (compose (length) (< 0)): []:[<a>]"
3"Expect-that: success: nonempty"
4"Expect-that: success: nonempty"]
5

We got three lines of output here because we ran this interactively. However, if we put the same code into a REPL file...

1; test.repl
2(map (expect-that "nonempty" (compose (length) (< 0))) [[] [1] [1 2]])
3

...and then we execute that REPL file, you'll find that only the errors are printed:

1$ pact pact.repl
2pact.repl:1:5: FAILURE: not empty: did not satisfy (compose (length) (< 0)): []:[<a>]
3Load failed
4

This is a useful bit of output filtering. You'll also see that the process exited with a failure status code (1), whereas if we remove the empty list and run this again we'll see a successful output with a success status code (0):

1$ pact pact.repl
2Load successful
3
4$ echo $?
50
6

The third and final unit testing function provided for use in the Pact REPL is expect-failure. This function takes a single expression and expects it to throw an error — for example, because the function contains a call to enforce that should fail — and fails only if the provided function succeeds. It's useful for when you know some inputs to a function that definitely should not work.

1pact> (expect-failure "Enforce should throw on false" (enforce false "Uh oh"))
2"Expect failure: success: Enforce should throw on false"
3

You can optionally include the error message you expect to see; if the thrown error does not contain that message, then expect-failure will fail. This helps you verify that the error message you expect users to see when they call your contract code incorrect. Below, our provided expression throws as expected, but the error message is wrong.

1pact> (expect-failure "Enforce should say 'Oh no'" "Oh no" (enforce false "Uh oh"))
2"FAILURE: Enforce should say 'Oh no': expected error message to contain 'Oh no', got '(enforce false "Uh oh"): Failure: Tx Failed: Uh oh'"
3

Let's say we're developing a smart contract with a few functions for working with lists. We can put this in a file named lists.pact:

1(module lists GOV
2  (defcap GOV () true)
3
4  (defun empty (xs)
5    "Check if a list is empty."
6    (= (length xs) 0))
7
8  (defun enforce-nonempty (xs)
9    "Enforce that a list is not empty."
10    (enforce (not (empty xs)) "List can't be empty."))
11
12  (defun head (xs)
13    "Get the first item in a list."
14    (enforce-nonempty xs)
15    (at 0 xs))
16
17  (defun safe-head (xs default)
18    "Get the first item in a list, or return the default if it is empty."
19    (if (empty xs) default (head xs)))
20
21  (defun snoc (xs a)
22    "Append a value to the end of a list"
23    (+ xs [a]))
24)
25

Let's write a few unit tests in a REPL file named lists.repl:

1; First we need to load the module code we want to test. It's a good
2; practice to wrap this in (begin-tx) and (commit-tx) so that we don't
3; automatically have governance privileges for the module.
4(begin-tx)
5(load "lists.pact")
6(commit-tx)
7
8; We have to refer to functions qualified by the module name — such as
9; 'lists.empty', 'lists.snoc' — unless we use (use) to bring the full
10; module into scope.
11(use lists)
12
13; Next, we can test that our functions behave as expected. We'll start
14; with some simple 'expect' and 'expect-that' calls. These should all
15; succeed.
16(expect-that "Empty list is empty" (empty) [])
17(expect "List with values is not empty" false (empty [1]))
18(expect "First elem is 1" 1 (head [1]))
19(expect "Safe head falls back to default" 1 (safe-head [] 1))
20(expect "Appends to end of list" [1 2 3] (snoc [1 2] 3))
21
22; Notice that we tested that (empty [1]) was equal to 'false' instead of
23; using (expect-failure). That's because (expect-failure) only fails if
24; the expression throws an error. Returning 'false' is considered fine.
25(expect-failure "Cannot use head on empty list" (safe-head []))
26(expect-failure "Enforce nonempty on empty lists" (enforce-nonempty []))
27

If we then run this file at the command line we should see all tests pass:

1$ pact lists.repl
2Load successful
3

I encourage you to take a moment to write other list functions and tests for them. For example:

Write and test a function last that gets the last item from a list. What happens if the list is empty? Can you write a safe-last that can work on empty lists by returning a default value?
Write and test a function occurrences that counts how many times an item is seen in a list, returning 0 if the item is not in the list.
Write and test a function flatten that takes a list of lists and flattens them into a single list by concatenating them all together.

Testing Transactions, Capabilities, and Signatures

The expect family of functions are wonderful for testing Pact functions based on their inputs and outputs, including those which use enforce internally. However, since Pact is a smart contract language, many Pact functions can only be tested in the context of a specific transaction and its digital signatures. The Pact REPL supplies several functions for simulating transactions.

The env-data function allows you to attach an object to a transaction. This should be used when a contract uses the read family of functions to read a transaction payload. The data object can either contain JSON-encoded values or it can contain Pact code directly.

1pact> (read-integer "my-int")
2<interactive>:0:0: No such key in message: my-int
3 at <interactive>:0:0: (read-integer "my-int")
4
5pact> (env-data { "my-int": 1 })
6"Setting transaction data"
7
8pact> (read-integer "my-int")
91
10

The env-sigs function allows you to attach digital signatures to a transaction. Each signature can be scoped to a specific capability, which means the signature is valid only for that capability and not others. The env-sigs function takes an array of keys and associated capabilities, which represents the transaction being signed with the private key associated with the indicated public key.

1pact> (env-sigs [ { "key": "my-public-key" }, "caps": [] } ])
2

With these two functions in hand we are able to simulate transactions in the REPL and test Pact code that depends on the transaction payload and/or digital signatures. To demonstrate, let's write another tiny module, this time in caps.pact:

1(module caps GOV
2  (defcap GOV () (enforce false "No upgrades."))
3
4  (defcap INTERNAL () true)
5
6  (defcap ALICE () (enforce-keyset "free.alice-keyset"))
7
8  (defcap SHARED () (enforce-keyset "free.shared-keyset"))
9
10  (defun internal-fn ()
11    (require-capability (INTERNAL))
12    "Internal only!")
13
14  (defun public-fn ()
15    (with-capability (INTERNAL)
16      (internal-fn)))
17
18  (defun alice-fn ()
19    (with-capability (ALICE)
20      "Alice signed!"))
21
22  (defun shared-fn ()
23    (with-capability (SHARED)
24      "All parties signed!"))
25)
26

There are a few interesting things going on here.

First, we use the INTERNAL capability as a way to designate functions that should not be callable from outside the module. The only way to acquire a capability is via (with-capability CAP ...) used within the module (or with governance rights), so even though INTERNAL can be trivially granted, no one can acquire it without going through some function in this module. In our case, we'll see that we can't call internal-fn ourselves, but we can call public-fn.

Second, the alice-fn and shared-fn functions attempt to acquire the ALICE and SHARED capabilities, respectively. However, both capabilities use the enforce-keyset function to verify that the digital signatures indicated by a particular keyset are satisfied before the capability can be granted. This is how you can ensure a transaction can only go through if signed by specific keys. We'll refer to permanent keychain references here, but you can also store keysets in databases.

Before we can start writing tests we need to simulate registering the keysets our module relies on on-chain. To do that we need to be in a namespace, so let's pause for a quick bit of setup. Put the below code in a file named caps-setup.repl:

1; First we register the 'free namespace, which already exists on Chainweb
2; but which we must create in the REPL
3(begin-tx)
4(env-data { "admin-keyset": ["admin-pubkey"] })
5(env-sigs [{ "key": "admin-pubkey", "caps": [] }])
6(define-namespace 'free (read-keyset 'admin-keyset) (read-keyset 'admin-keyset))
7(commit-tx)
8
9; Then, we'll register the alice-keyset and shared-keyset. The former requires
10; Alice's signature, and the latter requires both Alice and Bob's signatures.
11(begin-tx)
12(env-data {
13  "alice-keyset": { "keys": ["alice-pubkey"], "pred": "keys-all" },
14  "shared-keyset": { "keys": ["alice-pubkey", "bob-pubkey"], "pred": "keys-all" }
15})
16
17; We can enter our namespace, define the keysets needed for our module, and then
18; load the module.
19(namespace 'free)
20(define-keyset "free.alice-keyset" (read-keyset "alice-keyset"))
21(define-keyset "free.shared-keyset" (read-keyset "shared-keyset"))
22(load "caps.pact")
23
24; Before we commit we should clear out the transaction data and signatures so
25; our tests begin with a clean slate.
26(env-data {})
27(env-sigs [])
28(commit-tx)
29

It's common to have a convenience file like this to set up your REPL session. You can then load it into your actual test file. Let's go ahead and write our test file under the assumption our module has been loaded.

In our tests we would like to verify that our internal-fn cannot be called outside the module, that public-fn can be, and that alice-fn and shared-fn are only callable if signatures exist on the transaction that satisfy their respective keysets.

1(load "caps-setup.repl")
2(use free.caps)
3
4(expect-failure "Cannot call internal function." (internal-fn))
5(expect "Can call via public function." "Internal only!" (public-fn))
6
7(expect-failure
8  "Cannot call Alice-only function without her signature."
9  (alice-fn))
10
11(env-sigs [ { "key": "alice-pubkey", "caps": [ (ALICE) ] } ])
12(expect
13  "Can call Alice-only function if Alice signs."
14  "Alice signed!"
15  (alice-fn))
16
17(expect-failure
18  "Cannot call shared function without both signatures."
19  (shared-fn))
20
21(env-sigs [
22  { "key": "alice-pubkey", "caps": [ (ALICE) ] },
23  { "key": "bob-pubkey", "caps": [ (ALICE) ] }
24])
25(expect-failure
26  "Cannot call multi-sig function with wrong capability."
27  (shared-fn))
28
29(env-sigs [
30  { "key": "alice-pubkey", "caps": [ (SHARED) ] },
31  { "key": "bob-pubkey", "caps": [ (SHARED) ] }
32])
33(expect
34  "Can call multi-sig function with sigs & caps."
35  "All parties signed!"
36  (shared-fn))
37

Static Type Checking & Formal Verification in Pact

Pact provides two ways to machine-check your code: static types and formal verification.

Static type-checking helps you verify that your module never uses a value of one type when another is required (such as providing an integer to the length function, which requires a list). Most (but not all) errors caught by the type checker would throw an exception at runtime, but in the smart contract world you certainly don't want to wait until then!

You can ask Pact to check your types are correct for any module with the typecheck REPL-only function, which takes the name of the module to check as its argument. As a brief example (this will not actually work, since we haven't implemented a my-module.pact):

1pact> (load "my-module.pact")
2Loaded module my-module, ...
3
4pact> (typecheck "my-module")
5"Typecheck my-module: success"
6

We won't spend much time on type checking because it is also included in formal verification. In short, I recommend that you provide type annotations in your code wherever possible so that Pact can help ensure you don't make a mistake.

Formal verification is one of my favorite Pact features. It's a way to mathematically prove that a program works as intended. First you express a property that must be true of some code for all possible states that code can be in. Then, the Pact property checking system tries all possible inputs for that code to find a code path that produces an invalid state. If one can be found then the verifier will tell you the exact function calls and arguments that led to the bug. Pact's system is built on Microsoft's Z3 theorem prover.

You can verify a module as easily as you typechecked it (again, this will not actually work, since we haven't implemented a my-module.pact):

1pact> (load "my-module.pact")
2Loaded module my-module, ...
3
4pact> (verify "my-module")
5"Verification of my-module succeeded"
6

The best way to learn the Pact property checking system is via the quite good docs in the Pact language reference. You should read it! However, if that's a bit too much all at once, we can start with a few minimal examples so you can recognize the system when you see it in Pact contracts in the wild.

To use the Pact property checking system you must have z3 installed and available in your shell. If you don't have z3 already and have been following along with Nix, you can add z3 temporarily to your shell with the following command:

1$ nix-shell -p z3
2

Let's write some properties! We can define properties via the @model metadata form. Within functions we can use property to indicate a property that must hold true if the transaction succeeds. Within schema definitions we can use invariant to indicate a property that must hold true for the fields of the schema. You can see the language reference for a list of usable property and invariant functions.

For the next short exercise, write the following module to the file verifier.pact. It contains a basic transfer function and underlying table. The transfer function specifies some properties that must hold true, and we've used some enforcements to rule out potential bugs, but there's still a bug lurking in this code.

1(module verifier GOV
2  (defcap GOV () (enforce false "No upgrades."))
3
4  (defschema account
5    @model [
6      ; An account should never have a negative balance.
7      (invariant (>= balance 0.0))
8    ]
9
10    balance:decimal
11    auth:guard)
12
13  (deftable accounts:{account})
14
15  (defun transfer (from:string to:string amount:decimal)
16    @model [
17      ; A transfer should never create new money — the table should
18      ; contain the same total balance before and after.
19      (property (= (column-delta accounts 'balance) 0.0))
20
21      ; You cannot send funds unless you satisfy the guard associated
22      ; with that account. Without this, you could send others' money.
23      (property (row-enforced accounts "auth" from))
24    ]
25
26    (enforce (!= from to) "Cannot send to yourself.")
27    (enforce (> amount 0.0) "Cannot send negative funds".)
28    (with-read accounts from { "balance" := from-funds, "auth" := auth }
29      (enforce-guard auth)
30      (with-read accounts to { "balance" := to-funds }
31        ; First we debit funds from the sender
32        (update accounts from { "balance": (- from-funds amount) })
33        ; Then we credit funds to the receiver
34        (update accounts to { "balance": (+ to-funds amount) }))))
35)
36

We can then load this into the Pact REPL and verify it:

1pact> (load "verifier.pact")
2pact> (verify "verifier")
3

Uh oh! z3 is able to locate a violation of our invariant that an account can never have a negative balance. It tells us the violated property was on line 7, and the error occurred within the transfer function. Let's take a look:

1verifier.pact:7:17:OutputFailure: Invalidating model found in verifier.transfer
2  Program trace:
3    entering function verifier.transfer with arguments
4      from = "W"
5      to = "r"
6      amount = 0.2
7

We begin with the arguments z3 provided to our function. Next, z3 walks through our code step-by-step. It steps through both our enforce calls and sees that they pass:

1      satisfied assertion: = from to) "C
2      satisfied assertion:  amount 0.0) "C
3

Next, we have our database reads and enforcement of the auth guard:

1      read { auth: 4, balance: 0.1 } from accounts at key "W" succeeds
2      destructuring object
3        from-funds := 0.1
4        auth := 4
5        satisfied guard from database
6        read { balance: 0.1 } from accounts at key "r" succeeds
7        destructuring object
8          to-funds := 0.1
9

The sender "W" has a balance of 0.1 and the receiver "r" has a balance of 0.1. Next, the database updates happen:

1          update accounts at key "W" with { balance: -0.1 } succeeds
2          update accounts at key "r" with { balance: 0.3 } succeeds
3

Uh oh! There's the bug. The user "W" only has a balance of 0.1 but has sent 0.2, which produces a negative balance. This transaction should fail, but our current code allows it. z3 reaches the end of the transaction without a problem:

1      returning with "Write succeeded"
2

Try fixing the problem by adding another enforce. Once fixed, reload and re-verify your module. You can now be more confident your code is correct!

Measuring Gas Consumption

We've learned the fundamentals of testing the correctness of Pact code in the REPL. But correctness is not the only important consideration for your code. Recall that either you or your users will have to pay, in the form of gas fees, for your smart contract code to be executed. The lower the gas consumption of your contract the cheaper it is to use for you or your users.

Let's start a new REPL session and explore the gas costs of a few common functions.

You can enable gas logging by setting a gas model via env-gasmodel (defaults to a fixed 0 gas per operation) and a gas limit via env-gaslimit (defaults to a limit of 0 gas). It's a common practice to use the "table" gasmodel in which the interpreter provides estimates and either an enormous gas limit (you don't care about the limit), or a limit of 180,000 (the maximum a transaction can consume), or a limit of what you feel is reasonable for your transaction.

1pact> (env-gasmodel "table")
2"Set gas model to table-based cost model"
3
4pact> (env-gaslimit 180000)
5"Set gas limit to 180000"
6

Once you have set a gas model and limit you can use the env-gas function to set or read the amount of gas consumed. For example, it is common to set gas to 0 with (env-gas 0), run a function, and then read how much gas was consumed with (env-gas).

1pact> (env-gas 0)
2"Set gas to 0"
3pact> (+ 1 2)
43
5pact> (env-gas)
61
7

From this short session we can deduce that simple addition costs a single unit of gas. Let's explore a few more functions — from here, I will only include the gas output from the REPL to keep things concise.

How much do various math operations cost?

1pact> (env-gas 0) (- 3 4) (env-gas)
21
3
4pact> (env-gas 0) (* 2 3) (env-gas)
53
6
7pact> (env-gas 0) (/ 2 3) (env-gas)
83
9
10pact> (env-gas 0) (^ 2 3) (env-gas)
114
12
13pact> (env-gas 0) (shift 1 3) (env-gas)
141
15

We can see that basic arithmetic is extremely cheap. Addition and subtraction costs a single unit of gas; multiplication and division cost 3; exponentiation costs 4. Bit-shifting costs 1 unit. These numbers grow

How about a more complicated function like fold?

1pact> (env-gas 0) (fold (+) 0 []) (env-gas)
23
3
4pact> (env-gas 0) (fold (+) 0 [1]) (env-gas)
54
6
7pact> (env-gas 0) (fold (+) 0 [1 2]) (env-gas)
85
9

Folding a list incurs 3 gas for the basic operation and then the cost of your accumulation function for each item in the list. How much gas do you think each example above would cost if we had multiplied instead of adding items together? Try it in the REPL!

It is critical to measure the gas consumption of your smart contract functions. Some calls can surprise you — for example, reading the keys of a totally empty table still costs a ton of gas. Paste this module into the REPL:

1(module test GOV
2  (defcap GOV () true)
3
4  (defschema row-type age:decimal)
5
6  (deftable table:{row-type})
7)
8(create-table table)
9

Then, check the gas consumption of reading the table's keys:

1pact> (env-gas 0) (keys table) (env-gas)
240000
3

The keys function always costs 40,000 units of gas. This massive gas consumption is a penalty used to discourage the use of functions like keys in transactional code. After all, tables can end up recording massive amounts of data, in which case reading all rows requires a ton of computation.

Instead, you are meant to use keys and functions like it only in local requests, which don't cost any gas and aren't broadcast to the network. This isn't always obvious when you're reading the language documentation or others' code, so I recommend that you always check the gas consumption of your smart contract functions before deploying them.

Wrapping Up

You've made it to the end of the Pact Core Concepts series! You're now well-equipped to read Pact code you find in the wild and write some of your own. Still, it will take time for the concepts to become familiar.

I encourage you to begin writing your own small smart contracts. As you do, you can use the projects in Real World Pact as examples of real-world code ranging from beginner to advanced. The Real World Pact repository also demonstrates how to deploy your contracts to Chainweb, interact with contracts that exist on-chain, and write a frontend for your smart contract backend.

Author: