1,000 Ether bounty on a proven-correct wallet (with 17 instructions, just a beginning)

In the EDCON conference in Paris, I will talk about proving smart contracts correct. There I will release a bounty program. For everybody else who are not attending the conference, I’m putting a note here.

In the talk, I will talk about proving smart contracts against specifications. As a demonstration, I set up a proven-correct wallet and put 1,000 Ether on it. In the talk, I’ll ask the audience to break it and take funds from it. The wallet is deployed at 0x0fcc015903e7e51a947ed7276a21d37a11b29e61.

It is a really simple program that just checks the caller. However, in the past, when I set up a bounty to prove “False” in Coq, somebody actually did it. So I think I should start from the obvious.

I proved two theorems about this wallet. When any account except the special one calls the wallet, the wallet just returns (or out-of-gas happens).

lemma whole_program_invalid_caller:
"triple {OutOfGas} (⟨unat bn ≥ 2463000 ∧ ucast c ≠ w⟩ **
            block_number_pred bn **
            stack_height 0 **
            program_counter 0 ** caller c **
            storage (word_rcat [0]) w **
            gas_pred g **
            continuing
           )
           whole_concrete_program
           (block_number_pred bn **
            stack_height 0 **
            program_counter 8 ** caller c **
            storage (word_rcat [0]) w **
            gas_pred
               (g + (- Gsload (unat bn) - 2)
                - 2 * Gverylow - Gverylow - Ghigh) **
            not_continuing ** action (ContractReturn []))"

When the special address calls the wallet, the wallet gives all its balance to the caller (or out-of-gas happens).

lemma check_pass_whole_concrete:
  "triple {OutOfGas} (⟨unat bn ≥ 2463000 ⟩ **
                       block_number_pred bn **
                       stack_height 0 **
                       program_counter 0 ** caller c **
                       storage (word_rcat [0]) (ucast c) **
                       gas_pred g **
                       continuing **
                       this_account t **
                       balance t b **
                       memory_usage 0
                      )
                      whole_concrete_program
                      (memory_usage 0 **
                       stack_topmost 0 [] **
                       program_counter 22 **
                       this_account t **
                       balance t 0 **
                       gas_any **
                       not_continuing **
                       action (ContractCall ⦇
                         callarg_gas = word_rcat [(8 :: byte), 0]
                       , callarg_code = c
                       , callarg_recipient = c
                       , callarg_value = b
                       , callarg_data = []
                       , callarg_output_begin = word_rcat [0]
                       , callarg_output_size = word_rcat [0] ⦈) **
                       block_number_pred bn **
                       caller c **
                       storage (word_rcat [0]) (ucast c)
                      )"

The proofs of these theorems are available on GitHub.

I schedule this post to appear at 1pm on Friday, by which time my talk should have finished. I might be, and might not be, able to post this on reddit.