Commit 68f44f23 authored by Ralf Jung's avatar Ralf Jung

Merge remote-tracking branch 'origin/master' into ci/ralf/reftest

parents b8973675 b036013f
...@@ -28,16 +28,15 @@ build-dep: build-dep/opam phony ...@@ -28,16 +28,15 @@ build-dep: build-dep/opam phony
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements. @# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as @# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything. @# dependencies, but does not actually install anything itself.
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep @echo "# Pinning build-dep package." && \
@# package changed. if opam --version | grep "^1\." -q; then \
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \ BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \ opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \ opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
((! opam --version | grep "^1\." > /dev/null) || ( \ else \
echo "# Reinstalling build-dep package." && \ opam install $(OPAMFLAGS) build-dep/; \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \ fi
))
# Some files that do *not* need to be forwarded to Makefile.coq # Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ; Makefile: ;
......
...@@ -11,11 +11,6 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode ...@@ -11,11 +11,6 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1) COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o) COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
# Oh Unix...
REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
tests/.coqdeps.d: $(TESTFILES) tests/.coqdeps.d: $(TESTFILES)
$(SHOW)'COQDEP TESTFILES' $(SHOW)'COQDEP TESTFILES'
$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok) $(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
...@@ -28,13 +23,12 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) ...@@ -28,13 +23,12 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
else \ else \
REF="tests/$$TEST.ref"; \ REF="tests/$$TEST.ref"; \
fi && \ fi && \
echo $(if $(MAKE_REF),"COQTEST [ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \ echo $(if $(MAKE_REF),"COQTEST [make ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \
TMPFILE="$$(mktemp)" && \ TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \ $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \ $(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "$$REF", \ mv "$$TMPFILE" "$$REF", \
$(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE.filtered") \ $(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE") \
) && \ ) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \ rm -f "$$TMPFILE" && \
touch $@ touch $@
...@@ -105,8 +105,6 @@ that should be compatible with this version: ...@@ -105,8 +105,6 @@ that should be compatible with this version:
formalization of the core Rust type system. formalization of the core Rust type system.
* [iGPS](https://gitlab.mpi-sws.org/FP/sra-gps/tree/gen_proofmode_WIP) is a * [iGPS](https://gitlab.mpi-sws.org/FP/sra-gps/tree/gen_proofmode_WIP) is a
logic for release-acquire memory. logic for release-acquire memory.
* [Iris Atomic](https://gitlab.mpi-sws.org/iris/atomic) is an experimental
formalization of logically atomic triples in Iris.
* [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic * [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic
built on top of Iris for precise reasoning about resources (such as making built on top of Iris for precise reasoning about resources (such as making
sure there are no memory leaks). sure there are no memory leaks).
......
...@@ -11,5 +11,5 @@ install: [make "install"] ...@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [ depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") } "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-01-24.2.b72e1fa8") | (= "dev") } "coq-stdpp" { (= "dev.2019-01-25.1.26088f98") | (= "dev") }
] ]
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
aheap : atomic_heap Σ
Q : iProp Σ
l : loc
v : val
============================
"Hl" : l ↦ v
--------------------------------------∗
AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
1 subgoal 1 subgoal
Σ : gFunctors Σ : gFunctors
...@@ -10,11 +24,9 @@ ...@@ -10,11 +24,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
P : val → iProp Σ P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -23,14 +35,12 @@ ...@@ -23,14 +35,12 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
P : val → iProp Σ P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << ∀ x : val, P x _ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅ ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -46,11 +56,9 @@ ...@@ -46,11 +56,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -59,14 +67,11 @@ ...@@ -59,14 +67,11 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << ∀ x : val, l ↦ x _ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
<< l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅ @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
<< l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -82,11 +87,9 @@ ...@@ -82,11 +87,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -95,14 +98,12 @@ ...@@ -95,14 +98,12 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << l ↦ #() _ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ ABORT AU << l ↦ #() >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -118,11 +119,9 @@ ...@@ -118,11 +119,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -131,13 +130,11 @@ ...@@ -131,13 +130,11 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << l ↦ #() _ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -155,12 +152,10 @@ ...@@ -155,12 +152,10 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅ "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -178,12 +173,10 @@ ...@@ -178,12 +173,10 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -202,14 +195,12 @@ ...@@ -202,14 +195,12 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅ _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy << ∃ yyyy : val, l ↦ yyyy
∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Q -∗ Φ #() >> COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -227,12 +218,10 @@ ...@@ -227,12 +218,10 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅ "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >> << l ↦ x, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -252,12 +241,10 @@ ...@@ -252,12 +241,10 @@
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
x : val x : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅ "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -277,12 +264,10 @@ ...@@ -277,12 +264,10 @@
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
x : val x : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅ "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ #(), COMM Q -∗ Φ #() >> << l ↦ #(), COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -302,12 +287,10 @@ ...@@ -302,12 +287,10 @@
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
xx, yyyy : val xx, yyyy : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >> @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -328,31 +311,16 @@ ...@@ -328,31 +311,16 @@
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
xx, yyyy : val xx, yyyy : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅ "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Q -∗ Φ #() >> COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
"Prettification" "Prettification"
: string : string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
--------------------------------------∗
∀ Φ : language.val heap_lang → iProp Σ, AU << ∀
x : val,
P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
-∗ WP ! #0 {{ v, Φ v }}
1 subgoal 1 subgoal
Σ : gFunctors Σ : gFunctors
......
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
aheap : atomic_heap Σ
Q : iProp Σ
l : loc
v : val
============================
"Hl" : l ↦ v
--------------------------------------∗
AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
<< l ↦{q} v0, COMM Q -∗ Q >>
1 subgoal 1 subgoal
Σ : gFunctors Σ : gFunctors
...@@ -10,11 +24,9 @@ ...@@ -10,11 +24,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
P : val → iProp Σ P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -23,14 +35,12 @@ ...@@ -23,14 +35,12 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
P : val → iProp Σ P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << ∀ x : val, P x _ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅ ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -46,11 +56,9 @@ ...@@ -46,11 +56,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -59,14 +67,11 @@ ...@@ -59,14 +67,11 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << ∀ x : val, l ↦ x _ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
<< l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅ @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
<< l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -82,11 +87,9 @@ ...@@ -82,11 +87,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -95,14 +98,12 @@ ...@@ -95,14 +98,12 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << l ↦ #() _ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ ABORT AU << l ↦ #() >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -118,11 +119,9 @@ ...@@ -118,11 +119,9 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -131,13 +130,11 @@ ...@@ -131,13 +130,11 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
_ : AACC << l ↦ #() _ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}
...@@ -155,12 +152,10 @@ ...@@ -155,12 +152,10 @@
Σ : gFunctors Σ : gFunctors
heapG0 : heapG Σ heapG0 : heapG Σ
l : loc l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅ "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗ --------------------------------------∗
WP code {{ v, Φ v }} WP code {{ v, Φ v }}