Disallows impure non-ghost calls in ghost code

[ArquintL]

This PR depends on PR #747 and should thus only be reviewed & merged afterwards.

This PR checks that ghost code does not contain calls to non-ghost impure functions. Note that calling non-ghost pure functions is fine due to the absence of side effects. To support implementation proofs, this PR makes interface & closure implementation proofs non-ghost. Technically, we would need to distinguish between implementation proofs for a ghost or non-ghost member but due to the syntax restrictions for implementation proofs, we do not have to make this distinction (e.g., assignments are disallowed).

Fixes #420