As soon as we came up with the idea to create a Rust testing client Trdelnik, we also started thinking about its possible applications and extensions. In this blog, I would like to present a potential application that shook my head after reading an older but still excellent blog post by JP Smith (which I’ll refer to as the “Echidna post” from now on).
The author of the mentioned article tries to apply the idea of state machine testing to EVM. He supports this statement by saying that most smart contracts simply implement some textbook state machine. This idea has infuriated me because, as they say, the ability to write tests against such an invariant-rich representation would be invaluable.
To better understand what we’re going to talk about in this blog, let’s at least roughly explain what state-machine testing is. I’ll start with the concept of property-based testing, which I believe is much more familiar to most of you. Property-based tests are designed to test the aspects of a property that should always be true. They allow for a range of inputs to be programmed and tested within a single test, rather than writing a different test for every value you want to try. With state machine testing, we try to generate not just data but entire tests. You specify a number of primitive actions that can be combined together, and the goal of such testing is to find sequences of those actions that result in a failure. The motivation for state machine testing is that with just the property-based tests, we can easily end up with outstanding test coverage for the system’s edges but little assurance that the effect core is correct.
Example: Turnstile
Once I understood everything mentioned, I enthusiastically wanted to apply it to the Solana program, and this is where my hacking started. I took an example of a turnstile used in the Echidna post. You can see the state machine describing the behaviour of this model in the picture below.
So our system has two states, Locked and Unlocked. In each of these states, two actions are available, namely Push and Coin. Their effect on the machine’s state depends entirely on the initial state when the action is performed, and the result is some pretty straightforward logic. If the turnstile is locked, it can’t be pushed. If we insert a coin, the turnstile is unlocked. If we push an unlocked turnstile, it locks.
Step 0: Build the SUT
In the echidna post, the system under test (SUT) was a simple Solidity program. Therefore, the next step is clear, so we need to rewrite the Solidity smart contract to the Solana program. I did this using the Anchor framework (the figure below shows only the snippet of code needed to understand the example).
Step 1: Create a test model
For state machine testing in the Echidna blog, they used the Hedgehog library, which, like Echidna itself, is written in Haskell. Since I’m not such a big fan of functional programming, I fired up google and came across the Hypothesis library. It is a Python library that offers the functionality we want, with the difference that it is not called state-machine testing but stateful testing. The use is very straightforward, and after a short while, I was able to write our test model. The task of the test model is to invoke a SUT and then check whether the SUT (in our case, the Solana Turnstile program) behaves as expected.
The RuleBasedStateMachine class is used to define a model in the Hypothesis library, and the first step is to define the state of our test model. We represent the state simply by one boolean flag indicating whether the turnstile is locked or unlocked.
The second step is to define commands whose combination will then form tests generated by the Hypothesis library. In the hypothesis library context, these commands are referred to as @rule and actually define transitions of the state machine shown in the figure at the beginning of this section.
The simplest command is inserting a coin. This should always result in the turnstile being unlocked. This command initially calls the coin_client() method, which creates a coin instruction of our Solana turnstile program and makes an RPC call. Subsequently, we will make another RPC call to find out the current state of the SUT (i.e. our on-chain program). After these calls, we simply update the state of our test model and check if our SUT behaves as expected.
For push, outcomes are very different depending on the initial state. So, let’s break them out into two different commands. When the turnstile is locked, pushing should not change the state and should not allow anyone in—pushing while unlocked should succeed and result in the turnstile becoming locked.
We again implemented these two commands as @rules of the Hypothesis library. The only change is that each of these methods additionally has a @precondition annotation, which restricts the command call depending on the current state.
We now have a language that totally describes our state machine. From this point on, our work ends and the Hypothesis takes care of the rest.
Step 2: Test
So now, let’s test some Solana Rust code! The last thing we should do is configure the Hypothesis. In our example, we just restrict the number of tests to a maximum of 10000.
Let’s spin up pytest to check our SUT.
If you see in the figure below, we see that it works! The SUT (i.e. our Solana program) implements our model of the turnstile state machine. Hypothesis evaluated 10.000 random call sequences without finding anything wrong.
Now, let’s find some failures. Suppose we initialize the contract with the turnstile unlocked, as below. This should be a pretty easy failure to detect, since it’s now possible to push successfully without putting a coin in first.
After running the pytest one more time, we get the error. We are expecting the turnstile should be locked but it is instead unlocked and therefore the first call of push_locked() method fails. Hypothesis returns a minimal counterexample (Falsifying example) violating a given assert.
Now one can call an arbitrary program from our test model, which checks whether it implements our specified state machine correctly, and return either a minimal counterexample if it doesn’t or success.
Future Work
I hope I have presented this motivational example enough, and I have excited at least some readers of this blog. At Ackee Blockchain, we are currently actively developing our Rust client, which will also offer an API for RPC calls and can potentially automatically generate some basic tests.
The idea of a possible architecture that would connect our Rust Client with the potential of the Hypothesis library is shown in the figure below. The goal is to create a tool that would support both property-based testing and state-machine testing and be as user-friendly as possible (saving as much time as possible for developers when using it). At this stage, we are still working on the design of the architecture, so the diagram shown is only a rough estimate. We will actively update the new milestones, so stay tuned and follow our blog.
