We have just published the first release of the Act specification language!

Act is a formal specification language, designed to allow for the construction of an exhaustive, mathematically rigorous description of a smart contract system. Act allows diverse toolchains to interoperate on a single specification, with each generating and exchanging different kinds of knowledge. It has a built-in analysis engine that can automatically prove properties about the specification itself, as well as an integrated symbolic execution engine (based on hevm) that can prove equivalence between a specification and a given bytecode object. Finally, specifications can be exported into the Coq proof assistant, allowing for the verification of properties of almost arbitrary complexity, all with a proof chain right down to the bytecode level.

While a lot of work still remains to be done before Act can be used to verify properties of realistic contracts, we’re excited to share what we have, and invite feedback and ideas from the community. If you want to come chat about Act, we have a matrix channel, or you can also find us in #formal-methods in the ethereum r&d discord.

Contents

Motivation & Design Philosophy

Smart contract development is difficult. The code we write must secure large sums of money in an extremely adversarial environment, and even a single oversight can easily result in the loss of millions of dollars. In this context being able to define and prove the correctness of key security properties is enormously valuable. Act grew out of the verification work carried out for multi-collateral Dai and Uniswap v2, and is a ground-up rewrite in Haskell of the prototype specification language developed as a part of that process, incorporating many of the lessons learned along the way.

The following are some key design goals:

Ease of Refinement

Proving properties directly against EVM bytecode is difficult and expensive. Compiler output contains much extraneous detail (e.g. overflow checks, bitmasks in storage access routines, abi encoding / decoding, function selector dispatch logic) that is not generally relevant when proving the correctness of a high level property, but that must still be taken into account. A widely used and powerful technique is to use a process of refinement, where the properties of interest are proven against a high level specification that abstracts much of this detail away. A separate proof can then be carried out to show that a given bytecode object faithfully implements the abstract specification. The SeL4 microkernel is a notable real world application of this technique, where properties are proven against a high level spec in the Isabelle proof assistant, and then successive refinement steps are used to prove these properties down to the binary level ([1][2])

Act is a framework designed to allow for easy refinement. We want to make it as easy as possible for development teams to define a high level specification, which can then either be used “upwards” to prove higher level properties or “downwards” to demonstrate that an implementation in EVM bytecode conforms to the spec.

Modularity

Different tools and techniques for formal verification have different strengths and weaknesses, and with Act we want to make it as easy as possible to combine tools and share knowledge between them. For example an SMT based analysis engine will usually be significantly faster and more convenient than manually constructing a proof in a proof assistant like Coq, but the latter can prove the correctness of statements that would be impossible to even state in the language accepted by an SMT solver.

With Act as an intermediate language, we can combine and share knowledge between many different tools and frameworks in a way that allows us to leverage their different strengths where it makes most sense.

Expressiveness

Much of the work that we have released to date has been focused on making it easy for smart contract developers to prove statements in the language that they are most familiar with (e.g. the SMTChecker built directly into solc, or the integration of symbolic execution into the ds-test unit test framework). While this makes it easy to get fast results, and allows developers to quickly build confidence in their implementation, there are limits to the kind of properties that can be expressed in such a framework. For example, some properties may require a greater numeric range than the 256 bit integers available in the EVM allow, while others may require temporal operators or quantifiers, neither of which are expressible in a language like Solidity.

With Act we hope to provide a language expressive enough to natively express a wide range of properties, and combined with its ability to export the specification into the Coq proof assistant, we believe that it should be possible to express almost any property of a given specification.

Installation

Act can currently be installed via nix with the following commands:

# configure nix to use prebuilt binaries for hevm (optional)
nix-shell -p cachix --command "cachix add dapp"

# install act v0.1
nix-env -iA act -if https://api.github.com/repos/ethereum/act/tarball/v0.1

If you want to play around with the examples in this post, you can check out the act-examples repo. A call to nix-shell from the repository root will drop you into an environment with all required tools installed and configured.

Language

At a very high level Act is a kind of mathy english over the EVM, where contracts are defined as a set of pure functions taking a given EVM state (i.e. storage & blockchain context) and some calldata and producing a new EVM state ((EVM, Calldata) -> EVM).

