Add block granularity progress indication

[trktby]

This PR is part of a practical work supervised by @Aurel300. It is based on a previous work's PR. The main changes are:

• Adding new block-level gutter decorators, inspired by Dafny. Their purpose is to be able to track verification progress with a higher granularity than before. This includes a current block decorator to see on which basic block a program might be hanging during verification.
• Persisting partial results of a verification across selective verification runs - selectively verifying a method no longer wipes the results of the other, unmodified ones (they are marked as stale however).
• Refactoring of the storage of decorators. They are now stored and generated per method. Mainly for ease of organization of block-based decorators.