formal specification is tricky

Formal specification of programs must be done by hand. One day, it may be possible to describe programs in plain English and have the computer figure out the code on its own. For now, act is as close as we can get.

Let’s look back at the .act.md specification we used last time. If you haven’t yet, read the previous post to learn how to use klab and get some background information.

Here’s our previous spec:

```act
behaviour add of SafeAdd
interface add(uint256 X, uint256 Y)

iff in range uint256

    X + Y

iff

    VCallValue == 0

returns X + Y```

The two iff conditions in the spec above mean that the function can only run if the following conditions are both true:

  1. X + Y are within the range of uint256. This means the sum of the two inputs is between 0 and 2^256 - 1.

  2. The function call does not have any value, as this is not a payable function.

Let’s review our existing smart contract before proceeding. Last time, we proved this Solidity contract’s add() conforms to our specification.

pragma solidity >=0.4.21;

contract SafeAdd {
    function add(uint x, uint y) public pure returns (uint z) {
        require((z = x + y) >= x);
    }
}

Let’s try adding our own function to subtract. I’ll maintain the flavor of the original.

pragma solidity >=0.4.21;

contract SafeAdd {
    function add(uint x, uint y) public pure returns (uint z) {
        require((z = x + y) >= x);
    }

    function sub(uint x, uint y) public pure returns (uint z) {
      require((z = x - y) <= x);
    }
}

compiling your contract

Let’s compile this while we’re at it. Navigate to klab/examples/SafeAdd/dapp and run solc --combined-json=abi,bin,bin-runtime,srcmap,srcmap-runtime,ast src/SafeAdd.sol > out/dapp.sol.json. See the last post for more details.

How should we specify the behavior of this sub() function?

Start by thinking about conditions in which the function should revert:

  • y > x
  • call value > 0

Now we can express these as positive assertions in act:

```act
behaviour sub of SafeAdd
interface sub(uint256 X, uint256 Y)

iff

    X >= Y

iff

    VCallValue == 0

returns X - Y```

Now we can try to generate K modules from our specification.

From klab/examples/SafeAdd, run klab build. If it works, you should see an output similar to this logged to terminal:

12d6d3ef6a5bb43e16d0ea767d0f10035278b2099f8e8ed9458f02dce4aa12a3 SafeAdd__exhaustiveness
66b027f3d1b61dbf00af03b5335f53fb3b7ad83c13ddb7eeea30819c53b0c12d SafeAdd_sub_pass_rough
c0c39ab515831ac7fbf8b8eaa95686cbd6c2c297f76545ce8c0a9b4073058a79 SafeAdd_sub_fail_rough

You can see the names of the K modules generated from our act specification.

Try running one with klab prove --dump SafeAdd_sub_pass_rough. This should pass with a result like

Proof STARTING: 66b027f3d1b61dbf00af03b5335f53fb3b7ad83c13ddb7eeea30819c53b0c12d.k [SafeAdd_sub_pass_rough] (with state logging)
{"format":"KAST","version":1,"term":{"node":"KApply","label":"#True","variable":false,"arity":0,"args":[]}}Proof ACCEPT: 66b027f3d1b61dbf00af03b5335f53fb3b7ad83c13ddb7eeea30819c53b0c12d.k [SafeAdd_sub_pass_rough] (with state logging)

Nice, looks like it worked. If we can run all the proofs successfully (SafeAdd_sub_pass_rough, SafeAdd_sub_fail_rough, and so on), then that means our function has been verified to conform to its specification.

Let’s try to break our function and make sure klab catches it, so we know things are working.

I’ll change the code of SafeAdd.sub() to the following. Typos like switching + and - or <= and >= are a common source of errors.

function sub(uint x, uint y) public pure returns (uint z) {
  require((z = x + y) <= x);
}

Next, repeat the compilation step above, run klab build, and finally klab prove --dump <your choice of K module>. In my case, I ran klab prove --dump SafeAdd_sub_pass_rough.

{"format":"KAST","version":1,"term":{"node":"KToken","sort":"Bool","token":"false"}}Proof 1 REJECT: 6c2927ecb185d6be54e590792e05b300fec8a931086362b4f9cf469f6acb344b.k [SafeAdd_sub_pass_rough] (with state logging)

Failure, which in this case means success for us. klab is great at telling you whether your function matches the spec, but it’s trickier figuring out how it deviates.

Now you know how to write your own formal specifications for Solidity programs in act and prove your program conforms to them using klab.

Stay tuned for more posts about formal verification and smart contract security. Next time, we’ll try out klab’s interactive debugging tools and work on proving a contract with persistent state.