A specification of a contract written in Act consists of a constructor and a set of behaviours:

  • The constructor specification defines the structure of the contract’s state, the initial value of the state, and a list of invariants that the contract should satisfy.

  • Each behaviour specification determines how a contract method updates the state, the method’s return value (if any), and any conditions that must be satisfied in order for the state update to be applied.

Alternatively, they can be thought of as an initial state and a set of state transitions, determining an inductively defined state transition system.

A more detailed high level language reference can be found in the documentation.

Types

The types of Act consist of three basic primitives: Integers, Booleans and Bytestrings. Integers are unbounded, with true integer operations. However, as our integer expressions will often represent words in the EVM, we allow ourselves a slight abuse of notation and denote by uintN/intN integers together with the constraint that the value fits into a uintN/intN. If any operation could over- or underflow this bound, the constraint will be unfulfilled and the specification will fail to prove.

Using conventional ABI types for typing also allows us to specify function signatures in a concise way. As an example, consider this specification of a trivial contract that adds two numbers and stores the result on chain:



constructor of Add



interface constructor()







creates







  uint result := 0





behaviour add of Add



interface add(uint x, uint y)







iff in range uint







   x + y







storage







  result => x + y







returns x + y

Expressed in English and math, this specification would read:

The contract Add has a single state variable, named result, which is an integer such that 0 <= result < 2^256.

Given any pair of integers x and y, s.t. 0 <= x < 2^256 and 0 <= y < 2^256, an ABI encoded call to the contract Add with the signature add(uint256,uint256), with its respective arguments named x and y, will:

  • store x + y in result and return x + y if 0 <= x + y < 2^256
  • revert otherwise

Bytecode Level Proof

Act leverages the symbolic execution engine in hevm to provide a backend that can prove equivalence between a contract specification and an implementation of that specification in EVM.

Two claims are generated for each behaviour, Pass and Fail. The Pass claim states that if all preconditions in the iff block are true, then all executions will succeed, storage will be updated according to the storage block, and the specified return value will, in fact, be returned. The Fail claim states that should any of the preconditions be false, all executions will revert.

In both cases we begin the proof by constraining calldata to be of the form specified in the behaviours’ interface blocks, as well as making the relevant assumptions depending on whether the claim is Pass or Fail, and then symbolically executing the bytecode object with storage held to be completely abstract.

This produces a tree of potential executions where each node represents a potential branching point, and each leaf represents a possible final state of the contract after the execution of a single call.

In the case of a Fail claim, we can then check that each leaf represents a state in which execution has reverted, while for a Pass claim we can check that storage has been updated as expected, and that the contents of the return buffer matches what was specified in the behaviour’s returns block.

As an example, consider the following contract:

contract Simple {
    uint val;

    function set(uint x) external payable returns (uint) {
        require(x > 100);
        val = x;
        return x;
    }
}

We can represent this in Act as:



constructor of Simple



interface constructor()







creates







  uint val := 0





behaviour set of Simple



interface set(uint x)







iff







  x > 100







storage







  val => x







returns x

Act needs to have access to the storage layout metadata output by solc to compute the index in storage for each variable mentioned in the spec, so we need to pass a solc output json when trying to prove equivalence. In the examples repo you can run dapp build and then act hevm --spec src/simple.act --soljson out/dapp.sol.json to attempt to prove equivalence of the spec and the runtime bytecode:

< act hevm --spec src/simple.act --soljson out/dapp.sol.json
checking postcondition...
Q.E.D.
Successfully proved set(Pass), 2 cases.
checking postcondition...
Q.E.D.
Successfully proved set(Fail), 2 cases.
==== SUCCESS ====
All behaviours implemented as specified ∎.

If we try to prove equivalence of the spec and a faulty implementation like the one below:

contract Simple {
    uint val;

    function set(uint x) external payable returns (uint) {
        require(x > 100);
        if (x == 2000) {
          val = x + 1;
        } else {
          val = x;
        }
        return x;
    }
}

Then Act will give us a counterexample showing a case where the implementation differs from the specification:

