Skip to content

Instantly share code, notes, and snippets.

@jarjuk
Last active Dec 12, 2016
Embed
What would you like to do?
sbuilder-ethreum example TLA formal model
TLA+ language formal model for setup 'game1' in blog post https://jarjuk.wordpress.com/2016/12/09/sbuilder-ethereum-example/
pragma solidity ^0.4.0;
contract WithdrawalGame {
address public richest;
uint public mostSent;
mapping (address => uint) pendingWithdrawals;
function becomeRichest() payable returns (bool) {
if (msg.value >= mostSent) {
pendingWithdrawals[richest] += msg.value;
richest = msg.sender;
mostSent = msg.value;
return true;
} else {
return false;
}
}
function WithdrawalGame() payable {
richest = msg.sender;
mostSent = msg.value;
}
function withdraw() returns (bool) {
uint amount = pendingWithdrawals[msg.sender];
// Remember to zero the pending refund before
pendingWithdrawals[msg.sender] = 0;
// sending to prevent re-entrancy attacks
if (msg.sender.send(amount)) {
// open for re-entrant attack
// pendingWithdrawals[msg.sender] = 0;
return true;
} else {
pendingWithdrawals[msg.sender] = amount;
return false;
}
}
}
contract FairPlayer {
WithdrawalGame game;
function play() {
game.becomeRichest.value(2)();
}
function endGame() {
game.withdraw();
}
function FairPlayer( WithdrawalGame g ) {
game = g;
}
}
This file has been truncated, but you can view the full file.
Model version: Model version file /home/jj/work/org-beamer-presu/ethereum-meetup-hki-2016/demo/VERSION not found
Generator version: 0.3.4
Generation timestemp: 2016-12-12 08:06:56
------------------------------ MODULE model ------------------------------
EXTENDS TLC, FiniteSets, Sequences, Integers
(* Execution environment *)
CONSTANTS Steps \* Sequence process/parameter records
(* Magic values *)
CONSTANTS WildCard \* bind to any value
CONSTANTS Nil \* no value
CONSTANTS Abort \* response.status error
\* Extension point template extend/extend_const.mustache:
(******************************************************************
Domain definitions
- modelData domains
- template domains.mustache
******************************************************************)
CONSTANTS d_eth_address
CONSTANTS d_eth_value
CONSTANTS d_BOOLEAN
CONSTANTS d_WithdrawalGame
CONSTANTS d_default
CONSTANTS d_WithdrawalGame_pendingWithdrawals
CONSTANTS d_WithdrawalGame_address
CONSTANTS d_FairPlayer
CONSTANTS d_FairPlayer_address
CONSTANTS d_eth_gas
CONSTANTS d_eth_code_hash
(* schedule operators *)
\* Notice: cardinality of +steps+ sequence elements is 1, change in future?
ProcessStep( stepdefs ) == (CHOOSE s \in Head( stepdefs ): TRUE )
ProcessRunning( stepdefs ) == ProcessStep( stepdefs ).process
ProcessEnabled( stepdefs, s ) == Len( stepdefs ) # 0 /\ s = ProcessRunning( stepdefs )
ProcessesToRun( stepdefs ) == Tail( stepdefs )
ProcessParameter( stepdefs ) == ProcessStep( stepdefs )
TickNext( t ) == t + 1 \* advance time (when process start)
InTransaction == FALSE \* TRUE when application service running, FALSE when not
(******************************************************************
Initial value for infrastructure service responses
- modelData infrastructureServices
- template infrastructure-service-init.mustache
******************************************************************)
\* create record to put into 'responses'variable field
InfrastructureServiceResponse( status, response ) == [ status |-> status, response |-> response ]
\* Initial value to variable 'responses'
InfrastructureServiceInit == [ i_personal_newAccount__ |-> InfrastructureServiceResponse( Nil, Nil ), i_geth_mine__ |-> InfrastructureServiceResponse( Nil, Nil ), i_GlobalScope_send_ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame_becomeRichest_ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame__ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame_withdraw_ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame_getRichest_ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame_getMostSent_ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame_getPendingWithdrawals_ |-> InfrastructureServiceResponse( Nil, Nil ), i_WithdrawalGame_getAddress_ |-> InfrastructureServiceResponse( Nil, Nil ), i_FairPlayer_play_ |-> InfrastructureServiceResponse( Nil, Nil ), i_FairPlayer_endGame_ |-> InfrastructureServiceResponse( Nil, Nil ), i_FairPlayer__ |-> InfrastructureServiceResponse( Nil, Nil ), i_FairPlayer_getGame_ |-> InfrastructureServiceResponse( Nil, Nil ), i_FairPlayer_getAddress_ |-> InfrastructureServiceResponse( Nil, Nil ) ]
(******************************************************************
Defined types Data type definitions
- modelData definitions
- template definition_types.mustache
*******************************************************************)
(* DEFINITION: definitions:Accounts *)
t_Accounts == [
address: d_eth_address,
codeHash: d_eth_code_hash,
balance: d_eth_value
]
(* END-OF-DEFINTION Accounts *)
(* DEFINITION: definitions:WithdrawalGame_pendingWithdrawals *)
t_WithdrawalGame_pendingWithdrawals == [ d_eth_address -> d_default ]
(* END-OF-DEFINTION WithdrawalGame_pendingWithdrawals (function type!) *)
(* DEFINITION: definitions:WithdrawalGame *)
t_WithdrawalGame == [
richest: d_eth_address,
mostSent: d_eth_value,
pendingWithdrawals: t_WithdrawalGame_pendingWithdrawals,
address: d_WithdrawalGame_address
]
(* END-OF-DEFINTION WithdrawalGame *)
(* DEFINITION: definitions:FairPlayer *)
t_FairPlayer == [
game: d_eth_address,
address: d_FairPlayer_address
]
(* END-OF-DEFINTION FairPlayer *)
(******************************************************************
Interface input types: Interface types
- modelData interfaces
- template interface_types.mustache
*******************************************************************)
(* REQUEST: personal_newAccount() --> TLA process: p_personal_newAccount__ *)
t_req_personal_newAccount__ == [dummy: {Nil}
]
(* END-OF-REQUEST *)
(* REQUEST: geth_mine() --> TLA process: p_geth_mine__ *)
t_req_geth_mine__ == [
value: d_eth_value,
beneficiary: d_eth_address
]
(* END-OF-REQUEST *)
(* REQUEST: GlobalScope(send) --> TLA process: p_GlobalScope_send_ *)
t_req_GlobalScope_send_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame(becomeRichest) --> TLA process: p_WithdrawalGame_becomeRichest_ *)
t_req_WithdrawalGame_becomeRichest_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame() --> TLA process: p_WithdrawalGame__ *)
t_req_WithdrawalGame__ == [
sender: d_eth_address,
originator: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame(withdraw) --> TLA process: p_WithdrawalGame_withdraw_ *)
t_req_WithdrawalGame_withdraw_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame(getRichest) --> TLA process: p_WithdrawalGame_getRichest_ *)
t_req_WithdrawalGame_getRichest_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame(getMostSent) --> TLA process: p_WithdrawalGame_getMostSent_ *)
t_req_WithdrawalGame_getMostSent_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame(getPendingWithdrawals) --> TLA process: p_WithdrawalGame_getPendingWithdrawals_ *)
t_req_WithdrawalGame_getPendingWithdrawals_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: WithdrawalGame(getAddress) --> TLA process: p_WithdrawalGame_getAddress_ *)
t_req_WithdrawalGame_getAddress_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: FairPlayer(play) --> TLA process: p_FairPlayer_play_ *)
t_req_FairPlayer_play_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: FairPlayer(endGame) --> TLA process: p_FairPlayer_endGame_ *)
t_req_FairPlayer_endGame_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: FairPlayer() --> TLA process: p_FairPlayer__ *)
t_req_FairPlayer__ == [
g: d_eth_address,
sender: d_eth_address,
originator: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: FairPlayer(getGame) --> TLA process: p_FairPlayer_getGame_ *)
t_req_FairPlayer_getGame_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
(* REQUEST: FairPlayer(getAddress) --> TLA process: p_FairPlayer_getAddress_ *)
t_req_FairPlayer_getAddress_ == [
sender: d_eth_address,
originator: d_eth_address,
recipient: d_eth_address,
value: d_eth_value
]
(* END-OF-REQUEST *)
\* end of Interface input types
(******************************************************************
Interface response types: Interface types
- modelData interfaces
- template interface_types.mustache
*******************************************************************)
(* RESPONSE: personal_newAccount() --> TLA process: p_personal_newAccount__ *)
t_resp_personal_newAccount__ == [
address: d_eth_address
]
(* END-OF-RESPONSE *)
(* RESPONSE: geth_mine() --> TLA process: p_geth_mine__ *)
t_resp_geth_mine__ == { Nil }
(* END-OF-RESPONSE *)
(* RESPONSE: GlobalScope(send) --> TLA process: p_GlobalScope_send_ *)
t_resp_GlobalScope_send_ == [
status: d_BOOLEAN
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame(becomeRichest) --> TLA process: p_WithdrawalGame_becomeRichest_ *)
t_resp_WithdrawalGame_becomeRichest_ == [
becomeRichest: d_BOOLEAN
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame() --> TLA process: p_WithdrawalGame__ *)
t_resp_WithdrawalGame__ == [
address: d_eth_address
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame(withdraw) --> TLA process: p_WithdrawalGame_withdraw_ *)
t_resp_WithdrawalGame_withdraw_ == [
withdraw: d_BOOLEAN
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame(getRichest) --> TLA process: p_WithdrawalGame_getRichest_ *)
t_resp_WithdrawalGame_getRichest_ == [
richest: d_eth_address
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame(getMostSent) --> TLA process: p_WithdrawalGame_getMostSent_ *)
t_resp_WithdrawalGame_getMostSent_ == [
mostSent: d_eth_value
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame(getPendingWithdrawals) --> TLA process: p_WithdrawalGame_getPendingWithdrawals_ *)
t_resp_WithdrawalGame_getPendingWithdrawals_ == [
pendingWithdrawals: d_WithdrawalGame_pendingWithdrawals
]
(* END-OF-RESPONSE *)
(* RESPONSE: WithdrawalGame(getAddress) --> TLA process: p_WithdrawalGame_getAddress_ *)
t_resp_WithdrawalGame_getAddress_ == [
address: d_WithdrawalGame_address
]
(* END-OF-RESPONSE *)
(* RESPONSE: FairPlayer(play) --> TLA process: p_FairPlayer_play_ *)
t_resp_FairPlayer_play_ == { Nil }
(* END-OF-RESPONSE *)
(* RESPONSE: FairPlayer(endGame) --> TLA process: p_FairPlayer_endGame_ *)
t_resp_FairPlayer_endGame_ == { Nil }
(* END-OF-RESPONSE *)
(* RESPONSE: FairPlayer() --> TLA process: p_FairPlayer__ *)
t_resp_FairPlayer__ == [
address: d_eth_address
]
(* END-OF-RESPONSE *)
(* RESPONSE: FairPlayer(getGame) --> TLA process: p_FairPlayer_getGame_ *)
t_resp_FairPlayer_getGame_ == [
game: d_eth_address
]
(* END-OF-RESPONSE *)
(* RESPONSE: FairPlayer(getAddress) --> TLA process: p_FairPlayer_getAddress_ *)
t_resp_FairPlayer_getAddress_ == [
address: d_FairPlayer_address
]
(* END-OF-RESPONSE *)
(*
--algorithm model {
(******************************************************************
State environment model
- modelData none
- template tla/plc_run_state.mustache
******************************************************************)
variables
\* sequence of [ { process |-> {}, parameter |-> {} }]
steps = Steps;
\* process currently running = self with _ replcing non-numeric
step = Nil;
\* head from +steps+ sequence used to schedule +step+
step_parameter = {};
\* current time tick, each process run in own tick
now = 0;
\* TRUE when process is running
tx_running = FALSE;
\* rec [ ret_ctx |-> stack entry push in resume ], when resuming, Nil when not
resume_context = Nil;
(******************************************************************
Variables used by infrastructure-services
- modelData none
- template infrastructure-service-variables.mustache
******************************************************************)
\* Variable for returning responses from infrastructure services
responses = InfrastructureServiceInit;
\* Extension point template extend/extend_state.mustache:
(* ETH-SNIPPET: eth:accounts --> eth_accounts *)
(* eth:accounts - Accounts created in the system *)
\* account entries
eth_accounts = {};
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:storageRoot --> eth_storageRoot *)
(* eth:storageRoot - Account storageRoot (contract state) *)
eth_storageRoot = {};
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:storageRoot_temp --> eth_storageRoot_temp *)
(* eth:storageRoot_temp - storageRoot temporary state during service execution *)
eth_storageRoot_temp = <<>>;
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:accounts_temp --> eth_accounts_temp *)
(* eth:accounts_temp - accounts temporary state during service execution *)
\* account transient state
eth_accounts_temp = <<>>;
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:address_free --> eth_address_free *)
(* eth:address_free - Set of unassigned addresses *)
\* Unassigned addresses
eth_address_free = d_eth_address \ { Nil };
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:mined --> eth_mined *)
(* eth:mined - Value mined *)
eth_mined = 0;
(* ETH-SNIPPET-END *)
define {
(*
Current time in state variable now gets ticked
when process starts.
*)
currentTime == now
(*
Return set of possible bindings to an enabled process
@param [Set] inputSet set of all possible inputs to a process
@return first that matches
- inputSet if step_parameter.bindSet == Nil
- step_parameter.bindSet if step_parameter.bindSet != Nil
*)
ProcessParameterInput( inputSet ) ==
IF step_parameter'.bindSet = Nil
THEN inputSet
ELSE step_parameter'.bindSet
(* All record fields in 'bindDef' must bind with corresponding fields in 'inputParam' *)
\* ProcessParameterEnablesTst( inputParam, bindDefs ) == \A key \in { k \in DOMAIN bindDefs : k # "_key" }: bindDefs[key] = inputParam[key]
(*
ProcessParameterEnables: 'inputParam' satisfies 'bindDefs'
- all 'normal' field in 'bindDefs' are found in 'inputParam'
- and all subrecords can be validated recursively using 'ProcessParameterEnables' using a the set in field '_key'
- and for each record in the set in field '_rows'
-- validates at least one row in 'inputParam'
--- cardinality of inputParam[key] = cardinality _row.set
-- OR equals 'values' set
Recurse one level down in 'inputParam' using keys 'bindDefs._key.key'.
Recursion is done only if 'bindDefs' defines field '_key'.
*)
RECURSIVE ProcessParameterEnables( _, _ )
ProcessParameterEnables( inputParam, bindDefs ) ==
( \A key \in { k \in DOMAIN bindDefs : Len(k)<4 \/ (SubSeq(k,1,4) # "_key" /\ k # "_rows" )}: bindDefs[key] = inputParam[key] )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : Len(k)>3 /\SubSeq(k,1,4) = "_key" }: \A r \in bindDefs[reckey] : ProcessParameterEnables( inputParam[r.key], r.rec ) )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_rows" }: \A r \in bindDefs[reckey] :
(r.row_types = "singletons" /\ r.set = inputParam[r.key] )
\/ (r.row_types = "hashes" /\ Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\ \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef ) )
)
(*
Predicate to filter elements in ProcessParameterInput set to pass
to +steps+ element in +step_parameter' variable.
Pass +inputParameter+ to a process if one the following matches
- resume_contex # Nil (i.e. process execution is resuming)
- step_parameter = WildCard (i.e. Head elemend of +steps+ sequence is WildCard, allow everything )
- step_parameter.bindSet = WildCard (i.e. Head element defines bindSet element)
- predicate 'ProcessParameterEnables' resolves TRUE for step_parameter'.bindRule
*)
ProcessParameterBind( inputParam ) ==
\/ resume_context' # Nil
\/ step_parameter' = WildCard
\/ step_parameter'.bindRule = WildCard
\/ ProcessParameterEnables( inputParam, step_parameter'.bindRule )
(******************************************************************
Operators for infrastrcuture service (generated)
- modelData infrastructureServices
- template operator-infrastructure-service.mustache
******************************************************************)
InterfaceOperation2ProcessName( op ) == CASE op = "xxXXxx" -> Nil
[] op = "personal_newAccount()" -> "i_personal_newAccount__"
[] op = "geth_mine()" -> "i_geth_mine__"
[] op = "GlobalScope(send)" -> "i_GlobalScope_send_"
[] op = "WithdrawalGame(becomeRichest)" -> "i_WithdrawalGame_becomeRichest_"
[] op = "WithdrawalGame()" -> "i_WithdrawalGame__"
[] op = "WithdrawalGame(withdraw)" -> "i_WithdrawalGame_withdraw_"
[] op = "WithdrawalGame(getRichest)" -> "i_WithdrawalGame_getRichest_"
[] op = "WithdrawalGame(getMostSent)" -> "i_WithdrawalGame_getMostSent_"
[] op = "WithdrawalGame(getPendingWithdrawals)" -> "i_WithdrawalGame_getPendingWithdrawals_"
[] op = "WithdrawalGame(getAddress)" -> "i_WithdrawalGame_getAddress_"
[] op = "FairPlayer(play)" -> "i_FairPlayer_play_"
[] op = "FairPlayer(endGame)" -> "i_FairPlayer_endGame_"
[] op = "FairPlayer()" -> "i_FairPlayer__"
[] op = "FairPlayer(getGame)" -> "i_FairPlayer_getGame_"
[] op = "FairPlayer(getAddress)" -> "i_FairPlayer_getAddress_"
[] OTHER -> Assert( FALSE, "Unknown infrastructure service" )
(******************************************************************
Operators supporting infrastructure services
- modelData none
- template tla/operators-infrastructure-service.mustache
******************************************************************)
\* return response for 'operation' from 'responses' state variable
InfrastructureServiceGetResponse( operation ) == responses[InterfaceOperation2ProcessName(operation)].response
\* return status for 'operation' from 'responses' state variable
InfrastructureServiceGetStatus( operation ) == responses[InterfaceOperation2ProcessName(operation)].status
\* Extension point template extend/extend_operations.mustache:
(* ETH-SNIPPET: framework-svc:NewStep --> NewStep *)
(* Create a step entry to schedule in +steps+ sequence
* @param procci process identifier to schedule
* @param procInput an elment in process input set to pass to the process
* @param ctx context where to resume, Nil if no resume
*)
NewStep( procci, procInput, ctx ) == [ process |-> procci, bindRule |-> WildCard ,bindSet |-> procInput, ctx |-> ctx ]
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:Push --> Push *)
(* framework-svc:Push - Add element to sequence head *)
Push( s, e ) == <<e>> \o s
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:UpdateTop --> UpdateTop *)
(* framework-svc:UpdateTop - Update element to sequence head *)
UpdateTop( s, e ) == <<e>> \o Tail(s)
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:PropageTopAndPop --> PropageTopAndPop *)
(* framework-svc:PropageTopAndPop - Propgate top element to stack & pop *)
PropageTopAndPop( s ) == [i \in 1..(Len(s) -1 )|-> s[1] ]
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:PropageOnStack --> PropageOnStack *)
(* framework-svc:PropageOnStack - Propgate top element to stack & pop *)
(* PropageOnStack( s, v ) == [i \in 1..Len(s) |-> v ] *)
PropageOnStack( s, v ) == [i \in 1..Len(s) |-> IF i = 1 THEN v ELSE s[i] ]
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:Stable --> Stable *)
(* framework-svc:Stable - stable when process finished running *)
Stable == tx_running = FALSE
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:SumRecordField --> 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)
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:SumOfFunction --> 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] ] )
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:uniqueElements --> 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
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:NextId --> 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
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:getElement --> getElement *)
(* framework-svc:getElement - Return element form a set by id *)
(*
* Return element from 'set' such that element['key'] == 'id'
* Assume 'id' unique, and element exists
*)
getElement( set, key, id ) == ( CHOOSE x \in { e \in set : e[key] = id } : TRUE )
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:elementExists --> elementExists *)
(* framework-svc:elementExists - Ensure that element exists *)
(*
* Unique element exists
*)
elementExists( set, key, id ) == Cardinality( { e \in set : e[key] = id } ) = 1
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:status_OK --> status_OK *)
(* framework-svc:status_OK - Service ran successfully *)
status_OK == TRUE
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:status_FAIL --> status_FAIL *)
(* framework-svc:status_FAIL - Service execution failed *)
status_FAIL == FALSE
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:gasPrice --> gasPrice *)
(* framework-svc:gasPrice - Price of gas used to calculate value of gas *)
\* Use integer math, and gasPrice is just 1
gasPrice == 0
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:gasValue --> gasValue *)
(* framework-svc:gasValue - Operator calculating value of gas (using gasPrice) *)
\* @return [Integer] gas * gasPrice
gasValue( gas ) == gas * gasPrice
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:intrinsicGas --> 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
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:transactionGas --> transactionGas *)
(* framework-svc:transactionGas - Amount of gas consumed when running the transaction *)
(*
* Running transaction consumes always 1 unit of gas.
*)
transactionGas == 1
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:upFrontCost --> 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
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:accounts_unique --> accounts_unique *)
(* framework-svc:accounts_unique *)
\* Invariant: unique entries in account state variable
accounts_unique == uniqueElements( eth_accounts, "address" )
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:storageRoot_unique --> storageRoot_unique *)
(* framework-svc:storageRoot_unique *)
\* Invariant: unique entries in storageRoot state variable
storageRoot_unique == uniqueElements( eth_storageRoot, "address" )
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:accounts_valid --> 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
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:total_value --> total_value *)
(* framework-svc:total_value - SUM( accounts.balance ) + mined == 0 *)
total_value == Stable => ( eth_mined + SumRecordField( eth_accounts, "balance" ) = 0 )
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:accounts_type --> accounts_type *)
(* framework-svc:accounts_type - Invariant operator to account type *)
accounts_type == \A e \in eth_accounts: e \in t_Accounts
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: invariants:stack_ok --> invariant__stack_ok *)
(* Define operator 'invariant__stack_ok' to guard against stack size growing to large.
*
* TLA-tools model checking mode uses breadth-first approach for the state space exploration (default),
* and havig stack depth so large means that a infinite recusion (is most likely) encountered.
*
*)
invariant__stack_ok == \A se \in DOMAIN stack: Len(stack[se]) <= 20
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: invariants:game_ok --> invariant__game_ok *)
(* operator 'invariant__game_ok' validates that 'WithdrawalGame' posesses enough value to
* pay all pending withdrawals.
*
* Len( eth_accounts_temp ) # 0 : game transaction is running
* Len( eth_storageRoot_temp) = Len( eth_accounts_temp ) : game is ready to run
*
* a.codeHash \in { "WithdrawalGame", "WithdrawalGameInErr" } : game contract
* a.address = s.address : join
*
* a.balance > SumOfFunction( s.pendingWithdrawals : enough value to pay all pending withdrawals
*
*)
invariant__game_ok ==
Len( eth_accounts_temp ) # 0 /\ Len( eth_storageRoot_temp) = Len( eth_accounts_temp ) =>
\A a \in Head(eth_accounts_temp): \A s \in Head(eth_storageRoot_temp):
a.codeHash \in { "WithdrawalGame", "WithdrawalGameInErr" } /\ a.address = s.address => a.balance > SumOfFunction( s.pendingWithdrawals )
(* ETH-SNIPPET-END *)
} \* define
(***********************************************************************
Macros to control process execution && time
***********************************************************************)
macro tick() {
now := TickNext( now ); \* now := now + 1;
}
macro enable( s ) {
(* head in sequence 'steps' enable processes *)
\* await Len( steps ) # 0 /\ ProcessEnabled( steps, s );
await ProcessEnabled( steps, s );
(* process entered, remove head from sequence 'steps' *)
step := ProcessRunning( steps ); \* Head( steps ).process;
step_parameter := ProcessParameter( steps );
\* steps := ProcessesToRun( steps ); \* Tail( steps );
\* Context to resume to from Head(steps ), Nil = not resuming
resume_context := ProcessStep( steps ).ctx;
(* Reset infrastructure service responses on process entry *)
responses := InfrastructureServiceInit;
(* Flag Transaction started *)
tx_running := TRUE;
(* time advances by one tick for each process step *)
tick();
\* debug( s );
}
(* Remove currently running prosess from head of 'step'.
Calling this macro enables next process to take turn.
If a process comprises several steps, this results
processes runing parallel, unless 'process_done' is
called in the end of the process.
*)
macro process_done( s ) {
steps := ProcessesToRun( steps ); \* Tail( steps );
\* process must clear resume context
assert( resume_context = Nil );
(* Flag Transaction started *)
tx_running := FALSE;
}
(******************************************************************
Macros for infrastructure services
- modelData none
- template tla/macro-infrastructure-service.mustache
******************************************************************)
\* set 'status' with 'response' for 'operation' into state variable 'responses'
macro InfrastructureServiceReturn( operation, status, response ) {
\* update field for 'operation' in 'responses' variable with record [ status |-> s , response |-> r ]
responses[InterfaceOperation2ProcessName(operation)] := InfrastructureServiceResponse( status, response );
}
\* Extension point template extend/extend_macros.mustache:
(* ETH-SNIPPET: framework-svc:schedule_throw --> schedule_throw *)
(*
Throw exception and exit current process via +exitLocation+.
Modify +stack+ top to return from current procedure to
+exitLocation+, and retain stack bottom to return from current
process. *)
macro schedule_throw( exitLocation ) {
stack := <<
[ stack[self][1] EXCEPT !.pc = exitLocation ],
stack[self][ Len(stack[self]) ]
>>;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:schedule_process_mac --> schedule_process_mac *)
(*
Schedule a call for an external process +called+ with +input+, and
+resume+ back to the calling process in context +resumeCtx+.
Implementation adds two step entries in +steps+ sequence.
Entries cannot be made to position 1 because it represents
currently running process, which get shifted away the sequnce
once the process finishes.
*)
macro schedule_process_mac( called, input, resume, resumeCtx ) {
\* NOTICE!!: call and resume steps always successive elements
\* The only option is to apped to +steps+
if ( Cardinality( { p \in 1..Len(steps) : \A s \in steps[p]: s.ctx = Nil } ) <= 1 ) {
steps := steps \o
<< { NewStep( called, input, Nil ) },
{ NewStep( resume, Nil, resumeCtx ) } >>;
} else {
\* Non-deteministic choice where to put
with ( pos \in { p \in 2..Len(steps) : \A s \in steps[p]: s.ctx = Nil } ) {
steps := IF pos = Len(steps) THEN
steps \o
<< { NewStep( called, input, Nil ) },
{ NewStep( resume, Nil, resumeCtx ) } >>
ELSE
SubSeq( steps, 1, pos-1 ) \o
<< { NewStep( called, input, Nil ) },
{ NewStep( resume, Nil, resumeCtx ) } >> \o
SubSeq( steps, pos, Len(steps))
;
}; \* with
}; \* else
skip;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:update_existing_contract --> update_existing_contract *)
(* framework-svc:update_existing_contract - macro to update existing contract *)
macro update_existing_contract() {
print <<"update_existing_contract">>;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:create_new_contract --> create_new_contract *)
(* framework-svc:create_new_contract - macro to create new contract *)
macro create_new_contract( var, entry, idPool, id ) {
print <<"create_new_contract", entry >>;
var := var \union { entry };
idPool := idPool \ {id};
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:ethereum_service_start --> ethereum_service_start *)
(* framework-svc:ethereum_service_start - Start ethereum transaction, create stack *)
(*
* Macro called when transaction starts.
* Inializes ethreum block context to stack.
*
* @see ethereum_service_done
* @see ethereum_service_push
*)
macro ethereum_service_start() {
eth_storageRoot_temp := <<eth_storageRoot>>;
eth_accounts_temp := <<eth_accounts>>;
\* eth_gasUsed_temp := <<eth_gasUsed>>;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:personal_newAccount() --> i__personal_newAccount__ *)
(* service_implementation:personal_newAccount() - Interface entry for "createAccount" *)
macro i__personal_newAccount__( input ) {
\* prepare for transaction
\* print <<"TRACE>","TX-start@personal_newAccount(): push block state to stack">>;
ethereum_service_start();
call eth_personal_newAccount( [ codeHash |-> input.dummy, address |-> Nil ] );
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:personal_newAccount_done --> personal_newAccount_done *)
(* framework-svc:personal_newAccount_done - Finalize "personal_newAccount" *)
macro personal_newAccount_done( interface ) {
\* like ethereum_service_done( interface ) + creates eth_storageRoot
eth_storageRoot := Head(eth_storageRoot_temp) \union { [address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] };
eth_accounts := Head(eth_accounts_temp);
\* eth_gasUsed := Head(eth_gasUsed_temp);
eth_storageRoot_temp := <<>>;
eth_accounts_temp := <<>>;
\* eth_gasUsed_temp := <<>>;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:geth_mine() --> i__geth_mine__ *)
(* service_implementation:geth_mine() - Interface entry for "mine" *)
macro i__geth_mine__( input ) {
call eth_mine( input );
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:ethereum_service_done --> ethereum_service_done *)
(* framework-svc:ethereum_service_done - Pop ethreum block context from stack *)
(*
* Interface process (called scheduled) has finished.
* Check service response status, and
* commit changes in 'eth_storageRoot' and 'eth_accounts', if success.
* In any case clear variables modeling block status because
* they are not needed anymore (after all scheduler starts a new
* round).
*
*)
macro ethereum_service_done( interface ) {
if ( InfrastructureServiceGetStatus(interface ) = TRUE ) {
\* Success commit changes to 'temp' & cleanup
\* print <<"TRACE>", "TX-end@", interface, "success: restore eth_storageRoot ">>;
\* print <<"TRACE>", "TX-end@", interface, "success: restore eth_accounts ">>;
(* \* print <<"TRACE>", "TX-end@", interface, "success: restore eth_gasUsed ">>; *)
eth_storageRoot := Head(eth_storageRoot_temp);
eth_accounts := Head(eth_accounts_temp);
\* eth_gasUsed := Head(eth_gasUsed_temp);
};
eth_storageRoot_temp := <<>>;
eth_accounts_temp := <<>>;
\* eth_gasUsed_temp := <<>>;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:ethereum_service_push --> ethereum_service_push *)
(* framework-svc:ethereum_service_push - Push ethereum block context to stack *)
(*
* Macro called when service starts. Duplicates current
* top of stack.
*
* @see ethereum_service_start
* @see ethereum_service_done
*)
macro ethereum_service_push() {
eth_storageRoot_temp := Push( eth_storageRoot_temp, Head( eth_storageRoot_temp )) ;
eth_accounts_temp := Push( eth_accounts_temp, Head( eth_accounts_temp ));
\* eth_gasUsed_temp := Push( eth_gasUsed_temp, Head(eth_gasUsed_temp));
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: framework-svc:ethereum_service_pop --> ethereum_service_pop *)
(* framework-svc:ethereum_service_pop - Finish service procedure: propage stack top on succcess && pop *)
(*
* Service procedure for 'interface' has finished.
* Check status of service response.
* For success make changes in procedure permanent by propagating
* stack top to top-1..bottom.
*
* In any case pop one element from stack.
*
*)
macro ethereum_service_pop( interface ) {
if ( InfrastructureServiceGetStatus(interface ) = TRUE ) {
\* Success - propage changes, and make the permanent
eth_storageRoot_temp := PropageTopAndPop( eth_storageRoot_temp );
eth_accounts_temp := PropageTopAndPop( eth_accounts_temp );
\* eth_gasUsed_temp := PropageTopAndPop( eth_gasUsed_temp );
}
else {
eth_storageRoot_temp := Tail(eth_storageRoot_temp);
eth_accounts_temp := Tail(eth_accounts_temp);
\* eth_gasUsed_temp := Tail( eth_gasUsed_temp );
};
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame(becomeRichest) --> i__WithdrawalGame_becomeRichest_ *)
(* service_implementation:WithdrawalGame(becomeRichest) - Service entry for WithdrawalGame(becomeRichest) *)
macro i__WithdrawalGame_becomeRichest_( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(becomeRichest): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(becomeRichest): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(becomeRichest): call call service implementation","x3_WithdrawalGame_becomeRichest_">>;
call x3_WithdrawalGame_becomeRichest_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame() --> i__WithdrawalGame__ *)
(* service_implementation:WithdrawalGame() - Service entry for WithdrawalGame() *)
macro i__WithdrawalGame__( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","">>;
if ( elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(): call call service implementation","x3_WithdrawalGame__">>;
call x3_WithdrawalGame__( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame(withdraw) --> i__WithdrawalGame_withdraw_ *)
(* service_implementation:WithdrawalGame(withdraw) - Service entry for WithdrawalGame(withdraw) *)
macro i__WithdrawalGame_withdraw_( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(withdraw): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(withdraw): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(withdraw): call call service implementation","x3_WithdrawalGame_withdraw_">>;
call x3_WithdrawalGame_withdraw_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame(getRichest) --> i__WithdrawalGame_getRichest_ *)
(* service_implementation:WithdrawalGame(getRichest) - Service entry for WithdrawalGame(getRichest) *)
macro i__WithdrawalGame_getRichest_( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getRichest): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(getRichest): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getRichest): call call service implementation","x3_WithdrawalGame_getRichest_">>;
call x3_WithdrawalGame_getRichest_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame(getMostSent) --> i__WithdrawalGame_getMostSent_ *)
(* service_implementation:WithdrawalGame(getMostSent) - Service entry for WithdrawalGame(getMostSent) *)
macro i__WithdrawalGame_getMostSent_( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getMostSent): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(getMostSent): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getMostSent): call call service implementation","x3_WithdrawalGame_getMostSent_">>;
call x3_WithdrawalGame_getMostSent_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame(getPendingWithdrawals) --> i__WithdrawalGame_getPendingWithdrawals_ *)
(* service_implementation:WithdrawalGame(getPendingWithdrawals) - Service entry for WithdrawalGame(getPendingWithdrawals) *)
macro i__WithdrawalGame_getPendingWithdrawals_( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getPendingWithdrawals): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(getPendingWithdrawals): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getPendingWithdrawals): call call service implementation","x3_WithdrawalGame_getPendingWithdrawals_">>;
call x3_WithdrawalGame_getPendingWithdrawals_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:WithdrawalGame(getAddress) --> i__WithdrawalGame_getAddress_ *)
(* service_implementation:WithdrawalGame(getAddress) - Service entry for WithdrawalGame(getAddress) *)
macro i__WithdrawalGame_getAddress_( par ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getAddress): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@WithdrawalGame(getAddress): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@WithdrawalGame(getAddress): call call service implementation","x3_WithdrawalGame_getAddress_">>;
call x3_WithdrawalGame_getAddress_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: dispatcher:address_getAddress --> dispatch_address_getAddress *)
(* dispatcher:address_getAddress *)
macro dispatch_address_getAddress( rec ) {
responses := InfrastructureServiceInit;
if ( getElement( Head( eth_accounts_temp ),"address",rec.recipient ).codeHash \in { "WithdrawalGame" } ) {
call x3_WithdrawalGame_getAddress_( rec);
} else {
if ( getElement( Head( eth_accounts_temp ),"address",rec.recipient ).codeHash \in { "FairPlayer" } ) {
call x3_FairPlayer_getAddress_( rec);
} else {
(* "Unkwon interface" *)
assert( FALSE );
};
};
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:FairPlayer(play) --> i__FairPlayer_play_ *)
(* service_implementation:FairPlayer(play) - Service entry for FairPlayer(play) *)
macro i__FairPlayer_play_( par ) {
\* print <<"TRACE>","TX-start@FairPlayer(play): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@FairPlayer(play): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@FairPlayer(play): call call service implementation","x3_FairPlayer_play_">>;
call x3_FairPlayer_play_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:FairPlayer(endGame) --> i__FairPlayer_endGame_ *)
(* service_implementation:FairPlayer(endGame) - Service entry for FairPlayer(endGame) *)
macro i__FairPlayer_endGame_( par ) {
\* print <<"TRACE>","TX-start@FairPlayer(endGame): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@FairPlayer(endGame): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@FairPlayer(endGame): call call service implementation","x3_FairPlayer_endGame_">>;
call x3_FairPlayer_endGame_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:FairPlayer() --> i__FairPlayer__ *)
(* service_implementation:FairPlayer() - Service entry for FairPlayer() *)
macro i__FairPlayer__( par ) {
\* print <<"TRACE>","TX-start@FairPlayer(): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@FairPlayer(): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","">>;
if ( elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@FairPlayer(): call call service implementation","x3_FairPlayer__">>;
call x3_FairPlayer__( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:FairPlayer(getGame) --> i__FairPlayer_getGame_ *)
(* service_implementation:FairPlayer(getGame) - Service entry for FairPlayer(getGame) *)
macro i__FairPlayer_getGame_( par ) {
\* print <<"TRACE>","TX-start@FairPlayer(getGame): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@FairPlayer(getGame): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@FairPlayer(getGame): call call service implementation","x3_FairPlayer_getGame_">>;
call x3_FairPlayer_getGame_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: service_implementation:FairPlayer(getAddress) --> i__FairPlayer_getAddress_ *)
(* service_implementation:FairPlayer(getAddress) - Service entry for FairPlayer(getAddress) *)
macro i__FairPlayer_getAddress_( par ) {
\* print <<"TRACE>","TX-start@FairPlayer(getAddress): push block state to stack">>;
ethereum_service_start()
;
\* print <<"TRACE>","TX-start@FairPlayer(getAddress): check pre-conditions","1) sender account exists","2) sender balance>= upFrontCost","3) receive account non nil">>;
if ( par.recipient # Nil /\ elementExists( eth_accounts,"address",par.sender ) /\ getElement( eth_accounts,"address",par.sender ).balance >= upFrontCost( par ) ) {
\* print <<"TRACE>","TX-start@FairPlayer(getAddress): call call service implementation","x3_FairPlayer_getAddress_">>;
call x3_FairPlayer_getAddress_( par)
;
}
;
}
(* ETH-SNIPPET-END *)
(******************************************************************
Interfaces generated Create a dummy procedure to have &#39;defaultInitValue&#39; in the model
- modelData none
- template interface_stubs_dummy.mustache
******************************************************************)
(* Allow 'interface-extension.implementation' without specification code snippet *)
macro dummy( dummy_input ) {
print << "Dummy macro called should replace with actual macro" >>;
}
(* Create a dummy procedure with input variable so that pcal creates
constant defaultInitValue (which is assigned a value in setup.tla)
*)
procedure dummy( dummy_input ) {
dummy_start: skip;
}
\* Extension point template extend/extend_implementation.mustache:
(* ETH-SNIPPET: framework-svc:schedule_process_proc --> schedule_process_proc *)
(*
Schedule process +input.called+ with +input.input+, and resume back
to currently running process +step+ to pc of +self+ ProcDef.
Creates a record with +ret_ctx+ property, which calling process can
use to restore its context, adds call step and resume step to
+steps+ sequence.
*)
procedure schedule_process_proc( input ) {
schedule_process_start:
schedule_process_mac(
input.called, input.input, step,
[ ret_ctx |-> [ stack[self][2] EXCEPT !.pc = stack[self][1].pc ] ]
);
return;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:personal_newAccount --> eth_personal_newAccount *)
(* eth:personal_newAccount - Interface service "createAccount" *)
(*
* @param [codeHash] class name, Nil for non-contract accounts
* @param [address] Nil|address to take from pools
*)
procedure eth_personal_newAccount( input ) {
eth_personal_newAccount_enter:
\* Must have NextId available in free address pool
assert( eth_address_free # {} );
\* Create account record in 'accounts' variable, input.dummy is default - because no input defined
eth_accounts_temp :=
UpdateTop( eth_accounts_temp,
Head( eth_accounts_temp ) \union { [ address |-> NextId( eth_address_free, input.address ), balance |-> 0, codeHash |-> input.codeHash ]});
\* Set return
InfrastructureServiceReturn( "personal_newAccount()", status_OK, NextId( eth_address_free, input.address ) );
\* Remove 'NextId' from frees address pool
eth_address_free :=
eth_address_free \ { NextId( eth_address_free, input.address ) };
eth_personal_newAccount_exit:
return;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: eth:mine --> eth_mine *)
(* eth:mine - Interface service "mine" *)
procedure eth_mine( input ) {
eth_mine_enter:
\* Check that account input.etherbase exists
if ( { e \in eth_accounts: e.address = input.beneficiary } = {}) {
goto eth_mine_exit;
};
eth_mine_ok:
\* Update on 'account.balance' with 'input.value'
eth_accounts :=
{ IF e.address = input.beneficiary THEN [ e EXCEPT !.balance = e.balance + input.value ] ELSE e : e \in eth_accounts };
\* Update total value 'mined'
eth_mined := eth_mined - input.value;
eth_mine_exit:
return;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:GlobalScope(send) --> x3_GlobalScope_send_ *)
(* solidity_contract_function:GlobalScope(send) - Service procedure for GlobalScope(send) *)
procedure x3_GlobalScope_send_( x3_GlobalScope_send__input )
variable locals;
{
x3_GlobalScope_send__start:
\* print <<"TRACE>","ENTRY:","x3_GlobalScope_send_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_GlobalScope_send__input>>;
skip
;
(* body of GlobalScope(send) *)
x3_GlobalScope_send__0: skip;
x3_GlobalScope_send__1: \* print <<"TRACE>","SVC-exec@GlobalScope(send): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@GlobalScope(send): non-deterministic out-of-gas-check">>;
either skip or goto x3_GlobalScope_send__abort
;
x3_GlobalScope_send__2: locals := x3_GlobalScope_send__input.recipient;
skip;
x3_GlobalScope_send__3: if ( x3_GlobalScope_send__input.sender # x3_GlobalScope_send__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_GlobalScope_send__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_GlobalScope_send__input.value ] ELSE IF a.address = x3_GlobalScope_send__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_GlobalScope_send__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@GlobalScope(send): moved value">>;
skip
;
InfrastructureServiceReturn( "GlobalScope(send)",status_FAIL,TRUE );
skip;
x3_GlobalScope_send__4: \* print <<"TRACE>","SVC-exec@GlobalScope(send): set return status",status_OK>>;
InfrastructureServiceReturn( "GlobalScope(send)",status_OK,InfrastructureServiceGetResponse( "GlobalScope(send)" ) )
;
x3_GlobalScope_send__exit:
goto x3_GlobalScope_send__end;
x3_GlobalScope_send__fail:
\* throw command sends here
InfrastructureServiceReturn( "GlobalScope(send)", FALSE, Nil);
goto x3_GlobalScope_send__end;
x3_GlobalScope_send__abort:
\* should not happen??
print <<"ABORT x3_GlobalScope_send_">>;
InfrastructureServiceReturn( "GlobalScope(send)", Abort, Nil);
\* schedule_throw( "x3_GlobalScope_send__exit" );
x3_GlobalScope_send__end:
ethereum_service_pop( "GlobalScope(send)" );
\* print <<"TRACE>","EXIT:","x3_GlobalScope_send_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_GlobalScope_send__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame(becomeRichest) --> x3_WithdrawalGame_becomeRichest_ *)
(* solidity_contract_function:WithdrawalGame(becomeRichest) - Service procedure for WithdrawalGame(becomeRichest) *)
procedure x3_WithdrawalGame_becomeRichest_( x3_WithdrawalGame_becomeRichest__input )
variable locals;
{
x3_WithdrawalGame_becomeRichest__start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame_becomeRichest_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_becomeRichest__input>>;
skip
;
(* body of WithdrawalGame(becomeRichest) *)
x3_WithdrawalGame_becomeRichest__0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame_becomeRichest__1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame_becomeRichest__abort
;
x3_WithdrawalGame_becomeRichest__2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame_becomeRichest__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_becomeRichest__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame_becomeRichest__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_becomeRichest__input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame_becomeRichest__input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(becomeRichest): abort">>;
goto x3_WithdrawalGame_becomeRichest__abort
;
}
;
x3_WithdrawalGame_becomeRichest__3: skip;
locals := x3_WithdrawalGame_becomeRichest__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_WithdrawalGame_becomeRichest__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_WithdrawalGame_becomeRichest__input.recipient ])
;
x3_WithdrawalGame_becomeRichest__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame_becomeRichest__input.sender # x3_WithdrawalGame_becomeRichest__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_becomeRichest__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_becomeRichest__input.value ] ELSE IF a.address = x3_WithdrawalGame_becomeRichest__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_becomeRichest__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): moved value">>;
skip
;
x3_WithdrawalGame_becomeRichest__call_construct: InfrastructureServiceReturn( "WithdrawalGame(becomeRichest)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(becomeRichest)" ) );
goto x3_WithdrawalGame_becomeRichest__end;
};
x3_WithdrawalGame_becomeRichest__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "WithdrawalGame" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): wrong type">>;
goto x3_WithdrawalGame_becomeRichest__abort
;
};
x3_WithdrawalGame_becomeRichest__6: if ( x3_WithdrawalGame_becomeRichest__input.sender # x3_WithdrawalGame_becomeRichest__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_becomeRichest__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_becomeRichest__input.value ] ELSE IF a.address = x3_WithdrawalGame_becomeRichest__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_becomeRichest__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): moved value">>;
skip
;
if ( x3_WithdrawalGame_becomeRichest__input.value >= getElement( Head( eth_storageRoot_temp ),"address",locals ).mostSent ) {
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.pendingWithdrawals[getElement( Head( eth_storageRoot_temp ),"address",locals ).richest] = getElement( Head( eth_storageRoot_temp ),"address",locals ).pendingWithdrawals[getElement( Head( eth_storageRoot_temp ),"address",locals ).richest] + x3_WithdrawalGame_becomeRichest__input.value ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
skip;
x3_WithdrawalGame_becomeRichest__7: eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.richest = x3_WithdrawalGame_becomeRichest__input.sender ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
skip;
x3_WithdrawalGame_becomeRichest__8: eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.mostSent = x3_WithdrawalGame_becomeRichest__input.value ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
InfrastructureServiceReturn( "WithdrawalGame(becomeRichest)",status_FAIL,TRUE );
} else {
InfrastructureServiceReturn( "WithdrawalGame(becomeRichest)",status_FAIL,FALSE );
};
x3_WithdrawalGame_becomeRichest__9: skip;
x3_WithdrawalGame_becomeRichest__10: \* print <<"TRACE>","SVC-exec@WithdrawalGame(becomeRichest): set return status",status_OK>>;
InfrastructureServiceReturn( "WithdrawalGame(becomeRichest)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(becomeRichest)" ) )
;
x3_WithdrawalGame_becomeRichest__exit:
goto x3_WithdrawalGame_becomeRichest__end;
x3_WithdrawalGame_becomeRichest__fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame(becomeRichest)", FALSE, Nil);
goto x3_WithdrawalGame_becomeRichest__end;
x3_WithdrawalGame_becomeRichest__abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame_becomeRichest_">>;
InfrastructureServiceReturn( "WithdrawalGame(becomeRichest)", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame_becomeRichest__exit" );
x3_WithdrawalGame_becomeRichest__end:
ethereum_service_pop( "WithdrawalGame(becomeRichest)" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame_becomeRichest_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_becomeRichest__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame() --> x3_WithdrawalGame__ *)
(* solidity_contract_function:WithdrawalGame() - Constructor for contract WithdrawalGame()' *)
procedure x3_WithdrawalGame__( x3_WithdrawalGame___input )
variable locals;
{
x3_WithdrawalGame___start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame__","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame___input>>;
skip
;
(* body of WithdrawalGame() *)
x3_WithdrawalGame___0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame___1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame___abort
;
x3_WithdrawalGame___2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame___input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame___input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame___input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame___input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame___input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(): abort">>;
goto x3_WithdrawalGame___abort
;
}
;
x3_WithdrawalGame___3: skip;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> "WithdrawalGame", address |-> Nil ])
;
x3_WithdrawalGame___4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame___input.sender # InfrastructureServiceGetResponse( "personal_newAccount()" ) ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = InfrastructureServiceGetResponse( "personal_newAccount()" ) THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame___input.value ] ELSE IF a.address = x3_WithdrawalGame___input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame___input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(): moved value">>;
skip
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(): process constructor body">>;
x3_WithdrawalGame____body: skip
;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.richest = x3_WithdrawalGame___input.sender ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
skip;
x3_WithdrawalGame___5: eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.mostSent = x3_WithdrawalGame___input.value ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(): set return status",status_OK,"return account id created",locals>>;
InfrastructureServiceReturn( "WithdrawalGame()",status_OK,locals )
;
skip;
x3_WithdrawalGame___exit:
goto x3_WithdrawalGame___end;
x3_WithdrawalGame___fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame()", FALSE, Nil);
goto x3_WithdrawalGame___end;
x3_WithdrawalGame___abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame__">>;
InfrastructureServiceReturn( "WithdrawalGame()", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame___exit" );
x3_WithdrawalGame___end:
ethereum_service_pop( "WithdrawalGame()" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame__","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame___input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame(withdraw) --> x3_WithdrawalGame_withdraw_ *)
(* solidity_contract_function:WithdrawalGame(withdraw) - Service procedure for WithdrawalGame(withdraw) *)
procedure x3_WithdrawalGame_withdraw_( x3_WithdrawalGame_withdraw__input )
variable locals, amount;
{
x3_WithdrawalGame_withdraw__start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame_withdraw_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_withdraw__input>>;
skip
;
(* body of WithdrawalGame(withdraw) *)
x3_WithdrawalGame_withdraw__0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame_withdraw__1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame_withdraw__abort
;
x3_WithdrawalGame_withdraw__2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame_withdraw__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_withdraw__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame_withdraw__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_withdraw__input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame_withdraw__input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(withdraw): abort">>;
goto x3_WithdrawalGame_withdraw__abort
;
}
;
x3_WithdrawalGame_withdraw__3: skip;
locals := x3_WithdrawalGame_withdraw__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_WithdrawalGame_withdraw__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_WithdrawalGame_withdraw__input.recipient ])
;
x3_WithdrawalGame_withdraw__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame_withdraw__input.sender # x3_WithdrawalGame_withdraw__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_withdraw__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_withdraw__input.value ] ELSE IF a.address = x3_WithdrawalGame_withdraw__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_withdraw__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): moved value">>;
skip
;
x3_WithdrawalGame_withdraw__call_construct: InfrastructureServiceReturn( "WithdrawalGame(withdraw)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(withdraw)" ) );
goto x3_WithdrawalGame_withdraw__end;
};
x3_WithdrawalGame_withdraw__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "WithdrawalGame" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): wrong type">>;
goto x3_WithdrawalGame_withdraw__abort
;
};
x3_WithdrawalGame_withdraw__6: if ( x3_WithdrawalGame_withdraw__input.sender # x3_WithdrawalGame_withdraw__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_withdraw__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_withdraw__input.value ] ELSE IF a.address = x3_WithdrawalGame_withdraw__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_withdraw__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): moved value">>;
skip
;
amount := getElement( Head( eth_storageRoot_temp ),"address",locals ).pendingWithdrawals[x3_WithdrawalGame_withdraw__input.sender];
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.pendingWithdrawals[x3_WithdrawalGame_withdraw__input.sender] = 0 ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",x3_WithdrawalGame_withdraw__input.sender ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): abort because called address of contract does not exist">>;
goto x3_WithdrawalGame_withdraw__abort
;
};
x3_WithdrawalGame_withdraw__7: call x3_GlobalScope_send_( [ value |-> amount, recipient |-> x3_WithdrawalGame_withdraw__input.sender, sender |-> locals, originator |-> x3_WithdrawalGame_withdraw__input.originator ]);
x3_WithdrawalGame_withdraw__8: if ( Abort = InfrastructureServiceGetStatus( "GlobalScope(send)" ) ) {
goto x3_WithdrawalGame_withdraw__abort;
};
x3_WithdrawalGame_withdraw__9: if ( InfrastructureServiceGetResponse( "GlobalScope(send)" ) ) {
InfrastructureServiceReturn( "WithdrawalGame(withdraw)",status_FAIL,TRUE );
} else {
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.pendingWithdrawals[x3_WithdrawalGame_withdraw__input.sender] = amount ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
InfrastructureServiceReturn( "WithdrawalGame(withdraw)",status_FAIL,FALSE );
};
skip;
x3_WithdrawalGame_withdraw__10: \* print <<"TRACE>","SVC-exec@WithdrawalGame(withdraw): set return status",status_OK>>;
InfrastructureServiceReturn( "WithdrawalGame(withdraw)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(withdraw)" ) )
;
x3_WithdrawalGame_withdraw__exit:
goto x3_WithdrawalGame_withdraw__end;
x3_WithdrawalGame_withdraw__fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame(withdraw)", FALSE, Nil);
goto x3_WithdrawalGame_withdraw__end;
x3_WithdrawalGame_withdraw__abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame_withdraw_">>;
InfrastructureServiceReturn( "WithdrawalGame(withdraw)", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame_withdraw__exit" );
x3_WithdrawalGame_withdraw__end:
ethereum_service_pop( "WithdrawalGame(withdraw)" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame_withdraw_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_withdraw__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame(getRichest) --> x3_WithdrawalGame_getRichest_ *)
(* solidity_contract_function:WithdrawalGame(getRichest) - Service procedure for WithdrawalGame(getRichest) *)
procedure x3_WithdrawalGame_getRichest_( x3_WithdrawalGame_getRichest__input )
variable locals;
{
x3_WithdrawalGame_getRichest__start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame_getRichest_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getRichest__input>>;
skip
;
(* body of WithdrawalGame(getRichest) *)
x3_WithdrawalGame_getRichest__0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame_getRichest__1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame_getRichest__abort
;
x3_WithdrawalGame_getRichest__2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame_getRichest__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getRichest__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame_getRichest__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getRichest__input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame_getRichest__input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(getRichest): abort">>;
goto x3_WithdrawalGame_getRichest__abort
;
}
;
x3_WithdrawalGame_getRichest__3: skip;
locals := x3_WithdrawalGame_getRichest__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_WithdrawalGame_getRichest__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_WithdrawalGame_getRichest__input.recipient ])
;
x3_WithdrawalGame_getRichest__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame_getRichest__input.sender # x3_WithdrawalGame_getRichest__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getRichest__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getRichest__input.value ] ELSE IF a.address = x3_WithdrawalGame_getRichest__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getRichest__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): moved value">>;
skip
;
x3_WithdrawalGame_getRichest__call_construct: InfrastructureServiceReturn( "WithdrawalGame(getRichest)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getRichest)" ) );
goto x3_WithdrawalGame_getRichest__end;
};
x3_WithdrawalGame_getRichest__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "WithdrawalGame" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): wrong type">>;
goto x3_WithdrawalGame_getRichest__abort
;
};
x3_WithdrawalGame_getRichest__6: if ( x3_WithdrawalGame_getRichest__input.sender # x3_WithdrawalGame_getRichest__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getRichest__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getRichest__input.value ] ELSE IF a.address = x3_WithdrawalGame_getRichest__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getRichest__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): moved value">>;
skip
;
InfrastructureServiceReturn( "WithdrawalGame(getRichest)",status_FAIL,getElement( Head( eth_storageRoot_temp ),"address",locals ).richest );
skip;
x3_WithdrawalGame_getRichest__7: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getRichest): set return status",status_OK>>;
InfrastructureServiceReturn( "WithdrawalGame(getRichest)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getRichest)" ) )
;
x3_WithdrawalGame_getRichest__exit:
goto x3_WithdrawalGame_getRichest__end;
x3_WithdrawalGame_getRichest__fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame(getRichest)", FALSE, Nil);
goto x3_WithdrawalGame_getRichest__end;
x3_WithdrawalGame_getRichest__abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame_getRichest_">>;
InfrastructureServiceReturn( "WithdrawalGame(getRichest)", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame_getRichest__exit" );
x3_WithdrawalGame_getRichest__end:
ethereum_service_pop( "WithdrawalGame(getRichest)" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame_getRichest_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getRichest__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame(getMostSent) --> x3_WithdrawalGame_getMostSent_ *)
(* solidity_contract_function:WithdrawalGame(getMostSent) - Service procedure for WithdrawalGame(getMostSent) *)
procedure x3_WithdrawalGame_getMostSent_( x3_WithdrawalGame_getMostSent__input )
variable locals;
{
x3_WithdrawalGame_getMostSent__start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame_getMostSent_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getMostSent__input>>;
skip
;
(* body of WithdrawalGame(getMostSent) *)
x3_WithdrawalGame_getMostSent__0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame_getMostSent__1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame_getMostSent__abort
;
x3_WithdrawalGame_getMostSent__2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame_getMostSent__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getMostSent__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame_getMostSent__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getMostSent__input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame_getMostSent__input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(getMostSent): abort">>;
goto x3_WithdrawalGame_getMostSent__abort
;
}
;
x3_WithdrawalGame_getMostSent__3: skip;
locals := x3_WithdrawalGame_getMostSent__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_WithdrawalGame_getMostSent__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_WithdrawalGame_getMostSent__input.recipient ])
;
x3_WithdrawalGame_getMostSent__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame_getMostSent__input.sender # x3_WithdrawalGame_getMostSent__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getMostSent__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getMostSent__input.value ] ELSE IF a.address = x3_WithdrawalGame_getMostSent__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getMostSent__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): moved value">>;
skip
;
x3_WithdrawalGame_getMostSent__call_construct: InfrastructureServiceReturn( "WithdrawalGame(getMostSent)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getMostSent)" ) );
goto x3_WithdrawalGame_getMostSent__end;
};
x3_WithdrawalGame_getMostSent__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "WithdrawalGame" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): wrong type">>;
goto x3_WithdrawalGame_getMostSent__abort
;
};
x3_WithdrawalGame_getMostSent__6: if ( x3_WithdrawalGame_getMostSent__input.sender # x3_WithdrawalGame_getMostSent__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getMostSent__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getMostSent__input.value ] ELSE IF a.address = x3_WithdrawalGame_getMostSent__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getMostSent__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): moved value">>;
skip
;
InfrastructureServiceReturn( "WithdrawalGame(getMostSent)",status_FAIL,getElement( Head( eth_storageRoot_temp ),"address",locals ).mostSent );
skip;
x3_WithdrawalGame_getMostSent__7: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getMostSent): set return status",status_OK>>;
InfrastructureServiceReturn( "WithdrawalGame(getMostSent)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getMostSent)" ) )
;
x3_WithdrawalGame_getMostSent__exit:
goto x3_WithdrawalGame_getMostSent__end;
x3_WithdrawalGame_getMostSent__fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame(getMostSent)", FALSE, Nil);
goto x3_WithdrawalGame_getMostSent__end;
x3_WithdrawalGame_getMostSent__abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame_getMostSent_">>;
InfrastructureServiceReturn( "WithdrawalGame(getMostSent)", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame_getMostSent__exit" );
x3_WithdrawalGame_getMostSent__end:
ethereum_service_pop( "WithdrawalGame(getMostSent)" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame_getMostSent_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getMostSent__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame(getPendingWithdrawals) --> x3_WithdrawalGame_getPendingWithdrawals_ *)
(* solidity_contract_function:WithdrawalGame(getPendingWithdrawals) - Service procedure for WithdrawalGame(getPendingWithdrawals) *)
procedure x3_WithdrawalGame_getPendingWithdrawals_( x3_WithdrawalGame_getPendingWithdrawals__input )
variable locals;
{
x3_WithdrawalGame_getPendingWithdrawals__start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame_getPendingWithdrawals_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getPendingWithdrawals__input>>;
skip
;
(* body of WithdrawalGame(getPendingWithdrawals) *)
x3_WithdrawalGame_getPendingWithdrawals__0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame_getPendingWithdrawals__1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame_getPendingWithdrawals__abort
;
x3_WithdrawalGame_getPendingWithdrawals__2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame_getPendingWithdrawals__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getPendingWithdrawals__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame_getPendingWithdrawals__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getPendingWithdrawals__input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame_getPendingWithdrawals__input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(getPendingWithdrawals): abort">>;
goto x3_WithdrawalGame_getPendingWithdrawals__abort
;
}
;
x3_WithdrawalGame_getPendingWithdrawals__3: skip;
locals := x3_WithdrawalGame_getPendingWithdrawals__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_WithdrawalGame_getPendingWithdrawals__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_WithdrawalGame_getPendingWithdrawals__input.recipient ])
;
x3_WithdrawalGame_getPendingWithdrawals__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame_getPendingWithdrawals__input.sender # x3_WithdrawalGame_getPendingWithdrawals__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getPendingWithdrawals__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getPendingWithdrawals__input.value ] ELSE IF a.address = x3_WithdrawalGame_getPendingWithdrawals__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getPendingWithdrawals__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): moved value">>;
skip
;
x3_WithdrawalGame_getPendingWithdrawals__call_construct: InfrastructureServiceReturn( "WithdrawalGame(getPendingWithdrawals)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getPendingWithdrawals)" ) );
goto x3_WithdrawalGame_getPendingWithdrawals__end;
};
x3_WithdrawalGame_getPendingWithdrawals__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "WithdrawalGame" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): wrong type">>;
goto x3_WithdrawalGame_getPendingWithdrawals__abort
;
};
x3_WithdrawalGame_getPendingWithdrawals__6: if ( x3_WithdrawalGame_getPendingWithdrawals__input.sender # x3_WithdrawalGame_getPendingWithdrawals__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getPendingWithdrawals__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getPendingWithdrawals__input.value ] ELSE IF a.address = x3_WithdrawalGame_getPendingWithdrawals__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getPendingWithdrawals__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): moved value">>;
skip
;
InfrastructureServiceReturn( "WithdrawalGame(getPendingWithdrawals)",status_FAIL,getElement( Head( eth_storageRoot_temp ),"address",locals ).pendingWithdrawals );
skip;
x3_WithdrawalGame_getPendingWithdrawals__7: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getPendingWithdrawals): set return status",status_OK>>;
InfrastructureServiceReturn( "WithdrawalGame(getPendingWithdrawals)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getPendingWithdrawals)" ) )
;
x3_WithdrawalGame_getPendingWithdrawals__exit:
goto x3_WithdrawalGame_getPendingWithdrawals__end;
x3_WithdrawalGame_getPendingWithdrawals__fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame(getPendingWithdrawals)", FALSE, Nil);
goto x3_WithdrawalGame_getPendingWithdrawals__end;
x3_WithdrawalGame_getPendingWithdrawals__abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame_getPendingWithdrawals_">>;
InfrastructureServiceReturn( "WithdrawalGame(getPendingWithdrawals)", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame_getPendingWithdrawals__exit" );
x3_WithdrawalGame_getPendingWithdrawals__end:
ethereum_service_pop( "WithdrawalGame(getPendingWithdrawals)" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame_getPendingWithdrawals_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getPendingWithdrawals__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:WithdrawalGame(getAddress) --> x3_WithdrawalGame_getAddress_ *)
(* solidity_contract_function:WithdrawalGame(getAddress) - Service procedure for WithdrawalGame(getAddress) *)
procedure x3_WithdrawalGame_getAddress_( x3_WithdrawalGame_getAddress__input )
variable locals;
{
x3_WithdrawalGame_getAddress__start:
\* print <<"TRACE>","ENTRY:","x3_WithdrawalGame_getAddress_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getAddress__input>>;
skip
;
(* body of WithdrawalGame(getAddress) *)
x3_WithdrawalGame_getAddress__0: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_WithdrawalGame_getAddress__1: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): non-deterministic out-of-gas-check">>;
either skip or goto x3_WithdrawalGame_getAddress__abort
;
x3_WithdrawalGame_getAddress__2: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): check sender balance >= gasValue(transactionGas) + value",x3_WithdrawalGame_getAddress__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getAddress__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_WithdrawalGame_getAddress__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_WithdrawalGame_getAddress__input.sender ).balance < ( gasValue( transactionGas ) + x3_WithdrawalGame_getAddress__input.value ) ) {
\* print <<"TRACE>","SVC-EXECWithdrawalGame(getAddress): abort">>;
goto x3_WithdrawalGame_getAddress__abort
;
}
;
x3_WithdrawalGame_getAddress__3: skip;
locals := x3_WithdrawalGame_getAddress__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_WithdrawalGame_getAddress__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_WithdrawalGame_getAddress__input.recipient ])
;
x3_WithdrawalGame_getAddress__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ richest |-> Nil, mostSent |-> 0, pendingWithdrawals |-> [ a \in d_eth_address |-> 0 ], address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_WithdrawalGame_getAddress__input.sender # x3_WithdrawalGame_getAddress__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getAddress__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getAddress__input.value ] ELSE IF a.address = x3_WithdrawalGame_getAddress__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getAddress__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): moved value">>;
skip
;
x3_WithdrawalGame_getAddress__call_construct: InfrastructureServiceReturn( "WithdrawalGame(getAddress)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getAddress)" ) );
goto x3_WithdrawalGame_getAddress__end;
};
x3_WithdrawalGame_getAddress__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "WithdrawalGame" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): wrong type">>;
goto x3_WithdrawalGame_getAddress__abort
;
};
x3_WithdrawalGame_getAddress__6: if ( x3_WithdrawalGame_getAddress__input.sender # x3_WithdrawalGame_getAddress__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_WithdrawalGame_getAddress__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_WithdrawalGame_getAddress__input.value ] ELSE IF a.address = x3_WithdrawalGame_getAddress__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_WithdrawalGame_getAddress__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): moved value">>;
skip
;
InfrastructureServiceReturn( "WithdrawalGame(getAddress)",status_FAIL,getElement( Head( eth_storageRoot_temp ),"address",locals ).address );
skip;
x3_WithdrawalGame_getAddress__7: \* print <<"TRACE>","SVC-exec@WithdrawalGame(getAddress): set return status",status_OK>>;
InfrastructureServiceReturn( "WithdrawalGame(getAddress)",status_OK,InfrastructureServiceGetResponse( "WithdrawalGame(getAddress)" ) )
;
x3_WithdrawalGame_getAddress__exit:
goto x3_WithdrawalGame_getAddress__end;
x3_WithdrawalGame_getAddress__fail:
\* throw command sends here
InfrastructureServiceReturn( "WithdrawalGame(getAddress)", FALSE, Nil);
goto x3_WithdrawalGame_getAddress__end;
x3_WithdrawalGame_getAddress__abort:
\* should not happen??
print <<"ABORT x3_WithdrawalGame_getAddress_">>;
InfrastructureServiceReturn( "WithdrawalGame(getAddress)", Abort, Nil);
\* schedule_throw( "x3_WithdrawalGame_getAddress__exit" );
x3_WithdrawalGame_getAddress__end:
ethereum_service_pop( "WithdrawalGame(getAddress)" );
\* print <<"TRACE>","EXIT:","x3_WithdrawalGame_getAddress_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_WithdrawalGame_getAddress__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:FairPlayer(play) --> x3_FairPlayer_play_ *)
(* solidity_contract_function:FairPlayer(play) - Service procedure for FairPlayer(play) *)
procedure x3_FairPlayer_play_( x3_FairPlayer_play__input )
variable locals;
{
x3_FairPlayer_play__start:
\* print <<"TRACE>","ENTRY:","x3_FairPlayer_play_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_play__input>>;
skip
;
(* body of FairPlayer(play) *)
x3_FairPlayer_play__0: \* print <<"TRACE>","SVC-exec@FairPlayer(play): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_FairPlayer_play__1: \* print <<"TRACE>","SVC-exec@FairPlayer(play): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@FairPlayer(play): non-deterministic out-of-gas-check">>;
either skip or goto x3_FairPlayer_play__abort
;
x3_FairPlayer_play__2: \* print <<"TRACE>","SVC-exec@FairPlayer(play): check sender balance >= gasValue(transactionGas) + value",x3_FairPlayer_play__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_play__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_FairPlayer_play__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_play__input.sender ).balance < ( gasValue( transactionGas ) + x3_FairPlayer_play__input.value ) ) {
\* print <<"TRACE>","SVC-EXECFairPlayer(play): abort">>;
goto x3_FairPlayer_play__abort
;
}
;
x3_FairPlayer_play__3: skip;
locals := x3_FairPlayer_play__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_FairPlayer_play__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(play): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_FairPlayer_play__input.recipient ])
;
x3_FairPlayer_play__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@FairPlayer(play): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ game |-> Nil, address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_FairPlayer_play__input.sender # x3_FairPlayer_play__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_play__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_play__input.value ] ELSE IF a.address = x3_FairPlayer_play__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_play__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(play): moved value">>;
skip
;
x3_FairPlayer_play__call_construct: InfrastructureServiceReturn( "FairPlayer(play)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(play)" ) );
goto x3_FairPlayer_play__end;
};
x3_FairPlayer_play__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "FairPlayer" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(play): wrong type">>;
goto x3_FairPlayer_play__abort
;
};
x3_FairPlayer_play__6: if ( x3_FairPlayer_play__input.sender # x3_FairPlayer_play__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_play__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_play__input.value ] ELSE IF a.address = x3_FairPlayer_play__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_play__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(play): moved value">>;
skip
;
if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",getElement( Head( eth_storageRoot_temp ),"address",locals ).game ) ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(play): abort because called address of contract does not exist">>;
goto x3_FairPlayer_play__abort
;
};
x3_FairPlayer_play__7: call x3_WithdrawalGame_becomeRichest_( [ recipient |-> getElement( Head( eth_storageRoot_temp ),"address",locals ).game, sender |-> locals, originator |-> x3_FairPlayer_play__input.originator, value |-> 2 ]);
x3_FairPlayer_play__8: if ( Abort = InfrastructureServiceGetStatus( "WithdrawalGame(becomeRichest)" ) ) {
goto x3_FairPlayer_play__abort;
};
x3_FairPlayer_play__9: skip;
x3_FairPlayer_play__10: \* print <<"TRACE>","SVC-exec@FairPlayer(play): set return status",status_OK>>;
InfrastructureServiceReturn( "FairPlayer(play)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(play)" ) )
;
x3_FairPlayer_play__exit:
goto x3_FairPlayer_play__end;
x3_FairPlayer_play__fail:
\* throw command sends here
InfrastructureServiceReturn( "FairPlayer(play)", FALSE, Nil);
goto x3_FairPlayer_play__end;
x3_FairPlayer_play__abort:
\* should not happen??
print <<"ABORT x3_FairPlayer_play_">>;
InfrastructureServiceReturn( "FairPlayer(play)", Abort, Nil);
\* schedule_throw( "x3_FairPlayer_play__exit" );
x3_FairPlayer_play__end:
ethereum_service_pop( "FairPlayer(play)" );
\* print <<"TRACE>","EXIT:","x3_FairPlayer_play_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_play__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:FairPlayer(endGame) --> x3_FairPlayer_endGame_ *)
(* solidity_contract_function:FairPlayer(endGame) - Service procedure for FairPlayer(endGame) *)
procedure x3_FairPlayer_endGame_( x3_FairPlayer_endGame__input )
variable locals;
{
x3_FairPlayer_endGame__start:
\* print <<"TRACE>","ENTRY:","x3_FairPlayer_endGame_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_endGame__input>>;
skip
;
(* body of FairPlayer(endGame) *)
x3_FairPlayer_endGame__0: \* print <<"TRACE>","SVC-exec@FairPlayer(endGame): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_FairPlayer_endGame__1: \* print <<"TRACE>","SVC-exec@FairPlayer(endGame): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): non-deterministic out-of-gas-check">>;
either skip or goto x3_FairPlayer_endGame__abort
;
x3_FairPlayer_endGame__2: \* print <<"TRACE>","SVC-exec@FairPlayer(endGame): check sender balance >= gasValue(transactionGas) + value",x3_FairPlayer_endGame__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_endGame__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_FairPlayer_endGame__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_endGame__input.sender ).balance < ( gasValue( transactionGas ) + x3_FairPlayer_endGame__input.value ) ) {
\* print <<"TRACE>","SVC-EXECFairPlayer(endGame): abort">>;
goto x3_FairPlayer_endGame__abort
;
}
;
x3_FairPlayer_endGame__3: skip;
locals := x3_FairPlayer_endGame__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_FairPlayer_endGame__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_FairPlayer_endGame__input.recipient ])
;
x3_FairPlayer_endGame__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ game |-> Nil, address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_FairPlayer_endGame__input.sender # x3_FairPlayer_endGame__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_endGame__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_endGame__input.value ] ELSE IF a.address = x3_FairPlayer_endGame__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_endGame__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): moved value">>;
skip
;
x3_FairPlayer_endGame__call_construct: InfrastructureServiceReturn( "FairPlayer(endGame)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(endGame)" ) );
goto x3_FairPlayer_endGame__end;
};
x3_FairPlayer_endGame__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "FairPlayer" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): wrong type">>;
goto x3_FairPlayer_endGame__abort
;
};
x3_FairPlayer_endGame__6: if ( x3_FairPlayer_endGame__input.sender # x3_FairPlayer_endGame__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_endGame__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_endGame__input.value ] ELSE IF a.address = x3_FairPlayer_endGame__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_endGame__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): moved value">>;
skip
;
if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",getElement( Head( eth_storageRoot_temp ),"address",locals ).game ) ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(endGame): abort because called address of contract does not exist">>;
goto x3_FairPlayer_endGame__abort
;
};
x3_FairPlayer_endGame__7: call x3_WithdrawalGame_withdraw_( [ recipient |-> getElement( Head( eth_storageRoot_temp ),"address",locals ).game, sender |-> locals, originator |-> x3_FairPlayer_endGame__input.originator, value |-> 0 ]);
x3_FairPlayer_endGame__8: if ( Abort = InfrastructureServiceGetStatus( "WithdrawalGame(withdraw)" ) ) {
goto x3_FairPlayer_endGame__abort;
};
x3_FairPlayer_endGame__9: skip;
x3_FairPlayer_endGame__10: \* print <<"TRACE>","SVC-exec@FairPlayer(endGame): set return status",status_OK>>;
InfrastructureServiceReturn( "FairPlayer(endGame)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(endGame)" ) )
;
x3_FairPlayer_endGame__exit:
goto x3_FairPlayer_endGame__end;
x3_FairPlayer_endGame__fail:
\* throw command sends here
InfrastructureServiceReturn( "FairPlayer(endGame)", FALSE, Nil);
goto x3_FairPlayer_endGame__end;
x3_FairPlayer_endGame__abort:
\* should not happen??
print <<"ABORT x3_FairPlayer_endGame_">>;
InfrastructureServiceReturn( "FairPlayer(endGame)", Abort, Nil);
\* schedule_throw( "x3_FairPlayer_endGame__exit" );
x3_FairPlayer_endGame__end:
ethereum_service_pop( "FairPlayer(endGame)" );
\* print <<"TRACE>","EXIT:","x3_FairPlayer_endGame_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_endGame__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:FairPlayer() --> x3_FairPlayer__ *)
(* solidity_contract_function:FairPlayer() - Constructor for contract FairPlayer()' *)
procedure x3_FairPlayer__( x3_FairPlayer___input )
variable locals;
{
x3_FairPlayer___start:
\* print <<"TRACE>","ENTRY:","x3_FairPlayer__","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer___input>>;
skip
;
(* body of FairPlayer() *)
x3_FairPlayer___0: \* print <<"TRACE>","SVC-exec@FairPlayer(): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_FairPlayer___1: \* print <<"TRACE>","SVC-exec@FairPlayer(): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@FairPlayer(): non-deterministic out-of-gas-check">>;
either skip or goto x3_FairPlayer___abort
;
x3_FairPlayer___2: \* print <<"TRACE>","SVC-exec@FairPlayer(): check sender balance >= gasValue(transactionGas) + value",x3_FairPlayer___input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer___input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_FairPlayer___input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer___input.sender ).balance < ( gasValue( transactionGas ) + x3_FairPlayer___input.value ) ) {
\* print <<"TRACE>","SVC-EXECFairPlayer(): abort">>;
goto x3_FairPlayer___abort
;
}
;
x3_FairPlayer___3: skip;
\* print <<"TRACE>","SVC-exec@FairPlayer(): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> "FairPlayer", address |-> Nil ])
;
x3_FairPlayer___4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@FairPlayer(): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ game |-> Nil, address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_FairPlayer___input.sender # InfrastructureServiceGetResponse( "personal_newAccount()" ) ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = InfrastructureServiceGetResponse( "personal_newAccount()" ) THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer___input.value ] ELSE IF a.address = x3_FairPlayer___input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer___input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(): moved value">>;
skip
;
\* print <<"TRACE>","SVC-exec@FairPlayer(): process constructor body">>;
x3_FairPlayer____body: skip
;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ IF a.address = locals THEN [ a EXCEPT !.game = x3_FairPlayer___input.g ] ELSE a : a \in Head( eth_storageRoot_temp ) } );
\* print <<"TRACE>","SVC-exec@FairPlayer(): set return status",status_OK,"return account id created",locals>>;
InfrastructureServiceReturn( "FairPlayer()",status_OK,locals )
;
skip;
x3_FairPlayer___exit:
goto x3_FairPlayer___end;
x3_FairPlayer___fail:
\* throw command sends here
InfrastructureServiceReturn( "FairPlayer()", FALSE, Nil);
goto x3_FairPlayer___end;
x3_FairPlayer___abort:
\* should not happen??
print <<"ABORT x3_FairPlayer__">>;
InfrastructureServiceReturn( "FairPlayer()", Abort, Nil);
\* schedule_throw( "x3_FairPlayer___exit" );
x3_FairPlayer___end:
ethereum_service_pop( "FairPlayer()" );
\* print <<"TRACE>","EXIT:","x3_FairPlayer__","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer___input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:FairPlayer(getGame) --> x3_FairPlayer_getGame_ *)
(* solidity_contract_function:FairPlayer(getGame) - Service procedure for FairPlayer(getGame) *)
procedure x3_FairPlayer_getGame_( x3_FairPlayer_getGame__input )
variable locals;
{
x3_FairPlayer_getGame__start:
\* print <<"TRACE>","ENTRY:","x3_FairPlayer_getGame_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_getGame__input>>;
skip
;
(* body of FairPlayer(getGame) *)
x3_FairPlayer_getGame__0: \* print <<"TRACE>","SVC-exec@FairPlayer(getGame): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_FairPlayer_getGame__1: \* print <<"TRACE>","SVC-exec@FairPlayer(getGame): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@FairPlayer(getGame): non-deterministic out-of-gas-check">>;
either skip or goto x3_FairPlayer_getGame__abort
;
x3_FairPlayer_getGame__2: \* print <<"TRACE>","SVC-exec@FairPlayer(getGame): check sender balance >= gasValue(transactionGas) + value",x3_FairPlayer_getGame__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_getGame__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_FairPlayer_getGame__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_getGame__input.sender ).balance < ( gasValue( transactionGas ) + x3_FairPlayer_getGame__input.value ) ) {
\* print <<"TRACE>","SVC-EXECFairPlayer(getGame): abort">>;
goto x3_FairPlayer_getGame__abort
;
}
;
x3_FairPlayer_getGame__3: skip;
locals := x3_FairPlayer_getGame__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_FairPlayer_getGame__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(getGame): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_FairPlayer_getGame__input.recipient ])
;
x3_FairPlayer_getGame__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@FairPlayer(getGame): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ game |-> Nil, address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_FairPlayer_getGame__input.sender # x3_FairPlayer_getGame__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_getGame__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_getGame__input.value ] ELSE IF a.address = x3_FairPlayer_getGame__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_getGame__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(getGame): moved value">>;
skip
;
x3_FairPlayer_getGame__call_construct: InfrastructureServiceReturn( "FairPlayer(getGame)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(getGame)" ) );
goto x3_FairPlayer_getGame__end;
};
x3_FairPlayer_getGame__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "FairPlayer" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(getGame): wrong type">>;
goto x3_FairPlayer_getGame__abort
;
};
x3_FairPlayer_getGame__6: if ( x3_FairPlayer_getGame__input.sender # x3_FairPlayer_getGame__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_getGame__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_getGame__input.value ] ELSE IF a.address = x3_FairPlayer_getGame__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_getGame__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(getGame): moved value">>;
skip
;
InfrastructureServiceReturn( "FairPlayer(getGame)",status_FAIL,getElement( Head( eth_storageRoot_temp ),"address",locals ).game );
skip;
x3_FairPlayer_getGame__7: \* print <<"TRACE>","SVC-exec@FairPlayer(getGame): set return status",status_OK>>;
InfrastructureServiceReturn( "FairPlayer(getGame)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(getGame)" ) )
;
x3_FairPlayer_getGame__exit:
goto x3_FairPlayer_getGame__end;
x3_FairPlayer_getGame__fail:
\* throw command sends here
InfrastructureServiceReturn( "FairPlayer(getGame)", FALSE, Nil);
goto x3_FairPlayer_getGame__end;
x3_FairPlayer_getGame__abort:
\* should not happen??
print <<"ABORT x3_FairPlayer_getGame_">>;
InfrastructureServiceReturn( "FairPlayer(getGame)", Abort, Nil);
\* schedule_throw( "x3_FairPlayer_getGame__exit" );
x3_FairPlayer_getGame__end:
ethereum_service_pop( "FairPlayer(getGame)" );
\* print <<"TRACE>","EXIT:","x3_FairPlayer_getGame_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_getGame__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(* ETH-SNIPPET: solidity_contract_function:FairPlayer(getAddress) --> x3_FairPlayer_getAddress_ *)
(* solidity_contract_function:FairPlayer(getAddress) - Service procedure for FairPlayer(getAddress) *)
procedure x3_FairPlayer_getAddress_( x3_FairPlayer_getAddress__input )
variable locals;
{
x3_FairPlayer_getAddress__start:
\* print <<"TRACE>","ENTRY:","x3_FairPlayer_getAddress_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_getAddress__input>>;
skip
;
(* body of FairPlayer(getAddress) *)
x3_FairPlayer_getAddress__0: \* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): persist accounts">>;
eth_accounts := Head( eth_accounts_temp )
;
skip;
x3_FairPlayer_getAddress__1: \* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): init return status",Abort>>;
ethereum_service_push()
;
\* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): non-deterministic out-of-gas-check">>;
either skip or goto x3_FairPlayer_getAddress__abort
;
x3_FairPlayer_getAddress__2: \* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): check sender balance >= gasValue(transactionGas) + value",x3_FairPlayer_getAddress__input.sender,"balance",getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_getAddress__input.sender ).balance,"value needed",( gasValue( transactionGas ) + x3_FairPlayer_getAddress__input.value )>>;
if ( getElement( Head( eth_accounts_temp ),"address",x3_FairPlayer_getAddress__input.sender ).balance < ( gasValue( transactionGas ) + x3_FairPlayer_getAddress__input.value ) ) {
\* print <<"TRACE>","SVC-EXECFairPlayer(getAddress): abort">>;
goto x3_FairPlayer_getAddress__abort
;
}
;
x3_FairPlayer_getAddress__3: skip;
locals := x3_FairPlayer_getAddress__input.recipient;
if ( ~ elementExists( eth_accounts,"address",x3_FairPlayer_getAddress__input.recipient ) ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): call 'personal_newAccount' to create new account entry">>;
call eth_personal_newAccount( [ codeHash |-> Nil, address |-> x3_FairPlayer_getAddress__input.recipient ])
;
x3_FairPlayer_getAddress__4: locals := InfrastructureServiceGetResponse( "personal_newAccount()" );
\* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): create contract entry to storageRoot_temp">>;
eth_storageRoot_temp := UpdateTop( eth_storageRoot_temp,{ [ game |-> Nil, address |-> InfrastructureServiceGetResponse( "personal_newAccount()" ) ] } \union Head( eth_storageRoot_temp ) )
;
if ( x3_FairPlayer_getAddress__input.sender # x3_FairPlayer_getAddress__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_getAddress__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_getAddress__input.value ] ELSE IF a.address = x3_FairPlayer_getAddress__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_getAddress__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): moved value">>;
skip
;
x3_FairPlayer_getAddress__call_construct: InfrastructureServiceReturn( "FairPlayer(getAddress)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(getAddress)" ) );
goto x3_FairPlayer_getAddress__end;
};
x3_FairPlayer_getAddress__5: if ( ~ elementExists( Head( eth_storageRoot_temp ),"address",locals ) \/ "FairPlayer" # getElement( Head( eth_accounts_temp ),"address",locals ).codeHash ) {
\* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): wrong type">>;
goto x3_FairPlayer_getAddress__abort
;
};
x3_FairPlayer_getAddress__6: if ( x3_FairPlayer_getAddress__input.sender # x3_FairPlayer_getAddress__input.recipient ) {
eth_accounts_temp := UpdateTop( eth_accounts_temp,{ IF a.address = x3_FairPlayer_getAddress__input.recipient THEN [ a EXCEPT !.balance = a.balance + x3_FairPlayer_getAddress__input.value ] ELSE IF a.address = x3_FairPlayer_getAddress__input.sender THEN [ a EXCEPT !.balance = a.balance - x3_FairPlayer_getAddress__input.value ] ELSE a : a \in Head( eth_accounts_temp ) } );
};
\* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): moved value">>;
skip
;
InfrastructureServiceReturn( "FairPlayer(getAddress)",status_FAIL,getElement( Head( eth_storageRoot_temp ),"address",locals ).address );
skip;
x3_FairPlayer_getAddress__7: \* print <<"TRACE>","SVC-exec@FairPlayer(getAddress): set return status",status_OK>>;
InfrastructureServiceReturn( "FairPlayer(getAddress)",status_OK,InfrastructureServiceGetResponse( "FairPlayer(getAddress)" ) )
;
x3_FairPlayer_getAddress__exit:
goto x3_FairPlayer_getAddress__end;
x3_FairPlayer_getAddress__fail:
\* throw command sends here
InfrastructureServiceReturn( "FairPlayer(getAddress)", FALSE, Nil);
goto x3_FairPlayer_getAddress__end;
x3_FairPlayer_getAddress__abort:
\* should not happen??
print <<"ABORT x3_FairPlayer_getAddress_">>;
InfrastructureServiceReturn( "FairPlayer(getAddress)", Abort, Nil);
\* schedule_throw( "x3_FairPlayer_getAddress__exit" );
x3_FairPlayer_getAddress__end:
ethereum_service_pop( "FairPlayer(getAddress)" );
\* print <<"TRACE>","EXIT:","x3_FairPlayer_getAddress_","accounts_temp",eth_accounts_temp,"storageRoot_temp",eth_storageRoot_temp,"mined",eth_mined,"input",x3_FairPlayer_getAddress__input>>;
return
;
}
(* ETH-SNIPPET-END *)
(******************************************************************
Interfaces generated Process interfaces
- modelData interfaces
- template interface_processes.mustache
******************************************************************)
(* Process personal_newAccount() *)
fair process (p_personal_newAccount__="personal_newAccount()") {
p_personal_newAccount___enter: while (TRUE) {
enable( "p_personal_newAccount__" );
(* enable next process to run parallel *)
\* process_done( "personal_newAccount()" );
with ( _input \in { t \in ProcessParameterInput( t_req_personal_newAccount__ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_personal_newAccount__ for operation 'personal_newAccount()',tick=", currentTime>>;
(* Valid input type? - API configuration did not define any parameters - must have Nil for _input.dummy: *)
assert( _input.dummy = Nil );
i__personal_newAccount__( _input );
}; \* with _input
(* enable next process - after current process *)
p_personal_newAccount___exit:
personal_newAccount_done( "personal_newAccount()" );
process_done( "personal_newAccount()" );
} \* while(TRUE)
} \* fair process p_personal_newAccount__
(* Process geth_mine() *)
fair process (p_geth_mine__="geth_mine()") {
p_geth_mine___enter: while (TRUE) {
enable( "p_geth_mine__" );
(* enable next process to run parallel *)
\* process_done( "geth_mine()" );
with ( _input \in { t \in ProcessParameterInput( t_req_geth_mine__ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_geth_mine__ for operation 'geth_mine()',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_geth_mine__ );
i__geth_mine__( _input );
}; \* with _input
(* enable next process - after current process *)
p_geth_mine___exit:
process_done( "geth_mine()" );
} \* while(TRUE)
} \* fair process p_geth_mine__
(* Process GlobalScope(send) *)
fair process (p_GlobalScope_send_="GlobalScope(send)") {
p_GlobalScope_send__enter: while (TRUE) {
enable( "p_GlobalScope_send_" );
(* enable next process to run parallel *)
\* process_done( "GlobalScope(send)" );
with ( _input \in { t \in ProcessParameterInput( t_req_GlobalScope_send_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_GlobalScope_send_ for operation 'GlobalScope(send)',tick=", currentTime>>;
\* print <<" - input=>", _input >>;
(* print <<" - t_req_GlobalScope_send_ =>", t_req_GlobalScope_send_ >>; *)
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_GlobalScope_send_ );
}; \* with _input
(* enable next process - after current process *)
p_GlobalScope_send__exit:
process_done( "GlobalScope(send)" );
} \* while(TRUE)
} \* fair process p_GlobalScope_send_
(* Process WithdrawalGame(becomeRichest) *)
fair process (p_WithdrawalGame_becomeRichest_="WithdrawalGame(becomeRichest)") {
p_WithdrawalGame_becomeRichest__enter: while (TRUE) {
enable( "p_WithdrawalGame_becomeRichest_" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame(becomeRichest)" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame_becomeRichest_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame_becomeRichest_ for operation 'WithdrawalGame(becomeRichest)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame_becomeRichest_ );
i__WithdrawalGame_becomeRichest_( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame_becomeRichest__exit:
ethereum_service_done( "WithdrawalGame(becomeRichest)" );
process_done( "WithdrawalGame(becomeRichest)" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame_becomeRichest_
(* Process WithdrawalGame() *)
fair process (p_WithdrawalGame__="WithdrawalGame()") {
p_WithdrawalGame___enter: while (TRUE) {
enable( "p_WithdrawalGame__" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame()" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame__ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame__ for operation 'WithdrawalGame()',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame__ );
i__WithdrawalGame__( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame___exit:
ethereum_service_done( "WithdrawalGame()" );
process_done( "WithdrawalGame()" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame__
(* Process WithdrawalGame(withdraw) *)
fair process (p_WithdrawalGame_withdraw_="WithdrawalGame(withdraw)") {
p_WithdrawalGame_withdraw__enter: while (TRUE) {
enable( "p_WithdrawalGame_withdraw_" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame(withdraw)" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame_withdraw_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame_withdraw_ for operation 'WithdrawalGame(withdraw)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame_withdraw_ );
i__WithdrawalGame_withdraw_( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame_withdraw__exit:
ethereum_service_done( "WithdrawalGame(withdraw)" );
process_done( "WithdrawalGame(withdraw)" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame_withdraw_
(* Process WithdrawalGame(getRichest) *)
fair process (p_WithdrawalGame_getRichest_="WithdrawalGame(getRichest)") {
p_WithdrawalGame_getRichest__enter: while (TRUE) {
enable( "p_WithdrawalGame_getRichest_" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame(getRichest)" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame_getRichest_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame_getRichest_ for operation 'WithdrawalGame(getRichest)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame_getRichest_ );
i__WithdrawalGame_getRichest_( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame_getRichest__exit:
ethereum_service_done( "WithdrawalGame(getRichest)" );
process_done( "WithdrawalGame(getRichest)" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame_getRichest_
(* Process WithdrawalGame(getMostSent) *)
fair process (p_WithdrawalGame_getMostSent_="WithdrawalGame(getMostSent)") {
p_WithdrawalGame_getMostSent__enter: while (TRUE) {
enable( "p_WithdrawalGame_getMostSent_" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame(getMostSent)" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame_getMostSent_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame_getMostSent_ for operation 'WithdrawalGame(getMostSent)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame_getMostSent_ );
i__WithdrawalGame_getMostSent_( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame_getMostSent__exit:
ethereum_service_done( "WithdrawalGame(getMostSent)" );
process_done( "WithdrawalGame(getMostSent)" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame_getMostSent_
(* Process WithdrawalGame(getPendingWithdrawals) *)
fair process (p_WithdrawalGame_getPendingWithdrawals_="WithdrawalGame(getPendingWithdrawals)") {
p_WithdrawalGame_getPendingWithdrawals__enter: while (TRUE) {
enable( "p_WithdrawalGame_getPendingWithdrawals_" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame(getPendingWithdrawals)" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame_getPendingWithdrawals_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame_getPendingWithdrawals_ for operation 'WithdrawalGame(getPendingWithdrawals)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame_getPendingWithdrawals_ );
i__WithdrawalGame_getPendingWithdrawals_( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame_getPendingWithdrawals__exit:
ethereum_service_done( "WithdrawalGame(getPendingWithdrawals)" );
process_done( "WithdrawalGame(getPendingWithdrawals)" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame_getPendingWithdrawals_
(* Process WithdrawalGame(getAddress) *)
fair process (p_WithdrawalGame_getAddress_="WithdrawalGame(getAddress)") {
p_WithdrawalGame_getAddress__enter: while (TRUE) {
enable( "p_WithdrawalGame_getAddress_" );
(* enable next process to run parallel *)
\* process_done( "WithdrawalGame(getAddress)" );
with ( _input \in { t \in ProcessParameterInput( t_req_WithdrawalGame_getAddress_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_WithdrawalGame_getAddress_ for operation 'WithdrawalGame(getAddress)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_WithdrawalGame_getAddress_ );
i__WithdrawalGame_getAddress_( _input );
}; \* with _input
(* enable next process - after current process *)
p_WithdrawalGame_getAddress__exit:
ethereum_service_done( "WithdrawalGame(getAddress)" );
process_done( "WithdrawalGame(getAddress)" );
} \* while(TRUE)
} \* fair process p_WithdrawalGame_getAddress_
(* Process FairPlayer(play) *)
fair process (p_FairPlayer_play_="FairPlayer(play)") {
p_FairPlayer_play__enter: while (TRUE) {
enable( "p_FairPlayer_play_" );
(* enable next process to run parallel *)
\* process_done( "FairPlayer(play)" );
with ( _input \in { t \in ProcessParameterInput( t_req_FairPlayer_play_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_FairPlayer_play_ for operation 'FairPlayer(play)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_FairPlayer_play_ );
i__FairPlayer_play_( _input );
}; \* with _input
(* enable next process - after current process *)
p_FairPlayer_play__exit:
ethereum_service_done( "FairPlayer(play)" );
process_done( "FairPlayer(play)" );
} \* while(TRUE)
} \* fair process p_FairPlayer_play_
(* Process FairPlayer(endGame) *)
fair process (p_FairPlayer_endGame_="FairPlayer(endGame)") {
p_FairPlayer_endGame__enter: while (TRUE) {
enable( "p_FairPlayer_endGame_" );
(* enable next process to run parallel *)
\* process_done( "FairPlayer(endGame)" );
with ( _input \in { t \in ProcessParameterInput( t_req_FairPlayer_endGame_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_FairPlayer_endGame_ for operation 'FairPlayer(endGame)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_FairPlayer_endGame_ );
i__FairPlayer_endGame_( _input );
}; \* with _input
(* enable next process - after current process *)
p_FairPlayer_endGame__exit:
ethereum_service_done( "FairPlayer(endGame)" );
process_done( "FairPlayer(endGame)" );
} \* while(TRUE)
} \* fair process p_FairPlayer_endGame_
(* Process FairPlayer() *)
fair process (p_FairPlayer__="FairPlayer()") {
p_FairPlayer___enter: while (TRUE) {
enable( "p_FairPlayer__" );
(* enable next process to run parallel *)
\* process_done( "FairPlayer()" );
with ( _input \in { t \in ProcessParameterInput( t_req_FairPlayer__ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_FairPlayer__ for operation 'FairPlayer()',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_FairPlayer__ );
i__FairPlayer__( _input );
}; \* with _input
(* enable next process - after current process *)
p_FairPlayer___exit:
ethereum_service_done( "FairPlayer()" );
process_done( "FairPlayer()" );
} \* while(TRUE)
} \* fair process p_FairPlayer__
(* Process FairPlayer(getGame) *)
fair process (p_FairPlayer_getGame_="FairPlayer(getGame)") {
p_FairPlayer_getGame__enter: while (TRUE) {
enable( "p_FairPlayer_getGame_" );
(* enable next process to run parallel *)
\* process_done( "FairPlayer(getGame)" );
with ( _input \in { t \in ProcessParameterInput( t_req_FairPlayer_getGame_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_FairPlayer_getGame_ for operation 'FairPlayer(getGame)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_FairPlayer_getGame_ );
i__FairPlayer_getGame_( _input );
}; \* with _input
(* enable next process - after current process *)
p_FairPlayer_getGame__exit:
ethereum_service_done( "FairPlayer(getGame)" );
process_done( "FairPlayer(getGame)" );
} \* while(TRUE)
} \* fair process p_FairPlayer_getGame_
(* Process FairPlayer(getAddress) *)
fair process (p_FairPlayer_getAddress_="FairPlayer(getAddress)") {
p_FairPlayer_getAddress__enter: while (TRUE) {
enable( "p_FairPlayer_getAddress_" );
(* enable next process to run parallel *)
\* process_done( "FairPlayer(getAddress)" );
with ( _input \in { t \in ProcessParameterInput( t_req_FairPlayer_getAddress_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: false
\* print <<"Default process p_FairPlayer_getAddress_ for operation 'FairPlayer(getAddress)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t_req_FairPlayer_getAddress_ );
i__FairPlayer_getAddress_( _input );
}; \* with _input
(* enable next process - after current process *)
p_FairPlayer_getAddress__exit:
ethereum_service_done( "FairPlayer(getAddress)" );
process_done( "FairPlayer(getAddress)" );
} \* while(TRUE)
} \* fair process p_FairPlayer_getAddress_
fair process ( tail="Tail") {
tail_wait: await( Len(steps) = 0 );
step := "Tail";
step_parameter := {};
tail: while( TRUE ) {
skip;
}
}
} \* end of algorithm
*)
\* BEGIN TRANSLATION
\* Label tail of process tail at line 2692 col 15 changed to tail_
\* Procedure variable locals of procedure x3_GlobalScope_send_ at line 1292 col 14 changed to locals_
\* Procedure variable locals of procedure x3_WithdrawalGame_becomeRichest_ at line 1345 col 14 changed to locals_x
\* Procedure variable locals of procedure x3_WithdrawalGame__ at line 1439 col 14 changed to locals_x3
\* Procedure variable locals of procedure x3_WithdrawalGame_withdraw_ at line 1513 col 14 changed to locals_x3_
\* Procedure variable locals of procedure x3_WithdrawalGame_getRichest_ at line 1614 col 14 changed to locals_x3_W
\* Procedure variable locals of procedure x3_WithdrawalGame_getMostSent_ at line 1699 col 14 changed to locals_x3_Wi
\* Procedure variable locals of procedure x3_WithdrawalGame_getPendingWithdrawals_ at line 1784 col 14 changed to locals_x3_Wit
\* Procedure variable locals of procedure x3_WithdrawalGame_getAddress_ at line 1869 col 14 changed to locals_x3_With
\* Procedure variable locals of procedure x3_FairPlayer_play_ at line 1954 col 14 changed to locals_x3_F
\* Procedure variable locals of procedure x3_FairPlayer_endGame_ at line 2047 col 14 changed to locals_x3_Fa
\* Procedure variable locals of procedure x3_FairPlayer__ at line 2140 col 14 changed to locals_x3_Fai
\* Procedure variable locals of procedure x3_FairPlayer_getGame_ at line 2212 col 14 changed to locals_x3_Fair
\* Parameter input of procedure schedule_process_proc at line 1218 col 40 changed to input_
\* Parameter input of procedure eth_personal_newAccount at line 1237 col 36 changed to input_e
CONSTANT defaultInitValue
VARIABLES steps, step, step_parameter, now, tx_running, resume_context,
responses, eth_accounts, eth_storageRoot, eth_storageRoot_temp,
eth_accounts_temp, eth_address_free, eth_mined, pc, stack
(* define statement *)
currentTime == now
ProcessParameterInput( inputSet ) ==
IF step_parameter'.bindSet = Nil
THEN inputSet
ELSE step_parameter'.bindSet
RECURSIVE ProcessParameterEnables( _, _ )
ProcessParameterEnables( inputParam, bindDefs ) ==
( \A key \in { k \in DOMAIN bindDefs : Len(k)<4 \/ (SubSeq(k,1,4) # "_key" /\ k # "_rows" )}: bindDefs[key] = inputParam[key] )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : Len(k)>3 /\SubSeq(k,1,4) = "_key" }: \A r \in bindDefs[reckey] : ProcessParameterEnables( inputParam[r.key], r.rec ) )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_rows" }: \A r \in bindDefs[reckey] :
(r.row_types = "singletons" /\ r.set = inputParam[r.key] )
\/ (r.row_types = "hashes" /\ Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\ \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef ) )
)
ProcessParameterBind( inputParam ) ==
\/ resume_context' # Nil
\/ step_parameter' = WildCard
\/ step_parameter'.bindRule = WildCard
\/ ProcessParameterEnables( inputParam, step_parameter'.bindRule )
InterfaceOperation2ProcessName( op ) == CASE op = "xxXXxx" -> Nil
[] op = "personal_newAccount()" -> "i_personal_newAccount__"
[] op = "geth_mine()" -> "i_geth_mine__"
[] op = "GlobalScope(send)" -> "i_GlobalScope_send_"
[] op = "WithdrawalGame(becomeRichest)" -> "i_WithdrawalGame_becomeRichest_"
[] op = "WithdrawalGame()" -> "i_WithdrawalGame__"
[] op = "WithdrawalGame(withdraw)" -> "i_WithdrawalGame_withdraw_"
[] op = "WithdrawalGame(getRichest)" -> "i_WithdrawalGame_getRichest_"
[] op = "WithdrawalGame(getMostSent)" -> "i_WithdrawalGame_getMostSent_"
[] op = "WithdrawalGame(getPendingWithdrawals)" -> "i_WithdrawalGame_getPendingWithdrawals_"
[] op = "WithdrawalGame(getAddress)" -> "i_WithdrawalGame_getAddress_"
[] op = "FairPlayer(play)" -> "i_FairPlayer_play_"
[] op = "FairPlayer(endGame)" -> "i_FairPlayer_endGame_"
[] op = "FairPlayer()" -> "i_FairPlayer__"
[] op = "FairPlayer(getGame)" -> "i_FairPlayer_getGame_"
[] op = "FairPlayer(getAddress)" -> "i_FairPlayer_getAddress_"
[] OTHER -> Assert( FALSE, "Unknown infrastructure service" )
InfrastructureServiceGetResponse( operation ) == responses[InterfaceOperation2ProcessName(operation)].response
InfrastructureServiceGetStatus( operation ) == responses[InterfaceOperation2ProcessName(operation)].status
NewStep( procci, procInput, ctx ) == [ process |-> procci, bindRule |-> WildCard ,bindSet |-> procInput, ctx |-> ctx ]
Push( s, e ) == <<e>> \o s
UpdateTop( s, e ) == <<e>> \o Tail(s)
PropageTopAndPop( s ) == [i \in 1..(Len(s) -1 )|-> s[1] ]
PropageOnStack( s, v ) == [i \in 1..Len(s) |-> IF i = 1 THEN v ELSE s[i] ]
Stable == tx_running = FALSE
RECURSIVE SumRecordField(_,_)
SumRecordField(S,f) ==
IF S = {} THEN 0
ELSE LET x == CHOOSE x \in S : TRUE
IN x[f] + SumRecordField(S \ {x}, f)
RECURSIVE SumOfFunction(_)
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] ] )
uniqueElements( set, key ) == \A e1 \in set: \A e2 \in set: e1[key] = e2[key] => e1 = e2
NextId( ids, address ) == CHOOSE x \in ids: (address = x /\ address # Nil) \/ address = Nil
getElement( set, key, id ) == ( CHOOSE x \in { e \in set : e[key] = id } : TRUE )
elementExists( set, key, id ) == Cardinality( { e \in set : e[key] = id } ) = 1
status_OK == TRUE
status_FAIL == FALSE
gasPrice == 0
gasValue( gas ) == gas * gasPrice
intrinsicGas == 1
transactionGas == 1
upFrontCost( request ) == request.value + gasPrice * intrinsicGas
accounts_unique == uniqueElements( eth_accounts, "address" )
storageRoot_unique == uniqueElements( eth_storageRoot, "address" )
accounts_valid == \A a \in eth_accounts: a.address # Nil /\ a.balance >= 0
total_value == Stable => ( eth_mined + SumRecordField( eth_accounts, "balance" ) = 0 )
accounts_type == \A e \in eth_accounts: e \in t_Accounts
invariant__stack_ok == \A se \in DOMAIN stack: Len(stack[se]) <= 20
invariant__game_ok ==
Len( eth_accounts_temp ) # 0 /\ Len( eth_storageRoot_temp) = Len( eth_accounts_temp ) =>
\A a \in Head(eth_accounts_temp): \A s \in Head(eth_storageRoot_temp):
a.codeHash \in { "WithdrawalGame", "WithdrawalGameInErr" } /\ a.address = s.address => a.balance > SumOfFunction( s.pendingWithdrawals )
VARIABLES dummy_input, input_, input_e, input, x3_GlobalScope_send__input,
locals_, x3_WithdrawalGame_becomeRichest__input, locals_x,
x3_WithdrawalGame___input, locals_x3,
x3_WithdrawalGame_withdraw__input, locals_x3_, amount,
x3_WithdrawalGame_getRichest__input, locals_x3_W,
x3_WithdrawalGame_getMostSent__input, locals_x3_Wi,
x3_WithdrawalGame_getPendingWithdrawals__input, locals_x3_Wit,
x3_WithdrawalGame_getAddress__input, locals_x3_With,
x3_FairPlayer_play__input, locals_x3_F,
x3_FairPlayer_endGame__input, locals_x3_Fa, x3_FairPlayer___input,
locals_x3_Fai, x3_FairPlayer_getGame__input, locals_x3_Fair,
x3_FairPlayer_getAddress__input, locals
vars == << steps, step, step_parameter, now, tx_running, resume_context,
responses, eth_accounts, eth_storageRoot, eth_storageRoot_temp,
eth_accounts_temp, eth_address_free, eth_mined, pc, stack,
dummy_input, input_, input_e, input, x3_GlobalScope_send__input,
locals_, x3_WithdrawalGame_becomeRichest__input, locals_x,
x3_WithdrawalGame___input, locals_x3,
x3_WithdrawalGame_withdraw__input, locals_x3_, amount,
x3_WithdrawalGame_getRichest__input, locals_x3_W,
x3_WithdrawalGame_getMostSent__input, locals_x3_Wi,
x3_WithdrawalGame_getPendingWithdrawals__input, locals_x3_Wit,
x3_WithdrawalGame_getAddress__input, locals_x3_With,
x3_FairPlayer_play__input, locals_x3_F,
x3_FairPlayer_endGame__input, locals_x3_Fa, x3_FairPlayer___input,
locals_x3_Fai, x3_FairPlayer_getGame__input, locals_x3_Fair,
x3_FairPlayer_getAddress__input, locals >>
ProcSet == {"personal_newAccount()"} \cup {"geth_mine()"} \cup {"GlobalScope(send)"} \cup {"WithdrawalGame(becomeRichest)"} \cup {"WithdrawalGame()"} \cup {"WithdrawalGame(withdraw)"} \cup {"WithdrawalGame(getRichest)"} \cup {"WithdrawalGame(getMostSent)"} \cup {"WithdrawalGame(getPendingWithdrawals)"} \cup {"WithdrawalGame(getAddress)"} \cup {"FairPlayer(play)"} \cup {"FairPlayer(endGame)"} \cup {"FairPlayer()"} \cup {"FairPlayer(getGame)"} \cup {"FairPlayer(getAddress)"} \cup {"Tail"}
Init == (* Global variables *)
/\ steps = Steps
/\ step = Nil
/\ step_parameter = {}
/\ now = 0
/\ tx_running = FALSE
/\ resume_context = Nil
/\ responses = InfrastructureServiceInit
/\ eth_accounts = {}
/\ eth_storageRoot = {}
/\ eth_storageRoot_temp = <<>>
/\ eth_accounts_temp = <<>>
/\ eth_address_free = d_eth_address \ { Nil }
/\ eth_mined = 0
(* Procedure dummy *)
/\ dummy_input = [ self \in ProcSet |-> defaultInitValue]
(* Procedure schedule_process_proc *)
/\ input_ = [ self \in ProcSet |-> defaultInitValue]
(* Procedure eth_personal_newAccount *)
/\ input_e = [ self \in ProcSet |-> defaultInitValue]
(* Procedure eth_mine *)
/\ input = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_GlobalScope_send_ *)
/\ x3_GlobalScope_send__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_ = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame_becomeRichest_ *)
/\ x3_WithdrawalGame_becomeRichest__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame__ *)
/\ x3_WithdrawalGame___input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3 = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame_withdraw_ *)
/\ x3_WithdrawalGame_withdraw__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_ = [ self \in ProcSet |-> defaultInitValue]
/\ amount = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame_getRichest_ *)
/\ x3_WithdrawalGame_getRichest__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_W = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame_getMostSent_ *)
/\ x3_WithdrawalGame_getMostSent__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_Wi = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame_getPendingWithdrawals_ *)
/\ x3_WithdrawalGame_getPendingWithdrawals__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_Wit = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_WithdrawalGame_getAddress_ *)
/\ x3_WithdrawalGame_getAddress__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_With = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_FairPlayer_play_ *)
/\ x3_FairPlayer_play__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_F = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_FairPlayer_endGame_ *)
/\ x3_FairPlayer_endGame__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_Fa = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_FairPlayer__ *)
/\ x3_FairPlayer___input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_Fai = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_FairPlayer_getGame_ *)
/\ x3_FairPlayer_getGame__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals_x3_Fair = [ self \in ProcSet |-> defaultInitValue]
(* Procedure x3_FairPlayer_getAddress_ *)
/\ x3_FairPlayer_getAddress__input = [ self \in ProcSet |-> defaultInitValue]
/\ locals = [ self \in ProcSet |-> defaultInitValue]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self = "personal_newAccount()" -> "p_personal_newAccount___enter"
[] self = "geth_mine()" -> "p_geth_mine___enter"
[] self = "GlobalScope(send)" -> "p_GlobalScope_send__enter"
[] self = "WithdrawalGame(becomeRichest)" -> "p_WithdrawalGame_becomeRichest__enter"
[] self = "WithdrawalGame()" -> "p_WithdrawalGame___enter"
[] self = "WithdrawalGame(withdraw)" -> "p_WithdrawalGame_withdraw__enter"
[] self = "WithdrawalGame(getRichest)" -> "p_WithdrawalGame_getRichest__enter"
[] self = "WithdrawalGame(getMostSent)" -> "p_WithdrawalGame_getMostSent__enter"
[] self = "WithdrawalGame(getPendingWithdrawals)" -> "p_WithdrawalGame_getPendingWithdrawals__enter"
[] self = "WithdrawalGame(getAddress)" -> "p_WithdrawalGame_getAddress__enter"
[] self = "FairPlayer(play)" -> "p_FairPlayer_play__enter"
[] self = "FairPlayer(endGame)" -> "p_FairPlayer_endGame__enter"
[] self = "FairPlayer()" -> "p_FairPlayer___enter"
[] self = "FairPlayer(getGame)" -> "p_FairPlayer_getGame__enter"
[] self = "FairPlayer(getAddress)" -> "p_FairPlayer_getAddress__enter"
[] self = "Tail" -> "tail_wait"]
dummy_start(self) == /\ pc[self] = "dummy_start"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << steps, step, step_parameter, now,
tx_running, resume_context, responses,
eth_accounts, eth_storageRoot,
eth_storageRoot_temp, eth_accounts_temp,
eth_address_free, eth_mined, stack,
dummy_input, input_, input_e, input,
x3_GlobalScope_send__input, locals_,
x3_WithdrawalGame_becomeRichest__input,
locals_x, x3_WithdrawalGame___input,
locals_x3,
x3_WithdrawalGame_withdraw__input,
locals_x3_, amount,
x3_WithdrawalGame_getRichest__input,
locals_x3_W,
x3_WithdrawalGame_getMostSent__input,
locals_x3_Wi,
x3_WithdrawalGame_getPendingWithdrawals__input,
locals_x3_Wit,
x3_WithdrawalGame_getAddress__input,
locals_x3_With, x3_FairPlayer_play__input,
locals_x3_F, x3_FairPlayer_endGame__input,
locals_x3_Fa, x3_FairPlayer___input,
locals_x3_Fai,
x3_FairPlayer_getGame__input,
locals_x3_Fair,
x3_FairPlayer_getAddress__input, locals >>
dummy(self) == dummy_start(self)
schedule_process_start(self) == /\ pc[self] = "schedule_process_start"
/\ IF Cardinality( { p \in 1..Len(steps) : \A s \in steps[p]: s.ctx = Nil } ) <= 1
THEN /\ steps' = steps \o
<< { NewStep( (input_[self].called), (input_[self].input), Nil ) },
{ NewStep( step, Nil, ([ ret_ctx |-> [ stack[self][2] EXCEPT !.pc = stack[self][1].pc ] ]) ) } >>
ELSE /\ \E pos \in { p \in 2..Len(steps) : \A s \in steps[p]: s.ctx = Nil }:
steps' = (IF pos = Len(steps) THEN
steps \o
<< { NewStep( (input_[self].called), (input_[self].input), Nil ) },
{ NewStep( step, Nil, ([ ret_ctx |-> [ stack[self][2] EXCEPT !.pc = stack[self][1].pc ] ]) ) } >>
ELSE
SubSeq( steps, 1, pos-1 ) \o
<< { NewStep( (input_[self].called), (input_[self].input), Nil ) },
{ NewStep( step, Nil, ([ ret_ctx |-> [ stack[self][2] EXCEPT !.pc = stack[self][1].pc ] ]) ) } >> \o
SubSeq( steps, pos, Len(steps)))
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ input_' = [input_ EXCEPT ![self] = Head(stack[self]).input_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << step, step_parameter, now,
tx_running, resume_context,
responses, eth_accounts,
eth_storageRoot,
eth_storageRoot_temp,
eth_accounts_temp,
eth_address_free, eth_mined,
dummy_input, input_e, input,
x3_GlobalScope_send__input,
locals_,
x3_WithdrawalGame_becomeRichest__input,
locals_x,
x3_WithdrawalGame___input,
locals_x3,
x3_WithdrawalGame_withdraw__input,
locals_x3_, amount,
x3_WithdrawalGame_getRichest__input,
locals_x3_W,
x3_WithdrawalGame_getMostSent__input,
locals_x3_Wi,
x3_WithdrawalGame_getPendingWithdrawals__input,
locals_x3_Wit,
x3_WithdrawalGame_getAddress__input,
locals_x3_With,
x3_FairPlayer_play__input,
locals_x3_F,
x3_FairPlayer_endGame__input,
locals_x3_Fa,
x3_FairPlayer___input,
locals_x3_Fai,
x3_FairPlayer_getGame__input,
locals_x3_Fair,
x3_FairPlayer_getAddress__input,
locals >>
schedule_process_proc(self) == schedule_process_start(self)
eth_personal_newAccount_enter(self) == /\ pc[self] = "eth_personal_newAccount_enter"
/\ Assert(( eth_address_free # {} ),
"Failure of assertion at line 1242, column 3.")
/\ eth_accounts_temp' = UpdateTop( eth_accounts_temp,
Head( eth_accounts_temp ) \union { [ address |-> NextId( eth_address_free, input_e[self].address ), balance |-> 0, codeHash |-> input_e[self].codeHash ]})
/\ responses' = [responses EXCEPT ![InterfaceOperation2ProcessName("personal_newAccount()")] = InfrastructureServiceResponse( status_OK, (NextId( eth_address_free, input_e[self].address )) )]
/\ eth_address_free' = eth_address_free \ { NextId( eth_address_free, input_e[self].address ) }
/\ pc' = [pc EXCEPT ![self] = "eth_personal_newAccount_exit"]