consensys / scribble

Scribble instrumentation tool

A Solidity runtime verification tool for property based testing.

Tip

Scribble is useful to prepare smart contracts for behavior verification with Diligence Fuzzing or with tools, such as Mythril.

Here are some related videos:

• Test security properties for smart contracts & Detect vulnerabilities
• Web3 Tutorial 23: Next level smart contract security with Diligence Fuzzing

Principles and Design Goals

The design of the Scribble specification language takes inspiration from several existing languages and we expect the language to evolve gradually as we gain more experience in using it. We rely on the following principles and design goals to guide language evolution:

1. Specifications are easy to understand by developers and auditors
2. Specifications are simple to reason about
3. Specifications can be efficiently checked using off-the-shelf analysis tools
4. A small number of core specification constructs are sufficient to express and reason about more advanced constructs

We are aware that this will make it difficult or impossible to express certain properties. We encourage users to reach out if they encounter such properties. However, it is not our itention to support every property imaginable. We consider it a great success if Scribble is able to capture 95% of the properties that users want to express.

Usage

Install Scribble with npm:

npm install -g eth-scribble

Use CLI tool with the Solidity source file:

scribble sample.sol

Use --help to see all available features.

Extension for VS Code

There is a Scribble extension for VSCode that enhances user experience: prividing syntax highlight, hints-on-hover and other features.

Note that it is maintained in separate repostory. Report extension-related suggestions and issues there.

Documentation

For more information on the Scribble specification language, and any other documentation, go to: Scribble Documentation

Development installation

Prerequisites

Preinstall NodeJS of compatible version. If there is a need to run different NodeJS versions, consider using NVM or similar tool for your platform.

Clone and build

Clone repository, install and link:

git clone https://github.com/ConsenSys/scribble.git
cd scribble/
npm install
npm link

Prior to running the tests it would be better to setup local compiler cache:

scribble --download-compilers native wasm

scribble's Issues

Scribble grammar unnecessarily requires `forall` be wrapped in parenthesis

Given the following sample:

contract Foo {
        /// #if_succeeds true && forall (uint i in arr) arr[i] > 1;
        function main(uint[] memory arr) public {}
}

scribble will produce the following syntax error:

tmp.sol:2:26 SyntaxError: Expected "!", "'", "(", "-", "0x", "\"", "hex", "int", "old", "u", [0-9], or whitespace but "f" found.

In:

/// #if_succeeds true && forall (uint i in arr) arr[i] > 1;

The issue is that in the grammar we specify precedence of operators with explicit rules, and the For_All rule is above the LogicalANDExpression rule. However I think its safe to move For_All at the bottom of the chain. Thus the bottom expression rule would become:

PrimaryExpression =
    HexLiteral
    / Identifier
    / Number
    / BooleanLiteral
    / StringLiteral
    / (
        "(" __ expr: Expression __ ")" { return expr; }
    )
    / (RESULT { return new SResult(location()); })
    / For_All

Support user-specified compiler settings in scribble

After the merge of Consensys/solc-typed-ast#66 solc-typed-ast will support user-specified compilerSetting.

We would like to add a new --compiler-settings command-line option to scribble, similar to the one in solc-typed-ast, to allow users to pass their own custom settings to the compiler.

This is useful in cases where the code may not compile with the default compiler settings. One example we encountered was with code that doesn't compile without the optimizer enabled, due to stack limitations.

--debug-events flag doesn't emit correct value for variables inside of `old()`

What the title says :). If you have an annotation like old(a+1) == b, and you add --debug-events then the value that would be emitted in the events for a would be its new value, not its old value. We should fix this.

Add optional assertions for checking property coverage

Users want to know what assertions have been covered. This can usually be checked by looking at the coverage data provided by the underlying tool, and mapping it back to source code.

However sometimes this may not be possible (e.g. missing source code, or missing source mappings). For those case, as a quick and dirty workaround, for every actual instrumented property P, we can add "dummy" property P' which fires if P is reached. For example for this code:

contract Foo {
    /// #if_succeeds true;
    function foo(uint[] memory a) public {}
}

We would generate the following code:

