Avoiding BigInteger

[ajewellamz]

Dafny version

3.10.0.41215

Code to produce this issue

include "../../private-aws-encryption-sdk-dafny-staging/libraries/src/Wrappers.dfy"

module Integer52 {
  import opened Wrappers

  const UInt52Limit := 0x10000000000000

  // requires BigInt
  // newtype UInt52 = x : nat | 0 <= x < UInt52Limit
  // type seq52<T> = x : seq<T> | |x| < UInt52Limit

  // does not require BigInt
  newtype UInt52 = x : nat | 0 <= x < 0x10000000000000
  type seq52<T> = x : seq<T> | |x| < 0x10000000000000
  type map52<T,U> = x : map<T,U> | |x| < 0x10000000000000

  const uint52Max := 0xfffffffffffff as UInt52

  function method Add52(a : UInt52, b : UInt52)
    : Result<UInt52, string>
  {
    if b < (uint52Max - a) then
      Success(a + b)
    else
      Failure("overflow")
  }

  // Fails for c++ "Subtraction of non-native type"
  function method Add52X(a : UInt52, b : UInt52)
    : Result<UInt52, string>
  {
    if b < ((UInt52Limit - 1) as UInt52 - a) then
      Success(a + b)
    else
      Failure("overflow")
  }

  function method Append52<T>(a : seq52<T>, b : seq52<T>)
    : Result<seq52<T>, string>
  {
    if (|b| as UInt52) < (uint52Max - (|a| as UInt52)) then
      Success(a + b)
    else
      Failure("overflow")
  }
}

Command to run and resulting output

No response

What happened?

Avoiding the use of the BigInteger type is important for performance in all languages, and especially important for C++ where it's simply not supported.

Unfortunately, the subtlest of changes can unexpectedly make BigInteger pop up.

In the above code,

newtype UInt52 = x : nat | 0 <= x < 0x10000000000000

needs no BigInteger, where

const UInt52Limit := 0x10000000000000
newtype UInt52 = x : nat | 0 <= x < UInt52Limit

unexpectedly does.

There was another tiny change that resulting in the parameters to Add52 becoming BigIntegers, but I can't seem to reproduce it.

==========================

For context, we're experimenting with UInt52 because JavaScript integers are limited to 52 bits, and we'll want code that avoids BigIntegers everywhere, so we can ship in C++.

I realize that this is not a feature request issue, but it seems that this is exactly the sort of thing that should be provided by the Dafny library, i.e. the largest possible numeric types that avoids BigIntegers in all target languages, and far more importantly, support for actually using them, including earlier warnings when BigIntegers have unintentionally been triggered.

What type of operating system are you experiencing the problem on?

Mac

[davidcok]

This is possibly related to constant folding that allows a symbolic constant to be used in a newtype at all. In this case, it is likely not a performance problem, as the computation would be done just once. However, that does not helpwhere BigInteger is not supported at all.

[fabiomadge]

Consider checking out this table to get a sense of the viability of compiling the ESDK to C++ today.

[ajewellamz]

Wow, I had no idea that C++ was so unsupported. It makes me wonder why you pretend that it is.

Next to the C++ column in that table is a "Dafny" column. What is that column trying to convey?

[fabiomadge]

We try to refrain from claiming full C++ support, like not mentioning it on the website. The Dafny column is broken and an artefact of a work-in-progress effort to compile Dafny to a subset of it.

[MikaelMayer]

Would either the following work for you?

const {:compile false} UInt52Limit := 0x10000000000000
ghost const UInt52Limit := 0x10000000000000

[ajewellamz]

Yes, either of those would work. The "ghost" one seems better to me.

[MikaelMayer]

I leave this issue open in case someone wants to work on a flag to raise these early warnings.