In-place testing with Scribble

A lot of projects come with their own set of tests. Tests are a useful quick check for your properties - if the properties you have in mind don't hold for the user tests, then something might be wrong with them. However in order to build an arbitrary project and run its test suite, Scribble needs to instrument the files in-place, without changing the file/directory structure, or contracts' external interfaces.
In this tutorial we will learn how to instrument a simple project in-place with scribble, and check whether its tests still pass after instrumentation. A failing test may indicate either a bug in your specifications or a bug in your actual program.
Prerequisites
You should have the following installed:
git
node version 12.x
Setting-up
You need to first install scribble:
npm install -g eth-scribble
Next you need to clone the sample project repo:
git clone https://github.com/consensys/scribble-getting-started
And run npm install in the directory containing the tutorial:
cd scribble-getting-started/in-place-testing
npm install
This will install truffle and ganache-cli and any remaining dependencies.
The project
In the scribble-getting-started/in-place-testing directory of the repository you should find a simple Truffle project. Under contracts/ there are 2 contracts of interest - a base contract Managed that contains some logic for adding and removing administrators and a test contract Test that extendsManaged.
Managed.sol
contract Managed {
    address owner;
    mapping(address=>bool) admins;
​
    constructor() public {
        owner = msg.sender;
        admins[owner] = true;
    }
​
    modifier OwnerOnly {
        assert(owner == msg.sender);
        _;
    }
​
    modifier AdminOnly {
        assert(admins[msg.sender]);
        _;
    }
​
    function addAdminInternal(address addr) internal {
        admins[addr] = true;
    }
}
Test.sol
import "./Managed.sol";
​
contract Test is Managed {
    function addAdmin(address newAdmin) public {
        addAdminInternal(newAdmin);
    }
}
One property we may want to add to Managed.sol, is that only current administrators may call the addAdminInternal function. The contract Test violates that property - Test.addAdmin calls addAdminInternal without first checking if the caller is an admin. 

As a first try we can add the following annotation in Managed.sol (extra brownie points if you see something weird already ;)):
/// #if_succeeds {:msg "only owner can add admins"} admins[msg.sender];
function addAdminInternal(address addr) internal {
    admins[addr] = true;
}
The added annotation is a 'function annotation`. It consists of 3 parts:
1.#if_succeeds specifies that the predicate should only be checked if the addAdminInternal function succeeds.
2.{:msg "only owner can add admins"} provides a human-readable message to help remind you what this property is checking. As shorthand you can skip the {:msg } and only specify "only owner can add admins".
3.admins[msg.sender] is the actual property. Its a valid boolean Solidity expression. In this case we are saying that the value of admin[msg.sender] must be true upon successful execution of addAdminInternal.
This project has a test test/tests.js in which a random user tries to add himself as an admin.
contract("Test", (accounts) => {
    it("can add admin", () => {
        return Test.deployed().then(
            async function(instance) {
                await instance.addAdmin(accounts[1], {from: accounts[1]});
            }
        );
    })
})
If we run the test suite without instrumentation this test would actually succeed. We would expect that if we instrumented the contract, and ran the test, the test would fail, showing that the contract doesn't respect the specification.
Instrumenting contracts in-place manually
To instrument the contracts we can run:
scribble contracts/Test.sol --output-mode files
Found 1 annotations in 1 different files.
contracts/Managed.sol -> contracts/Managed.sol.instrumented
The output tells us that scribble created a .instrumented version for Managed.sol. Indeed we should see the new under contracts:
ls contracts
Managed.sol  Managed.sol.instrumented  Migrations.sol  __scribble_ReentrancyUtils.sol  Test.sol
There is a 2nd new file there as well - __scribble_ReentrancyUtils.sol. This is a contract for internal use that scribble always emits.
Now we want to swap the .instrumented file with its original counterpart and re-run the tests. Since we don't want to loose our original files, lets first copy the originals to the side:
cp contracts/Managed.sol contracts/Managed.sol.original
Then copy the instrumented file in-place of the original:
cp contracts/Managed.sol.instrumented contracts/Managed.sol
Now you should be able to run the test suite and hit the failure. To do so in another shell window you must start ganache-cli by running:
npm run testrpc
Back in the original shell you can run the tests with:
truffle test
Using network 'development'.
​
​
Compiling your contracts...
===========================
> Compiling ./contracts/Managed.sol
> Compiling ./contracts/Test.sol
> Compiling ./contracts/__scribble_ReentrancyUtils.sol
> Compilation warnings encountered:
​
    /home/dimo/work/consensys/scribble-getting-started/in-place-testing/contracts/__scribble_ReentrancyUtils.sol:2:1: Warning: Source file does not specify required compiler version! Consider adding "pragma solidity ^0.5.16;"
