​
Get Started

Welcome to the introduction tutorial on how to use State Space. This tutorial is based on the OpenZeppelin ERC20 implementation and the Pausable feature. Read the test objective below, and follow the steps to understand how State Space works. Objective: Determine who should be able to mint() tokens after the contract has been paused.
1

Open the ERC20 playground

Login or create your account hereFrom the “Home” menu, open the pre-loaded ERC20 Workbench project.
You will see a folder tree containing the ERC20 project and a canvas with a pre-designed transaction sequence.Expand the folder tree to view all the externally visable functions as components. These components can be dragged onto the canvas to create multi-contract test scenarios and transaction sequences (e.g. end-to-end flows, integration tests, etc).There are four types of components:Blue = CALL - function call
Purple = VIEW - view function
Green = CREATE - constructor
Gray = DEPLOY - a deployment script
2

Design a test scenario

​
The transaction sequence

Since the objective is to determine whether any EOA can mint tokens after the contract has been paused, we created a sequence of transactions that calls first deploys the contract, and then calls pause() and mint() in succession:Deployment → constructor(...) → pause(...) → mint(...)It should look like this:

Pause-->Mint Transaction Sequence

You can use your existing deployment scripts (if you have one in Foundry or Hardhat) to create custom deployment nodes for deeper testing.

​
Configure symbolic input parameters

State Space supports the use of both symbolic and concrete input values, or any combination thereof for both transaction values and function parameters.For values set to symbolic, State Space will automatically search for and generate structured dynamic inputs that will satisfy the conditions of the entire transaction sequence.What if we’re not sure what parameters to set? Rather than manually figuring out all combinations to test, we can use symbolic values to explore all possible inputs for any field.Let’s assume that Alice is the contract deployer and Bob is the initialOwner. In our test setup, we configure the following:
  • Set the transaction From field for the constructor() function call to Alice.
  • Set the initialOwner parameter in the constructor() to Bob.
  • Leave the transaction From field for pause() set to symbolic to consider all EOAs preconfigured in the deployment (Alice and Bob).
So far, it should look like this:

Configure deployment and mint() parameters

Since part of our objective is to determine whether any externally owned account (EOA) can successfully mint tokens, we take a symbolic approach for the mint() transaction:
  • We leave the transaction From field for mint() set to symbolic. Symbolic means it represents all possible EOAs (limited to the accounts configured in the deployment) rather than being fixed to a specific account (a concrete input). This allows State Space to autonomously discover which accounts can trigger unique execution paths.
  • We also leave the function parameters of mint() symbolic (to and amount), allowing State Space to explore all possible input values to determine which concrete inputs and conditions (if any) would result in a successful mint operation after pause has been called.
It should look like this:

Final Parameter Configuration

This hybrid symbolic/concrete input parameterization ensures that we can still maximize coverage while minimizing state space explosion.Alternatively, you could set everything to symbolic too, and you’ll get a wider state space to explore and analyze. It will just take more compute time, and include scenarios that may not be as meaningful in answering the test objective.Now, it’s time to explore the state space.
3

Explore the state space

Select the icon to start exploring and generating the execution state space.State Space will autonomously explore code paths, automatically taking into consideration all multi-contract interactions for your test scenario. For each unique code path it discovers, it will generate the verified concrete input conditions that trigger their execution.Because State Space models the full EVM semantics, the symbolic execution can reason about every operation with bit level precision, uncover obscure edge cases manual testing misses, and maximize coverage and path exploration.

Resulting execution paths, input conditions, and coverage.

Discovered execution paths, input conditions, and resulting contract state, will appear dynamically during execution. Once completed, detailed coverage metrics will be displayed for each run.The results should display 14 test cases (execution paths) and 46% health coverage.Run times can vary depending on the number of sequences, transaction depth, the amount of symbolic parameters, compute, and more. Complex codebases will require increased allocation of compute resources. If you’re curious about what performance to expect, reach out to us and we’ll help you estimate it.Feel free to experiement with different sequences to analyze different behaviors.
4

Analyze and validate behavior

As you review the results, you’ll notice that every execution path results in a revert, with no successful mint() transaction occurring.We determine that we could not find any path or combination of inputs that will successfully lead to a mint transaction, and provide the test cases for each executed path.This outcome matches our expectations because after invoking the pause() function, the _paused contract value should be set to true preventing any minting operation from successfully completing.Let’s confirm that the _paused state value was indeed updated, and visually validate all other states and state changes are correct.Select and open the test case (execution path) with the following input conditions:
  • Alice deploys the contract and Bob is set as the initialOwner
  • Bob calls the pause() function
  • Transaction reverts with an EnforcedPause error after Bob attempts to mint 1 token to Alice.
Once you have opened test case, click through the constructor() —> pause() —> mint() transactions. You can examine the storage layout, values, changes, account balances, and emitted events that occurred throughout the execution of the transaction sequence.Locate the _paused storage value, and validate it was correctly set to true after the pause() transaction and that it remained unchanged after the mint() transaction (which reverted). Source code is also highlighted for lines and branch coverage:
Mark the state value as valid by clicking the shield icon. You can click through the shield icon to mark it as invalid or back to unreviewed as well.
  • Green shield: Valid state
  • Red shield: Invalid state
  • Grey shield: Not reviewed
You can also view your validation history under the History tab.If you added any other team members to your project, their reviews will be visable to everyone in your team. If one team member flags a state as invalid, it will appear as invalid (red) to all other collaborators. This is especially useful when working with auditors or extended teams to make code and security reviews easier.
5

Exporting to Hardhat or Foundry

export
From the same view, select your test framework (Hardhat or Foundry) to copy or download the complete test case.You can also include emitted events in the test case by selecting the “Export Test” button in the top left of the screen.The test case represents the exact behavior of code, including both expected and unexpected behavior.
6

Optional: remove the `pause` function

Return to the canvas, and delete the pause function from the transaction sequence, and reconnect the mint(..) function to the constructor().Run the analysis again.

Mint

You’ll see the mint(..) transaction completing successfully.Select a path where a successful mint operation occurs, and analyze the contract state and changes.Find the _totalSupply state value, and evaluate its behavior. Has _totalSupply increased as expected by the amount? Have the balances correctly updated as well? Toggle through the transactions to become familiar with the process.

Contract state analysis

If you would like a tutorial on any specific topic, of have suggestions on improving existing tutorials, please contact us! We’d love to hear from you.