Fine-grained post-conditions for forked-off threads

This commit extends the state interpretation with an additional parameter to talk about the post-conditions of forked-off threads so that one can keep precise account of resources (e.g. to ensure the absence of memory leaks). The state interpretation will be as follows:

state_interp : Λstate → list Λobservation → list (iProp Σ) → iProp Σ;

This way, instead of having True as the post-condition of Fork, one can have any post-condition, which is then recorded in the state interpretation. The point of keeping track of the postconditions of forked-off threads, is that we get an (additional) stronger adequacy theorem:

Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
  (∀ `{Hinv : invG Σ} κs,
     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → list (iProp Σ) → iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
       stateI σ1 κs [] ∗ WP e @ s; ⊤ {{ v, ∀ Qs,
         ⌜ length vs = length Qs ⌝ -∗
         stateI σ2 [] Qs -∗
         [∗] Qs ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
  rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
  φ v.

The difference with the ordinary adequacy theorem is that this one only applies once all threads terminated. In this case, one gets back the post-conditions Qs of all forked-off threads.

In Iron we showed that we can use this mechanism to make sure that all resources are disposed of properly in the presence of fork-based concurrency. See https://robbertkrebbers.nl/research/articles/iron.pdf for a draft of the paper (to appear at POPL!)

Note that this MR is not specific to Iron in any way. Iron expects the post-conditions of threads to be of a very specific form (𝖊 π), while this MR abstracts over that. It leaves this choice to the state interpretation. Iron thus obtains its concrete mode of use by instantiating the state interpretation in a specific way.

Some questions:

• This MR introduces even more lifting lemmas. To reduce this a bit, we could turn wp_lift_step_fupd into wp_lift_step, and get rid of the old one (i.e. with one with ={∅,E}=∗ instead of ={∅,∅,E}▷=∗).
• This MR introduced the predicate state_interp_fork_indep, which basically says that the state interpretation ignores the post-conditions of forked-off threads. Some of the lifting lemmas have state_interp_fork_indep as a premise. Should we turn state_interp_fork_indep into a class? Note that for all practical purposes, this condition is solved by a mere reflexivity.