Provably correct contracts and atomic operations

LarsPensjoLarsPensjo SwedenMember Posts: 35
Wouldn't it be highly desirable to be able to prove correctness of contracts? If you do something wrong, you can end up with resources stuck for ever in limbo.

To be able to prove correctness, it is usually easier if the programming language is based on a functional language, with not side effects. There is quite a lot of research done on this. A contract should be a function that takes a state and a message as input, and returns a new state as output. If successfully executed (not aborted), the resulting state is stored. This could easily be scaled to bigger systems, where you can call sub contracts. In the end, the success of the top level contract simply depends on what is returned at that level. Either every part of the algorithm succeeds, or nothing succeeds.

Being free of side effects is a desirable property. It means the top level contract can easily discard changes of lower level contracts. It also means atomic operations are easier to implement. E.g. if you run out of Gas, everything should fail. However, to be able to properly support this, the underlying low level language has to support it.

This idea started at http://www.reddit.com/r/ethereum/comments/2bsg7o/difficult_to_develop_contracts/ , but I thought I should bring it here for discussion. I know there is LLL, but the implementation would require bigger changes reaching outside the scope of LLL.

Comments

  • LarsPensjoLarsPensjo SwedenMember Posts: 35
    I had a look at the LLL language, but I see some problems:

    1. The syntax is difficult, based on the old Lisp language. There are more recent and readable syntax that could be used.
    2. The language supports side effects, which makes it harder to implement provable correct algorithms.
    3. Sending a message to another contract may have side effects. This is not because of LLL, but rather how the Ethereum protocol is defined.
  • StephanTualStephanTual London, EnglandMember, Moderator Posts: 1,282 mod
    I'm not sure I see a question in your post, but I'll give it a shot :)

    In a nutshell, today, if a contract calls another contract, and the second contract 'runs out of gas', only the last contract rolls back. This is implemented by simply 'backing up' the state before execution and reverting to that backup if an 'out of gas' situation occurs.

    This does indeed mean that a conscious effort needs to take place when coding 'higher level' contracts (callers) to insure that they don't end up in an invalid state leading to further errors down the line.
  • LarsPensjoLarsPensjo SwedenMember Posts: 35
    Thanks for the clarification, now I understand a little more!

    Isn't this a possibly serious problem? I am thinking about complex situations, where a master contract calls several other sub contracts. That is, real world contracts, not simple demonstrations.

    Use case:
    1. Contract A successfully calls contract B, with a state change as side effect.
    2. Contract A next calls contract C, which runs out of gas. Or contract A itself runs of out gas.

    The state of contract A is now inconsistent or invalid, and should not be allowed to happen. There are a workarounds for this:

    1. Never call more than one sub contract. That would be an unfortunate limitation, not encouraging "libraries" of common contracts.
    2. Make sure all contracts have a "revert" command. I am not sure it is feasible. It would cost gas to revert.
    3. Accept that there can be an inconsistent state, and design the master contracts accordingly. This can make contract design complicated.

    My proposal to solve this is a change on how state changes are managed. All contracts take a state as input, and return a new state as output. When a contract calls another contract, only one state change (which can be empty) is returned at the top level. That would help consistency. As there would be no side effects, it would also help make provable correct contracts.

    I understand this is probably a change not compatible with the current design, and maybe too late. Or maybe there already is some support for this that I didn't know about.
  • mimarobmimarob Member Posts: 33
    I think let people experiment and screw up!

    Perhaps one could prove that a contract is terminally stuck and can then be purged?
  • rabbitrabbit Member Posts: 15 ✭✭
    You could maybe avoid this by having only one contract responsible for managing state. All other contracts would be stateless where the input carries all the state needed for the contract to function then return the result without storage. This is arguably a more reusable design. If you were to restrict write operations to the base contract but allow read operations from any relying party it would be possible for third parties to create their own adapters to satisfy arbitrary format requirements.
Sign In or Register to comment.