diff --git a/.dir-locals.el b/.dir-locals.el
index 79f36369df7a6c427c0f74df265c796c95d4b4ab..ee845344606b5da0003bb921dffd010b2a7313e5 100644
--- a/.dir-locals.el
+++ b/.dir-locals.el
@@ -3,6 +3,6 @@
((coq-mode
(coq-load-path
- (rec "lib/recdom/" "RecDom"))))
+ (rec "lib/ModuRes/" "ModuRes"))))
diff --git a/Makefile b/Makefile
index 28798520812627f93e02d5636b4c4645f06a3a89..85dbe4633bbc4b3f71e883ceb53df7b0f3f22cca 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.4pl3 ##
+## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
#############################################################################
# WARNING
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile lib/recdom/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/recdom/ RecDom
+# coq_makefile lib/ModuRes/ core_lang.v iris.v lang.v masks.v world_prop.v -R lib/ModuRes/ ModuRes -o Makefile
#
.DEFAULT_GOAL := all
@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# #
##########################
-COQLIBS?=-I . -R lib/recdom/ RecDom
-COQDOCLIBS?=-R lib/recdom/ RecDom
+COQLIBS?=-I . -R lib/ModuRes/ ModuRes
+COQDOCLIBS?=-R lib/ModuRes/ ModuRes
##########################
# #
@@ -108,7 +108,7 @@ endif
# #
#######################################
-all: ./lib/recdom/ $(VOFILES)
+all: $(VOFILES) ./lib/ModuRes/
spec: $(VIFILES)
@@ -142,7 +142,7 @@ beautify: $(VFILES:=.beautified)
@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 opt byte archclean clean install userinstall depend html validate ./lib/recdom/
+.PHONY: all opt byte archclean clean install userinstall depend html validate ./lib/ModuRes/
###################
# #
@@ -150,8 +150,8 @@ beautify: $(VFILES:=.beautified)
# #
###################
-./lib/recdom/:
- cd ./lib/recdom/ ; $(MAKE) all
+./lib/ModuRes/:
+ cd ./lib/ModuRes/ ; $(MAKE) all
####################
# #
@@ -169,27 +169,27 @@ userinstall:
+$(MAKE) USERINSTALL=true install
install:
- install -d $(DSTROOT)$(COQLIBINSTALL)/RecDom; \
+ install -d $(DSTROOT)$(COQLIBINSTALL)/ModuRes; \
for i in $(VOFILESINC); do \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/`basename $$i`; \
+ install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/`basename $$i`; \
done
- (cd ./lib/recdom/; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/recdom/ install)
+ (cd ./lib/ModuRes/; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/ModuRes/ install)
install-doc:
- install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+ install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
for i in html/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\
+ install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
done
clean:
rm -f $(VOFILES) $(VIFILES) $(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
- (cd ./lib/recdom/ ; $(MAKE) clean)
+ (cd ./lib/ModuRes/ ; $(MAKE) clean)
archclean:
rm -f *.cmx *.o
- (cd ./lib/recdom/ ; $(MAKE) archclean)
+ (cd ./lib/ModuRes/ ; $(MAKE) archclean)
printenv:
@$(COQBIN)coqtop -config
diff --git a/README.txt b/README.txt
index eb476e8cafc38cc8b7c1b00495eee6101328d9de..a2154985165333eea25d334ee9263c450101c044 100644
--- a/README.txt
+++ b/README.txt
@@ -53,14 +53,16 @@ CONTENTS
* masks.v introduces some lemmas about masks
- * world_prop.v uses the aforementioned Coq library to construct the
- domain for Iris propositions
+ * world_prop.v uses the ModuRes Coq library to construct the domain
+ for Iris propositions
* iris.v is the main file and contains the actual logic and the
proof of the rules for view shifts and Hoare triples
- It uses a Coq library in lib/ by Sieczkowski et al. to solve the
- recursive domain equation (see the paper for a reference).
+ The development uses ModuRes, a Coq library in by Sieczkowski et
+ al. to solve the recursive domain equation (see the paper for a
+ reference) and prove some of the standard separation logic rules. It
+ is located in the lib/ subdirectory.
REQUIREMENTS
diff --git a/core_lang.v b/core_lang.v
index d1d427d9516dd080d1f4daee290fe642e19fd823..62b061a0cc79d1c0f47d8ca5d76730a69dc53bcb 100644
--- a/core_lang.v
+++ b/core_lang.v
@@ -1,4 +1,4 @@
-Require Import RecDom.PCM.
+Require Import ModuRes.PCM.
Module Type CORE_LANG.
Delimit Scope lang_scope with lang.
diff --git a/iris.v b/iris.v
index 95f3c00c43293d8657168aaf3ce9c41df44471e2..a433c8d3ca123192c02278958f88f94823fabbb8 100644
--- a/iris.v
+++ b/iris.v
@@ -1,5 +1,5 @@
Require Import world_prop core_lang lang masks.
-Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
+Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module Iris (RL : PCM_T) (C : CORE_LANG).
@@ -215,6 +215,12 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
intros w n r; simpl; unfold const; reflexivity.
Qed.
+ Lemma box_disj p q :
+ □ (p ∨ q) == □ p ∨ □ q.
+ Proof.
+ intros w n r; reflexivity.
+ Qed.
+
(** Ghost state ownership **)
Lemma ownL_sc (u t : option RL.res) :
ownL (u · t)%pcm == ownL u * ownL t.
diff --git a/lang.v b/lang.v
index 5f09ade3204014e861dab3e75aa867316c7a939a..5a33d268a09f490b5bf53c0865814e650c4ab2d9 100644
--- a/lang.v
+++ b/lang.v
@@ -1,5 +1,5 @@
Require Import List.
-Require Import RecDom.PCM.
+Require Import ModuRes.PCM.
Require Import core_lang.
(******************************************************************)
diff --git a/lib/recdom/.dir-locals.el b/lib/ModuRes/.dir-locals.el
similarity index 82%
rename from lib/recdom/.dir-locals.el
rename to lib/ModuRes/.dir-locals.el
index 82ea871da38b04b9047cb5afdf61bf7b5063c320..44673b5a49b0e9c498059e82dad73354f19024ff 100644
--- a/lib/recdom/.dir-locals.el
+++ b/lib/ModuRes/.dir-locals.el
@@ -3,6 +3,6 @@
((coq-mode
(coq-load-path
- (rec "./" "RecDom"))))
+ (rec "./" "ModuRes"))))
diff --git a/lib/recdom/BI.v b/lib/ModuRes/BI.v
similarity index 100%
rename from lib/recdom/BI.v
rename to lib/ModuRes/BI.v
diff --git a/lib/recdom/CBUltInst.v b/lib/ModuRes/CBUltInst.v
similarity index 100%
rename from lib/recdom/CBUltInst.v
rename to lib/ModuRes/CBUltInst.v
diff --git a/lib/recdom/CSetoid.v b/lib/ModuRes/CSetoid.v
similarity index 100%
rename from lib/recdom/CSetoid.v
rename to lib/ModuRes/CSetoid.v
diff --git a/lib/recdom/Constr.v b/lib/ModuRes/Constr.v
similarity index 100%
rename from lib/recdom/Constr.v
rename to lib/ModuRes/Constr.v
diff --git a/lib/recdom/Finmap.v b/lib/ModuRes/Finmap.v
similarity index 100%
rename from lib/recdom/Finmap.v
rename to lib/ModuRes/Finmap.v
diff --git a/lib/recdom/Makefile b/lib/ModuRes/Makefile
similarity index 92%
rename from lib/recdom/Makefile
rename to lib/ModuRes/Makefile
index dc09c4a156011bd1462fbde2cf18986845453e7b..0affb72850ca00c0ee77db57cd4b84877446c15e 100644
--- a/lib/recdom/Makefile
+++ b/lib/ModuRes/Makefile
@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.4pl3 ##
+## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
#############################################################################
# WARNING
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile -R . RecDom BI.v CBUltInst.v CSetoid.v Constr.v Finmap.v MetricCore.v MetricRec.v PCBUltInst.v PCM.v Predom.v PreoMet.v TOTInst.v UPred.v -o Makefile
+# coq_makefile -R . ModuRes BI.v CBUltInst.v CSetoid.v Constr.v Finmap.v MetricCore.v MetricRec.v PCBUltInst.v PCM.v Predom.v PreoMet.v TOTInst.v UPred.v -o Makefile
#
.DEFAULT_GOAL := all
@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# #
##########################
-COQLIBS?= -R . RecDom
-COQDOCLIBS?=-R . RecDom
+COQLIBS?= -R . ModuRes
+COQDOCLIBS?=-R . ModuRes
##########################
# #
@@ -168,14 +168,14 @@ userinstall:
install:
for i in $(VOFILES); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i; \
+ install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i`; \
+ install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i; \
done
install-doc:
- install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+ install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
for i in html/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\
+ install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
done
clean:
diff --git a/lib/recdom/MetricCore.v b/lib/ModuRes/MetricCore.v
similarity index 100%
rename from lib/recdom/MetricCore.v
rename to lib/ModuRes/MetricCore.v
diff --git a/lib/recdom/MetricRec.v b/lib/ModuRes/MetricRec.v
similarity index 100%
rename from lib/recdom/MetricRec.v
rename to lib/ModuRes/MetricRec.v
diff --git a/lib/recdom/PCBUltInst.v b/lib/ModuRes/PCBUltInst.v
similarity index 100%
rename from lib/recdom/PCBUltInst.v
rename to lib/ModuRes/PCBUltInst.v
diff --git a/lib/recdom/PCM.v b/lib/ModuRes/PCM.v
similarity index 100%
rename from lib/recdom/PCM.v
rename to lib/ModuRes/PCM.v
diff --git a/lib/recdom/Predom.v b/lib/ModuRes/Predom.v
similarity index 100%
rename from lib/recdom/Predom.v
rename to lib/ModuRes/Predom.v
diff --git a/lib/recdom/PreoMet.v b/lib/ModuRes/PreoMet.v
similarity index 100%
rename from lib/recdom/PreoMet.v
rename to lib/ModuRes/PreoMet.v
diff --git a/lib/recdom/TOTInst.v b/lib/ModuRes/TOTInst.v
similarity index 100%
rename from lib/recdom/TOTInst.v
rename to lib/ModuRes/TOTInst.v
diff --git a/lib/recdom/UPred.v b/lib/ModuRes/UPred.v
similarity index 100%
rename from lib/recdom/UPred.v
rename to lib/ModuRes/UPred.v
diff --git a/world_prop.v b/world_prop.v
index 9e78564400ab020829bf50e49bbc027a910fd01f..103ead16f7dcdb3ce68d72f51269dc7cd6bec61e 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -1,8 +1,8 @@
(** In this file, we show how we can use the solution of the recursive
domain equations to build a higher-order separation logic *)
-Require Import RecDom.PreoMet RecDom.MetricRec RecDom.CBUltInst.
-Require Import RecDom.Finmap RecDom.Constr.
-Require Import RecDom.PCM RecDom.UPred RecDom.BI.
+Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
+Require Import ModuRes.Finmap ModuRes.Constr.
+Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
Module WorldProp (Res : PCM_T).