...
 
Commits (316)
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
.Makefile.coq.d
*.glob
*.cache
*.aux
......
......@@ -18,8 +18,8 @@ variables:
paths:
- opamroot/
only:
- master
- /^ci/
- master@iris/iris
- /^ci/@iris/iris
except:
- triggers
- schedules
......@@ -30,38 +30,32 @@ variables:
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1"
build-coq.8.10.dev:
build-coq.8.11.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.dev"
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.1"
OPAM_PINS: "coq version 8.11.dev"
CI_COQCHK: "1"
build-coq.8.9.0:
build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PINS: "coq version 8.10.2"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
TIMING_CONF: "coq-8.9.0"
TIMING_CONF: "coq-8.10.2"
tags:
- fp-timing
build-coq.8.8.2:
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
OPAM_PINS: "coq version 8.9.1"
build-coq.8.7.2:
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
OPAM_PINS: "coq version 8.8.2"
This diff is collapsed.
# Contributing to the Iris Coq Development
Here you can find some how-tos for various thing sthat might come up when doing
Iris development.
Iris development. This is for contributing to Iris itself; see
[the README](README.md#further-resources) for resources helpful for all Iris
users.
## How to submit a merge request
......@@ -24,6 +26,8 @@ a feature branch instead.
* Wait for CI to publish a new std++ version on the opam archive, then run
`opam update iris-dev`.
* In Iris, change the `opam` file to depend on the new version.
(In case you do not use opam yourself, you can see recently published versions
[in this repository](https://gitlab.mpi-sws.org/iris/opam/commits/master).)
* Run `make build-dep` (in Iris) to install the new version of std++.
You may have to do `make clean` as Coq will likely complain about .vo file
mismatches.
......
......@@ -9,7 +9,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
......
......@@ -9,7 +9,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
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|8)\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
......
This diff is collapsed.
......@@ -9,8 +9,8 @@ For using the Coq library, check out the
For understanding the theory of Iris, 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 document is
[available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
[docs/iris.tex](tex/iris.tex). A compiled PDF version of this document is
[available online](http://plv.mpi-sws.org/iris/appendix-3.2.pdf).
## Building Iris
......@@ -18,7 +18,7 @@ definitions and some derived forms is available in
This version is known to compile with:
- Coq 8.7.2 / 8.8.2 / 8.9.0 / 8.9.1
- Coq 8.8.2 / 8.9.1 / 8.10.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
......@@ -83,7 +83,7 @@ followed by `make build-dep`.
[MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
intuitionistic and spatial BI++ assertions. It also contains tactics for
interactive proofs. Documentation can be found in
[ProofMode.md](ProofMode.md).
[ProofMode.md](docs/proof_mode.md).
* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
language
* The subfolder [lib](theories/heap_lang/lib) contains a few derived
......@@ -113,11 +113,11 @@ that should be compatible with this version:
Getting along with Iris in Coq:
* Iris proof patterns are documented in the [proof guide](ProofGuide.md).
* Syntactic conventions are described in the [style guide](StyleGuide.md).
* Iris proof patterns are documented in the [proof guide](docs/proof_guide.md).
* Syntactic conventions are described in the [style guide](docs/style_guide.md).
* The Iris tactics are described in the
[the Iris Proof Mode (IPM) / MoSeL documentation](ProofMode.md) as well as the
[HeapLang documentation](HeapLang.md).
[the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
[HeapLang documentation](docs/heap_lang.md).
* The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
Contacting the developers:
......@@ -137,7 +137,7 @@ Contacting the developers:
Miscellaneous:
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
collected in [Editor.md](docs/editor.md).
* If you are writing a paper that uses Iris in one way or another, you could use
the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
the [Iris LaTeX macros](tex/iris.sty) for typesetting the various Iris
connectives.
......@@ -17,7 +17,6 @@ theories/algebra/big_op.v
theories/algebra/cmra_big_op.v
theories/algebra/sts.v
theories/algebra/auth.v
theories/algebra/frac_auth.v
theories/algebra/gmap.v
theories/algebra/ofe.v
theories/algebra/base.v
......@@ -39,7 +38,9 @@ theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v
theories/algebra/namespace_map.v
theories/algebra/ufrac_auth.v
theories/algebra/lib/excl_auth.v
theories/algebra/lib/frac_auth.v
theories/algebra/lib/ufrac_auth.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
......@@ -100,10 +101,12 @@ theories/heap_lang/lang.v
theories/heap_lang/metatheory.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/array.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_erasure.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/assert.v
......@@ -112,9 +115,12 @@ theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/nondet_bool.v
theories/heap_lang/lib/lazy_coin.v
theories/heap_lang/lib/clairvoyant_coin.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/diverge.v
theories/heap_lang/lib/arith.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
......@@ -13,17 +13,30 @@ if not "GITLAB_TOKEN" in os.environ:
print("You can create such tokens at <https://gitlab.mpi-sws.org/profile/personal_access_tokens>.")
print("Make sure you grant access to the 'api' scope.")
sys.exit(1)
if not "IRIS_REV" in os.environ:
print("Please set IRIS_REV, STDPP_REV, ORC11_REV and GPFSL_REV environment variables to the branch/tag/commit of the respective project that you want to use.")
print("Only IRIS_REV is mandatory, the rest defaults to 'master'.")
sys.exit(1)
GITLAB_TOKEN = os.environ["GITLAB_TOKEN"]
PROJECTS = [
{ 'name': 'examples', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'lambda-rust', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'lambda-rust', 'branch': 'ci/weak_mem', 'vars': ['STDPP_REV', 'IRIS_REV', 'ORC11_REV', 'GPFSL_REV'] },
{ 'name': 'lambda-rust', 'branch': 'ci/weak_mem', 'vars': ['STDPP_REV', 'IRIS_REV', 'ORC11_REV', 'GPFSL_REV'] }, # covers GPFSL and ORC11
{ 'name': 'iron', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'ora', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'reloc', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'c', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'tutorial-popl18', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'spygame', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] }, # these do not work, for some reason
{ 'name': 'time-credits', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'actris', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
]
for project in PROJECTS:
print("Triggering build for {}{}...".format(project['name'], '' if project['branch'] == 'master' else ':'+project['branch']))
url = "https://gitlab.mpi-sws.org/api/v4/projects/iris%2F{}/pipeline".format(project['name'])
id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name'])
url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
json = {
'ref': project['branch'],
'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])),
......
......@@ -68,6 +68,9 @@ on the math symbol list, and with some custom aliases for symbols used a lot in
(append math-symbol-list-basic math-symbol-list-extended))
```
Finally, set your default input method with `M-x customize-set-value`, setting
`default-input-method` to `math`.
### Font Configuration
Even when usable fonts are installed, Emacs tends to pick bad fonts for some
......
......@@ -7,7 +7,7 @@ language for simple examples.
## Language
HeapLang is a lambda-calculus with operations to allocate individual locations,
`load`, `store`, `CAS` (compare-and-swap) and `FAA` (fetch-and-add). Moreover,
`load`, `store`, `CmpXchg` (compare-and-exchange) and `FAA` (fetch-and-add). Moreover,
it has a `fork` construct to spawn new threads. In terms of values, we have
integers, booleans, unit, heap locations, as well as (binary) sums and products.
......@@ -76,17 +76,17 @@ Tactics for the heap:
- `wp_alloc l as "H"`: Reduce an allocation instruction and call the new
location `l` (in the Coq context) and the points-to assertion `H` (in the
spatial context). You can leave away the `as "H"` to introduce it as an
anonymous assertion, i.e., that is equivalent to `as "?"`.
spatial context). You can leave out the `as "H"` to introduce it as an
anonymous assertion, which is equivalent to `as "?"`.
- `wp_load`: Reduce a load operation. This automatically finds the points-to
assertion in the spatial context, and fails if it cannot be found.
- `wp_store`: Reduce a store operation. This automatically finds the points-to
assertion in the spatial context, and fails if it cannot be found.
- `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This
- `wp_cmpxchg_suc`, `wp_cmpxchg_fail`: Reduce a succeeding/failing CmpXchg. This
automatically finds the points-to assertion. It also automatically tries to
solve the (in)equality to show that the CAS succeeds/fails, and opens a new
solve the (in)equality to show that the CmpXchg succeeds/fails, and opens a new
goal if it cannot prove this goal.
- `wp_cas as H1 | H2`: Reduce a CAS, performing a case distinction over whether
- `wp_cmpxchg as H1 | H2`: Reduce a CmpXchg, performing a case distinction over whether
it succeeds or fails. This automatically finds the points-to assertion. The
proof of equality in the first new subgoal will be called `H1`, and the proof
of the inequality in the second new subgoal will be called `H2`.
......@@ -105,6 +105,12 @@ Further tactics:
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
To verify a recursive function, use `iLöb`. Make sure you do `wp_pures` before
running `iLöb`; otherwise the induction hypothesis will likely not be applicable
when you need it. (This makes sure that all administrative redexes are reduced
in your induction hypothesis, just like we state our `WP` specifications with
all of the redexes reduced.)
## Notation and lemmas for derived notions involving a thunk
Sometimes, it is useful to define a derived notion in HeapLang that involves
......@@ -120,7 +126,7 @@ value lambda). However, the *specification* for parallel composition should use
value lambdas, because prior to applying it the term will be reduced as much as
possible to achieve a normal form. To facilitate this, we define a copy of the
`e1 ||| e2` notation in the value scope that uses value lambdas.
This is not actually a value, but we still but it in the value scope to
This is not actually a value, but we still put it in the value scope to
differentiate from the other notation that uses expression lambdas. (In the
future, we might decide to add a separate scope for this.) Then, we write the
canonical specification using the notation in the value scope.
......
......@@ -6,6 +6,24 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and
[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
the [style guide](StyleGuide.md).
## Order of `Requires`
In Coq, declarations in modules imported later may override the
previous definition. Therefore, in order to make sure the most
relevant declarations and notations always take priority, we recommend
importing dependencies from the furthest to the closest.
In particular, when importing Iris, Stdpp and Coq stdlib modules, we
recommend importing in the following order:
- Coq
- stdpp
- iris.bi
- iris.proofmode
- iris.algebra
- iris.base_logic
- iris.program_logic
- iris.heap_lang
## Combinators for functors
In Iris, the type of propositions [iProp] is described by the solution to the
......
This diff is collapsed.
......@@ -36,8 +36,8 @@ is used by clients.
### small letters
* a : A = cmraT or cofeT
* b : B = cmraT or cofeT
* a : A = cmraT or ofeT
* b : B = cmraT or ofeT
* c
* d
* e : expr = expressions
......@@ -67,8 +67,8 @@ is used by clients.
### capital letters
* A : Type, cmraT or cofeT
* B : Type, cmraT or cofeT
* A : Type, cmraT or ofeT
* B : Type, cmraT or ofeT
* C
* D
* E : coPset = Viewshift masks
......@@ -110,9 +110,12 @@ is used by clients.
### Suffixes
* C: OFEs
* O: OFEs
* R: cameras
* UR: unital cameras or resources algebras
* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
* G: global camera functor management
* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
* G: global camera functor management (typeclass; see `ProofGuide.md`)
* I: bunched implication logic (of type `bi`)
* SI: step-indexed bunched implication logic (of type `sbi`)
* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
* Σ: global camera functor management (`gFunctors`; see `ProofGuide.md`)
......@@ -11,6 +11,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-05-30.0.84fd0660") | (= "dev") }
"coq" { (= "8.8.2") | (>= "8.9.1" & < "8.12~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-11-22.2.16eb222f") | (= "dev") }
]
From iris.base_logic.lib Require Import invariants.
Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _.
Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests.
Context `{!invG Σ}.
Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
λne P v, ( (P v))%I.
Solve Obligations with solve_proper.
......
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
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
<<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Now come the long pre/post tests"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ #(), COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Φ : language.val heap_lang → iProp Σ
============================
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Prettification"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
"AU" : ∃ x : val, P x
∗ (P x
={∅,⊤}=∗ AU << ∀ x0 : val,
P x0 >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>)
∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
--------------------------------------∗
WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Default Proof Using "Type".
......
......@@ -40,7 +40,7 @@
============================
_ : ▷ l ↦ #0
--------------------------------------∗
WP CAS #l #0 #1 {{ _, l ↦ #1 }}
WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
1 subgoal
......@@ -86,6 +86,16 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP "x" {{ _, True }}
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go",
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iAndDestruct (constr) as (constr) (constr)", last call failed.
Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
1 subgoal
Σ : gFunctors
......@@ -144,8 +154,9 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
"not_cas"
"not_cmpxchg"
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
Ltac call to "wp_cmpxchg_suc" failed.
Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in
(#() #()).
......@@ -76,17 +76,18 @@ Section tests.
Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Lemma heap_e6_spec (v : val) :
val_is_unboxed v (WP heap_e6 v {{ w, w = #true }})%I.
Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
Lemma heap_e7_spec_total l : l #0 - WP heap_e7 #l [{_, l #1 }].
Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
Proof. iIntros. wp_lam. wp_cmpxchg_suc. auto. Qed.
Check "heap_e7_spec".
Lemma heap_e7_spec l : ^2 l #0 - WP heap_e7 #l {{_, l #1 }}.
Proof. iIntros. wp_lam. Show. wp_cas_suc. Show. auto. Qed.
Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
Definition FindPred : val :=
rec: "pred" "x" "y" :=
......@@ -124,11 +125,11 @@ Section tests.
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
Lemma wp_cas l v :
Lemma wp_cmpxchg l v :
val_is_unboxed v
l v - WP CAS #l v v {{ _, True }}.
l v - WP CmpXchg #l v v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
Qed.
Lemma wp_alloc_split :
......@@ -154,6 +155,23 @@ Section tests.
by iApply "HΦ".
Qed.
Lemma wp_load_array l :
{{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l + #1) {{{ RET #1; True }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_op.
wp_apply (wp_load_offset _ _ _ 1 with "Hl"); first done.
iIntros "Hl". by iApply "HΦ".
Qed.
Lemma test_array_app l vs1 vs2 :
l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
Proof.
Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
Fail iSplitL "H1".
iApply array_app. iSplitL "H1"; done.
Qed.
End tests.
Section printing_tests.
......@@ -210,11 +228,11 @@ End printing_tests.
Section error_tests.
Context `{!heapG Σ}.
Check "not_cas".
Lemma not_cas :
Check "not_cmpxchg".
Lemma not_cmpxchg :
(WP #() #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Fail wp_cmpxchg_suc.
Abort.
End error_tests.
......
(* Test yet another way of importing heap_lang modules that used to break
printing *)
From iris.heap_lang Require Export lifting notation.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -8,46 +8,22 @@ Section tests.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Definition CAS_resolve e1 e2 e3 p v :=
Resolve (CAS e1 e2 e3) p v.
Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) :
vals_cas_compare_safe v1 v1
{{{ proph p vs l v1 }}}
CAS_resolve #l v1 v2 #p v @ s; E
{{{ RET #true ; vs', vs = (#true, v)::vs' proph p vs' l v2 }}}.
Proof.
iIntros (Hcmp Φ) "[Hp Hl] HΦ".
wp_apply (wp_resolve with "Hp"); first done.
assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
wp_cas_suc. iIntros (vs' ->) "Hp".
iApply "HΦ". eauto with iFrame.
Qed.
Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
val_for_compare v' val_for_compare v1 vals_cas_compare_safe v' v1
{{{ proph p vs l v' }}}
CAS_resolve #l v1 v2 #p v @ s; E
{{{ RET #false ; vs', vs = (#false, v)::vs' proph p vs' l v' }}}.
Proof.
iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
wp_apply (wp_resolve with "Hp"); first done.
wp_cas_fail. iIntros (vs' ->) "Hp".
iApply "HΦ". eauto with iFrame.
Qed.
Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
l #n -
proph p vs -
WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, v = #true vs, proph p vs l #(n+1) }}%I.
WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
{{ v, v = (#n, #true)%V vs, proph p vs l #(n+1) }}.
Proof.
iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
wp_cmpxchg_suc. iIntros (ws ->) "Hp". eauto with iFrame.
Restart.
iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
Qed.
Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
proph p vs -
WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, v = #0 vs, proph p vs }}%I.
WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, v = #0 vs, proph p vs }}.
Proof.
iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
......
......@@ -3,8 +3,8 @@
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany and Lars Birkedal
POPL 2017 *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import base_logic.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......@@ -132,7 +132,7 @@ Section M.
Arguments op _ _ !_ !_/.
Arguments core _ _ !_/.
Canonical Structure M_C : ofeT := leibnizC M.
Canonical Structure M_O : ofeT := leibnizO M.
Instance M_valid : Valid M := λ x, x Bot.
Instance M_op : Op M := λ x y,
......@@ -222,19 +222,19 @@ 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 (CmpXchg _ _ _). 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γ".
iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
wp_cas_suc. iSplitL "Hl Hγ".
wp_cmpxchg_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_if. rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega).
wp_pures. rewrite {3}/C; eauto 10.
- wp_cmpxchg_fail; first (intros [=]; abstract omega).
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed.
Check "read_spec".
......
......@@ -10,7 +10,7 @@
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP rev hd acc [{ v, Φ v }]
WP (rev hd) acc [{ v, Φ v }]
1 subgoal
......@@ -28,6 +28,6 @@
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
"l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
end [{ v, Φ v }]
......@@ -10,7 +10,7 @@
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP (rev hd) acc [{ v, Φ v }]
WP rev hd acc [{ v, Φ v }]
1 subgoal
......@@ -28,6 +28,6 @@
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
end [{ v, Φ v }]
(** Correctness of in-place list reversal *)
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export total_weakestpre weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -5,8 +5,8 @@ Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
ICFP 2018 *)
From iris.proofmode Require Import tactics monpred.
From iris.bi Require Import monpred.
From iris.proofmode Require Import tactics monpred.
Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) :
P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a).
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl agree csum.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
(** This is the introductory example from the "Iris from the Ground Up" journal
paper. *)
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* tryset *) (λ: "n",
......@@ -21,7 +24,7 @@ Definition one_shot_example : val := λ: <>,
end
end)).
Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
Definition Pending : one_shotR := Cinl (Excl ()).
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
......@@ -49,13 +52,13 @@ Proof.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
wp_pures. iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_lam. wp_pures.
- iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
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). }
wp_cas_suc. iSplitL; last eauto.
iModIntro. iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iSplitL; last eauto.
wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iNext; iRight; iExists n; by iFrame.
+ wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
......
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
l : loc
γ : gname
============================
"HN" : inv N (one_shot_inv γ l)
--------------------------------------□
"Hl" : l ↦ InjLV #()
_ : own γ (Pending (1 / 2))
--------------------------------------∗
one_shot_inv γ l
∗ (⌜InjLV #() = InjLV #()⌝
∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
l : loc
γ : gname
m, m' : Z
============================
"HN" : inv N (one_shot_inv γ l)
"Hγ'" : own γ (Shot m)
--------------------------------------□
"Hl" : l ↦ InjRV #m'
"Hγ" : own γ (Shot m')
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
∗ WP let: "y'" := InjRV #m' in
match: InjRV #m with
InjL <> => #()
| InjR <> => assert: InjRV #m = "y'"
end {{ _, True }}
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac agree csum.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
(** This is the introductory example from Ralf's PhD thesis.
The difference to [one_shot] is that [set] asserts to be called only once. *)
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* set *) (λ: "n",
assert: CAS "x" NONE (SOME "n")),
(* check *) (λ: <>,
let: "y" := !"x" in λ: <>,
let: "y'" := !"x" in
match: "y" with
NONE => #()
| SOME <> => assert: "y" = "y'"
end)).
Definition one_shotR := csumR fracR (agreeR ZO).
Definition Pending (q : Qp) : one_shotR := Cinl q.
Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ one_shotG Σ.
Proof. solve_inG. Qed.
Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !one_shotG Σ}.
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
(l NONEV own γ (Pending (1/2)%Qp)
n : Z, l SOMEV #n own γ (Shot n))%I.
Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
unfold one_shot_inv : core.
Lemma pending_split γ q :
own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) own γ (Pending (q/2)).
Proof.
rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op' Qp_div_2 //.
Qed.
Lemma pending_shoot γ n :
own γ (Pending 1%Qp) == own γ (Shot n).
Proof.
iIntros "Hγ". iMod (own_update with "Hγ") as "$"; last done.
by apply cmra_update_exclusive with (y:=Shot n).
Qed.
Lemma wp_one_shot (Φ : val iProp Σ) :
( (f1 f2 : val) (T : iProp Σ), T
( n : Z, T - WP f1 #n {{ w, True }})
WP f2 #() {{ g, WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".
{ iNext. iLeft. by iFrame. }
wp_pures. iModIntro. iApply ("Hf" $! _ _ (own γ (Pending (1/2)%Qp))).
iSplitL; first done. iSplit.
- iIntros (n) "!# Hγ1". wp_pures.
iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
+ iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
iMod (pending_shoot _ n with "Hγ") as "Hγ".
wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
iNext; iRight; iExists n; by iFrame.
+ by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
- iIntros "!# /=". wp_lam. wp_bind (! _)%E.
iInv N as ">Hγ".
iAssert ( v, l v (v = NONEV own γ (Pending (1/2)%Qp)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
+ iExists NONEV. iFrame. eauto.
+ iExists (SOMEV #m). iFrame. eauto. }
iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l (v = NONEV n : Z,
v = SOMEV #n own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
iSplitL "Hinv"; first by eauto.
iModIntro. wp_pures. iIntros "!#". wp_lam. wp_bind (! _)%E.
iInv N as "Hinv".
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
+ iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
wp_load; iModIntro; (iSplitL "Hl Hγ"; first by eauto with iFrame);
wp_pures; done.
+ iDestruct "Hinv" 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 Hγ"; first by eauto with iFrame.
wp_pures. iApply wp_assert. wp_op. by case_bool_decide.
Qed.
Lemma ht_one_shot (Φ : val iProp Σ) :
{{ True }} one_shot_example #()
{{ ff, T, T
( n : Z, {{ T }} Fst ff #n {{ _, True }})
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
}}.
Proof.
iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
iExists T. iFrame "HT". iSplit.
- iIntros (n) "!# HT". wp_apply "Hf1". done.
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
(* Have a client with a closed proof. *)
Definition client : expr :=
let: "ff" := one_shot_example #() in
(Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.