sbuilder-ethereum

Table of Contents

References

[1] CPU Mining with Geth. [ bib | http ]
[2] Test-driven development. [ bib | http ]
[3] Tla+ tools. [ bib | .html ]
[4] Ethreum solity translation to tla+ language, 2016. [ bib | http ]
[5] Ethereum Org. Solidity Language Documentation. [ bib | http ]
[6] Ethereum Org. Web3 JavaScript Dapp API. [ bib | http ]
[7] Ethereum Org. Go-Ethereum Wiki, 2016. [ bib | http ]
[8] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional. [ bib | .html ]
[9] Ethereum Org. The solidity contract-oriented programming language. [ bib | http ]
[10] Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger, homestead revision. Technical report. [ bib | .pdf ]

1 General

This document presents Ethereum[10] Solidity language[5] translation to TLA+ language[8] in sbuilder-ethereum tool[4].

overview.jpg

The picture above gives an overview of the translation process:

  • Applications on Ethereum platform are implemented using Solidity language. Application source code is compiled to byte code using solc Solidity compiler[9], and uploaded for execution in Ethereum platform[10].
  • sbuilder-ethereum receives Abstract Syntax Tree created by solc compiler and translates it into a TLA+ language model. The correctness of the formal TLA+ language model, as specified by user, can be checked on TLA-tools[3] under various environment context, represented by sbuilder-ethereum setups.

The picture presents also the two face role of this document: to map the translation to Ethereum platform, and act as a reference guide for the translation result. The two face role is also reflected in the structure of this document:

  • Chapter 2 describes how Solidity/TLA translation corresponds to Ethereum environment and links to reference sections in chapters 3 and 4.
  • Chapters 3 and 4 provide reference information for the translated TLA+ language model: chapter 3 describes Ethereum platform modeling, and chapter 4 Solidity contract translation. Sections in these chapters include automated tests, which validate that the document is up-to-date with respect to the implementation. An overview of service execution is shown in flow diagram in chapter 4.3.1 .

2 Overview of Solidity/TLA Translation

2.1 Ether Balance, Gas Used

2.1.1 Reward Application for Successful Mining

Mining results to rewarding beneficiary addresses ([10], Defs. 147-150).

Ethreum Wiki [7] explains, how mining may be started [1] using geth command line.

In Solidity/TLA translation:

  • Section 3.1.1.6: state variable models beneficiary address
  • Section 3.2.2: request and response message for interface get_mine

2.1.2 Gas Used in Processing Transactions

Before starting a transaction Ethereum platform checks the transaction validity [10](, Defs. 66). The check validates that:

  • amount of gas on a request exceeds intrinsic amount
  • the up front cost (= intrinsic amount + value transferred) of the transaction does not exceed the account balance

Total gas used in a transaction [10], Defs. 79) includes gas paid prior to transaction execution ([10], Defs. 67-69), and the amount consumed in processing transaction ([10], Defs. 70).

In Solidity/TLA translation:

  • account balance:
    • Section 3.1.1.1: defines state variable holding account information
    • Section 3.1.2.1: defines type of elements in state variable 3.1.1.1
  • operators to calculate gas:
    • Section 3.1.3.2 defines operator upFrontCost
    • Section 3.1.3.3 defines fixed operator intrinsicGas
    • Section 3.1.3.1 defines a fixed operator transactionGas modeling total amount gas consumed in transaction
    • Section 3.1.3.4 defines price of price, and section 3.1.3.5 an operator to convert gas to ethereum value.
  • request messages
    • Section 4.2.2 show request message for a constructor, the message does NOT include gas. The design choice is due to focusing on verifying contract behavior, instead of modeling Ethereum platform. Operations require enough value on an account, and they consume value on an account. Ref. next section.
    • Section 4.2.3 shows request and response messages for set method for Demo contract.
  • service execution
    • Section 4.3.2 shows actions during constructor transaction.
    • Section 4.3.3 shows actions during service transaction.

2.1.3 Gas Used Given to Beneficiary Address

