Commit 61f3b3f5 authored by Filip Sieczkowski's avatar Filip Sieczkowski

More README, renamed library to ModuRes

parent c7b8538e
...@@ -3,6 +3,6 @@ ...@@ -3,6 +3,6 @@
((coq-mode ((coq-mode
(coq-load-path (coq-load-path
(rec "lib/recdom/" "RecDom")))) (rec "lib/ModuRes/" "ModuRes"))))
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ## ## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ## ## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.4pl3 ## ## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
############################################################################# #############################################################################
# WARNING # WARNING
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
# #
# This Makefile was generated by the command line : # 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 .DEFAULT_GOAL := all
...@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config) ...@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# # # #
########################## ##########################
COQLIBS?=-I . -R lib/recdom/ RecDom COQLIBS?=-I . -R lib/ModuRes/ ModuRes
COQDOCLIBS?=-R lib/recdom/ RecDom COQDOCLIBS?=-R lib/ModuRes/ ModuRes
########################## ##########################
# # # #
...@@ -108,7 +108,7 @@ endif ...@@ -108,7 +108,7 @@ endif
# # # #
####################################### #######################################
all: ./lib/recdom/ $(VOFILES) all: $(VOFILES) ./lib/ModuRes/
spec: $(VIFILES) spec: $(VIFILES)
...@@ -142,7 +142,7 @@ beautify: $(VFILES:=.beautified) ...@@ -142,7 +142,7 @@ beautify: $(VFILES:=.beautified)
@echo 'Do not do "make clean" until you are sure that everything went well!' @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/' @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) ...@@ -150,8 +150,8 @@ beautify: $(VFILES:=.beautified)
# # # #
################### ###################
./lib/recdom/: ./lib/ModuRes/:
cd ./lib/recdom/ ; $(MAKE) all cd ./lib/ModuRes/ ; $(MAKE) all
#################### ####################
# # # #
...@@ -169,27 +169,27 @@ userinstall: ...@@ -169,27 +169,27 @@ userinstall:
+$(MAKE) USERINSTALL=true install +$(MAKE) USERINSTALL=true install
install: install:
install -d $(DSTROOT)$(COQLIBINSTALL)/RecDom; \ install -d $(DSTROOT)$(COQLIBINSTALL)/ModuRes; \
for i in $(VOFILESINC); do \ for i in $(VOFILESINC); do \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/`basename $$i`; \ install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/`basename $$i`; \
done 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-doc:
install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
for i in html/*; do \ for i in html/*; do \
install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\ install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
done done
clean: clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) 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 -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 - rm -rf html mlihtml
(cd ./lib/recdom/ ; $(MAKE) clean) (cd ./lib/ModuRes/ ; $(MAKE) clean)
archclean: archclean:
rm -f *.cmx *.o rm -f *.cmx *.o
(cd ./lib/recdom/ ; $(MAKE) archclean) (cd ./lib/ModuRes/ ; $(MAKE) archclean)
printenv: printenv:
@$(COQBIN)coqtop -config @$(COQBIN)coqtop -config
......
...@@ -53,14 +53,16 @@ CONTENTS ...@@ -53,14 +53,16 @@ CONTENTS
* masks.v introduces some lemmas about masks * masks.v introduces some lemmas about masks
* world_prop.v uses the aforementioned Coq library to construct the * world_prop.v uses the ModuRes Coq library to construct the domain
domain for Iris propositions for Iris propositions
* iris.v is the main file and contains the actual logic and the * iris.v is the main file and contains the actual logic and the
proof of the rules for view shifts and Hoare triples proof of the rules for view shifts and Hoare triples
It uses a Coq library in lib/ by Sieczkowski et al. to solve the The development uses ModuRes, a Coq library in by Sieczkowski et
recursive domain equation (see the paper for a reference). 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 REQUIREMENTS
......
Require Import RecDom.PCM. Require Import ModuRes.PCM.
Module Type CORE_LANG. Module Type CORE_LANG.
Delimit Scope lang_scope with lang. Delimit Scope lang_scope with lang.
......
Require Import world_prop core_lang lang masks. 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). Module Iris (RL : PCM_T) (C : CORE_LANG).
...@@ -215,6 +215,12 @@ 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. intros w n r; simpl; unfold const; reflexivity.
Qed. Qed.
Lemma box_disj p q :
(p q) == p q.
Proof.
intros w n r; reflexivity.
Qed.
(** Ghost state ownership **) (** Ghost state ownership **)
Lemma ownL_sc (u t : option RL.res) : Lemma ownL_sc (u t : option RL.res) :
ownL (u · t)%pcm == ownL u * ownL t. ownL (u · t)%pcm == ownL u * ownL t.
......
Require Import List. Require Import List.
Require Import RecDom.PCM. Require Import ModuRes.PCM.
Require Import core_lang. Require Import core_lang.
(******************************************************************) (******************************************************************)
......
...@@ -3,6 +3,6 @@ ...@@ -3,6 +3,6 @@
((coq-mode ((coq-mode
(coq-load-path (coq-load-path
(rec "./" "RecDom")))) (rec "./" "ModuRes"))))
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ## ## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ## ## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.4pl3 ## ## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
############################################################################# #############################################################################
# WARNING # WARNING
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
# #
# This Makefile was generated by the command line : # 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 .DEFAULT_GOAL := all
...@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config) ...@@ -39,8 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# # # #
########################## ##########################
COQLIBS?= -R . RecDom COQLIBS?= -R . ModuRes
COQDOCLIBS?=-R . RecDom COQDOCLIBS?=-R . ModuRes
########################## ##########################
# # # #
...@@ -168,14 +168,14 @@ userinstall: ...@@ -168,14 +168,14 @@ userinstall:
install: install:
for i in $(VOFILES); do \ for i in $(VOFILES); do \
install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i`; \ install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i`; \
install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i; \ install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i; \
done done
install-doc: install-doc:
install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
for i in html/*; do \ for i in html/*; do \
install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\ install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
done done
clean: clean:
......
(** In this file, we show how we can use the solution of the recursive (** In this file, we show how we can use the solution of the recursive
domain equations to build a higher-order separation logic *) domain equations to build a higher-order separation logic *)
Require Import RecDom.PreoMet RecDom.MetricRec RecDom.CBUltInst. Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
Require Import RecDom.Finmap RecDom.Constr. Require Import ModuRes.Finmap ModuRes.Constr.
Require Import RecDom.PCM RecDom.UPred RecDom.BI. Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
Module WorldProp (Res : PCM_T). Module WorldProp (Res : PCM_T).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment