2vyper
2vyper copied to clipboard
A static verifer for Ethereum Smart Contracts written in Vyper
If an event is used as a trigger in the specification function `forall`, the `forall` expression cannot be verified by Carbon. An example for such an `forall` is in the...
**Issue by [robinsierra](https://github.com/robinsierra)** _Friday Feb 07, 2020 at 07:47 GMT_ _Originally opened as https://github.com/robinsierra/2vyper/issues/14_ ---- 2vyper currently doesn't choose triggers when performing a quantified resource operation, e.g. ```foreach({a: address}, offer[token...
**Issue by [robinsierra](https://github.com/robinsierra)** _Thursday Feb 06, 2020 at 16:04 GMT_ _Originally opened as https://github.com/robinsierra/2vyper/issues/11_ ---- 2vyper currently does not support `slice`. The reason is a bug in Vyper, see https://github.com/vyperlang/vyper/issues/1467.
**Issue by [robinsierra](https://github.com/robinsierra)** _Thursday Feb 06, 2020 at 15:54 GMT_ _Originally opened as https://github.com/robinsierra/2vyper/issues/8_ ---- At the moment equality of maps does not take into account type assumptions, i.e., two...
**Issue by [robinsierra](https://github.com/robinsierra)** _Thursday Feb 06, 2020 at 15:51 GMT_ _Originally opened as https://github.com/robinsierra/2vyper/issues/7_ ---- Currently, 2vyper translates equality of two maps by using a pre-defined Viper domain function that...