Exercises: contracts

Each problem comes from the exercise at the end of a gallery example. Try it in the example’s notebook first, then open the solution. Every solution is run by the documentation build, so its code is known to work.

1. The weakest precondition of a withdrawal

From Floyd and Hoare: proving a withdrawal correct with assertions (1967-1969). Compute the weakest precondition of the withdrawal for balance >= 0. What does the require contribute, and what changes without it?

Solution

>>> withdraw = '''
... require(amount <= balance)
... balance = balance - amount
... received = received + amount
... '''
>>> wp = bk.contracts.weakest_precondition(withdraw, "balance >= 0")
>>> bk.contracts.to_source(wp)
'not amount <= balance or balance - amount >= 0'
>>> unguarded = withdraw.replace("require(amount <= balance)", "")
>>> bk.contracts.to_source(bk.contracts.weakest_precondition(unguarded, "balance >= 0"))
'balance - amount >= 0'

Pushing balance >= 0 back through the assignment gives balance - amount >= 0. The require adds not amount <= balance or ...: a call that reverts proves nothing, so the condition only has to hold when the check passes, and then it always does. The weakest precondition is therefore true for every input. Without the require it is balance - amount >= 0 itself, an obligation every caller must meet.

2. Oyente with three recipients

From Oyente: symbolic execution finds the BeautyChain overflow in bytecode (2016). With three recipients the overflowing value is not \(2^{255}\). Find one, and let the solver confirm it.

Solution

We need 3 * value to wrap around to a small number: take \(\lceil 2^{256}/3 \rceil\), whose triple is \(2^{256} + 2 \equiv 2\).

>>> value = (2**256 + 2) // 3
>>> 3 * value % 2**256
2
>>> program = bk.vm.batch_transfer(1, [2, 3, 4])
>>> result = bk.contracts.symbolic_bytecode(program, arguments=("value",))
>>> [stop] = [path for path in result.paths if path.outcome == "stop"]
>>> bug = bk.contracts.expression("slot2 > s1 + s2", **stop.state)
>>> witness = bk.contracts.solve((*stop.conditions, bug), modulus=2**256,
...                              candidates={"value": [1, value], "s1": [0, 2], "s2": [0]})
>>> witness["value"] == value, witness["s1"]
(True, 2)

A sender holding 2 tokens pays 2 and gives each of three recipients about \(3.9 \times 10^{76}\). The boundary values miss it because it is neither a constant of the program nor half the word size; an SMT solver such as Z3 finds it by reasoning about the multiplication instead.

3. Approving zero first

From ERC-20 tokens and the approve/transferFrom race (2015). Alice approves 0, then 50, instead of overwriting 100 with 50. Can Bob still take 150?

Solution

>>> world = bk.contracts.World()
>>> token = world.deploy("alice", bk.contracts.ERC20, 1_000)
>>> _ = world.transact("alice", token, "approve", "bob", 100)
>>> _ = world.transact("bob", token, "transfer_from", "alice", "bob", 100)  # Front-run.
>>> _ = world.transact("alice", token, "approve", "bob", 0)
>>> _ = world.transact("alice", token, "approve", "bob", 50)
>>> _ = world.transact("bob", token, "transfer_from", "alice", "bob", 50)
>>> world.view(token, "balance_of", "bob")
150

Yes. Approving zero first only helps if Alice looks between her two transactions: after the approve(0) is mined she can see that the 100 was already spent and decide not to grant 50 more. A decrease_allowance makes that check in the contract, in the same transaction.

4. GovernMental under today’s gas limit

From GovernMental: an unbounded loop meets the block gas limit (2016). With a 30 million gas limit, how many creditors freeze the payout?

Solution

The payout’s gas is linear in the number of creditors: measure two small games for the slope and intercept, then solve for the limit.

>>> def payout_gas(creditors):
...     world = bk.contracts.World()
...     game = world.deploy("operator", bk.contracts.GovernMental)
...     for index in range(creditors):
...         world.fund(f"p{index}", 1)
...         _ = world.transact(f"p{index}", game, "invest", value=1)
...     world.advance(seconds=43_200)
...     return world.transact("anyone", game, "payout").gas_used
>>> slope = (payout_gas(20) - payout_gas(10)) // 10
>>> intercept = payout_gas(10) - 10 * slope
>>> slope, intercept
(5000, 31500)
>>> (30_000_000 - intercept) // slope + 1
5994

Each creditor costs one storage write (5,000 gas in this model) and the rest of the payout about 31,500, so 5,994 creditors are enough. A bigger block only moves the threshold; the loop is still unbounded.

5. Excluding players who do not reveal

From Commit-reveal schemes and on-chain randomness (2016). If a player who does not reveal is excluded from the draw and loses the stake, what is Dave’s best strategy as the last revealer?

Solution

Withholding now guarantees that Dave loses, while revealing wins with probability 1/4, so he always reveals.

>>> import random
>>> rng = random.Random(1)
>>> def dave_wins(strategic):
...     others = [rng.randrange(2**64) for _ in range(3)]
...     mine = rng.randrange(2**64)
...     revealed = others[0] ^ others[1] ^ others[2]
...     if strategic and (revealed ^ mine) % 4 != 3:
...         return False  # Withheld: excluded from the draw.
...     return (revealed ^ mine) % 4 == 3
>>> games = 20_000
>>> round(sum(dave_wins(True) for _ in range(games)) / games, 2)
0.25

Withholding can no longer win Dave the pot. It can still change the winner among the others, so a last revealer colluding with another player keeps an advantage; that is why penalties are set above what such a deviation could gain.

6. A storage collision on the admin slot

From Upgradeable proxies and storage collisions (2018). Behind the naive proxy, an implementation’s second field shares slot 1 with the proxy’s admin. What can Mallory do with an open store?

Solution

>>> class Open(bk.contracts.Contract):
...     layout = ("unused", "value")
...     def store(self, value):
...         self.write("value", value)
>>> class Drain(bk.contracts.Contract):
...     layout = ()
...     def take(self, to):
...         self.call(to, None, value=self.ether_balance())
>>> world = bk.contracts.World()
>>> proxy = world.deploy("dev", bk.contracts.NaiveProxy, world.deploy("dev", Open))
>>> world.fund(proxy, 1_000)
>>> world.transact("mallory", proxy, "store", "mallory").success
True
>>> world.read(proxy, "admin")
'mallory'
>>> world.transact("mallory", proxy, "upgrade_to", world.deploy("mallory", Drain)).success
True
>>> _ = world.transact("mallory", proxy, "take", "mallory")
>>> world.balance("mallory")
1000

Writing value writes the proxy’s admin, so Mallory makes herself admin, upgrades to code of her choosing, and takes everything the proxy holds. A lost implementation pointer only bricks the contract; a lost admin hands it over.