Numbers

The int type is a native type built into the core of Quint. Despite their simplicity, integers are the workhorse of most specifications, serving as counters, balances, timestamps, or the primitive type behind an alias or a compound type. In this lesson you will explore the nuances of Quint’s integers and learn how to take full advantage of the language’s syntax and tooling. Mastering integers and taking the right approach when working with them is essential for writing accurate Quint specifications.

What this lesson covers:

• Integer literals.
• Built-in operators (arithmetic and comparison) and their distinct calling forms.
• Modelling bounded integers with predicates.
• Working with decimals in a language without floats.

Integer literals

Integer literals are written using the standard syntax:

  // 0 is an integer literal
  pure val zero: int = 0
 
  // integers can be positive
  pure val two: int = 2
 
  // integers can be negative
  pure val minus_three: int = -3

Similarly to other languages, in Quint one can separate digits with ’_’:

  // digits can be separated with '_' for readability
  pure val hundred_million: int = 100_000_000

Hexadecimal notation is also supported, including the underscore ’_’ separator for readability. Try these literals in the REPL:

0xAbC456

0xAB_CD_EF

By definition, an integer is a whole number without a fractional component. You may have noticed that Quint does not have a built-in floating-point type. Consequently, modelling fractional values requires specific techniques. We explain these approaches and the available libraries later in the Decimals section of this lesson.

Unlike most programming languages, Quint’s integers are big integers. This means there are no language imposed boundaries or type-level checks on the size of an integer. There is neither a minimum integer, nor is there a maximum integer, and there is no overflow. Consequently, Quint’s integers are mathematically unbounded. For example, the following is a perfectly valid Quint module:

  module big_numbers {
    pure val MAX_IPV6: int = 2^128 - 1
 
    pure def fits_in_64_bits(x) = x >= 0 and x < 2^64
  }

This unbounded nature is highly useful. Because Quint is a specification language, it allows you to abstract away the machine-level constraints that traditional programming languages force you to consider immediately. When you first begin specifying a system, you likely do not yet know whether a variable should be implemented as a uint32 or an int8. Unbounded integers let you focus entirely on your core design choices before committing to these low-level details.

Although the language will allow you to write arbitrarily large integers, the verification tools you may use on your specs come with their own practical boundaries. Knowing these constraints and choosing the toolset that best fits your needs is a major step towards writing robust specifications. We will cover Quint’s tooling and verification methods in later lessons, but for now, it is important to clarify:

• When using the Rust backend (the default for quint run or quint repl), integer literals must fit within the 64-bit signed integer range (-2^63 to 2^63-1). Using integers outside of this range will result in an error.

• The Typescript backend (called via the --backend=typescript flag for the quint run or quint repl commands) has no fixed limits on integer size.

• When using the TLC model checker (called with quint verify --backend=tlc), integer literals must fit within the 32-bit signed integer range (-2^31 to 2^31-1). Using integers outside of this range will result in an error.

• The Apalache verifier (the default for quint verify) has no fixed limits on integer size.

Fortunately, for most use cases you may have, the size of integers will not matter to you. Practical systems typically operate on smaller, bounded integers anyway and exceeding these thresholds is a rare exception rather than the norm. If you are primarily interested in exploring concurrency and state interleavings, then Quint’s default tooling will serve you perfectly. However, if you are modelling a system that relies heavily on large-scale arithmetic, you will want to take advantage of Apalache (Quint’s default verifier) or use the TypeScript simulator (--backend=typescript).

If you are interested in modelling bounded integers and clearly communicate your intentions, you can enforce these constraints explicitly using predicates rather than relying on the type system. It is straightforward to express standard 32-bit, 64-bit, 128-bit and 256-bit limits with Quint integers. We will explore exactly how to do this in the Modelling Bounded Integers section.

Built-in Operators

Quint has the standard built-in arithmetic operators for integers that you would expect in a programming language. We cover them here while omitting some operators that produce sets and lists. These will be covered in their corresponding lessons.

Most integer operators in Quint have two forms:

• The infix form is the idiomatic syntax you will use most of the time.
• The named form provides an alternative calling syntax that is primarily intended for tooling and is rarely used by programmers directly.

Let’s see an example of these two calling styles. Addition is one of the most basic operations you can perform on integers. Try evaluating the following expressions in the REPL.

The infix form uses the standard syntax you would expect:

// i + j is the infix integer addition
3 + 5

Equivalently, the named form of this operator also performs integer addition:

// iadd is the named integer addition
iadd(3,5)

Arithmetic Operators

Knowing operator precedence is essential for writing accurate specifications. The following table summarizes all arithmetic operators from highest to lowest precedence, along with both their infix and named forms.

Arithmetic operators follow standard precedence rules, where operators at the same level are evaluated left to right:

• Exponentiation ^ binds the tightest.
• Multiplication *, division /, and modulo % share the next level.
• Addition + and subtraction - share the lowest level.

Also, it is worth noting that:

• Integer division truncates towards zero. For example, 7 / 2 evaluates to 3, not 3.5. Because of this truncation, - 7 / 2 evaluates to -3 and not -4.
• Division by zero is undefined and will cause a runtime error.
• Exponentiation is not defined on all of its arguments. 0 ^ 0 and i ^ j for j < 0 are both undefined and will throw a runtime error.

Comparison Operators

Comparison operators also have both infix and named forms:

All comparison operators evaluate to bool. Try running a few examples in the REPL to confirm your intuition about these operations.