< act hevm --spec src/simple.act --soljson out/dapp.sol.json
checking postcondition...
Calldata:
0x60fe47b100000000000000000000000000000000000000000000000000000000000007d0
Caller:
0x0000000000000000000000000000000000000000
Callvalue:
0
Failed to prove set(Pass)
checking postcondition...
Q.E.D.
Successfully proved set(Fail), 2 cases.
==== FAILURE ====
1 out of 2 claims unproven:

1	Failed to prove set(Pass)

Automated Analysis

Act has an integrated analysis engine that is currently able to automatically prove two kinds of properties:

  • Behaviour level postconditions (i.e. properties that are always true in every possible poststate of a single behaviour)
  • Contract level invariants (i.e. properties that are true in all possible poststates of the constructor, as well as in all possible pre- and poststates of any behaviours)

Postcondition syntax

Postconditions are defined in an optional ensures block of each behaviour. All references to storage in an ensures block must specify whether they talk about the variable’s value in the pre- or the poststate, by using pre(x) or post(x).

An example:



behaviour f of F



interface f(uint z)







storage







  y => z



  x => 30 * z







ensures







  post(x) == 30 * post(y)

Invariant syntax

Invariants are defined in the invariants block in the constructor specification. Each invariant is a predicate that should hold between the execution of any state transitions. Invariant predicates have access to the constructor’s calldata. Note that since invariant predicates are defined over a single abstract contract state (as opposed to predicates in ensures blocks which have access to a pair of states), it is neither necessary nor allowed to disambiguate storage references using pre(x) and post(x) in invariant predicates.

An example:



constructor of C



interface constructor(uint _x, uint _y, uint _z)







iff _x * _y == _z







creates







  uint x := _x



  uint y := _y







invariants







  x * y == _z

Implementation

In order to discharge these proofs, we construct an SMT-based encoding of each behaviour in the spec, and then dispatch queries based on this encoding to an SMT solver (currently z3 and cvc4 are supported). An SMT solver is a system that takes a collection of constraints (a query), where each constraint is a statement in first order logic, and determines whether there exists an assignment of values to the abstract variables in the query such that all constraints are satisfied.

As an example, we could encode the query “for all integers x and y, is there an assignment of values to x and y such that x + y == 13 and y - 7 == x” in the widely supported smt-lib language as follows:

(declare-const x Int)
(declare-const y Int)

(assert (= (+ x y) 13))
(assert (= (- y 7) x))

(check-sat)
(get-model)

When passed to an smt solver (e.g. z3), this would return:

sat
(
  (define-fun x () Int
    3)
  (define-fun y () Int
    10)
)

Where sat means that a satisfying assignment does exist, and the remaining output gives us the values of the assignment found by the solver (x == 3 and y == 10).

SMT-based program verification is often done by contradiction: instead of asking the solver to directly provide a proof for a given statement, we instead ask it to find an example where the statement is untrue, and if none are found, we can infer the truth of the original statement. As an example, if we wished to prove distributivity for integer arithmetic, we would encode the query as follows:

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

(assert (not
  (= (* x (+ y z))
     (+ (* x y) (* x z)))))

(check-sat)

and when run in a solver, we would get unsat as a result, meaning that there are no possible assignments to the variables, x, y and z where distributivity does not hold.

Postcondition Encoding

For the postcondition claims, we tell the solver to assume the truth of all preconditions, and that all storage updates have occurred as defined in the storage block, and then ask it to find an assignment for the symbolic variables in the spec (calldata, environment, and storage) that violates the postcondition. If none can be found, we have a proof that the postcondition always holds.

Invariant Encoding

Invariant claims are proved inductively. For the base case, we ask the solver to once again assume preconditions and storage rewrites, and then to find an assignment for the variables in the constructor that would result in a violation of the invariant predicate over the poststate. If none can be found, we have a proof of the base case.

For the inductive step, we construct a query for each behaviour that assumes preconditions and storage rewrites, and additionally assumes that the invariant claim is true over the prestate. We then ask the solver to find an assignment for the variables in the behaviour that would result in a violation of the invariant predicate over the storage post state. If none can be found, we have an inductive proof that the invariant must hold over all possible contract states.

