Commit c9be14ee authored by Robbert Krebbers's avatar Robbert Krebbers

Add skeletons.

parent 0de7dd98
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
.PHONY: all
clean: Makefile.coq
+@make -f Makefile.coq clean
find ./ \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
Makefile.coq: _CoqProject Makefile
coq_makefile -f _CoqProject -o Makefile.coq
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
This diff is collapsed.
# This configuration file was generated by running:
# coq_makefile -f _CoqProject -o Makefile.coq
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = ex_01_swap.v ex_02_sumlist.v ex_03_spinlock.v ex_04_parallel_add.v ex_05_parallel_add_mul.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS =
COQMF_SRC_SUBDIRS =
COQMF_COQLIBS = -Q . tutorial
COQMF_COQLIBS_NOML = -Q . tutorial
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=1
COQMF_COQLIB=/home/robbert/coq/coq-8.7.0//
COQMF_DOCDIR=/home/robbert/coq/coq-8.7.0/doc/
COQMF_OCAMLFIND=/usr/bin/ocamlfind
COQMF_CAMLP4=camlp5
COQMF_CAMLP4O=/usr/bin/camlp5o
COQMF_CAMLP4BIN=/usr/bin/
COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5
COQMF_CAMLP4OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=/home/robbert/coq/coq-8.7.0
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS = -w -notation-overridden,-redundant-canonical-projection,-several-object-files
COQMF_INSTALLCOQDOCROOT = tutorial
This diff is collapsed.
# The Iris tutorial @ POPL'18
For the tutorial material you need to have the following dependencies installed:
- Coq 8.6.1 / 8.7.0 / 8.7.1
- Ssreflect 1.6.4
- Coq-std++ 1.1
- Iris 3.1
*Note:* the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above.
## Installing Iris via opam
The easiest, and recommend, way of installing Iris and its dependencies is via
the OCaml package manager opam (1.2.2 or newer). You first have to add the Coq
opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released
Then you can do `opam install coq-iris`.
## Installing Iris from source
If you are unable to use opam, you can also build Iris from source. For this,
make sure to `git checkout` the correct versions, and run `make; make install`
for Ssreflect, Coq-std++ and Iris.
## Compiling the exercises
Run `make` to compile the exercises. You need to have exercise 3 compiled to
work on exercise 4 and 5.
## Documentation
The file `ProofMode.md` in the tutorial material (which can also be found in the
root of the Iris repository) contains a list of the Iris Proof Mode tactics.
If you would like to know more about Iris, we recommend to take a look at:
- http://iris-project.org/tutorial-material.html
Lecture Notes on Iris: Higher-Order Concurrent Separation Logic
Lars Birkedal and Aleš Bizjak
Used for an MSc course on concurrent separation logic at Aarhus University
- https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent
Separation Logic
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars
Birkedal, Derek Dreyer.
A detailed description of the Iris logic and its model
-Q . tutorial
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
ex_01_swap.v
ex_02_sumlist.v
ex_03_spinlock.v
ex_04_parallel_add.v
ex_05_parallel_add_mul.v
(*
This exercise introduces the basic Iris Proof Mode tactics by proving a simple
example: a function that swaps the contents of two pointers. We will use this
function to implement two other functions.
*)
From iris.heap_lang Require Import proofmode notation.
(* The swap function, defined as a heap-lang value. This looks like an ordinary
Coq function, but it is not: heap-lang is a deeply embedded language in Coq. It
uses strings for name binding and notations close to Coq's (but typically
augmented with a colon to avoid ambiguity) to make it easy to read and write
programs. *)
Definition swap : val := λ: "x" "y",
let: "tmp" := !"x" in
"x" <- !"y";;
"y" <- "tmp".
(* Using swap, we can define functions that rotate three pointers in left and
right direction. *)
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Definition rotate_l : val := λ: "x" "y" "z",
swap "x" "y";; swap "y" "z".
Section proof.
(* Iris is parameterized by the type of ghost state that is needed to carry out
a proof. As such, the type of Iris propositions [iProp] is indexed by a [Σ]: a
list of cameras (actually, functors from OFEs to cameras). To make our proofs
generic, we abstract over any such [Σ] and use type classes to ensure that the
necessary cameras are present in [Σ].
For this proof, we do not need any special ghost state (i.e. cameras) apart from
the ghost state that's the heap-lang uses internally for modeling the [l ↦ v]
connective. The cameras for this ghost state is provided by the class [heapG].
*)
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x v1 y v2 }}} swap #x #y {{{ RET #(); x v2 y v1 }}}.
(* The "Texan triple" [ {{{ P }}} e {{{ RET v, Q }}} ] is syntactic sugar for:
∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e {{ v, Φ v }}
Which is logically equivalent to [ P -∗ WP e {{ x, x = v ∗ Q }} ]
In practice, the "Texan triple" is not more difficult to prove, but usually
easier to use other proofs, because the post-condition does not have to
syntactically match [Q]. Using this way of stating specifications, the
consequence and framing rule is implicitly applied on the post-condition.
Note that [ # v ] is the embedding of values ([bool], [Z], [loc]) into
heap-lang values.*)
Proof.
iIntros (Φ) "[Hx Hy] Post".
unfold swap.
wp_lam. wp_lam.
wp_load. wp_let.
wp_load. wp_store.
wp_store.
iApply "Post".
iSplitL "Hx".
- iApply "Hx".
- iApply "Hy".
Qed.
(* Same lemma, but using a bit of automation to shorten the proof. *)
Lemma swap_spec_2 x y v1 v2 :
{{{ x v1 y v2 }}} swap #x #y {{{ RET #(); x v2 y v1 }}}.
Proof.
iIntros (Φ) "[??] Post".
wp_lam. wp_lam. wp_load. wp_let. wp_load. wp_store. wp_store.
iApply "Post". iFrame.
Qed.
(* We can further automate the lemma by defining a simple Ltac tactic for
symbolic executing. *)
Ltac wp_exec := repeat (wp_pure _ || wp_load || wp_store).
(* This tactic repeatedly tries to symbolically execute pure redexes, loads and
stores. It makes use of the tactic [wp_pure t], which tries to find the redex
[t] in the goal, and executes that redex. The redex [t] may contain holes, and
as such, tactics like [wp_seq] are actually defined as [wp_pure (_ ;; _)%E]. By
using [wp_pure _] it will symbolically execute *any* pure redex. *)
(* Same lemma again, but now using the tactic we just defined. *)
Lemma swap_spec_2_more_automation x y v1 v2 :
{{{ x v1 y v2 }}} swap #x #y {{{ RET #(); x v2 y v1 }}}.
Proof.
iIntros (Φ) "[??] Post". wp_exec.
iApply "Post". iFrame.
Qed.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x v1 y v2 z v3 }}}
rotate_r #x #y #z
{{{ RET #(); x v3 y v1 z v2 }}}.
Proof.
(* As in Coq, the IPM introduction pattern (p1 & p2 & .. & pn) ] is syntactic
sugar for [ [p1 [p2 [... pn]]] ]. *)
iIntros (Φ) "(Hx & Hy & Hz) Post".
unfold rotate_r. do 3 wp_lam.
wp_bind (swap _ _).
iApply (swap_spec with "[Hy Hz]").
{ iFrame. }
(* Inspired by ssreflect, the IPM introduction pattern [ /= ] performs
[simpl]. *)
iNext. iIntros "[Hy Hz] /=". wp_seq.
(* We can also immediately frame hypothesis when using a lemma: *)
iApply (swap_spec with "[$Hx $Hy]"); iNext; iIntros "[Hx Hy]".
iApply "Post". iFrame.
Qed.
Lemma rotate_r_spec_again x y z v1 v2 v3 :
{{{ x v1 y v2 z v3 }}}
rotate_r #x #y #z
{{{ RET #(); x v3 y v1 z v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
(* We can shorten the above a bit: Instead of using the [iApply] tactic, we
can use [wp_apply] which automatically uses [wp_bind] first. Also, it strips
the later [▷] by calling [iNext] afterwards. *)
wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz] /="; wp_seq.
wp_apply (swap_spec with "[$Hx $Hy]"); iIntros "[Hx Hy] /=".
iApply "Post". iFrame.
Qed.
(* *Exercise*: Do this proof yourself. Try a couple of variations of the tactics
we have seen before:
- Do the whole proof explicitly by proving [swap] inline,
- Use the specification of [swap] in combination with [iApply],
- Use the specification of [swap] in combination with [wp_apply]
*)
Lemma rotate_l_spec x y z v1 v2 v3 :
{{{ x v1 y v2 z v3 }}}
rotate_l #x #y #z
{{{ RET #(); x v2 y v3 z v1 }}}.
Proof.
(* exercise *)
Admitted.
End proof.
(**
This exercise shows how to use representation predicates in Iris. We consider
some basic operations on linked lists. Although heap-lang is untyped, our
representation of lists intuitively corresponds to the following (rec-) type
in an ML-style language:
list A := option (ref (A * list A))
*)
From iris.heap_lang Require Import proofmode notation.
(** A function that sums all elements of a list, defined as a heap-lang value: *)
Definition sum_list : val :=
rec: "sum_list" "l" :=
match: "l" with (* A list is either... *)
NONE => #0 (* ... the empty list *)
| SOME "p" => (* ... or [SOME p], where [p] points to a pair ... *)
let: "x" := Fst !"p" in (* ... whose first component is the head of the list *)
let: "l" := Snd !"p" in (* ... and whose second component is the rest of the list. *)
"x" + "sum_list" "l"
end.
(** A function that increases all elements of a list in-place: *)
Definition inc_list : val :=
rec: "inc_list" "n" "l" :=
match: "l" with
NONE => #()
| SOME "p" =>
let: "x" := Fst !"p" in
let: "l" := Snd !"p" in
"p" <- ("n" + "x", "l");;
"inc_list" "n" "l"
end.
(** The previous functions combined. *)
Definition sum_inc_list : val := λ: "n" "l",
inc_list "n" "l";;
sum_list "l".
(** A function that maps a function over all elements of a list: *)
Definition map_list : val :=
rec: "inc_list" "f" "l" :=
match: "l" with
NONE => #()
| SOME "p" =>
let: "x" := Fst !"p" in
let: "l" := Snd !"p" in
"p" <- ("f" "x", "l");;
"inc_list" "f" "l"
end.
Section proof.
Context `{!heapG Σ}.
(** Representation predicate in separation logic for a list of integers [l]: *)
Fixpoint is_list (l : list Z) (v : val) : iProp Σ :=
match l with
| [] => v = NONEV
| x :: l' => (p : loc), v = SOMEV #p
v' : val, p (#x, v') is_list l' v'
end%I.
(**
In order to give a specification of [sum_list] we relate its result to the
sum defined as a pure Coq function.
*)
Definition sum_list_coq (l : list Z) : Z :=
fold_right Z.add 0 l.
(**
The proof of the recursive function [sum_list] requires some form of recursion.
We can either do the induction over the list [l], or use the Löb induction
principle, given by the step-indexed nature of Iris. *)
(** The proof using induction over [l]: *)
Lemma sum_list_spec_induction l v :
{{{ is_list l v }}} sum_list v {{{ RET #(sum_list_coq l); is_list l v }}}.
Proof.
iIntros (Φ) "Hl Post".
iInduction l as [|x l] "IH" forall (v Φ); simpl.
(**
Note that the option type is in fact encoded using sum types.
Hence, [NONE] is syntactic sugar for [InjL #()] (or [InjLV #()]
for values), and [SOME x] is syntactic sugar for [InjR x].
*)
- iDestruct "Hl" as %->.
wp_rec.
wp_match.
iApply "Post". iPureIntro. reflexivity.
- iDestruct "Hl" as (p) "[-> Hl]". iDestruct "Hl" as (v) "[Hp Hl]".
wp_rec.
wp_match.
wp_load. wp_proj. wp_let.
wp_load. wp_proj. wp_let.
wp_apply ("IH" with "Hl"). iIntros "Hl". wp_op.
iApply "Post".
iExists p. iSplitR; [done|].
iExists v. iSplitR "Hl"; [iApply "Hp"|iApply "Hl"].
Qed.
(** The proof using Löb induction. The parts which are in common with
[sum_list_spec_induction] are shortened using automation. *)
Lemma sum_list_spec_löb l v :
{{{ is_list l v }}} sum_list v {{{ RET #(sum_list_coq l); is_list l v }}}.
Proof.
iIntros (Φ) "Hl Post".
iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec.
- iDestruct "Hl" as %->. wp_match. by iApply "Post".
- iDestruct "Hl" as (p -> v) "[Hp Hl]". wp_match.
do 2 (wp_load; wp_proj; wp_let).
wp_apply ("IH" with "Hl"). iIntros "Hl". wp_op.
iApply "Post". eauto with iFrame.
Qed.
(** *Exercise*: Do the proof of [inc_list] yourself. Use ordinary induction. *)
Lemma inc_list_spec_induction n l v :
{{{ is_list l v }}}
inc_list #n v
{{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof.
(* exercise *)
Admitted.
(** *Exercise*: Now do the proof again using Löb induction. *)
Lemma inc_list_spec_löb n l v :
{{{ is_list l v }}}
inc_list #n v
{{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof.
(* exercise *)
Admitted.
(** *Exercise*: Do the proof of [sum_inc_list] by making use of the lemmas of
[sum_list] and [inc_list] we just proved. Make use of [wp_apply]. *)
Lemma sum_inc_list_spec n l v :
{{{ is_list l v }}}
sum_inc_list #n v
{{{ RET #(sum_list_coq (map (Z.add n) l)); is_list (map (Z.add n) l) v }}}.
Proof.
(* exercise *)
Admitted.
(** *Optional exercise*: Prove the following spec of [map_list] which makes use
of a nested Texan triple, This spec is rather weak, as it requires [f] to be
pure, if you like, you can try to make it more general. *)
Lemma map_list_spec_induction (f : val) (f_coq : Z Z) l v :
( n, {{{ True }}} f #n {{{ RET #(f_coq n); True }}}) -
{{{ is_list l v }}} map_list f v {{{ RET #(); is_list (map f_coq l) v }}}.
Proof.
(* exercise *)
Admitted.
End proof.
(**
In this exercise, we prove the correctness of a spin lock module.
*)
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
Definition newlock : val := λ: <>,
ref #false.
Definition try_acquire : val := λ: "l",
CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" :=
if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l",
"l" <- #false.
(**
As shown, the spin lock is implemented as a reference to a Boolean. If the
Boolean is [true], it means some thread has acquired the lock/entered the
critical section. We initiate the lock with the value [false], which means that
the lock is initially in the unlocked state.
The most interesting function of the spin lock is [acquire], which checks if the
lock is in the unlocked state, and if not, changes the lock into [true]. Since
multiple threads could try to acquire the lock at the same time, we use the
[CAS l v w] (compare-and-set) instruction. This instruction atomically checks
if the value of the reference [l] is equal to [v], and if so, changes it into
[w] and returns [true]. If the value of [l] is unequal to [v], it leaves the
value of [l] as if, and returns [false].
*)
(**
We will prove the following lock specification in Iris:
{{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}.
{{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}
{{{ is_lock lk R ∗ R }}} release lk {{{ RET #(); True }}}.
Here, [is_lock lk R] is a representation predicate which says that a lock at
location [lk] guards the payload [R] described as an Iris proposition.
*)
Section proof.
Context `{!heapG Σ}.
(** The invariant of the lock:
- It owns the memory location [l ↦ #b], which contain a Boolean [b],
- If the Boolean [b] is [false] (the lock is in the unlocked state),
then the payload [R] of the lock holds.
*)
Definition lock_inv (l : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, l #b if b then True else R)%I.
(** Invariants in Iris are named by a *namespace* so that several invariants
can be opened at the same time, while guaranteeing that no invariant is opened
twice at the same time (which would be unsound). Here, this is irrelevant,
since acquiring and releasing a lock only requires to open one invariant.
The namespace [lockN] of the lock invariant:
*)
Definition lockN : namespace := nroot .@ "lock".
Definition is_lock (lk : val) (R : iProp Σ) : iProp Σ :=
( l: loc, lk = #l inv lockN (lock_inv l R))%I.
(** The main proofs. *)
Lemma newlock_spec (R : iProp Σ):
{{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". iApply wp_fupd.
wp_lam. wp_alloc l as "Hl".
(** Use the Iris rule [inv_alloc] for allocating a lock. We put both the
resources [HR : R] and the points-to [l ↦ #false] into the lock. *)
iMod (inv_alloc lockN _ (lock_inv l R) with "[HR Hl]") as "#Hinv".
{ iNext. iExists false. iFrame. }
iModIntro. iApply "HΦ". iExists l. eauto.
Qed.
(** *Exercise*: finish the proof below. *)
Lemma try_acquire_spec lk R :
{{{ is_lock lk R }}} try_acquire lk
{{{ b, RET #b; if b is true then R else True }}}.
Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec.
(** Using the tactic [iInv] we open the invariant. *)
iInv lockN as (b) "[Hl HR]" "Hclose".
(** The post-condition of the WP is augmented with an *update* modality
[ |={⊤ ∖ ↑lockN,⊤}=> ... ], which keeps track of the fact that we opened
the invariant named [lockN]. We can introduce this update modality by
closing the lock using the hypothesis:
"Hclose" : ▷ lock_inv l R ={⊤ ∖ ↑lockN,⊤}=∗ True
*)
destruct b.
- wp_cas_fail. iMod ("Hclose" with "[Hl]") as "_".
{ iNext. iExists true. iFrame. }
iModIntro. (* exercise *)
Admitted.
(** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive
function, you should use the tactic [iLöb] for Löb induction. Use the tactic
[wp_apply] to use [try_acquire_spec] when appropriate. *)
Lemma acquire_spec lk R :
{{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}.
Proof.
(* exercise *)
Admitted.
(** *Exercise*: prove the spec of [release]. At a certain point in this proof,
you need to open the invariant. For this you can use:
iInv lockN as (b) "[Hl HR]" "Hclose".
In the same way as in the proof of [try_acquire]. You also need to close the
invariant. *)
Lemma release_spec lk R :
{{{ is_lock lk R R }}} release lk {{{ RET #(); True }}}.
Proof.
(* exercise *)
Admitted.
End proof.
(**
In this exercise we use the spin-lock from the previous exercise to implement
the running example during the lecture of the tutorial: proving that when two
threads increase a reference that's initially zero by two, the result is four.
*)
From iris.algebra Require Import auth frac_auth.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation.
From tutorial Require Import ex_03_spinlock.
(** The program as a heap-lang expression. We use the heap-lang [par] module for
parallel composition. *)
Definition parallel_add : expr :=
let: "r" := ref #0 in
let: "l" := newlock #() in
(
(acquire "l";; "r" <- !"r" + #2;; release "l")
|||
(acquire "l";; "r" <- !"r" + #2;; release "l")
);;
acquire "l";;
!"r".
(** 1st proof : we only prove that the return value is even.
No ghost state is involved in this proof. *)
Section proof1.
Context `{!heapG Σ, !spawnG Σ}.
Definition parallel_add_inv_1 (r : loc) : iProp Σ :=
( n : Z, r #n Zeven n )%I.
(** *Exercise*: finish the missing cases of this proof. *)
Lemma parallel_add_spec_1 :
{{{ True }}} parallel_add {{{ n, RET #n; Zeven n }}}.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let.
wp_apply (newlock_spec (parallel_add_inv_1 r) with "[Hr]").
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, True%I) (λ _, True%I)).
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr %]".
wp_seq. wp_load. wp_op. wp_store.
wp_apply (release_spec with "[Hr $Hl]"); [|done].
iExists _. iFrame "Hr". iPureIntro. by apply Zeven_plus_Zeven.
- (* exercise *)
admit.
- (* exercise *)
admit.
Admitted.
End proof1.
(** 2nd proof : we prove that the program returns 4 exactly.
We need a piece of ghost state: integer ghost variables.
Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the
proofs, we now need to make sure that we can use integer ghost variables. For
this, we add the type class constraint:
inG Σ (authR (optionUR (exclR ZC)))
*)
Section proof2.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZC)))}.
Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ :=
( n1 n2 : Z, r #(n1 + n2)
own γ1 ( (Excl' n1)) own γ2 ( (Excl' n2)))%I.
(** Some helping lemmas for ghost state that we need in the proof. In actual
proofs we tend to inline simple lemmas like these, but they are here to
make things easier to understand. *)
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
Proof.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]"; by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ n m :
own γ ( (Excl' n)) - own γ ( (Excl' m)) - n = m .
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
Qed.
Lemma ghost_var_update γ n' n m :
own γ ( (Excl' n)) - own γ ( (Excl' m)) ==
own γ ( (Excl' n')) own γ ( (Excl' n')).
Proof.
iIntros "Hγ● Hγ◯".
iMod (own_update_2 _ _ _ ( Excl' n' Excl' n') with "Hγ● Hγ◯") as "[$$]".
{ by apply auth_update, option_local_update, exclusive_local_update. }
done.
Qed.
(** *Exercise*: finish the missing cases of the proof. *)
Lemma parallel_add_spec_2 :
{{{ True }}} parallel_add {{{ RET #4; True }}}.
Proof.
iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (ghost_var_alloc 0) as (γ1) "[Hγ1● Hγ1◯]".
iMod (ghost_var_alloc 0) as (γ2) "[Hγ2● Hγ2◯]".
wp_apply (newlock_spec (parallel_add_inv_2 r γ1 γ2) with "[Hr Hγ1● Hγ2●]").
{ (* exercise *)
admit. }
iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ1 ( Excl' 2)) (λ _, own γ2 ( Excl' 2))
with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n1 n2) "(Hr & Hγ1● & Hγ2●)".
wp_seq. wp_load. wp_op. wp_store.
iDestruct (ghost_var_agree with "Hγ1● Hγ1◯") as %->.
iMod (ghost_var_update γ1 2 with "Hγ1● Hγ1◯") as "[Hγ1● Hγ1◯]".
wp_apply (release_spec with "[- $Hl Hγ1◯]"); [|by auto].
iExists _, _. iFrame "Hγ1● Hγ2●". rewrite (_ : 2 + n2 = 0 + n2 + 2); [done|ring].
- (* exercise *)
admit.
- (* exercise *)