A nicer version of adequacy of Iris and specialize it to heap_lang.

Use it to prove that tests/barrier_client and tests/heap_lang are adequate.

_CoqProject

@@ -101,6 +101,7 @@ heap_lang/lib/barrier/specification.v
 heap_lang/lib/barrier/protocol.v
 heap_lang/lib/barrier/proof.v
 heap_lang/proofmode.v
+heap_lang/adequacy.v
 tests/heap_lang.v
 tests/one_shot.v
 tests/joining_existentials.v

heap_lang/heap.v

@@ -18,8 +18,6 @@ Class heapG Σ := HeapG {
   heap_name : gname
 }.
 (** The Functor we need. *)
-Definition heapGF : gFunctor := authGF heapUR.
-
 Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
 Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd).
 
@@ -101,24 +99,6 @@ Section heap.
   Qed.
   Hint Resolve heap_store_valid.
 
-  (** Allocation *)
-  Lemma heap_alloc `{irisG heap_lang Σ, authG Σ heapUR} E σ :
-    ownP σ ={E}=> ∃ _ : heapG Σ, heap_ctx ∧ [★ map] l↦v ∈ σ, l ↦ v.
-  Proof.
-    intros. rewrite -{1}(from_to_heap σ). etrans.
-    { rewrite [ownP _]later_intro.
-      apply (auth_alloc (ownP ∘ of_heap) heapN E); auto using to_heap_valid. }
-    apply pvs_mono, exist_elim=> γ.
-    rewrite -(exist_intro (HeapG _ _ _ γ)) /heap_ctx; apply and_mono_r.
-    rewrite heap_mapsto_eq /heap_mapsto_def /heap_name.
-    induction σ as [|l v σ Hl IH] using map_ind.
-    { rewrite big_sepM_empty; apply True_intro. }
-    rewrite to_heap_insert big_sepM_insert //.
-    rewrite (insert_singleton_op (to_heap σ));
-      last by rewrite lookup_fmap Hl; auto.
-    by rewrite auth_own_op IH.
-  Qed.
-
   Context `{heapG Σ}.
 
   (** General properties of mapsto *)

program_logic/adequacy.v

@@ -4,6 +4,29 @@ From iris.program_logic Require Import ownership.
 From iris.proofmode Require Import tactics weakestpre.
 Import uPred.
 
+Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
+  adequate_result t2 σ2 v2 :
+   rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
+  adequate_safe t2 σ2 e2 :
+   rtc step ([e1], σ1) (t2, σ2) →
+   e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
+}.
+
+Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
+  adequate e1 σ1 φ →
+  rtc step ([e1], σ1) (t2, σ2) →
+  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
+Proof.
+  intros Had ?.
+  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
+  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
+  destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&ef&?)];
+    rewrite ?eq_None_not_Some; auto.
+  { exfalso. eauto. }
+  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
+  right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
+Qed.
+
 Section adequacy.
 Context `{irisG Λ Σ}.
 Implicit Types e : expr Λ.
@@ -102,41 +125,19 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem adequacy_result `{irisPreG Λ Σ} e v2 t2 σ1 σ2 φ :
-  (∀ `{irisG Λ Σ}, ownP σ1 ⊢ WP e {{ v, ■ φ v }}) →
-  rtc step ([e], σ1) (of_val v2 :: t2, σ2) →
-  φ v2.
+Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ :
+  (∀ `{irisG Λ Σ}, ownP σ ⊢ WP e {{ v, ■ φ v }}) →
+  adequate e σ φ.
 Proof.
-  intros Hwp [n ?]%rtc_nsteps.
-  eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-  rewrite Nat_iter_S. iVs (iris_alloc σ1) as (?) "(?&?&?&Hσ)".
-  iVsIntro. iNext. iApply wptp_result; eauto.
-  iFrame. iSplitL. by iApply Hwp. done.
-Qed.
-
-Lemma wp_adequacy_reducible `{irisPreG Λ Σ} e1 e2 t2 σ1 σ2 Φ :
-  (∀ `{irisG Λ Σ}, ownP σ1 ⊢ WP e1 {{ Φ }}) →
-  rtc step ([e1], σ1) (t2, σ2) →
-  e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2).
-Proof.
-  intros Hwp [n ?]%rtc_nsteps ?.
-  eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
-  rewrite Nat_iter_S. iVs (iris_alloc σ1) as (?) "(Hw & HE & Hσ & Hσf)".
-  iVsIntro. iNext. iApply wptp_safe; eauto.
-  iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. done.
-Qed.
-
-Theorem wp_adequacy_safe `{irisPreG Λ Σ} e1 t2 σ1 σ2 Φ :
-  (∀ `{irisG Λ Σ}, ownP σ1 ⊢ WP e1 {{ Φ }}) →
-  rtc step ([e1], σ1) (t2, σ2) →
-  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
-Proof.
-  intros.
-  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
-  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (wp_adequacy_reducible e1 e2 t2 σ1 σ2 Φ) as [?|(e3&σ3&ef&?)];
-    rewrite ?eq_None_not_Some; auto.
-  { exfalso. eauto. }
-  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
-  right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
+  intros Hwp; split.
+  - intros t2 σ2 v2 [n ?]%rtc_nsteps.
+    eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+    rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(?&?&?&Hσ)".
+    iVsIntro. iNext. iApply wptp_result; eauto.
+    iFrame. iSplitL; auto. by iApply Hwp.
+  - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
+    eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+    rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
+    iVsIntro. iNext. iApply wptp_safe; eauto.
+    iFrame "Hw HE Hσ". iSplitL; auto. by iApply Hwp.
 Qed.

