v0.5.3

This is a patch release that fixes a bug introduced in 0.5.2 when instrumenting code with map sums or foralls over maps for solidity code older than 0.8.0. The instrumented code included an unchecked block, which made it fail to compile.

v0.5.2

This release brings:

1. Support for Solidity 0.8.4, 0.8.5 and 0.8.6

2. Extends the universal quantification support to work over maps. (i.e. forall (address a in m) ... where m is a map works now)

3. Adds the new builtin unchecked_sum() function, which returns the sum of all values in a numeric map/array. As the name suggests, the sum may overflow, and should be used with carefully.

4. The debug events emitted with --debug-events have been changed to a new simpler format, and now support arrays as well as include more identifiers. (forall iterator vars, path identifiers appearing in if_assigned, etc.).

5. Fixed a bug in debug events where identifiers appearing inside of old(...) expressions had their new value reported erroneously.

6. Cleanup of InstrumentationContext and smaller fixes.

v0.5.1

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

v0.5.0

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)

v0.4.4

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

v0.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

v0.4.2

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 (#36)
2. Spurious syntax error on docstring that contain the 'define' word at the begining of a line (#28)
3. External view function calls not transpiled correctly (#27)

v0.4.1

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.

v0.4.0

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)

v0.3.6

Small patch release including just one fix:

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