[More Detail] [Collapse All]
Feature: Invariant to verify contract member variable and account balance
features/200-correctness/020-invariant-checks-balance.feature
- Background: Create Demo contracts, define 2 setups, and an invariant
link

Define solidity contract Demo, which updates 'storedValue'
with 'msg.value' in constructor.

We define invariant 'invariant_storedValue.tla', which requires
that 'storedValue' should be equal to account 'balance' for 'Demo'
-contracts.

Demo(set) -method simply overrides 'storedValue', causing
a violation of the invariant.

Define two setups, which are are used to verify user defined
invariants (and also invariants defined by sbuilder-ethereum).
features/200-correctness/020-invariant-checks-balance.feature:3
Given I create initial sbuilder context with:
Directory
solidity demo1
setup setup1
setup setup2
# Content of solidity 'demo1'
And a file named "solidity/demo1.sol" with:
pragma solidity ^0.3.5;

contract Demo {

    uint storedValue;

    // constructor sets storedValue 
    function Demo() {
         storedValue = msg.value;
    }

    // override storedValue
    function set(uint x) {
        storedValue = x;
    }

}
And a file named "src/invariant_storedValue.tla" with:
(* 
 *  'storedValue' should be equal to account 'balance' for 'Demo' -contracts
*)
invariant_storedValue == 
    \A demoAcc  \in  {  acc \in eth_accounts:  acc.codeHash = "Demo" }: 
         demoAcc.balance = (CHOOSE contract \in eth_storageRoot: contract.address = demoAcc.address ).storedValue
And an entry in `snippets` -section in YAML file `cnf/sbuilder.yaml`:
#
#  Here load operator snippet in  file  'src/invariant_storedValue.tla' 
#  into sbuilder context.
#
- className: Sbuilder::SnippetLoaderSimple 
  snippets:
       - metatype: invariants
         appName: invariant_storedValue
         name: invariant_storedValue
         url: src/invariant_storedValue.tla
And an entry in `invariants` -section in YAML file `cnf/sbuilder.yaml`:
#
#  We have created a file TLA+ code defining an operator 'invariant_storedValue'.
#  The operator snippet has been loaded to sbuilder context. We need to 
#  instruct sbuilder that the operator should be used to check invariant
#  property in model checking.
#
#
- invariant_storedValue: contract 'storedValue' must equal account 'balance'
- Scenario: Invariant not violated in constructor
link
features/200-correctness/020-invariant-checks-balance.feature:88
#
# In this scenario, we construct an account with 'Demo' contract.
# Model checking for 'setup1' finds all invariants, including
# 'invariant_storedValue', to be respected. 
#
# State space after step 3 (constructing Demo() finds:
#
# eth_accounts@3={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0],
#                  [address |-> "d_eth_address_2", codeHash |-> "Demo", balance |-> 2] }
# eth_storageRoot@3={[address |-> "d_eth_address_2", storedValue |-> 2]}
#
# Notice that:
#
# - d_eth_address_2.balance == storedValue == 2, corrponding the value transferred to Demo()
# - d_eth_address_1.balance == 0 == 4 - 1 - 1 -2, corresponding
#       -- 4 units mined 
#       -- 1 units transferred to d_eth_address_2
#       -- 1 unit for intrinsicGas
#       -- 2 unit for running Demo() transaction
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_code_hash
       values:
          - Demo

     - domain: eth_address
       cardinality: 4

       # Ether value range - later used non-deterministic choice
     - domain: eth_value
       range: [0,5]

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account
 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          input:
              value: 4
        - interface: Demo()
          input:
              value: 2
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Regexp
1 step p_personal_newAccount__
2 step p_geth_mine__
3 step p_Demo__
- Scenario: Invariant violated in setter function
link
features/200-correctness/020-invariant-checks-balance.feature:149
#
# In this scenario, we construct 'Demo' contract, however
# we call also 'Demo(set)' interface, which bluntly overrides
# 'storedValue', resulting to a violatio of 'invariant_storedValue',
#
Given a file named "cnf/setup2.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 3

       # Ether value range - later used non-deterministic choice
     - domain: eth_value
       range: [0,7]

    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account
 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          input:
              value: 7
        - interface: Demo()
          input:
              sender: 1
              value: 1
        - interface: Demo(set)
          input:
              sender: 1
              recipient: 2
              x: 4
When I generate, translate, and model check setup `setup2` to find violation in `invariant_storedValue`
Then State space extract `gen/setup2/tla/err.dump` contains
Tick Variable Key Field Field
1 step p_personal_newAccount__
2 step p_geth_mine__
3 step p_Demo__
3 eth_accounts d_eth_address_1 balance 6
3 eth_accounts d_eth_address_2 balance 1
#
# Last state shows the error: d_eth_address_2.balance <>
# d_eth_address_2.storedValue
#
Then State space extract `gen/setup2/tla/err.dump` last state contains
Tick Variable Key Field Value
4 step p_Demo_set_
4 eth_accounts d_eth_address_2 balance 1
4 eth_storageRoot d_eth_address_2 storedValue 4