support strongest-postcondition reasoning

[lsf37]

We currently have _sp rules for a number of the basic monad constructs, and we're using them manually in some situations, e.g. to avoid case blow-up in wp reasoning or when chaining trivial steps in corres proofs.

We should:

• consistently support at least all of the basic nondet monad constructs with _sp rules -- I think they do have to be manually stated, but their proofs should all follow automatically from the corresponding wp rule
• have a basic sp tactic, analogous to wp, but not as sophisticated. For a first version, I would propose a simple Eisbach method that repeatedly applies an sp set, and potentially automatically does an sp_pre (analogously to wp_pre).
• find (most of) the existing manual _sp proofs and replace these to make sure the automation works and is convenient enough to use

I don't think we need a full-blown wp equivalent for sp, because we do not want to switch over to general sp reasoning or use more of it than necessary (to avoid duplicating rules for kernel functions). This issue only proposes to make those instances where it would be beneficial to use more ergonomic to use and easier to read/review.

MCS seems to have a higher use count of sp rules, so we should make sure to test the method there.

[lsf37]

There is also a question about which other monads to support (e.g. error and/or reader monad), but so far most of the instances I've seen are on the plain nondet monad, so I'd vote for starting small and doing that one properly first.