Change wp to have a view shift in the value case.

program_logic/adequacy.v

@@ -55,21 +55,19 @@ Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
   nsteps step k ([e1],σ1) (t2,σ2) →
   1 < n → wsat (k + n) coPset_all σ1 r1 →
   P (k + n) r1 →
-  ∃ rs2 Qs', wptp n t2 ((λ v, pvs coPset_all coPset_all (Q v)) :: Qs') rs2 ∧
-             wsat n coPset_all σ2 (big_op rs2).
+  ∃ rs2 Qs', wptp n t2 (Q :: Qs') rs2 ∧ wsat n coPset_all σ2 (big_op rs2).
 Proof.
-  intros Hht ????; apply (nsteps_wptp [pvs coPset_all coPset_all ∘ Q] k n
-    ([e1],σ1) (t2,σ2) [r1]); rewrite /big_op ?right_id; auto.
+  intros Hht ????; apply (nsteps_wptp [Q] k n ([e1],σ1) (t2,σ2) [r1]);
+    rewrite /big_op ?right_id; auto.
   constructor; last constructor.
   apply Hht with r1 (k + n); eauto using cmra_included_unit.
-  by destruct (k + n).
+  eapply uPred.const_intro; eauto.
 Qed.
 Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
   ✓m →
   {{ ownP σ1 ★ ownG m }} e1 @ coPset_all {{ Q }} →
   rtc step ([e1],σ1) (t2,σ2) →
-  ∃ rs2 Qs', wptp 3 t2 ((λ v, pvs coPset_all coPset_all (Q v)) :: Qs') rs2 ∧
-             wsat 3 coPset_all σ2 (big_op rs2).
+  ∃ rs2 Qs', wptp 3 t2 (Q :: Qs') rs2 ∧ wsat 3 coPset_all σ2 (big_op rs2).
 Proof.
   intros Hv ? [k ?]%rtc_nsteps.
   eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
@@ -103,7 +101,7 @@ Proof.
   destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto.
   { by rewrite -(ht_mask_weaken E coPset_all). }
   destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 3 r) t2
