[Heapster] Improve widening for changing offsets

[m-yac]

This PR improves the way widening works in Heapster to be able to handle examples where a pointer into a block of memory is modified (e.g. incremented) over the course of a loop. For example:

uint64_t sum(const uint8_t *arr, size_t len) {
  uint64_t sum = 0;
  while (len--) {
    sum += arr[0];
    arr += 1;
  }
  return sum;
}

This is in service of being able to handle this sha512 example which this PR adds to the heapster-saw/examples directory – though currently, only the function above (which mirrors the loop structure of sha512_block_data_order) has been verified.

[eddywestbrook]

The coq proof for this seems to be stuck in an infinite loop. The CI says that it blew the stack.

[m-yac]

@eddywestbrook looks like the heapster-saw CI passes now. It was Coq type-checking that got stuck in an infinite loop 🤦‍♂️

[eddywestbrook]

Overall this looks great, good job! Please address the one change I suggested.

[eddywestbrook]

Please put these two helper functions into Permissions.hs and make them top-level functions

[m-yac]

Done. I initially added them to the bitvector section but they depend on the definition of PartialSubst, so I added them in a new section below that definition.

[eddywestbrook]

Nice, I like this. At first I thought there were multiple potential solutions for z, which would be problematic if we chose the wrong one, but you are right, this is a most general solution