Simplify sequential syncer; use Texan triples

requires a new Iris version

IRIS_VERSION

-05a588df59ddfdc2e7a4aec5a98a50614c819693
+6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838

atomic_incr.v

@@ -46,7 +46,7 @@ Section incr.
       iSpecialize ("Hvs'" $! #x').
       wp_cas_suc.
       iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iModIntro. wp_if. iModIntro. by iExists x'.
+      iModIntro. wp_if. by iExists x'.
     - iDestruct "Hvs'" as "[Hvs' _]".
       wp_cas_fail.
       iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.

atomic_pcas.v

@@ -35,11 +35,11 @@ Section atomic_pair.
   
   Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β ⊤.
   Proof.
-    iIntros (_ l) "!# _". wp_seq. iModIntro. iPureIntro.
+    iIntros (_ l) "!# _". wp_seq. iPureIntro.
     iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
     iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
     iDestruct "Hα" as (a b) "%".
-    subst. simpl. wp_let. wp_proj. wp_load. wp_proj.
+    subst. simpl. iApply wp_fupd. wp_let. wp_proj. wp_load. wp_proj.
     wp_op=>[?|Hx1na].
     - subst.
       wp_if. wp_proj. wp_load. wp_proj.

atomic_sync.v

@@ -57,10 +57,9 @@ Section atomic_sync.
     iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
     { by rewrite pair_op dec_agree_idemp. }
     repeat wp_let. wp_bind (mk_syncer _).
-    iApply (Hsync (∃ g: A, ϕ l g ★ gHalf γ g)%I)=>//. iFrame "Hh".
-    iSplitL "Hg1 Hϕ".
+    iApply (Hsync (∃ g: A, ϕ l g ★ gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
     { iExists g0. by iFrame. }
-    iIntros (s) "#Hsyncer".
+    iNext. iIntros (s) "#Hsyncer".
     wp_let. wp_bind (f_seq _). iApply wp_wand_r.
     iSplitR; first iApply Hseq=>//; auto.
     iIntros (f) "%".
@@ -70,7 +69,7 @@ Section atomic_sync.
     iExists γ. iFrame.
     iIntros (x). iAlways.
     iIntros (P Q) "#Hvss".
-    iSpecialize ("Hsynced" $! P Q x).
+    iSpecialize ("Hsynced" $! (P x) (Q x) x).
     iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".

flat.v

@@ -130,9 +130,9 @@ Section proof.
       by iApply "HΦ".
   Qed.
 
-  Definition installed_recp (ts: toks) (x: val) (Q: val → val → iProp Σ) :=
+  Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
     let '(γx, _, γ3, _, γq) := ts in
-    (own γ3 (Excl ()) ★ own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq (Q x))%I.
+    (own γ3 (Excl ()) ★ own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq Q)%I.
 
   Lemma install_spec
         R P Q
@@ -140,7 +140,7 @@ Section proof.
         (Φ: val → iProp Σ):
     heapN ⊥ N →
     heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★
-    P x ★ ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) ★
+    P ★ ({{ R ★ P }} f x {{ v, R ★ Q v }}) ★
     (∀ (p: loc) (ts: toks), installed_recp ts x Q -★ evm γm p ts -★(∃ hd, evs γs hd #p) -★ Φ #p)
     ⊢ WP install f x #s {{ Φ }}.
   Proof.
@@ -151,7 +151,7 @@ Section proof.
     iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
     iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
     iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
-    iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
+    iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) Q) as (γq) "#?".
     iInv N as "[Hrs >Hm]" "Hclose".
     iDestruct "Hm" as (m) "[Hm HRm]".
     destruct (m !! p) eqn:Heqn.
@@ -170,8 +170,10 @@ Section proof.
         iApply install_push_spec=>//.
         iFrame "#". rewrite /evm /installed_s. iFrame.
         iSplitL "Hpx Hf".
-        { iExists P, Q. by iFrame. }
-        iIntros "Hhd". wp_seq. iModIntro.
+        { (* TODO: Something somewhere can be simplified so that we don't have
+             to add these dummy arguments any more. *)
+          iExists (fun _ => P), (fun _ => Q). by iFrame. }
+        iIntros "Hhd". wp_seq. 
         iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
         { rewrite /installed_recp. iFrame. iFrame "#". }
         by iApply ("HΦ" with "[]").
@@ -206,7 +208,7 @@ Section proof.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
           iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
-        iModIntro. wp_match. iModIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
+        iModIntro. wp_match. iApply ("HΦ'" with "[Hor HR]"). iFrame.
       + iDestruct "Hp" as (f' x') "(Hp & Hs)".
         wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
         iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
@@ -227,7 +229,7 @@ Section proof.
         wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
         { iApply "Hf'". iFrame. }
         iIntros (v) "[HR HQ]".
-        wp_value. iModIntro. iInv N as "[Hs >Hm]" "Hclose".
+        wp_value. iInv N as "[Hs >Hm]" "Hclose".
         iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
         iDestruct "HRs" as (m') "[>Hom HRs]".
         iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
@@ -304,8 +306,8 @@ Section proof.
   Proof.
     iIntros (?) "(#? & #? & #? & HΦ)".
     wp_seq. wp_let.
-    wp_bind (try_acquire _). iApply try_acquire_spec.
-    iFrame "#". iNext. iIntros ([]); last by (iIntros; wp_if).
+    wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
+    iNext. iIntros ([]); last by (iIntros; wp_if).
     (* acquired the lock *)
     iIntros "[Hlocked [Ho2 HR]]".
     wp_if. wp_bind (! _)%E.
@@ -320,8 +322,8 @@ Section proof.
     { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ★ R ★ v = #()))%I=>//.      
       iFrame "#". iFrame. iIntros "? ?". by iFrame. }
     iIntros (f') "[Ho [HR %]]". subst.
-    wp_let. iApply release_spec. iFrame "#".
-    iFrame. iNext. iIntros. done.
+    wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#★".
+    iNext. iIntros. done.
   Qed.
 
   Lemma loop_spec R (p s: loc) (lk: val)
@@ -390,20 +392,20 @@ Section proof.
 
   Lemma mk_flat_spec: mk_syncer_spec N mk_flat.
   Proof.
-    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
+    iIntros (R HN Φ) "(#Hh & HR) HΦ".
     iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
     iMod (own_alloc (● (∅: tokmR) ⋅ ◯ ∅)) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
     iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
     { iExists ∅. iFrame. by rewrite big_sepM_empty. }
     wp_seq. wp_bind (newlock _).
-    iApply (newlock_spec _ (own γr (Excl ()) ★ R))%I=>//.
-    iFrame "Hh Ho2 HR". iNext. iIntros (lk γlk) "#Hlk".
+    iApply (newlock_spec _ (own γr (Excl ()) ★ R)%I with "[$Hh $Ho2 $HR]")=>//.
+    iNext. iIntros (lk γlk) "#Hlk".
     wp_let. wp_bind (new_stack _).
     iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
     iFrame "Hh Hm". iIntros (γ s) "#Hss".
-    wp_let. iModIntro. iApply "HΦ". rewrite /synced.
+    wp_let. iApply "HΦ". rewrite /synced.
     iAlways.
-    iIntros (f). wp_let. iModIntro. iAlways.
+    iIntros (f). wp_let. iAlways.
     iIntros (P Q x) "#Hf".
     iIntros "!# Hp". wp_let.
     wp_bind (install _ _ _).

peritem.v

@@ -92,7 +92,7 @@ Lemma new_stack_spec' Φ RI:
     heap_ctx ★ RI ★ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ★ RI) -★ Φ #s)
     ⊢ WP new_stack #() {{ Φ }}.
   Proof.
-    iIntros (HN) "(#Hh & HR & HΦ)".
+    iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd.
     iMod (own_alloc (● (∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
     { apply auth_valid_discrete_2. done. }
     wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
@@ -115,10 +115,10 @@ Lemma new_stack_spec' Φ RI:
     induction xs as [|x xs' IHxs'].
     - simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
       iDestruct "Hxs1" as (q) "Hhd".
-      wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
+      wp_rec. wp_value. wp_let. wp_load. wp_match. by iApply "HΦ".
     - simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
       iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
-      wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. wp_proj.
+      wp_rec. wp_value. wp_let. wp_load. wp_match. wp_proj.
       wp_bind (f' _). iApply Hf=>//. iFrame "#".
       iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
       wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.

simple_sync.v

@@ -23,20 +23,19 @@ Section syncer.
   
   Lemma mk_sync_spec: mk_syncer_spec N mk_sync.
   Proof.
-    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
+    iIntros (R HN Φ) "(#Hh & HR) HΦ".
     wp_seq. wp_bind (newlock _).
-    iApply newlock_spec; first done.
-    iSplitL "HR"; first by iFrame. iNext.
+    iApply (newlock_spec _ R with "[$Hh $HR]"); first done. iNext.
     iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
-    iIntros (f). wp_let. iModIntro. iAlways.
+    iIntros (f). wp_let. iAlways.
     iIntros (P Q x) "#Hf !# HP".
     wp_let. wp_bind (acquire _).
-    iApply acquire_spec. iSplit; first done. iNext.
+    iApply (acquire_spec with "Hl"). iNext.
     iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
-    iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
-    iApply wp_wand_r.  iSplitL "Hf'"; first done.
+    iSpecialize ("Hf" with "[R HP]"); first by iFrame.
+    iApply wp_wand_r.  iSplitL "Hf"; first done.
     iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
-    iApply release_spec. iFrame "HR Hl Hlocked".
+    iApply (release_spec with "[$HR $Hl $Hlocked]").
     iNext. iIntros "_". by wp_seq.
   Qed.
 End syncer.

sync.v

@@ -7,15 +7,22 @@ From iris.heap_lang Require Import proofmode notation.
 Section sync.
   Context `{!heapG Σ} (N : namespace).
 
-  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.
+  (* TODO: We could get rid of the x, and hard-code a unit. That would
+     be no loss in expressiveness, but probably more annoying to apply.
+     How much more annoying? And how much to we gain in terms of things
+     becomign easier to prove? *)
+  Definition synced R (f f': val) :=
+    (□ ∀ P Q (x: val), {{ R ★ P }} f x {{ v, R ★ Q v }} →
+                       {{ P }} f' x {{ Q }})%I.
 
+  (* Notice that `s f` is *unconditionally safe* to execute, and only 
+     when executing the returned f' we have to provide a spec for f.
+     This is crucial. *)
+  (* TODO: Use our usual style with a generic post-condition. *)
   Definition is_syncer (R: iProp Σ) (s: val) :=
-    (□ ∀ (f : val), WP s f {{ f', synced R f' f }})%I.
+    (□ ∀ (f : val), WP s f {{ f', synced R f f' }})%I.
 
   Definition mk_syncer_spec (mk_syncer: val) :=
-    ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
-      heapN ⊥ N →
-      heap_ctx ★ R ★ (∀ s, is_syncer R s -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
+    ∀ (R: iProp Σ), heapN ⊥ N →
+      {{{ heap_ctx ★ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
 End sync.

treiber.v

@@ -133,7 +133,7 @@ Section proof.
     * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
       iMod ("Hvs'" $! #() with "[-]") as "HQ".
       { iExists l. iSplitR; first done. by iFrame. }
-      iModIntro. wp_if. iModIntro. eauto.
+      iModIntro. wp_if. eauto.
     * wp_cas_fail.
       iDestruct "Hvs'" as "[Hvs' _]".
       iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
@@ -167,7 +167,7 @@ Section proof.
       iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
       { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
       iModIntro. wp_let. wp_load. wp_match.
-      iModIntro. eauto.
+      eauto.
     - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
       iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
       wp_load. iDestruct "Hvs'" as "[Hvs' _]".