forall comprehension over bounded `newtype`

[seebees]

Dafny version

4.8.0

Code to produce this issue

module Foo {

  const TWO_TO_THE_64:  int := 0x1_00000000_00000000
  newtype uint64 = x: int | 0 <= x < TWO_TO_THE_64

  method Foo(lo: nat, hi: nat) {
    var t := new nat[hi](i => 1);
    forall i | lo <= i < hi
    {
      t[i] := i;
    }
  }

  method Bar(lo: uint64, hi: uint64) {
    var t := new uint64[hi](i => 1);
    forall i | lo <= i < hi
    {
      t[i] := i;
    }
  }

}

Command to run and resulting output

dafny translate java asdf.dfy

What happened?

The translated Java looks like this

    for (java.lang.Long _guard_loop_0_boxed0 : Foo.uint64.IntegerRange(java.math.BigInteger.ZERO, __default.TWO__TO__THE__64())) {
      long _guard_loop_0 = ((long)(java.lang.Object)(_guard_loop_0_boxed0));
      long _2_i = (long)_guard_loop_0;
      if (true) {
        if ((((dafny.Helpers.unsignedToBigInteger(_2_i)).signum() != -1) && ((dafny.Helpers.unsignedToBigInteger(_2_i)).compareTo(__default.TWO__TO__THE__64()) < 0)) && ((java.lang.Long.compareUnsigned(lo, _2_i) <= 0) && (java.lang.Long.compareUnsigned(_2_i, hi) < 0))) {
          (_0_t)[dafny.Helpers.toInt(dafny.Helpers.unsignedToInt((_2_i)))] = _2_i;
        }
      }
    }

As you can see this creates a huge range. This code can't even run its so big.
Additionally, if you are trying to use bounded numbers for performance,
that is to avoid BigInteger, even the IntegerRange for this type is sub-optimal.

  public static java.util.ArrayList<java.lang.Long> IntegerRange(java.math.BigInteger lo, java.math.BigInteger hi) {
    java.util.ArrayList<java.lang.Long> arr = new java.util.ArrayList<>();
    for (java.math.BigInteger j = lo; j.compareTo(hi) < 0; j = j.add(java.math.BigInteger.ONE)) { arr.add(java.lang.Long.valueOf(j.longValue())); }
    return arr;
  }

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

Linux, Mac