Lifting lemmas.

iris/lifting.v

+Require Export iris.hoare.
+Require Import iris.wsat.
+Local Hint Extern 10 (_ ≤ _) => omega.
+Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
+Local Hint Extern 10 (✓{_} _) =>
+  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
+  solve_validN.
+
+Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
+  (default True%I ef (λ e, ht E P e Q))
+  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : uPred_scope.
+Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
+  (True ⊑ default True ef (λ e, ht E P e Q))
+  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.
+
+Section lifting.
+Context {Σ : iParam}.
+Implicit Types v : ival Σ.
+Implicit Types e : iexpr Σ.
+Implicit Types σ : istate Σ.
+
+Lemma wp_lift_step E1 E2
+    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
+  E1 ⊆ E2 → to_val e1 = None →
+  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★
+    pvs E1 E2 (wp E2 e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True))))
+  ⊑ wp E2 e1 Q.
+Proof.
+  intros ? He Hsafe Hstep r n ? Hvs; constructor; auto.
+  intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
+    as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
+  destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
+  { by apply ownP_spec; auto. }
+  { by rewrite (associative _). }
+  constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
+  destruct (λ H1 H2 H3, Hwp e2 σ2 ef (update_pst σ2 r1) k H1 H2 H3 rf k Ef σ2)
+    as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
+  { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
+  { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
+  by exists r1', r2'; split_ands; [| |by intros ? ->].
+Qed.
+Lemma wp_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) Q e1 :
+  to_val e1 = None →
+  (∀ σ1, ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
+  (▷ ∀ e2 ef, ■ φ e2 ef →
+    wp E e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True)))
+  ⊑ wp E e1 Q.
+Proof.
+  intros He Hsafe Hstep r [|n] ?; [done|]; intros Hwp; constructor; auto.
+  intros rf k Ef σ1 ???; split; [done|].
+  intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
+  destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto; [by destruct k|].
+  exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
+Qed.
+End lifting.

iris/ownership.v

@@ -63,6 +63,11 @@ Proof.
       (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
   * intros ?; split_ands; try apply cmra_empty_least; eauto.
 Qed.
+Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ={n}= Excl σ.
+Proof.
+  intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
+  naive_solver (apply cmra_empty_least).
+Qed.
 Lemma ownG_spec r n m : (ownG m) n r ↔ m ≼{n} gst r.
 Proof.
   rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_least).

iris/wsat.v

 Require Export iris.model prelude.co_pset.
+Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
 Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
@@ -21,6 +22,7 @@ Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
 Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : res' Σ) : Prop :=
   match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end.
 Instance: Params (@wsat) 4.
+Arguments wsat : simpl never.
 
 Section wsat.
 Context {Σ : iParam}.
@@ -38,7 +40,25 @@ Global Instance wsat_ne n : Proper (dist n ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
 Global Instance wsat_proper n : Proper ((≡) ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
-Lemma wsat_valid n E σ (r : res' Σ) : wsat n E σ r → ✓{n} r.
+Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
+Proof.
+  destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
+  intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto.
+  intros i P ? HiP; destruct (wld (r ⋅ big_opM rs) !! i) as [P'|] eqn:HP';
+    [apply (injective Some) in HiP|inversion_clear HiP].
+  assert (P' ={S n}= to_agree $ Later $ iProp_unfold $
+                       iProp_fold $ later_car $ P' (S n)) as HPiso.
+  { rewrite iProp_unfold_fold later_eta to_agree_car //.
+    apply (map_lookup_validN _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. }
+  assert (P ={n'}= iProp_fold (later_car (P' (S n)))) as HPP'.
+  { apply (injective iProp_unfold), (injective Later), (injective to_agree).
+    by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
+  destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto.
+  { by rewrite HP' -HPiso. }
+  assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
+  exists r'; split; [done|apply HPP', uPred_weaken with r' n; auto].
+Qed.
+Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r.
 Proof.
   destruct n; [intros; apply cmra_valid_0|intros [rs ?]].
   eapply cmra_valid_op_l, wsat_pre_valid; eauto.
@@ -78,13 +98,19 @@ Proof.
     + intros. destruct (Hwld j P') as (r'&?&?); auto.
       exists r'; rewrite lookup_insert_ne; naive_solver.
 Qed.
-Lemma wsat_update_pst n E σ1 σ2 r :
-  pst r ={S n}= Excl σ1 → wsat (S n) E σ1 r → wsat (S n) E σ2 (update_pst σ2 r).
+Lemma wsat_update_pst n E σ1 σ1' r rf :
+  pst r ={S n}= Excl σ1 → wsat (S n) E σ1' (r ⋅ rf) →
+  σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf).
 Proof.
-  intros Hr [rs [(?&Hpst&?) Hσ HE Hwld]]; simpl in *.
-  assert (pst (big_opM rs) = ∅) as Hpst_rs.
-  { by apply: (excl_validN_inv_l n σ1); rewrite -Hr. }
-  by exists rs; constructor; split_ands'; rewrite /= ?Hpst_rs.
+  intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
+  assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
+  { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r (associative _). }
+  assert (σ1' = σ1) as ->.
+  { apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
+    apply (injective Excl).
+    by rewrite -Hpst_r -Hpst -(associative _) Hpst' (right_id _). }
+  split; [done|exists rs].
+  by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
 Qed.
 Lemma wsat_update_gst n E σ r rf m1 (P : icmra' Σ → Prop) :
   m1 ≼{S n} gst r → m1 ⇝: P →