No longer require iFunctor to have an identity element.

program_logic/adequacy.v

@@ -72,9 +72,9 @@ Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
              wsat 3 coPset_all σ2 (big_op rs2).
 Proof.
   intros Hv ? [k ?]%rtc_nsteps.
-  eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
+  eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
   { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
-  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m); split_ands.
+  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_ands.
   * by rewrite Res_op ?left_id ?right_id.
   * by rewrite /uPred_holds /=.
   * by apply ownG_spec.

program_logic/functor.v

@@ -2,8 +2,6 @@ Require Export algebra.cmra.
 
 Structure iFunctor := IFunctor {
   ifunctor_car :> cofeT → cmraT;
-  ifunctor_empty A : Empty (ifunctor_car A);
-  ifunctor_identity A : CMRAIdentity (ifunctor_car A);
   ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
   ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
   ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x ≡ x;
@@ -11,7 +9,6 @@ Structure iFunctor := IFunctor {
     ifunctor_map (g ◎ f) x ≡ ifunctor_map g (ifunctor_map f x);
   ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
 }.
-Existing Instances ifunctor_empty ifunctor_identity.
 Existing Instances ifunctor_map_ne ifunctor_map_mono.
 
 Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :

program_logic/ownership.v

@@ -4,7 +4,7 @@ Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
 Arguments inv {_ _} _ _%I.
 Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Λ Σ} (m : iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ m).
+Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ (Some m)).
 Instance: Params (@inv) 3.
 Instance: Params (@ownP) 2.
 Instance: Params (@ownG) 2.
@@ -53,7 +53,7 @@ Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
 Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
 Proof.
   apply uPred.always_own.
-  by rewrite Res_unit !cmra_unit_empty cmra_unit_idempotent.
+  by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idempotent m).
 Qed.
 Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
@@ -78,7 +78,7 @@ Proof.
   intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
   naive_solver (apply cmra_empty_leastN).
 Qed.
-Lemma ownG_spec r n m : (ownG m) n r ↔ m ≼{n} gst r.
+Lemma ownG_spec r n m : (ownG m) n r ↔ Some m ≼{n} gst r.
 Proof.
   rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
 Qed.

program_logic/pviewshifts.v

@@ -100,8 +100,8 @@ Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
-  destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P)
-    as (m'&?&?); eauto using cmra_includedN_le.
+  destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P) as (m'&?&?); auto.
+  { apply cmra_includedN_le with (S n); auto. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
 Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ inv i P).

program_logic/resources.v

@@ -4,7 +4,7 @@ Require Export program_logic.language program_logic.functor.
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);
   pst : exclRA (istateC Λ);
-  gst : Σ A;
+  gst : optionRA (Σ A);
 }.
 Add Printing Constructor res.
 Arguments Res {_ _ _} _ _ _.
@@ -136,7 +136,7 @@ Qed.
 Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
   Res (wld r) (Excl σ) (gst r).
 Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
-  Res (wld r) (pst r) m.
+  Res (wld r) (pst r) (Some m).
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
 Proof. by intros (?&?&?). Qed.
@@ -167,9 +167,9 @@ Arguments resC : clear implicits.
 Arguments resRA : clear implicits.
 
 Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
-  Res (agree_map f <$> (wld r))
+  Res (agree_map f <$> wld r)
       (pst r)
-      (ifunctor_map Σ f (gst r)).
+      (ifunctor_map Σ f <$> gst r).
 Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
   (∀ n, Proper (dist n ==> dist n) f) →
   ∀ n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).
@@ -178,23 +178,25 @@ Lemma res_map_id {Λ Σ A} (r : res Λ Σ A) : res_map cid r ≡ r.
 Proof.
   constructor; simpl; [|done|].
   * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
-    by rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
-  * by rewrite -{2}(ifunctor_map_id Σ (gst r)); apply ifunctor_map_ext=> m /=.
+    by rewrite -{2}(agree_map_id y); apply agree_map_ext.
+  * rewrite -{2}(option_fmap_id (gst r)); apply option_fmap_setoid_ext=> m /=.
+    by rewrite -{2}(ifunctor_map_id Σ m); apply ifunctor_map_ext.
 Qed.
 Lemma res_map_compose {Λ Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Λ Σ A) :
   res_map (g ◎ f) r ≡ res_map g (res_map f r).
 Proof.
   constructor; simpl; [|done|].
   * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
-    by rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
-  * by rewrite -ifunctor_map_compose; apply ifunctor_map_ext=> m /=.
+    by rewrite -agree_map_compose; apply agree_map_ext.
+  * rewrite -option_fmap_compose; apply option_fmap_setoid_ext=> m /=.
+    by rewrite -ifunctor_map_compose; apply ifunctor_map_ext.
 Qed.
 Lemma res_map_ext {Λ Σ A B} (f g : A -n> B) (r : res Λ Σ A) :
   (∀ x, f x ≡ g x) → res_map f r ≡ res_map g r.
 Proof.
   intros Hfg; split; simpl; auto.
   * by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
-  * by apply ifunctor_map_ext.
+  * by apply option_fmap_setoid_ext=>m; apply ifunctor_map_ext.
 Qed.
 Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
   CMRAMonotone (@res_map Λ Σ _ _ f).
@@ -211,5 +213,5 @@ Instance resC_map_ne {Λ Σ A B} n :
 Proof.
   intros f g Hfg r; split; simpl; auto.
   * by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
-  * by apply ifunctor_map_ne.
+  * by apply optionC_map_ne, ifunctor_map_ne.
 Qed.

program_logic/tests.v

@@ -3,5 +3,5 @@ Require Import program_logic.model.
 
 Module ModelTest. (* Make sure we got the notations right. *)
   Definition iResTest {Λ : language} {Σ : iFunctor}
-    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
+    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p (Some g).
 End ModelTest.

program_logic/wsat.v

@@ -33,6 +33,7 @@ Implicit Types r : iRes Λ Σ.
 Implicit Types rs : gmap positive (iRes Λ Σ).
 Implicit Types P : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
+Implicit Types mm : option (iGst Λ Σ).
 
 Instance wsat_ne' : Proper (dist n ==> impl) (@wsat Λ Σ n E σ).
 Proof.
@@ -66,7 +67,7 @@ Proof.
   destruct n; [done|intros [rs ?]].
   eapply cmra_validN_op_l, wsat_pre_valid; eauto.
 Qed.
-Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl σ) m).
+Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) mm).
 Proof.
   intros Hv. exists ∅; constructor; auto.
   * rewrite big_opM_empty right_id.
@@ -125,12 +126,12 @@ Proof.
   by constructor; split_ands'; try (rewrite /= -associative Hpst').
 Qed.
 Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
-  m1 ≼{S n} gst r → m1 ~~>: P →
+  Some m1 ≼{S n} gst r → m1 ~~>: P →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
-  intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
-  destruct (Hup (mf ⋅ gst (rf ⋅ big_opM rs)) n) as (m2&?&Hval').
-  { by rewrite /= (associative _ m1) -Hr (associative _). }
+  intros [mf Hr] Hup%option_updateP' [rs [(?&?&?) Hσ HE Hwld]].
+  destruct (Hup (mf ⋅ gst (rf ⋅ big_opM rs)) n) as ([m2|]&?&Hval'); try done.
+  { by rewrite /= (associative _ (Some m1)) -Hr associative. }
   exists m2; split; [exists rs; split; split_ands'; auto|done].
 Qed.
 Lemma wsat_alloc n E1 E2 σ r P rP :