为何Dafny的encode_varint返回空序列？LEB64编解码无损性验证异常

我正在尝试证明LEB64（类LEB128）变长整数的编解码过程是无损的，编写了如下Dafny代码：

function decode_varint(input: seq<bv8>) : bv64
    requires |input| > 0
{
    var byte := input[0];
    var val := (byte & 0x7F) as bv64;
    var more := byte & 0x80 == 0 && |input| > 1;

    if more then val | (decode_varint(input[1..]) << 7) else val
}

function encode_varint(input: bv64) : seq<bv8>
{
    var byte := (input & 0x7F) as bv8;
    var shifted := input >> 7;
    if shifted == 0 then [byte | 0x80] else [byte] + encode_varint(shifted)
}

lemma Lossless(input: bv64) {
    var test := encode_varint(128);
    var encoded := encode_varint(input);
    var decoded := decode_varint(encoded);
    assert decoded == input;
}

但Lossless引理中的断言无法成立，使用VSCode插件的反例功能（F7）查看时，反例选取的input值为0x8000000000000000，且test变量的值显示为test:seq<bv8> = ()。

我有两个困惑：

• Dafny中序列通常以方括号表示，为何此处显示为()？
• encode_varint函数逻辑上不可能返回空序列，且NeverEmpty引理已成功证明这一点：

lemma NeverEmpty(input: bv64) {
    var encoded := encode_varint(input);
    assert |encoded| > 0;
}

这到底是怎么回事？

补充：若添加如下Examples引理：

lemma Examples()
{
    assert encode_varint(1 << 7) == [0x00, 0x81];
    assert encode_varint(1 << 14) == [0x00, 0x00, 0x81];
    assert encode_varint(1 << 28) == [0x00, 0x00, 0x00, 0x00, 0x81];
    assert encode_varint(1 << 42) == [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x81];
    assert encode_varint(1 << 56) == [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x81];
    assert encode_varint(1 << 63) == [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x81];
    assert encode_varint(0x8000000000000000) == [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x81];
}

所有断言均可被证明，但仅保留最后一个针对反例值的断言时，却无法证明！

内容的提问来源于stack exchange，提问作者Timmmm