The ether of gas used during contract creation, or message processing, is given to a beneficiary address of a miner ([10], Defs. 73-76).

2.1.4 Ether Invariant

In Solidity/TLA translation

  • Section 3.1.4.5: defines an invariant, which requires that value + sum of account balances + ether of gas used should equal to 0

2.2 Contract Creation

2.2.1 Modeling Account Information

Ethereum account comprises fields ([10], section 4.1) nonce, balance, and codeHash. Accounts with empty codeHash are simple accounts, also referred as "non-contract" accounts

In Solidity/TLA translation:

  • Section 3.1.2.1: defines data type used to model Ethereum accounts
  • Section 3.1.1.1: state variable storing records modeling Ethereum accounts

2.2.2 Modeling Contract Storage Content

Account field storageRoot refers to storage content of the contract. ([10], section 4.1)

In Solidity/TLA translation:

  • Section 3.1.1.3 state variable models storage content of a contract
  • Section 4.2.1: data type definition modeling solidity contract Demo

2.2.3 Contract Creation Request and Reply

Ethreum Contract Creation ([10], Section 7, Def. 81) accepts parameters: sender, original transactor, available gas, gasPrice, endowment.

In Solidity/TLA translation:

  • Section 3.2.1 document request and reply message for constructing non-contract account
  • Section 4.2.2 defines request and response messages for constructing a new Demo contract

2.2.4 Contract Creation Success/Failure

When Contract Creation fails no new contract is created, and no value is transferred ([10], Section 7).

The address of a new account is defined using hash function ([10], Def 82)

In Solidity/TLA translation:

  • see diagram 4.3.1 documenting service execution in sbuilder-ethrereum
  • see trace of steps for executing constructor4.3.2, and service function 4.3.3
  • Notes/warnings: when called procedure reaches normal/successful end it persists caller procedure up to the call point. This differs from real ethereum semantics, where remote transactions are separate.

2.3 TODO Open Questions/TODO

2.3.1 TODO Add Solidity Language Constructs

Execution framework has been mostly implemented (See flow diagram in [4.3.1]), but it is missing most of the Solidity language constructs.

2.3.2 Sending and Receiving Ether

  • See documenation

In general, validate & enhance documentation on ether balance. For example, non-contract account calls contract A, which further calls/constructs contract B. Which account is responsible for paying gas, and how solidity implementation can control paying party. Particularly:

  • What Solidity constructs represent CALL, CALLCODE, and DELEGATECALL op-codes defined in [10] appendix H.2.
  • Understand and model Solidity call command e.g. msg.sender.call.value(amount)()
    1. which function gets called, 2) who is paying for the gas.

2.3.3 TODO Transaction Model

Analyze and document transaction model vs. real ethrereum environment. Currently sbuilder-ethreum model in chained contract calls (contract A calls contract B), successful called contract finish commits state of caller contract up to the call point. This should be documented and its impact should be analyzed and better documented. Any other cases, where sbuilder-model and ethreum model differ?

Comment in sending and receiving ether

There is a way to forward more gas to the receiving contract using addr.call.value(x)(). This is essentially the same as addr.send(x), only that it forwards all remaining gas and opens up the ability for the recipient to perform more expensive actions.

Analysis: implementation may rely on additional safe of addr.call.value(x)(), in model checking safety should be result of design.

2.3.4 TODO Implement withdrawal and send patterns

Implement withdrawal-pattern:

The recommended method of sending funds after an effect is using the withdrawal pattern. …

as opposed to the more intuitive sending pattern

3 Specification Model of Ethereum Infrastructure

3.1 Definitions

3.1.1 Ethreum State

3.1.1.1 State accounts

References:

  • See chapter 3.1.2.1 for element types stored in this variable.
  • See chapter 3.1.4.1 for type invariant checking type correctness
  • See chapter 3.1.4.5 for invariant checking ether value balance, which this state variable is part of
(* eth:accounts - Accounts created in the system *)
\* account entries
eth_accounts = {};

Elements in variable definition:

