Support for rationals in the simulator

[shonfeder]

Discussed in https://github.com/informalsystems/quint/discussions/1159

^{Originally posted by konnov September 12, 2023} Champions: @andrey-kuprianov and @angbrav

We had a very long discussion about native support for rationals in the Quint simulator and, potentially, in Apalache. The same issue was raised in the past by @rnbguy and @ivan-gavran.

Given that Andrey or Manu are specifying a protocol, e.g., a DEX or a PoS protocol,

When they need to express a fraction, e.g., $\frac{2}{3}$, and later multiply it by an integer, e.g., $\frac{2}{3} \cdot n$,

Then they do not want to lose precision (e.g., truncating $\frac{2}{3}$ would produce 0), that is, they want to use a standard module to express rational numbers.

The current solution is to simply encode a rational number as a pair (nom, denom). There are two specifications that implement this idea: HighPrecisionDec.tla and dec.qnt. In principle, this works reasonably well for SMT, though this solution may lead to hard problems quickly. In case of the random simulator, it may quickly happen that the nominator and denominator are growing very fast, as the trivial implementation does not enforce the canonical representation of rationals, that is, that nom and denom do not have a common divisor (different from 1).

Potential solution:

1. Introduce a standard library for rationals, which is probably just a small refactoring of dec.qnt.
2. Override operations over rationals by using a library, e.g., bigint-rational.