avoid using Hoare triples

theories/barrier/example_joining_existentials.v

-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
 From iris.heap_lang Require Import notation par proofmode.
@@ -34,12 +34,12 @@ Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ :=
   (∃ x, own γ (Shot x) ∗ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) :
-  recv N l (barrier_res γ Φ) -∗ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) -∗
+  recv N l (barrier_res γ Φ) -∗ (∀ x, Φ x -∗ WP e {{ _, Ψ x }}) -∗
   WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
-  iIntros "Hl #He". wp_apply (wait_spec with "[- $Hl]"); simpl.
+  iIntros "Hl He". wp_apply (wait_spec with "Hl"); simpl.
   iDestruct 1 as (x) "[#Hγ Hx]".
-  wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
+  wp_seq. iApply (wp_wand with "[Hx He]"); [by iApply "He"|].
   iIntros (v) "?"; iExists x; by iSplit.
 Qed.
 
@@ -71,19 +71,18 @@ Proof.
 Qed.
 
 Lemma client_spec_new (fM fW1 fW2 : val) :
-  P -∗
-  {{ P }} fM #() {{ _, ∃ x, Φ x }} -∗
-  (∀ x, {{ Φ1 x }} fW1 #() {{ _, Ψ1 x }}) -∗
-  (∀ x, {{ Φ2 x }} fW2 #() {{ _, Ψ2 x }}) -∗
+  WP fM #() {{ _, ∃ x, Φ x }} -∗
+  □ (∀ x, Φ1 x -∗ WP fW1 #() {{ _, Ψ1 x }}) -∗
+  □ (∀ x, Φ2 x -∗ WP fW2 #() {{ _, Ψ2 x }}) -∗
   WP client fM fW1 fW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof using All.
-  iIntros "/= HP #Hf #Hf1 #Hf2"; rewrite /client.
+  iIntros "/= Hf #Hf1 #Hf2"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
   wp_lam. wp_pures. wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
   iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ∗ barrier_res γ Ψ2)%I).
-  wp_smart_apply (par_spec  (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
-  - wp_lam. wp_bind (fM #()). iApply (wp_wand with "[HP]"); [by iApply "Hf"|].
+  wp_smart_apply (par_spec  (λ _, True)%I workers_post with "[Hf Hs Hγ] [Hr]").
+  - wp_lam. wp_bind (fM #()). iApply (wp_wand with "Hf").
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_seq.
     iMod (own_update with "Hγ") as "Hx".
     { by apply (cmra_update_exclusive (Shot x)). }

theories/barrier/specification.v

-From iris.program_logic Require Export hoare.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode.
 From iris_examples.barrier Require Export barrier.
 From iris_examples.barrier Require Import proof.
@@ -11,19 +11,18 @@ Context `{!heapG Σ, !barrierG Σ}.
 
 Lemma barrier_spec (N : namespace) :
   ∃ recv send : loc → iPropO Σ -n> iPropO Σ,
-    (∀ P, ⊢ {{ True }} newbarrier #()
-                     {{ v, ∃ l : loc, ⌜v = #l⌝ ∗ recv l P ∗ send l P }}) ∧
-    (∀ l P, ⊢ {{ send l P ∗ P }} signal #l {{ _, True }}) ∧
-    (∀ l P, ⊢ {{ recv l P }} wait #l {{ _, P }}) ∧
+    (∀ P, ⊢ {{{ True }}} newbarrier #()
+                     {{{ (l : loc), RET #l; recv l P ∗ send l P }}}) ∧
+    (∀ l P, ⊢ {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}) ∧
+    (∀ l P, ⊢ {{{ recv l P }}} wait #l {{{ RET #(); P }}}) ∧
     (∀ l P Q, recv l (P ∗ Q) ={↑N}=∗ recv l P ∗ recv l Q) ∧
     (∀ l P Q, (P -∗ Q) -∗ recv l P -∗ recv l Q).
 Proof.
   exists (λ l, OfeMor (recv N l)), (λ l, OfeMor (send N l)).
   split_and?; simpl.
-  - iIntros (P) "!# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
-    iNext. eauto.
-  - iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
-  - iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
+  - iIntros (P) "!#". iIntros (Φ). iApply (newbarrier_spec _ P).
+  - iIntros (l P) "!#". iIntros (Φ). iApply signal_spec.
+  - iIntros (l P) "!#". iIntros (Φ). iApply wait_spec.
   - iIntros (l P Q). by iApply recv_split.
   - apply recv_weaken.
 Qed.

theories/concurrent_stacks/concurrent_stack3.v

-From iris.program_logic Require Export weakestpre hoare.
+From iris.base_logic Require Import invariants.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris_examples.concurrent_stacks Require Import specs.
 Set Default Proof Using "Type".

theories/concurrent_stacks/concurrent_stack4.v

-From iris.program_logic Require Export weakestpre hoare.
+From iris.base_logic Require Import invariants.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import excl.
 From iris_examples.concurrent_stacks Require Import specs.

theories/lecture_notes/modular_incr.v

 (* Modular Specifications for Concurrent Modules. *)
 
-From iris.program_logic Require Export hoare weakestpre.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import agree frac frac_auth.
@@ -134,7 +134,7 @@ Section cnt_spec.
 
   Theorem read_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z → iProp Σ) (ℓ : loc):
     ↑(N .@ "internal") ⊆ E →
-    (∀ m, (γ ⤇½ m ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ m ∗ Q m)) ⊢
+    (∀ m, □ (γ ⤇½ m ∗ P ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇½ m ∗ Q m)) ⊢
     {{{ Cnt ℓ γ ∗ P}}} read #ℓ @ E {{{ (m : Z), RET #m; Cnt ℓ γ ∗ Q m }}}.
   Proof.
     iIntros (Hsubset) "#HVS".
@@ -154,7 +154,7 @@ Section cnt_spec.
 
   Theorem incr_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z → iProp Σ) (ℓ : loc):
     ↑(N .@ "internal") ⊆ E →
-    (∀ (n : Z), γ ⤇½ n ∗ P  ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q n) ⊢
+    (∀ (n : Z), □ (γ ⤇½ n ∗ P  ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗ Q n)) ⊢
     {{{ Cnt ℓ γ ∗ P }}} incr #ℓ @ E {{{ (m : Z), RET #m; Cnt ℓ γ ∗ Q m}}}.
   Proof.
     iIntros (Hsubset) "#HVS".
@@ -189,7 +189,7 @@ Section cnt_spec.
 
   Theorem wk_incr_spec (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
     ↑(N .@ "internal") ⊆ E →
-    (γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q) -∗
+    □ (γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗ Q) -∗
     {{{ Cnt ℓ γ ∗ γ ⤇[q] n ∗ P}}} wk_incr #ℓ @ E {{{ RET #(); Cnt ℓ γ ∗ Q}}}.
   Proof.
     iIntros (Hsubset) "#HVS".
@@ -216,7 +216,7 @@ Section cnt_spec.
 
   Theorem wk_incr_spec' (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
     ↑(N .@ "internal") ⊆ E →
-    (γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗  γ ⤇[q] (n + 1) ∗ Q) -∗
+    □ (γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗  γ ⤇[q] (n + 1) ∗ Q) -∗
     {{{ Cnt ℓ γ ∗ γ ⤇[q] n ∗ P}}} wk_incr #ℓ @ E {{{ RET #(); Cnt ℓ γ ∗  γ ⤇[q] (n + 1) ∗ Q}}}.
   Proof.
     iIntros (Hsubset) "#HVS".
@@ -232,9 +232,9 @@ Section incr_twice.
 
   Theorem incr_twice_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q Q' : Z → iProp Σ) (ℓ : loc):
     ↑(N .@ "internal") ⊆ E →
-    (∀ (n : Z), (γ ⤇½ n ∗ P  ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q n))
+    (∀ (n : Z), □ (γ ⤇½ n ∗ P  ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗ Q n))
       -∗
-      (∀ (n : Z), γ ⤇½ n ∗ (∃ m, Q m)  ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q' n)
+      (∀ (n : Z), □ (γ ⤇½ n ∗ (∃ m, Q m)  ={E ∖ ↑(N .@ "internal")}=∗ γ ⤇½ (n+1) ∗ Q' n))
       -∗
       {{{ Cnt N ℓ γ ∗ P }}} incr_twice #ℓ @ E {{{ (m : Z), RET #m; Cnt N ℓ γ ∗ Q' m}}}.
   Proof.
@@ -284,7 +284,6 @@ Section example_1.
     { iIntros (v1 v2) "_ !>".
       wp_seq.
       wp_apply (read_spec _ _ _ True%I (λ _, True%I)); auto.
-      iIntros (n) "!# [Hown _] !>"; by iFrame.
     }
   Qed.
 End example_1.

theories/logatom/flat_combiner/atomic_sync.v

-From iris.program_logic Require Export weakestpre hoare atomic.
+From iris.program_logic Require Export weakestpre atomic.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import agree frac.
@@ -23,7 +23,7 @@ Section atomic_sync.
   Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, to_agree g).
 
   Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) :=
-    (∀ g, {{ ϕ g ∗ α g }} f x {{ v, ∃ g', ϕ g' ∗ β g g' v }})%I.
+    (∀ g, □ ( ϕ g ∗ α g -∗ WP f x {{ v, ∃ g', ϕ g' ∗ β g g' v }}))%I.
 
   (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
   Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) :=

theories/logatom/flat_combiner/simple_sync.v

 (* Coarse-grained syncer *)
 
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import frac.

theories/logatom/flat_combiner/sync.v

 (* Syncer spec *)
 
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 
@@ -12,8 +12,8 @@ Section sync.
      How much more annoying? And how much to we gain in terms of things
      becoming 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.
+    (□ ∀ P Q (x: val), □ (R ∗ P -∗ WP f x {{ v, R ∗ Q v }}) →
+                       □ (P -∗ WP 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.