Bump opam; update to new bi interface (removing admits); developing ATimeless infrastructure.

_CoqProject

@@ -41,7 +41,6 @@ theories/program_logic/pstepshifts.v
 theories/program_logic/lifting.v
 theories/program_logic/invariants.v
 theories/program_logic/viewshifts.v
-theories/program_logic/stepshifts.v
 theories/program_logic/wsat.v
 theories/program_logic/ownership.v
 theories/program_logic/weakestpre.v

opam

@@ -7,5 +7,5 @@ remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fri" ]
 depends: [
   "coq" { >= "8.7" }
   "coq-stdpp" { (>= "1.1.0") | (>= "dev") }
-  "coq-iris"  { (= "branch.gen_proofmode.2018-02-19.0") } 
+  "coq-iris"  { (= "branch.gen_proofmode.2018-02-26.0") }
 ]

theories/algebra/upred.v

@@ -1553,6 +1553,13 @@ Proof.
   intros ((?&Heq1)&Heq2). rewrite /uPred_holds//=. rewrite -Heq2 Heq1. done. 
 Qed.
 
+Lemma unlimited_affine_persistent P: ⧈P ⊣⊢ uPred_affine (uPred_persistent P).
+Proof.
+  unseal; split; intros n x y ??; split.
+  - intros ((?&Heq1)&Heq2). rewrite /uPred_holds//=. rewrite -Heq2 Heq1. done. 
+  - intros (HP&Heq1). rewrite /uPred_holds//= Heq1.
+    rewrite /core/core'//= ucmra_pcore_unit //=.
+Qed.
 
 Global Instance relevant_if_ne n p : Proper (dist n ==> dist n) (@uPred_relevant_if M p).
 Proof. intros ?? ?. destruct p => //=. rewrite H. reflexivity. Qed.

theories/algebra/upred_bi.v

@@ -28,21 +28,35 @@ Proof.
   - intros; by rewrite assoc.
   - intros; by apply wand_intro_r.
   - intros; by apply wand_elim_l'.
-  - admit. (* plainly to be deleted from the interface *) 
-    (* intros P QR HP. unseal; split=> n x y ?? ? //=; by apply HP; eauto using ucmra_unit_validN. *)
-  - admit.
-  - admit. 
-  - admit.
-  - admit. 
-  - admit. 
-  - admit. 
-  - admit. 
+  - unseal. intros P Q HPQ; split => n x y ?? HP //=. apply HPQ => //=.
+    * apply ucmra_unit_validN.
+    * apply ucmra_unit_validN.
+  - unseal. intros P. split => n x y ?? => //=. rewrite /uPred_holds //=.
+    intros HP. eapply uPred_mono; eauto.
+    exists (core x). rewrite left_id. reflexivity.
+  - unseal. split => n x y ?? => //=.
+  - unseal. split => n x y ?? => //=.
+  - unseal. split => n x y ?? => //=.
+    do 2 rewrite /uPred_holds //=.
+    intros HPQ n' x' ???? HP. eapply uPred_mono; first eapply HPQ; eauto.
+    * eapply cmra_validN_le; eauto. 
+    * eapply cmra_validN_le; eauto. 
+    * apply cmra_included_includedN; auto.
+  - unseal. split => n x y ?? => //=.
+    do 2 rewrite /uPred_holds //=.
+    intros HPQ n' x' ???? HP. eapply uPred_mono; first eapply HPQ; eauto.
+    * eapply cmra_validN_le; eauto. 
+    * eapply cmra_validN_le; eauto. 
+    * apply cmra_included_includedN; auto.
+  - unseal. split => n x y ?? => //= HP.
+    repeat rewrite /uPred_holds //=.
+  - unseal. split => n x y ?? => //=. intros (x1&x2&y1&y2&Heqx&Heqy&HP&HQ).
+    apply HP.
   - intros P Q.
     unseal=> HPQ.
     split=> n x y ?? ?.
     auto. apply HPQ; simpl; auto using @cmra_core_validN, @ucmra_unit_validN.
   - intros P. by apply persistent_intro'.
-  - admit.
   - intros.
     unseal; split=>n x y ??. 
     simpl; try naive_solver.
@@ -60,15 +74,14 @@ Proof.
     exists (core x), x, (∅: M), y; split_and!.
     * by rewrite cmra_core_l.
     * by rewrite left_id.
-    * split => //=; eauto.
-      rewrite /uPred_holds//=.
+    * move: HP. rewrite /uPred_holds//=.
     * done.
-Admitted. 
+Qed.
 
 Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin (ofe_mixin_of (uPred M))
   uPred_entails uPred_pure uPred_and uPred_or uPred_impl
                 (@uPred_forall M) (@uPred_exist M) 
-                uPred_sep uPred_plainly uPred_persistent (@uPred_eq M)
+                uPred_sep uPred_wand uPred_plainly uPred_persistent (@uPred_eq M)
                 uPred_later.
 Proof.
   split; try apply _; eauto with I.
@@ -79,7 +92,13 @@ Proof.
   - by unseal.
   - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝ *)
     intros A a b ?. unseal; split=> n x y ??; by apply (discrete_iff n).
