C support

[seebees]

If C is a compile target, these function are useful. However, it is hard because they use int | nat et al. This makes sense, but blocks using theses function if you want to support a C compile target.

There are many ways that might work to support this. This might imply some feature in Dafny such that if I can prove that I'm always using bounded numbers, then everything will just work.

[robin-aws]

One solution that's somewhat relevant: in my dafny-runtime-in-dafny branch, I've got an abstract module that defines lots of sequence-related declarations in terms of a newtype size_t, where the actual upper bound is not defined: https://github.com/robin-aws/dafny/blob/dafny-runtime-in-dafny/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy#L39-L52

A concrete refining module per target language then actually defines what that limit is, and therefore allows the compiler to pick the appropriate native type: https://github.com/robin-aws/dafny/blob/dafny-runtime-in-dafny/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntimeGo.dfy

We could use a similar approach in this repo to allow clients to choose the desired bounded type for the generic declarations. The only issue is I don't see a way to opt-out of bounding the type and just use int instead.

Just to double-check:

This makes sense, but blocks using theses function if you want to support a C compile target.

It would not be a hard blocker for using the C++ compiler if we implement https://github.com/dafny-lang/dafny/issues/1259. I'm assuming you'd have the hard requirement of not using BigIntegers at runtime, however. But then I have to ask, won't that be a large enough efficiency concern for using some of the code in this repo for other compilation targets as well? IOW, this request isn't necessarily C-specific if you add that efficiency requirement.