Check Comments OK?
eth_accounts State variable OK
3.1.1.2 State accounts_temp
(* eth:accounts_temp - accounts temporary state during service execution *)
\* account transient state
eth_accounts_temp = <<>>;

Elements in variable definition:

Check Comments OK?
eth_accounts_temp State variable OK
3.1.1.3 State storageRoot

Generated model.tla defines state variable eth_storageRoot:

(* eth:storageRoot - Account storageRoot (contract state) *)
eth_storageRoot = {};

Elements in variable definition

Check Comments OK?
eth_storageRoot Name of state variable defined OK
3.1.1.4 State storageRoot_temp

Generated model.tla defines state variable eth_storageRoot_temp:

(* eth:storageRoot_temp - storageRoot temporary state during service execution *)
eth_storageRoot_temp = <<>>;

Elements in variable definition

Check Comments OK?
eth_storageRoot_temp Name of state variable defined OK
<<>> Initialized as an empty sequence OK
3.1.1.5 State address_free
(* eth:address_free - Set of unassigned addresses *)
\* Unassigned addresses
eth_address_free = d_eth_address \ { Nil };

Elements in variable definition:

Check Comments OK?
eth_address_free State variable OK
d_eth_address Domain for Ethereum addresses OK
Nil Nil is not a valid address OK
3.1.1.6 State mined
(* eth:mined - Value mined *)
eth_mined = 0;

Elements in variable definition:

Check Comments OK?
eth_mined State variable OK
0 Initialized to zero OK

3.1.2 Ethereum Types

3.1.2.1 Type t_Accounts
t_Accounts == [
  address: d_eth_address,
  codeHash: d_eth_code_hash,
  balance: d_eth_value
]

Elements in data type definition:

Check Comments OK?
address Unique id OK
balance Scalar value number of Wei owned OK
codeHash Identify EVM- class name, empty string OK
d_eth_code_hash Domain for field codeHash OK

3.1.3 Base Operators

3.1.3.1 Operator transactionGas

Generated model.tla defines operator transactionGas

(* framework-svc:transactionGas - Amount of gas consumed when running the transaction *)
(*
 * Running transaction consumes always 1 unit of gas.
 *)
transactionGas == 1

Elements in operator definition:

Check Comments OK?
transactionGas Name of operator defined OK
1 Using fixed value OK
3.1.3.2 Operator upFrontCost

Generated model.tla defines operator upFrontCost

(* framework-svc:upFrontCost - Acount balance must exceed upFronCost before starting *)
(*
* Value account must hold before transaction possible to start
* 
* @return [Integer] request.value  + gasPrice * intrinsicGas
*)
upFrontCost( request ) == request.value + gasPrice *  intrinsicGas

Elements in operator definition:

Check Comments OK?
upFrontCost Name of operator defined OK
request.value Use 'value' property in request message OK
gasPrice * intrinsicGas Amount to pay at the start transaction OK
3.1.3.3 Operator intrinsicGas

Generated model.tla defines operator intrinsicGas

(* framework-svc:intrinsicGas - Gas paid prior to execution *)
(* Always consume at least one unit of gas
 * Account must have balance >= intrinsicGas*gasPrice before execution
 *)
intrinsicGas == 1

Elements in operator definition:

Check Comments OK?
intrinsicGas Name of operator defined OK
1 Assigned fixed value 1 OK
3.1.3.4 Operator gasPrice

Generated model.tla defines operator gasPrice

(* framework-svc:gasPrice - Price of gas used to calculate value of gas *)
\* Use integer math, and gasPrice is just 1
gasPrice == 0

Elements in operator definition:

Check Comments OK?
gasPrice Name of operator defined OK
0 Assigned fixed valuei.e. not used OK
3.1.3.5 Operator gasValue
(* framework-svc:gasValue - Operator calculating value of gas (using gasPrice) *)
\* @return [Integer] gas * gasPrice
gasValue( gas ) == gas * gasPrice

Operator elements:

