Features to avoid any uses of unbounded ints at runtime

[robin-aws]

Summary

As a Dafny developer, I want to ensure I don't ever use unbounded ints at runtime unless it is actually necessary.

Background and Motivation

The Dafny int type is unbounded, which is excellent for mathematical reasoning without worrying about overflow, but is always more expensive at runtime than a bounded type like newtype x: int | 0 <= x < 256 that maps to a direct primitive numeric type in the target language. It's very easy to accidentally write verified Dafny code that ends up very slow at runtime, because the uses of int can be quite implicit - see #6100 for example.

Proposed Feature

There are multiple possible ways to tackle this:

1. The weakest guarantee could be just a runtime error if the target language's BigInteger type is every used. This could be enabled just for unit tests to catch references to int in the source program. This is probably the cheapest to implement.
2. Another mode could emit compile-time errors on any reference to int. This would be much more reliable since it would catch cases not covered by tests and prevent the wrong code from being written in the first place.
3. Since you will often end up with existing code bases that use int and then want to optimize that away, we could allow users to opt-in to interpreting int as bounded by shared fixed limits. A reasonable default bound might be the equivalent of uint64, but it's likely useful to let users select 32-bit numbers or narrower if that fits their application.

Independently, there should probably be a way to allow exceptions. For 1 and 2 this means suppressing the run-time or compile-time error, but for 3 this means also defining a bigint synonym of some kind.

Alternatives

Enumerated some in the above section. Not immediately aware of prior art, biasing for cutting the issue first.

[robin-aws]

Also relevant: #1259 - the C++ backend already implements a form of option 2, since it don't support unbounded integers at all.

[ajewellamz]

For CryptoTools, only option 3 has any value.
We have far too many uses of int and nat to change them all in the Dafny code.