contract __scribble_REENTRANCY_UTILS {
^ (Relevant source part starts here and spans across multiple lines).
​
> Artifacts written to /tmp/test-202066-9871-gaivy6.q7obe
> Compiled successfully using:
   - solc: 0.5.16+commit.9c3226ce.Emscripten.clang
​
​
​
  Contract: Test
    ✓ can add admin (77ms)
  1 passing (104ms)
But wait! why did that test succeed? Shouldn't it have failed since the sender wasn't an administrator?
The key here is when the admin[msg.sender] predicate was evaluated - it was evaluated after the function had successfully executed, at which point the sender had already added themselves to the admin map. To fix this, we want to talk about the value of admin[msg.sender] before the function started executing. We can do this using the old()operator, which specifies that scribble should compute the value of a given expression before the function is called.
So lets fix this. First lets move the original annotated file back:
cp contracts/Managed.sol.original contracts/Managed.sol
Now lets change the annotation to look like this:
/// #if_succeeds {:msg "only owner can add admins"} old(admins[msg.sender]);
function addAdminInternal(address addr) internal {
    admins[addr] = true;
}
Now if we repeated the whole process of instrumenting, swapping the files, and running tests we should hit an error. But that process is so laborious! There must be a better way! And there is - introducing --armand --disarm.
Scribble --arm and --disarm
Copying files back and forth, keeping track of .sol.instrumented and .sol.original files is annoying. So scribble provides you with two options that take care of this for you.
If you add the --arm option when instrumenting, then scribble will automatically create .sol.original copies of the original files, and swap the instrumented files in-place, so you can start testing immediately. So now that we have fixed our annotation, lets use --arm and --disarm.
First we will instrument the contracts and swap them in-place with a single command:
scribble contracts/Test.sol --output-mode files --arm
Found 1 annotations in 1 different files.
contracts/Managed.sol -> contracts/Managed.sol.instrumented
Copying contracts/Managed.sol to contracts/Managed.sol.original
Copying contracts/Managed.sol.instrumented to contracts/Managed.sol
Note that the new output shows which files were copied where. At this point if we run the tests, we can verify that the fixed annotation fails:
truffle test
...
  1) Contract: Test
       can add admin:
     Error: Returned error: VM Exception while processing transaction: invalid opcode
      at /home/dimo/work/consensys/scribble-getting-started/in-place-testing/test/test.js:7:32
      at process._tickCallback (internal/process/next_tick.js:68:7)
And afterwards we can revert the workspace back by using the--disarm option:
scribble contracts/Test.sol --disarm
Moving contracts/Managed.sol.original to contracts/Managed.sol
Removing contracts/Managed.sol.instrumented
Removing /home/dimo/work/consensys/tmp/test_pass/scribble-getting-started/in-place-testing/contracts/__scribble_ReentrancyUtils.sol
Removing /home/dimo/work/consensys/tmp/test_pass/scribble-getting-started/in-place-testing/instrumentation.scribble.json
Note that the additional .original and .instrumented files, as well as other auxilary files emitted by scribble are all removed:
ls contracts/
Managed.sol  Migrations.sol  Test.sol
If you want to keep the .instrumented files for debugging purposes, add the --keep-instrumented option when disarming.
Testing with and without asserts
When we ran the instrumented tests, we hit an assertion and the test fails. However if we had multiple properties, we wouldn't know WHICH property fails. It would be nice to get a message telling us which property failed. To do so, lets re-instrument the code with the --no-assert option:
scribble contracts/Test.sol --output-mode files --arm --no-assert
Found 1 annotations in 1 different files.
contracts/Managed.sol -> contracts/Managed.sol.instrumented
Copying contracts/Managed.sol to contracts/Managed.sol.original
Copying contracts/Managed.sol.instrumented to contracts/Managed.sol
The --no-assert option tells scribble to not emit an explicit assert(false) on failure, and instead just emit an event. As a result, the tests may not fail anymore, but if you run them with--show-eventsyou will see all the failing properties:
truffle test --show-events
Using network 'development'.
​
​
Compiling your contracts...
===========================
> Compiling ./contracts/Managed.sol
> Compiling ./contracts/Test.sol
> Compiling ./contracts/__scribble_ReentrancyUtils.sol
...
​
  Contract: Test
    ✓ can add admin (72ms)
​
    Events emitted during test:
    ---------------------------
​
    Managed.AssertionFailed(
      message: '0: only owner can add admins' (type: string)
    )
​
​
    ---------------------------
​
​
  1 passing (177ms)
Now we see the AssertionFailed event. Its text contains the human-readable label from the original annotation.
Tutorials - Previous
Property Checking with Scribble and Mythril
Last modified 8mo ago