[More Detail] [Collapse All]
Feature: Datatypes
features/010-solidity/010-data-types.feature
- Background: Define contract with functions
link
features/010-solidity/010-data-types.feature:3
Given I create initial sbuilder context with:
Directory
solidity Demo1
setup setup1
And a file named "solidity/Demo1.sol" with:
pragma solidity >0.4.0;

contract Demo1 {

    address richest;
    mapping (address => uint) pendingWithdrawals;

    function Demo1() payable {
          pendingWithdrawals[msg.sender] = msg.value;
          richest = msg.sender;
    }

    function becomeRichest() payable returns (bool) {
        pendingWithdrawals[richest] += msg.value;
    }

}
- Scenario: Mapping variable indexed
link


Constructor indexes using 'msg.sender'
Function becomeRichest indexes using conctract variable 'richest'

See comments on setup

Account balances:
- Step 5: msg.value=3 transffed to 'acc3', total 3
- Step 6: msg.value=4 transffed to 'acc3'  total 7


Pending withdrawals:
- Step 5: d_eth_address1: 3
- Step 6: d_eth_address1: 7 = 3 + 4

Richest:
- Step 5: acc1
- Step 6: acc1


Partial (sic!) stace space extract:

eth_accounts:
eth_accounts@5={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0],
                 [address |-> "d_eth_address_2", codeHash |-> Nil, balance |-> 7],
                 [address |-> "d_eth_address_3", codeHash |-> "Demo1", balance |-> 3] }

eth_accounts@6={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0],
                 [address |-> "d_eth_address_2", codeHash |-> Nil, balance |-> 3],
                 [address |-> "d_eth_address_3", codeHash |-> "Demo1", balance |-> 7] }



eth_storageRoot:
eth_storageRoot@6={ ...   [ address |-> "d_eth_address_3",
                            richest |-> "d_eth_address_1",
                            pendingWithdrawals |->
                              ( Nil :> Nil @@ "d_eth_address_1" :> 7 @@  "d_eth_address_2" :> Nil @@  "d_eth_address_3" :> Nil ) ] }
# And a file named "src/invariant_storedValue.tla" with:
# """
# (* 
# *  'pendingWithdrawals' should be equal to account 'balance' for 'Demo1' -contracts
# *)
# invariant_storedValue == 
# \A demoAcc  \in  {  acc \in eth_accounts:  acc.codeHash = "Demo1" }: 
# demoAcc.balance = (CHOOSE contract \in eth_storageRoot: contract.address = demoAcc.address ).storedValue
# """
features/010-solidity/010-data-types.feature:44
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 3

       # Ether value range - later used non-deterministic choice
     - domain: eth_value
       type: Int

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:

        # step 1,2: create account 'acc1' & mine 3 units

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

        # step 3,4: create account 'acc2' & mine 7 units

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


        # step 5: accounts 'acc1' creates contract 'Demo1'
        # in address 'acc3', passess msg.value=3 and is
        # becomes richest
        # 

        - interface: Demo1()
          bindExact: true
          input: 
              _default: 0
              sender: 1
              value: 3

        # step 6: account 'acc2' calls 'becomeRichest' in
        # Demo1 contract address 'acc3', passess msg.value=4
        # and is becomes richest.

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