runtimeverification / runtimeverification/kontrol
CSE: manually specified preconditions
Open
@palinatolmach is already working on this.
Since Jun 27, 2024.
cse
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
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`
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.