Check Comments OK?
gas formal parameter OK
gasPrice Operator defining currentprice of gas OK
gasValue Operator definition OK

3.1.4 Ethereum State Invariant

3.1.4.1 Invariant account_type
(* framework-svc:accounts_type - Invariant operator to account type *)
accounts_type == \A e \in eth_accounts: e \in t_Accounts

Elements in operator definition:

Check Comments OK?
accounts_type Operator defined OK
eth_accounts Checks all element in state variable OK
t_Accounts Type of account element must be correct (are element of this set) OK
3.1.4.2 Invariant accounts_unique
(* framework-svc:accounts_unique *)
\* Invariant: unique entries in account state variable
accounts_unique == uniqueElements( eth_accounts, "address" )

Elements in operator definition:

Check Comments OK?
accounts_unique Operator defined OK
uniqueElements Uses operator to check uniqueness OK
eth_accounts Element in state variable must satisfy uniqueness criteria OK
address Record field, which makes element unique OK
3.1.4.3 Invariant storageRoot_unique
(* framework-svc:storageRoot_unique *)
\* Invariant: unique entries in storageRoot state variable
storageRoot_unique == uniqueElements( eth_storageRoot, "address" )

Elements in operator definition:

Check Comments OK?
storageRoot_unique Operator defined OK
uniqueElements Uses operator to check uniqueness OK
eth_storageRoot Element in state variable must satisfy uniqueness criteria OK
address Record field, which makes element unique OK
3.1.4.4 Invariant accounts_valid
(* framework-svc:accounts_valid - Invariant operator to check that accounts are valid *)
\* valid account must have value >= 0, and address # Nil
accounts_valid == \A a \in eth_accounts: a.address # Nil /\ a.balance >= 0

Elements in the operator:

Check Comments OK?
accounts_valid Operator defined OK
eth_accounts Element in state variable are checked for validity OK
3.1.4.5 Invariant total_value
(* framework-svc:total_value - SUM( accounts.balance ) + mined == 0 *)
total_value == Stable =>  ( eth_mined + SumRecordField( eth_accounts, "balance" ) =  0 )

Operator elements:

