Followup on Tutorial 06 - Thinking about properties

I am curious about the way people approached thinking about properties in Tutorial 06.

I personally started thinking about the valid states first.

The way the code is written, it has a lot of unspoken rules being fulfilled through values used in functions other than where they are checked. For example, bid being dependent on the deletion of auction in close, or bid relying on uninitialized auction[id] struct values being 0.

		require(b < auctions[id].prize); // prize can only decrease
		// new winner pays by repaying last winner
		require(transferTo(auctions[id].winner, auctions[id].payment));

Would love to discuss how to approach such non-standard code.

2 Likes

Great discussion IMO.
I’ll start by saying how i think about properties usually.

When a I start a new verification project i also like to start with the valid states and the state transitions. There are a couple reasons for that:

  1. Drawing the state machine (when possible) helps me understand the flow of the system. Breaking down the possible values and restriction of each variable in each state, and the actions (functions) that transit the system from one state to another make me familiar with the code, computations and the physical units that each variable represent.

  2. Valid states and state transitions may seem like trivial rules at times, but in reality the invariants/rules that represent them are fairly strong. Often in order to prove complex rules a set of valid states has to be determined. After all the prover starts every rule by over approximating, which usually requires applying the right restrictions. When proving valid states the complex rule becomes much stronger, since the rule is true not given that we are in a certain state, but it is always true since we proved that a certain set values are is the only set that the system can be in. Besides valid states are fundamentals, so any case where a variable deviates from an expected value can be extremely hazardous to the system as often developers count on the fact that the certain values cannot be reached.

The next step for me, once i understand the system better, is always following the funds. Based on the system, e.g. liquidity pool, loaning system, etc., i try to form properties that will keep the integrity of funds - i try to define properties that prevent creation of funds out of thin air or the opposite - disappearance/lock of funds, solvency - the system should always be in a good position to pay back its users, independency - actions from one user does not effect actions of another user, and so on.

I always try to think as a user of what the system tries to replicate in the real world, however, it’s important to also remember that you need to take care of the house. If the system loses, then the consequences are far worse - in either the short or long term not just one user will lose, but all of them, which will cause a collapse.

this is the way i see things, but obviously it is only my point of view and i still have a lot to learn myself.
I’d like to hear how others approaching this both from within and from outside the company.

1 Like