Proving The Constant Product Invariant

As a larger and practical example, let’s consider the following specification of a highly simplified Uniswap-style constant product automatic market maker. For the purposes of this example we focus only on the core logic, and ignore e.g. interactions with the underlying tokens.

The Amm has two state variables representing its underlying token balances, reserve0 and reserve1. These are initialized to 1000 units each upon creation.

We define a single invariant, that the product of the two reserves should never decrease. This is an important safety property – if it is violated, an attacker is able to execute a sequence of trades that can drain all funds from the exchange.



behaviour init of Amm



interface constructor()







creates







    uint256 reserve0 := 1000



    uint256 reserve1 := 1000







invariants







    1000 * 1000 <= reserve0 * reserve1

Next, we define the two swap methods, that allow a user to exchange tokens. These methods take an amount (amt) of input reserves, and the Amm will adjust the size of the other reserve according to the x * y == k constant product formula.



behaviour swap0 of Amm



interface swap0(uint256 amt)







iff in range uint256







    reserve0 + amt







storage







    reserve0 => reserve0 + amt



    reserve1 => (reserve0 * reserve1) / (reserve0 + amt)





behaviour swap1 of Amm



interface swap1(uint256 amt)







iff in range uint256







    reserve1 + amt







storage







    reserve0 => (reserve0 * reserve1) / (reserve1 + amt)



    reserve1 => reserve1 + amt

If we run act prove against the above spec, we find that there is in fact an error:

> act prove --file src/amm-broken.act

Invariants:


  ((1000 * 1000) <= (Amm.reserve0 * Amm.reserve1)) of Amm violated:

    counterexample:

      calldata:

        swap0(amt = 1)

      storage:

        prestate:

          Amm.reserve0 = 2
          Amm.reserve1 = 500000

        poststate:

          Amm.reserve0 = 3
          Amm.reserve1 = 333333

    counterexample:

      calldata:

        swap1(amt = 1)

      storage:

        prestate:

          Amm.reserve1 = 2
          Amm.reserve0 = 500000

        poststate:

          Amm.reserve1 = 3
          Amm.reserve0 = 333333

If the Amm is in the state reserve0 == 2 and reserve1 == 500,000, and swap0 is called with amt == 1, the final state of the Amm will be reserve0 == 3 and reserve1 == 333,333. The same is true with swap1 if the amounts for reserve0 and reserve1 are switched. In these cases 3 * 333,333 is 999,999, meaning that the product of the reserves has decreased slightly due to imprecision introduced by the EVM’s flooring division.

A safe specification for the swap methods is as follows. Notice the extra + 1 added to the output reserve in both cases. With this implementation, the rounding error is now in favor of the pool instead of the trader, and the contract is now safe against this particular attack.



behaviour swap0 of Amm



interface swap0(uint256 amt)







iff in range uint256







    reserve0 + amt







storage







    reserve0 => reserve0 + amt



    reserve1 => (reserve0 * reserve1) / (reserve0 + amt) + 1





behaviour swap1 of Amm



interface swap1(uint256 amt)







iff in range uint256







    reserve1 + amt







storage







    reserve0 => (reserve0 * reserve1) / (reserve1 + amt) + 1



    reserve1 => reserve1 + amt

If we again run act prove against the fixed specification, we see that the invariant holds for all possible executions of the contract:

> act prove --file src/amm-fixed.act

Invariants:


  ((1000 * 1000) <= (Amm.reserve0 * Amm.reserve1)) of Amm holds ∎

Underpowered Invariants

Due to the inductive nature of the proof, there are some true invariants that the SMT backend is unable to prove. For example, consider the following state machine:



constructor of C



interface constructor()







creates







  uint x := 0







invariants







  x < 9





behaviour f of C



interface f()







case x == 0:







  storage







    x => 1







behaviour g of C



interface g()







case x == 1:







  storage







    x => 2





behaviour h of C



interface h()







case x == 7:







  storage







    x => 100

