Lesson 4  Fun with sets
1. Introduction
Progress: 0%
In this tutorial, we explain the most powerful data structure of Quint. Yes, that's right, sets are the most powerful data structure.
To make the tutorial a bit more entertaining, we will help an anonymous crypto Degen (opens in a new tab), who asked us to help with Quint. We only know their handle @KryptoCoffeeCat (opens in a new tab). They want to trade a few coins over different exchanges. They have collected all the pairs of coins they could exchange, but this table is not easy to analyze:
Coin A  Coin B 

BTC  USDC 
BTC  USDT 
ETH  USDC 
ETH  USDT 
EVMOS  USDC 
EVMOS  WETH 
ETH  WETH 
ATOM  EVMOS 
ATOM  JUNO 
ATOM  OSMO 
ATOM  JUNO 
EVMOS  JUNO 
EVMOS  OSMO 
For example, @KryptoCoffeeCat want to know whether they could exchange BTC for ATOM by doing up to three swaps. Unfortunately, @KryptoCoffeeCat have lost access to their browser, as they did not update it as often as it was required. Now they are stuck with the Quint REPL (opens in a new tab). Fortunately, they have found the Quint cheatsheet (opens in a new tab). We will help them!
In this tutorial, you will see how to:

use tuples,

use sets,

do plenty of interesting computations over sets.
If you would like to see the complete code before diving into the details, check sets.qnt (opens in a new tab).
2. Defining swap pairs
Progress: 7%
Code snippet:
module sets {
// We represent swap pairs as tuples of two strings
type Pair = (str, str)
// the first element of a pair
pure def fst(pair: Pair): str = pair._1
// the second element of a pair
pure def snd(pair: Pair): str = pair._2
Since @KryptoCoffeeCat write down swap pairs in their table,
the most natural way of representing a row in this table is a pair.
Hence, we declare the type Pair
as (str, str)
. This type is a special
case of a tuple.
In general, tuples of the same type contain a fixed number of elements, which can have different types themselves. Tuples are a very simple data structure in Quint that basically has two kinds of operations:
 We can construct a tuple. For example:
echo '("BTC", "ETH")'  quint
 We can access a tuple element via special fields
_1
,_2
, etc. For example:
echo '("BTC", "ETH")._2'  quint
3. Defining available pairs
Progress: 14%
Code snippet:
// all available swap pairs as a set of tuples
pure val availablePairs = Set(
("BTC", "USDC"), ("BTC", "USDT"), ("ETH", "USDC"), ("ETH", "USDT"),
("EVMOS", "USDC"), ("EVMOS", "WETH"), ("ETH", "WETH"), ("ATOM", "EVMOS"),
("ATOM", "JUNO"), ("ATOM", "OSMO"), ("EVMOS", "JUNO"), ("ATOM", "JUNO"),
("EVMOS", "OSMO")
)
Once we have decided to use tuples to represent the rows of the table,
we can define the table of all pairs as the set availablePairs
.
Would it make sense to use an array or a list instead? The answer is yes, provided that our goal was to write an efficient implementation. However, our goal is to describe the problem in a way that is free of irrelevant implementation details. In this case, the set is the best data structure:

The table of swap pairs was written in some order, but this order is actually irrelevant. @KryptoCoffeeCat wrote the pairs in some order, but they could do it differently.

The table should not contain duplicate pairs. If you look carefully, @KryptoCoffeeCat wrote the pair
("ATOM", "JUNO")
twice. We can see that Quint removed the duplicates:
echo 'availablePairs'  quint r sets.qnt::sets
4. Testing set elements
Progress: 21%
Code snippet:
pure val hasAtomJuno = ("ATOM", "JUNO").in(availablePairs)
pure val hasEvmosEth = availablePairs.contains(("EVMOS", "ETH"))
The simplest thing @KryptoCoffeeCat can do with availablePairs
is
to check, which pairs are in the table. For example, try the
following definitions:
echo 'hasAtomJuno'  quint r sets.qnt::sets
echo 'hasEvmosEth'  quint r sets.qnt::sets
5. Testing some elements and all elements
Progress: 28%
Code snippet:
pure val hasAtom = availablePairs.exists(p => p._1 == "ATOM")
// is SCRT missing from the pairs?
pure val missingScrt =
availablePairs.forall(p => p._1 != "SCRT" and p._2 != "SCRT")
Now @KryptoCoffeeCat check whether they could swap Atom for some coins and that they cannot swap Secret for any coin:
echo 'hasAtom'  quint r sets.qnt::sets
echo 'missingScrt'  quint r sets.qnt::sets
This works. However, @KryptoCoffeeCat notice that their definition of
hasAtom
was not exactly right. The definition tests only the first element
of the pair. Actually, @KryptoCoffeeCat realize that the order of coins in
every pair does not matter. So we should treat the pair ("ATOM", "JUNO")
to be the same as the pair ("JUNO", "ATOM")
. But this does not work as
expected:
echo '("ATOM", "JUNO") == ("JUNO", "ATOM")'  quint
After a bit of thinking @KryptoCoffeeCat realizs that they already know how to express that the order of coins does not matter: Just use a set instead of a tuple. Yes, @KryptoCoffeeCat, this is the way!
6. Mapping pairs to sets
Progress: 35%
Code snippet:
// swap pairs as twoelement sets (unordered pairs)
pure val availableUnorderedPairs =
availablePairs.map(p => Set(p._1, p._2))
pure val hasAtomRight = availableUnorderedPairs.exists(p => "ATOM".in(p))
After having the moment of revelation @KryptoCoffeeCat, decide to redefine the
set availablePairs
. This time the set should contain sets like
Set("ATOM", "JUNO")
instead of pairs like ("ATOM", "JUNO")
.
@KryptoCoffeeCat does not want to write the whole table again. So they quickly
map every pair p
in availablePairs
to the Set(p._1, p._2)
.
The type of availableUnorderedPairs
is Set[Set[str]]
, that is,
a set that contains sets of strings. Will that work in Quint? @KryptoCoffeeCat's
friends tell them that programming languages need a bit of boilerplate like
defining hashes, comparators, and equality. Sets of sets work in Quint out of
the box:
echo 'availableUnorderedPairs'  quint r sets.qnt::sets
Now @KryptoCoffeeCat can fix the definition of hasAtom
. They write down
the definition hasAtomRight
. This makes them happy. Time to have a coffee!
7. Filtering sets
Progress: 42%
Code snippet:
// all unordered pairs that contain ATOM at one end
pure val atomPairs = availableUnorderedPairs.filter(p => p.contains("ATOM"))
The next thing @KryptoCoffeeCat want to do with availableUnorderedPairs
is
to see, which pairs can be swapped with Atom.
To this end, they filter the set availableUnorderedPairs
as in atomPairs
:
echo 'atomPairs'  quint r sets.qnt::sets
The set atomPairs
contains only those unordered pairs that satisfy this
condition.
8. Counting the number of elements
Progress: 50%
Code snippet:
// the number of swap pairs
pure val howMany = availableUnorderedPairs.size()
To see how many swap pairs are available, @KryptoCoffeeCat
use the operator size
in the definition howMany
:
echo 'howMany'  quint r sets.qnt::sets
9. Flattening sets
Progress: 57%
Code snippet:
// get all coins that appear in pairs
pure def coinsInPairs(pairs: Set[Set[str]]): Set[str] = pairs.flatten()
// all coins in our swap pairs
pure val coins = coinsInPairs(availableUnorderedPairs)
Now @KryptoCoffeeCat wonder what kind of coins could be swapped at all.
This seems to be hard to figure out. Fortunately, they discover the right
operator in the cheatsheet. It's called flatten
:
echo 'availableUnorderedPairs.flatten()'  quint r sets.qnt::sets
It is easy to see how flatten
works by evaluating
availableUnorderedPairs.flatten()
. This operator computes the set
that contains all elements of the set's direct elements, which must be sets
themselves.
10. Reachability via one or two swaps
Progress: 64%
Code snippet:
// an example of `someCoins` in `buyableVia1Swap`
pure def someCoinsExample = Set("ATOM", "ETH", "USDT")
// which coins can be bought by swapping a coin from `someCoins` once?
pure def buyableVia1Swap(someCoins) =
availableUnorderedPairs
.filter(p => p.intersect(someCoins).size() == 1)
.flatten()
.exclude(someCoins)
// which coins can be bought by swapping a coin from `someCoins` exactly twice?
pure def buyableVia2Swaps(someCoins) =
someCoins
.buyableVia1Swap()
.buyableVia1Swap()
// which coins can be bought by swapping a coin from `someCoins` twice?
pure def buyableVia1or2Swaps(someCoins) =
buyableVia1Swap(someCoins)
.union(buyableVia2Swaps(someCoins))
@KryptoCoffeeCat are a bit tired of this tutorial. Their real goal is to find the coins that could be bought by one or two swaps. This sounds hard but it is not.
How to find, whether a pair from availableUnorderedPairs
involves a
coin from someCoins
? For example, assume that we have an unordered pair
Set("ATOM", "EVMOS")
and a set someCoinsExample
that is defined as
Set("ATOM", "ETH", "USDT")
.
Since Set("ATOM", "EVMOS")
is a twoelement set,
it's easy: We compute the intersection of Set("ATOM", "EVMOS")
and someCoinsExample
. If the pair involves a coin from
someCoinsExample
, such an intersection should contain exactly
one coin. Let's check that:
echo 'Set("ATOM", "EVMOS").intersect(someCoinsExample)'  quint r sets.qnt::sets
This works, so @KryptoCoffeeCat filter the whole set of availableUnorderedPairs
with the following condition:
echo 'availableUnorderedPairs.filter(p => p.intersect(someCoinsExample).size() == 1)'  quint r sets.qnt::sets
However, there is a small issue: The result has the type of a set of twoelement
sets (of strings), whereas they need a set of strings (coins).
@KryptoCoffeeCat already know how to solve this problem, by calling flatten()
:
echo 'availableUnorderedPairs.filter(p => p.intersect(someCoinsExample).size() == 1).flatten()'  quint r sets.qnt::sets
Finally, they do not need the coins that they started with, that is, someCoinsExample
.
Hence, they add exclude(someCoinsExample)
to the result. The complete
definition is written in buyableVia1Swap
.
@KryptoCoffeeCat want to see how this actually works. So they try:
echo 'buyableVia1Swap(Set("ATOM"))'  quint r sets.qnt::sets
This seems to work!
Now @KryptoCoffeeCat want to see what is possible to buy by doing exactly two
swaps. This is also easy: Just call buyableVia1Swap
twice. This works:
echo 'buyableVia2Swaps(Set("ATOM"))'  quint r sets.qnt::sets
And how would they find out what could be bought by one or two swaps? Also easy: Just take the set union of what is possible in one or two swaps:
echo 'buyableVia1or2Swaps(Set("ATOM"))'  quint r sets.qnt::sets
11. Reachability via multiple swaps
Progress: 71%
Code snippet:
// which coins can we buy via n swaps when starting from `someCoins`
pure def buyableNSwaps(someCoins, n) =
1.to(n).fold(someCoins,
(prevCoins, i) => buyableVia1Swap(prevCoins))
@KryptoCoffeeCat want to know how to find the coins that could be bought after a given number of swaps, not just 1 or 2. This is also quite easy. First, we have to understand how to iterate over numbers 1, 2, ..., n. There are several ways to do that in Quint. Since we are talking about sets in this tutorial, we will see how to do that using sets.
Quint has the operator i.to(j)
that constructs the set Set(i, ..., j)
.
Let's try it:
echo '3.to(10)'  quint
Now @KryptoCoffeeCat want to write something like this in pseudo JavaScript:
var prevCoins = someCoins
for (let i = 0; i < n; i++) {
prevCoins = buyableVia1Swap(prevCoins)
}
// use prevCoins
@KryptoCoffeeCat find a blog post on medium.com about Exploring folds (opens in a new tab) in JavaScript. It happens that Quint supports exactly this pattern, though it has a slightly different syntax:
1.to(n)
.fold(someCoins,
(prevCoins, i) => buyableVia1Swap(prevCoins))
The above expression iterates over the set 1.to(n)
in some order
and passes the previously computed value as the first argument prevCoins
and a set element as the second argument i
. It's important that the order
of iteration is not known in advance. However, it does not matter here, as we
are not even using i
. @KryptoCoffeeCat could even have written _
instead of i
in the above expression, which would indicate that the second
argument is not used:
1.to(n)
.fold(someCoins,
(prevCoins, _) => buyableVia1Swap(prevCoins))
Now @KryptoCoffeeCat can compute what they can buy via various numbers of swaps:
echo 'buyableNSwaps(Set("ATOM"), 3)'  quint r sets.qnt::sets
echo 'buyableNSwaps(Set("ATOM"), 4)'  quint r sets.qnt::sets
echo 'buyableNSwaps(Set("ATOM"), 5)'  quint r sets.qnt::sets
12. Power to the folds!
Progress: 78%
Code snippet:
// inSet.exists(myFun) can be expressed via `fold`, when `inSet` is finite
pure def myExists(inSet: Set[a], pred: a => bool): bool =
inSet.fold(false, (result, elem) => result or pred(elem))
// inSet.forall(myFun) can be expressed via `fold`, when `inSet` is finite
pure def myForall(inSet: Set[a], pred: a => bool): bool =
inSet.fold(true, (result, elem) => result and pred(elem))
// inSet.filter(myFun) can be expressed via `fold`, when `inSet` is finite
pure def myFilter(inSet: Set[a], pred: a => bool): Set[a] =
inSet.fold(Set(),
(result, elem) =>
if (pred(elem)) result.union(Set(elem)) else result)
// inSet.map(myFun) can be expressed via `fold`, when `inSet` is finite
pure def myMap(inSet: Set[a], mapper: a => b): Set[b] =
inSet.fold(Set(),
(result, elem) => result.union(Set(mapper(elem))))
// flatten(inSet) can be expressed via `fold`, when `inSet` is finite
pure def myFlatten(inSet: Set[Set[a]]): Set[a] =
inSet.fold(Set(), (result, elem) => result.union(elem) )
When @KryptoCoffeeCat decided to learn a bit more about fold
, they have found
that this operator is quite powerful. For instance, they could write their
own versions of exists
, forall
, filter
, map
, and flatten
.
Does it mean that they should use fold
everywhere now? Better not.
Although folds can express a lot of things, they should be used when really
required. After all, exists
, forall
, filter
, map
, flatten
are much easier to read.
13. Computing cycles with powersets
Progress: 85%
Code snippet:
// all combinations of unordered pairs that have exactly 4 pairs
pure val quads =
availableUnorderedPairs
.powerset()
.filter(pairs => pairs.size() == 4)
// Do pairs form a cycle? If they do, then for every participating coin,
// there are exactly two pairs that have this coin in common.
pure def isCycle(pairs: Set[Set[str]]): bool = {
pure def appearsTwice(coin) = {
pairs.filter(ps => coin.in(ps)).size() == 2
}
// for every coin that appears in `pairs`,
// there are exactly two pairs that cointain it
coinsInPairs(pairs).forall(appearsTwice)
}
// all pair cycles of length 4
pure val cycles4 = quads.filter(isCycle)
OK, here is a real challenge for @KryptoCoffeeCat! Can they find four pairs that could be swapped in some order, so the sequence of swaps starts with one coin and ends with the same coin? Degens love swap cycles!
To do that, they first write availableUnorderedPairs.powerset()
, which
blasts availableUnorderedPairs
into a huge set that contains all combinations
of pairs. These sets have all possible sizes. @KryptoCoffeeCat filter out the
sets that are not quadruples. How many quadruples are there? Let's see:
echo 'quads.size()'  quint r sets.qnt::sets
Phew. It will take @KryptoCoffeeCat hours to analyze all these pairs by hand. How do we know that some pairs form a cycle? Let's have a look at an example:
Coin A  Coin B 

JUNO  ATOM 
ATOM  OSMO 
OSMO  EVMOS 
EVMOS  JUNO 
There is an interesting property here. Every coin appears exactly twice in the above set. By browsing Wikipedia (opens in a new tab), @KryptoCoffeeCat found that a slightly more general observation was made by Leonard Euler about 300 years ago, when he analyzed the bridges of Königsberg (opens in a new tab). Not bad, @KryptoCoffeeCat!
After figuring out the cycles, @KryptoCoffeeCat write the predicate isCycle
and finally the definition cycles4
. Now they compute all these cycles in a
single click:
echo 'cycles4'  quint r sets.qnt::sets
14. Conclusions
Progress: 92%
@KryptoCoffeeCat has learned a lot in this tutorial. By looking at the Quint cheatsheet (opens in a new tab), they have found that this tutorial did not cover two operators on sets. Can you find them too?
If you are writing code in programming languages such as JavaScript, Rust, Golang, Java, Python, and similar, sets may be not your everyday data structure (such as arrays and lists), though there is a good chance that you have used sets before. In Quint, it's the opposite. If there is a problem, then sets are most likely there to solve it. If not, you can use maps or lists, which will be explained in follow up tutorials.
The end
You have made it!