Compile WISL invariants to actual invariants.

[NatKarmios]

The problem

Currently, WISL loops with invariants are compiled to a separate function for the loop body, with a pre and post based on the invariant. This function looks something like:

f_loop0(vars) {
  if (guard) {
    // ... loop body goes here...
    vars = f_loop0(vars)
  }
  return vars
}

While this is semantically equivalent, it creates some issues when debugging or using the LSP in manual mode; if one needs to fold or unfold to match the pre of the recursive call to f_loop0, then they can't apply the inverse afterwads to make the post-condition match, like so:

f_loop0(vars) {
  if (guard) {
    // ... loop body goes here...
    [[ unfold P(x) ]]  // <- Still part of the loop body
    vars = f_loop0(vars)
    // Need to put [[ fold P(x) here]] !
  }
  return vars
}

This is particularly problematic as the debugger is instructed to stop at the recursive call, meaning it verifies fine while debugging, but does not for the LSP or CLI.

The short-term workaround

This may be unsound, but we can gain consistency by using assume false to vanish after the recursive call; we think this is okay, since the invariant is already established by performing the compositional recursive call.
This would look like:

f_loop0(vars) {
  if (guard) {
    // ... loop body goes here...
    vars = f_loop0(vars)
    [[ assume false ]]
  }
  return vars
}

The solution

GIL has native support for invariants (it didn't at the time WISL was written); we should just compile WISL invariant loops to GIL ones.