The contract C can never be in a state where x == 7 and so the write of 100 to x in j() can never occur, however if we run act prove against this specification, this exact case (x == 7) is found as a counterexample:

> act prove --file src/underpowered.act

Invariants:


  (C.x < 9) of C violated:

    counterexample:

      calldata:

        h()

      storage:

        prestate:

          C.x = 7

        poststate:

          C.x = 100

This is due to the inductive nature of the proof: Act checks that the invariant holds after running the constructor, and then for each method assumes that the invariant holds over the pre state and checks that the invariant holds over the post state.

In the case above, the invariant states that x < 9, and if this is assumed as a precondition, then the x == 7 branch in h() is still reachable.

We can fix this by strengthening the invariant to make the x == 7 branch unreachable. Specifically, the weakest invariant that does hold over the full transition system (while remaining on the same form as the original) is x < 7. The strongest is x < 3.

Coq Export

While the automated proof backend is quite capable, there are still many properties that are too challenging for automated tools. For this reason Act allows exporting the transition system to the Coq proof assistant, where manual proofs of arbitrary complexity can be carried out.

A proof assistant provides tools that help to construct proofs. Coq, in particular, is highly interactive. The user typically builds proofs step by step, with the software giving feedback as the proof progresses.

The requirements on proofs in a system like Coq, Isabelle, or Lean are quite strict. These tools only accept proofs that are algorithmically verifiable to be valid series of applications of the system’s inference rules. This is generally stricter than what is typically expected of pen and paper proofs, which often omit tedious details in the interest of clarity and concision.

The verification of these proofs is performed in a minimal and well-audited kernel. Although occasionally bugs have been found in Coq’s and other systems’ kernels, a proof in these systems is generally quite strong evidence of correctness.

A Brief Introduction to Proof in Coq

Coq is a complex system with a steep learning curve, and while a full tutorial on programming in Coq is out of the scope of this blog post, we can give a little taste of how things work. For a more thorough introduction, the books Software Foundations and Certified Programming With Dependent Types are both excellent. Software Foundations in particular is a great introduction for users with little experience in the fields of formal logic and proof theory.

The Coq system is composed of three languages: a minimal functional programming language (Gallina), a tactics language for proof construction (Ltac), and a “vernacular” for interaction with the kernel. Let’s start with the very basics: defining the natural numbers and proving something about addition.

We start by defining the type of natural numbers. There are infinitely many natural numbers, so of course they must be defined inductively. In fact, all type definitions are done with the Inductive vernacular command, even if they are not in fact inductive. Coq’s Inductive is analogous to Haskell’s data and OCaml’s type (with the added power of dependent types).

We define two constructors: O, representing 0, and S, which when applied to the natural number n produces the representation of the number n + 1 (S as in “successor”). To give a concrete example, 3 would be represented in this encoding as S (S (S 0))) i.e 1 + (1 + (1 + 0)).

Inductive nat : Type :=
  | O
  | S (n : nat).

This is an example of a unary number representation. It can often be helpful to represent numbers this way, since the inductive nature of the definition lends itself to inductive proof techniques.

Let’s continue by defining addition over our nat type:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O ⇒ m
  | S n' ⇒ S (plus n' m)
  end.

Here we define a recursive function (a Fixpoint) that takes two numbers n and m and returns the sum of these two numbers. The implementation is defined recursively with pattern matching. You might think of this definition as “unwrapping” each application of S from the first argument until we reach its O. Then we start wrapping the second argument in the same number of Ss.

Now we’re ready to prove something! Let’s prove that 0 + n == n:

Theorem plus_O_n :
  forall n : nat, plus O n = n.
Proof.
  intros n. simpl. reflexivity.
Qed.

We first define our theorem and give it a name (plus_O_n). Then we define the proof goal, in the form of a dependent type. We claim that for all n, where n is an instance of our nat type, 0 + n is equal to n. Finally, we construct a proof, in the form of a series of tactics. Tactics may implement either backwards inference (transforming the goal) or forwards inference (transforming evidence).

