New Iris weakest precondition, based on the typical Iris WP

This merge request includes a new weakest precondition using the standard (non evaluation-context based) language instantiation for Iris.

The new WP is an "exception-handling" Hoare triple, which considers two cases for its postcondition, each for the return and exception continuation cases. We use the notation

      WP (try m f h)
         {{ | RET x => ϕ x ;
            | EXN x => ψ x }}

to indicate that the expression may return a value and satisfy postcondition ϕ, or throw an exception and satisfy postcondition ψ.

See the directory theories/program_logic for the language instantiation (wp.v) and the corresponding Hoare rules (rules.v).

All properties proved in the "old" WP has been reproved in this setting, including any Qed'ed examples. (I've stored some "non-Qed'ed" examples in the attic for now, since I assumed that they will likely become deprecated)

I am planning to look further into the adequacy statement that is derived from Iris and how it compares to the prior adequacy statement for the custom WP that had been defined on Osiris.