Contract design by contract -> correctness and maximum gas consumption

This question is a general design question that regards contract correctness and the functions I list here are just examples.

As I develop on Ethereum, it becomes aparent to me that it might be relatively easy to mal-design a contract that deadlocks itself because necessary key functions may suddenly become not callable anymore because their excecution suddenly exceeds the gas limit.

That leads me to the likely difficult question:

How can I assert that a specific function never uses more than a certain ammount of gas? This seems to be a crucial necessity for contract correctness.

For example

function unbound() returns (uint256) {
uint256 total = 0;
for (uint i=0; i < users.length; i++) {
total+= users[i].value;
}
}


calling this function has undeterministic gas cost and could easily at some point become uncallable. Of course in such a simple example like this it's easy to redesign and calculate this total not in a loop but by other means. But it's not always possible to avoid loops. The question is, how do you write correct functions in that case?

For example, the system might be designed such that there are never more than 6 users, in which case the loop is bound and the execution cost deterministic, so if I have:

function bound() returns (uint256) {
uint256 total = 0;
assert(users.length < 6);
for (uint i=0; i < users.length; i++) {
total+= users[i].value;
}
}


This function uses a loop but has a deterministic upper bound for gas consumption.

A: How can I calculate the maximum amount of gas calling this function will consume?

B: How can I communicate this maximum to clients of the function?

Can I somehow do something like this:

function bound() returns (uint256) {
uint256 total = 0;
for (uint i=0; i < users.length; i++) {
total+= users[i].value;
}
assert(gasConsumend < 1234);
}


?

We're writing contracts after all, and pre- and post- conditions are an integral part of design by contract. We can write preconditions with require() and postconditions with assert() - but for correctness on ethereum it seems also necessary to assert a maximum gas consumption. How?

I fear that there may not be a fool-proof answer to this, for the simple reason that over the course of forks, gas costs can change for certain op codes (as was done to stop spam attacks some time ago).

Due to the above, a hardcoded gas check may no longer be valid in the long run.

When dealing with a loop function, requiring that your input is under a certain length is a feasible option. Moreover, if you know the input, you can use the eth_estimateGas call to perform a "dry run" of the transaction and estimate the gas used, which is how MyEtherWallet, Metamask, etc. sometimes auto fill the max gas field.

Note that gas estimation is not perfect, especially for transactions that change depending on external factors (such as timestamps, or the blockhash being odd/even).

Unfortunately, limiting array lengths is often not feasible. If your array must exceed a size where looping over it in one tx is not possible, an alternate is to rebuild your function so that it accepts a list of indices as parameters, and only access those indices in that transaction. This can allow you to update array contents/perform some operation piecemeal over the course of a few transactions.

For instance, a sum variable could be declared at a contract-level, and a 1 million element array could be summed over the course of 5000 transactions that add up 20 elements each.

At the end, I suspect that careful contract writing is the key to dealing with avoiding the situations, and good wallet/frontend design can communicate to end users when an action will exceed the block gas limit, and ask them to reduce their input size.

• but eth_estimateGas is a feature of geth, not a feature of the EVM that's somehow accessible by contracts, right? It would seem that if gas cost can suddenly change, this would mean that there is not a single contract that can ensure its correctness (in the sense that it will remain being executable). This seems to be an extreme design-flaw of a plattform that's supposed to provide security and correctness by 'contracts'... – user1282931 Aug 22 '18 at 10:41
• gas estimation should be used by wallets/front end clients to prevent users from making blatantly incorrect transactions. Additionally, while gas costs can change, it is exceedingly rare for that to happen, and a situation where it jumps by such a huge amount that it renders normal contracts broken would likely swiftly be met with a community fork. But yes, there is probably no excellent way to ensure this at an evm level – Raghav Sood Aug 22 '18 at 10:43