diff --git a/_CoqProject b/_CoqProject
index 9ae0b82edd228152b290a23f9ccc2d7b27f59255..1d657fb0b77749dc969a58d08aa84c78ebdc25c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -91,6 +91,7 @@ theories/hocap/lib/oneshot.v
theories/hocap/concurrent_runners.v
theories/hocap/parfib.v
+theories/logatom/cinc.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/elimination_stack/hocap_spec.v
diff --git a/opam b/opam
index 9931da432855c6ff50d0501d5a5cea0071aa048d..89cd8efae6d2bbbb81848b0d3083e715c30d0a5a 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
- "coq-iris" { (= "dev.2019-05-31.0.5c07c3be") | (= "dev") }
+ "coq-iris" { (= "dev.2019-06-03.2.b368c861") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logatom/cinc.v b/theories/logatom/cinc.v
new file mode 100644
index 0000000000000000000000000000000000000000..1f010799ac1c7d09639ad7ce1965c0ec5635b4f0
--- /dev/null
+++ b/theories/logatom/cinc.v
@@ -0,0 +1,985 @@
+From iris.algebra Require Import excl auth agree frac list cmra.
+From iris.base_logic.lib Require Export invariants.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Import uPred bi List Decidable.
+Set Default Proof Using "Type".
+
+(** Using prophecy variables with helping: implementing conditional counter from
+ "Logical Relations for Fine-Grained Concurrency" by Turon et al. (POPL 2013) *)
+
+(** * Implementation of the functions. *)
+
+(*
+ new_counter() :=
+ let c = ref (injL 0) in
+ let f = ref false in
+ ref (f, c)
+ *)
+Definition new_counter : val :=
+ λ: <>,
+ let: "c" := ref (ref (InjL #0)) in
+ let: "f" := ref #true in
+ ("f", "c").
+
+(*
+ set_flag(ctr, b) :=
+ ctr.1 <- b
+ *)
+Definition set_flag : val :=
+ λ: "ctr" "b",
+ Fst "ctr" <- "b".
+
+(*
+ complete(c, f, x, n, p) :=
+ Resolve CAS(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
+ *)
+Definition complete : val :=
+ λ: "c" "f" "x" "n" "p",
+ Resolve (CAS "c" "x" (ref (InjL (if: !"f" then "n" + #1 else "n")))) "p" (ref #()) ;; #().
+
+(*
+ get(c, f) :=
+ let x = !c in
+ match !x with
+ | injL n => n
+ | injR (n, p) => complete c f x n p; get(c, f)
+ *)
+Definition get : val :=
+ rec: "get" "ctr" :=
+ let: "f" := Fst "ctr" in
+ let: "c" := Snd "ctr" in
+ let: "x" := !"c" in
+ match: !"x" with
+ InjL "n" => "n"
+ | InjR "args" =>
+ complete "c" "f" "x" (Fst "args") (Snd "args") ;;
+ "get" "ctr"
+ end.
+
+(*
+ cinc(c, f) :=
+ let x = !c in
+ match !x with
+ | injL n =>
+ let p := new proph in
+ let y := ref (injR (n, p)) in
+ if CAS(c, x, y) then complete(c, f, y, n, p)
+ else cinc(c, f)
+ | injR (n, p) =>
+ complete(c, f, x, n, p);
+ cinc(c, f)
+ *)
+Definition cinc : val :=
+ rec: "cinc" "ctr" :=
+ let: "f" := Fst "ctr" in
+ let: "c" := Snd "ctr" in
+ let: "x" := !"c" in
+ match: !"x" with
+ InjL "n" =>
+ let: "p" := NewProph in
+ let: "y" := ref (InjR ("n", "p")) in
+ if: CAS "c" "x" "y" then complete "c" "f" "y" "n" "p" ;; Skip
+ else "cinc" "ctr"
+ | InjR "args'" =>
+ complete "c" "f" "x" (Fst "args'") (Snd "args'") ;;
+ "cinc" "ctr"
+ end.
+
+(** ** Proof setup *)
+
+(** To represent histories of allocated locations, we need some helper lemmas
+ about suffixes on lists. *)
+Section suffixes.
+
+ Lemma suffix_trans (h1 h2 h3 : list loc) :
+ h1 `suffix_of` h2 →
+ h2 `suffix_of` h3 →
+ h1 `suffix_of` h3.
+ Proof.
+ intros [? ->] [? ->]. rewrite app_assoc. by eexists.
+ Qed.
+
+ Lemma suffix_eq (h1 h2 : list loc) :
+ h1 `suffix_of` h2 →
+ h2 `suffix_of` h1 →
+ h1 = h2.
+ Proof.
+ intros [xs ->] [ys Heq]. rewrite <- app_nil_l in Heq at 1. rewrite app_assoc in Heq.
+ apply app_inv_tail, eq_sym in Heq. by apply app_eq_nil in Heq as [_ ->].
+ Qed.
+
+ Lemma suffix_in (h1 h2 : list loc) l :
+ h1 `suffix_of` h2 →
+ In l h1 →
+ In l h2.
+ Proof.
+ destruct h1 as [|y ys]; first done.
+ intros Hs Hin. destruct Hs as [l2' ->]. apply in_or_app. by right.
+ Qed.
+
+ Lemma suffix_in_head (h1 h2 : list loc) l :
+ h1 `suffix_of` h2 →
+ Some l = head h1 →
+ In l h2.
+ Proof.
+ destruct h1 as [|y ys]; first done.
+ intros Hs [=->]. eapply suffix_in; first done. apply in_eq.
+ Qed.
+
+ (** A helper lemma that will come up in the proof of [complete] *)
+ Lemma nodup_suffix_contradiction (l1 l2 l3 : loc) (H1 H2 H3 : list loc) :
+ Some l1 = hd_error H1 →
+ Some l2 = hd_error H2 →
+ Some l3 = hd_error H3 →
+ In l3 H1 →
+ H1 `suffix_of` H2 →
+ H2 `suffix_of` H3 →
+ l2 ≠l3 →
+ NoDup H3 →
+ False.
+ Proof.
+ intros Heq Heq' Heq'' Hin Hs Hs' Hn Hd.
+ destruct Hs' as [xs ->]. destruct Hs as [ys ->]. destruct (in_split _ _ Hin) as (x & y & ->).
+ do 2 rewrite app_assoc in Hd. apply NoDup_remove_2 in Hd.
+ (* xs, ys, and x must be empty *)
+ destruct xs as [|x' xs]; last first.
+ { simpl in *. inversion Heq''. subst.
+ contradict Hd. by left. }
+ destruct ys as [|y' ys]; last first.
+ { simpl in *. inversion Heq''; subst.
+ contradict Hd. by left. }
+ destruct x as [|z' zs]; last first.
+ { simpl in *. inversion Heq''; subst.
+ contradict Hd. by left. }
+ simpl in *. inversion Heq'; done.
+ Qed.
+
+End suffixes.
+
+(** Resource algebra for histories *)
+Section histories.
+
+ Inductive hist :=
+ | histv (h : list loc) : hist
+ | histbot : hist.
+
+ Inductive hist_equiv : Equiv hist :=
+ | Hist_equiv h1 h2 : h1 = h2 → h1 ≡ h2.
+
+ Existing Instance hist_equiv.
+
+ Instance hist_equiv_Equivalence : @Equivalence hist equiv.
+ Proof.
+ split.
+ - move => [|]; by constructor.
+ - move => [?|] []; inversion 1; subst; by constructor.
+ - move => [?|] [] [];
+ inversion 1; inversion 1; subst; by constructor.
+ Qed.
+
+ Canonical Structure histC : ofeT := discreteC hist.
+
+ Instance hist_valid : Valid hist :=
+ λ x, match x with histv _ => True | histbot => False end.
+
+ Instance hist_op : Op hist := λ h1 h2,
+ match h1, h2 with
+ | histv h1', histv h2' =>
+ if decide (h1' `suffix_of` h2')
+ then h2
+ else if decide (h2' `suffix_of` h1')
+ then h1
+ else histbot
+ | _, _ =>
+ histbot
+ end.
+
+ Arguments op _ _ !_ !_ /.
+
+ Instance hist_PCore : PCore hist := Some.
+
+ Global Instance hist_op_comm: Comm equiv hist_op.
+ Proof.
+ intros [h1|] [h2|]; auto. simpl.
+ case_decide as H1; [case_decide as H2|auto]; last auto.
+ constructor. destruct H1. subst. destruct H2.
+ rewrite <- app_nil_l in H at 1. rewrite app_assoc in H.
+ by apply app_inv_tail, eq_sym, app_eq_nil in H as [-> ->].
+ Qed.
+
+ Global Instance hist_op_idemp : IdemP eq hist_op.
+ Proof. intros [|]; [by simpl; rewrite decide_True|auto]. Qed.
+
+ Lemma hist_op_l h1 h2 (Le: h1 `suffix_of` h2) :
+ histv h1 â‹… histv h2 = histv h2.
+ Proof. simpl. case_decide; done. Qed.
+
+ Lemma hist_op_r h1 h2 (Le: h1 `suffix_of` h2) :
+ histv h2 â‹… histv h1 = histv h2.
+ Proof.
+ simpl. case_decide.
+ - f_equal. by apply suffix_eq.
+ - by case_decide.
+ Qed.
+
+ Global Instance hist_op_assoc: Assoc equiv (op: Op hist).
+ Proof.
+ intros [h1|] [h2|] [h3|]; eauto; simpl.
+ - repeat (case_decide; auto).
+ + rewrite !hist_op_l; auto. etrans; eauto.
+ + simpl. repeat case_decide; last done.
+ * destruct H as [xs ->]. destruct H2 as [ys [[k [->->]] | [k [->->]]]%app_eq_inv].
+ ** contradict H1. by apply suffix_app_r.
+ ** contradict H0. by apply suffix_app_r.
+ * contradict H1. by etrans.
+ + rewrite hist_op_l; [by rewrite hist_op_r|auto].
+ + rewrite !hist_op_r; auto. by etrans.
+ + simpl. rewrite !decide_False; auto.
+ + simpl. rewrite !decide_False; auto.
+ + simpl. case_decide.
+ * exfalso. apply H. by etrans.
+ * case_decide; last done. exfalso.
+ destruct H4 as [xs ->]. destruct H2 as [ys [[k [->->]] | [k [->->]]]%app_eq_inv].
+ ** contradict H0. by apply suffix_app_r.
+ ** contradict H. by apply suffix_app_r.
+ - simpl. repeat case_decide; auto.
+ Qed.
+
+ Lemma hist_included h1 h2 :
+ histv h1 ≼ histv h2 ↔ h1 `suffix_of` h2.
+ Proof.
+ split.
+ - move => [[?|]]; simpl; last by inversion 1.
+ case_decide.
+ * inversion 1. naive_solver.
+ * case_decide; inversion 1; naive_solver.
+ - intros. exists (histv h2). by rewrite hist_op_l.
+ Qed.
+
+ Lemma hist_valid_op h1 h2 :
+ ✓ (histv h1 ⋅ histv h2) → h1 `suffix_of` h2 ∨ h2 `suffix_of` h1.
+ Proof. simpl. case_decide; first by left. case_decide; [by right|done]. Qed.
+
+ Lemma hist_core_self (X: hist) : core X = X.
+ Proof. done. Qed.
+
+ Instance hist_unit : Unit hist := histv nil.
+
+ Definition hist_ra_mixin : RAMixin hist.
+ Proof.
+ apply ra_total_mixin; eauto.
+ - intros [?|] [?|] [?|]; auto; inversion 1; naive_solver.
+ - by destruct 1; constructor.
+ - destruct 1. naive_solver.
+ - apply hist_op_assoc.
+ - apply hist_op_comm.
+ - intros ?. by rewrite hist_core_self idemp_L.
+ - intros [|] [|]; simpl; done.
+ Qed.
+
+ Canonical Structure histR := discreteR hist hist_ra_mixin.
+
+ Global Instance hist_cmra_discrete : CmraDiscrete histR.
+ Proof. apply discrete_cmra_discrete. Qed.
+
+ Global Instance hist_core (h: hist) : CoreId h.
+ Proof.
+ rewrite /CoreId. reflexivity.
+ Qed.
+
+ Definition hist_ucmra_mixin : UcmraMixin hist.
+ Proof.
+ split; [done| |auto]. intros [|]; [simpl|done]. done.
+ Qed.
+
+ Lemma hist_local_update h1 X h2 :
+ h1 `suffix_of` h2 → (histv h1, X) ~l~> (histv h2, histv h2).
+ Proof.
+ intros Le. rewrite local_update_discrete.
+ move => [[h3|]|] /= ? Eq; split => //; last first; move : Eq.
+ - destruct X; by inversion 1.
+ - destruct X; rewrite /cmra_op /= => Eq;
+ repeat case_decide; auto; inversion Eq; subst; try naive_solver.
+ + constructor. inversion H1. subst. f_equal. by apply suffix_eq.
+ + constructor. inversion H2. subst. f_equal. apply suffix_eq; by etrans.
+ + inversion H3; subst. by apply (suffix_trans _ _ _ H0) in Le.
+ Qed.
+
+ Canonical Structure histUR := UcmraT hist hist_ucmra_mixin.
+
+End histories.
+
+Definition histListUR := optionUR $ prodR fracR $ agreeR $ listC locC.
+
+Definition historyUR := prodUR (authUR histListUR) (authUR histUR).
+Definition flagUR := authR $ optionUR $ exclR boolC.
+Definition numUR := authR $ optionUR $ exclR ZC.
+Definition tokenUR := authR $ optionUR $ exclR valC.
+
+Class cincG Σ := ConditionalIncrementG {
+ cinc_historyG :> inG Σ historyUR;
+ cinc_flagG :> inG Σ flagUR;
+ cinc_numG :> inG Σ numUR;
+ cinc_tokenG :> inG Σ tokenUR;
+ }.
+
+Definition cincΣ : gFunctors :=
+ #[GFunctor historyUR; GFunctor flagUR; GFunctor numUR; GFunctor tokenUR].
+
+Instance subG_cincΣ {Σ} : subG cincΣ Σ → cincG Σ.
+Proof. solve_inG. Qed.
+
+Section conditional_counter.
+ Context {Σ} `{!heapG Σ, !cincG Σ}.
+ Context (N : namespace).
+
+ Local Definition stateN := N .@ "state".
+ Local Definition counterN := N .@ "counter".
+
+ Definition token : tokenUR :=
+ â— Excl' #().
+
+ Definition histList (H : list loc) (q : Qp) : histListUR :=
+ Some (q, to_agree H).
+
+ Definition half_history_frag (H : list loc) : historyUR :=
+ (â—¯ (histList H (1/2)%Qp), â—¯ (histv H)).
+
+ Definition full_history_frag (H : list loc) : historyUR :=
+ (â—¯ (histList H 1%Qp), â—¯ (histv H)).
+
+ Definition full_history_auth (H : list loc) : historyUR :=
+ (â— (histList H 1%Qp), â— (histv H)).
+
+ Definition hist_snapshot H : historyUR :=
+ (â—¯ None, â—¯ histv H).
+
+ Global Instance snapshot_persistent H γ_h : Persistent (own γ_h (hist_snapshot H)).
+ Proof.
+ apply own_core_persistent. rewrite /CoreId. done.
+ Qed.
+
+ (** Updating and synchronizing history RAs *)
+
+ Lemma sync_histories H1 H2 γ_h :
+ own γ_h (half_history_frag H1) -∗ own γ_h (half_history_frag H2) -∗ ⌜H1 = H2âŒ.
+ Proof.
+ iIntros "H1 H2". iCombine "H1" "H2" as "H". iPoseProof (own_valid with "H") as "H".
+ iDestruct "H" as %H. iPureIntro. destruct H as [[_ Hl1%agree_op_inv] _].
+ by apply to_agree_inj, leibniz_equiv in Hl1.
+ Qed.
+
+ Lemma add_half_histories (H : list loc) γ_h :
+ own γ_h (half_history_frag H) -∗
+ own γ_h (half_history_frag H) -∗
+ own γ_h (full_history_frag H).
+ Proof.
+ iIntros "H1 H2". iCombine "H1" "H2" as "H". done.
+ Qed.
+
+ Lemma update_history H H' l γ_h :
+ own γ_h (full_history_auth H) -∗
+ own γ_h (half_history_frag H) -∗
+ own γ_h (half_history_frag H') ==∗
+ own γ_h (full_history_auth (l :: H)) ∗
+ own γ_h (half_history_frag (l :: H)) ∗
+ own γ_h (half_history_frag (l :: H)).
+ Proof.
+ iIntros "Hâ— H1â—¯ H2â—¯". iDestruct (sync_histories with "H1â—¯ H2â—¯") as %<-.
+ iDestruct (add_half_histories with "H1â—¯ H2â—¯") as "Hâ—¯".
+ iCombine "Hâ— Hâ—¯" as "H". rewrite -own_op -own_op.
+ iApply (own_update with "H"). apply prod_update.
+ - apply auth_update, option_local_update. rewrite pair_op frac_op' agree_idemp.
+ rewrite Qp_div_2. apply exclusive_local_update. by constructor.
+ - apply auth_update. simpl. rewrite hist_op_l; last done.
+ by apply hist_local_update, suffix_cons_r.
+ Qed.
+
+ Lemma sync_snapshot H1 H2 H2' γ_h :
+ own γ_h (full_history_auth H1) -∗ own γ_h (â—¯ H2', â—¯ histv H2) -∗ ⌜H2 `suffix_of` H1âŒ.
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H".
+ by iDestruct (own_valid with "H") as %[_ [Hs%hist_included _]%auth_both_valid].
+ Qed.
+
+ Lemma extract_snapshot H γ_h :
+ own γ_h (half_history_frag H) -∗ □ own γ_h (hist_snapshot H).
+ Proof.
+ iIntros "H".
+ iAssert (own γ_h (half_history_frag H) ∗ own γ_h (hist_snapshot H))%I with "[H]" as "[_ H2]".
+ { rewrite -own_op pair_op.
+ assert (â—¯ histList H (1 / 2) â‹… â—¯ None = â—¯ (histList H (1 / 2) â‹… None)) as Heq by apply auth_frag_op.
+ assert (â—¯ histv H â‹… â—¯ histv H = â—¯ (histv H â‹… histv H)) as Heq' by apply auth_frag_op.
+ rewrite Heq Heq' right_id. rewrite <- core_id_dup; first done. by rewrite /CoreId. }
+ rewrite intuitionistically_into_persistently.
+ by iApply persistent.
+ Qed.
+
+ Lemma sync_counter_values γ_n (n m : Z) :
+ own γ_n (â— Excl' n) -∗ own γ_n (â—¯ Excl' m) -∗ ⌜n = mâŒ.
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H". iDestruct (own_valid with "H") as "H".
+ by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
+ Qed.
+
+
+ (** Updating and synchronizing the counter and flag RAs *)
+
+ Lemma sync_flag_values γ_n (b1 b2 : bool) :
+ own γ_n (â— Excl' b1) -∗ own γ_n (â—¯ Excl' b2) -∗ ⌜b1 = b2âŒ.
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H". iDestruct (own_valid with "H") as "H".
+ by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
+ Qed.
+
+ Lemma update_counter_value γ_n (n1 n2 m : Z) :
+ own γ_n (◠Excl' n1) -∗ own γ_n (◯ Excl' n2) ==∗ own γ_n (◠Excl' m) ∗ own γ_n (◯ Excl' m).
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H". rewrite -own_op. iApply (own_update with "H").
+ by apply auth_update, option_local_update, exclusive_local_update.
+ Qed.
+
+ Lemma update_flag_value γ_n (b1 b2 b : bool) :
+ own γ_n (◠Excl' b1) -∗ own γ_n (◯ Excl' b2) ==∗ own γ_n (◠Excl' b) ∗ own γ_n (◯ Excl' b).
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H". rewrite -own_op. iApply (own_update with "H").
+ by apply auth_update, option_local_update, exclusive_local_update.
+ Qed.
+
+ Definition counter_content (γs : gname * gname * gname) (c : bool * Z) :=
+ (own γs.1.2 (◯ Excl' c.1) ∗ own γs.2 (◯ Excl' c.2))%I.
+
+
+ (** Definition of the invariant *)
+
+ Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
+ match vs with
+ | (#true , LitV (LitLoc l)) :: _ => Some l
+ | _ :: vs => val_to_some_loc vs
+ | _ => None
+ end.
+
+ Lemma val_to_some_loc_some vs l :
+ val_to_some_loc vs = Some l →
+ ∃ v1 v2 vs', vs = (v1, v2) :: vs' ∧
+ ( (v1 = #true ∧ v2 = LitV (LitLoc l))
+ ∨ val_to_some_loc vs' = Some l).
+ Proof.
+ intros H. destruct vs as [|[v1 v2] vs']; first done.
+ exists v1, v2, vs'. split; first done.
+ destruct v1; try by right. destruct l0; try by right.
+ destruct b; try by right. destruct v2; try by right.
+ destruct l0; try by right. simpl in H. inversion H. by left.
+ Qed.
+
+ Inductive abstract_state : Set :=
+ | injl : Z → abstract_state
+ | injr : Z → proph_id → abstract_state.
+
+ Definition own_token γ_t := (own γ_t token)%I.
+
+ Definition used_up l γ_h :=
+ (∃ H, â–¡ own γ_h (hist_snapshot H) ∗ ⌜In l H ∧ Some l ≠head HâŒ)%I.
+
+ Definition not_done_state H l (γ_h : gname) :=
+ (own γ_h (half_history_frag H) ∗ ⌜Some l = head HâŒ)%I.
+
+ Definition pending_state P (n : Z) vs l_ghost (γ_h γ_n : gname) :=
+ (P ∗ ⌜match val_to_some_loc vs with None => True | Some l => l = l_ghost end⌠∗ own γ_n (◠Excl' n))%I.
+
+ Definition accepted_state Q vs (l l_ghost : loc) (γ_h : gname) :=
+ (l_ghost ↦{1/2} - ∗ match val_to_some_loc vs with None => True | Some l => ⌜l = l_ghost⌠∗ Q end)%I.
+
+ Definition done_state Q (l l_ghost : loc) (γ_t γ_h : gname) :=
+ ((Q ∨ own_token γ_t) ∗ l_ghost ↦ - ∗ used_up l γ_h)%I.
+
+ Definition state_inv P Q (p : proph_id) n l l_ghost H γ_h γ_n γ_t : iProp Σ :=
+ (∃ vs, proph p vs ∗
+ ((not_done_state H l γ_h ∗
+ ( pending_state P n vs l_ghost γ_h γ_n
+ ∨ accepted_state Q vs l l_ghost γ_h ))
+ ∨ done_state Q l l_ghost γ_t γ_h))%I.
+
+ Definition pau P Q γs :=
+ (▷ P -∗ ◇ AU << ∀ (b : bool) (n : Z), counter_content γs (b, n) >> @ ⊤∖↑N, ∅
+ << counter_content γs (b, (if b then n + 1 else n)), COMM Q >>)%I.
+
+ Definition counter_inv γ_h γ_b γ_n f c :=
+ (∃ (b : bool) (l : loc) (H : list loc) (q : Qp) (v : val),
+ f ↦ #b ∗ c ↦ #l ∗ l ↦{q} v ∗
+ own γ_h (full_history_auth H) ∗
+ own γ_h (half_history_frag H) ∗
+ ([∗ list] l ∈ H, ∃ q, l ↦{q} -) ∗
+ ⌜Some l = head H ∧ NoDup H⌠∗
+ own γ_b (◠Excl' b) ∗
+ ((∃ (n : Z), ⌜v = InjLV #n⌠∗ own γ_h (half_history_frag H) ∗ own γ_n (◠Excl' n)) ∨
+ (∃ (n : Z) (p : proph_id), ⌜v = InjRV(#n,#p)⌠∗
+ ∃ P Q l_ghost γ_t, inv stateN (state_inv P Q p n l l_ghost H γ_h γ_n γ_t) ∗
+ □ pau P Q (γ_h, γ_b, γ_n))))%I.
+
+ Definition is_counter (γs : gname * gname * gname) (ctr : val) :=
+ (∃ (γ_h γ_b γ_n : gname) (f c : loc),
+ ⌜γs = (γ_h, γ_b, γ_n) ∧ ctr = (#f, #c)%V⌠∗
+ inv counterN (counter_inv γ_h γ_b γ_n f c))%I.
+
+ Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.
+
+ Global Instance counter_content_timeless γs ctr : Timeless (counter_content γs ctr) := _.
+
+ Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (injl 0).
+
+
+ (** A few more helper lemmas that will come up later *)
+
+ Lemma mapsto_valid_3 l v1 v2 q :
+ l ↦ v1 -∗ l ↦{q} v2 -∗ ⌜FalseâŒ.
+ Proof.
+ iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %Hv.
+ apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
+ Qed.
+
+ Instance in_dec (l : loc) H: Decision (In l H).
+ Proof.
+ induction H as [|a H IH].
+ - right. naive_solver.
+ - destruct (decide (l = a)).
+ + left. naive_solver.
+ + destruct IH; [ left | right]; naive_solver.
+ Qed.
+
+ Lemma nodup_fresh_loc l v H:
+ NoDup H → l ↦ v -∗ ([∗ list] l ∈ H, ∃ q, l ↦{q} -) -∗ ⌜NoDup (l :: H)âŒ.
+ Proof.
+ intros Hd. iIntros "Hl Hls".
+ destruct (decide (In l H)) as [(x1 & x2 & ->)%in_split | Hn%NoDup_cons]; last done.
+ - destruct x1 as [|x1 x1s];
+ [ rewrite app_nil_l in Hd; rewrite app_nil_l; iDestruct "Hls" as "[Hl' _]" |
+ iDestruct "Hls" as "[_ [Hl' _]]" ];
+ iDestruct "Hl'" as (q v') "Hl'";
+ by iDestruct (mapsto_valid_3 with "Hl Hl'") as %?.
+ - by iPureIntro.
+ Qed.
+
+
+ (** ** Proof of [complete] *)
+
+ (** The part of [complete] for the succeeding thread that moves from [pending] to [accepted] state *)
+
+ Lemma complete_succeeding_thread_pending γ_h γ_b γ_n γ_t f_l c_l P Q p (m n : Z) l l_ghost l_new H Φ :
+ Some l = head H →
+ inv counterN (counter_inv γ_h γ_b γ_n f_l c_l) -∗
+ inv stateN (state_inv P Q p m l l_ghost H γ_h γ_n γ_t) -∗
+ pau P Q (γ_h, γ_b, γ_n) -∗
+ l_ghost ↦{1 / 2} #() -∗
+ ((own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
+ own γ_n (◠Excl' n) -∗
+ l_new ↦ InjLV #n -∗
+ WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
+ Proof.
+ iIntros (Heq) "#InvC #InvS PAU Hl_ghost HQ Hnâ— Hl_new". wp_bind (Resolve _ _ _)%E.
+ iInv counterN as (b' l' H' q v) "[>Hf [>Hc [>Hl' [>Hâ— [>Hâ—¯ [>HlH [>Heq [Hbâ— Hrest]]]]]]]]".
+ iDestruct "Heq" as %[Heq'' Hd']. simpl.
+ iDestruct ((nodup_fresh_loc _ _ _ Hd') with "Hl_new HlH") as %Hd''.
+ (* It must be that l' = l because we are in the succeeding thread. *)
+ destruct (decide (l' = l)) as [->|HNeq]; last first. {
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ _] State] | Done]]".
+ - iDestruct "State" as "[Pending | Accepted]".
+ + iDestruct "Pending" as "[_ >[_ Hnâ—']]".
+ iCombine "Hnâ—'" "Hnâ—" as "Contra".
+ iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
+ + iDestruct (sync_histories with "Hhâ—¯ Hâ—¯") as %->.
+ rewrite <- Heq'' in Heq. by inversion Heq.
+ - iDestruct "Done" as "[_ >[Hlghost _]]".
+ wp_apply (wp_resolve with "Hp'"); first done. wp_cas_fail.
+ iDestruct "Hlghost" as (?) "Hlghost".
+ by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost") as %?.
+ }
+ (* To apply the CAS, we need the prophecy variable, so we open the state invariant. *)
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] State] | Done]]".
+ - iDestruct "State" as "[Pending | Accepted]".
+ + (* Pending: contradiction. *)
+ iDestruct "Pending" as "[_ >[_ Hnâ—']]".
+ iCombine "Hnâ—" "Hnâ—'" as "Contra".
+ iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
+ + (* We perform the CAS. *)
+ iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
+ wp_apply (wp_resolve with "Hp'"); first done; wp_cas_suc.
+ destruct (val_to_some_loc vs') eqn:Hvtsl; last first. {
+ (* Wrong prophecy: contradiction. *)
+ iIntros (vs ->). inversion Hvtsl.
+ }
+ (* Update to Done. *)
+ iDestruct "Accepted" as "[Hl_ghost_inv H]".
+ rewrite Hvtsl. iDestruct "H" as "[HEq Q]".
+ (* The first element of H is l. *)
+ destruct H as [|l' H]; inversion Heq; subst l'.
+ (* And we have l ≠l_new. *)
+ destruct (decide (l = l_new)) as [->|HNeq]. {
+ iDestruct "HlH" as "[Hl HlH]". iDestruct "Hl" as (q' v') "Hl".
+ by iDestruct (mapsto_valid_3 with "Hl_new Hl") as %Contra.
+ }
+ (* Update histories. *)
+ iDestruct (update_history _ _ l_new with "Hâ— Hâ—¯ Hhâ—¯") as ">[Hhâ— [Hâ—¯ Hâ—¯']]".
+ iIntros (pv' ->) "Hp". iModIntro.
+ (* Extract snapshot to prove used_up. *)
+ iDestruct (extract_snapshot with "Hâ—¯'") as "#Hs".
+ iSplitL "Hl_ghost_inv Hl_ghost Q Hp".
+ (* Update state to Done. *)
+ { iNext. iExists _. iSplitL "Hp"; first done. repeat iRight.
+ iDestruct "Hl_ghost_inv" as (v'') "Hl_ghost''".
+ iDestruct (mapsto_agree with "Hl_ghost Hl_ghost''") as %<-.
+ iCombine "Hl_ghost" "Hl_ghost''" as "Hl_ghost'".
+ iSplitL "Q"; first by iFrame. iSplitL "Hl_ghost'"; first by eauto.
+ iExists (l_new :: l :: H). iSplit; first done. iPureIntro.
+ split; first by apply in_cons, in_eq. by intros [=->]. }
+ iModIntro. iSplitR "HQ".
+ { iNext. iExists _, _, _, _, _. iSplitL "Hf"; first done.
+ iSplitL "Hc"; first done. iDestruct "Hl_new" as "[$ Hl_new]".
+ iSplitL "Hhâ—"; first done. iSplitL "Hâ—¯'"; first done.
+ iSplitL "HlH Hl_new". { iSplitL "Hl_new"; first by iExists _, _. iFrame. }
+ iSplit; first done. iSplitL "Hbâ—"; first done. iLeft. iExists n. by iFrame. }
+ iApply wp_fupd. wp_seq. iApply "HQ". iModIntro. iIntros "Ht".
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] _] | Done]]".
+ * iInv counterN as (b5 l5 H5 q5 v5) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ _]]]]]".
+ iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
+ by iDestruct (sync_snapshot with "Hâ— Hs") as %?%suffix_cons_not.
+ * iDestruct "Done" as "[QT [>Hlghost Usedup]]".
+ iModIntro. iDestruct (later_intro with "Ht") as "Ht".
+ iDestruct (later_or with "QT") as "[Q | T]"; last first.
+ { iCombine "Ht" "T" as "Contra". iDestruct (own_valid with "Contra") as "#Contra'".
+ iSplitL; try iModIntro; try iNext; iDestruct "Contra'" as %Contra;
+ by inversion Contra. }
+ iSplitR "Q"; last done. iNext. iExists _. iSplitL "Hp'"; first done.
+ repeat iRight. iFrame.
+ - (* Done: contradiction. *)
+ iDestruct "Done" as "[QT [>Hlghost Usedup]]".
+ iDestruct "Hlghost" as (v') "Hlghost".
+ by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %?.
+ Qed.
+
+ (** The part of [complete] for the failing thread *)
+
+ Lemma complete_failing_thread γ_h γ_b γ_n γ_t f_l c_l l1 l H1 H P Q p m n l_ghost_inv l_ghost l_new Φ :
+ Some l1 = head H1 →
+ In l H1 →
+ l_ghost_inv ≠l_ghost →
+ inv counterN (counter_inv γ_h γ_b γ_n f_l c_l) -∗
+ inv stateN (state_inv P Q p m l l_ghost_inv H γ_h γ_n γ_t) -∗
+ pau P Q (γ_h, γ_b, γ_n) -∗
+ □ own γ_h (hist_snapshot H1) -∗
+ ((own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
+ l_new ↦ InjLV #n -∗
+ WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
+ Proof.
+ iIntros (Heq Hin Hnl) "#InvC #InvS PAU #Hs1 HQ Hl_new". wp_bind (Resolve _ _ _)%E.
+ iInv counterN as (b l' H' q v) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ [HlH [>Heq [Hbâ— Hrest]]]]]]]]".
+ iDestruct (extract_snapshot with "Hâ—¯") as "#Hs2".
+ iDestruct (sync_snapshot with "Hâ— Hs1") as %H12.
+ (* It must be that l' = l because we are in the succeeding thread. *)
+ destruct (decide (l' = l)) as [->|Hn]. {
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ _] State] | Done]]".
+ - wp_apply (wp_resolve with "Hp'"); first done; wp_cas_suc. iIntros (vs ->).
+ iDestruct "State" as "[Pending | Accepted]".
+ + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ + iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ - iDestruct "Done" as "[QT [>Hlghost Usedup]]".
+ iDestruct "Usedup" as (H'') "[Hs >Usedup]".
+ iDestruct "Usedup" as %[Hin' Hn].
+ iDestruct "Heq" as %[Heq' Hd'].
+ iMod (intuitionistically_elim with "Hs") as "Hs".
+ iDestruct (sync_snapshot with "Hâ— Hs") as %Hs'.
+ destruct Hs' as [xs ->]. destruct (in_split _ _ Hin) as (x & y & ->).
+ destruct xs as [|z zs]; first done.
+ simpl in *. inversion Heq'; subst. destruct (in_split _ _ Hin') as (x1 & x2 & ->).
+ rewrite app_comm_cons in Hd'. rewrite app_assoc in Hd'.
+ apply (NoDup_remove _ _ _) in Hd' as [_ Contra].
+ rewrite <- app_comm_cons in Contra. simpl in *. exfalso. eauto.
+ }
+ (* The CAS fails. *)
+ iInv stateN as (vs') "[>Hp' State]".
+ wp_apply (wp_resolve with "Hp'"); first done. wp_cas_fail.
+ iDestruct (extract_snapshot with "Hâ—¯") as "#Hs".
+ iIntros (vs ->) "Hp". iModIntro. iDestruct "Heq" as %[Heq' Hd'].
+ iSplitL "State Hp". { iNext. iExists vs. iFrame. } iModIntro.
+ iSplitL "Hf Hc Hl Hâ— Hâ—¯ HlH Hbâ— Hrest". { iNext. iExists _, _, _, _. eauto with iFrame. }
+ wp_seq. iApply "HQ". iIntros "Ht".
+ iInv counterN as (b3 l3 H3 q3 v3) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ [HlH [>Heq [Hbâ— Hrest]]]]]]]]".
+ iDestruct "Heq" as %[Heq'' Hd''].
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] _] | Done]]".
+ - iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
+ iDestruct (sync_snapshot with "Hâ— Hs") as %Hs.
+ iDestruct "Heq'" as %Heq'''. rewrite <- Heq'' in Heq'''.
+ inversion Heq'''. subst. exfalso.
+ by eapply (nodup_suffix_contradiction _ _ _ _ _ _ Heq Heq' Heq'').
+ - iDestruct "Done" as "[[Q | >T] Hrest']"; iModIntro.
+ + iSplitL "Ht Hp' Hrest'".
+ { iNext. iExists _. iSplitL "Hp'"; first done. repeat iRight. iFrame. }
+ iModIntro. iSplitR "Q"; last done. iNext. iExists _, _, _, _. eauto with iFrame.
+ + iCombine "T" "Ht" as "Contra".
+ iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
+ Qed.
+
+ (** ** Proof of [complete] *)
+
+ Lemma complete_spec (c f l : loc) H (n : Z) (p : proph_id) γs γ_t l_ghost_inv P Q :
+ is_counter γs (#f, #c) -∗
+ inv stateN (state_inv P Q p n l l_ghost_inv H γs.1.1 γs.2 γ_t) -∗
+ □ pau P Q γs -∗
+ {{{ True }}}
+ complete #c #f #l #n #p
+ {{{ RET #(); own_token γ_t ={⊤}=∗ ▷Q }}}.
+ Proof.
+ iIntros "#InvC #InvS #PAU". destruct γs as [[γ_h γ_b] γ_n].
+ iDestruct "InvC" as (??? f_l c_l [[=<-<-<-][=->->]]) "#InvC".
+ iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
+ wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_bind (! _)%E. simpl.
+ (* open outer invariant to read `f` *)
+ iInv counterN as (b1 l1 H1 q1 v1) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ [Hlh1 [>Heq [Hbâ— Hrest]]]]]]]]".
+ iDestruct "Heq" as %[Heq Hd]. wp_load.
+ (* two different proofs depending on whether we are succeeding thread *)
+ destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
+ - (* we are the succeeding thread *)
+ (* we need to move from pending to accepted. *)
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq] [Pending | Accepted]] | Done]]".
+ + (* Pending: update to accepted *)
+ iDestruct "Pending" as "[P >[Hvs Hnâ—]]". iDestruct "Heq" as %Heq'.
+ iDestruct ("PAU" with "P") as ">AU".
+ (* open AU, sync flag and counter *)
+ iMod "AU" as (b2 n2) "[CC [_ Hclose]]".
+ iDestruct "CC" as "[Hbâ—¯ Hnâ—¯]". simpl.
+ iDestruct (sync_flag_values with "Hbâ— Hbâ—¯") as %->.
+ iDestruct (sync_counter_values with "Hnâ— Hnâ—¯") as %->.
+ iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
+ rewrite <- Heq in Heq'. inversion_clear Heq'; subst.
+ iMod (update_counter_value _ _ _ (if b2 then n2 + 1 else n2) with "Hnâ— Hnâ—¯")
+ as "[Hnâ— Hnâ—¯]".
+ iMod ("Hclose" with "[Hnâ—¯ Hbâ—¯]") as "Q"; first by iFrame.
+ (* close state inv *)
+ iModIntro. iSplitL "Q Hâ—¯ Hl_ghost' Hp' Hvs".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
+ iSplitL "Hâ—¯"; first by iFrame. iRight. iSplitL "Hl_ghost'"; first by iExists _.
+ destruct (val_to_some_loc vs') eqn:Hvts; iFrame. }
+ (* close outer inv *)
+ iModIntro. iSplitR "Hl_ghost'2 HQ Hnâ—".
+ { iNext. iExists _, _, _, _, _. iFrame. done. }
+ destruct b2; wp_if; [ wp_op | .. ]; wp_alloc l_new as "Hl_new"; wp_pures;
+ iApply ((complete_succeeding_thread_pending _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq)
+ with "InvC InvS PAU Hl_ghost'2 HQ Hnâ— Hl_new").
+ + (* Accepted: contradiction *)
+ iDestruct "Accepted" as "[>Hl_ghost_inv _]".
+ iDestruct "Hl_ghost_inv" as (v) "Hlghost".
+ iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
+ by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
+ + (* Done: contradiction *)
+ iDestruct "Done" as "[QT >[Hlghost _]]".
+ iDestruct "Hlghost" as (v) "Hlghost".
+ iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
+ by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
+ - (* we are the failing thread *)
+ (* extract history and assert that it contains l *)
+ iDestruct (extract_snapshot with "Hâ—¯") as "#Hs1".
+ iAssert (|={⊤ ∖ ↑counterN}=> (⌜In l H1⌠∗ own γ_h (full_history_auth H1)))%I with "[Hâ—]" as "Hin". {
+ iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] State] | Done]]".
+ - iDestruct (sync_snapshot with "Hâ— Hhâ—¯") as %Hs1. iDestruct "Heq'" as %Heq'.
+ iModIntro. iSplitR "Hâ—".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft. iFrame. done. }
+ iModIntro. iFrame. iPureIntro. by eapply suffix_in_head.
+ - iDestruct "Done" as "[QT [>Hlghost Usedup]]".
+ iDestruct "Usedup" as (H') "[Hs >Usedup]". iDestruct "Usedup" as %[Hin Hn].
+ iMod (intuitionistically_elim with "Hs") as "Hs".
+ iDestruct (sync_snapshot with "Hâ— Hs") as %Hs'.
+ iModIntro. iSplitR "Hâ—".
+ { iNext. iExists _. iSplitL "Hp'"; first done. repeat iRight. iFrame.
+ iExists _. iSplit; last by iPureIntro. iDestruct "Hs" as "#Hs". iModIntro.
+ iApply "Hs". }
+ iModIntro. iSplit; last done.
+ iPureIntro. by eapply suffix_in.
+ }
+ (* close invariant *)
+ iMod "Hin" as (Hin) "Hâ—". iModIntro.
+ iSplitL "Hf Hc Hâ— Hâ—¯ Hbâ— Hrest Hl Hlh1". { iNext. iExists _, _, _, _. eauto with iFrame. }
+ (* two equal proofs depending on value of b1 *)
+ destruct b1; wp_if; [ wp_op | ..]; wp_alloc Hl_new as "Hl_new"; wp_pures;
+ iApply ((complete_failing_thread _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq Hin Hnl)
+ with "InvC InvS PAU Hs1 HQ Hl_new").
+ Qed.
+
+ (** ** Proof of [cinc] *)
+
+ Lemma cinc_spec c f γs :
+ is_counter γs (f, c) -∗
+ <<< ∀ (b : bool) (n : Z), counter_content γs (b, n) >>>
+ cinc (f, c)%V @⊤∖↑N
+ <<< counter_content γs (b, if b then n + 1 else n), RET #() >>>.
+ Proof.
+ iIntros "#InvC". iDestruct "InvC" as (γ_h γ_b γ_n f_l c_l) "[Heq InvC]".
+ iDestruct "Heq" as %[-> [=->->]]. iIntros (Φ) "AU". iLöb as "IH".
+ wp_lam. wp_proj. wp_let. wp_proj. wp_let. wp_bind (!_)%E.
+ iInv counterN as (b' l' H' q v) "[>Hf [>Hc [>[Hl Hl'] [>Hâ— [>Hâ—¯ [Hlh [>Heq [>Hbâ— Hv]]]]]]]]".
+ wp_load. simpl. iDestruct "Hv" as "[Hv|Hv]".
+ - iDestruct "Hv" as (n) "[% Hv]"; subst v.
+ iModIntro. iSplitR "Hl' AU".
+ { iModIntro. iExists _, _, _, (q/2)%Qp, (InjLV #n). eauto with iFrame. }
+ wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
+ iIntros (l_ghost p') "Hp'".
+ wp_let. wp_alloc ly as "Hly". wp_let. wp_bind (CAS _ _ _)%E.
+ (* open outer invariant to read c_l *)
+ iInv counterN as (b l'' H'' q' v') "[>Hf [>Hc [>Hl'2 [>Hâ— [>Hâ—¯ [>Hlh [>Heq [Hbâ— Hrest]]]]]]]]".
+ iDestruct "Heq" as %[Heq Hd].
+ (* assert that ly is not in the history *)
+ iDestruct (extract_snapshot with "Hâ—¯") as "#Hs".
+ iDestruct ((nodup_fresh_loc _ _ _ Hd) with "Hly Hlh") as %Hd'.
+ destruct (decide (l' = l'')) as [<- | Hn].
+ + (* CAS succeeds *)
+ wp_cas_suc.
+ (* We need to update the half history with `ly`.
+ For that we will need to get the second half of the history *)
+ iDestruct "Hrest" as "[InjL | InjR]";
+ iPoseProof (mapsto_agree with "Hl' Hl'2") as "#Heq"; last first.
+ { (* injR: contradiction *)
+ iDestruct "InjR" as (??) "[Heq' InjR_rest]".
+ iDestruct "Heq'" as %->. iDestruct "Heq" as %Heq'. inversion Heq'. }
+ (* injL: update history *)
+ iDestruct "InjL" as (n'') "[Heq' [Hâ—¯' Hnâ—]]".
+ iDestruct "Heq'" as %->. simpl. iDestruct "Heq" as %[=<-].
+ iPoseProof ((update_history _ _ ly) with "Hâ— Hâ—¯ Hâ—¯'") as ">[Hâ— [Hâ—¯' Hâ—¯'']]".
+ iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
+ iDestruct (own_alloc token) as ">Ht"; first by apply auth_auth_valid.
+ iDestruct "Ht" as (γ_t) "Token".
+ destruct (val_to_some_loc l_ghost) eqn:H.
+ * destruct (val_to_some_loc_some l_ghost l H) as [v1 [v2 [vs' [-> HCases]]]].
+ destruct HCases as [[-> ->] | Hl].
+ ++ iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ γ_t)
+ with "[AU Hâ—¯' Hp' Hnâ—]") as "#Hinv".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
+ iSplitL "Hâ—¯'"; first by iFrame. iLeft. by iFrame. }
+ iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
+ (* close invariant *)
+ iNext. iExists _, ly, _, _, _. iFrame.
+ iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
+ iRight. iExists _, _. iSplit; first done. iExists _, _, _, _. iSplit; done.
+ }
+ wp_if.
+ wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
+ ++ iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ ly l _ _ _ γ_t)
+ with "[AU Hâ—¯' Hp' Hnâ—]") as "#Hinv".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
+ iSplitL "Hâ—¯'"; first by iFrame. iLeft. iFrame. by rewrite H. }
+ iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
+ (* close invariant *)
+ iNext. iExists _, ly, _, _, _. iFrame.
+ iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
+ iRight. iExists _, _. iSplit; first done. iExists _, _, _, _. iSplit; done.
+ }
+ wp_if.
+ wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
+ * iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ ly l' _ _ _ γ_t)
+ with "[AU Hâ—¯' Hp' Hnâ—]") as "#Hinv".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
+ iSplitL "Hâ—¯'"; first by iFrame. iLeft. iFrame. by rewrite H. }
+ iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
+ (* close invariant *)
+ iNext. iExists _, ly, _, _, _. iFrame.
+ iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
+ iRight. iExists _, _. iSplit; first done. iExists _, _, _, _. iSplit; done.
+ }
+ wp_if.
+ wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
+ + (* CAS fails: closing invariant and invoking IH *)
+ wp_cas_fail.
+ iModIntro. iSplitR "Hl' AU".
+ iModIntro. iExists _, _, _, _. eauto 10 with iFrame.
+ wp_if. by iApply "IH".
+ - (* l' ↦ injR *)
+ iModIntro. iDestruct "Hv" as (n p) "[% Hrest]"; subst v.
+ (* extract state invariant *)
+ iDestruct "Hrest" as (P Q l_ghost γ_t) "[#InvS #P_AU]".
+ iSplitR "Hl' AU".
+ (* close invariant *)
+ { iModIntro. iExists _, _, _, _, _. iFrame. iRight. eauto 10 with iFrame. }
+ wp_let. wp_load. wp_match. repeat wp_proj.
+ wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ iIntros "_". wp_seq. by iApply "IH".
+ Qed.
+
+ Lemma new_counter_spec :
+ {{{ True }}}
+ new_counter #()
+ {{{ ctr γs, RET ctr ; is_counter γs ctr ∗ counter_content γs (true, 0) }}}.
+ Proof.
+ iIntros (Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
+ wp_alloc l_n as "Hl_n". wp_alloc l_c as "Hl_c". wp_let.
+ wp_alloc l_f as "Hl_f". wp_let. wp_pair.
+ iMod (own_alloc (full_history_auth [l_n] ⋅ full_history_frag [l_n])) as (γ_h) "[Hh◠Hh◯]".
+ { rewrite pair_op. apply pair_valid. split; by apply auth_both_valid. }
+ iMod (own_alloc (◠Excl' true ⋅ ◯ Excl' true)) as (γ_b) "[Hb◠Hb◯]".
+ { by apply auth_both_valid. }
+ iMod (own_alloc (◠Excl' 0 ⋅ ◯ Excl' 0)) as (γ_n) "[Hn◠Hn◯]".
+ { by apply auth_both_valid. }
+ iMod (inv_alloc counterN _ (counter_inv γ_h γ_b γ_n l_f l_c)
+ with "[Hl_f Hl_c Hl_n Hhâ— Hhâ—¯ Hbâ— Hnâ—]") as "#InvC".
+ { iNext. iDestruct "Hhâ—¯" as "[Hhâ—¯1 Hhâ—¯2]". iDestruct "Hl_n" as "[Hl_n1 Hl_n2]".
+ iExists true, l_n, [l_n], _, (InjLV #0). iFrame.
+ iSplitL "Hl_n1". { simpl. iSplitL; last done. by iExists _, _. }
+ iSplitR. { iPureIntro. split; first done. apply NoDup_cons. apply in_nil. apply NoDup_nil. }
+ iLeft. iExists 0. iSplitR; first done. iFrame. }
+ iModIntro.
+ iApply ("HΦ" $! (#l_f, #l_c)%V (γ_h, γ_b, γ_n)).
+ iSplitR; last by iFrame. iExists γ_h, γ_b, γ_n, l_f, l_c. iSplit; done.
+ Qed.
+
+ Lemma set_flag_spec γs f c (new_b : bool) :
+ is_counter γs (f, c) -∗
+ <<< ∀ (b : bool) (n : Z), counter_content γs (b, n) >>>
+ set_flag (f, c)%V #new_b @⊤∖↑N
+ <<< counter_content γs (new_b, n), RET #() >>>.
+ Proof.
+ iIntros "#InvC" (Φ) "AU". wp_lam. wp_let. wp_proj.
+ iDestruct "InvC" as (γ_h γ_b γ_n l_f l_c) "[[HEq1 HEq2] InvC]".
+ iDestruct "HEq1" as %->. iDestruct "HEq2" as %HEq. inversion HEq; subst; clear HEq.
+ iInv counterN as (b c H q v) "[>Hl_f [>Hl_c [>Hl [>Hâ— [>Hâ—¯ [>HlH [>HEq [Hbâ— H]]]]]]]]".
+ iMod "AU" as (b' n') "[[Hbâ—¯ Hnâ—¯] [_ Hclose]]"; simpl.
+ wp_store.
+ iDestruct (sync_flag_values with "Hbâ— Hbâ—¯") as %HEq; subst b.
+ iDestruct (update_flag_value with "Hbâ— Hbâ—¯") as ">[Hbâ— Hbâ—¯]".
+ iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame.
+ iModIntro. iModIntro. iSplitR "HΦ"; last done.
+ iNext. iExists new_b, c, H, q, v. iFrame.
+ Qed.
+
+ Lemma get_spec γs f c :
+ is_counter γs (f, c) -∗
+ <<< ∀ (b : bool) (n : Z), counter_content γs (b, n) >>>
+ get (f, c)%V @⊤∖↑N
+ <<< counter_content γs (b, n), RET #n >>>.
+ Proof.
+ iIntros "#InvC" (Φ) "AU". iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
+ iDestruct "InvC" as (γ_h γ_b γ_n l_f l_c) "[[HEq1 HEq2] InvC]".
+ iDestruct "HEq1" as %->. iDestruct "HEq2" as %HEq. inversion HEq; subst.
+ iInv counterN as (b c H q v) "[>Hl_f [>Hl_c [>[Hc Hc'] [>Hâ— [>Hâ—¯ [>HlH [>HEq [Hbâ— [H|H]]]]]]]]]".
+ - wp_load. iDestruct "H" as (n) "[% [Hâ—¯2 Hnâ—]]". simpl in *; subst v.
+ iMod "AU" as (au_b au_n) "[[Hbâ—¯ Hnâ—¯] [_ Hclose]]"; simpl.
+ iDestruct (sync_counter_values with "Hnâ— Hnâ—¯") as %->.
+ iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame.
+ iModIntro. iSplitR "HΦ Hc'". {
+ iNext. iExists b, c, H, (q/2)%Qp, (InjLV #au_n). iFrame.
+ iLeft. iExists au_n. iFrame. done.
+ }
+ wp_let. wp_load. wp_match. iApply "HΦ".
+ - wp_load. iDestruct "H" as (n p) "[% H]". simpl in *; subst v.
+ iDestruct "H" as (P Q l_ghost γ_t) "[#InvS #PAU]".
+ iModIntro. iSplitR "AU Hc'". {
+ iNext. iExists b, c, H, (q/2)%Qp, (InjRV(#n,#p)). iFrame.
+ iRight. iExists n, p. iSplit; first done. iExists P, Q, l_ghost, γ_t. eauto.
+ }
+ wp_let. wp_load. wp_match. repeat wp_proj. wp_bind (complete _ _ _ _ _)%E.
+ wp_apply complete_spec; [ iExists _, _, _, _, _; eauto | done | done | done | .. ].
+ iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
+ Qed.
+
+End conditional_counter.
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 93723832e78bffcf0b8710bb9d2a4db398e6e6b6..026750bd8f2e0cf4c4dced3997234ff2bc65a262 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -365,10 +365,10 @@ Section atomic_snapshot.
wp_load. eauto.
Qed.
- Definition val_list_to_bool (v : list val) : bool :=
+ Definition prophecy_to_bool (v : list (val * val)) : bool :=
match v with
- | LitV (LitBool b) :: _ => b
- | _ => false
+ | (_, LitV (LitBool b)) :: _ => b
+ | _ => false
end.
Lemma readPair_spec γ p :
@@ -413,7 +413,7 @@ Section atomic_snapshot.
iMod "AU" as (xv yv) "[Hpair Hclose]".
rewrite /pair_content.
iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- destruct (val_list_to_bool proph_val) eqn:Hproph.
+ destruct (prophecy_to_bool proph_val) eqn:Hproph.
- (* prophecy value is predicting that timestamp has not changed, so we commit *)
(* committing AU *)
iMod ("Hclose" with "Hpair") as "HΦ".