search

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
48 stars 5 forks source link

CSE: manually specified preconditions #650

Open palinatolmach opened 3 months ago

palinatolmach commented 3 months ago

We should add the ability to manually specify range constraints (e.g., that all values representing times are less than 2 ^Int 40) to remove various chops — this would require extending the natspec annotation mechanism.

The annotations should support at least basic boolean operations on variables including input and storage ones and having different types (e.g., mapping elements should be translated to lookups).

One example of preconditions we want to support is

`(_sharesAmount * totalPooledEther) / totalPooledEther == _sharesAmount`
PetarMax commented 3 months ago

Slightly more generally, we should be able to give the user the ability to specify arbitrary pre-conditions.