如何在Dafny中证明带符号LEB128编解码的无损性？

我正在尝试证明带符号LEB128算法的编解码过程是无损的。正数对应的引理SLebLosslessPos可由Dafny自动推导，但负数的SLebLosslessNeg引理始终无法完成证明，瓶颈在于负数的符号扩展操作：由于Dafny中的整数是无界的，我只能用%和/来模拟符号扩展，这导致求解器无法关联编码时的欧几里得除法与解码时的补码操作。

我已在[-100000, 100000]范围内测试该算法，结果正确，但证明始终无法通过。

以下是我的代码：

type LEB128 = seq<bv8>

function Abs(n: int) : int
{
  if (n < 0) then -n else n
}

function SEncode(N: int) : (S: LEB128)
  decreases Abs(N)
  ensures |S| > 0
  ensures S[|S|-1] < 0x80
  ensures N < 0 <==> S[|S|-1] % 128 >= 64
  ensures N >= 0 <==> S[|S|-1] % 128 < 64
{
  var c := (N % 128) as bv8;
  var r := N / 128;
  if (r == 0 && c < 64) || (r == -1 && c >= 64) then
    [c]
  else
    [c + 0x80] + SEncode(r)
}

function SDecode(S: LEB128) : (N: int)
  requires |S| > 0
  requires S[|S|-1] < 0x80
{
  if S[|S|-1] < 0x40 then
    SDecodePos(S)
  else
    SDecodeNeg(S, 1)
}

function SDecodePos(S: LEB128) : (N: int)
  requires |S| > 0
  requires S[|S|-1] < 0x80
  ensures N >= 0
{
  if |S| == 1 then
    S[0] as int
  else
    (S[0] - 0x80) as int + 128 * SDecodePos(S[1..])
}

function SDecodeNeg(S: LEB128, carry: bv8) : (N: int)
  requires |S| > 0
  requires S[|S|-1] < 0x80
  ensures N <= 0
{
  var c := if |S| == 1 then S[0] else S[0] - 0x80;
  if |S| == 1 then
    var temp := ((!c - 0x80) + carry) as int;
    -temp
  else
    var temp := ((!c - 0x80) + carry) as int;
    -temp + 128 * SDecodeNeg(S[1..], (c / 128) as bv8)
}

lemma SLebLosslessPos(n: int)
  requires n >= 0
  ensures SDecode(SEncode(n)) == n
{}

lemma SLebLosslessNeg(s: LEB128, n: int)
  requires |s| > 0
  requires n < 0
  requires s == SEncode(n)
  ensures SDecode(s) == n
{}


method Main() {
  var i := -100000;
  while i < 100000 {
    var s := SEncode(i);
    var n := SDecode(s);
    print s, " ",  n, " ", i == n, " ", i, "
";
    i := i + 1;
  }
}

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