Simpler syncer specs

This simplifies the syncer specs. The sequential syncer only is slightly improved, by changing

  Definition synced R (f' f: val) :=
    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
                       ({{ P x }} f' x {{ v, Q x v }}))%I.

such that P, Q don't factor in a dependency on x any more. Since all three are quantified at the same time, the two specs are equivalent -- and the one where P is not a predicate and Q is exactly the postcondition is arguably simpler:

  Definition synced R (f f': val) :=
    (□ ∀ P Q (x: val), ({{ R ★ P }} f x {{ v, R ★ Q v }}) →
                       ({{ P }} f' x {{ Q }}))%I.

For the atomic spec, the changes are deeper. The currying on some location l is entirely removed. is_atomic_syncer better mirrors is_syncer from the sequential version. And finally, we use "original" atomic triples and not some modified version thereof (so atomic_triple_base is killed).

TODO: Fix atomic_pcas.v, it relied on the location currying done by atomic_sync.v. However, I don't entirely grok that file. @zhangz could you give that a look?

Notice that there still is a subtle difference between is_syncer and is_atomic_syncer: The former quantifies over x once, and lifts the spec for x "pointwise". The latter demands that the sequential spec holds for all x before proving the atomic spec for all x. That's strictly weaker, and I think there is no reason to make it weaker like that. We could then probably even remove the dependency of \alpha, \beta on x as they would all be quantified at the same place.

I'll look into that tomorrow.

Because the post-condition Q in goal WP f' x {{ v, ∃ x0 : A, Q x0 v }} in goal doesn't look like the assumption we have from syncer spec:

  ​"Hsynced" : ∀ (P0 : uPred (iResUR Σ))
               (Q0 : language.val heap_lang → uPred (iResUR Σ)) 
               (x0 : val),
               {{ (∃ g : A, ϕ g ★ gHalf γ g) ★ P0 }} 
               f x0 {{ v, (∃ g : A, ϕ g ★ gHalf γ g) ★ Q0 v }}
               → {{ P0 }} f' x0 {{ v, Q0 v }}

?

But it looks like if we drop the x argument of Q as @robbertkrebbers proposed in the mail, this should be more elegant

Well, but the assumption Hsynced has a generalized post-condition that should match any postcondition.

Indeed simplifying the atomic triple did not help.

@robbertkrebbers could you have a look at the iApply-related TODO in atomic_sync.v? Looks to me as if iApply transparently stripping boxes doesn't work here, or maybe sth. else is going on.

Regarding atomic_pcas.v, I will certainly take care of that :) However this week I am stuck in SPLASH-conf at Amsterdam, so feel free to temporarily break it (or remove it from the _CoqProject.

All right, I will just comment out atomic_pcas then.

Added 3 commits:

• 129cd4e8 - 1 commit from branch master
• 087a2abd - Simplify sequential syncer; use Texan triples
• 958942c3 - Improve atomic_syncer

Compare with previous version

Added 1 commit:

• 531ed2a1 - simplify atomic triples as suggested by Robbert

Compare with previous version

Unmarked this merge request as a Work In Progress

All right, as far as I am concerned, this is ready to be merged.

Added 4 commits:

• 6396d121 - 1 commit from branch master
• 79caa21f - Simplify sequential syncer; use Texan triples
• c0647f6a - Improve atomic_syncer
• 908a83a4 - simplify atomic triples as suggested by Robbert

Compare with previous version

I will take 5 days without complaint as "okay to merge" ;) just so that I can proceed with enabling CI for this repository.

Mentioned in commit 8d5768cb

Status changed to merged