This post presents how API traces, generated for sbuilder formal models, can be inspected, and how the output can be modified using api-call-init extension point of tla-trace-filter -tool.
Sbuilder possibility operators may generate traces, which demonstrate that behaviour given by the operator is present in the model checking state space. An API trace is a sequence of steps, where a step includes the state of the formal model before the API call, interface operation called and its parameters bindings, and the state of formal model after the API call. This post shows to how to extend rendering of formal model API traces.
Table of Contents
1 SBuilder User’s Guide Blog Series
A series of posts comprising a User’s Guide for sbuilder-eth plugin in SBuilder tool:
- Truffle install: documents steps to install Truffle Ethereum development environment to Node-js.
- Sbuilder install: shows steps to install sbuilder-eth GEM to Truffle Ethereum development environment. After installation a minimal configuration is used to validate that the installation was successful.
- Managing state space generation in Sbuilder: expolore, how to state space explosion manifests itself in formal models created by Sbuilder -tool, and how state space explosion can be controlled by limiting cardinality of domain sets in application data model.
- Simple Bank contract: use a simple 10 line Solidity contract containing two (subtle) “bugs” (=violations of correctness promise), and a demonstrates, how to use invariants in Sbuilder to find these violations.
- Sbuilder generated correctness criteria: demonstrates using Sbuilder generated correctness criteria. The criteria presented include ensuring correctness of 1) contract function return values, 2) contract type, and 3) account balances on blockchain.
- Demonstrate Sbuilder Translation Results (Wallet-1): use a very contrived example to demonstrate, how to include manually crafted TLA+ snippets into a formal model created by SBuilder. The main purpose is to 1) show, how to bind TLA code with Solidity interfaces, 2) understand TLA -files generated in Sbuilder translation, and 3) explain, how Sbuilder “possibility” operator relates to model checking formal model correctness. A more realistic example of using manual TLA+ to specify is given in another post.
- Translate Solidity Automatically (Wallet-2): explains how to integrate manually crafted and automatically translated TLA+ snippets to work together in a Sbuilder formal model.
- API Trace Extension Point (Wallet-3): presents how API traces, generated for sbuilder formal models, can be inspected, and how the output can be modified using api-call-init extension point of tla-trace-filter -tool.
Rest of this blog entry assumes that sbuilder-eth GEM and has been installed to a Truffle Ethereum development environment as documented in a previous blog post.
2 Assumptions
The examples used in this post assume that the possibility operator dummy_created for setup wallet-1 introduced in a previous blog post has been executed,
export POSSIBILITY=dummy_created; SETUP=wallet-1 npm run-script sbuilder-possible
and that the formal model trace exists in a file gen/$SETUP/tlc.out.
3 API Trace Rendering Extension Point
Sbuilder Formal model API traces are outputted with tla-trace-filter.rb api-calls -command, which previosly, in Sbuilder installation on Truffle, was configured as npm script sbuilder-api in file package.json:
"sbuilder-api": "bundle exec tla-trace-filter.rb api-calls $SETUP --src-dir=. --solc-line",
3.1 Read Instructions In api-call-init.mustache File
Trace Rendering Extension Point uses Mustache template -tool. The extension is activated by overriding mustache/api-call-init.mustache file within tla-trace-filter GEM.
Instructions for the extension point are shown with the command:
cat $(bundle show tla-trace-filter)/mustache/api-call-init.mustache
The output shows:
{{!
api-call-init.mustache: define rendering for 'api-call' command
Override this template to use other than default rendering.
This template is called once for a 'tla-trace-filter.rb api-call'.
It initialize four mappings:
- API_INPUT_INIT : render state before API call
- API_CALL_INIT : render API interface and API input parameters
- API_RETURN_INIT : render API interface and API return parameters
- API_OUTPUT_INIT : render state after API call
These mappings wrap mustache lambda sections, which contain a YAML
formatted hash mapping interface operation to a name of mustache
partial template. Two special keys are used: 1) 'default'
(=template to use if no other found), and 2) 'empty' (=template to
use if 'interface.interface_operation' is nil).
Example:
Demo(): solidity-constructor
Demo(execute): solidity-message
empty: api-call-empty
default: api-call-input
Which reads:
- inteface operation "Demo()" uses mustache partial 'solidity-constructor.mustache'
- interface Demo(execute) use partial 'solidity-message.mustache
- undedefined interface operation (initial state) use partial 'api-call-empty.mustache'
- all other interface operations use template 'api-call-input.mustache'
Search parth of these template files is configured using command line option --mustache
}}{{!
Configure templates to render state before API call
}}{{#API_INPUT_STATE_INIT}}
default: api-call-input
empty: api-call-input
{{/API_INPUT_STATE_INIT}}{{!
Configure templates to render API CALL
}}{{#API_CALL_INIT}}
default: api-call-default
{{/API_CALL_INIT}}{{!
Configure templates to render API_RETURN
}}{{#API_RETURN_INIT}}
default: api-call-return
empty: api-call-return
{{/API_RETURN_INIT}}{{!
Configure templates to render state after API call
}}{{#API_OUTPUT_STATE_INIT}}
default: api-call-output
empty: api-call-output
{{/API_OUTPUT_STATE_INIT}}{{!
Do not output new-line
Local Variables:
require-final-newline: nil
End:
}}
3.2 Create a Directory to Hold Extension Partials
For an example, start by creating a directory testcase-templates to hold extension templates:
mkdir testcase-templates
3.3 Override api-call-init.mustache
Create file testcase-templates/api-call-init.mustache to override default api-call-init.mustache in tla-trace-filter GEM.
In this example, we instruct tla-trace-filer.rb to use template demo-call.mustache to render API calls to Wallet() interface:
{{!
Modify rendering API calls to Wallet() interface operation.
Use defaults for otherwise.
}}
{{#API_CALL_INIT}}
Wallet(): demo-call
{{/API_CALL_INIT}}
3.4 Implement Partial Template to Render API Call
Create a file in testcase-templates/demo-call.mustache
{{!
demo-call.mustache: render state before making API call
}}
CALL-WALLET:{{now}} {{interface.interface_operation}}( value: {{{api_input.value }}}, sender: {{api_input.sender}}, owners: {{{api_input._owners.to_a }}} )
to implement API call for Wallet() constructor, as configured above.
4 Output Sbuilder API Trace
4.1 Default Sbuilder API Trace Output
In Sbuilder installation on Truffle , we have bound tla-trace-filter.rb api-calls -command to npm script sbuilder-api. This command outputs default Sbuilder API trace
SETUP=wallet-1 npm run-script sbuilder-api
The output for example setup wallet-1 shows the following API calls and formal parameter bindings:
CALL:1 geth(newAccount)( {"sender"=>nil, "originator"=>nil, "value"=>0, "recipient"=>nil} )
CALL:2 Wallet()( {"sender"=>"d_eth_address_1", "originator"=>nil, "value"=>0, "_owners"=>#<Set: {"d_eth_address_1", "d_eth_address_3"}>} )
CALL:3 Wallet(execute)( {"sender"=>nil, "originator"=>nil, "value"=>0, "recipient"=>"d_eth_address_2", "_undersigners"=>#<Set: {"d_eth_address_1", "d_eth_address_3"}>, "_nonce"=>0} )
4.2 Extended Sbuilder API Trace Output
To use the template extension created, we have to pass extension directory testcase-templates/ to tla-trace-filter.rb -command using --mustache option
export SETUP=wallet-1 && bundle exec tla-trace-filter.rb api-calls $SETUP --src-dir=. --solc-line --mustache=testcase-templates/
Comparing output of this command with the default output
0a1,3
>
> > bundle exec tla-trace-filter.rb api-calls $SETUP --src-dir=. --solc-line
>
73c76,77
< CALL-WALLET:2 Wallet()( value: 0, sender: d_eth_address_1, owners: ["d_eth_address_1", "d_eth_address_3"] )
---
>
> CALL:2 Wallet()( {"sender"=>"d_eth_address_1", "originator"=>nil, "value"=>0, "_owners"=>#<Set: {"d_eth_address_1", "d_eth_address_3"}>} )
demonstrates that Wallet() constructor API gets rendered differently.
5 Use Case For The Extension Point
The extension point presented here can be used to generate test cases on implementation.
One possible use of the extension point is to implement unit tests of system services. In this case, a step in a formal model API trace is translated to a unit test case. Step before state is translated to actions in unit test setup initializing service environment to a known state, step API call parameters are mapped to parameters of the service call, and step after state is mapped to unit test assertions.
Another possibility is to use the formal model API traces to define system tests. In this case, the initial state in a formal model trace is mapped to system initialization, each step in the formal model API trace is translated to a service API call with parameters mapped from step formal model parameters, and step output state is mapped to assertions validating implementation state after each system test service call.
Unit tests extracted from formal model API traces validate that a service plays its role in a longer chain of operations. In addition, because units test execute in isolation, infrastructure required is simpler compared to running system wide tests based on formal model traces.
For an implementation refer to tla-trace-arch, a set of mustache templates extending tla-trace-filter -tool to create a self extracting achieve for API traces generated, when model checking formal models created by Sbuilder -tool.
6 Changes
| Date | Change |
|---|---|
| 2018-01-03 | Added reference to ‘tla-trace-arch’ |
7 Version Information
- Language environments:
- node version:
v6.11.4- testrpc version:
6.0.3 - Truffle version:
4.0.3
- testrpc version:
- ruby version :
ruby 2.3.1p112 (2016-04-26 revision 54768) [x86_64-linux] - java version =java version “1.8.0_151″=
- node version:
- Sbuilder GEM versions:
- sbuilder version: =sbuilder.rb – 0.3.8 =
- sbuilder-eth: Translate Ethereum Solidity to Sbuilder AL version = * sbuilder-eth (0.0.4)=
- sbuilder-al: Translate SBuilder AL langauage to TLA+ language = * sbuilder-al (0.0.8)=
- tla-trace-filter: Command line utility to process TLA+tools output = * tla-trace-filter (0.0.4)=
- tla-parser-s: Utility to parse TLA+ language = * tla-parser-s (0.2.5)=
8 Fin
This post has presented an extension point to avail formal model API traces for example in creating unit tests or system test on implementation. Obviously, infrastructure is needed to map formal model values to implementation values, and to execute test cases.
jarjuk 
7 thoughts on “API Trace Rendering Extension Point”