Error Running quint verify

[zicklag]

I'm getting an error when trying to run quint verify on the example bank.qnt from the website:

module bank {
  /// A state variable to store the balance of each account
  var balances: str -> int
 
  pure val ADDRESSES = Set("alice", "bob", "charlie")
 
  action deposit(account, amount) = {
    // Increment balance of account by amount
    balances' = balances.setBy(account, curr => curr + amount)
  }
 
  action withdraw(account, amount) = {
    // Decrement balance of account by amount
    balances' = balances.setBy(account, curr => curr - amount)
  }
 
  action init = {
    // At the initial state, all balances are zero
    balances' = ADDRESSES.mapBy(_ => 0)
  }
 
  action step = {
    // Non-deterministically pick an address and an amount
    nondet account = ADDRESSES.oneOf()
    nondet amount = 1.to(100).oneOf()
    // Non-deterministically choose to either deposit or withdraw
    any {
      deposit(account, amount),
      withdraw(account, amount),
    }
  }
 
  /// An invariant stating that all accounts should have a non-negative balance
  val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0)
}

➜ quint verify bank.qnt --invariant=no_negatives
cli.js verify <input>

Verify a Quint specification via Apalache

Options:
  --help                Show help                                      [boolean]
  --version             Show version number                            [boolean]
  --out                 output file (suppresses all console output)     [string]
  --main                name of the main module (by default, computed from
                        filename)                                       [string]
  --init                name of the initializer action[string] [default: "init"]
  --step                name of the step action       [string] [default: "step"]
  --invariant           the invariants to check, separated by commas    [string]
  --temporal            the temporal properties to check, separated by commas
                                                                        [string]
  --out-itf             output the trace in the Informal Trace Format to file,
                        e.g., out.itf.json (suppresses all console output)
                                                                        [string]
  --max-steps           the maximum number of steps in every trace
                                                          [number] [default: 10]
  --random-transitions  choose transitions at random (= use symbolic simulation)
                                                      [boolean] [default: false]
  --apalache-config     path to an additional Apalache configuration file (in
                        JSON)                                           [string]
  --verbosity           control how much output is produced (0 to 5)
                                                           [number] [default: 2]
  --apalache-version    The version of Apalache to use, if no running server is
                        found (using this option may result in incompatibility)
                                                    [string] [default: "0.46.1"]
  --server-endpoint     Apalache server endpoint hostname:port
                                            [string] [default: "localhost:8822"]

RangeError [ERR_BUFFER_OUT_OF_BOUNDS]: "length" is outside of buffer bounds
    at proto.utf8Write (node:internal/buffer:1066:13)
    at Op.writeStringBuffer [as fn] (/home/zicklag/.local/share/pnpm/global/5/.pnpm/protobufjs@7.4.0/node_modules/protobufjs/src/writer_buffer.js:61:13)
    at BufferWriter.finish (/home/zicklag/.local/share/pnpm/global/5/.pnpm/protobufjs@7.4.0/node_modules/protobufjs/src/writer.js:453:14)
    at /home/zicklag/.local/share/pnpm/global/5/.pnpm/@grpc+proto-loader@0.7.13/node_modules/@grpc/proto-loader/build/src/index.js:177:109
    at Array.map (<anonymous>)
    at createPackageDefinition (/home/zicklag/.local/share/pnpm/global/5/.pnpm/@grpc+proto-loader@0.7.13/node_modules/@grpc/proto-loader/build/src/index.js:177:39)
    at Object.loadSync (/home/zicklag/.local/share/pnpm/global/5/.pnpm/@grpc+proto-loader@0.7.13/node_modules/@grpc/proto-loader/build/src/index.js:223:12)
    at loadProtoDefViaReflection (/home/zicklag/.local/share/pnpm/global/5/.pnpm/@informalsystems+quint@0.22.3/node_modules/@informalsystems/quint/dist/src/apalache.js:169:37)
    at tryConnect (/home/zicklag/.local/share/pnpm/global/5/.pnpm/@informalsystems+quint@0.22.3/node_modules/@informalsystems/quint/dist/src/apalache.js:239:19)
    at connect (/home/zicklag/.local/share/pnpm/global/5/.pnpm/@informalsystems+quint@0.22.3/node_modules/@informalsystems/quint/dist/src/apalache.js:329:36) {
  code: 'ERR_BUFFER_OUT_OF_BOUNDS'

I've also tested using my own apalache install with the same result.

Versions

➜ java --version
openjdk 17.0.13-internal 2024-10-15
OpenJDK Runtime Environment (build 17.0.13-internal+0-adhoc..src)
OpenJDK 64-Bit Server VM (build 17.0.13-internal+0-adhoc..src, mixed mode, sharing)

➜ quint --version
0.22.3

apalache-0.47.0

[bugarela]

Thanks for the repo! Did you ever run quint verify for anything else btw? This seems to me like a general problem, not specific to the bank.qnt spec - am I correct?

Also, which OS are you on?

[zicklag]

Yeah, I couldn't get quint verify to work on any file yet.

I'm on Linux Pop!_OS 22.04 ( which is essentially Ubuntu 22.04 ):

Linux pop-os 6.9.3 x86_64 GNU/Linux

For some extra background, I had this work at one point on my system months ago, and then I ran it recently I'm not aware that I changed anything, but maybe my node module got updated, and this time I didn't work, so I'm not sure exactly what changed.

[bugarela]

Seems like this was a problem on node and was fixed in Node v22.8.0. This is the PR: nodejs/node#54524. There are a bunch of related issues there. Can you try upgrading your Node (or downgrading to 20 where the issue was not present yet)?

[zicklag]

That worked, thank you!