Commit 5651e5a8 authored by Amin Timany's avatar Amin Timany
Browse files

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents c54861f9 302ffc56
......@@ -32,12 +32,18 @@ Context management
- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis whose conclusion is persistent. In this
case, all hypotheses can be used for proving the premises, as well as for
the resulting goal.
- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
`H`.
- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
put `P` in the context of the original goal. The specialization pattern
`spat` specifies which hypotheses will be consumed by proving `P` and the
`spat` specifies which hypotheses will be consumed by proving `P`. The
introduction pattern `ipat` specifies how to eliminate `P`.
- `iAssert P with "spat" as %cpat` : assert `P` and eliminate it using the Coq
introduction pattern `cpat`.
Introduction of logical connectives
-----------------------------------
......@@ -60,12 +66,17 @@ Elimination of logical connectives
----------------------------------
- `iExFalso` : Ex falso sequitur quod libet.
- `iDestruct pm_trm as (x1 ... xn) "spat1 ... spatn"` : elimination of
existential quantifiers using Coq introduction patterns `x1 ... xn` and
elimination of object level connectives using the proof mode introduction
patterns `ipat1 ... ipatn`.
- `iDestruct pm_trm as (x1 ... xn) "ipat"` : elimination of existential
quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
object level connectives using the proof mode introduction pattern `ipat`.
In case all branches of `ipat` start with an `#` (moving the hypothesis to the
persistent context) or `%` (moving the hypothesis to the pure Coq context),
one can use all hypotheses for proving the premises of `pm_trm`, as well as
for proving the resulting goal.
- `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
introduction pattern `cpat`.
introduction pattern `cpat`. When using this tactic, all hypotheses can be
used for proving the premises of `pm_trm`, as well as for proving the
resulting goal.
Separating logic specific tactics
---------------------------------
......@@ -180,9 +191,9 @@ so called specification patterns to express this splitting:
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a primitive view shift, in which case the view shift will be kept in the
goal of the premise too.
- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
`Q` is persistent. In this case, all hypotheses are available in the goal for
the premise as none will be consumed.
- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
persistent. Using this pattern, all hypotheses are available in the goal for
`P`, as well the remaining goal.
- `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
It will generate a Coq goal for `P` and does not consume any hypotheses.
- `*` : instantiate all top-level universal quantifiers with meta variables.
......
......@@ -62,6 +62,7 @@ algebra/updates.v
algebra/local_updates.v
algebra/gset.v
algebra/coPset.v
algebra/double_negation.v
program_logic/model.v
program_logic/adequacy.v
program_logic/lifting.v
......
......@@ -95,9 +95,10 @@ Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Lemma authoritative_validN n (x : auth A) : {n} x {n} authoritative x.
Lemma authoritative_validN n x : {n} x {n} authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_own_validN n (x : auth A) : {n} x {n} auth_own x.
Lemma auth_own_validN n x : {n} x {n} auth_own x.
Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
Lemma auth_valid_discrete `{CMRADiscrete A} x :
......@@ -111,6 +112,14 @@ Proof.
setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
Qed.
Lemma authoritative_valid x : x authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_own_valid `{CMRADiscrete A} x : x auth_own x.
Proof.
rewrite auth_valid_discrete.
destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
Qed.
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Proof.
apply cmra_total_mixin.
......
......@@ -342,6 +342,8 @@ Global Instance cmra_included_trans: Transitive (@included A _ _).
Proof.
intros x y z [z1 Hy] [z2 Hz]; exists (z1 z2). by rewrite assoc -Hy -Hz.
Qed.
Lemma cmra_valid_included x y : y x y x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.
Lemma cmra_validN_includedN n x y : {n} y x {n} y {n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included n x y : {n} y x y {n} x.
......@@ -984,6 +986,10 @@ Section prod_unit.
Lemma pair_split (x : A) (y : B) : (x, y) (x, ) (, y).
Proof. by rewrite pair_op left_id right_id. Qed.
Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
(x, y) = (x, ) (, y).
Proof. unfold_leibniz. apply pair_split. Qed.
End prod_unit.
Arguments prodUR : clear implicits.
......
From iris.algebra Require Import upred.
Import upred.
(* In this file we show that the rvs can be thought of a kind of
step-indexed double-negation when our meta-logic is classical *)
(* To define this, we need a way to talk about iterated later modalities: *)
Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
Nat.iter n uPred_later P.
Instance: Params (@uPred_laterN) 2.
Notation "▷^ n P" := (uPred_laterN n P)
(at level 20, n at level 9, right associativity,
format "▷^ n P") : uPred_scope.
Definition uPred_nnvs {M} (P: uPred M) : uPred M :=
n, (P - ^n False) - ^n False.
Notation "|=n=> Q" := (uPred_nnvs Q)
(at level 99, Q at level 200, format "|=n=> Q") : uPred_scope.
Notation "P =n=> Q" := (P |=n=> Q)
(at level 99, Q at level 200, only parsing) : C_scope.
Notation "P =n=★ Q" := (P - |=n=> Q)%I
(at level 99, Q at level 200, format "P =n=★ Q") : uPred_scope.
(* Our goal is to prove that:
(1) |=n=> has (nearly) all the properties of the |=r=> modality that are used in Iris
(2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent
*)
Section rvs_nnvs.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Implicit Types x : M.
Import uPred.
(* Helper lemmas about iterated later modalities *)
Lemma laterN_big n a x φ: {n} x a n (^a ( φ))%I n x φ.
Proof.
induction 2 as [| ?? IHle].
- induction a; repeat (rewrite //= || uPred.unseal).
intros Hlater. apply IHa; auto using cmra_validN_S.
move:Hlater; repeat (rewrite //= || uPred.unseal).
- intros. apply IHle; auto using cmra_validN_S.
eapply uPred_closed; eauto using cmra_validN_S.
Qed.
Lemma laterN_small n a x φ: {n} x n < a (^a ( φ))%I n x.
Proof.
induction 2.
- induction n as [| n IHn]; [| move: IHn];
repeat (rewrite //= || uPred.unseal).
naive_solver eauto using cmra_validN_S.
- induction n as [| n IHn]; [| move: IHle];
repeat (rewrite //= || uPred.unseal).
red; rewrite //=. intros.
eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S.
Qed.
(* It is easy to show that most of the basic properties of rvs that
are used throughout Iris hold for nnvs.
In fact, the first three properties that follow hold for any
modality of the form (- - Q) - Q for arbitrary Q. The situation
here is slightly different, because nnvs is of the form
n, (- - (Q n)) - (Q n), but the proofs carry over straightforwardly.
*)
Lemma nnvs_intro P : P =n=> P.
Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed.
Lemma nnvs_mono P Q : (P Q) (|=n=> P) =n=> Q.
Proof.
intros HPQ. apply forall_intro=>n.
apply wand_intro_l. rewrite -{1}HPQ.
rewrite /uPred_nnvs (forall_elim n).
apply wand_elim_r.
Qed.
Lemma nnvs_frame_r P R : (|=n=> P) R =n=> P R.
Proof.
apply forall_intro=>n. apply wand_intro_r.
rewrite (comm _ P) -wand_curry.
rewrite /uPred_nnvs (forall_elim n).
by rewrite -assoc wand_elim_r wand_elim_l.
Qed.
Lemma nnvs_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x =n=> y, Φ y uPred_ownM y.
Proof.
intros Hrvs. split. rewrite /uPred_nnvs. repeat uPred.unseal.
intros n y ? Hown a.
red; rewrite //= => n' yf ??.
inversion Hown as (x'&Hequiv).
edestruct (Hrvs n' (Some (x' yf))) as (y'&?&?); eauto.
{ by rewrite //= assoc -(dist_le _ _ _ _ Hequiv). }
case (decide (a n')).
- intros Hle Hwand.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' (y' x'))); eauto.
* rewrite comm -assoc. done.
* rewrite comm -assoc. done.
* eexists. split; eapply uPred_mono; red; rewrite //=; eauto.
- intros; assert (n' < a). omega.
move: laterN_small. uPred.unseal.
naive_solver.
Qed.
(* However, the transitivity property seems to be much harder to
prove. This is surprising, because transitivity does hold for
modalities of the form (- - Q) - Q. What goes wrong when we quantify
now over n?
*)
Remark nnvs_trans P: (|=n=> |=n=> P) (|=n=> P).
Proof.
rewrite /uPred_nnvs.
apply forall_intro=>a. apply wand_intro_l.
rewrite (forall_elim a).
rewrite (nnvs_intro (P - _)).
rewrite /uPred_nnvs.
(* Oops -- the exponents of the later modality don't match up! *)
Abort.
(* Instead, we will need to prove this in the model. We start by showing that
nnvs is the limit of a the following sequence:
(- - False) - False,
(- - False) - False (- - False) - False,
(- - ^2 False) - ^2 False (- - False) - False (- - False) - False,
...
Then, it is easy enough to show that each of the uPreds in this sequence
is transitive. It turns out that this implies that nnvs is transitive. *)
(* The definition of the sequence above: *)
Fixpoint uPred_nnvs_k {M} k (P: uPred M) : uPred M :=
((P - ^k False) - ^k False)
match k with
O => True
| S k' => uPred_nnvs_k k' P
end.
Notation "|=n=>_ k Q" := (uPred_nnvs_k k Q)
(at level 99, k at level 9, Q at level 200, format "|=n=>_ k Q") : uPred_scope.
(* One direction of the limiting process is easy -- nnvs implies nnvs_k for each k *)
Lemma nnvs_trunc1 k P: (|=n=> P) |=n=>_k P.
Proof.
induction k.
- rewrite /uPred_nnvs_k /uPred_nnvs.
rewrite (forall_elim 0) //= right_id //.
- simpl. apply and_intro; auto.
rewrite /uPred_nnvs.
rewrite (forall_elim (S k)) //=.
Qed.
Lemma nnvs_k_elim n k P: n k ((|=n=>_k P) (P - (^n False)) (^n False))%I.
Proof.
induction k.
- inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l.
- inversion 1; subst; rewrite //= ?right_id.
* rewrite and_elim_l. apply wand_elim_l.
* rewrite and_elim_r IHk //.
Qed.
Lemma nnvs_k_unfold k P:
(|=n=>_(S k) P) ⊣⊢ ((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P).
Proof. done. Qed.
Lemma nnvs_k_unfold' k P n x:
(|=n=>_(S k) P)%I n x (((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P))%I n x.
Proof. done. Qed.
Lemma nnvs_k_weaken k P: (|=n=>_(S k) P) |=n=>_k P.
Proof. by rewrite nnvs_k_unfold and_elim_r. Qed.
(* Now we are ready to show nnvs is the limit -- ie, for each k, it is within distance k
of the kth term of the sequence *)
Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I {k} (|=n=>_k P)%I.
split; intros n' x Hle Hx. split.
- by apply (nnvs_trunc1 k).
- revert n' x Hle Hx; induction k; intros n' x Hle Hx;
rewrite ?nnvs_k_unfold' /uPred_nnvs.
* rewrite //=. unseal.
inversion Hle; subst.
intros (HnnP&_) n k' x' ?? HPF.
case (decide (k' < n)).
** move: laterN_small; uPred.unseal; naive_solver.
** intros. exfalso. eapply HnnP; eauto.
assert (n k'). omega.
intros n'' x'' ???.
specialize (HPF n'' x''). exfalso.
eapply laterN_big; last (unseal; eauto).
eauto. omega.
* inversion Hle; subst.
** unseal. intros (HnnP&HnnP_IH) n k' x' ?? HPF.
case (decide (k' < n)).
*** move: laterN_small; uPred.unseal; naive_solver.
*** intros. exfalso. assert (n k'). omega.
assert (n = S k n < S k) as [->|] by omega.
**** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
**** move:nnvs_k_elim. unseal. intros Hnnvsk.
eapply laterN_big; eauto. unseal.
eapply (Hnnvsk n k); first omega; eauto.
exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
eapply cmra_validN_op_l; eauto.
** intros HP. eapply IHk; auto.
move:HP. unseal. intros (?&?); naive_solver.
Qed.
(* nnvs_k has a number of structural properties, including transitivity *)
Lemma nnvs_k_intro k P: P (|=n=>_k P).
Proof.
induction k; rewrite //= ?right_id.
- apply wand_intro_l. apply wand_elim_l.
- apply and_intro; auto.
apply wand_intro_l. apply wand_elim_l.
Qed.
Lemma nnvs_k_mono k P Q: (P Q) (|=n=>_k P) (|=n=>_k Q).
Proof.
induction k; rewrite //= ?right_id=>HPQ.
- do 2 (apply wand_mono; auto).
- apply and_mono; auto; do 2 (apply wand_mono; auto).
Qed.
Instance nnvs_k_mono' k: Proper (() ==> ()) (@uPred_nnvs_k M k).
Proof. by intros P P' HP; apply nnvs_k_mono. Qed.
Instance nnvs_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnvs_k M k).
Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
Lemma nnvs_k_proper k P Q: (P ⊣⊢ Q) (|=n=>_k P) ⊣⊢ (|=n=>_k Q).
Proof. intros HP; apply (anti_symm ()); eapply nnvs_k_mono; by rewrite HP. Qed.
Instance nnvs_k_proper' k: Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_nnvs_k M k).
Proof. by intros P P' HP; apply nnvs_k_proper. Qed.
Lemma nnvs_k_trans k P: (|=n=>_k |=n=>_k P) (|=n=>_k P).
Proof.
revert P.
induction k; intros P.
- rewrite //= ?right_id. apply wand_intro_l.
rewrite {1}(nnvs_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r.
- rewrite {2}(nnvs_k_unfold k P).
apply and_intro.
* rewrite (nnvs_k_unfold k P). rewrite and_elim_l.
rewrite nnvs_k_unfold. rewrite and_elim_l.
apply wand_intro_l.
rewrite {1}(nnvs_k_intro (S k) (P - ^(S k) (False)%I)).
rewrite nnvs_k_unfold and_elim_l. apply wand_elim_r.
* do 2 rewrite nnvs_k_weaken //.
Qed.
Lemma nnvs_trans P : (|=n=> |=n=> P) =n=> P.
Proof.
split=> n x ? Hnn.
eapply nnvs_nnvs_k_dist in Hnn; eauto.
eapply (nnvs_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto;
[| symmetry; eapply nnvs_nnvs_k_dist].
eapply nnvs_nnvs_k_dist; eauto.
by apply nnvs_k_trans.
Qed.
(* Now that we have shown nnvs has all of the desired properties of
rvs, we go further and show it is in fact equivalent to rvs! The
direction from rvs to nnvs is similar to the proof of
nnvs_ownM_updateP *)
Lemma rvs_nnvs P: (|=r=> P) |=n=> P.
Proof.
split. rewrite /uPred_nnvs. repeat uPred.unseal. intros n x ? Hrvs a.
red; rewrite //= => n' yf ??.
edestruct Hrvs as (x'&?&?); eauto.
case (decide (a n')).
- intros Hle Hwand.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
* rewrite comm. done.
* rewrite comm. done.
- intros; assert (n' < a). omega.
move: laterN_small. uPred.unseal.
naive_solver.
Qed.
(* However, the other direction seems to need a classical axiom: *)
Section classical.
Context (not_all_not_ex: (P : M Prop), ¬ ( n : M, ¬ P n) n : M, P n).
Lemma nnvs_rvs P: (|=n=> P) (|=r=> P).
Proof.
rewrite /uPred_nnvs.
split. uPred.unseal; red; rewrite //=.
intros n x ? Hforall k yf Hle ?.
apply not_all_not_ex.
intros Hfal.
specialize (Hforall k k).
eapply laterN_big; last (uPred.unseal; red; rewrite //=; eapply Hforall);
eauto.
red; rewrite //= => n' x' ???.
case (decide (n' = k)); intros.
- subst. exfalso. eapply Hfal. rewrite (comm op); eauto.
- assert (n' < k). omega.
move: laterN_small. uPred.unseal. naive_solver.
Qed.
End classical.
(* We might wonder whether we can prove an adequacy lemma for nnvs. We could combine
the adequacy lemma for rvs with the previous result to get adquacy for nnvs, but
this would rely on the classical axiom we needed to prove the equivalence! Can
we establish adequacy without axioms? Unfortunately not, because adequacy for
nnvs would imply double negation elimination, which is classical: *)
Lemma nnvs_dne φ: True (|=n=> ((¬¬ φ φ)): uPred M)%I.
Proof.
rewrite /uPred_nnvs. apply forall_intro=>n.
apply wand_intro_l. rewrite ?right_id.
assert ( φ, ¬¬¬¬φ ¬¬φ) by naive_solver.
assert (Hdne: ¬¬ (¬¬φ φ)) by naive_solver.
split. unseal. intros n' ?? Hvs.
case (decide (n' < n)).
- intros. move: laterN_small. unseal. naive_solver.
- intros. assert (n n'). omega.
exfalso. specialize (Hvs n' ).
eapply Hdne. intros Hfal.
eapply laterN_big; eauto.
unseal. rewrite right_id in Hvs *; naive_solver.
Qed.
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
under classical axioms) directly without passing through the proofs for rvs: *)
Lemma adequacy_helper1 P n k x:
{S n + k} x ¬¬ (Nat.iter (S n) (λ P, |=n=> P)%I P (S n + k) x)
¬¬ ( x', {n + k} (x') Nat.iter n (λ P, |=n=> P)%I P (n + k) (x')).
Proof.
revert k P x. induction n.
- rewrite /uPred_nnvs. unseal=> k P x Hx Hf1 Hf2.
eapply Hf1. intros Hf3.
eapply (laterN_big (S k) (S k)); eauto.
specialize (Hf3 (S k) (S k) ). rewrite right_id in Hf3 *. unseal.
intros Hf3. eapply Hf3; eauto.
intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
unseal.
assert (n' < S k n' = S k) as [|] by omega.
* intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
eapply Hsmall; eauto.
* subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
- intros k P x Hx. rewrite ?Nat_iter_S_r.
replace (S (S n) + k) with (S n + (S k)) by omega.
replace (S n + k) with (n + (S k)) by omega.
intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by omega. eauto.
rewrite ?Nat_iter_S_r. eauto.
Qed.
Lemma adequacy_helper2 P n k x:
{S n + k} x ¬¬ (Nat.iter (S n) (λ P, |=n=> P)%I P (S n + k) x)
¬¬ ( x', {k} (x') Nat.iter 0 (λ P, |=n=> P)%I P k (x')).
Proof.
revert x. induction n.
- specialize (adequacy_helper1 P 0). rewrite //=. naive_solver.
- intros ?? Hfal%adequacy_helper1; eauto using cmra_validN_S.
intros Hfal'. eapply Hfal. intros (x''&?&?).
eapply IHn; eauto.
Qed.
Lemma adequacy φ n : (True Nat.iter n (λ P, |=n=> P) ( φ)) ¬¬ φ.
Proof.
cut ( x, {S n} x Nat.iter n (λ P, |=n=> P)%I ( φ)%I (S n) x ¬¬φ).
{ intros help H. eapply (help ); eauto using ucmra_unit_validN.
eapply H; try unseal; eauto using ucmra_unit_validN. red; rewrite //=. }
destruct n.
- rewrite //=; unseal; auto.
- intros ??? Hfal.
eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by omega); eauto.
unseal. intros (x'&?&Hphi). simpl in *.
eapply Hfal. auto.
Qed.
(* Open question:
Do the basic properties of the |=r=> modality (rvs_intro, rvs_mono, rvs_trans, rvs_frame_r,
rvs_ownM_updateP, and adequacy) uniquely characterize |=r=>?
*)
End rvs_nnvs.
\ No newline at end of file
From iris.heap_lang Require Export notation.
Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", "x" <- #1.
Definition newbarrier : val := λ: <>, ref #false.
Definition signal : val := λ: "x", "x" <- #true.
Definition wait : val :=
rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
rec: "wait" "x" := if: !"x" then #() else "wait" "x".
Global Opaque newbarrier signal wait.
......@@ -28,7 +28,7 @@ Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
(P - [ set] i I, Ψ i) [ set] i I, saved_prop_own i (Ψ i))%I.
Coercion state_to_val (s : state) : val :=
match s with State Low _ => #0 | State High _ => #1 end.
match s with State Low _ => #false | State High _ => #true end.
Arguments state_to_val !_ / : simpl nomatch.
Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ :=
......@@ -145,7 +145,7 @@ Proof.
{ iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
iVsIntro. wp_op=> ?; simplify_eq; wp_if.
iVsIntro. wp_if.
iApply ("IH" with "Hγ [HQR] HΦ"). auto.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
......@@ -157,7 +157,7 @@ Proof.
{ iSplit; [iPureIntro; by eauto using wait_step|].
iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iVsIntro. wp_op=> ?; simplify_eq/=; wp_if.
iVsIntro. wp_if.
iVsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
......
......@@ -9,7 +9,7 @@ Definition par : val :=
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
Pair "v1" "v2".
("v1", "v2").
Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Global Opaque par.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Import auth.
From iris.proofmode Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset.
From iris.algebra Require Import auth gset.
From iris.heap_lang.lib Require Export lock.
Import uPred.
Definition wait_loop: val :=
rec: "wait_loop" "x" "lock" :=
let: "o" := !(Fst "lock") in
rec: "wait_loop" "x" "lk" :=
let: "o" := !(Fst "lk") in
if: "x" = "o"
then #() (* my turn *)
else "wait_loop" "x" "lock".
else "wait_loop" "x" "lk".
Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition acquire : val :=
rec: "acquire" "lock" :=
let: "n" := !(Snd "lock") in
if: CAS (Snd "lock") "n" ("n" + #1)
then wait_loop "n" "lock"
else "acquire" "lock".