How to prove properties of non-linear operators involved in LEB128 algorithm in Dafny?

I'm trying to prove that encoding/decoding a (signed) LEB128 algorithm is lossless.

https://en.wikipedia.org/wiki/LEB128

What's got me stuck is the "Sign Extension" operation for the negative numbers. Since the integers in Dafny is unbounded, I have to use stuff like % and / to simulate the sign extension, which I guess stuck the solver. The property I tried to prove is SLebLosslessNeg, its positive counterpart can be derived automatically by Dafny.

Here is my code:

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, "\n";
    i := i + 1;
  }

I think the pow is causing the issue here as Dafny couldn't figure out how to connect it to the 2's complement, but I don't know how to tell Dafny such things. I have a rather vague idea of bounding each n using 0 <= n < 2^p and showing Dafny such a thing holds, but it's just an idea, and I don't know how to approach it...

Also, I tested my algorithm with input in [-100000, 100000], and the results are correct.

EDIT: Updated to include functions. Thanks, @Hath995.

I tried to approach this problem in a more step-wise way.

In short, I have updated the code to do the complement as the SDecode proceeds. But it still does not work. I think it's that Dafny could not figure out the link between the complement and the encoding process.

In the encoding, there is no explicit complement occurs, Dafny does this automatically due to the feature of Euclidean division, but it fails to do so when the process is reversed.

EDIT Removed confusing assumption.

Solution

Thanks to @Hath995, I have come up with a solution.

The key to the proof is two parts.

There are TWO cases of SDecode's result. carry == 0 and carry == 1. Both are needed to be included in the base case where |s| == 1.
Need to show the equivalence between X % 128 - 128 and (!X & 0x7f) + 1

The proof is as follows.

  lemma SLebLosslessNeg(s: LEB128, n: int)
    requires |s| > 0
    requires n < 0
    requires s == SEncode(n)
    ensures SDecode(s) == n
  {
    //assume {:axiom} SDecode(SEncode(n)) == n;
    if |s| == 1 {
      assert SDecode(s) == n;
      assert SDecodeNeg(s, 0) == n + 1; // base case 1: carry == 0
      assert SDecodeNeg(s, 1) == n;     // base case 2: carry == 1
    } else {
      calc {
        SDecode(s);
        -(((!(s[0] - 0x80) - 0x80) + 1) as int) + 128 * SDecodeNeg(s[1..], 0);
        -(((!((n % 128) as bv8) - 0x80) + 1) as int) + 128 * SDecodeNeg(s[1..], 0);
        (n % 128) - 128 + 128 * SDecodeNeg(s[1..], 0);
        { SLebLosslessNeg(s[1..], n / 128); }
        (n % 128) - 128 + 128 * (n / 128 + 1);
      }
    }
  }