[More Detail] [Collapse All]
Feature: Send pattern of sending Ether


Although the most intuitive method of sending Ether, as a result of
an effect, is a direct send call, this is not recommended as it
introduces a potential security risk.
features/050-ether-balance/200-send-pattern.feature
- Background: Create SendContract and define setups
link
features/050-ether-balance/200-send-pattern.feature:9
Given I create initial sbuilder context with:
Directory
solidity SendContract
setup setup1
And a file named "solidity/SendContract.sol" with:
pragma solidity ^0.3.5;

contract SendContract {
    address richest;
    uint mostSent;

    function SendContract()  {
        richest = msg.sender;
        mostSent = msg.value;
    }

    function becomeRichest() returns (bool) {
        if (msg.value > mostSent) {
            // Check if call succeeds to prevent an attacker
            // from trapping the previous person's funds in
            // this contract through a callstack attack
            if (!richest.send(msg.value)) {
                throw;
            }
            richest = msg.sender;
            mostSent = msg.value;
            return true;
        } else {
            return false;
        }
    }

}
- Scenario: Create contract, mine and send ether
link


See the comments in the setup for explanation


State space extract:
features/050-ether-balance/200-send-pattern.feature:50
# eth_accounts@1={[address |-> "acc1", codeHash |-> Nil, balance |-> 0]}
# eth_storageRoot@1={[address |-> "acc1"]}
# eth_accounts@2={[address |-> "acc1", codeHash |-> Nil, balance |-> 3]}
# eth_storageRoot@2={[address |-> "acc1"]}
# eth_accounts@3={ [address |-> "acc1", codeHash |-> Nil, balance |-> 3],
#                  [address |-> "acc2", codeHash |-> Nil, balance |-> 0] }
# eth_storageRoot@3={[address |-> "acc1"], [address |-> "acc2"]}
# eth_accounts@4={ [address |-> "acc1", codeHash |-> Nil, balance |-> 3],
#                  [address |-> "acc2", codeHash |-> Nil, balance |-> 3] }
# eth_storageRoot@4={[address |-> "acc1"], [address |-> "acc2"]}
# eth_accounts@5={ [address |-> "acc1", codeHash |-> Nil, balance |-> 2],
#                  [address |-> "acc2", codeHash |-> Nil, balance |-> 3],
#                  [address |-> "acc3", codeHash |-> "SendContract", balance |-> 1] }
# eth_storageRoot@5={ [address |-> "acc1"],  [address |-> "acc2"],
#                     [address |-> "acc3", richest |-> "acc1", mostSent |-> 1] }
# eth_accounts@6={ [address |-> "acc1", codeHash |-> Nil, balance |-> 5],
#                  [address |-> "acc2", codeHash |-> Nil, balance |-> 0],
#                  [address |-> "acc3", codeHash |-> "SendContract", balance |-> 1] }
# eth_storageRoot@6={ [address |-> "acc1"],
#                     [address |-> "acc2"],
#                     [address |-> "acc3", richest |-> "acc2", mostSent |-> 3] }
# eth_accounts@7={ [address |-> "acc1", codeHash |-> Nil, balance |-> 4],
#                  [address |-> "acc2", codeHash |-> Nil, balance |-> 0],
#                  [address |-> "acc3", codeHash |-> "SendContract", balance |-> 2] }
# eth_storageRoot@7={ [address |-> "acc1"],
#                     [address |-> "acc2"],
#                     [address |-> "acc3", richest |-> "acc2", mostSent |-> 3] }
And a file named "cnf/setup1.yaml" with:
 - domain-extension:


     - domain: eth_address
       values:
          - acc1
          - acc2
          - acc3
          - acc4

       # Ether value range
     - domain: eth_value
       type: Int
    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:

          # step 1: Create accounts acc1 with 3 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 1
                value: 3

          # step 3: Create accounts acc2 with 3 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 2
                value: 3

          # step 5: Acc1 creates contract, and becomes richest (msg.value 1)

        - interface: SendContract()
          bindExact: true
          input:
              _default: 1
              value: 1
              sender: 1

         # steup 6: Acc becomes richest because the msg.value 3
         # exceeds previous mostSent (1). Old richest receives
         # msg.value. 
         #
         # Balances after this step:
         # - acc1 = 2 + 3 = 5
         # - acc2 = 3 - 3 = 0
         # - acc3 = 1 (no change, because msg.value was transfferred to acc1)


        - interface: SendContract(becomeRichest)
          bindExact: true
          input:
              _default: 1
              value: 3
              sender: 2
              recipient: 3

         #
         # step 7: 'acc1' sends one unit to 'acc3' when calling
         # 'becomeRichest'. This, however, does not make 'acc1'
         # the richest. Acc3 receives the msg.value (1 unit) of call.

        - interface: SendContract(becomeRichest)
          bindExact: true
          input:
              _default: 1
              value: 1
              sender: 1
              recipient: 3
Given I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
2 eth_accounts acc1 balance 3
4 eth_accounts acc2 balance 3
5 eth_accounts acc1 balance 2
5 eth_accounts acc2 balance 3
5 eth_accounts acc3 balance 1
5 eth_storageRoot acc3 richest acc1
5 eth_storageRoot acc3 mostSent 1
6 eth_accounts acc1 balance 5
6 eth_accounts acc2 balance 0
6 eth_accounts acc3 balance 1
6 eth_storageRoot acc3 richest acc2
6 eth_storageRoot acc3 mostSent 3
7 eth_accounts acc1 balance 4
7 eth_accounts acc2 balance 0
7 eth_accounts acc3 balance 2
7 eth_storageRoot acc3 richest acc2
7 eth_storageRoot acc3 mostSent 3