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.
• 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!
  • there are regressions in the test suite due to this change
• support body_invariant!