...
 
Commits (154)
image: ralfjung/opam-ci:latest
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "10"
GIT_SUBMODULE_STRATEGY: "recursive"
.template: &template
stage: build
tags:
- fp
script:
- git clone https://gitlab.mpi-sws.org/FP/iris-ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
......@@ -29,9 +29,24 @@ variables:
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
VALIDATE: "1"
build-coq.8.9.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.dev"
TIMING_PROJECT: "iris"
TIMING_CONF: "coq-8.9.dev"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.1:
<<: *template
variables:
......@@ -42,6 +57,7 @@ build-coq.8.8.0:
variables:
OPAM_PINS: "coq version 8.8.0"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
TIMING_PROJECT: "iris"
TIMING_CONF: "coq-8.8.0"
tags:
......
......@@ -17,11 +17,31 @@ Changes in and extensions of the theory:
* [#] Add weakest preconditions for total program correctness.
* [#] "(Potentially) stuck" weakest preconditions are no longer considered
experimental.
* [#] The adequacy statement for weakest preconditions now also involves the
final state.
* [#] Add the notion of an "observation" to the language interface, so that
every reduction step can optionally be marked with an event, and an execution
trace has a matching list of events. Change WP so that it is told the entire
future trace of observations from the beginning. Use this in heap_lang to
implement prophecy variables.
* [#] The Löb rule is now a derived rule; it follows from later-intro, later
being contractive and the fact that we can take fixpoints of contractive
functions.
* [#] Add atomic updates and logically atomic triples, including tactic support.
See `heap_lang/lib/increment.v` for an example.
* [#] heap_lang now uses right-to-left evaluation order. This makes it
significantly easier to write specifications of curried functions.
* [#] heap_lang values are now injected in heap_lang expressions via a specific
constructor of the expr inductive type. This simplifies much the tactical
infrastructure around the language. In particular, this allow us to get rid
the reflection mechanism that was needed for proving closedness, atomicity and
"valueness" of a term. The price to pay is the addition of new
"administrative" reductions in the operational semantics of the language.
* [#] Extend the state interpretation with a natural number that keeps track of
the number of forked-off threads, and have a global fixed proposition that
describes the postcondition of each forked-off thread (instead of it being
`True`). Additionally, there is a stronger variant of the adequacy theorem
that allows to make use of the postconditions of the forked-off threads.
Changes in Coq:
......@@ -74,6 +94,11 @@ Changes in Coq:
* `namespaces` has been moved to std++.
* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
* `wp_fork` is now written in curried form.
* `PureExec`/`wp_pure` now supports taking multiple steps at once.
* A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
steps that would require unlocking subterms. Every impure wp_ tactic executes
this tactic before doing anything else.
## Iris 3.1.0 (released 2017-12-19)
......
......@@ -8,15 +8,13 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile awk.Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies
build-dep/opam: opam Makefile
......
......@@ -8,7 +8,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.9" > /dev/null && echo 1)
COQ_BROKEN=
# 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.
......@@ -24,14 +24,14 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
$(if $(COQ_BROKEN), \
true, \
diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
) \
) && \
) \
) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
touch $@
# IRIS COQ DEVELOPMENT
This is the Coq development of the [Iris Project](http://iris-project.org).
This is the Coq development of the [Iris Project](http://iris-project.org),
which includes [MoSeL](http://iris-project.org/mosel/), a general proof mode
for carrying out separation logic proofs in Coq.
A LaTeX version of the core logic definitions and some derived forms is
available in [docs/iris.tex](docs/iris.tex). A compiled PDF version of this
......@@ -12,8 +14,8 @@ document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
This version is known to compile with:
- Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1
- A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
- Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
For a version compatible with Coq 8.6, have a look at the
[iris-3.1 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.1).
......@@ -106,7 +108,7 @@ that should be compatible with this version:
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md).
* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
* Naming conventions are documented at [Naming.md](Naming.md).
### How to update the std++ dependency
......
......@@ -81,19 +81,23 @@ theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/heap_lang/proph_map.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
theories/heap_lang/lib/lock.v
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/coin_flip.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/conditional_counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/proofmode/base.v
......
# awk program that patches the Makefile generated by Coq.
# Detect the name this project will be installed under.
/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
# we can just split the string at '/' here.
split($0, PIECES, /\//);
PROJECT=PIECES[2];
}
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
# This forwards all unchanged lines
1
Subproject commit 1664067bf3f01bd7a081874d26c21e26ad2a3bbf
......@@ -132,7 +132,7 @@ Then, using the standard proof rules for invariants, we show that it satisfies \
Furthermore, assuming the rule for opening invariants without a $\later$, we can prove a slightly weaker version of \ruleref{sprop-agree}, which is sufficient for deriving a contradiction.
% Taking ${\upd}_\bot$ and ${\upd}_\top$ to be the fancy update modalities $\pvs[\emptyset]$
% Taking ${\upd}_0$ and ${\upd}_1$ to be the fancy update modalities $\pvs[\emptyset]$
% and $\pvs[\nat]$, respectively, we can see that Iris
% \emph{almost} satisfies these axioms. First, to implement the tokens,
% we can use the RA with the carrier
......@@ -167,14 +167,14 @@ We can show variants of \ruleref{sprop-agree} and \ruleref{sprop-alloc} for the
\begin{lem}
\label{lem:counterexample-invariants-saved-prop-alloc}
We have
\(\proves {\upd}_\top \Exists \gname. \gname \Mapsto \prop(\gname)\).
\(\proves {\upd}_1 \Exists \gname. \gname \Mapsto \prop(\gname)\).
\end{lem}
\begin{proof}
We have to show the allocation rule \[\proves {\upd}_\top \Exists \gname. \gname \Mapsto \prop.\]
From \ruleref{eq:start-alloc} we have a $\gname$ such that ${\upd}_\bot \ownGhost \gname \starttoken$ holds and hence from \ruleref{eq:update-weaken-mask} we have ${\upd}_\top\ownGhost\gname \starttoken$.
Since we are proving a goal of the form ${\upd}_\top R$ we may assume $\ownGhost \gname \starttoken$.
Thus for any $\prop$ we have ${\upd}_\top\left(\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \prop\right)$.
Again since our goal is still of the form ${\upd}_\top$ we may assume $\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \always \prop$.
We have to show the allocation rule \[\proves {\upd}_1 \Exists \gname. \gname \Mapsto \prop.\]
From \ruleref{eq:start-alloc} we have a $\gname$ such that ${\upd}_0 \ownGhost \gname \starttoken$ holds and hence from \ruleref{eq:update-weaken-mask} we have ${\upd}_1\ownGhost\gname \starttoken$.
Since we are proving a goal of the form ${\upd}_1 R$ we may assume $\ownGhost \gname \starttoken$.
Thus for any $\prop$ we have ${\upd}_1\left(\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \prop\right)$.
Again since our goal is still of the form ${\upd}_1$ we may assume $\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \always \prop$.
The rule \ruleref{eq:inv-alloc} then gives us precisely what we need.
\qed \end{proof}
......@@ -183,18 +183,18 @@ We have
\label{lem:counterexample-invariants-saved-prop-agree}
We have
\(
\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_\top \always \propB
\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB
\)
and thus
\(
\gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_\top \always \prop) \Lra ({\upd}_\top \always \propB).
\gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB).
\)
\end{lem}
\begin{proof}[\lemref{lem:counterexample-invariants-saved-prop-agree}]
\begin{itemize}
\item We first show
\[\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_\top \always \propB.\]
\[\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.\]
We use \ruleref{eq:inv-open} to open the invariant in $\gname \Mapsto \prop$ and consider two cases:
%
\begin{enumerate}
......@@ -206,17 +206,17 @@ and thus
After closing the invariant, we have obtained $\ownGhost \gname \finishtoken$.
Hence, it is sufficient to prove
\[
\ownGhost{\gname}{\finishtoken} * \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_\top \always \propB.\]
\ownGhost{\gname}{\finishtoken} * \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.\]
We proceed by using \ruleref{eq:inv-open} to open the other invariant in $\gname \Mapsto \propB$, and we again consider two cases:
\begin{enumerate}
\item $\ownGhost{\gname}{\starttoken}$ (the invariant is ``uninitialized''): As witnessed by \ruleref{eq:start-not-finished}, this cannot happen, so we derive a contradiction.
Notice that this is a key point of the proof: because the two invariants ($\gname \Mapsto \prop$ and $\gname \Mapsto \propB$) \emph{share} the ghost name $\gname$, initializing one of them is enough to show that the other one has been initialized.
Essentially, this is an indirect way of saying that really, we have been opening the same invariant two times.
\item $\ownGhost{\gname}{\finishtoken} * \always \propB$ (the invariant is ``initialized''):
Since $\always \propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\upd}_\top \always \propB$.
Since $\always \propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\upd}_1 \always \propB$.
\end{enumerate}
\item By applying the above twice, we easily obtain
\[ \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_\top \always \prop) \Lra ({\upd}_\top \always \propB) \]
\[ \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB) \]
\end{itemize}
\qed \end{proof}
% When allocating $\gname \Mapsto \prop(\gname)$ in \lemref{lem:counterexample-invariants-saved-prop-alloc}, we will start off in ``state'' $\ownGhost \gname \starttoken$, and once we have $P$ in \lemref{lem:counterexample-invariants-saved-prop-agree} we use \ruleref{eq:start-finish} to transition to $\ownGhost\gname \finishtoken$, obtaining ourselves a copy of said token.
......@@ -224,9 +224,9 @@ and thus
Intuitively, \lemref{lem:counterexample-invariants-saved-prop-agree} shows that we can ``convert'' a proof from $\prop$ to $\propB$.
We are now in a position to replay the counterexample from \Sref{sec:saved-prop-no-later}.
The only difference is that because \lemref{lem:counterexample-invariants-saved-prop-agree} is slightly weaker than the rule \ruleref{sprop-agree} of \thmref{thm:counterexample-1}, we need to use ${\upd}_\top \FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
The only difference is that because \lemref{lem:counterexample-invariants-saved-prop-agree} is slightly weaker than the rule \ruleref{sprop-agree} of \thmref{thm:counterexample-1}, we need to use ${\upd}_1 \FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
we let \(
A(\gname) \eqdef \Exists \prop : \Prop. \always (\prop \Ra {\upd}_\top \FALSE) \land \gname \Mapsto \prop\)
A(\gname) \eqdef \Exists \prop : \Prop. \always (\prop \Ra {\upd}_1 \FALSE) \land \gname \Mapsto \prop\)
and replay the proof that we have presented above.
%TODO: What about executing a view shift under a later?
......
......@@ -272,7 +272,7 @@ The signature can of course state arbitrary additional properties of $\pred$, as
The adequacy statement now reads as follows:
\begin{align*}
&\All \mask, \expr, \val, \state.
\\&( \TRUE \proves {\upd}_\mask \Exists \stateinterp. \stateinterp(\state) * \wpre[\stateinterp]{\expr}[\stuckness;\mask]{x.\; \pred(x)}) \Ra
\\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp. \stateinterp(\state) * \wpre[\stateinterp]{\expr}[\stuckness;\mask]{x.\; \pred(x)}) \Ra
\\&\expr, \state \vDash_\stuckness V
\end{align*}
Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
......
......@@ -10,6 +10,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-06-30.1.1a21e908") | (= "dev") }
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-11-12.0.1a00ee7e") | (= "dev") }
]
......@@ -18,7 +18,7 @@ End tests.
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
exists R, @Reflexive Prop R /\ R = iff.
R, @Reflexive Prop R R = iff.
Proof.
eexists. split.
- apply _.
......
......@@ -50,6 +50,20 @@
--------------------------------------∗
True
"wp_nonclosed_value"
: string
The command has indeed failed with message:
Ltac call to "wp_pure (open_constr)" failed.
Tactic failure: wp_pure: cannot find ?y in (Var "x") or
?y is not a redex.
1 subgoal
Σ : gFunctors
H : heapG Σ
============================
--------------------------------------∗
WP "x" {{ _, True }}
1 subgoal
Σ : gFunctors
......@@ -104,4 +118,4 @@
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
......@@ -27,8 +27,8 @@ Section tests.
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Proof.
iIntros "". rewrite /heap_e. Show.
wp_alloc l as "?". wp_let. wp_load. Show.
wp_op. wp_store. by wp_load.
wp_alloc l as "?". wp_load. Show.
wp_store. by wp_load.
Qed.
Definition heap_e2 : expr :=
......@@ -39,8 +39,8 @@ Section tests.
Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
Proof.
iIntros "". rewrite /heap_e2.
wp_alloc l as "Hl". Show. wp_let. wp_alloc l'. wp_let.
wp_load. wp_op. wp_store. wp_load. done.
wp_alloc l as "Hl". Show. wp_alloc l'.
wp_load. wp_store. wp_load. done.
Qed.
Definition heap_e3 : expr :=
......@@ -60,17 +60,17 @@ Section tests.
Lemma heap_e4_spec : WP heap_e4 [{ v, v = #1 }]%I.
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
wp_alloc l''. wp_let. by repeat wp_load.
rewrite /heap_e4. wp_alloc l. wp_alloc l'.
wp_alloc l''. by repeat wp_load.
Qed.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
rewrite /heap_e5. wp_alloc l. wp_alloc l'.
wp_load. wp_faa. do 2 wp_load. by wp_pures.
Qed.
Definition heap_e6 : val := λ: "v", "v" = "v".
......@@ -92,8 +92,7 @@ Section tests.
Proof.
iIntros (Hn) "HΦ".
iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
wp_rec. wp_let. wp_op. wp_let.
wp_op; case_bool_decide; wp_if.
wp_rec. wp_pures. case_bool_decide; wp_if.
- iApply ("IH" with "[%] [%] HΦ"); omega.
- by assert (n1' = n2 - 1) as -> by omega.
Qed.
......@@ -101,16 +100,15 @@ Section tests.
Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
Proof.
iIntros "HΦ". wp_lam.
wp_op. case_bool_decide; wp_if.
- wp_op. wp_op.
wp_apply FindPred_spec; first omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
wp_op. case_bool_decide.
- wp_apply FindPred_spec; first omega. wp_pures.
by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- wp_apply FindPred_spec; eauto with omega.
Qed.
Lemma Pred_user E :
WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
Lemma wp_apply_evar e P :
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
......@@ -118,7 +116,7 @@ Section tests.
Lemma wp_cas l v :
val_is_unboxed v
l v - WP CAS #l v v {{ _, True }}.
l v - WP cas: #l, v, v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
......@@ -131,6 +129,11 @@ Section tests.
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "_". Show. done. Qed.
Check "wp_nonclosed_value".
Lemma wp_nonclosed_value :
WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
End tests.
Section printing_tests.
......@@ -183,11 +186,11 @@ Section error_tests.
Check "not_cas".
Lemma not_cas :
(WP #() {{ _, True }})%I.
(WP #() #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Abort.
End error_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
......@@ -82,14 +82,14 @@ Section list_reverse.
destruct xs as [|x xs]; iSimplifyEq.
- (* nil *) by wp_match.
- (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
wp_match. wp_load. wp_load. wp_store.
rewrite reverse_cons -assoc.
iApply ("IH" $! hd' (InjRV #l) xs (x :: ys) with "Hxs [Hx Hys]").
iExists l, acc; by iFrame.
Qed.
Lemma rev_ht hd xs :
{{ is_list hd xs }} rev hd NONE {{ w, is_list w (reverse xs) }}.
{{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
Proof.
iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
......@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0.
Definition incr : val :=
rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
if: cas: "l", "n", #1 + "n" then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** The CMRA we need. *)
......@@ -204,7 +204,7 @@ Section counter_proof.
Lemma newcounter_spec :
{{ True }} newcounter #() {{ v, l, v = #l C l 0 }}.
Proof.
iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
set (N:= nroot .@ "counter").
......@@ -222,7 +222,7 @@ Section counter_proof.
iDestruct 1 as (c) "[Hl Hγ]".
wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_bind (CAS _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
wp_bind (cas: _, _, _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c') ">[Hl Hγ]".
destruct (decide (c' = c)) as [->|].
- iCombine "Hγ" "Hγf" as "Hγ".
......@@ -242,7 +242,7 @@ Section counter_proof.
{{ C l n }} read #l {{ v, m : nat, v = #m n m C l m }}.
Proof.
iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
iDestruct (own_valid γ (Frag n Auth c) with "[-]") as % ?%auth_frag_valid.
{ iApply own_op. by iFrame. }
......
......@@ -23,11 +23,11 @@
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w ys -∗ Φ w
--------------------------------------∗
WP match: InjL #() with
WP match: InjLV #() with
InjL <> => acc
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; (rev "tmp2") (InjL #())
"l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
end [{ v, Φ v }]
......@@ -36,14 +36,14 @@ Proof.
iSimplifyEq; wp_rec; wp_let.
- Show. wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
wp_load. wp_load. wp_store.
iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. }
iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Qed.
Lemma rev_wp hd xs :
[[{ is_list hd xs }]] rev hd NONE [[{ w, RET w; is_list w (reverse xs) }]].
[[{ is_list hd xs }]] rev hd NONEV [[{ w, RET w; is_list w (reverse xs) }]].
Proof.
iIntros (Φ) "Hxs HΦ".
iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
......
......@@ -35,7 +35,7 @@
"Hγ" : own γ (Shot m')
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
∗ WP match: InjR #m' with
∗ WP match: InjRV #m' with
InjL <> => assert: #false
| InjR "m" => assert: #m = "m"
end {{ _, True }}
......
......@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* tryset *) (λ: "n",
CAS "x" NONE (SOME "n")),
cas: "x", NONE, SOME "n"),
(* check *) (λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
......@@ -43,12 +43,12 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc Pending) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_let.
wp_pures. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_pures.
iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ iMod (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). }
......@@ -56,7 +56,7 @@ Proof.
iModIntro. iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iSplitL; last eauto.
rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_seq. wp_bind (! _)%E.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
iAssert ( v, l v ((v = NONEV own γ Pending)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
......@@ -70,18 +70,17 @@ Proof.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_let. iIntros "!#". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_bind (! _)%E.
iModIntro. wp_pures. iIntros "!#". wp_lam.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
subst; wp_match; [done|].
wp_bind (! _)%E.
iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
{ by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
wp_load. Show.
iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
iModIntro. iSplitL "Hl".
{ iNext; iRight; by eauto. }
wp_match. iApply wp_assert.
wp_op. by case_bool_decide.
wp_apply wp_assert. wp_pures. by case_bool_decide.
Qed.
Lemma ht_one_shot (Φ : val iProp Σ) :
......@@ -92,8 +91,7 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
}}.
Proof.
iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
- iIntros (n) "!# _". wp_proj. iApply "Hf1".
- iIntros "!# _". wp_proj.
iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
- iIntros (n) "!# _". wp_apply "Hf1".
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
......@@ -454,14 +454,19 @@ Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
failed.
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
failed.
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
Tactic failure: iRename: "H" not fresh.
"iRevert_fail"
: string
......@@ -474,15 +479,23 @@ Tactic failure: iElaborateSelPat: "H" not found.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>", last call failed.
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
"iApply_fail"
......@@ -493,8 +506,7 @@ In nested Ltac calls to "iApply (open_constr)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
"goal_tac" (bound to
fun _ => <ssreflect_plugin::ssrtclseq@0> spec_tac ltac:(()) ; last tac Htmp) and
"<ssreflect_plugin::ssrtclseq@0> spec_tac ltac:(()) ; last tac Htmp", last
call failed.
"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: cannot apply P.
From iris.proofmode Require Import tactics intro_patterns.
From stdpp Require Import gmap hlist.
Set Default Proof Using "Type".
Section tests.
......@@ -267,6 +266,15 @@ Proof.
rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega.
Qed.
Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat nat PROP) y :
([ map] x i m, Φ y x) - ([ map] x i m, emp Φ y x).
Proof.
iIntros "Hm". iInduction m as [|i x m] "IH" using map_ind forall(y).
- by rewrite !big_sepM_empty.
- rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
by iApply "IH".
Qed.
Lemma test_iIntros_start_proof :
(True : PROP)%I.
Proof.
......@@ -578,6 +586,12 @@ Proof.
iIntros "?". iExists _. iApply modal_if_lemma2. done.
Qed.
Lemma test_iDestruct_clear P Q R :
P - (Q R) - True.
Proof.
iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
Qed.
End tests.
(** Test specifically if certain things print correctly. *)
......
......@@ -107,6 +107,8 @@
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
"test_iInv_12"
: string
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) in (tactic)" and
......@@ -125,6 +127,8 @@ In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
failed.
Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
: string
1 subgoal
Σ : gFunctors
......@@ -139,6 +143,8 @@ Tactic failure: iInv: invariant "H2" not found.
--------------------------------------∗
|={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
"test_iInv_with_close"
: string
1 subgoal
Σ : gFunctors
......
......@@ -202,6 +202,7 @@ Section iris_tests.
Qed.
(* error messages *)
Check "test_iInv_12".
Lemma test_iInv_12 N P: inv N (<pers> P) ={}= True.
Proof.
iIntros "H".
......@@ -229,6 +230,7 @@ Section monpred_tests.
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
Check "test_iInv".
Lemma test_iInv N E 𝓟 :
N E
inv N 𝓟⎤ @{monPredI} |={E}=> emp.
......@@ -238,6 +240,7 @@ Section monpred_tests.
iFrame "HP". auto.
Qed.
Check "test_iInv_with_close".
Lemma test_iInv_with_close N E 𝓟 :
N E
inv N 𝓟⎤ @{monPredI} |={E}=> emp.
......
......@@ -42,13 +42,11 @@ Proof.
iIntros (Φ) "[Hl Ht] HΦ".
iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
wp_load. wp_store.
by iApply ("HΦ" with "[$Hl]").
- iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load.
wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
iExists ll, lr, vl, vr. by iFrame.
......@@ -58,8 +56,8 @@ Lemma sum_wp `{!heapG Σ} v t :
[[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
Proof.
iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
wp_let. wp_alloc l as "Hl". wp_let.
wp_lam. wp_alloc l as "Hl".
wp_apply (sum_loop_wp with "[$Hl $Ht]").
rewrite Z.add_0_r.
iIntros "[Hl Ht]". wp_seq. wp_load. by iApply "HΦ".
iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
Qed.
......@@ -241,6 +241,18 @@ Section gmap.
([^o map] ky <[i:=x]> m, <[i:=P]> f k) (P `o` [^o map] ky m, f k).
Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
Lemma big_opM_union f m1 m2 :
m1 ## m2
([^o map] ky m1 m2, f k y) ([^o map] ky m1, f k y) `o` ([^o map] ky m2, f k y).
Proof.
intros. induction m1 as [|i x m ? IH] using map_ind.
{ by rewrite big_opM_empty !left_id. }
decompose_map_disjoint.
rewrite -insert_union_l !big_opM_insert //;
last by apply lookup_union_None.
rewrite -assoc IH //.
Qed.
Lemma big_opM_opM f g m :
([^o map] kx m, f k x `o` g k x)
([^o map] kx m, f k x) `o` ([^o map] kx m, g k x).
......
......@@ -1395,6 +1395,10 @@ Section option.
by eapply (cmra_validN_le n); last lia.
- done.
Qed.
Global Instance option_cancelable (ma : option A) :
( a : A, IdFree a) ( a : A, Cancelable a) Cancelable ma.
Proof. destruct ma; apply _. Qed.
End option.
Arguments optionR : clear implicits.
......@@ -1426,6 +1430,14 @@ Section option_prod.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
End option_prod.
Lemma option_fmap_mono {A B : cmraT} (f : A B) ma mb :
Proper (() ==> ()) f
( a b, a b f a f b)
ma mb f <$> ma f <$> mb.
Proof.
intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.
Instance option_fmap_cmra_morphism {A B : cmraT} (f: A B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A option B).
Proof.
......
......@@ -21,7 +21,7 @@ Notation map := (cFunctor_map F).
Fixpoint A (k : nat) : ofeT :=
match k with 0 => unitC | S k => F (A k) end.
Local Instance: k, Cofe (A k).
Proof using Fcofe. induction 0; apply _. Defined.
Proof using Fcofe. induction k; apply _. Defined.
Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
......
......@@ -105,4 +105,9 @@ Section frac_auth.
Proof.
intros. by apply auth_update, option_local_update, prod_local_update_2.
Qed.
Lemma frac_auth_update_1 a b a' : a' ! a ! b ~~> ! a' ! a'.
Proof.
intros. by apply auth_update, option_local_update, exclusive_local_update.
Qed.
End frac_auth.
......@@ -93,6 +93,9 @@ Proof.
Qed.
Global Instance gmap_singleton_discrete i x :
Discrete x Discrete ({[ i := x ]} : gmap K A) := _.
Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
End cofe.
Arguments gmapC _ {_ _} _.
......@@ -285,6 +288,16 @@ Proof.
- by rewrite lookup_singleton_ne // !(left_id None _).
Qed.
Global Instance gmap_cancelable (m : gmap K A) :
( x : A, IdFree x) ( x : A, Cancelable x) Cancelable m.
Proof.
intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
Qed.
Lemma insert_op m1 m2 i x y :
<[i:=x y]>(m1 m2) = <[i:=x]>m1 <[i:=y]>m2.
Proof. by rewrite (insert_merge () m1 m2 i (x y) x y). Qed.
Lemma insert_updateP (P : A Prop) (Q : gmap K A Prop) m i x :
x ~~>: P ( y, P y Q (<[i:=y]>m)) <[i:=x]>m ~~>: Q.
Proof.
......@@ -461,8 +474,39 @@ Proof.
apply (delete_local_update_cancelable m _ i (Some x));
[done|by rewrite lookup_singleton].
Qed.
Lemma gmap_fmap_mono {B : cmraT} (f : A B) m1 m2 :
Proper (() ==> ()) f
( x y, x y f x f y) m1 m2 fmap f m1 fmap f m2.
Proof.
intros ??. rewrite !lookup_included=> Hm i.
rewrite !lookup_fmap. by apply option_fmap_mono.
Qed.
End properties.
Section unital_properties.
Context `{Countable K} {A : ucmraT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
Lemma insert_alloc_local_update m1 m2 i x x' y' :
m1 !! i = Some x m2 !! i = None
(x, ε) ~l~> (x', y')
(m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
Proof.
intros Hi1 Hi2 Hup. apply local_update_unital=> n mf Hm1v Hm.
assert (mf !! i {n} Some x) as Hif.
{ move: (Hm i). by rewrite lookup_op Hi1 Hi2 left_id. }
destruct (Hup n (mf !! i)) as [Hx'v Hx'eq].
{ move: (Hm1v i). by rewrite Hi1. }
{ by rewrite Hif -(inj_iff Some) -Some_op_opM -Some_op left_id. }
split.
- by apply insert_validN.
- simpl in Hx'eq. by rewrite -(insert_idN n mf i x) // -insert_op -Hm Hx'eq Hif.
Qed.
End unital_properties.
(** Functor *)
Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
......
......@@ -31,7 +31,8 @@ Inductive step : relation (state sts * tokens sts) :=
tok s1 T1 tok s2 T2 step (s1,T1) (s2,T2).
Notation steps := (rtc step).
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
(* Probably equivalent definition: (\mathcal{L}(s') ## T) ∧ s \rightarrow s' *)
(* Possible alternative definition: (tok s2) ## T) ∧ s \rightarrow s'.
This is not equivalent, but it might be good enough? *)
| Frame_step T1 T2 :
T1 ## tok s1 T step (s1,T1) (s2,T2) frame_step T s1 s2.
Notation frame_steps T := (rtc (frame_step T)).
......@@ -63,7 +64,7 @@ Qed.
Global Instance frame_step_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /collection_equiv_spec [??]; split; by apply frame_step_mono. Qed.
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper (() ==> () ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Global Instance up_preserving : Proper ((=) ==> flip () ==> ()) up.
......
......@@ -144,13 +144,13 @@ Proof. exact: bupd_plainly. Qed.
(** extra BI instances *)
Global Instance uPred_affine : BiAffine (uPredI M) | 0.
Proof. intros P Q. exact: pure_intro. Qed.
Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
Hint Immediate uPred_affine.
Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredSI M).
Proof. exact: @plainly_exist_1. Qed.
(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
......
From iris.base_logic.lib Require Export own.
From stdpp Require Export coPset.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Export invG.
......@@ -40,13 +41,56 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed
Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
Proof.
split.
- iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
iAssert ( P)%I as "#HP".
{ by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
iMod "HP". iFrame. auto.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
iAssert ( P)%I with "[-]" as "#$"; last by iFrame.
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.
\ No newline at end of file
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
iAssert ( P)%I as "#>HP".
{ by iMod ("H" with "[$]") as "(_ & _ & HP)". }
by iFrame.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
iAssert ( P)%I as "#>HP".
{ by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
by iFrame.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
iAssert ( P)%I as "#HP".
{ iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
iFrame. iIntros "!> !> !>". by iMod "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
iAssert ( x : A, Φ x)%I as "#>HP".
{ iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
by iFrame.
Qed.
Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
( `{Hinv: invG Σ}, (|={,E}=> P)%I) ( P)%I.
Proof.
iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
iPoseProof (Hfupd Hinv) as "H".
rewrite uPred_fupd_eq /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
Lemma step_fupdN_soundness `{invPreG Σ} φ n :
( `{Hinv: invG Σ}, (|={,}=>^n |={,}=> φ : iProp Σ)%I)
φ.
Proof.
intros Hiter.
apply (soundness (M:=iResUR Σ) _ (S (S n))); simpl.
apply (fupd_plain_soundness _)=> Hinv.
iPoseProof (Hiter Hinv) as "H". clear Hiter.
destruct n as [|n].
- iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
- iDestruct (step_fupdN_wand _ _ _ _ (|={}=> ⌜φ⌝)%I with "H []") as "H'".
{ by iApply fupd_plain_mask_empty. }
rewrite -step_fupdN_S_fupd.
iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
rewrite -later_laterN laterN_later.
iNext. by iMod "Hφ".
Qed.
Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
( `{Hinv: invG Σ}, (|={,}=>^n φ : iProp Σ)%I)
φ.
Proof.
iIntros (Hiter). eapply (step_fupdN_soundness _ n).
iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
Qed.
......@@ -4,6 +4,9 @@ From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(** All definitions in this file are internal to [fancy_updates] with the
exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
Module invG.
Class invG (Σ : gFunctors) : Set := WsatG {
inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
......@@ -13,6 +16,21 @@ Module invG.
enabled_name : gname;
disabled_name : gname;
}.
Definition invΣ : gFunctors :=
#[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
GFunctor coPset_disjUR;
GFunctor (gset_disjUR positive)].
Class invPreG (Σ : gFunctors) : Set := WsatPreG {
inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
enabled_inPreG :> inG Σ coPset_disjR;
disabled_inPreG :> inG Σ (gset_disjR positive);
}.
Instance subG_invΣ {Σ} : subG invΣ Σ invPreG Σ.
Proof. solve_inG. Qed.
End invG.
Import invG.
......@@ -175,3 +193,15 @@ Proof.
iFrame "HI". by iRight.
Qed.
End wsat.
(* Allocation of an initial world *)
Lemma wsat_alloc `{invPreG Σ} : (|==> _ : invG Σ, wsat ownE )%I.
Proof.
iIntros.
iMod (own_alloc ( ( : gmap _ _))) as (γI) "HI"; first done.
iMod (own_alloc (CoPset )) as (γE) "HE"; first done.
iMod (own_alloc (GSet )) as (γD) "HD"; first done.
iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
rewrite /wsat /ownE -lock; iFrame.
iExists . rewrite fmap_empty big_opM_empty. by iFrame.
Qed.
......@@ -49,6 +49,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scop
(** * Properties *)
Section bi_big_op.
Context {PROP : bi}.
Implicit Types P Q : PROP.
Implicit Types Ps Qs : list PROP.
Implicit Types A : Type.
......@@ -91,7 +92,7 @@ Section sep_list.
(big_opL (@bi_sep PROP) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
Global Instance big_sepL_id_mono' :
Proper (Forall2 () ==> ()) (big_opL (@bi_sep M) (λ _ P, P)).
Proper (Forall2 () ==> ()) (big_opL (@bi_sep PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_sepL_emp l : ([ list] ky l, emp) ⊣⊢@{PROP} emp.
......@@ -185,6 +186,10 @@ Section sep_list.
rewrite -decide_emp. by repeat case_decide.
Qed.
Lemma big_sepL_replicate l P :
[] replicate (length l) P ⊣⊢ [ list] y l, P.
Proof. induction l as [|x l]=> //=; by f_equiv. Qed.
Global Instance big_sepL_nil_persistent Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.