-  - admit.
+  - unseal; split => n x y ?? [HPQ HQP].
+    rewrite /uPred_holds//= in HPQ HQP.
+    split => n' x' y' Hle1 Hvalidx Hvalidy; split.
+    * intros. specialize (HPQ n' x' y' Hle1). rewrite ?left_id in HPQ * => HPQ.
+      apply HPQ; eauto.
+    * intros. specialize (HQP n' x' y' Hle1). rewrite ?left_id in HQP * => HQP.
+      apply HQP; eauto.
   - by unseal. 
   - by unseal. 
   - apply later_mono.
@@ -91,8 +110,8 @@ Proof.
     * destruct Hsat as (a&?). right. by exists a.
   - intros; by rewrite later_sep.
   - intros; by rewrite later_sep.
-  - admit. 
-  - admit. 
+  - by unseal. 
+  - by unseal. 
   - by unseal.
   - by unseal.
   - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
@@ -103,7 +122,7 @@ Proof.
     * omega. 
     * eapply cmra_validN_le; eauto.
     * by apply cmra_included_includedN.
-Admitted.
+Qed.
 
 Canonical Structure uPredI (M : ucmraT) : bi :=
   {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
@@ -218,4 +237,158 @@ Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
   unfold_bi. rewrite -unlimited_persistent.
   rewrite relevant_affine relevant_ownMl affine_affine0 //=.
-Qed.
\ No newline at end of file
+Qed.
+
+Class ATimeless {PROP: sbi} (P: PROP)
+  := atimeless : ⧆▷ P ⊢ ◇ ⧆ P.
+Arguments ATimeless {_} _%I.
+Arguments atimeless {_} _%I {_}.
+
+Section ATimeless_sbi.
+  Context {PROP: sbi}.
+  Implicit Types P Q : PROP. 
+
+  Lemma timeless_atimeless P: Timeless P → ATimeless P.
+  Proof.
+    rewrite /Timeless /ATimeless. intros ->. apply bi.except_0_affinely_2.
+  Qed.
+  Import bi.
+
+  Global Instance and_atimeless P Q: ATimeless P → ATimeless Q → ATimeless (P ∧ Q).
+  Proof.
+    intros; rewrite /ATimeless affinely_and except_0_and later_and !affinely_and.
+    auto with *.
+  Qed.
+  Global Instance or_atimeless P Q : ATimeless P → ATimeless Q → ATimeless (P ∨ Q).
+  Proof.
+    intros; rewrite /ATimeless affinely_or except_0_or later_or affinely_or; auto with *.
+  Qed.
+
+  (*
+Global Instance impl_atimeless P Q : ATimeless Q → ATimeless (P → Q).
+Proof.
+  rewrite /ATimeless=> HQ. rewrite later_false_em.
+  rewrite affinely_or.
+  apply or_mono.
+  { rewrite affinely_elim.  done. }
+  apply affinely_mono, impl_intro_l.
+  rewrite -{2}(löb Q); apply impl_intro_l.
+  rewrite HQ /sbi_except_0. !and_or_r. apply or_elim; last auto.
+  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
+  rewrite !atimelessP_spec; unseal=> HP [|n] x ? HPQ  [|n'] x' ?????; auto.
+  apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le.
+Qed.
+*)
+  Global Instance sep_atimeless P Q: Timeless P → Timeless Q → ATimeless (P ∗ Q).
+  Proof.
+    intros; rewrite /ATimeless. apply timeless_atimeless; apply _. 
+  Qed.
+  Global Instance affinely_atimeless P :
+    ATimeless P → ATimeless (bi_affinely P).
+  Proof.
+    intros HP; rewrite /ATimeless.
+    rewrite {1}(affinely_elim P).
+    rewrite atimeless. apply except_0_mono.
+      by rewrite affine_affinely.
+  Qed.
+End ATimeless_sbi.
+
+Section ATimeless_uPred.
+  Import bi.
+  Context (M: ucmraT).
+  Implicit Types P Q : uPred M.
+
+  Lemma atimeless_spec P : ATimeless P ↔ ∀ n x, ✓{n} x → P 0 x ∅ → P n x ∅.
+  Proof.
+    split.
+    - intros HP n x ??; induction n as [|n]; auto.
+      move: HP; rewrite /ATimeless/sbi_except_0; unseal=> /uPred_in_entails /(_ (S n) x ∅).
+      unseal => //=.
+      destruct 1 as [ HlP | HlF]; auto using cmra_validN_S, ucmra_unit_validN.
+      * split; rewrite /uPred_holds => //=. 
+          by apply IHn, cmra_validN_S.
+      * destruct HlP. 
+      * destruct HlF as [? ?]; auto. 
+    - move=> HP; rewrite /ATimeless/sbi_except_0; unseal.
+      split=> -[|n] x y /=; auto; unseal; intros ?? (Haff&HP').
+      * left. split; auto.
+      * right. split; auto. rewrite Haff.
+        apply HP, uPred_closed with n; eauto using cmra_validN_le, ucmra_unit_validN.
+        ** rewrite -(dist_le _ _ _ _ Haff); auto with *.
+        ** omega.
+        ** eapply cmra_validN_le; eauto; omega.
+  Qed.
+
+  Global Instance forall_atimeless {A} (Ψ : A → uPred M) :
+    (∀ x, ATimeless (Ψ x)) → ATimeless (∀ x, Ψ x).
+  Proof. by setoid_rewrite atimeless_spec; unseal=> HΨ n x ?? a; apply HΨ. Qed.
+  Global Instance exist_atimeless {A} (Ψ : A → uPred M) :
+    (∀ x, ATimeless (Ψ x)) → ATimeless (∃ x, Ψ x).
+  Proof.
+      by setoid_rewrite atimeless_spec;
+        unseal=> HΨ [|n] x ?; [|intros [a ?]; exists a; apply HΨ].
+  Qed.
+  Lemma except_0_relevant P:  uPred_relevant (sbi_except_0 P) ⊢ sbi_except_0 (uPred_relevant P).
+  Proof.
+    rewrite /sbi_except_0. unfold_bi.
+    rewrite relevant_or.
+    rewrite relevant_later_1. apply or_mono; auto. apply later_mono => //=.
+      by rewrite relevant_elim.
+  Qed.
+  Global Instance persistently_atimeless P : ATimeless P → ATimeless (□ P).
+  Proof.
+    rewrite /ATimeless.
+    rewrite -?uPred_affine_bi_affinely.
+    unfold_bi. rewrite -unlimited_affine_persistent.
+    rewrite -relevant_affine affine_relevant_later.
+    rewrite -relevant_affine. rewrite {2}(affine_elim P) => ->.
+    rewrite except_0_relevant. apply except_0_mono. rewrite relevant_affine.
+      by rewrite affine_affine0.
+  Qed.
+
+  Global Instance eq_atimeless {A : ofeT} (a b : A) :
+    Discrete a → ATimeless (a ≡ b : uPred M)%IP.
+  Proof. intros. apply timeless_atimeless; apply _. Qed.
+  Global Instance ownM_atimeless (a : M) : Discrete a → ATimeless (uPred_ownM a).
+  Proof. intros. apply timeless_atimeless; apply _. Qed.
+
+(*
+Global Instance sep_atimeless_2 P Q: 
+  Affine P → Affine Q → ATimeless P → ATimeless Q → ATimeless (P ★ Q).
+Proof.
+  intros; rewrite /ATimeless.
+  rewrite affine_affinely.
+  rewrite except_0_sep.
+  rewrite -(affine_affinely P).
+  rewrite -(affine_affinely Q).
+  rewrite later_sep.
+  rewrite later_sep.
+  rewrite (atimeless P) (atimelessP Q).
+  rewrite sep_or_l. rewrite sep_or_r.
+  apply or_elim.
+  - apply or_elim.
+    * apply or_intro_l'. apply sep_affine_1.
+    * apply or_intro_r'. apply sep_elim_l.
+  - apply or_intro_r'. rewrite sep_or_r.
+    apply or_elim; first apply sep_elim_r.
+    unseal. split=> -[|n] x y ?? Hfalse /=; auto.
+    destruct Hfalse as (?&?&?&?&?&?&?&?). auto.
+Qed.
+Global Instance wand_atimeless P Q : AffineP P → ATimeless Q → ATimeless (P -★ Q).
+Proof.
+  rewrite !atimelessP_spec. 
+  unseal=> HA HP [|n] x ? HPQ [|n'] x' y' ??? HP'; auto.
+  apply affineP in HP'; eauto using cmra_validN_op_r.
+  revert HP'. unseal.
+  intros (HP'&Haff).
+  rewrite Haff ?right_id.
+  apply HP; auto.
+  specialize (HPQ 0 x' ∅). rewrite ?left_id in HPQ *=> HPQ.
+  eapply HPQ;
+    eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
+  apply uPred_closed with (S n');
+    eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
+  rewrite -Haff. eauto.
+Qed.
+ *)
+End ATimeless_uPred.
\ No newline at end of file

theories/program_logic/auth.v

 From fri.algebra Require Export auth upred_tactics.
 From fri.program_logic Require Export invariants ghost_ownership.
-From fri.proofmode Require Import invariants ghost_ownership pstepshifts.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (* The CMRA we need. *)
@@ -28,13 +28,13 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
   Proof. solve_proper. Qed.
-  Global Instance auth_own_affine a : AffineP (auth_own a).
+  Global Instance auth_own_affine a : Affine (auth_own a).
   Proof. apply _. Qed.
-  Global Instance auth_own_atimeless a : ATimelessP (auth_own a).
+  Global Instance auth_own_atimeless a : ATimeless (auth_own a).
   Proof. apply _. Qed.
-  Global Instance auth_ctx_relevant N φ : RelevantP (auth_ctx N φ).
+  Global Instance auth_ctx_relevant N φ : Persistent (auth_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance auth_ctx_affine N φ : AffineP (auth_ctx N φ).
+  Global Instance auth_ctx_affine N φ : Affine (auth_ctx N φ).
   Proof. apply _. Qed.
   Global Instance auth_inv_ne n : 
     Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv).
@@ -61,11 +61,11 @@ Section auth.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
 
   Global Instance auth_own_relevant γ a :
-    Persistent a → RelevantP (auth_own γ a).
+    cmra.Persistent a → Persistent (auth_own γ a).
   Proof. rewrite /auth_own. apply _. Qed.
 
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
-  Proof. intros [? ->]. by rewrite auth_own_op affine_sep_elim_l'. Qed.
+  Proof. intros [? ->]. rewrite auth_own_op. by iIntros "(?&_)". Qed.
 
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ⧆✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
@@ -75,11 +75,12 @@ Section auth.
     ⧆▷ φ a ={E}=> ∃ γ, ⧆■(γ ∉ G) ★ auth_ctx γ N φ ★ auth_own γ a.
   Proof.
     iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
-    iPvs (own_alloc_strong' (Auth (Excl' a) a) _ G) as (γ) "[% Hγ]"; first done.
-    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
-    iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
-    { iIntros "@". iNext. iExists a. by iFrame. }
-    iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
+    iMod (own_alloc_strong' (Auth (Excl' a) a) _ G with "[#]") as (γ) "[% Hγ]";
+      [done|auto|set_solver|].
+    iRevert "Hγ"; rewrite auth_both_op. iIntros "(Hγ&Hγ')".
+    iMod (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done; try set_solver.
+    { iIntros "!# ". iNext. iExists a. by iFrame. }
+    iModIntro; iExists γ. iFrame. by iPureIntro.
   Qed.
 
   Lemma auth_alloc N E a :
@@ -87,15 +88,19 @@ Section auth.
     ⧆▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ★ auth_own γ a.
   Proof.
     iIntros (??) "Hφ".
-    iPvs (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; [done..|].
-    by iExists γ.
+    iMod (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; auto; try set_solver. 
   Qed.
 
-  Lemma auth_empty γ E : Emp ={E}=> auth_own γ ∅.
+  Lemma auth_empty γ E : emp ={E}=> auth_own γ ∅.
   Proof. by rewrite -own_empty. Qed.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!AffineFrameShiftAssertion fsaV fsa}.
 
+    Global Instance into_except_0_affine_later {PROP : sbi} (P : PROP):
+      ATimeless P → IntoExcept0 (⧆▷ P) (⧆P).
+    Proof.
+      by rewrite /ATimeless/IntoExcept0 => ->.
+    Qed.
 
   Lemma auth_afsa E N (Ψ : V → iPropG Λ Σ) γ a :
     fsaV → nclose N ⊆ E →
@@ -106,7 +111,9 @@ Section auth.
      ⊢ fsa E Ψ.
   Proof.
     iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
-    iInv "Hinv" as (a') "[Hγ Hφ]".
+    iInv "Hinv" as (a') "H" "_".
+    iDestruct "H" as "[Hγ Hφ]".
+    iMod "Hγ".
     iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
     rewrite (affine_elim (own γ _)).
     iDestruct (own_valid with "#Hγ") as "Hvalid".
@@ -158,273 +165,4 @@ Proof. destruct p; by rewrite /FromAssumption /= ?affine_elim. Qed.
   Qed.
 
 
-
-  (*
-  Lemma auth_afsa_alt E N (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV → nclose N ⊆ E →
-    auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
-      ⧆■ ✓ (a ⋅ af) ★ ⧆▷ φ (a ⋅ af) -★
-      ∃ b,  ⧆■ (a ~l~> b @ Some af) ★ (auth_own γ b -★
-      fsa (E ∖ nclose N) (λ x,
-        ⧆■ (a ~l~> b @ Some af) ★ ⧆▷ φ (b ⋅ af) ★ Ψ x)))
-     ⊢ fsa E Ψ.
-  Proof.
-    iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
-    iInv "Hinv" as (a') "[Hγ Hφ]".
-    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
-    rewrite (affine_elim (own γ _)).
-    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
-    iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl. 
-    iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
-    rewrite ->(left_id _ _) in Ha'; setoid_subst.
-    iApply pvs_afsa_afsa. 
-    iDestruct ("HΨ" $! af with "[Hφ]") as (b) "(%&HΨ)". 
-    { iSplitL ""; first done. iIntros "@". iNext. iAssumption. }
-    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
-    iSpecialize ("HΨ" with "Hγf").
-    iApply afsa_wand_r. iSplitL "HΨ".
-    { iClear "Hinv". iClear "Hvalid". iAssumption. } 
-    iIntros "@". iIntros (v) "HL". iDestruct "HL" as "(% & Hφ & HΨ)".
-    iPvsIntro. iSplitL "Hφ Hγ". 
-    - iIntros "@". rewrite /auth_inv.
-      iNext. iExists (b ⋅ af). by iFrame "Hφ".
-    - iAssumption.
-  Qed.
-   *)
-
-  (*
-  Lemma auth_afsa_alt' E N (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV → nclose N ⊆ E →
-    auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
-      ⧆■ ✓ (a ⋅ af) ★ ⧆▷ φ (a ⋅ af) -★
-      ∃ β,  ⧆■ (a ~l~> b @ Some af) ★ (auth_own γ b -★
-      fsa (E ∖ nclose N) (λ x,
-        ⧆■ (a ~l~> b @ Some af) ★ ⧆▷ φ (b ⋅ af) ★ Ψ x)))
-     ⊢ fsa E Ψ.
-  Proof.
-    iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
-    iInv "Hinv" as (a') "[Hγ Hφ]".
-    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
-    rewrite (affine_elim (own γ _)).
-    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
-    iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl. 
-    iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
-    rewrite ->(left_id _ _) in Ha'; setoid_subst.
-    iApply pvs_afsa_afsa. 
-    iDestruct ("HΨ" $! af with "[Hφ]") as (b) "(%&HΨ)". 
-    { iSplitL ""; first done. iIntros "@". iNext. iAssumption. }
-    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
-    iSpecialize ("HΨ" with "Hγf").
-    iApply afsa_wand_r. iSplitL "HΨ".
-    { iClear "Hinv". iClear "Hvalid". iAssumption. } 
-    iIntros "@". iIntros (v) "HL". iDestruct "HL" as "(% & Hφ & HΨ)".
-    iPvsIntro. iSplitL "Hφ Hγ". 
-    - iIntros "@". rewrite /auth_inv.
-      iNext. iExists (b ⋅ af). by iFrame "Hφ".
-    - iAssumption.
-  Qed.
-    - iApply "HΨ".
-
-
-iApply "HΨ". iSplitL ""; first by iPureIntro.
-      by rewrite -affine_affine_later. }
-
-
-iAssumption. iExact. iApply "Hφ". done.  iNext. iIntros "@". iNext. 
- first by iPureIntro.
-
-as "?".
-    iApply afsa_wand_r; iSplitL "HΨ Hφ".
-    { iApply "HΨ". iSplitL ""; first by iPureIntro.
-      by rewrite -affine_affine_later. }
-    iIntros "@". iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
-    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
-    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
-    iIntros "@". iNext.  iExists (b ⋅ af). by iFrame.
-
-  (*
-  Lemma auth_afsa_alt E N (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV → nclose N ⊆ E →
-    (auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ ∀ a',
-      ⧆■ ✓ (a ⋅ a') ★ 
-         ⧆▷ φ (a ⋅ a') -★
-           ∃ L Lv (Hup: LocalUpdate Lv L), ⧆■ (Lv a ∧ ✓ (L a ⋅ a')) ★ (auth_own γ (L a) -★
-            fsa (E ∖ nclose N) (λ x, 
-              ⧆■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ⧆▷ φ (L a ⋅ a') ★
-                 Ψ x)))
-     ⊢ fsa E Ψ.
-  Proof.
-    iIntros {??} "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
-    iInv "Hinv" as "Hinv'".
-    rewrite {2}/auth_inv.
-    rewrite {1}later_exist.
-    rewrite {1}affine_exist.
-    iDestruct "Hinv'" as {a'} "Hinv'".
-    rewrite affine_later_distrib'.
-    iDestruct "Hinv'" as "(Hγ&Hφ)".
-    iTimeless "Hγ" (own γ (● a')).
-    iTimeless "Hγf" (own γ (◯ a)).
-    rewrite affine_elim.
-    rewrite affine_elim.
-    iCombine "Hγ" "Hγf" as "Hγ".
-    iPoseProof (own_valid_r _ with "Hγ") as "Hγval". 
-    iDestruct "Hγval" as "(Hγ&#Hvalid)".
-    iPoseProof (@auth_validI' A (iResR Λ (globalF Σ)) _ _  (● a' ⋅ ◯ a)) as "Hav".
-    rewrite affine_and.
-    iDestruct "Hav" as "(Hav&_)".
-    rewrite (affine_elim (_ -★ _)%I).
-    iSpecialize ("Hav" with "Hvalid").
-    iDestruct "Hav" as "[Ha' %]".
-    simpl.
-    iClear "Hvalid".
-    rewrite affine_exist.
-    iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
-    rewrite ->(left_id _ _) in Ha'; setoid_subst.
-    iPoseProof pvs_afsa_afsa as "Hpvsfsa"; eauto.
-    rewrite affine_and.
-    iDestruct "Hpvsfsa" as "(Hpvsfsa&_)".
-    rewrite affine_elim.
-    iApply "Hpvsfsa".
-    iSpecialize ("HΨ" $! b).
-      rewrite const_equiv; eauto. rewrite -emp_True ?left_id.
-      rewrite affine_affine_later.
-      iSpecialize ("HΨ" with "Hφ").
-      iDestruct "HΨ" as {L Lv ?} "(%&HΨ)".
-      iPoseProof (own_update _ _ _ (E ∖ N) with "Hγ") as "Hown".
-      { apply (auth_local_update_l L); tauto. }
-    iPvs "Hown" (own γ _). 
-    iDestruct "Hown" as "[Hγ Hγf]".
-    iSpecialize ("HΨ" with "Hγf").
-    iApply afsa_wand_r. iSplitL "HΨ".
-    { iClear "Hinv". iApply "HΨ". }
-    apply affine_intro; first apply _.
-    iIntros {v} "HL". iDestruct "HL" as "(% & Hφ & HΨ)".
-    iPvsIntro. iSplitL "Hφ Hγ". 
-    - apply affine_intro; first apply _. rewrite affine_affine_later.
-      rewrite affine_elim.
-      iNext. iExists (L a ⋅ b). iClear "Hinv". by iFrame "Hφ". 
-    - iClear "Hinv". by iApply "HΨ".
-  Qed.
-    
-  (*
-  Lemma auth_afsa_alt' E N (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV → nclose N ⊆ E →
-    (auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ ∀ a',
-      ⧆■ ✓ (a ⋅ a') ★ 
-         ⧆▷ φ (a ⋅ a') -★
-           ∃ L Lv, ∀ x, ∃ (Hup: LocalUpdate (Lv x) (L x)),  
-                 ⧆■ (Lv x a ∧ ✓ (L x a ⋅ a')) ★ (auth_own γ (L x a) -★
-            fsa (E ∖ nclose N) (λ x, 
-              ⧆■ (Lv x a ∧ ✓ (L x a ⋅ a')) ★ ⧆▷ φ (L x a ⋅ a') ★
-                 Ψ x)))
-     ⊢ fsa E Ψ.
-  Proof.
-    iIntros {??} "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
-    iInv "Hinv" as "Hinv'".
-    rewrite {2}/auth_inv.
-    rewrite {1}later_exist.
-    rewrite {1}affine_exist.
-    iDestruct "Hinv'" as {a'} "Hinv'".
-    rewrite affine_later_distrib'.
-    iDestruct "Hinv'" as "(Hγ&Hφ)".
-    iTimeless "Hγ" (own γ (● a')).
-    iTimeless "Hγf" (own γ (◯ a)).
-    rewrite affine_elim.
-    rewrite affine_elim.
-    iCombine "Hγ" "Hγf" as "Hγ".
-    iPoseProof (own_valid_r _ with "Hγ") as "Hγval". 
-    iDestruct "Hγval" as "(Hγ&#Hvalid)".
-    iPoseProof (@auth_validI' A (iResR Λ (globalF Σ)) _ _  (● a' ⋅ ◯ a)) as "Hav".
-    rewrite affine_and.
-    iDestruct "Hav" as "(Hav&_)".
-    rewrite (affine_elim (_ -★ _)%I).
-    iSpecialize ("Hav" with "Hvalid").
-    iDestruct "Hav" as "[Ha' %]".
-    simpl.
-    iClear "Hvalid".
-    rewrite affine_exist.
-    iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
-    rewrite ->(left_id _ _) in Ha'; setoid_subst.
-    iPoseProof pvs_afsa_afsa as "Hpvsfsa"; eauto.
-    rewrite affine_and.
-    iDestruct "Hpvsfsa" as "(Hpvsfsa&_)".
-    rewrite affine_elim.
-    iApply "Hpvsfsa".
-    iSpecialize ("HΨ" $! b).
-      rewrite const_equiv; eauto. rewrite -emp_True ?left_id.
-      rewrite affine_affine_later.
-      iSpecialize ("HΨ" with "Hφ").