Check Comments OK?
total_value Operator defined OK
Stable => Evaluate only when transaction not running OK
eth_mined Total value mined (negative) OK
SumRecordField( eth_accounts … Sum over balance of all accounts/contracts OK
balance Account/contract field for balance OK
= 0 Must add up 0 OK

3.1.5 Helper Operators

3.1.5.1 Helper uniqueElements
(* framework-svc:uniqueElements - operator to check element uniques in a set *)
uniqueElements( set, key ) == \A e1  \in set:  \A e2 \in set:   e1[key] = e2[key] => e1 = e2

Element in operator definition:

Check Comments OK?
uniqueElements Operator defined OK
3.1.5.2 Helper Stable
(* framework-svc:Stable - stable when process finished running *)
Stable == tx_running = FALSE

Element in operator definition:

Check Comments OK?
Stable Operator defined OK
tx_running State variable TRUE when service is executing- TRUE/FALSE OK
3.1.5.3 Helper SumRecordField
(* framework-svc:SumRecordField - Sum record fields *)
RECURSIVE SumRecordField(_,_)
(* 
 *  Sum of field 'f' of record elements in set 'S'
 * 
 *  @param [Set] S set of records
 *  @param [String] f name of field 
 *)
SumRecordField(S,f) == 
   IF S = {} THEN 0
   ELSE LET x == CHOOSE x \in S : TRUE
	IN x[f] + SumRecordField(S \ {x}, f)

Elements in operator definition:

Check Comments OK?
SumRecordField Operator defined OK
RECURSIVE TLA directive enabling operator recursion OK
3.1.5.4 Helper SumOfFunction
(* framework-svc:SumOfFunction - Sum function *)
RECURSIVE SumOfFunction(_)
(*
 * Sum of function values
 *
 * @param [Sequnce|Function] F to sum over
 *
 *)
SumOfFunction( F ) ==
   IF F = <<>> THEN 0
   ELSE LET x == CHOOSE x \in DOMAIN F : TRUE
	IN F[x] + SumOfFunction( [ v \in DOMAIN F \ {x} |-> F[v] ] )

Elements in operator definition:

Check Comments OK?
SumOfFunction Operator defined OK
RECURSIVE TLA directive enabling operator recursion OK
3.1.5.5 Helper NextId
(* framework-svc:NextId - Take given 'address', or choose any address from pool of 'ids'. Notice (CHOOSE operation is deterministic) *)
NextId( ids, address ) == CHOOSE x \in ids: (address = x /\ address # Nil) \/ address = Nil

Elements in operator definition:

Check Comments OK?
NextId Operator defined OK

3.2 Running Ethereum Infrastructure TLA Code

3.2.1 Interface personal_newAccount() Request and Response Datatypes

Data type definition modeling personal_newAccount() request:

t_req_personal_newAccount__ == [dummy: {Nil}
]

Elements in request data type definition:

Check Comments OK?
t_req_personal_newAccount__ Name data type definition modeling personal_newAccount() OK

Data type definition modeling personal_newAccount() response:

t_resp_personal_newAccount__ == [
    address: d_eth_address
]

Elements in response data type definition:

Check Comments OK?
t_resp_personal_newAccount__ Name data type definition modeling personal_newAccount() OK
account Returns account created OK

3.2.2 Interface geth_mine - Request and Response

Request message to interface get_mine()

t_req_geth_mine__ == [
          value: d_eth_value,
          beneficiary: d_eth_address
]

Elements in request definition:

Check Comments OK?
t_req_geth_mine__ Name of state message type (parenthesis as underscores) OK
beneficiary Address to rewarded for mining OK

Response of interface get_mine()

t_resp_geth_mine__ == { Nil }

Elements in response data type definition:

Check Comments OK?
t_resp_geth_mine__ Name of state message type (parenthesis as underscores) OK

4 Specification Model of Ethereum Contracts

4.1 Example Contract

pragma solidity ^0.3.5;

contract Demo {
    uint storedData;
    address owner;

    // Generated automatically if missing
    // uint balance;

    // Generate automatically if missing
    // function Demo() {
    // }

    function set(uint x) {
	storedData = x;
    }

    function tst() constant returns (uint t) {
	// return 1;
	return storedData;    
    }

    function get() constant returns (uint retVal) {
	return storedData;
    }
}

4.2 Definitions

4.2.1 Example Contract t_Demo

Contract type shows members it inherits from Address and members defined on contract solidity source:

t_Demo == [
  storedData: d_Demo_storedData,
  owner: d_Demo_owner,
  address: d_Demo_address
]

Record fields in contract record type:

Check Comments OK?
storedData Contract member variable OK
owner Contract member variable OK
address Member variable inherited from Address OK

4.2.2 Interface Demo() Constructor Request and Reply

Request message to create new Ethereum Demo contract:

t_req_Demo__ == [
          sender: d_eth_address,
          originator: d_eth_address,
          value: d_eth_value
]

The record models request fields:

Check Comments OK?
value value/endowment onq the request OK
send sender of the request OK
originator transaction origniator OK

The record shows also domains of request message fields:

Check Comments OK?
D_eth_value domain of parameter 'value' OK
d_eth_address domain of parameter 'sender' OK

Data type definition modeling contract construction response:

t_resp_Demo__ == [
    address: d_eth_address
]

Elements in contract construct response data type definition:

Check Comments OK?
t_resp_Demo__ Data type modeling constructor response OK
address Address of (contract )account created OK

4.2.3 Interface Demo(set) Setter Request and Reply

Request message to for Demo(set) interface operation:

t_req_Demo_set_ == [
          x: d_Demo_storedData,
          sender: d_eth_address,
          originator: d_eth_address,
          recipient: d_eth_address,
          value: d_eth_value
]

The record models request fields:

Check Comments OK?
gas gas value on the request OK
value value/endowment onq the request OK
send sender of the request OK
originator transaction origniator OK

Data type definition modeling contract construction response:

t_resp_Demo_set_ == { Nil }

Elements in contract construct response data type definition:

Check Comments OK?
t_resp_Demo__ Data type modeling constructor response OK
address Address of (contract )account created OK

4.3 Execution

4.3.1 Execution Flow Diagram

The flow diagram below documents transaction processing in sbuilder-ethreum.

In consists of two main part:

  • scheduler - modeled as TLA "fair process" calling the two macros shown in block labeled "scheduler"
  • service procedure executing solidity contract function shown in block labeled "svc"

transaction.jpg

Service procedure block above shows

  • initialization steps: during which sbuilder-ethereum initializes temporary variables to block stack comprising account state 3.1.1.2, contract state 3.1.1.4.
  • contract constructor steps:
    • creating an account entry [3.1.1.1] in block stack 3.1.1.2 using personal_newAccount() [3.2.1] service
    • creating storageRoot [3.1.1.3]-entry in bloc stack [3.1.1.4]
  • step to move value from sender to receiver
  • body execution steps: in block labeled with "body" representing statement in solidity source
  • finishing steps with
    • normal/successful end: reached after all body statements have been successfully executed
    • user failure: reached after throw statement (or any other valid exception condition) during which
      • transaction state in temporary variables is discarded, and
      • caller procedure is returned fail status, which it may check
    • abort - which indicates error in application modeling i.e. control flow has not set return status. Abort condition is checked by sbuilder-ethreum framework
  • cleanup step, where block stack is popped
4.3.1.1 TODO Analysis of transaction semantics

4.3.2 Constructor Execution

Actions starting constructor transaction:

"TX-start@Demo(): push block state to stack"
"TX-start@Demo(): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","" 
"TX-start@Demo(): call call service implementation", "x3_Demo__"

Actions during constructor service:

"SVC-exec@Demo(): persist accounts"
"SVC-exec@Demo(): init return status", Abort
"SVC-exec@Demo(): non-deterministic out-of-gas-check"
"SVC-exec@Demo(): check sender balance >= gasValue(transactionGas) + value","d_eth_address_1","balance",6,"value needed",3 
"SVC-exec@Demo(): call 'personal_newAccount' to create new account entry" 
"SVC-exec@Demo(): create contract entry to storageRoot_temp"
"SVC-exec@Demo(): moved value"
"SVC-exec@Demo(): process constructor body"
"SVC-exec@Demo(): set return status",TRUE,"return account id created","d_eth_address_2" 

Actions finishing constructor transaction

"TX-end@", "Demo()", "success: restore eth_storageRoot "
"TX-end@", "Demo()", "success: restore eth_accounts "

4.3.3 Service Execution

Actions starting service transaction:

"TX-start@Demo(set): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account exists" 
"TX-start@Demo(set): credit  gasUsed with value of  intrinsicGas",1 
"TX-start@Demo(set): debit sender account","d_eth_address_1","with gasValue",1 
"TX-start@Demo(set): storageRoot_temp := storageRoot"
"TX-start@Demo(set): accounts_temp := accounts"
"TX-start@Demo(set): gasUsed_temp := gasUsed"
"TX-start@Demo(set): call call service implementation","x3_Demo_set_" 

Actions during service execution:

"SVC-exec@Demo(set): init return status", FALSE
"SVC-exec@Demo(set): check sender balance >= gasValue(transactionGas) + value","d_eth_address_1","balance",3,"value needed",3 
"SVC-exec@Demo(set): service body"
"SVC-exec@Demo(set): credit 'transactionGas' for transaction gas value",1 
"SVC-exec@Demo(set): debit sender","d_eth_address_1","for transaction gas value",1 
"SVC-exec@Demo(set): set return status", TRUE

Actions finishing service transaction

"TX-end@", "Demo(set)", "success: restore eth_storageRoot "
"TX-end@", "Demo(set)", "success: restore eth_accounts "
"TX-end@", "Demo(set)", "success: restore eth_gasUsed "

5 Document context

5.1 Version numbers

sbuilder version:

sbuilder.rb - 0.3.5-SNAPSHOT   

sbuilder-ethreum version:

0.0.6-SNAPSHOT

5.2 Configuration file sbuilder.yaml

# ------------------------------------------------------------------
# Generate preferences
#
preferences:
      debug-output: false

# ------------------------------------------------------------------
# Load and configure sbuilder plugin extensions
#
# Activate sbuilder-ethereum && define one loader instance

extend:
  loaders:
     - className: Sbuilder::Ethereum::Plugin
       gem: sbuilder-ethereum
       configuration:
	 solc_command: '../solc/solidity/build/solc/solc'
       objects:
	  - objectName: solcLoader
	    configuration:
	      preferences:
		 tla-debug: false
		 tla-trace: true

     # - className: Sbuilder::SnippetLoaderSimple
     #   configuration:
     #        src_dir: src/pet


# ------------------------------------------------------------------
# Define how to load interfaces configuration
#
# Load interfaces for  'sbuilder-ethreum'


interfaces:

    - 
       objectName: solcLoader
       # url: examples/test.sol
       # url: examples/simple_storage.sol
       url: examples/demo.sol

#  Possibliity to run other loaders besides 'sbuilder-ethereum'
#     # -  
#     #    className: Sbuilder::ParamSetLoaderSwagger
#     #    file: interface_customer.yaml



# ------------------------------------------------------------------
# Load manual snippets to sbuilder code repository
#

# Load snippets for  'sbuilder-ethreum'
snippets:

  -  objectName: solcLoader
     snippets:

# Possibility to include manually include snipppets, not used in 'sbuilder-ethereum'


#   - className: Sbuilder::SnippetLoaderSimple 
#     snippets:




# ------------------------------------------------------------------
# Define how parameter names are mapped to domain
#
# No need to configure resolver: domains are managed by sbuilder-ethereum


# resolvers:
#      # - file: resolver_customer.yaml
#      - file: resolver_default.yaml           

# ------------------------------------------------------------------
# Define environment setups
#
# These setups used to create sbuilder-ethreum documentation

setups:

    #
    # Document infrastructure services
    #
    - setupDirectory: demo0
      extensions:
	-  url: cnf/setup-demo0.yaml

    #
    # Document interface 'personal_newAccount()'
    #

    - setupDirectory: demo1
      extensions:
	-  url: cnf/setup-demo1.yaml

    #
    # Document interface 'geth_mine()'
    #


    - setupDirectory: demo2
      extensions:
	-  url: cnf/setup-demo2.yaml

    #
    # Document contract & successfulle contract creation
    #

    - setupDirectory: contract-1
      extensions:
	-  url: cnf/setup-contract-1.yaml

    #
    # Contract upFrontCost exceeds account balance
    #

    - setupDirectory: contract-2
      extensions:
	-  url: cnf/setup-contract-2.yaml


    #
    # Contract Demo created, setter method
    #

    - setupDirectory: contract-3
      extensions:
	-  url: cnf/setup-contract-3.yaml


    #
    # Demo(), Demo.set, Demo.get
    #

    - setupDirectory: contract-4
      extensions:
	-  url: cnf/setup-contract-4.yaml



    #
    # Free to test (not used in document generatior)
    #


    - setupDirectory: tst
      extensions:
	-  url: cnf/setup-tst.yaml


# ------------------------------------------------------------------
# Generate definitions

# No use in 'embedded mode', intended use in 'upfront desing' mode

# ------------------------------------------------------------------
# Activate invariant operator defines in sBuilder code repository
#
# TODO: activate invariants over snippet loader facade

invariants:
    - accounts_type: account type valid
    - accounts_unique: unique entries in account state variable
    - accounts_valid: account id valid && account value valid
    - total_value: SUM( accounts.balance ) + mined must be 0
    # - invariant__Demo: contract 'Demo' valid

Date: <2016-10-14 pe>

Author: jj

Created: 2016-12-05 ma 14:18

Validate