contract Foo {
    event AssertionFailed(string message);

    function foo(uint[] memory a) public {
        _original_Foo_foo(a);
        {
            emit AssertionFailed("HIT: 0: ");
            if (!(true)) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Foo_foo(uint[] memory a) private {}
}

Note that the event emit AssertionFaield("HIT: 0: ") is emitted regardless of whether the actual assertion failed, as long as its condition was evaluated.

We should add a command line flag --cov-assertions to emit these.

Ability to execute scribble programmatically

Currently scribble is designed to be used from cli
to make it easier to write tool around scribble, it would be great if we could execute it programmatically from js.
Maybe it is just a matter of documentation ?

force disarm

With this contract have trouble. Command scribble --arm -m files Test.sol working, but command scribble --disarm -m files Test.sol doesn't.

pragma solidity ^0.6.0;

contract Test {

    /// if_succeeds {:msg "wrong byte"} checkBytes(_bytes) == result;
    function process(bytes calldata _bytes) external returns (bool result) {
        return this.checkBytes(_bytes);
    }

    function checkBytes(bytes calldata _bytes) pure external returns (bool result) {
        return _bytes.length > 0;
    }
}

log:

$ scribble --arm -m files Test.sol
Test.sol -> Test.sol.instrumented
Copying Test.sol to Test.sol.original
Copying Test.sol.instrumented to Test.sol

$ scribble --disarm -m files Test.sol
Compile errors encountered for Test.sol:
SolcJS 0.6.12:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.11:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.10:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.9:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.8:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.7:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.6:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.5:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.4:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.3:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.2:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.1:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.0:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

Support for arbitrary assertions

There are times when an assertion is relatively simple and easiest to express in-line. This can obviously be expressed directly in solidity, but using Scribble in these cases would save the trouble of carefully removing these assertions before deploying (or incurring the gas cost of these checks in live contracts).

I am envisioning a #raw or #inline property type that allows you to write a normal solidity if statement + assertion, and just takes care of inserting/removing this assertion for you.

contract Calculator {
    enum Op {
        PLUS,
        TIMES
    }
    function calc(Op operator, uint left, uint right) public returns (uint result) {
        if (operator == Op.TIMES) {
            return left * right;
        }
        if (operator == Op.PLUS) {
            return left + right;
        }
        /// #raw {:msg "no return"} assert (false);
    }
}

Adding an invariant to a contract function is silently ignored when arming the smart contract

Example for the batch deposit contract where an invariant is placed before a function* https://gist.github.com/Magicking/fe63df8e8fce9a0710c53bc34fec7ac9/0890379fc80c3f55aba53dc52639723c48be6dfc#file-batchdeposit-sol-L72
And the result from npx scribble --arm batchDeposit.sol produced this armed smart contract https://gist.github.com/Magicking/fe63df8e8fce9a0710c53bc34fec7ac9/e57c7b5b094083dfea77bfcd3434528e6440d948#file-batchdepositarmed-sol-L64 where the NatSpec documentation is remove (which I think may be a separate bug) and the assert for this invariant is silently ignored.

*The solution found was to return the value and verify it's value, see here https://gist.github.com/Magicking/fe63df8e8fce9a0710c53bc34fec7ac9

Support structural equality comparison of non-value types in Scribble

We have use cases for comparing strings, arrays and structs in properties. However the base Solidity language doesn't support equality comparison of non-value types.

We could add structural equality comparison support to Scribble, by transpiling it into comparison between the abi.encode-ed versions of the data structures. So for example this:

contract Foo {
   /// #if_succeeds a == b;
   function main(string memory a, string calldata b) public { ... }
}

Would be transpiled to:

contract Foo is __scribble_ReentrancyUtils  {
    event AssertionFailed(string message);

    function main(string memory a, string calldata b) public {
        _original_Foo_main(a, b);
        unchecked {
            if (!(bytesEq(abi.encode(a), abi.encode(b)))) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Foo_main(string memory a, string calldata b) private { ... }
}
/// Utility contract holding a stack counter
contract __scribble_ReentrancyUtils {
    bool __scribble_out_of_contract = true;
    
    function bytesEq(bytes memory a, bytes memory b) internal returns (boolean) {
      if (a.length != b.length) { return false; }
      
      for (uint i = 0; i < a.length; i++) {
        if (a[i] != b[i]) return false;
      }
      
      return true;
    }
}

Support custom NatSpec tags

Since Solidity 0.8.2 (March 2021) custom NatSpec tags are supported (see the docs and this discussion for context).

It would be nice for Scribble to support it, e.g.:

/// @custom:scribble if_succeeds {:msg "P0"} y == x + 1;

I understand that for supporting older language versions the current syntax should also be kept supported, but at least users' of newer versions can move on to custom tags, which means their NatSpec output will not have Scribble instructions in their user facing @notice tags.

Support Using For

Сan you add support for similar solidity instructions?
solidity using-for

Scribble crashes when interposing on public variable accessor calls

For the following sample:

contract A {
  uint public a;
}

/// #invariant uint24(1) == 2;
contract B {
  function f() external returns (uint) {
     return A(msg.sender).a();
  }
}

Scribble crashes with the following stack:

 /home/dimo/work/consensys/scribble/dist/bin/scribble.js:484
            throw e;
            ^

Error
    at Object.assert (/home/dimo/work/consensys/scribble/dist/util/misc.js:16:11)
    at Object.interposeCall (/home/dimo/work/consensys/scribble/dist/instrumenter/interpose.js:245:16)
    at replaceExternalCallSites (/home/dimo/work/consensys/scribble/dist/instrumenter/instrument.js:406:45)
    at Object.instrumentContract (/home/dimo/work/consensys/scribble/dist/instrumenter/instrument.js:262:9)
    at instrumentFiles (/home/dimo/work/consensys/scribble/dist/bin/scribble.js:185:17)
    at Object.<anonymous> (/home/dimo/work/consensys/scribble/dist/bin/scribble.js:478:13)
    at Module._compile (internal/modules/cjs/loader.js:1137:30)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1157:10)
    at Module.load (internal/modules/cjs/loader.js:985:32)
    at Function.Module._load (internal/modules/cjs/loader.js:878:14)

We fail this assertion in interposeCall:

    if (call.vFunctionCallType === ExternalReferenceType.UserDefined) {
        const calleeDef = call.vReferencedDeclaration;

        assert(calleeDef !== undefined && calleeDef instanceof FunctionDefinition, ``);

        const fPtrT = makeFunPtrType(calleeDef, factory);

Esentially the logic here doesn't handle the case when calleeDef is a VariableDeclaration.

Handling it correctly here first requires a fix in solc-typed-ast to get the expected argument and return types of a getter for an arbitrary public state var.

Scribble needs to disallow equality comparisons between reference types

Consider the following sample:

contract Foo {
    struct S {
        uint[] arr;
    }
    /// #if_succeeds a == b;
    function main(S memory a, S memory b) private {
    }
}

Scrible's type-checker will allow the expression a==b and transpile it into the following code:

...
    function main(S memory a, S memory b) private {
        _original_Foo_main(a, b);
        unchecked {
            if (!(a == b)) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }
...

That code however doesn't compile since you can't compare pointers in Solidity. To fix this the scribble type-checker should be made more precise, to disallow equality comparison between reference types.

Warn users when annotations may add inifinte loops

Instrumentation turns the following terminating code into non-terminating code:

contract Foo {
        function double1(uint x) public view returns (uint) {
                return double2(x);
        }

        /// if_succeeds $result == double1(x);
        function double2(uint x) public view returns (uint) {
                return x + x;
        }
}

We can use the callgraph of the original code to detect when function calls in the annotations may create cycles and issue warnings for users that the annotations may introduce infinite recursion. For example this check shouldn't flag anything in the following sample:

contract Foo {
        /// if_succeeds $result == double2(x);
        function double1(uint x) public view returns (uint) {
                return x * 2;
        }       

        /// if_succeeds $result == double1(x);
        function double2(uint x) public view returns (uint) {
                return x + x;
        }       
}

Javascript call stack exceeded

On the same codebase whatever I do (like adding an invariant or a if_succeeds statement) I keep getting Javascript Maximum call stack size exceeded errors.

Two kinds in particular:

1. The first seems to be inside type checking:

Internal error in type-checking: Maximum call stack size exceeded

2. The seconds seems to be around recursive imports:

/Users/alex/Projects/scribble/dist/bin/scribble.js:494
            throw e;
            ^

RangeError: Maximum call stack size exceeded
    at ImportDirective.get vSymbolAliases [as vSymbolAliases] (/Users/alex/Projects/scribble/node_modules/solc-typed-ast/dist/ast/implementation/meta/import_directive.js:55:45)
    at lookupInSourceUnit (/Users/alex/Projects/scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:101:28)
    at lookupInSourceUnit.next (<anonymous>)
    at new Set (<anonymous>)
    at lookupInScope (/Users/alex/Projects/scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:229:12)
    at lookupInSourceUnit (/Users/alex/Projects/scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:104:35)
    at lookupInSourceUnit.next (<anonymous>)
    at new Set (<anonymous>)
    at lookupInScope (/Users/alex/Projects/scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:229:12)
    at lookupInSourceUnit (/Users/alex/Projects/scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:104:35)

(It is a local install of 912a472)

I think the second case may be connected to #64.

I tried for a quite bit of time create a reduced example, but can't really spend too many hours on it. @cd1m0 do you have any idea based on the above?

Scribble fails on explicit call to inherited constructor.

The following two examples are accepted by Scribble:

contract A {
    int public a;
    constructor() {}
}

/// #invariant a >= 0;
contract B is A {
    constructor() {}
}

contract A {
    int public a;
    constructor(int _a) { require(_a >= 0); a = _a; }
}

/// #invariant a > 0;
contract B is A(1) {
    constructor() {}
}

The following example yields Error: Mismatch in length between [VariableDeclaration#6] of len 1 and [] of len 0:

contract A {
    uint public a;
    constructor(uint _a) { require(_a >= 0); a = _a; }
}

/// #invariant a > 0;
contract B is A {
    constructor() A(1) {}
}

I am running the latest version of Scribble on npm using node version 10.24.1.

Extending OpenZeppelin's ERC20 as an abstract contract fails

import "@openzeppelin/contracts/token/ERC20/ERC20.sol";

abstract contract MyERC20 is ERC20 {
}

This fails with the error:

/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/util/misc.js:16
    throw new Error(message);
    ^

Error: Mismatch in length between [VariableDeclaration#32,VariableDeclaration#34] of len 2 and [] of len 0
    at assert (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/util/misc.js:16:11)
    at Object.zip (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/util/misc.js:195:5)
    at helper (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:104:24)
    at getAssignments (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:238:20)
    at getAssignments.next (<anonymous>)
    at Object.findAliasedStateVars (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:272:21)
    at new InstrumentationContext (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/instrumentation_context.js:231:38)
    at Object.<anonymous> (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/bin/scribble.js:582:26)
    at Module._compile (node:internal/modules/cjs/loader:1101:14)
    at Object.Module._extensions..js (node:internal/modules/cjs/loader:1153:10)

Parsing openzeppelin/contracts/token/ERC20/ERC20.sol directly works with scribble, so abstract seems to have some relevance here.

Disarm fails when instrumented code fails to compile

If you have a contract that compiles before being instrumented but fails to compile after being instrumented, scribble will successfully arm the contract but fail to disarm it. This can leave a bit of a mess of armed files to clean up before you can fix or diagnose the issue.

Example

Shadowed.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

interface IShadower {
    function shadowed(uint256 a) external;
    function shadowed(uint256 a, uint256 b) external;
}

/// #invariant {:msg "I0"} 0 == 0;
contract Scribbled {
    function entry() external {
        IShadower(address(0)).shadowed(1);
    }
}

solc Shadowed.sol

Succeeds.

scribble Shadowed.sol --output-mode files --arm

Succeeds, but leaves an instrumented Shadowed.sol that fails to compile.

In this case, it is because the function pointer passed to the _callsite_ method cannot discern between the two versions of IShadower.shadowed(). As far as I know, this is a limitation of solidity rather than a scribble bug, but used here as an example.

scribble Shadowed.sol --output-mode files --disarm

Because the newly instrumented Shadowed.sol won't compile, this fails and leaves armed files that must be sorted out manually or reverted to a previous commit.

Feature Request

• If it's not necessary to compile the armed contracts before disarming, that seems like an easy fix. Maybe this could be behind a --disarm --force flag.
• Attempt to compile the armed contracts and revert instrumenting if they fail to compile.

Support multiple properties in `#try`

In #112 we added the new #try annotation that can guide underlying tools (e.g. Harvey) by giving them vacuous target branches to flip. Currently #try accepts a single predicate:

#try x == 1;

To express multiple predicates to try independently, we need multiple tries:

#try x == 1;
#try y == 2;
#try z == 3;

It would be a little cleaner to allow #try to take multiple predicates, where the semantics is the same as if there were multiple tries, one per predicate. So the above would be equivalently expressed as:

#try x ==1, y==2, z== 3;

Note that these shouldn't just be treated as one giant disjunction x == 1 || y ==2 || z ==3. If we transpile them as such, then due to short-circuiting of the compiler, certain truth combinations will not be explored. For example if x==1, the emitted code will not even evaluate y==2 || z ==3, so for example the fuzzer will not explore x == 1 && y == 2 and x == 1 && y != 2.

Scribble compiles `old()` in `if_updated` incorrectly when there are inline initializers of state vars

Consider the below sample:

contract Foo {
        /// #if_updated !(old(x) == 1);
        uint x = 1;
}

x is initialized only once, and before that its "old" value is 0. So this shouldn't fail. However we incorrectly instrument this to the following code:

contract Foo {
    event AssertionFailed(string message);

    struct vars0 {
        uint256 old_0;
    }

    uint internal x = 1;

    function Foo_x_inline_initializer() internal {
        vars0 memory _v;
        unchecked {
            _v.old_0 = x;
        }
        unchecked {
            if (!(!(_v.old_0 == 1))) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    constructor() {
        Foo_x_inline_initializer();
    }

The problem is that to correctly "check" old values before inline initializers, we need to migrate those inside the constructor. Since inline initializers may depend on each other, this is a rather non-trivial task. Also fundamentally we can spend more time arguing about what "old" means for state variable updates at the begining of time.

For now add a check that makes scribble fail with the proper error message in this case.

Support require-annotations to guide tools

It could be useful to support require-annotation for guiding tools without changing the code itself. This could be very similar to the existing assert-annotations. Below is a more concrete example where some known tokens should be used as inputs:

contract C {
    function foo(address token) public {
      /// #require token == address(0x0) || token == address(0x1234) || token == address(0xabcd);
      ...
      token.transferFrom(...);

Bug if using if_updated and if_succeeds

scribble 0.4.2

pragma solidity >=0.6.0 <0.8.0;

contract Token {
    function balanceOf(address x) external pure returns (uint) {
        return 123;
    }
}

contract Foo {
    /// if_updated tokenBalance == 123;
    uint public tokenBalance = 1;
    
    /// if_succeeds Token(x).balanceOf(address(this)) == 123;
    function updateBalance(address x) public returns (uint) {
        tokenBalance = Token(x).balanceOf(address(this));
        return tokenBalance;
    }
}

/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/bin/scribble.js:574
            throw e;
            ^

Error: Mismatch in length between [] of len 0 and [Identifier#81] of len 1
    at assert (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/util/misc.js:16:11)
    at Object.zip (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/util/misc.js:194:5)
    at helper (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:99:24)
    at getAssignments (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:204:20)
    at getAssignments.next (<anonymous>)
    at Object.findAliasedStateVars (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:262:21)
    at instrumentFiles (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/bin/scribble.js:165:38)
    at Object.<anonymous> (/.nvm/versions/node/v12.22.1/lib/node_modules/eth-scribble/dist/bin/scribble.js:568:40)
    at Module._compile (internal/modules/cjs/loader.js:999:30)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1027:10)

When interposing on constructors super constructor invocations get put on the wrong function.

Given the following code:

contract Base {
    constructor(uint x) public {}
}

/// #if_succeeds true;
contract Child is Base {
    constructor() Base(1) {
    }
}

When we instrument the Base(1) super-constructor invocation gets mistakenly placed on the inner _original_Child_constructor function, instead of the constructor:

/// #if_succeeds true;
contract Child is Base {
    event AssertionFailed(string message);

    constructor() {
        _original_Child_constructor();
        unchecked {
            if (!(true)) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Child_constructor() Base(1)  private {}
}

Thus the resulting code doesn't compile. It should be placed on the constructor.

Re-consider the semantics of #limit and #hint

As mentioned in #103 the semantics of #limit and #hint is a little confusing. More specifically:

1. #limit and #hint are the only two function-level annotations that are implicitly evaluated in the old state. This might be confusing for users

2. #limit and #hint are allowed at the contract state as well, and the intent is to have the same behavior as if_succeeds. This needs to be tested well with old()

3. The names #limit and #hint are confusing. As per discussions with the team, change them to #require and #try and allow #try to accept a list of predicates.

Support `abi.encodePacked` in scribble

Do as the title says. After fixing the following code should instrument:

contract Foo {
   /// #if_succeeds abi.encodePacked(a).length > 0;
   function main(string memory a) public { }
}

Instead of throwing the below error:

tmp3.sol:2:37 TypeError: Builtin struct "abi" does not have a member "encodePacked"

In:

if_succeeds abi.encodePacked(a).length > 0;

Type-checker needs to support library-level constants

The below code will throw a type error at Foo.Life. We need to support library constants in the type-checker.

library Foo {
        uint256 constant Life = 42;
}

contract Boo {
        /// #if_succeeds $result == Foo.Life;
        function answerOfLife() public returns (uint) {}
}

Don't apply contract-level `if_succeeds` annotations to view functions

Currently we support contract-level if_succeed annotations that get applied to all non-pure public/external functions of the contract. There is really no need to apply them to the view functions, as they don't change state. However adding these annotations to view functions changes their mutability, which can sometimes cause not to compile. So lets not do it.

Scribble crashes in the presence of assingments from storage pointers to storage pointers

Consider the following sample:

contract Foo {
    struct S {
        uint[] arr;
    }

    function main(S storage v) private {
        S storage v1 = v;
    }
}

Running scribble (up to version 0.5.5) on this produces the following crash:

/home/dimo/work/consensys/scribble-clean/dist/instrumenter/state_vars.js:321
        throw new Error(`Unexpected RHS element ${__1.print(rhs)} in assignment to state var pointer`);
        ^

Error: Unexpected RHS element v in assignment to state var pointer
    at gatherRHSVars (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/state_vars.js:321:15)
    at Object.findAliasedStateVars (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/state_vars.js:350:26)
    at new InstrumentationContext (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/instrumentation_context.js:231:38)
    at Object.<anonymous> (/home/dimo/work/consensys/scribble-clean/dist/bin/scribble.js:487:26)
    at Module._compile (internal/modules/cjs/loader.js:1015:30)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1035:10)
    at Module.load (internal/modules/cjs/loader.js:879:32)
    at Function.Module._load (internal/modules/cjs/loader.js:724:14)
    at Function.executeUserEntryPoint [as runMain] (internal/modules/run_main.js:60:12)
    at internal/main/run_main_module.js:17:47

The issue is that the logic of this does not account for the case where the RHS of an assignment to a storage pointer is an Identifier, but its not a direct reference to a state var. This happens when the RHS is another storage pointer. (see code below):

    /**
     * Given a potentially complex RHS expression, return the list of
     * state variable declarations that it may alias
     */
    const gatherRHSVars = (rhs: Expression): VariableDeclaration[] => {
        if (isStateVarRef(rhs)) { // <-- This check needs to handle all Identifiers
            return [rhs.vReferencedDeclaration as VariableDeclaration];
        }

...
        throw new Error(`Unexpected RHS element ${print(rhs)} in assignment to state var pointer`);
    };

Remove support for deprecated annotations without hashtag

We have deprecated annotations that do not start with a hashatag since 2021-05-18 ( 03e036d ). We should now fully remove those to reduce code complexity.

if_updated annotations lost when mixing in forall annotations

Consider the following sample:

contract Foo {
    function main() public {
        m[0] = 1;
    }

    /// #if_updated forall(uint i in m) m[i] > 0;
    mapping(uint=>uint) m;

}

When we instrument it, the resulting code is missing the actual check:

pragma solidity 0.8.7;

contract Foo {
    uint256_to_uint256.S internal m;

    function main() public {
        uint256_to_uint256.set(m, 0, 1);
    }
}
...

GitCoin Bounty 💰 - Syntax Highlighting

The most popular code understanding tool is syntax highlighting. Scribble is a specification language for Solidity smart contracts, where users write annotations in their smart contracts to formalise properties. Unfortunately, Scribble is a new language and there aren’t any highlighters written for it yet.

✍️ Description of Challenge

Scribble is a specification language for solidity smart contracts. This is a bounty for the implementation of syntax highlighting for Scribble annotations.

Requirements

1. Write a grammar for Scribble annotations
   1. You can use either tree-sitter or TextMate
   2. The grammar should cover the features currently in Scribble. Including:
      1. if_succeeds
      2. invariant
      3. define
      4. let bindings
      5. old
      6. $result
      7. implication (==>)
   3. Add support for highlighting to the grammar (how depends on whether you’ll use tree-sitter or text-mate)
   4. If supported by the grammar tooling then there should be adequate tests.
2. Implement a VSCode plugin for Scribble
   1. This plugin should use the tree-sitter or text-mate highlighting to highlight scribble annotations
   2. Highlighting should use colours provided by the editor theme
3. Submit a PR for the add-on to ConsenSys/scribble-highlighting
   1. This PR should add both the required grammar and vscode plugin code

☑ Judging Criteria

• Test suite quality
• Implementation of CI/CD pipelines to automatically build, test and deploy newer versions of the tree-sitter grammar and VSCode package
• Maintainability, and available documentation
• You get bonus points if you also submit plugins for popular editors like vim 😁

🔗 Useful Links

• Scribble Documentation
• Tree-sitter｜Syntax Highlighting
• Language Grammars — TextMate 1.x Manual
• GitHub - JoranHonig/tree-sitter-solidity: Solidity grammar for tree sitter
• Syntax Highlight Guide | Visual Studio Code Extension API
• Reference Scribble PEG.js grammar

PS

If you're working on this bounty, then come hang out with us on discord! We'll be there to help you out in case you have any questions.

false positive SyntaxError

I have a false positive syntax error in a dependent contract from openzeppelin
MerkleProof.sol

/**
 * @dev These functions deal with verification of Merkle trees (hash trees),
 */
library MerkleProofUpgradeable {
    /**
     * @dev Returns true if a `leaf` can be proved to be a part of a Merkle tree
     * defined by `root`. For this, a `proof` must be provided, containing
     * sibling hashes on the branch from the leaf to the root of the tree. Each
     * pair of leaves and each pair of pre-images are assumed to be sorted.
     */
    function verify(bytes32[] memory proof, bytes32 root, bytes32 leaf) internal pure returns (bool) {
        bytes32 computedHash = leaf;

        for (uint256 i = 0; i < proof.length; i++) {
            bytes32 proofElement = proof[i];

            if (computedHash <= proofElement) {
                // Hash(current computed hash + current element of the proof)
                computedHash = keccak256(abi.encodePacked(computedHash, proofElement));
            } else {
                // Hash(current element of the proof + current computed hash)
                computedHash = keccak256(abi.encodePacked(proofElement, computedHash));
            }
        }

        // Check if the computed hash (root) is equal to the provided root
        return computedHash == root;
    }
}

log:

$ scribble --arm ./MerkleProof.sol

./MerkleProof.sol:11:15 SyntaxError: Expected "(" or whitespace but "b" found.

In:


     * defined by `root`. For this, a `proof` must be provided, containing
     * sibling hashes on the branch from the leaf to the root of the tree. Each
     * pair of leaves and each pair of pre-images are assumed to be sorted.
     */

scribble veriosn 0.4.0

Exception thrown when calling an annotated function from another annotation

Instrumenting the following sample:

contract CallinInstrumentedFun {
    uint x = 1;
    /// if_succeeds res > 0;
    function getX() public view returns (uint res) {
        return x;
    }

    /// if_succeeds res == x + getX();
    function inc(uint x) public returns (uint res) {
        return x + getX();
    }
}

Produces this exception:

/home/dimo/work/consensys/scribble-clean/dist/bin/scribble.js:574
            throw e;
            ^

Error: Internal error: variable id getX has different name from underlying variable FunctionDefinition #208
    id: 208
    src: "2967:72:0"
    type: "FunctionDefinition"
    implemented: true
    virtual: false
    scope: 204
    kind: "function"
    name: "_original_CallinInstrumentedFun_getX"
    visibility: "private"
    stateMutability: "view"
    isConstructor: false
    documentation: undefined
    nameLocation: undefined
    vParameters: ParameterList #210
    vReturnParameters: ParameterList #211
    vModifiers: Array(0)
    vOverrideSpecifier: undefined
    vBody: Block #214
    context: ASTContext #2
    parent: ContractDefinition #204
    <getter> children: Array(3) [ ParameterList #210, ParameterList #211, Block #214 ]
    <getter> vScope: ContractDefinition #204
    <getter> canonicalSignature: "_original_CallinInstrumentedFun_getX()"
    <getter> canonicalSignatureHash: "28cc8fb6"
    <getter> firstChild: ParameterList #210
    <getter> lastChild: Block #214
    <getter> previousSibling: FunctionDefinition #804
    <getter> nextSibling: FunctionDefinition #846
    <getter> root: SourceUnit #0
    <getter> sourceInfo: Object { offset: 2967, length: 72, sourceIndex: 0 }

    at generateIdAST (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/transpile.js:129:15)
    at generateExprAST (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/transpile.js:154:16)
    at generateExprAST (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/transpile.js:215:22)
    at generateExprAST (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/transpile.js:188:23)
    at Object.generateExprAST (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/transpile.js:188:23)
    at /home/dimo/work/consensys/scribble-clean/dist/instrumenter/instrument.js:436:74
    at Array.map (<anonymous>)
    at generateExpressions (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/instrument.js:436:44)
    at FunctionInstrumenter.instrument (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/instrument.js:792:29)
    at instrumentFiles (/home/dimo/work/consensys/scribble-clean/dist/bin/scribble.js:161:34)

This is due to an overzealous check in generateIdAST. Fix is to remove the check.

`forall` broken in new #limit annotation

Given the following sample:

contract Foo {
        /// #limit forall (uint k in a) a[k] > 1;
    function foo(uint[] memory a) public {}
}

Scribble produces the following broken instrumentation code:

pragma solidity 0.7.6;

contract Foo {
...
    function foo(uint[] memory a) public {
        vars0 memory _v;
        require(_v.forall_0);
        _original_Foo_foo(a);
        _v.forall_0 = true;
        for (_v.k0 = 0; _v.k0 < a.length; _v.k0++) {
            _v.forall_0 = a[_v.k0] > 1;
            if (!_v.forall_0) break;
        }
    }

    function _original_Foo_foo(uint[] memory a) private {}
}

The issue is that the require(_v.forall_0); is placed before the call to the original function, while the computation for the forall is placed after the call.

limit is intended to always be evaluated in the old() state of a function, so the forall should be placed before the function.

Note: As a separate issue we should revisit if the semantics of limit (to be implicitly in the old() state) makes sense.

Scribble crashes when mixing `for_all` and `if_updated` on nested mappings

Consider the following sample:

contract Foo {
    /// #if_updated forall(uint k in m) m[k][0] > 1;
    mapping(uint=>mapping(uint => uint)) m;

    function main() public {
        m[0][1] = 1;
    }
}```

Running scribble 0.5.5 on this sample produces the following crash:

/home/dimo/work/consensys/scribble-clean/dist/bin/scribble.js:500
throw e;
^

Error
at Object.assert (/home/dimo/work/consensys/scribble-clean/dist/util/misc.js:16:11)
at decomposeLHS (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/state_vars.js:395:9)
at addStateVarUpdateLocDesc (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/state_vars.js:456:33)
at Object.findStateVarUpdates (/home/dimo/work/consensys/scribble-clean/dist/instrumenter/state_vars.js:481:13)
at instrumentFiles (/home/dimo/work/consensys/scribble-clean/dist/bin/scribble.js:204:37)
at Object. (/home/dimo/work/consensys/scribble-clean/dist/bin/scribble.js:494:13)
at Module._compile (internal/modules/cjs/loader.js:1015:30)
at Object.Module._extensions..js (internal/modules/cjs/loader.js:1035:10)
at Module.load (internal/modules/cjs/loader.js:879:32)
at Function.Module._load (internal/modules/cjs/loader.js:724:14)

The issue is that the logic inside `decomposeLHS` is not written to handle functions returning a storage pointer, since scribble doesn't allow instrumenting state variables that are aliased. However the custom mapping instrumentation due to the `forall` introduces a call to `<custom map library>.get_lhs(...)` on the LHS of an assignment. To fix this we need to make `decomposeLHS` aware of potential changes done by the custom map instrumentation.

Migrate to PeggyJS

It seems that PEG.js is no longer maintained: pegjs/pegjs#639. There is a compatible alternative (pegjs/pegjs#667) called Peggy, that is revived version of original project. It also has an online sandbox. Consider to migrate.

`require` annotation keyword causing issues with openzeppelin

When trying to instrument the below contract inheriting from open zeppelin:

// contracts/simple.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.4;

import "@openzeppelin/contracts/token/ERC20/ERC20.sol";

/// #invariant unchecked_sum(_balances) == _totalSupply;
contract Simple is ERC20 {
    /**  @dev Token Constructor
     */     
    constructor() ERC20("Simple", "Simple") payable {
    }

Scribble throws the following error:

DEBUG:fuzzing-cli:Initializing configuration context
DEBUG:fuzzing-cli:Parsing config at .fuzz.yml
DEBUG:fuzzing-cli:Initializing tool name middleware with 0.8.1
Scribble has encountered an error (code: 1)
=====STDERR=====
@openzeppelin/contracts/token/ERC20/ERC20.sol:140:16 SyntaxError: Expected "!=", "%", "&", "&&", "*", "**", "+", "-", ".", "/", ";", "<", "<<", "<=", "==", "==>", ">", ">=", ">>", "?", "[", "^", "|", "||", or whitespace but "b" found.

In:


     * required by the EIP. See the note at the beginning of {ERC20}.
     *
     * Requirements:
     *
     * - `sender` and `recipient` cannot be the zero address.
     * - `sender` must have a balance of at least `amount`.
     * - the caller must have allowance for ``sender``'s tokens of at least
     * `amount`.
     */

=====STDOUT=====

The issue is that the regex pattern inside findAnnotations mistakenly considers the * required .... to be the start of an annotation:

    const rx =
        /\s*(\*|\/\/\/)\s*#?(if_succeeds|if_updated|if_assigned|invariant|assert|try|require|define\s*[a-zA-Z0-9_]*\s*\([^)]*\)|macro\s*[a-zA-Z0-9_]*\s*\([^)]*\))/g;

    let match = rx.exec(meta.text);
    ...

Honestly I think the best solution is to finally disallow the (already deprecated) annotation keywords without a '#' (as tracked by #125).

If we decide to do this will close this as duplicate of that one.

Make annotation metadata actual metadata

Annotations currently support the { :msg "some label" } syntax. The intent of the syntax is to support arbitrary metadata tags there, however currently there is only the :msg tag hardcoded in the grammar. In anticipation of allowing other tags (e.g. we are discussing a skipConstructor boolean metadata tag), we should:

1. Fix the grammar and data-types to support a comma separated list of :tag value

2. Check that the values provided correspond to the expected type of the tag (so for exampel ":msg 1" should be an error)

Support new 'hardhat' `--user-assert-mode`

Scribble is sometimes used to instrument the code for local testing. When this is done in a Hardhat environment, people often use console.log(...) to print out various information. In this mode, it is more convenient to signal user assertion failures with console.log() instead of emitting events, so that users can just look at their terminal instead of go hunting through the logs. In this mode we would support a new option for the --user-assert-mode key as follows.

Given the below sample:

contract Foo {
        /// #if_succeeds {:msg "Property 0 fail"} x > 0;
        function foo(uint x) public {}
}

When we instrument it with scribble --user-assert-mode hardhat tmp.sol we would get the following code:

import "hardhat/console.sol";

contract Foo {
    function foo(uint x) public {
        _original_Foo_foo(x);
        if (!(x > 0)) {
            console.log("0: Property 0 fail");
            assert(false);
        }
    }

    function _original_Foo_foo(uint x) private {}
}

Debug events would also be converted to console.logs. So running scribble --user-assert-mode hardhat tmp.sol --debug-events would produce:

import "hardhat/console.sol";

contract Foo {
    function foo(uint x) public {
        _original_Foo_foo(x);
        if (!(x > 0)) {
            console.log("0: Property 0 fail");
            console.log("x:", x);
            assert(false);
        }
    }

    function _original_Foo_foo(uint x) private {}
}

Note that the console.log() functions in hardhat are limited to up to 4 arguments, so extra work needs to be done when we need to print more than 4 values.

Scribble crashes on literals in certain places

The following sample cause a crash:

/// #invariant let a := 1 in a > 0;
contract Foo {
}

Stack trace:

/home/dimo/work/consensys/scribble/dist/bin/scribble.js:484
            throw e;
            ^

Error: Unsupported spec type int_const
    at transpileType (/home/dimo/work/consensys/scribble/dist/instrumenter/transpile.js:21:15)
    at transpileLet (/home/dimo/work/consensys/scribble/dist/instrumenter/transpile.js:387:22)
    at transpile (/home/dimo/work/consensys/scribble/dist/instrumenter/transpile.js:552:16)
    at Object.transpileAnnotation (/home/dimo/work/consensys/scribble/dist/instrumenter/transpile.js:494:16)
    at insertAnnotations (/home/dimo/work/consensys/scribble/dist/instrumenter/instrument.js:225:42)
    at makeInternalInvariantChecker (/home/dimo/work/consensys/scribble/dist/instrumenter/instrument.js:325:5)
    at Object.instrumentContract (/home/dimo/work/consensys/scribble/dist/instrumenter/instrument.js:258:36)
    at instrumentFiles (/home/dimo/work/consensys/scribble/dist/bin/scribble.js:185:17)
    at Object.<anonymous> (/home/dimo/work/consensys/scribble/dist/bin/scribble.js:478:13)
    at Module._compile (internal/modules/cjs/loader.js:1137:30)

The problem is that we are not inferring a type for the underlying temporary used to store a. For now the user can avoid this by just adding a cast:

    /// #invariant let a := uint(1) in a > 0;

We can try to pick the smallest type that fits the literal, but this may cause other problems, for example in this case /// invariant let a:= 1 in a == int(1). This would fail type checking with this scheme, as the smallest type to fit the 1 is uint8 but a is used in the body of the let as an int256.

Another solution would be to produce a proper error message, that asks the user to qualify the type of the temporary. The same problem can be hit with the following syntactic constructs:

/// #invariant (let a := true in 0) == 0;
contract Foo {
}

contract Foo {
        /// #if_succeeds old(0) > 0;
        function foo() internal {}
}

Scribble should allow comparison between addresses

The scribble type checker disallows expressions of the type address(0x0) < address(0x1). Solidity allows them however. We should allow them in the typechecker too.

Accessors are not properly supported

contract A {
  uint public a;
}

contract B {
  function f() external returns (uint) {
     return A(msg.sender).a();
  }
}

The above code will crash on develop:

/scribble/dist/util/misc.js:16
    throw new Error(message);
    ^

Error: Unexpected callee variable without function type
    at Object.assert (/scribble/dist/util/misc.js:16:11)
    at getAssignments (/scribble/dist/instrumenter/state_vars.js:182:21)
    at getAssignments.next (<anonymous>)
    at Object.findAliasedStateVars (/scribble/dist/instrumenter/state_vars.js:266:21)
    at new InstrumentationContext (/scribble/dist/instrumenter/instrumentation_context.js:231:38)
    at Object.<anonymous> (/scribble/dist/bin/scribble.js:471:26)
    at Module._compile (node:internal/modules/cjs/loader:1101:14)
    at Object.Module._extensions..js (node:internal/modules/cjs/loader:1153:10)
    at Module.load (node:internal/modules/cjs/loader:981:32)
    at Function.Module._load (node:internal/modules/cjs/loader:822:12)

Support binding return values in old expression

I want to shorten the entry for example this
/// if_succeeds {:msg "balance changed"} old(IERC20(Pool(pool).GetPairForToken(token1, token2, startDate)).balanceOf(address(this))) + old(IERC20(Pool(pool).GetPairForToken(token1, token2, startDate)).balanceOf(address(msg.sender))) == IERC20(Pool(pool).GetPairForToken(token1, token2, startDate)).balanceOf(address(this));
to
/// if_succeeds {:msg "balance changed"} let baseToken := Pool(pool).GetPairForToken(token1, token2, startDate) in old(IERC20(baseToken).balanceOf(address(this))) + old(IERC20(baseToken).balanceOf(address(msg.sender))) == IERC20(baseToken).balanceOf(address(this));

Reducing and reusing the code is very important. For example, I ran into a gas limit when deploying a contract and cannot cover the entire contract with tests

Unable to use `forall` on arrays with elements of used-defined type

Consider the following sample:

contract Test {
    struct MyStruct {
        uint i;
    }

    ///#if_succeeds forall(MyStruct elem in arg) true;
    function example(MyStruct[] calldata arg) public returns (bool) {
        return true;
    }
}

Expected Scribble to be able to handle user-defined types in forall but got crash:

scribble/dist/bin/scribble.js:421
            throw e;
            ^

TypeError: name.split is not a function
    at Object.resolveAny (scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:248:27)
    at makeUserDefinedType (scribble/dist/spec-lang/expr_parser.js:27:39)
    at peg$c286 (scribble/dist/spec-lang/expr_parser.js:541:16)
    at peg$parseUserDefinedType (scribble/dist/spec-lang/expr_parser.js:7890:22)
    at peg$parseSimpleType (scribble/dist/spec-lang/expr_parser.js:7621:38)
    at peg$parseArrayType (scribble/dist/spec-lang/expr_parser.js:7906:14)
    at peg$parseMappingType (scribble/dist/spec-lang/expr_parser.js:8178:18)
    at peg$parsePointerType (scribble/dist/spec-lang/expr_parser.js:8210:14)
    at peg$parseFunctionType (scribble/dist/spec-lang/expr_parser.js:8655:18)
    at peg$parseFor_All (scribble/dist/spec-lang/expr_parser.js:1145:30)

Looking into a stacktrace gives that there is an issue with resolveAny() in solc-typed-ast. However we should clarify if such things expected to work and cover functionality by test samples.

Scribble fails on ternary operator in tuple assignment

function f(bool cond) internal pure returns (uint[2] memory ret) {
  (ret[0], ret[1]) = cond ? (1, 2) : (3, 4);
}

results in

Error: Unexpected rhs in tuple assignment: Conditional#1710
    at getAssignmentComponents (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:41:19)
    at getAssignmentComponents.next (<anonymous>)
    at getAssignments (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:124:20)
    at getAssignments.next (<anonymous>)
    at Object.findAliasedStateVars (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/state_vars.js:272:21)
    at new InstrumentationContext (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/instrumenter/instrumentation_context.js:231:38)
    at Object.<anonymous> (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/bin/scribble.js:582:26)
    at Module._compile (node:internal/modules/cjs/loader:1101:14)
    at Object.Module._extensions..js (node:internal/modules/cjs/loader:1153:10)
    at Module.load (node:internal/modules/cjs/loader:981:32)

Recursive/cyclic imports are not supported

Solidity supports recursive/cyclic imports. We may want to question whether this is good or not, but it is being used.

A.sol:

import "./B.sol";

interface A {
  function a() external returns (B);
}

B.sol:

import "./A.sol";

interface B {
  function a() external returns (A);
}

The error:

/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/util/misc.js:16
    throw new Error(message);
    ^

Error: Order [[SourceUnit#9,SourceUnit#0],[SourceUnit#0,SourceUnit#9]] is not a valid proper order. Topo sort stalled at 1 out of 3
    at assert (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/util/misc.js:16:11)
    at Object.topoSort (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/util/misc.js:186:9)
    at sortUnits (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/bin/scribble.js:331:19)
    at Object.<anonymous> (/Users/alex/.nvm/versions/node/v16.8.0/lib/node_modules/eth-scribble/dist/bin/scribble.js:611:33)
    at Module._compile (node:internal/modules/cjs/loader:1101:14)
    at Object.Module._extensions..js (node:internal/modules/cjs/loader:1153:10)
    at Module.load (node:internal/modules/cjs/loader:981:32)
    at Function.Module._load (node:internal/modules/cjs/loader:822:12)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:79:12)
    at node:internal/main/run_main_module:17:47

Add support for scribble constants in the language

In properties we've written there is often some constant that keeps on repeating. (e.g. number of decimals in a Ray/Wad, number of seconds in a day, etc). It would make code cleaner if we could define Scribble constants similarly to how we can define user helper functions in scribble. I.e. something like:

/// #define SECONDS_PER_DAY: uint  = 60*60*24;
contract Foo {
    uint timestamp;
    
    /// #limit {:msg "no more than a day passed"} block.timestamp - timestamp < SECONDS_PER_DAY;
    function bar() public {}
}

There is still the issue here that constants would be defined per contract, while sometimes we may want to use them from another contract. No clear story for that yet, but the incremental improvement might be worth it.

Implication and calculation old value

I spent a lot of time figuring out what the error is in a similar situation.

pragma solidity >=0.6.0 <0.8.0;
contract Test {
    uint public value;

    function set(uint newValue) external {
        value =  newValue;
    }

    /// if_succeeds {:msg "wrong calculation"} from != address(0) ==> old(Test(from).value()) + old(value) == value;
    function add(address from) external {
        if(from != address(0)) {
	  value =  value + Test(from).value();
	  Test(from).set(block.timestamp);
        }
    }
}

The scribble will generate a similar code, but the fact is that "from" can equal 0 when reading the old value.
_v.old_0 = Test(from).value();

Can you take into account the condition when saving the old value?
Or tell me how to write something like this in a shorter way, there may be more than one old values

/// if_succeeds {:msg "wrong calculation"} from != address(0) ==> old(from != address(0) ? Test(from).value() : 0) + old(value) == value;

Avoid generating ghost state declarations for quantifiers unless quantifiers are used

Currently, ghost state declarations (e.g., for tracking map keys) are generated regardless of whether there is a quantifier that quantifies over the corresponding map. It would be great to only generate the declarations on demand.

Broken instrumentation for overriding public variables

Instrumenting the following code:

abstract contract Base {
    function a(uint x) external view virtual returns (uint);
}

/// #invariant forall (uint k in a) a[k] > 1;
contract Child is Base{
    mapping(uint=> uint) public override a;
}

Produces the following non-compiling code:

/// #invariant forall (uint k in a) a[k] > 1;
contract Child is __scribble_ReentrancyUtils, Base {
...
    uint256_to_uint256.S override a0;
...
    function a(uint256 ARG_0) public returns (uint256 RET_0) {
        vars2 memory _v;
        _v.__scribble_check_invs_at_end = __scribble_out_of_contract;
        __scribble_out_of_contract = false;
        RET_0 = _original_Child_a(ARG_0);
        if (_v.__scribble_check_invs_at_end) __scribble_check_state_invariants();
        __scribble_out_of_contract = _v.__scribble_check_invs_at_end;
    }

There are 3 issues here:

1. The override keyword should be moved from the state variable a0 to the introduced getter a
2. The getter a should have view mutability
3. The getter a shouldn't be instrumented with checks for state vars since its a view function.