Thanks @jtassaro.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

This commit extends the state interpretation with an additional parameter to
talk about the number of forked-off threads, and a fixed postcondition for each
forked-off thread:

    state_interp : Λstate → list Λobservation → nat → iProp Σ;
    fork_post : 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 Λ) → nat → iProp Σ)
             (fork_post : iProp Σ),
           let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
           stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
             let m := length vs in
             stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ 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
`[∗] replicate m fork_post` 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.

Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.

Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.

Marianna Rapoport authored 6 years ago and Ralf Jung committed 6 years ago

- Removing head of list of observations after each reduction step in definition of wp
- Adding support for observations to state_interp and world
- Applying Ralf's suggestions to previous commit (e.g. replacing /\ and -> with unicode characters)

Use telescopes for atomic accessors, updates and triples; improve mask handling; add notation for all of them

make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn