Open DavePearce opened 2 years ago
variant unchanged(&int p)
where old(*p) == *p
map<address,uint256> balances = ...
bool lock = false
public method get_balance(address sender) -> uint256
unchanged(&balances):
...
public method deposit(address sender):
sender.transfer(123) <-
public method main()
always lock ==> unchanged(&balances)
eventually ended
The keywords are from temporal logic. These are the transitive and reflexive closures of ensures
.
The rough idea is to use a keyword always
which reasons over the history. The intention is that this is a transitive constraint and, hence, we can use it to reason about multiple invocations of a method. Some notes:
always
clauses. For the example above, its quite easy as we can just imagine it holds after multiple calls to main()
. But, what about a method which accepts one or more parameters? Or is a function
rather than a method
?Another aspect of this idea is that we can use it for authorisation as well. For example, we can say something like this:
"unless
msg::sender
equals a particular account, this variable cannot be changed".
To verify reentrant computation relies on a two state predicate which summarises the effect making one (or more) reentrant calls into a method could have on local state. For example, consider this:
The necessary two-state predicate is actually
old(state) < state
forinc()
since we can callinc()
arbitrarily many times from external code. What we need is a way to either infer such a specification or (perhaps easier) to check such a specification is already transitive.Syntax
There are various ways we could try to encode the logic we need. One approach might be to impose constraints on how global data could be modified. For example:
Actually the
varies
clauses is perhaps similar or identical to Liskov and Wing'sconstraint
clause.References