Java code generation incorrect

[ajewellamz]

Dafny version

3.10 and 4.0

Code to produce this issue

newtype uint8 = x : int | 0 <= x < 256

predicate method IsHex(ch : char)
{
  || '0' <= ch <= '9'
  || 'a' <= ch <= 'f'
}

// return the hex character for this hex value
function method HexVal(x : uint8) : (res : char)
  requires x < 16
  ensures IsHex(res)
{
  if x < 10 then
    '0' + x as char
  else
    'a' + (x - 10) as char
}

// return the hex string for this byte
function method HexStr(x : uint8) : (ret : string)
  ensures |ret| == 2
  ensures IsHex(ret[0]) && IsHex(ret[1])
{
  if x < 16 then
    var res := ['0', HexVal(x)];
    res
  else
    var y := x as bv8;
    var res := [HexVal((y >> 4) as uint8), HexVal((y & 0xf) as uint8)];
    res
}

// return the hex string for these bytes, keeping any leading zero
function method {:tailrecursion} HexFmt(val : seq<uint8>) : (ret : string)
  ensures |ret| == 2 * |val|
  ensures forall ch <- ret :: IsHex(ch)
{
  if |val| == 0 then
    []
  else
    HexStr(val[0]) + HexFmt(val[1..])
}

  method {:test} TestBeacon() {
    var binary := [0x00,0x11,0x22,0x33,0x44,0x55,0x66,0x77,0x88,0x99,0xaa,0xbb,0xcc,0xdd,0xee,0xff];
    var str := "00112233445566778899aabbccddeeff";
    var conv := HexFmt(binary);
    print "\n", str, "\n", conv, "\n";
    expect str == conv;
  }

Command to run and resulting output

This passes the test
dafny /functionSyntax:3 /compileTarget:cs /runAllTests:1 /compile:3 HexFail.dfy

This fails the test
dafny /functionSyntax:3 /compileTarget:java /runAllTests:1 /compile:3 HexFail.dfy

What happened?

I expected both languages to pass.

Given the
ensures forall ch <- ret :: IsHex(ch)
I expected java to only produce hex characters, but instead of
00112233445566778899aabbccddeeff
java produces
0011223344556677ŏ8Ő9őaŒbœcŔdŕeŖf

In HexStr, where I have
var y := x as bv8;
var res := [HexVal((y >> 4) as uint8), HexVal((y & 0xf) as uint8)];
If I replace it with
var res := [HexVal((x / 16) as uint8), HexVal((x % 16) as uint8)];
then both languages are happy, so I'm guessing (y >> 4), with the leftmost bit set, does the "signed int" thing and extends the sign bit.

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

Mac