-    (pvs coPset_all coPset_all ∘ Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
+    (Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
   destruct (wp_step_inv coPset_all ∅ Q' e2 2 3 σ2 r2 (big_op (delete i rs2)));
     rewrite ?right_id_L ?big_op_delete; auto.
 Qed.

program_logic/hoare.v

 Require Export program_logic.weakestpre program_logic.viewshifts.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
-    (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ :=
-  (□ (P → wp E e (λ v, pvs E E (Q v))))%I.
+    (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ := (□ (P → wp E e Q))%I.
 Instance: Params (@ht) 3.
 
 Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
@@ -25,16 +24,16 @@ Global Instance ht_proper E :
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Lemma ht_mono E P P' Q Q' e :
   P ⊑ P' → (∀ v, Q' v ⊑ Q v) → {{ P' }} e @ E {{ Q' }} ⊑ {{ P }} e @ E {{ Q }}.
-Proof. by intros HP HQ; rewrite /ht -HP; setoid_rewrite HQ. Qed.
+Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
 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') }}.
+  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
 Proof.
   apply (always_intro' _ _), impl_intro_l.
-  by rewrite -wp_value -pvs_intro; apply const_intro.
+  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)
@@ -42,9 +41,9 @@ Lemma ht_vs E P P' Q Q' e :
 Proof.
   apply (always_intro' _ _), impl_intro_l.
   rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
-  rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
-  rewrite wp_pvs; apply wp_mono=> v.
-  by rewrite (forall_elim v) pvs_impl_r !pvs_trans'.
+  rewrite associative pvs_impl_r pvs_always_r wp_always_r.
+  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 →
@@ -55,7 +54,7 @@ Proof.
   rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
   rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
   rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
-  rewrite (forall_elim v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
+  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' }})
@@ -64,21 +63,17 @@ Proof.
   intros; apply (always_intro' _ _), impl_intro_l.
   rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
   rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
-  rewrite (forall_elim v) pvs_impl_r wp_pvs; apply wp_mono=> v'.
-  by rewrite pvs_trans'.
+  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; apply always_mono, impl_intro_l; rewrite impl_elim_r.
-  by rewrite -(wp_mask_weaken E1) //; apply wp_mono=> v; apply pvs_mask_weaken.
-Qed.
+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.
   apply always_intro, impl_intro_l.
   rewrite always_and_sep_r -(associative _) (sep_and P) always_elim impl_elim_r.
-  by rewrite wp_frame_l; apply wp_mono=>v; rewrite pvs_frame_l.
+  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 }}.

program_logic/hoare_lifting.v

@@ -68,7 +68,7 @@ Proof.
     by repeat apply and_intro; try apply const_intro.
   * apply (always_intro' _ _), impl_intro_l; rewrite and_elim_l.
     rewrite -always_and_sep_r'; apply const_elim_r=>-[[v Hv] ?].
-    rewrite -(of_to_val e2 v) // -wp_value -pvs_intro.
+    rewrite -(of_to_val e2 v) // -wp_value.
     rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
     by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
 Qed.

program_logic/invariants.v

@@ -110,9 +110,6 @@ Proof.
 Qed.
 
 Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
-Proof.
-  rewrite /inv (pvs_allocI N); first done.
-  apply coPset_suffixes_infinite.
-Qed.
+Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
 
 End inv.

program_logic/lifting.v

@@ -74,7 +74,7 @@ Proof.
   apply const_elim_l=>-[v2' [Hv ?]] /=.
   rewrite -pvs_intro.
   rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
-  by rewrite left_id wand_elim_r -(wp_value' _ _ e2').
+  by rewrite left_id wand_elim_r -(wp_value' _ _ e2' v2').
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :

program_logic/weakestpre.v

@@ -3,6 +3,7 @@ Require Import program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
+Local Hint Extern 100 (@subseteq coPset _ _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
@@ -19,7 +20,7 @@ Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ →
 }.
 CoInductive wp_pre {Λ Σ} (E : coPset)
      (Q : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop :=
-  | wp_pre_value n r v : Q v n r → wp_pre E Q (of_val v) n r
+  | wp_pre_value n r v : pvs E E (Q v) n r → wp_pre E Q (of_val v) n r
   | wp_pre_step n r1 e1 :
      to_val e1 = None →
      (∀ rf k Ef σ1,
@@ -62,33 +63,45 @@ Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Transparent uPred_holds.
 
-Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
-  E1 ⊆ E2 → (∀ v r n', n' ≤ n → ✓{n'} r → Q1 v n' r → Q2 v n' r) →
-  n' ≤ n → ✓{n'} r → wp E1 e Q1 n' r → wp E2 e Q2 n' r.
+Global Instance wp_ne E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
 Proof.
-  intros HE HQ; revert e r; induction n' as [n' IH] using lt_wf_ind; intros e r.
-  destruct 3 as [|n' r e1 ? Hgo]; constructor; eauto.
-  intros rf k Ef σ1 ???.
-  assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
-  { by rewrite associative_L -union_difference_L. }
-  destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
+  cut (∀ Q1 Q2, (∀ v, Q1 v ={n}= Q2 v) →
+    ∀ r n', n' ≤ n → ✓{n'} r → wp E e Q1 n' r → wp E e Q2 n' r).
+  { by intros help Q Q' HQ; split; apply help. }
+  intros Q1 Q2 HQ r n'; revert e r.
+  induction n' as [n' IH] using lt_wf_ind=> e r.
+  destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
+  { constructor. by eapply pvs_ne, HpvsQ; eauto. }
+  constructor; [done|]=> rf k Ef σ1 ???.
+  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
+  exists r2, r2'; split_ands; [|eapply IH|]; eauto.
 Qed.
-Global Instance wp_ne E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
-Proof. by intros Q Q' HQ; split; apply wp_weaken with n; try apply HQ. Qed.
 Global Instance wp_proper E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
 Proof.
   by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
+Lemma wp_mask_frame_mono E1 E2 e Q1 Q2 :
+  E1 ⊆ E2 → (∀ v, Q1 v ⊑ Q2 v) → wp E1 e Q1 ⊑ wp E2 e Q2.
+Proof.
+  intros HE HQ r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
+  destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
+  { constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
+  constructor; [done|]=> rf k Ef σ1 ???.
+  assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
+  { by rewrite associative_L -union_difference_L. }
+  destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
+  split; [done|intros e2 σ2 ef ?].
+  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
+  exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
+Qed.
 
-Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r → Q v n r.
+Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r → pvs E E (Q v) n r.
 Proof.
-  inversion 1 as [|??? He]; simplify_equality; auto.
-  by rewrite ?to_of_val in He.
+  by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_equality.
 Qed.
 Lemma wp_step_inv E Ef Q e k n σ r rf :
   to_val e = None → 1 < k < n → E ∩ Ef = ∅ →
@@ -97,22 +110,27 @@ Lemma wp_step_inv E Ef Q e k n σ r rf :
 Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
 
 Lemma wp_value E Q v : Q v ⊑ wp E (of_val v) Q.
-Proof. by constructor. Qed.
-Lemma wp_mono E e Q1 Q2 : (∀ v, Q1 v ⊑ Q2 v) → wp E e Q1 ⊑ wp E e Q2.
-Proof. by intros HQ r n ?; apply wp_weaken with n; intros; try apply HQ. Qed.
-Lemma wp_pvs E e Q : pvs E E (wp E e Q) ⊑ wp E e (λ v, pvs E E (Q v)).
+Proof. by constructor; apply pvs_intro. Qed.
+Lemma pvs_wp E e Q : pvs E E (wp E e Q) ⊑ wp E e Q.
 Proof.
   intros r [|n] ?; [done|]; intros Hvs.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
-  { by constructor; eapply pvs_mono, Hvs; [intros ???; apply wp_value_inv|]. }
-  constructor; [done|intros rf k Ef σ1 ???].
+  { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
+    intros ???; apply wp_value_inv. }
+  constructor; [done|]=> rf k Ef σ1 ???.
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
-  inversion Hwp as [|???? Hgo]; subst; [by rewrite to_of_val in He|].
-  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
+  eapply wp_step_inv with (S k) r'; eauto.
+Qed.
+Lemma wp_pvs E e Q : wp E e (λ v, pvs E E (Q v)) ⊑ wp E e Q.
+Proof.
+  intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HQ.
+  destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
+  { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Q)); auto. }
+  constructor; [done|]=> rf k Ef σ1 ???.
+  destruct (wp_step_inv E Ef (pvs E E ∘ Q) e k n σ1 r rf) as [? Hstep]; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
-  exists r2, r2'; split_ands; auto.
-  eapply wp_mono, Hwp'; auto using pvs_intro.
+  exists r2, r2'; split_ands; [|apply (IH k)|]; auto.
 Qed.
 Lemma wp_atomic E1 E2 e Q :
   E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Q v))) ⊑ wp E1 e Q.
@@ -120,24 +138,27 @@ Proof.
   intros ? He r n ? Hvs; constructor; eauto using atomic_not_val.
   intros rf k Ef σ1 ???.
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
-  inversion Hwp as [|???? Hgo]; subst; [by destruct (atomic_of_val v)|].
-  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; clear Hgo; auto.
-  split; [done|intros e2 σ2 ef ?].
+  destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Q) e k (S k) σ1 r' rf)
+    as [Hsafe Hstep]; auto using atomic_not_val.
+  split; [done|]=> e2 σ2 ef ?.
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
   destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
     [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
+  apply pvs_trans in Hvs'; auto.
   destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?(associative _); auto.
-  by exists r3, r2'; split_ands; [rewrite -(associative _)|constructor|].
+  exists r3, r2'; split_ands; last done.
+  * by rewrite -(associative _).
+  * constructor; apply pvs_intro; auto.
 Qed.
-Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q.
-Proof. by intros HE r n ?; apply wp_weaken with n. Qed.
 Lemma wp_frame_r E e Q R : (wp E e Q ★ R) ⊑ wp E e (λ v, Q v ★ R).
 Proof.
   intros r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
   rewrite Hr; clear Hr; revert e r Hwp.
   induction n as [n IH] using lt_wf_ind; intros e r1.
-  destruct 1 as [|n r e ? Hgo]; constructor; [exists r, rR; eauto|auto|].
-  intros rf k Ef σ1 ???; destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep]; auto.
+  destruct 1 as [|n r e ? Hgo]=>?.
+  { constructor; apply pvs_frame_r; auto. exists r, rR; eauto. }
+  constructor; [done|]=> rf k Ef σ1 ???.
+  destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep]; auto.
   { by rewrite (associative _). }
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
@@ -164,9 +185,10 @@ Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Q :
   wp E e (λ v, wp E (K (of_val v)) Q) ⊑ wp E (K e) Q.
 Proof.
-  intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?.
-  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using fill_not_val.
-  intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
+  intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
+  destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
+  constructor; auto using fill_not_val=> rf k Ef σ1 ???.
+  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split.
   { destruct Hsafe as (e2&σ2&ef&?).
     by exists (K e2), σ2, ef; apply fill_step. }
@@ -179,6 +201,8 @@ Qed.
 (* Derived rules *)
 Opaque uPred_holds.
 Import uPred.
+Lemma wp_mono E e Q1 Q2 : (∀ v, Q1 v ⊑ Q2 v) → wp E e Q1 ⊑ wp E e Q2.
+Proof. by apply wp_mask_frame_mono. Qed.
 Global Instance wp_mono' E e :
   Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
@@ -186,13 +210,6 @@ Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
 Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
-Lemma wp_mask_frame_mono E E' e (P Q : val Λ → iProp Λ Σ) :
-  E' ⊆ E →
-  (∀ v, P v ⊑ Q v) → wp E' e P ⊑ wp E e Q.
-Proof.
-  intros HE HPQ. rewrite wp_mask_weaken; last eexact HE.
-  by apply wp_mono.
-Qed.
 Lemma wp_frame_later_l E e Q R :
   to_val e = None → (▷ R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
 Proof.
@@ -207,7 +224,7 @@ Lemma wp_always_r E e Q R `{!AlwaysStable R} :
 Proof. by setoid_rewrite (always_and_sep_r' _ _); rewrite wp_frame_r. Qed.
 Lemma wp_impl_l E e Q1 Q2 : ((□ ∀ v, Q1 v → Q2 v) ∧ wp E e Q1) ⊑ wp E e Q2.
 Proof.
-  rewrite wp_always_l; apply wp_mono=> v.
+  rewrite wp_always_l; apply wp_mono=> // v.
   by rewrite always_elim (forall_elim v) impl_elim_l.
 Qed.
 Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2.