Proved htUnsafe.

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris_core.v iris_vs.v iris_wp.v lang.v masks.v world_prop.v -o Makefile 
+# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris_core.v iris_unsafe.v iris_vs.v iris_wp.v lang.v masks.v world_prop.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -50,14 +50,14 @@ COQDOCLIBS?=-R lib/ModuRes ModuRes
 
 
 OPT?=
-COQDEP?=$(COQBIN)coqdep -c
+COQDEP?="$(COQBIN)coqdep" -c
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
 COQCHKFLAGS?=-silent -o
 COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(COQBIN)coqc
-GALLINA?=$(COQBIN)gallina
-COQDOC?=$(COQBIN)coqdoc
-COQCHK?=$(COQBIN)coqchk
+COQC?="$(COQBIN)coqc"
+GALLINA?="$(COQBIN)gallina"
+COQDOC?="$(COQBIN)coqdoc"
+COQCHK?="$(COQBIN)coqchk"
 
 ##################
 #                #
@@ -66,12 +66,12 @@ COQCHK?=$(COQBIN)coqchk
 ##################
 
 ifdef USERINSTALL
-XDG_DATA_HOME?=$(HOME)/.local/share
+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
+COQLIBINSTALL="${COQLIB}user-contrib"
+COQDOCINSTALL="${DOCDIR}user-contrib"
 endif
 
 ######################
@@ -82,6 +82,7 @@ endif
 
 VFILES:=core_lang.v\
   iris_core.v\
+  iris_unsafe.v\
   iris_vs.v\
   iris_wp.v\
   lang.v\
@@ -175,12 +176,12 @@ install:
 	for i in $(VOFILESINC); do \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/`basename $$i`; \
 	done
-	(cd ./lib/ModuRes; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/ModuRes install)
+	+cd ./lib/ModuRes && $(MAKE) DSTROOT="$(DSTROOT)" INSTALLDEFAULTROOT="$(INSTALLDEFAULTROOT)/./lib/ModuRes" install
 
 install-doc:
-	install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
+	install -d "$(DSTROOT)"$(COQDOCINSTALL)/ModuRes/html
 	for i in html/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
+	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/ModuRes/$$i;\
 	done
 
 clean:
@@ -194,13 +195,13 @@ archclean:
 	(cd ./lib/ModuRes ; $(MAKE) archclean)
 
 printenv:
-	@$(COQBIN)coqtop -config
-	@echo CAMLC =	$(CAMLC)
-	@echo CAMLOPTC =	$(CAMLOPTC)
-	@echo PP =	$(PP)
-	@echo COQFLAGS =	$(COQFLAGS)
-	@echo COQLIBINSTALL =	$(COQLIBINSTALL)
-	@echo COQDOCINSTALL =	$(COQDOCINSTALL)
+	@"$(COQBIN)coqtop" -config
+	@echo 'CAMLC =	$(CAMLC)'
+	@echo 'CAMLOPTC =	$(CAMLOPTC)'
+	@echo 'PP =	$(PP)'
+	@echo 'COQFLAGS =	$(COQFLAGS)'
+	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
 
 ###################
 #                 #
@@ -227,7 +228,7 @@ printenv:
 	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
 
 %.g.html: %.v %.glob
-	$(COQDOC)$(COQDOCFLAGS)  -html -g $< -o $@
+	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
 
 %.v.d: %.v
 	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )

README.txt

@@ -63,6 +63,8 @@ CONTENTS
   * iris_wp.v defines weakest preconditions and proves the rules for
     Hoare triples
   
+  * iris_unsafe.v proves rules for unsafe Hoare triples
+
   The development uses ModuRes, a Coq library 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

iris_unsafe.v

+Set Automatic Coercions Import.
+Require Import ssreflect ssrfun ssrbool eqtype seq fintype.
+Require Import core_lang masks iris_wp.
+Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+(******************************************************************)
+(** * Rules for unsafe triples **)
+(******************************************************************)
+
+Module RobustSafety (RL : PCM_T) (C : CORE_LANG).
+
+  Module Export Iris := IrisWP RL C.
+  Local Open Scope iris_scope.
+  Local Open Scope mask_scope.
+  Local Open Scope pcm_scope.
+  Local Open Scope bi_scope.
+  Local Open Scope lang_scope.
+
+  Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : value -n> Props) (r : res) (w : Wld).
+
+  Lemma wpUnsafe m e φ : wp true m e φ ⊑ wp false m e φ.
+  Proof.
+    move=> w n r He; move: n e φ w r He; elim/wf_nat_ind; move=> n IH e φ w r /unfold_wp He.
+    rewrite unfold_wp; move=> w' k s rf mf σ HSw HLt HD Hw.
+    move: {IH} (IH _ HLt) => IH.
+    move: {He HSw HLt HD Hw} (He _ _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
+    split; [done | clear HV; split; [clear HF | split; [clear HS | done] ] ].
+    - move=> σ' ei ei' K HK Hstep.
+      move: {HS HK Hstep} (HS _ _ _ _ HK Hstep) => [w'' [r' [s' [HSw' [He' Hw'] ] ] ] ].
+      exists w'' r' s'; split; [done | split; [exact: IH | done] ].
+    move=> e' K HK.
+    move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [s' [HSw' [Hk [He' Hw'] ] ] ] ] ] ].
+    exists w'' rfk rret s'; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
+  Qed.
+
+  Lemma htUnsafe m P e φ : ht true m P e φ ⊑ ht false m P e φ.
+  Proof.
+    move=> w n rz He w' HSw n' r HLe Hr HP.
+    move: {He P w n rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
+    exact: wpUnsafe.
+  Qed.
+
+End RobustSafety.