search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.89k stars 259 forks source link

C++ support for unconstrained ints #1259

Open robin-aws opened 3 years ago

robin-aws commented 3 years ago

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 commented 3 years ago

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

robin-aws commented 3 years ago

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 commented 3 years ago

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

robin-aws commented 3 years ago

@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: https://github.com/dafny-lang/libraries/pull/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 commented 3 years ago

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 commented 3 years ago

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.