The best way to understand the system is to run the software yourself, and play around with the various tactics. In this case the goal is simple enough; once we’ve specified that the proof will be on n, Coq is able to simplify plus O n into n, leaving us the goal n = n. This turns out to be true by the definition of equality, and we invoke definitional equality by reflexivity.

More complicated proofs do not typically require proving basic facts about arithmetic, because Coq ships a substantial standard library of useful definitions and theorems. The above example hopefully serves to illustrate the formal nature of proof in these systems. In many cases it can be surprisingly hard to convince the kernel of the correctness of a statement that seems “obviously” true.

Act Export

Let’s take a look at using Coq to prove properties about a specification that is too difficult for the SMT backend. The following defines a contract that implements exponentiation via repeated multiplication. The contract is initialized with a base (b) and an exponent (e). exp() can then be repeatedly called until e is 1, and the result can then be read from the storage variable r. While obviously artificial, this example does highlight a key shortcoming of the SMT based analysis: exponentiation with a symbolic exponent is simply inexpressible in the smt-lib language used by all major SMT solvers, and so any contract making use of exponentiation where the exponent is a variable of some kind (e.g. calldata, storage) will be impossible to verify using SMT. Coq has no such restrictions, and we can export the spec below and prove correctness there.



constructor of Exponent



interface constructor(uint _b, uint _e)







iff







    _e > 0







creates







    uint b := _b



    uint e := _e



    uint r := _b





behaviour exp of Exponent



interface exp()







iff







    e > 1







iff in range uint







    r * b



    e - 1







storage







    r => r * b



    e => e - 1



    b

You can export the spec into Coq by running make Exponent.v in the src/exponent directory of the examples repo. This will create a file called Exponent.v which contains a model of the above Act specification in Coq:

(* --- GENERATED BY ACT --- *)

Require Import Coq.ZArith.ZArith.
Require Import ActLib.ActLib.
Require Coq.Strings.String.

Module Str := Coq.Strings.String.
Open Scope Z_scope.

Record State : Set := state
{ b : Z
; e : Z
; r : Z
}.

Definition exp0 (STATE : State)  :=
state (b STATE) (((e STATE) - 1)) (((r STATE) * (b STATE))).

Definition Exponent0 (_b : Z) (_e : Z) :=
state (_b) (_e) (_b).

Inductive reachable  : State -> State -> Prop :=
| Exponent0_base : forall (_b : Z) (_e : Z),
     (_e > 0)
  -> ((0 <= _b) /\ (_b <= (UINT_MAX 256)))
  -> ((0 <= _e) /\ (_e <= (UINT_MAX 256)))
  -> reachable (Exponent0 _b _e) (Exponent0 _b _e)

| exp0_step : forall (BASE STATE : State),
     reachable BASE STATE
  -> ((e STATE) > 1)
  -> ((0 <= ((r STATE) * (b STATE))) /\ (((r STATE) * (b STATE)) <= (UINT_MAX 256)))
  -> ((0 <= ((e STATE) - 1)) /\ (((e STATE) - 1) <= (UINT_MAX 256)))
  -> ((0 <= (r STATE)) /\ ((r STATE) <= (UINT_MAX 256)))
  -> ((0 <= (e STATE)) /\ ((e STATE) <= (UINT_MAX 256)))
  -> ((0 <= (b STATE)) /\ ((b STATE) <= (UINT_MAX 256)))
  -> reachable BASE (exp0 STATE )
.

Let’s break this down a bit. We have a definition of contract storage State, which consists of three variables b, e and r, all of type Z. Z is an integer type using a binary encoding from the ZArith library bundled with Coq.

Next we have exp0, which defines how the state is updated by the exp behaviour, and Exponent0 which defines how the state variables are initialized by the constructor arguments.

Finally we have an Inductive Proposition reachable that defines the conditions under which a certain state is reachable from another. There are two parts to this definition:

  • Exponent0_base: states that given two integers _b and _e, the initial state is reachable from the initial state if _e and _b are in the range of a uint256 and _e is greater than 0.
  • exp0_step: states that for a pair of states BASE and STATE, exp0 STATE (i.e. the result of calling exp() against an arbitrary contract state) is reachable from BASE if STATE is reachable from BASE, all the state variables in STATE (e, b, r) are within the range of a uint256, the result of the calculations r * b and e - 1 are within the range of a uint256, and e is greater than 1.

