chriseth/0 README.md

Nice. But what does this line - !msg.sender.call.value(amount)() do?

@hiddentao It's like a send with no gas limit.

@chriseth Well done! 👍

This is nice. Since the invariant has to be enforced on every method, this approach actually produces contracts with very high integrity. I have two comments.

• Fund.sol, line 5 should check <= instead of <. It's OK in the Why code.
• Instead of rejecting incoming Ether, you can change the conditions:

32: ensures { result.success = true ->
      (invariantFun this) <= (invariantFun result.new_state) }
42: ensures { invariantFun (old this) <= invariantFun result }

if you don't mind more Ether in the contract.

@pirapira thank you, these are nice suggestions! I was wondering how to generalize invariantFun (old this) <= invariantFun result, and I think a more relaxed notion of a transition condition (like the one you gave) could also be used, which has access to the pre- and to the post-state. It could be dangerous because it has to be a transitive condition, but perhaps we could add another VC that actually asserts the transitivity.

First of all awesome project. I'm currently working in a startup that issues stocks on ethereum and also underway academic research on formal verification.

I'm trying to reproduce what you're done here with online solidity compiler https://ethereum.github.io/browser-solidity/ it has a formal verification tab that generates code with prompt to test that on http://why3.lri.fr/try/ but the code generated differs from your's.

The latest build is showing the following code that fails on try on the line 30 starting with invariant word. Can you please explain what happened?

module UInt256
    use import mach.int.Unsigned
    type uint256
    constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
    clone export mach.int.Unsigned with
        type t = uint256,
        constant max = max_uint256
end

module Contract_Fund
    use import int.Int
    use import ref.Ref
    use import map.Map
    use import array.Array
    use import int.ComputerDivision
    use import mach.int.Unsigned
    use import UInt256
    exception Revert
    exception Return
    type state = {
        mutable _shares: uint256
    }
    type account = {
        mutable balance: uint256;
        storage: state
    }
    val external_call (this: account): bool
        ensures { result = false -> this = (old this) }
        writes { this }
        invariant { to_int this.storage._shares - to_int this.balance }
    let rec _withdraw (this: account) (arg_amount: uint256):
            ()
        invariant { to_int this.storage._shares - to_int this.balance }
        writes { this }
        =
        let prestate = {balance = this.balance; storage = {_shares = this.storage._shares}} in 
        let _amount = ref arg_amount in
        try
        begin
            if (!(_amount) < this.storage._shares) then
            begin
                this.storage._shares <- (this.storage._shares - !(_amount));
                if (not (
                    let amount = 0 in let amount = !(_amount) in 
                    if amount <= this.balance then
                        let balance_precall = this.balance in
                        begin
                            this.balance <- this.balance - amount;
                            if not (external_call this) then begin this.balance = balance_precall; false end else true
                        end
                    else false
                )) then
                begin
                    raise Revert
                end
            end
        end;
        raise Return
        with Return -> () |
             Revert -> this.balance <- prestate.balance; this.storage._shares <- prestate.storage._shares; ()
    end
end