Thank you for your thoughtful response! Your suggestion for the example illustrating the first BALANCE problem is to place a self call in the operation queue after every transfer, that asserts that BALANCE >= Min_Balance. At this point, BALANCE has been updated since the transfer has been executed, so eventually the assert will correctly fail. This seems like a nice solution for the example I described but I think we can make a slight modification to the example so that it is impossible to use BALANCE correctly.
In the current version of the scenario, the desired logic is as follows:
If BALANCE - Amt_requested <= Min_balance:
Fail;
Else:
Send(Amt_requested)
What if instead, we desire something slightly more complicated than simply failing if BALANCE is too low. For example:
If BALANCE - amt_requested <= Min_balance:
Request a bank for amt_requested (so that contract can execute transfer on a second request without BALANCE being too low)
Else:
Send(amt_requested)
In this situation, we cannot simply add an assertion to the operation queue as you do in the previous example. In our view, we should be able to reason, in code, about the state of the contract’s BALANCE at the time of an operation’s execution. To solve this problem, we propose a solution in Proposal for Changes to Balance in which we maintain a variable reflecting promised Outgoing funds in the queue so that we can correctly calculate a new variable, EffectiveBalance.
