Machine integers or "True" integers?

In K's builtin domains.k library we find a suite of functions implementing machine integers of arbitrary bit width represented in 2's complement. For example:

  /*@
   * Addition, subtraction, and multiplication are the same for signed and
   * unsigned integers represented in 2's complement
   */
  syntax MInt ::= addMInt(MInt, MInt)   [function, hook(MINT.add), smt-hook(bvadd)]
                | subMInt(MInt, MInt)   [function, hook(MINT.sub), smt-hook(bvsub)]
                | mulMInt(MInt, MInt)   [function, hook(MINT.mul), smt-hook(bvmul)]

Currently, this repo is not using these builtins, but rather, similar to evm-semantics, uses "True" integer representations + modulo operations.

I'm curious what the best approach is here. In writing proofs of EVM programs, a lot of effort goes in into writing lemmas that deals with quite simple arithmetic, which can otherwise be proven directly using the right SMT definitions. On the other hand, SMT theories dealing with large bitvectors (such as the 256-bit words of the EVM) quickly start being more difficult to reason with than modulo integer arithmetic.

There might also be speedups of concrete executions to consider in this choice. I expect the MINT library to be faster than custom made extra rules.

I'm tentatively in favor of replacing the custom rules dealing with machine integers in numeric.md in favor of the MINT module of domains.k, but I'm curious of others people's thoughts here. @ehildenb @hjorthjort @dwightguth

The issue names numeric.md as the current custom-rule entry point and points to the MINT module in K's domains.k. Read those definitions first, then compare the existing representation with MINT for proof and concrete-execution impact; done requires an agreed approach and corresponding semantics changes, but no acceptance criteria are specified.