This gives us a pair of inference rules that we can use to prove facts about the set of reachable states defined by the specification for the Exponent contract.

An example of such a proof is contained in the Theory.v file in the src/exponent directory of the examples repo. The core fact that we wish to prove is that when e is 1, r is equal to b ^ e. This can be expressed in Coq as:

forall (base, s : State),
  reachable base s -> e s = 1 -> r s = (b base) ^ (e base).

Expressed more verbosely: for all states base and s, if s is reachable from base, and the value of e in s is 1, then the result variable r in s is equal to b from base raised to the power of e from base.

The full proof is reproduced below. While an explanation of each step is out of scope for this post (and is anyway best made with the proof loaded into an interactive instance of the Coq prover like proof general or CoqIde), we can give a broad strokes overview.

We must first define a helper fact pow_pred which simply states that given two integers a and e, if e is greater than 0 then a * a ^ (e - 1) is equal to a ^ e. This fact is needed in the later steps of the proof. The next step is to define a loop invariant for exp() (i.e. a fact that is true before and after each loop iteration). This is the Lemma invariant, which states that for every state s reachable from base, r * b ^ (e - 1) over s is equal to b ^ e over base. Intuitively, this states that the partial result calculated so far (r), multiplied by the remaining portion of the input calculation b ^ (e - 1) is equal to the final expected result. Finally, given these two intermediate facts, we can discharge a proof for the correctness of Exponent as defined above.

Require Import Exponent.Exponent.
Require Import ActLib.ActLib.
Require Import Coq.ZArith.ZArith.
Open Scope Z_scope.

Lemma pow_pred : forall a e, 0 < e -> a * a ^ (Z.pred e) = a ^ e.
Proof.
  intros.
  apply eq_sym.
  replace (a ^ e) with (a ^ (Z.succ (Z.pred e))).
  - apply Z.pow_succ_r.
    apply Zlt_0_le_0_pred.
    assumption.
  - rewrite (Z.succ_pred e).
    reflexivity.
Qed.

Lemma invariant : forall base s,
  reachable base s -> (r s) * (b s) ^ ((e s) - 1) = (b base) ^ (e base).
Proof.
  intros base s H. induction H.
  - simpl.
    rewrite Z.sub_1_r.
    apply pow_pred.
    apply Z.gt_lt.
    assumption.
  - simpl.
    rewrite <- IHreachable.
    rewrite Z.sub_1_r.
    rewrite <- (pow_pred (b STATE) (e STATE - 1)).
    + rewrite Z.mul_assoc. reflexivity.
    + apply Z.gt_lt in H0.
      apply (proj1 (Z.sub_lt_mono_r 1 (e STATE) 1)).
      assumption.
Qed.

Theorem exp_correct : forall base s,
  reachable base s -> e s = 1 -> r s = (b base) ^ (e base).
Proof.
  intros base s H He.
  apply invariant in H.
  rewrite He in H. simpl in H.
  rewrite (Z.mul_1_r (r s)) in H.
  assumption.
Qed. Check exp_correct.

While this may seem like quite a lot of work to prove what looks like a pretty simple and obvious fact it is worth noting two things:

  1. A proof of this property is beyond the reach of any automated tool available today.
  2. Our mind is full of hidden assumptions, and facts that may seem obvious are not always so. This is not the case for the Coq proof kernel, and once we have convinced it that something is true, we can be very sure that it really is.

Future Work

Automated Spec Generation

Act is designed to be simple and explicit. While this supports automated analysis based on the Act specifications, it does mean that writing specifications by hand often involves quite some boilerplate. In many cases we are mostly interested in whether a given bytecode object satisfies some high level properties, and keeping both the implementation and specification in sync can introduce unwanted overhead to the development process.

For this reason we intend to build an automated spec generation engine into hevm that will utilise the symbolic execution engine to produce an exhaustive description of all possible execution paths as a set of Act specifications. This should allow for fast iteration on the implementation, while keeping the barrier low to at any time performing high-level analyses using Coq or the Act SMT backend.