Note: Observe that eq and neq (== and != respectively) are polymorphic operators: they work for any type, not just int. Their signature is (t, t) => bool, requiring both arguments to be of the same, arbitrary type. See the Types lesson for more details on polymorphism in Quint.

Modelling Bounded Integers

As previously mentioned, there are times when we need to formalize constraints on the size of integers directly in our specifications. This may be necessary for systems that use checked math, have specific rules for handling overflows, or require integers to remain within strict boundaries. In Quint, you enforce these limits using predicates rather than relying on the type system.

Consider the following example. We can start by fixing the actual maximum integer allowed in our system, along with a declarative type alias:

  // Note that UInt32 values are still integers
  type UInt32 = int
 
  // The actual upper bound
  pure val MAX_UINT32: UInt32 = 2^32 - 1

With this in place, we can define useful predicates. For example, we can check whether a value falls within the valid range.

  pure def isUInt32(i: int): bool = (0 <= i and i <= MAX_UINT32)

Finally, we can use isUInt32 as a guard on definitions to prevent overflow and underflow:

  type Result = Ok | Err(str)
 
  pure def isTransferInRange(balance: int, amount: int): bool = isUInt32(balance + amount)
 
  pure def transfer_result(balance: int, amount: int): Result =
    if (isTransferInRange(balance, amount))
      Ok
    else
      Err("transfer out of range")

The key insight here is that the type checker will not catch out-of-range values. UInt32 is still just int under the hood. The constraint lives in your definitions’ preconditions and invariants, not in the type system.

This example is adapted from the more comprehensive bank specification that we develop step by step in the Anatomy lesson. There, you can see these bounded integer patterns applied within a complete system.

In the Quint spells directory , you will find the BoundedUInt  module. While slightly more advanced than what we cover in this introductory lesson, this file contains a variety of sophisticated bounded unsigned integer operations that you can easily import and use in your own specifications.

In the spec you will find:

• A series of checked operations (checkedAdd, checkedSub, etc.) that return an Option sum type indicating either a successful result or an overflow error.
• A series of saturating operations (saturatingAdd, saturatingSub, etc.) that cap at the numeric bounds instead of overflowing.
• A series of wrapping operations (wrappingAdd, wrappingSub, etc.) that always return the result of the operation wrapping around at the boundary of the type.

These operations can be very useful for specifying systems with tailored overflow behavior.

Decimals

However, for cases where you are working with percentages, exchange rates, or other fractional values, it is helpful to have a way of representing these numbers in your Quint spec. In this section, we cover some approaches you can take to incorporate such values into your models.

The most straightforward technique is to use fixed-point arithmetic. In this case you simply choose a scale factor and work entirely with integers. For example, you could represent currency in cents instead of dollars:

  // $2.00 represented as 200 cents
  pure val price: int = 200
 
  // 10% fee rate
  pure val rate: int = 10
  pure val rateScale: int = 100
 
  // correct: multiply first, then divide
  pure val fee: int = price * rate / rateScale    // 20
    
  // wrong: dividing first loses precision
  pure val fee_truncated: int = price * (rate / rateScale) // 0

Because integer division truncates towards zero, the order of operations is critical here. You must always multiply before dividing to avoid losing precision. While effective, this approach is still limited: you will have problems representing anything smaller than your base scale (such as fractions of a cent).

A second option is to use rational arithmetic. By representing fractions as pairs of integers (a numerator and a denominator), you can perform exact mathematical calculations without being constrained by a fixed scale. The Decimals Module  provides a ready-made implementation of this exact pattern that you can easily import into your specifications.

Let’s look at a simple example of how to use this. First, you will need to download the decimals module:

curl -O https://raw.githubusercontent.com/informalsystems/partnership-heliax/refs/heads/trunk/PoS-quint/dec.qnt

Once downloaded, you can use its definitions simply by importing the module into your specification:

  module pool {
      // we import the Decimals module here
      import Dec.* from "./dec"
  
      pure val funds: int = 100
      pure val members: int = 3
  
      // exact: (100, 3) no truncation
      pure val sharePerMember: Dec = div(dec(funds), dec(members))
  
      // when you need an integer: 33
      pure val shareFloor: int = truncate(sharePerMember)
  }

To understand how this works under the hood, here are the relevant definitions from the module we are using here:

  module Dec {
    type Dec = (int, int)
 
    pure def dec(i: int): Dec =
        (i, 1)
 
    // assumes that b!=0
    pure def div(a: Dec, b: Dec): Dec =
        (a._1 * b._2, a._2 * b._1)
 
    pure def truncate(a: Dec): int =
        a._1 / a._2
        
    // ... more interesting definitions
  }

The complete Dec module includes operations for addition, subtraction, multiplication, division, exponentiation, comparisons, and rounding (truncate, ceil). Ultimately, both approaches trade off simplicity against precision: fixed-point is straightforward but loses precision below the scale factor, while the Dec module gives you exact arithmetic at the cost of slight additional complexity.

Summing it up

In this lesson, we covered the basic principles for working with integers in Quint. Because integers are a built-in core type, you can start using them without any imports. We explored the standard infix operators you will use daily, alongside their named equivalents.

We also discussed that while Quint integers are big integers, modelling specific systems and working with verification tools often requires bounding them. This can be done explicitly by defining appropriate predicates rather than relying on the type system, as we show in the BoundedUInt  spell. Finally, we explored how fixed-point arithmetic and the Dec module  can fill the gap left by the absence of floating-point types whenever your specifications require fractional values.