heap_lang/tests: provide a closed Hoare proof

barrier/barrier.v

@@ -100,7 +100,7 @@ Section proof.
 
   Local Hint Immediate i_states_closed low_states_closed.
 
-  Notation iProp := (iPropG heap_lang Σ).
+  Local Notation iProp := (iPropG heap_lang Σ).
 
   Definition waiting (P : iProp) (I : gset gname) : iProp :=
     (∃ R : gname → iProp, ▷(P -★ Π★{set I} (λ i, R i)) ★

heap_lang/tests.v

 (** This file is essentially a bunch of testcases. *)
-From program_logic Require Import ownership.
+From program_logic Require Import ownership hoare auth.
 From heap_lang Require Import wp_tactics heap notation.
 Import uPred.
 
@@ -23,19 +23,21 @@ End LangTests.
 
 Section LiftingTests.
   Context `{heapG Σ}.
-  Implicit Types P : iPropG heap_lang Σ.
-  Implicit Types Q : val → iPropG heap_lang Σ.
+  Local Notation iProp := (iPropG heap_lang Σ).
 
-  Definition e  : expr :=
+  Implicit Types P : iProp.
+  Implicit Types Q : val → iProp.
+
+  Definition heap_e  : expr :=
     let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
-  Goal ∀ N, heap_ctx N ⊑ wp N e (λ v, v = '2).
+  Lemma heap_e_spec E N : nclose N ⊆ E → heap_ctx N ⊑ wp E heap_e (λ v, v = '2).
   Proof.
-    move=> N. rewrite /e.
+    rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
     wp> eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
     wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
     wp_bin_op. wp> eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
     wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
-    by apply const_intro.
+      by apply const_intro.
   Qed.
 
   Definition FindPred : val :=
@@ -71,9 +73,33 @@ Section LiftingTests.
     - ewp apply FindPred_spec. auto with I omega.
   Qed.
 
-  Goal ∀ E,
+  Lemma Pred_user E :
     True ⊑ wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
   Proof.
     intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
   Qed.
 End LiftingTests.
+
+Section ClosedProofs.
+  
+  Definition Σ : iFunctorG := λ _, authF (constF heapRA).
+
+  Local Instance : inG heap_lang Σ (authRA heapRA).
+  Proof. by exists 1%nat. Qed.
+
+  (* TODO: Why do I even have to explicitly do this? *)
+  Local Instance : authG heap_lang Σ heapRA.
+  Proof. split; by apply _. Qed.
+  
+  Local Notation iProp := (iPropG heap_lang Σ).
+
+  Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e @ ⊤ {{ λ v, v = '2 }}.
+  Proof.
+    apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
+    apply wp_strip_pvs, exist_elim=>?. rewrite and_elim_l.
+    rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
+  Qed.
+
+  Print Assumptions heap_e_hoare.
+    
+End ClosedProofs.  

program_logic/hoare.v

@@ -29,12 +29,16 @@ Global Instance ht_mono' E :
   Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
 
-Lemma ht_val E v :
-  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
+Lemma ht_alt E P Q e : (P ⊑ wp E e Q) → {{ P }} e @ E {{ Q }}.
 Proof.
-  apply (always_intro _ _), impl_intro_l.
-  by rewrite -wp_value'; apply const_intro.
+  intros; rewrite -{1}always_const. apply (always_intro _ _), impl_intro_l.
+  by rewrite always_const right_id.
 Qed.
+
+Lemma ht_val E v :
+  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
+Proof. apply ht_alt. by rewrite -wp_value'; apply const_intro. Qed.
+
 Lemma ht_vs E P P' Q Q' e :
   ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Q' }} ∧ ∀ v, Q' v ={E}=> Q v)
   ⊑ {{ P }} e @ E {{ Q }}.
@@ -45,6 +49,7 @@ Proof.
   rewrite -(pvs_wp E e Q) -(wp_pvs E e Q); apply pvs_mono, wp_mono=> v.
   by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
 Qed.
+
 Lemma ht_atomic E1 E2 P P' Q Q' e :
   E2 ⊆ E1 → atomic e →
   ((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Q' }} ∧ ∀ v, Q' v ={E2,E1}=> Q v)
@@ -56,6 +61,7 @@ Proof.
   rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
   by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
 Qed.
+
 Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
   ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} K (of_val v) @ E {{ Q' }})
   ⊑ {{ P }} K e @ E {{ Q' }}.
@@ -65,9 +71,11 @@ Proof.
   rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
   by rewrite (forall_elim v) /ht always_elim impl_elim_r.
 Qed.
+
 Lemma ht_mask_weaken E1 E2 P Q e :
   E1 ⊆ E2 → {{ P }} e @ E1 {{ Q }} ⊑ {{ P }} e @ E2 {{ Q }}.
 Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
+
 Lemma ht_frame_l E P Q R e :
   {{ P }} e @ E {{ Q }} ⊑ {{ R ★ P }} e @ E {{ λ v, R ★ Q v }}.
 Proof.
@@ -75,9 +83,11 @@ Proof.
   rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
   by rewrite wp_frame_l.
 Qed.
+
 Lemma ht_frame_r E P Q R e :
   {{ P }} e @ E {{ Q }} ⊑ {{ P ★ R }} e @ E {{ λ v, Q v ★ R }}.
 Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
+
 Lemma ht_frame_later_l E P R e Q :
   to_val e = None →
   {{ P }} e @ E {{ Q }} ⊑ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Q v }}.
@@ -86,6 +96,7 @@ Proof.
   rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
   by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
 Qed.
+
 Lemma ht_frame_later_r E P R e Q :
   to_val e = None →
   {{ P }} e @ E {{ Q }} ⊑ {{ P ★ ▷ R }} e @ E {{ λ v, Q v ★ R }}.
@@ -93,4 +104,5 @@ Proof.
   rewrite (comm _ _ (▷ R)%I); setoid_rewrite (comm _ _ R).
   apply ht_frame_later_l.
 Qed.
+
 End hoare.

program_logic/namespaces.v

@@ -2,14 +2,14 @@ From prelude Require Export countable co_pset.
 From algebra Require Export base.
 
 Definition namespace := list positive.
-Definition nnil : namespace := nil.
+Definition nroot : namespace := nil.
 Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
 Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
 Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
-Lemma nclose_nnil : nclose nnil = ⊤.
+Lemma nclose_nroot : nclose nroot = ⊤.
 Proof. by apply (sig_eq_pi _). Qed.
 Lemma encode_nclose N : encode N ∈ nclose N.
 Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.