Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

Makefile

-#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.5rc1     ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject -o Makefile 
-#
-
-.DEFAULT_GOAL := all
-
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# TIMECMD set a command to log .v compilation time;
-# TIMED if non empty, use the default time command as TIMECMD;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-
-# Here is a hack to make $(eval $(shell works:
-define donewline
-
-
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
-
-TIMED=
-TIMECMD=
-STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
-TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
-
-vo_to_obj = $(addsuffix .o,\
-  $(filter-out Warning: Error:,\
-  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
-
-##########################
-#                        #
-# Libraries definitions. #
-#                        #
-##########################
-
-COQLIBS?=-Q "." ""
-COQDOCLIBS?=-Q "." ""
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-
-OPT?=
-COQDEP?="$(COQBIN)coqdep" -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(TIMER) "$(COQBIN)coqc"
-GALLINA?="$(COQBIN)gallina"
-COQDOC?="$(COQBIN)coqdoc"
-COQCHK?="$(COQBIN)coqchk"
-COQMKTOP?="$(COQBIN)coqmktop"
-
-##################
-#                #
-# Install Paths. #
-#                #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?="$(HOME)/.local/share"
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL="${COQLIB}user-contrib"
-COQDOCINSTALL="${DOCDIR}user-contrib"
-COQTOPINSTALL="${COQLIB}toploop"
-endif
-
-######################
-#                    #
-# Files dispatching. #
-#                    #
-######################
-
-VFILES:=barrier/heap_lang.v\
-  iris/parameter.v\
-  iris/hoare.v\
-  iris/resources.v\
-  iris/pviewshifts.v\
-  iris/language.v\
-  iris/weakestpre.v\
-  iris/ownership.v\
-  iris/wsat.v\
-  iris/viewshifts.v\
-  iris/namespace.v\
-  iris/lifting.v\
-  iris/hoare_lifting.v\
-  iris/adequacy.v\
-  iris/model.v\
-  modures/excl.v\
-  modures/ra.v\
-  modures/agree.v\
-  modures/cofe_solver.v\
-  modures/dra.v\
-  modures/base.v\
-  modures/cofe.v\
-  modures/logic.v\
-  modures/fin_maps.v\
-  modures/auth.v\
-  modures/sts.v\
-  modures/cmra.v\
-  modures/option.v\
-  prelude/error.v\
-  prelude/list.v\
-  prelude/decidable.v\
-  prelude/sets.v\
-  prelude/lexico.v\
-  prelude/co_pset.v\
-  prelude/zmap.v\
-  prelude/nmap.v\
-  prelude/numbers.v\
-  prelude/finite.v\
-  prelude/listset_nodup.v\
-  prelude/prelude.v\
-  prelude/tactics.v\
-  prelude/base.v\
-  prelude/gmap.v\
-  prelude/streams.v\
-  prelude/listset.v\
-  prelude/collections.v\
-  prelude/relations.v\
-  prelude/strings.v\
-  prelude/natmap.v\
-  prelude/orders.v\
-  prelude/countable.v\
-  prelude/pretty.v\
-  prelude/hashset.v\
-  prelude/proof_irrel.v\
-  prelude/mapset.v\
-  prelude/fin_collections.v\
-  prelude/stringmap.v\
-  prelude/pmap.v\
-  prelude/vector.v\
-  prelude/fin_maps.v\
-  prelude/bsets.v\
-  prelude/fin_map_dom.v\
-  prelude/option.v
-
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
--include $(addsuffix .d,$(VFILES))
-else
-ifeq ($(MAKECMDGOALS),)
--include $(addsuffix .d,$(VFILES))
-endif
-endif
-
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-VO=vo
-VOFILES:=$(VFILES:.v=.$(VO))
-GLOBFILES:=$(VFILES:.v=.glob)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-OBJFILES=$(call vo_to_obj,$(VOFILES))
-ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
-NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
-ifeq '$(HASNATDYNLINK)' 'true'
-HASNATDYNLINK_OR_EMPTY := yes
-else
-HASNATDYNLINK_OR_EMPTY :=
-endif
-
-#######################################
-#                                     #
-# Definition of the toplevel targets. #
-#                                     #
-#######################################
-
-all: $(VOFILES) 
-
-quick: $(VOFILES:.vo=.vio)
-
-vio2vo:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-checkproofs:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
-
-beautify: $(VFILES:=.beautified)
-	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
-	@echo 'Do not do "make clean" until you are sure that everything went well!'
-	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-
-.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
-
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
-
-byte:
-	$(MAKE) all "OPT:=-byte"
-
-opt:
-	$(MAKE) all "OPT:=-opt"
-
-userinstall:
-	+$(MAKE) USERINSTALL=true install
-
-install:
-	cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)//$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)//$$i; \
-	done
-
-install-doc:
-	install -d "$(DSTROOT)"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/html
-	for i in html/*; do \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT)/$$i;\
-	done
-
-uninstall_me.sh: Makefile
-	echo '#!/bin/sh' > $@
-	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/ && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/$(INSTALLDEFAULTROOT) \\\n' >> "$@"
-	printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
-	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find $(INSTALLDEFAULTROOT)/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
-	chmod +x $@
-
-uninstall: uninstall_me.sh
-	sh $<
-
-clean::
-	rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
-	find . -name .coq-native -type d -empty -delete
-	rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
-	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
-	- rm -rf html mlihtml uninstall_me.sh
-
-cleanall:: clean
-	rm -f $(patsubst %.v,.%.aux,$(VFILES))
-
-archclean::
-	rm -f *.cmx *.o
-
-printenv:
-	@"$(COQBIN)coqtop" -config
-	@echo 'CAMLC =	$(CAMLC)'
-	@echo 'CAMLOPTC =	$(CAMLOPTC)'
-	@echo 'PP =	$(PP)'
-	@echo 'COQFLAGS =	$(COQFLAGS)'
-	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
-	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
-
-Makefile: _CoqProject
-	mv -f $@ $@.bak
-	"$(COQBIN)coq_makefile" -f $< -o $@
-
-
-###################
-#                 #
-# Implicit rules. #
-#                 #
-###################
-
-$(VOFILES): %.vo: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-$(GLOBFILES): %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-$(VFILES:.v=.vio): %.vio: %.v
-	$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*
-
-$(GFILES): %.g: %.v
-	$(GALLINA) $<
-
-$(VFILES:.v=.tex): %.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-$(HTMLFILES): %.html: %.v %.glob
-	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-$(VFILES:.v=.g.tex): %.g.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-$(GHTMLFILES): %.g.html: %.v %.glob
-	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
-
-$(addsuffix .d,$(VFILES)): %.v.d: %.v
-	$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-$(addsuffix .beautified,$(VFILES)): %.v.beautified:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-

configure

+#!/bin/sh
+coq_makefile -f _CoqProject -o Makefile

iris/model.v

@@ -2,26 +2,32 @@ Require Export modures.logic iris.resources.
 Require Import modures.cofe_solver.
 
 Module iProp.
-Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ A).
+Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)).
 Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
     (f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
-  uPredC_map (resRA_map (f.1)).
+  uPredC_map (resRA_map (laterC_map (f.1))).
 Definition result Σ : solution (F Σ).
 Proof.
   apply (solver.result _ (@map Σ)).
-  * by intros A B r n ?; rewrite /uPred_holds /= res_map_id.
-  * by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?;
-      rewrite /= /uPred_holds /= res_map_compose.
-  * by intros A1 A2 B1 B2 n f f' [??] r;
-      apply upredC_map_ne, resRA_map_contractive.
+  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=>r {P} /=.
+    rewrite -{2}(res_map_id r). apply res_map_ext=>{r} r /=. by rewrite later_map_id.
+  * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
+    rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
+    rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
+    by rewrite -later_map_compose.
+  * intros A1 A2 B1 B2 n f f' [??] P.
+    by apply upredC_map_ne, resRA_map_ne, laterC_map_contractive.
 Qed.
 End iProp.
 
 (* Solution *)
 Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
-Notation res' Σ := (res Σ (iPreProp Σ)).
-Notation icmra' Σ := (icmra Σ (laterC (iPreProp Σ))).
-Definition iProp (Σ : iParam) : cofeT := uPredC (resRA Σ (iPreProp Σ)).
+Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
+Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
+Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))).
+Notation iPst Σ := (exclRA (istateC Σ)).
+Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))).
+Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
 Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
 Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
 Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
@@ -34,3 +40,7 @@ Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
 Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
 Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
 Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
+
+Module Test. (* Make sure we got the notations right. *)
+  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+End Test.

iris/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 {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Σ} (m : icmra' Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
+Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
 Instance: Params (@inv) 2.
 Instance: Params (@ownP) 1.
 Instance: Params (@ownG) 1.
@@ -13,10 +13,10 @@ Typeclasses Opaque inv ownG ownP.
 
 Section ownership.
 Context {Σ : iParam}.
-Implicit Types r : res' Σ.
+Implicit Types r : iRes Σ.
 Implicit Types σ : istate Σ.
 Implicit Types P : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iGst Σ.
 
 (* Invariants *)
 Global Instance inv_contractive i : Contractive (@inv Σ i).

iris/pviewshifts.v

@@ -29,7 +29,7 @@ Instance: Params (@pvs) 3.
 Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iGst Σ.
 Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
@@ -96,7 +96,7 @@ Proof.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
 Qed.
-Lemma pvs_updateP E m (P : icmra' Σ → Prop) :
+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.

iris/resources.v

 Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
 
 Record res (Σ : iParam) (A : cofeT) := Res {
-  wld : mapRA positive (agreeRA (laterC A));
+  wld : mapRA positive (agreeRA A);
   pst : exclRA (istateC Σ);
-  gst : icmra Σ (laterC A);
+  gst : icmra Σ A;
 }.
 Add Printing Constructor res.
 Arguments Res {_ _} _ _ _.
@@ -137,7 +137,7 @@ Canonical Structure resRA : cmraT :=
 
 Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
   Res (wld r) (Excl σ) (gst r).
-Definition update_gst (m : icmra Σ (laterC A)) (r : res Σ A) : res Σ A :=
+Definition update_gst (m : icmra Σ A) (r : res Σ A) : res Σ A :=
   Res (wld r) (pst r) m.
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
@@ -167,9 +167,9 @@ End res.
 Arguments resRA : clear implicits.
 
 Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B :=
-  Res (agree_map (later_map f) <$> (wld r))
+  Res (agree_map f <$> (wld r))
       (pst r)
-      (icmra_map Σ (laterC_map f) (gst r)).
+      (icmra_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,20 +178,22 @@ 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 ? /=.
-    rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
-    by rewrite later_map_id.
-  * rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
-    by rewrite later_map_id.
+    by rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
+  * by rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
 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 _ /=.
-    rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
-    by rewrite later_map_compose.
-  * rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
-    by rewrite later_map_compose.
+    by rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
+  * by rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
+Qed.
+Lemma res_map_ext {Σ A B} (f g : A -n> B) :
+  (∀ r, f r ≡ g r) -> ∀ r : res Σ A, res_map f r ≡ res_map g r.
+Proof.
+  move=>H r. split; simpl;
+    [apply map_fmap_setoid_ext; intros; apply agree_map_ext | | apply icmra_map_ext]; done.
 Qed.
 Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
   CofeMor (res_map f : resRA Σ A → resRA Σ B).
@@ -203,10 +205,10 @@ Proof.
       intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
   * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
 Qed.
-Instance resRA_map_contractive {Σ A B} : Contractive (@resRA_map Σ A B).
+Lemma resRA_map_ne {Σ A B} (f g : A -n> B) n :
+  f ={n}= g → resRA_map (Σ := Σ) f ={n}= resRA_map g.
 Proof.
-  intros n f g ? r; constructor; simpl; [|done|].
-  * by apply (mapRA_map_ne _ (agreeRA_map (laterC_map f))
-      (agreeRA_map (laterC_map g))), agreeRA_map_ne, laterC_map_contractive.
-  * by apply icmra_map_ne, laterC_map_contractive.
+  intros ? r. split; simpl;
+    [apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne
+     | | apply icmra_map_ne]; done.
 Qed.

iris/viewshifts.v

@@ -16,7 +16,7 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I)
 Section vs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
-Implicit Types m : icmra' Σ.
+Implicit Types m : iGst Σ.
 Import uPred.
 
 Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q.
@@ -85,7 +85,7 @@ Proof.
   intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_close.
 Qed.
-Lemma vs_updateP E m (P : icmra' Σ → Prop) :
+Lemma vs_updateP E m (P : iGst Σ → Prop) :
   m ⇝: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
 Lemma vs_update E m m' : m ⇝ m' → ownG m >{E}> ownG m'.

iris/weakestpre.v

@@ -7,8 +7,8 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
-    (k : nat) (rf : res' Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
+Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
+    (k : nat) (rf : iRes Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
   wf_safe : reducible e1 σ1;
   wp_step e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
@@ -18,7 +18,7 @@ Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
       ∀ e', ef = Some e' → Qfork e' k r2'
 }.
 CoInductive wp_pre {Σ} (E : coPset)
-     (Q : ival Σ → iProp Σ) : iexpr Σ → nat → res' Σ → Prop :=
+     (Q : ival Σ → iProp Σ) : iexpr Σ → nat → iRes Σ → Prop :=
   | wp_pre_0 e r : wp_pre E Q e 0 r
   | wp_pre_value n r v : Q v n r → wp_pre E Q (of_val v) n r
   | wp_pre_step n r1 e1 :

iris/wsat.v

@@ -5,7 +5,7 @@ Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
 Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
 
 Record wsat_pre {Σ} (n : nat) (E : coPset)
-    (σ : istate Σ) (rs : gmap positive (res' Σ)) (r : res' Σ) := {
+    (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := {
   wsat_pre_valid : ✓{S n} r;
   wsat_pre_state : pst r ≡ Excl σ;
   wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
@@ -19,7 +19,7 @@ Arguments wsat_pre_state {_ _ _ _ _ _} _.
 Arguments wsat_pre_dom {_ _ _ _ _ _} _ _ _.
 Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
 
-Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : res' Σ) : Prop :=
+Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : 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.
@@ -27,8 +27,8 @@ Arguments wsat : simpl never.
 Section wsat.
 Context {Σ : iParam}.
 Implicit Types σ : istate Σ.
-Implicit Types r : res' Σ.
-Implicit Types rs : gmap positive (res' Σ).
+Implicit Types r : iRes Σ.
+Implicit Types rs : gmap positive (iRes Σ).
 Implicit Types P : iProp Σ.
 
 Instance wsat_ne' : Proper (dist n ==> impl) (wsat (Σ:=Σ) n E σ).
@@ -120,7 +120,7 @@ Proof.
   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) :
+Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) :
   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.

modures/cmra.v

@@ -105,6 +105,13 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
   validN_preserving n x : ✓{n} x → ✓{n} (f x)
 }.
+Instance compose_cmra_monotone {A B C : cmraT} (f : A -n> B) (g : B -n> C) :
+  CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ◎ f).
+Proof.
+  split.
+  - move=> n x y Hxy /=. eapply includedN_preserving, includedN_preserving; done.
+  - move=> n x Hx /=. eapply validN_preserving, validN_preserving; done.
+Qed.
 
 (** * Updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,

modures/logic.v

@@ -54,20 +54,31 @@ Instance uPred_holds_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
 Proof. by intros x1 x2 Hx; apply uPred_holds_ne, equiv_dist. Qed.
 
 (** functor *)
-Program Definition uPred_map {M1 M2 : cmraT} (f : M2 → M1)
-  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
-  (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
-Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
+Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} (P : uPred M1) :
+  uPred M2 := {| uPred_holds n x := P n (f x) |}.
+Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
+Next Obligation. intros M1 M2 f _ P x; apply uPred_0. Qed.
 Next Obligation.
   naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
 Qed.
-Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 → M1)
-  `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f} :
+Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
+  `{!CMRAMonotone f} :
   Proper (dist n ==> dist n) (uPred_map f).
 Proof.
   by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
 Qed.
+Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
+Proof. by intros x n ?. Qed.
+Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
+      `{!CMRAMonotone f} `{!CMRAMonotone g}
+      (P : uPred M3):
+  uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
+Proof. by intros x n Hx. Qed.
+Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
+      `{!CMRAMonotone f} `{!CMRAMonotone g}:
+  (∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
+Proof. move=> H x P n Hx /=. by rewrite /uPred_holds /= H. Qed.
 Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :