[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.4.4;

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:

      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] }
features/050-ether-balance/200-send-pattern.feature:50
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: 'acc2' becomes richest because the msg.value 3
         # exceeds previous mostSent (1 of acc1). Old richest
         # (acc1) 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.

         # Balances after this step:
         # - acc1 = 5 -1  = 4
         # - acc2 = 0 (no change)
         # - acc3 = 1 +1  = 2

        - 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