Support functional actions in the Quint testing framework

[andrey-kuprianov]

This is intended as a discussion starter about possible improvements to the current Quint testing framework. The trigger for that was the particular problems that I've encountered while writing tests for a model of a blockchain protocol. I will be very grateful to both the Quint developers, as well as to the wider Quint community for their contributions to this discussion, in the hope that together we will be able to arrive to a solution satisfying many Quint users, while simultaneously incorporated nicely into the general Quint language framework.

Stateful actions

In the current Quint, actions are stateful: an action is supposed to modify state variables, which are received implicitly, and to return a bool. An example of such Quint model can be found in Lesson 3 - Basic anatomy of a protocol in Quint.

This approach, while being well-suited for small examples, quickly shows its limitations when applied to production systems:

• actions become bloated due to the necessity to mention unchanged clauses (x' = x) for all unchanged variables.
• actions become hard to maintain: adding a single state variable leads to the necessity to update all actions of the model at hand.
• the boolean return type is too restrictive: in production systems we want to specify and validate also different error types the system actions may return.

Functional actions

Purely functional actions receive an explicit state as an argument, and return an explicit result, which contains either a new, updated state, or an error. This is a well known concept in purely functional languages such as Haskell, or in the modern mixed-semantics languages like Rust. An example of Quint specs that follow this approach are e.g.:

• Cosmos Fungible token ICS-20
• Solidity Fungible token ERC-20

The advantages of functional actions are the the flipped drawbacks of the stateful ones:

• No need to mention unchanged vars, due to the record update syntax (r.with(...), or the more recent { f1: e1, fN: eN, ...r })
• Easy maintenance: no need to change existing actions when new state variables are added (because now we have record components of an explicit state, instead of separate state variables)
• The result of a functional action can contain arbitrary errors, which can be also validated.
• Finally, additional bookkeeping state components (such as history tracking, or ghost variables) can be added at no cost (no need to update functional actions)

The Problem

It is possible to write the functional actions themselves in Quint in a nice and a concise way. On the other hand, the current Quint testing framework (as outlined e.g. in the Language Summary: Runs) rests on such operators as then, reps, fail, etc., which act as stateful action combinators: given one or more stateful action, they give another stateful action as a result. While well-suited for stateful actions, these operators are not able to combine functional actions:

• Every time a functional action is executed, the result needs to be explicitly examined to be either a new state or an error
• The next state needs to be explicitly “unpacked” to be used in further actions

Attempts to fit purely functional actions into the current testing framework seem to lead either:

• to a lot of additional infrastructure in the model in order to cast functional actions as stateful ones, as in ICS-20 tests
• to a bloated test, where checking the error cases or unpacking of the next state needs to be done explicitly, as in this ERC-20 test.

Desired solution

I would like to have testing operators that explicitly support functional actions:

• Unpacking of the next state from the result should be implicit
• It should be possible to specify whether we expect the functional action to succeed or fail
• In case of a failure, it should be possible to specify which error we expect.

Looking forward to your inputs, and to a productive discussion!

[konnov]

I can see how staying at the functional layer may help. In principle, you should be able to use assert(...) in a test without introducing a state. As for error detection and handling, would something like Either or Result (in rust) help you? In this case, we would have to prioritize the work on ADTs.

[andrey-kuprianov]

I would say ADTs are the prerequisite for this, because a Result has to be effectively an Either. Also, not outlined here yet, but the typical interface for a blockchain protocol is a set of input messages. Each message has a selector, and message-specific fields. This all needs to be integrated with what I described above, and properly describing such input messages also requires ADTs.

[josef-widder]

As discussed with @andrey-kuprianov on Slack, his proposal addresses sequential computations, that is, in particular smart contracts.

To what extent this also addresses distributed computations is still a bit unclear to me. I agree, distributed and concurrent computations have a sequential aspect (what a process or a thread does locally). In addition and a distributed aspect, that is global invariants and the communication semantics between two processes, e.g., actions at a process A enable actions at B (e.g., via sending packets).

I think for the sequential part such testing operators would also be useful for distributed protocols, while for distributed aspects, we might still want the expressivity of actions and steps as we need to capture interleavings and communication that are inherent non-deterministic and cannot be captured in the functional layer.

[andrey-kuprianov]

I agree that distributed setting brings its own complications in the form of semantics of sending/receiving messages, or other means of distributed coordination. But it also seems that we both agree that local-state-modifying actions of processes fit well into the sequential setting, and thus the testing framework requirements discussed here should apply well to the local-state parts of a distributed system model.

The requirements wrt. testing distributed system specific parts of the model should be probably discussed later and separately, when the sequential setting is well covered.

[andrey-kuprianov]

The use case

To make the discussion more concrete, here is the example use case. It is about the Duality Decentralized Exchange, and in particular the mechanics of Constant-price Liquidity Pools. At a high-level, the mechanics is simple, and can be explained in a few words:

• The system holds multiple liquidity pools; each pool consists of reserves for a pair of coins that can be mutually swapped one into another at a constant price. E.g., a pool may say that 4 A coins can always be swapped for 2 B coin, i.e. the exchange rate is 2, provided there are enough reserves to perform the swap. Swaps are the main functionality a liquidity pool provides to traders, one category of system users.
• Another category of users are liquidity providers (LPs): users who provide their funds (liquidity) into the pool reserves such that traders can perform swaps. The motivation for LPs to provide their funds is to earn fees, which are taken from a trader for each performed swap.
• While swap is a trader's action, LPs perform two actions: they either deposit a certain amount of two coins that constitute a trading pair, and obtain a certain amount of pool shares in exchange for coins, or they withdraw a certain amount of previously obtained shares from the pool, and receive back the coins.

Based on this simplified description we can already discern one of the core system properties it should guarantee wrt. LPs: the following Pool Profitability Property:

For any liquidity provider LP, at any state of the system, and any liquidity pool P with the exchange rate p, if:

1. LP deposits an arbitrary number (Xa, Xb) of (A, B) coins into the liquidity pool P at some arbitrary Td time point, receiving the S amount of shares;
2. The system performs arbitrary actions, with no actions from the LP user wrt. the P pool;
3. LP withdraws all S shares at any arbitrary Tw > Td time point later;
4. then the number of coins LP redeems from the pool is not less than they have deposited, if calculated into a single coin (A or B) using the pool's exchange rate p.

Ideally, I would like to easily express the above property (among many others) as a test in the Quint testing framework, and to use it both in the randomized simulation, as well as later as an invariant for proving it with the Apalache model checker.

[andrey-kuprianov]

The model dummy, and the need for ADTs

To make the discussion even more concrete, below is the dummy model, with all the actual logic stripped, but with a couple of functional actions deposit and withdraw (which do nothing). Notice that it was possible to extend the model with history tracking without even touching its functional core.

module dex {

// Constants
pure val TOKENS = Set("A", "B", "C", "D")
pure val ADDRESSES = Set("Alice", "Bob", "Carol", "Dave")
pure val MAX_AMOUNT = 1000
pure val MAX_TICK = 100000
pure val TICKS = (-MAX_TICK).to(MAX_TICK)
pure val AMOUNTS = 0.to(MAX_AMOUNT)

// Basic types
type TickIndex = int
type Token = string
type Addr = string
type TradingPair = List[Token]
type PoolID = { tokens: TradingPair, tick: TickIndex, fee: TickIndex }
type AmountPair = List[int]
type Pool = { reserves: AmountPair, shares: int }
type TokenAccount = Token -> int
type ShareAccount = PoolID -> int

type Pools = PoolID -> Pool
type Coins = Addr -> TokenAccount
type Shares = Addr -> ShareAccount

type State = {
    pools: Pools,
    coins: Coins,
    shares: Shares,
}

pure def initialState: State = {
    pools: Map(), coins: Map(), shares: Map()
}

// Result of executing an operation on the state
type Result = { state: State, result: str }

pure def ok(s: State): Result = { state: s, result: "ok" }
pure def error(reason: str): Result = { state: initialState, result: reason }
pure def isOk(r: Result): bool = r.result == "ok"
pure def isError(r: Result): bool = not(r.isOk())

// Deposit token amounts into a pool
pure def deposit(s: State, sender: Addr, receiver: Addr, 
    tokens: TradingPair, tick: TickIndex, fee: TickIndex, tokenAmounts: AmountPair): Result = 
    ok(s)

// Withdraw shares from a pool
pure def withdraw(s: State, sender: Addr, receiver: Addr, 
    tokens: TradingPair, tick: TickIndex, fee: TickIndex, shares: int): Result =
    ok(s)

pure def MESSAGES = Set("deposit", "withdraw")

// A join of all parameters from all actions
type Message = {
    kind: string,
    sender: Addr, 
    receiver: Addr, 
    tokens: TradingPair,
    tick: TickIndex,
    fee: TickIndex, 
    amounts: AmountPair,
    shares: int
}

def nondetMessage(): Message = 
    nondet msg = {
        kind: oneOf(MESSAGES),
        sender: oneOf(ADDRESSES),
        receiver: oneOf(ADDRESSES),
        tokens: [oneOf(TOKENS), oneOf(TOKENS)], 
        tick: oneOf(TICKS), 
        fee: oneOf(TICKS),
        amounts: [oneOf(AMOUNTS), oneOf(AMOUNTS)],
        shares: oneOf(AMOUNTS)
    }
    msg

// State variables
var state: State
var history: List[(str, Message)]

action init: bool = all {
    state' = initialState,
    history' = []
}

action step: bool = {
    val msg = nondetMessage
    val res = 
        if(msg.kind == "deposit") 
            deposit(state, msg.sender, msg.receiver, 
                msg.tokens, msg.tick, msg.fee, msg.amounts)
        else if(msg.kind == "withdraw") 
            withdraw(state, msg.sender, msg.receiver, 
                msg.tokens, msg.tick, msg.fee, msg.shares)
        else error("Wrong message type")
    all {
        history' = history.append((res.result, msg)),
        state' = 
            if(res.result == "ok") res.state
            else state
    }
}
} // Module dex

One thing immediately noticeable is how ADTs would simplify this. Currently Message is a join of all message types; with more message types this will become unwieldy. With ADTs (concrete syntax yet unknown) the signatures could become e.g.

type Message = MsgDeposit | MsgWithdraw

pure def deposit(s: State, m: MsgDeposit): Result
pure def withdraw(s: State, m: MsgWithdraw): Result

And of course Result should also be Either a new state, or an error, as in Rust: smth. like Result<State, str>.

[andrey-kuprianov]

The need to reject invalid executions

When describing a test scenario, it is often the case that we are interested only in a subset of the executions. E.g. in the above use case:

• in step 1, we want to test only the executions where deposit succeeds, and want to ignore those where it fails, for any reason;
• in step 2, we want to perform any system action, but filter out the actions where LP performs an action on pool P;

Please note that this process of rejecting/ignoring/filtering out of invalid executions is different from assertions:

• with assertions, we assert that a certain condition should hold; if it doesn't, then we have found an error (a bug, a counterexample to the property, etc.)
• with rejections, when a certain condition doesn't hold, we just want to throw this execution away, and explore another one.

[andrey-kuprianov]

The need for implicit non-determinism

In the current testing framework, the non-determinism needs to be introduced explicitly, as it's done in this ERC-20 test. The problems with such an explicit approach:

• it is verbose: we need to introduce a separate named value for each case of non-determinism we want to use in the test;
• it is hard to extend: when we need to have multiple "invocations" of actions in a test, each with non-deterministic parameters, the need to have named values leads to name conflicts;
• it is low-level: currently, it seems, the only way to introduce non-determinism in Quint is via oneOf operator, which is limited to sets.

The desired solution

What I would like to have is effectively the opposite of the list above:

• be concise: do not require to introduce named values for non-determinism in tests. One possibility could be to receive an implicitly generated non-deterministic parameter at every step of the test
• be extensible: non-trivial tests will have many action "invocations". The non-determinism in the tests needs to be able to cope with this growth organically, i.e. with a very small, constant, syntactic and mental overhead for each new action introduced to the test.
• be high-level: ideally, I would like to have non-deterministic generators for arbitrary datatypes. E.g., for the Message from the model dummy, I would like to be able to say e.g. nondet m = Gen(Message), which would give me the equivalent of nondetMessage() function.

[andrey-kuprianov]

The need to relate distant execution steps

In many cases, tests need to relate several steps in the execution. E.g., in the use case we need to relate steps 1 and 3:

• the parameters of withdraw invocation used in step 3, need to be the same as the parameters of deposit invocation in step 1
• but instead of tokenAmounts parameter, the shares parameter needs to be used, and have the value returned from the deposit invocation.

Currently, there is no way to access something that happened previously in the trace, except for using explicit non-deterministic input for every parameter that needs to be related between different steps in the execution.

The desired solution

Here my head explodes a bit because of so many possible alternatives 😄 Ideally, I would like not to explicitly introduce named values for steps that need to be related, i.e. to have the ability to relate to any value at any previous step in the execution. The non-exhaustive list of alternatives of how this could be achieved:

• Use names for each step; e.g. "deposit" for step 1 and "withdraw" for step 3. Then relate to other steps by accessing them from the map of steps;
• Use indices, like in Apalache trace invariants. This seems to be a less preferable alternative, because when we write the test, we might want to introduce steps in between of already written ones, and then the indices start to shift. Besides, it's always easier to make mistakes with integers, which could go unnoticed;
• Use explicit non-determinism, but at a higher level, with named instances of entire messages produced by generators.

I am sure there are other, nicer alternatives, of which I have not thought yet.

[andrey-kuprianov]

The prototype API

I have tried to come up with an API that would satisfy the above wishlist; no claims of completeness, correctness, of fitness for a particular purpose is made. Here is the Pool Profitability Property from the use case, expressed in the prototype API:

def testDepositWithdraw = 
    nondet user = oneOf(ADDRESSES)
    Init(initialState)
    .ThenAny((s, m) => m.now.sender != user)
    .ThenOk("deposit", (s, m) => s.now.deposit(m.now))
    .Require((s, m) => m.now.sender == user)
    .ThenAny((s, m) => m.now.sender != user or m.now.tokens != m.at("deposit").tokens)
    .Then("withdraw", (s, m) => (s, m) => s.now.withdraw(m.now))
    .Require((s, m) => m.now == {
            shares: s.after("deposit").shares.get(user),
            ...m.at("deposit")})
    .AssertOk()
    .ThenAssert((s, m) => sum(s.now.coins.get(user)) >= 0)

The high-level idea

The test in this API describes declaratively the steps the execution should contain, as well as what is expected from that execution. There can be several kinds of steps:

• Initial step (Init) describes the state in which the test starts.
• Action invocations (Then, ThenAny, ThenOk) allow to invoke various system actions. Action invocations can be named, thus providing the ability to relate to distant execution steps.
• Requirements to the trace (Require) allow to specify constraints on the trace, i.e. to reject invalid executions.
• Assertions (Assert, ThenAssertOk) allow to specify error conditions, which, when failed, mean a property violation.

Steps that have Then as a prefix, advance on the execution, while steps that don't have this prefix, don't advance. The latter allows to attach requirements/assertions to the last executed action.

Given such a declarative test representation, a test executor, provided the additional generator for non-deterministic messages, could build a computational tree (e.g. up to the given depth, or the total number of steps in the tree), and explore only the valid branches, while looking for assertion violations.

States and messages

Almost each step of the test is a lambda function, receiving two parameters (s and m), which, at a high level, can be though of as a states and a messages:

• states give access to states of the execution;
• messages give access to (input) messages that have been used at each step of the execution; think about messages as non-deterministic inputs to the system, produced by a random generator; this provides for implicit non-determinism.

Each of states (s) and messages (m) has several components, which provide access to various (historic) execution steps:

• now gives access to the present state or message.
• at gives access to a state or a message at a previously named execution step.
• after gives access to a state or a message immediately after a previously named execution step.

Step-by-step explanation

• nondet user = oneOf(ADDRESSES): select one of the users non-deterministically
• Init(initialState): start the test at the initial system state
• .ThenAny((s, m) => m.now.sender != user): perform any action, not involving user
• .ThenOk("deposit", (s, m) => s.now.deposit(m.now)): perform deposit action using the random message (m.now) as parameter; require that the action succeeds
• .Require((s, m) => m.now.sender == user): require that the action is performed by user
• .ThenAny((s, m) => m.now.sender != user or m.now.tokens != m.at("deposit").tokens): perform any action, not involving user, or performed on another trading pair
• .Then("withdraw", (s, m) => (s, m) => s.now.withdraw(m.now)): Perform withdraw action using the random message (m.now) as parameter
• .Require((s, m) => m.now == { shares: s.after("deposit").shares.get(user), ...m.at("deposit")}): require that the witdhraw action uses the same message as the message at step deposit, but using shares that the user obtained after executing deposit
• .AssertOk(): assert that the withdraw action succeeds (it's an error if it fails)
• .ThenAssert((s, m) => sum(s.now.coins.get(user)) >= 0): assert that at the state after the last action the user has received a profit.

In order not to complicate the discussion, the sum function above is vaguely defined; the precise definition would require to compute the sum using the pool exchange ratio; that's unimportant in the present context.

---

As explained above, this proposed API is a very early prototype, and for sure doesn't fit nicely into the present Quint framework. Please regard it only as something to spark the discussion, in the hope that together we will be able to arrive a much better one, which integrates nicely into Quint. Looking forward to your thoughts!