There are some additional benefits to this approach. The current symbolic execution backend represents our first attempt at a bytecode level proof engine for Act. Unfortunately while building this out we encountered a fundamental issue: while Act specs are expressed in terms of unbounded integers, the symbolic execution engine in hevm uses bitvectors. This means that checking equivalence between a given bytecode object and a set of Act specs requires conversions from integers to bitvectors. While this is tractable for simple specs, it quickly overwhelms the SMT solver for any non-trivial contract (including any safe arithmetic!).

An automated spec generation engine would allow us to sidestep this issue; since the specs would be generated directly from the bytecode they are correct by construction, so it would be unnecessary to prove equivalence between bytecode and specs. Even in the case where specs have been written by hand, we would still only need to prove equivalence between two sets of specs (both of which are written in terms of Integers), once again allowing us to avoid the troublesome bv_to_int and int_to_bv SMT operations.

Automated Checks of Spec Integrity

There are currently many specs that typecheck but are still malformed and would invalidate the proofs derived from them. We intend to add automated analysis passes to detect issues of this kind. At the moment we currently have the following planned:

  • Arithmetic overflow detection (#109)
  • Case consistency checks (#110)
  • Collisions in mapping assignments (#111)

Support for Dynamic / Compound Types

While we have some support at the syntax level for specifications involving dynamic types (e.g. string or bytes), the various proof backends do not currently support proofs involving these types.

We also intend to add support for compound types (e.g. array / struct / tuple) to the language and its proof backends.

Multi Contract Specifications

Similarly to dynamic and compound types, while syntax does exist that allows for specification of multi contract systems, these features are not well supported in the various analysis backends.

Rounding Error Analysis

Understanding the impact of rounding errors in a smart contract is a critical task for secure development. As we saw in the AMM example above, a numeric error introduced by precision loss can result in unexpected violations of important security properties.

There are generally two properties of rounding errors which are of interest:

  • The direction of the rounding error (who loses out)
  • The size of the rounding error (by how much do they lose)

We intend to allow users to specify properties relating to rounding by introducing a new operator (e.g. exact, or toReal), which would indicate that the numeric expression contained within should be expressed in various backends using Reals instead of Ints. This would for example allow for properties that assert statements about the size and direction of the difference between the result of the calculation over the real numbers and its rounded result when expressed over the integers.

For an example of such an analysis performed manually, see the Uniswap v1 model produced by Runtime Verification.

Calls Into Unknown Code

Real world smart contracts must often make calls into unknown code, whether for simple tasks like an ether or token transfer, or for more complex actions (e.g. delegation of control for a flash loan). Each time they do so, they pass control to potentially malicious code that can make arbitrary modifications to the execution context, something that obviously has deep implications for the security of the calling contract. If we wish to prove security properties about realistic smart contracts with Act, we must therefore be able to specify behaviour that includes such calls.

We intend to introduce language constructs and verification routines which will allow specifying and proving properties of such contracts. For more information, we have an issue with early ideas.

Loops and Loop Invariants

Although generally inadvisable, loops are sometimes unavoidable when developing smart contracts (e.g. in numeric routines). We intend to introduce syntax and verification extensions which allow for specification and proving of loop invariants.

For those interested, we have some early thoughts and discussion on the specifics of how to encode loop invariants.

Economic Analysis

Act could be extended with a backend that exports to – possibly even integrates with – an agent-based modelling framework, to allow for complex economic analysis. We believe that Act has some unique advantages here. Simulation could be carried out against the Act expressions (which are generally significantly simpler than the EVM that they model), allowing for fast execution, while still maintaining a formal guarantee that the simulation accurately models the deployed implementation.

Final Remarks

We believe that tools like Act are essential for building high trust smart contract systems, particularly as their scale and complexity increases.

We hope that you’re as excited about this work as we are, and would love to hear your feedback and thoughts on the ideas presented here. Contributions, bug reports and questions are always very welcome in github, or you can always reach us on the chat channels mentioned in the introduction.