Spec blocks

[Aurel300]

• don't emit unused variable binds in the pure encoding
  • This might not emit some function calls into the AST, which may then not trigger some quantifiers; however, this should only happen if the call's result wasn't used at all.
  • Skipping binds is still imprecise when going across phi nodes (so any branching), so we have more binds than strictly necessary.
  • there are regressions in the test suite due to this change
• change MIR pure encoder interface
  • ExprInput is now a hashmap of locals -> expressions; it must contain the keys indicated by MirPureEncOutput::inputs.
• support prusti_assert!, prusti_assume!, prusti_refute! (closes prusti_assert! support #173)
• support body_invariant!
  • support nesting in loop guards (see test_pathological_nesting in v2/pass/invariants.rs, as well as the failing case verify/pass/loop-invs/nested-loops-3.rs)
    • the source seems to be that the PCG loop analysis identifies some blocks of the inner loop as not belonging to the outer loop
  • forbid multiple invariants in distinct locations (see test_multiple_invariants_wrong)
  • figure out where exactly to emit the invariant annotation wrt. statements (see test_invariant_following_local_decl)