C++ support for unconstrained ints

[robin-aws]

There is no real standard for "big integers" in C++ AFAIK, so the current compiler only supports constrained subset types like uint32.

This is the main gap blocking running many existing tests in the test suite against the C++ compiler, so it's making it difficult to measure just how complete the C++ compiler is. I'd be happy with even just the incremental step of depending on a big integer library only when running the Dafny test suite.

cc @parno

[parno]

Can you clarify what you have in mind for depending on a big integer library only when running the test suite?

[robin-aws]

I'm just suggesting that if we are nervous about picking a big integer implementation as an official dependency, it might be possible to pick one and make it clear that it's only to unblock more general C++ compiler testing and not production ready. Heck, perhaps we could even embed a really simple, inefficient version in DafnyRuntime.h for that purpose?

[parno]

Ah, I see. Thanks for the clarification. If I find a motivated student, I'll see what we can do :)

[robin-aws]

@parno: just had a thought that we could build a simple, inefficient (but formally-verified!) big integer implementation based on the positional natural numbers library under review here: dafny-lang/libraries#15 That would provide a great default backend for int for all new compilers, as long as there was an easy way to replace it with a much more performant version when available.

[parno]

Interesting, so you're imagining a two-stage compilation process, where we first compile the big-integer library, and then we compile subsequent Dafny programs, assuming the compiled big-integer library is available?

[robin-aws]

Exactly. I'd love for more of the Dafny runtime code for the various target languages to be compiled from Dafny itself, based on a smaller kernel for each language. The implementations of seq<T> in C# and Java, for example, look very similar, and could be implemented instead as a reflective Dafny trait with multiple classes implementing it, so that other runtimes (current and future) could take advantage of that optimization.