We need to have a more principled approach to generate arithmetic bounds for storage variables.
Right now:
inRange assertions in preconditions might generate duplicate bounds assertions as Enrich already adds some go theminRange assertion can be implicit and generated automatically using type information, though we need to be careful to with the semantics of this. For example for a storage variable uint128 x , writing the following update
x => (x + 1234) + 5678
will implicitly add the precondition inRange(uint128, (x + 1234) + 5678) which implies that every subexpression never goes out of uint128 bound.
Issue #109 describes how an inferring-bounds analysis can be performed.
We need to have a more principled approach to generate arithmetic bounds for storage variables.
Right now:
inRangeassertions in preconditions might generate duplicate bounds assertions as Enrich already adds some go theminRangeassertion can be implicit and generated automatically using type information, though we need to be careful to with the semantics of this. For example for a storage variableuint128 x, writing the following updatex => (x + 1234) + 5678will implicitly add the precondition
inRange(uint128, (x + 1234) + 5678)which implies that every subexpression never goes out ofuint128bound.Issue #109 describes how an inferring-bounds analysis can be performed.