quint verify converts big integers to MAX_INT somewhere

[konnov]

Here is a very simple example:

module t {
  var balance: int

  action init = {
    balance' = 100_000_000_000
  }

  action step = {
    balance' = balance + 10_000
  }

  action inv = {
    balance < 10_000
  }
}

Run quint verify as follows (with the proper ritual of starting the Apalache server first):

$ quint verify --invariant=inv t.qnt
An example execution:

[State 0] { balance: 2147483647 }

error: found a counterexample

It's obvious that the translation has converted a big integer to i32 MAX_INT somewhere on the way.

[shonfeder]

I suspect this is may be happening when deserializing into Apalache's version of the QuintIR.
Hopefully we just need to change

https://github.com/informalsystems/apalache/blob/d201ebaedeb21692e80d8cd27927819f5d0817c4/tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintIR.scala#L134-L137

to be

-  @key("int") case class QuintInt(id: Int, value: Int) extends QuintEx {}
+  @key("int") case class QuintInt(id: Int, value: BigInt) extends QuintEx {}
   object QuintInt {
     implicit val rw: RW[QuintInt] = macroRW
   }

thanks to upickle's support for BigInts.

[thpani]

Wow, thanks for the pointer!

This kind of deserialization looks highly optimistic on unpickle's end though. @shonfeder is there a way to make upickle throw instead of just truncating numbers?

[thpani]

Well, I changed it to BigInt and got this grandiose error message from upickle:

> Input was not a valid representation of the QuintIR: expected string got float64 at index -1 E@11:54:24.817

The reason is that upickle expects fields that are deserialized to BigInt to be a string in the JSON.
I will look at what we are currently doing with counterexamples and ITF, to keep things roughly synchronized.

[thpani]

There's this PR on the upickle repo, but it seems it never made it in:
com-lihaoyi/upickle#191

[thpani]

Not fixed until we also patch the Quint side