program_logic/global_functor.v

@@ -64,7 +64,7 @@ Module gFunctors.
   Definition nil : gFunctors := existT 0 (fin_0_inv _).
 
   Definition cons (F : gFunctor) (Σ : gFunctors) : gFunctors :=
-   existT (S (projT1 Σ)) (fin_S_inv _ F (projT2 Σ)).
+    existT (S (projT1 Σ)) (fin_S_inv _ F (projT2 Σ)).
 
   Fixpoint app (Fs : gFunctorList) (Σ : gFunctors) : gFunctors :=
     match Fs with

program_logic/iris.v

@@ -17,13 +17,13 @@ Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
   disabled_name : gname;
 }.
 
-Definition irisPreGF (Λ : language) : gFunctorList :=
+Definition irisGF (Λ : language) : gFunctorList :=
   [GFunctor (constRF (authUR (optionUR (exclR (stateC Λ)))));
    GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
    GFunctor (constRF coPset_disjUR);
    GFunctor (constRF (gset_disjUR positive))].
 
-Instance inGF_barrierG `{H : inGFs Σ (irisPreGF Λ)} : irisPreG Λ Σ.
+Instance inGF_barrierG `{H : inGFs Σ (irisGF Λ)} : irisPreG Λ Σ.
 Proof.
   by destruct H as (?%inGF_inG & ?%inGF_inG & ?%inGF_inG & ?%inGF_inG & _).
 Qed.

tests/barrier_client.v

@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.program_logic Require Import auth sts saved_prop hoare ownership.
-From iris.heap_lang Require Import proofmode.
+From iris.heap_lang Require Import adequacy proofmode.
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
@@ -57,18 +57,10 @@ Section client.
 Qed.
 End client.
 
-(*
-Section ClosedProofs.
-  Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
-  Notation iProp := (iPropG heap_lang Σ).
-
-  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
-  Proof.
-    iIntros "! Hσ".
-    iVs (heap_alloc with "Hσ") as (h) "[#Hh _]"; first done.
-    iApply (client_safe (nroot .@ "barrier")); auto with ndisj.
-  Qed.
+Lemma client_adequate σ : adequate client σ (λ _, True).
+Proof.
+  apply (heap_adequacy #[ heapGF ; barrierGF ; spawnGF ])=> ?.
+  apply (client_safe (nroot .@ "barrier")); auto with ndisj.
+Qed.
 
-  Print Assumptions client_safe_closed.
-End ClosedProofs.
-*)
\ No newline at end of file
+Print Assumptions client_adequate.

tests/heap_lang.v

 (** This file is essentially a bunch of testcases. *)
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
-From iris.program_logic Require Import ownership hoare.
+From iris.heap_lang Require Import adequacy.
+From iris.program_logic Require Import ownership.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LangTests.
@@ -75,15 +76,5 @@ Section LiftingTests.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
-(*
-Section ClosedProofs.
-  Definition Σ : gFunctors := #[ irisPreGF; heapGF ].
-
-  Lemma heap_e_closed σ : {{ ownP σ : iProp Σ }} heap_e {{ v, v = #2 }}.
-  Proof.
-    iProof. iIntros "! Hσ".
-    iVs (heap_alloc with "Hσ") as (h) "[? _]"; first solve_ndisj.
-    by iApply heap_e_spec; first solve_ndisj.
-  Qed.
-End ClosedProofs.
-*)
\ No newline at end of file
+Lemma heap_e_adequate σ : adequate heap_e σ (λ v, v = #2).
+Proof. eapply (heap_adequacy #[ heapGF ])=> ?. by apply heap_e_spec. Qed.