scribble

This release brings:

1. Quantification over numeric ranges/arrays:

   The language now has a forall construct that allows to compute a universally quantified expression over numeric ranges/indices in an array. For example:

forall (uint x in 5...10) x >0

Is a predicate that evalutes to true IFF for all values in the range from 5 (inclusive) to 10 (exclusive), its true that they are positive. (which is obviously true). Since iterating over arrays is a common use-case for this construct we have the following syntactic shortcut:

forall (uint i in arr) arr[i] > 0

The above expression is equivalent to the following form:

forall (uint i in 0...arr.length) arr[i] > 0

2. Fix a bug which produces invalid code when instrumenting a constructor in Solidity 0.8.x

NOTE: THIS IS A BREAKING RELEASE

In this release we change the annotation syntax to support a # prefix before annotation keywords invariant/if_succeeds/if_updated/define.

So for example if_succeeds x > 0 should now be #if_succeeds x > 0.
The old-style annotations without a # is deprecated, but will still be supported. You will get warning on stderr for each instance of an annotation without a #.

This change makes it easier to discern annotations from other text in a docstrings, for other tools (such as IDE plugins)

This patch fixes a bug in the type string grammar introduced by 0.4.3.

This release brings:

• Cleanup: Removed the type string parser, and related logic for getting a structured type of an arbitrary Expression ASTNode. All relevant logic was moved to solc-typed-ast
• bump solc-typed-ast to version 5.0.1
• Fix for issue #33
• Fix for issue #39

This release includes several one feature and several bug fixes.
Feature:

1. if_succeds annotations are now allowed on contract definitions. They are automatically applied to all public/view non-pure functions in this contract, and all inheriting contracts.

Bug fixes:

1. Exception thrown when calling annotated functions from another annotation (https://github.com/ConsenSys/scribble/issues/36)
2. Spurious syntax error on docstring that contain the 'define' word at the begining of a line (https://github.com/ConsenSys/scribble/issues/28)
3. External view function calls not transpiled correctly (https://github.com/ConsenSys/scribble/issues/27)

This version brings support for Solidity versions 0.8.0-0.8.3. Namely:

1. Add support for unchecked blocks
2. Ensure that when wrapping unchecked state variable updates, an updated block is emitted in the wrapper
3. Make sure that all Scribble arithmetic is unchecked. When designing scribble we aim to minimize the set of possible exceptions coming from Scribble instrumentation. The tradeoff here is that users need to think more carefully when writing arithmetic in Scribble as its unchecked.

New features:

-if_updated annotation type allows for the instrumentation of state variables
-if_assigned annotation type allows for the fine-grained instrumentation of state variables (experimental)

Small patch release including just one fix:

Don't emit empty invariant checkers on contracts with user functions

This version adds:

• support for a "instrumented source"-to-"original source" map
• unifies all instrumentation metadata (the property map and the source-to-source map) into a single InstrumentationMetadata object.
• the --property-map-file CLI option was removed, in favour of --instrumentation-metadata-file (which contains the property map as well as other metadata).

This release includes both new language features as well as bug fixes.

New Language Features

Support for user-defined functions (https://github.com/ConsenSys/scribble/pull/15). These are loop-free functions defined at the contract level (in the contract doc strings) that are available for all properties in that contract to refer to.

For example consider a toy 'wallet' contract, that keeps internal track of the balances of several tokens per user, in its _balances field:

contract Wallet {
    mapping(address => address => uint) _balances;
    
    function transferFrom(address from, address to, address token, uint amount) public {
       ...
    }
}

One might want to check that after transferFrom, the internal balance equals the 'real' balance in each token. To save on writing, we can add define our own function for getting the real balance and use it as follows:

/// define realBalance(address user, address token) uint = IERC20(token).balanceOf(user);
contract Wallet {
    mapping(address => address => uint) _balances;
    
    /// if_succeeds {:msg "Internal balance matches real balance"}
    ///        realBalance(from, token) == _balances[from][token] &&
    ///        realBalance(to, token) == _balances[to][token];
    function transfer(address from, address to, address token, uint amount) public {
       ...
    }
}

Bug fixes

• Add logic to handle the various flavours of import statements when re-writing in flat mode https://github.com/ConsenSys/scribble/pull/14
• Fix various edge-cases of shadowing when instrumenting using unique identifiers https://github.com/ConsenSys/scribble/pull/13
• Bump node-js in CI pipeline to 12 https://github.com/ConsenSys/scribble/pull/9

This release has 2 small fixes:

• disallow if_succeeds annotations on contracts and invariant annotations on functions
• fix buggy behavior for identifier paths in user-defined type names in flat mode