Bot releases are visible (Hide)
Published by cd1m0 over 3 years ago
This release brings:
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
Published by cd1m0 over 3 years ago
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)
Published by cd1m0 over 3 years ago
This patch fixes a bug in the type string grammar introduced by 0.4.3.
Published by cd1m0 over 3 years ago
This release brings:
Published by cd1m0 over 3 years ago
This release includes several one feature and several bug fixes.
Feature:
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:
Published by cd1m0 over 3 years ago
This version brings support for Solidity versions 0.8.0-0.8.3. Namely:
Published by cd1m0 over 3 years ago
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)
Published by cd1m0 over 3 years ago
Small patch release including just one fix:
Don't emit empty invariant checkers on contracts with user functions
Published by cd1m0 over 3 years ago
This version adds:
InstrumentationMetadata
object.--property-map-file
CLI option was removed, in favour of --instrumentation-metadata-file
(which contains the property map as well as other metadata).Published by cd1m0 over 3 years ago
This release includes both new language features as well as bug fixes.
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 {
...
}
}
Published by cd1m0 almost 4 years ago
This release has 2 small fixes: